Fix: MBT for PSS

proto/interchain_security/ccv/provider/v1/provider.proto

@@ -326,16 +326,3 @@ message ConsumerRewardsAllocation {
     (gogoproto.castrepeated) = "github.com/cosmos/cosmos-sdk/types.DecCoins"
   ];
 }
-
-// OptedInValidator is used to store a opted-in validator 
-// to a consumer chain with the following mapping:  (chainID, providerAddr) -> optedInValidator
-message OptedInValidator {
-  // validator address
-  bytes provider_addr = 1;
-  // block height at which the validator opted-in
-  int64 block_height = 2;
-  // validator voting power at the block it opted-in
-  int64 power = 3;
-  // public key used by the validator on the consumer
-  bytes public_key = 4;
-}

tests/e2e/actions.go

@@ -278,6 +278,7 @@ func (tr TestConfig) submitConsumerAdditionProposal(
 		UnbondingPeriod:                   params.UnbondingPeriod,
 		Deposit:                           fmt.Sprint(action.Deposit) + `stake`,
 		DistributionTransmissionChannel:   action.DistributionChannel,
+		TopN:                              100,
 	}
 
 	bz, err := json.Marshal(prop)

tests/mbt/driver/mbt_test.go

@@ -210,6 +210,12 @@ func RunItfTrace(t *testing.T, path string) {
 
 	t.Log("Reading the trace...")
 
+	// maps from string representations of cmttypes.Addresses to monikers
+	reverseAddressMap := make(map[string]string, len(addressMap))
+	for k, v := range addressMap {
+		reverseAddressMap[string(v.Address)] = k
+	}
+
 	for index, state := range trace.States {
 		t.Log("Height modulo epoch length:", driver.providerChain().CurrentHeader.Height%blocksPerEpoch)
 		t.Log("Model height modulo epoch length:", ProviderHeight(state.VarValues["currentState"].Value.(itf.MapExprType))%modelBlocksPerEpoch)
@@ -315,15 +321,41 @@ func RunItfTrace(t *testing.T, path string) {
 			for _, consumer := range consumersToStart {
 				chainId := consumer.Value.(itf.MapExprType)["chain"].Value.(string)
 				topN := consumer.Value.(itf.MapExprType)["topN"].Value.(int64)
+				yesVoters := consumer.Value.(itf.MapExprType)["yesVoters"].Value.(itf.ListExprType)
+				yesVotersMap := make(map[string]bool, len(yesVoters))
+				for _, voter := range yesVoters {
+					yesVotersMap[voter.Value.(string)] = true
+				}
+
+				initialValSet := cmttypes.ValidatorSet{}
+				for _, val := range driver.providerChain().Vals.Validators {
+					moniker := reverseAddressMap[string(val.Address)]
+					if _, ok := yesVotersMap[moniker]; ok {
+						initialValSet.Validators = append(initialValSet.Validators, val)
+					}
+				}
+				initialValSet.Proposer = driver.providerChain().Vals.Proposer
+
+				// opt the yes voters in, which would usually have been done for each one after voting on the proposal
+				// which we do not model
+				validatorsToOptIn := make([]*providertypes.ProviderConsAddress, 0)
+				for _, monikerExpr := range yesVoters {
+					moniker := monikerExpr.Value.(string)
+					valAddr := addressMap[moniker].Address
+					consAddr, err := sdktypes.ConsAddressFromHex(valAddr.String())
+					require.NoError(t, err, "Error getting consensus address from hex")
+					validatorsToOptIn = append(validatorsToOptIn, &providertypes.ProviderConsAddress{Address: consAddr})
+				}
+
 				driver.setupConsumer(
 					chainId,
 					modelParams,
-					driver.providerChain().Vals,
 					consumerSigners,
 					nodes,
 					valNames,
 					driver.providerChain(),
 					topN,
+					validatorsToOptIn,
 				)
 			}
 
@@ -690,7 +722,7 @@ func CompareValSet(modelValSet map[string]itf.Expr, systemValSet map[string]int6
 	}
 
 	if !reflect.DeepEqual(expectedValSet, actualValSet) {
-		return fmt.Errorf("Validator sets do not match: (+ expected, - actual): %v", pretty.Compare(expectedValSet, actualValSet))
+		return fmt.Errorf("Validator sets do not match: (- expected, + actual): %v", pretty.Compare(expectedValSet, actualValSet))
 	}
 	return nil
 }

tests/mbt/driver/setup.go

@@ -1,6 +1,7 @@
 package main
 
 import (
+	"bytes"
 	"encoding/json"
 	"log"
 	"testing"
@@ -13,6 +14,8 @@ import (
 	ibctesting "github.com/cosmos/ibc-go/v7/testing"
 	"github.com/stretchr/testify/require"
 
+	ce "github.com/cometbft/cometbft/crypto/encoding"
+
 	"cosmossdk.io/math"
 
 	"github.com/cosmos/cosmos-sdk/baseapp"
@@ -32,6 +35,7 @@ import (
 	"github.com/cosmos/interchain-security/v4/testutil/integration"
 	simibc "github.com/cosmos/interchain-security/v4/testutil/simibc"
 	consumertypes "github.com/cosmos/interchain-security/v4/x/ccv/consumer/types"
+	providertypes "github.com/cosmos/interchain-security/v4/x/ccv/provider/types"
 	ccvtypes "github.com/cosmos/interchain-security/v4/x/ccv/types"
 )
 
@@ -310,7 +314,7 @@ func newChain(
 // Creates a path for cross-chain validation from the consumer to the provider and configures the channel config of the endpoints
 // as well as the clients.
 // this function stops when there is an initialized, ready-to-relay channel between the provider and consumer.
-func (s *Driver) ConfigureNewPath(consumerChain, providerChain *ibctesting.TestChain, params ModelParams, topN uint32) *ibctesting.Path {
+func (s *Driver) ConfigureNewPath(consumerChain, providerChain *ibctesting.TestChain, params ModelParams, topN uint32, valsToOptIn []*providertypes.ProviderConsAddress, initialValSet []abcitypes.ValidatorUpdate) *ibctesting.Path {
 	consumerChainId := ChainId(consumerChain.ChainID)
 
 	path := ibctesting.NewPath(consumerChain, providerChain)
@@ -346,7 +350,7 @@ func (s *Driver) ConfigureNewPath(consumerChain, providerChain *ibctesting.TestC
 		[]string{"upgrade", "upgradedIBCState"},
 	)
 
-	consumerGenesis := createConsumerGenesis(params, providerChain, consumerClientState)
+	consumerGenesis := createConsumerGenesis(params, providerChain, consumerClientState, initialValSet)
 
 	s.consumerKeeper(consumerChainId).InitGenesis(s.ctx(consumerChainId), consumerGenesis)
 
@@ -373,9 +377,6 @@ func (s *Driver) ConfigureNewPath(consumerChain, providerChain *ibctesting.TestC
 		stakingValidators = append(stakingValidators, v)
 	}
 
-	nextValidators := s.providerKeeper().ComputeNextEpochConsumerValSet(s.providerCtx(), string(consumerChainId), stakingValidators)
-	s.providerKeeper().SetConsumerValSet(s.providerCtx(), string(consumerChainId), nextValidators)
-
 	err = s.providerKeeper().SetConsumerGenesis(
 		providerChain.GetContext(),
 		string(consumerChainId),
@@ -387,6 +388,16 @@ func (s *Driver) ConfigureNewPath(consumerChain, providerChain *ibctesting.TestC
 	// TODO: might be able to move this into setupConsumer, need to test once more logic is here
 	s.providerKeeper().SetTopN(providerChain.GetContext(), consumerChain.ChainID, topN)
 
+	// Opt-in validators to the consumer chain
+	for _, addr := range valsToOptIn {
+		s.providerKeeper().HandleOptIn(s.providerCtx(), consumerChain.ChainID, *addr, nil)
+	}
+
+	nextValidators := s.providerKeeper().ComputeNextEpochConsumerValSet(s.providerCtx(), string(consumerChainId), stakingValidators, func(validator stakingtypes.Validator) bool {
+		return s.providerKeeper().ShouldConsiderOnlyOptIn(s.providerCtx(), string(consumerChainId), validator)
+	})
+	s.providerKeeper().SetConsumerValSet(s.providerCtx(), string(consumerChainId), nextValidators)
+
 	// Client ID is set in InitGenesis and we treat it as a black box. So
 	// must query it to use it with the endpoint.
 	clientID, _ := s.consumerKeeper(consumerChainId).GetProviderClientID(s.ctx(consumerChainId))
@@ -437,32 +448,63 @@ func (s *Driver) setupProvider(
 func (s *Driver) setupConsumer(
 	chain string,
 	params ModelParams,
-	valSet *cmttypes.ValidatorSet, // the current validator set on the provider chain
 	signers map[string]cmttypes.PrivValidator, // a map of validator addresses to private validators (signers)
 	nodes []*cmttypes.Validator, // the list of nodes, even ones that have no voting power initially
 	valNames []string,
 	providerChain *ibctesting.TestChain,
 	topN int64,
+	validatorsToOptIn []*providertypes.ProviderConsAddress,
 ) {
 	s.t.Logf("Starting consumer %v", chain)
 
-	// TODO: reuse the partial set computation logic to compute the initial validator set
-	// for top N chains
-	initValUpdates := cmttypes.TM2PB.ValidatorUpdates(valSet)
+	minPowerToOptIn := s.providerKeeper().ComputeMinPowerToOptIn(s.providerCtx(), chain, s.providerValidatorSet(), uint32(topN))
+
+	valSet := s.providerChain().Vals
+
+	// Filter out all the validators that do not either a) have power at least minPowerToOptIn, or b) are in the validatorsToOptIn slice
+	filteredValSet := make([]*cmttypes.Validator, 0)
+	for _, val := range valSet.Validators {
+		if val.VotingPower >= minPowerToOptIn && topN > 0 {
+			filteredValSet = append(filteredValSet, val)
+			continue
+		}
+		for _, optInVal := range validatorsToOptIn {
+			if bytes.Equal(val.Address, optInVal.Address.Bytes()) {
+				filteredValSet = append(filteredValSet, val)
+				break
+			}
+		}
+	}
+
+	initValSet := cmttypes.ValidatorSet{Validators: filteredValSet, Proposer: filteredValSet[0]}
+	initValUpdates := cmttypes.TM2PB.ValidatorUpdates(&initValSet)
 
 	// start consumer chains
 	s.t.Logf("Creating consumer chain %v", chain)
-	consumerChain := newChain(s.t, params, s.coordinator, icstestingutils.ConsumerAppIniter(initValUpdates), chain, valSet, signers, nodes, valNames)
+	consumerChain := newChain(s.t, params, s.coordinator, icstestingutils.ConsumerAppIniter(initValUpdates), chain, &initValSet, signers, nodes, valNames)
 	s.coordinator.Chains[chain] = consumerChain
 
-	path := s.ConfigureNewPath(consumerChain, providerChain, params, uint32(topN))
+	valUpdates := cmttypes.TM2PB.ValidatorUpdates(&initValSet)
+	consumerVals := make([]providertypes.ConsumerValidator, len(initValSet.Validators))
+	for i, val := range initValSet.Validators {
+		pk, err := ce.PubKeyToProto(val.PubKey)
+		require.NoError(s.t, err)
+
+		consumerVals[i] = providertypes.ConsumerValidator{
+			ProviderConsAddr:  val.Address,
+			Power:             val.VotingPower,
+			ConsumerPublicKey: &pk,
+		}
+	}
+	s.providerKeeper().SetConsumerValSet(s.providerCtx(), chain, consumerVals)
+
+	path := s.ConfigureNewPath(consumerChain, providerChain, params, uint32(topN), validatorsToOptIn, valUpdates)
 	s.simibcs[ChainId(chain)] = simibc.MakeRelayedPath(s.t, path)
 }
 
-func createConsumerGenesis(modelParams ModelParams, providerChain *ibctesting.TestChain, consumerClientState *ibctmtypes.ClientState) *consumertypes.GenesisState {
+func createConsumerGenesis(modelParams ModelParams, providerChain *ibctesting.TestChain, consumerClientState *ibctmtypes.ClientState, initialValSet []abcitypes.ValidatorUpdate) *consumertypes.GenesisState {
 	providerConsState := providerChain.LastHeader.ConsensusState()
 
-	valUpdates := cmttypes.TM2PB.ValidatorUpdates(providerChain.Vals)
 	params := ccvtypes.NewParams(
 		true,
 		1000, // ignore distribution
@@ -479,5 +521,5 @@ func createConsumerGenesis(modelParams ModelParams, providerChain *ibctesting.Te
 		ccvtypes.DefaultRetryDelayPeriod,
 	)
 
-	return consumertypes.NewInitialGenesisState(consumerClientState, providerConsState, valUpdates, params)
+	return consumertypes.NewInitialGenesisState(consumerClientState, providerConsState, initialValSet, params)
 }

tests/mbt/model/ccv.qnt

@@ -244,27 +244,31 @@ module ccv_types {
     // In particular, holds:
     // the chain name/identifier,
     // and the top N factor for the chain.
+    // the set of nodes that votes yes on the proposal (we don't model the actual voting process, but use this only to set the initial set of opted-in nodes)
     type ConsumerAdditionMsg = {
         chain: Chain,
-        topN: int
+        topN: int,
+        yesVoters: Set[Node],
     }
 
-    // Creates a new ConsumerAdditionMsg with a given top N.
-    pure def NewTopNConsumer(chain: Chain, topN: int): ConsumerAdditionMsg = {
+    // Creates a new ConsumerAdditionMsg with a given top N and given set of nodes that voted yes.
+    pure def NewTopNConsumer(chain: Chain, topN: int, yesVoters: Set[Node]): ConsumerAdditionMsg = {
         {
             chain: chain,
-            topN: topN
+            topN: topN,
+            yesVoters: yesVoters
         }
     }
 
-    // Creates a new ConsumerAdditionMsg with topN = 0.
-    pure def NewOptInConsumer(chain: Chain): ConsumerAdditionMsg = {
-        NewTopNConsumer(chain, 0)
+    // Creates a new ConsumerAdditionMsg with topN = 0 and given set of nodes that voted yes.
+    pure def NewOptInConsumer(chain: Chain, yesVoters: Set[Node]): ConsumerAdditionMsg = {
+        NewTopNConsumer(chain, 0, yesVoters)
     }
 
     // Creates a new ConsumerAdditionMsg with top N = 100%.
-    pure def NewFullConsumer(chain: Chain): ConsumerAdditionMsg = {
-        NewTopNConsumer(chain, 100)
+    // Yes voters don't really matter - the chain will force everyone to validate anyways.
+    pure def NewFullConsumer(chain: Chain, yesVoters: Set[Node]): ConsumerAdditionMsg = {
+        NewTopNConsumer(chain, 100, yesVoters)
     }
 }
 
@@ -339,7 +343,7 @@ module ccv {
                 } else {
                     // set the validator set changed flag
                     val newProviderState = currentState.providerState.with(
-                        "consumersWithPowerChangesInThisEpoch", getRunningConsumers(currentState.providerState)
+                        "consumersWithPowerChangesInThisEpoch", getRunningConsumers(currentState.providerState).filter(consumer => currentState.providerState.optedInVals.get(consumer).contains(validator))
                     )
                     pure val tmpState = currentState.with(
                         "providerState", newProviderState
@@ -511,28 +515,33 @@ module ccv {
         // for each running consumer chain, opt in validators that are in the top N
         val providerStateAfterPSS = providerStateAfterConsumerAdvancement.endBlockPSS()
 
+        // for each new consumer addition, opt in the validators that voted yes
+        val providerStateAfterPSSAndYesOptIns = providerStateAfterPSS.OptInYesVoters(consumersToStart)
+
         if (err != "") {
             Err(err)
+        } else if (providerStateAfterConsumerAdvancement.chainState.votingPowerHistory.head().IsEmptyValSet()) {
+            Err("Validator set would be empty after ending this block!")
         } else {
             // for each consumer chain, apply the key assignment to the current validator set
-            val currentValSets = getRunningConsumers(providerStateAfterPSS).mapBy(
+            val currentValSets = getRunningConsumers(providerStateAfterPSSAndYesOptIns).mapBy(
                 (consumer) => 
-                providerStateAfterPSS.applyKeyAssignmentToValSet(
+                providerStateAfterPSSAndYesOptIns.applyKeyAssignmentToValSet(
                     consumer,
                     // get the validator set after partial set security has been applied
-                    GetPSSValidatorSet(providerStateAfterPSS, curValSet, consumer)
+                    GetPSSValidatorSet(providerStateAfterPSSAndYesOptIns, curValSet, consumer)
                 )
             )
 
             // store the current validator set with the key assignments applied in the history
             val newKeyAssignedValSetHistory = currentValSets.keys().mapBy(
                 (consumer) => 
-                providerStateAfterPSS.keyAssignedValSetHistory
+                providerStateAfterPSSAndYesOptIns.keyAssignedValSetHistory
                     .getOrElse(consumer, List()) // get the existing history (empty list if no history yet)
                     .prepend(currentValSets.get(consumer)) // prepend the current validator set with key assignments applied
             )
 
-            val providerStateAfterStoringValSets = providerStateAfterPSS.with(
+            val providerStateAfterStoringValSets = providerStateAfterPSSAndYesOptIns.with(
                 "keyAssignedValSetHistory", newKeyAssignedValSetHistory
             )
 

tests/mbt/model/ccv_boundeddrift.qnt

@@ -81,11 +81,15 @@ module ccv_boundeddrift {
         val possibleAdvancements = timeAdvancements.filter(t => t <= maxAdv)
         all {
             possibleAdvancements.size() > 0, // ensure there is a possible advancement, otherwise this action does not make sense
+            currentProviValSet.keys().filter(v => currentProviValSet.get(v) > 0).size() > 0, // ensure that at least one validator has positive voting power
             // advance a block for the provider
             val consumerStatus = currentState.providerState.consumerStatus
             nondet consumersToStart = oneOf(nonConsumers.powerset())
             nondet topN = oneOf(topNOracle)
-            nondet consumerAdditions = consumersToStart.map(c => Ccvt::NewTopNConsumer(c, topN))
+            // TODO: once we merge slashing, this also needs to filter jailed validators out! (leaving this comment here as a reminder)
+            // get a random subset of the current validator set as yes voters
+            nondet yesVoters = oneOf(currentProviValSet.keys().filter(v => currentProviValSet.get(v) > 0).powerset().filter(s => s.size() > 0)) // get rid of the empty set
+            nondet consumerAdditions = consumersToStart.map(c => Ccvt::NewTopNConsumer(c, topN, yesVoters))
             // make it so we stop consumers only with small likelihood:
             nondet stopConsumersRand = oneOf(1.to(100))
             nondet consumersToStop = if (stopConsumersRand <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set()
@@ -118,23 +122,6 @@ module ccv_boundeddrift {
         nondetKeyAssignment,
         StepOptIn,
         StepOptOut,
-
-        // advance a block for the provider
-        val maxAdv = findMaxTimeAdvancement(GetChainState(Ccvt::PROVIDER_CHAIN), GetOtherChainStates(Ccvt::PROVIDER_CHAIN), maxDrift)
-        val possibleAdvancements = timeAdvancements.filter(t => t <= maxAdv)
-        all {
-            possibleAdvancements.size() > 0, // ensure there is a possible advancement, otherwise this action does not make sense
-            // advance a block for the provider
-            val consumerStatus = currentState.providerState.consumerStatus
-            nondet consumersToStart = oneOf(nonConsumers.powerset())
-            nondet topN = oneOf(variousPossibleTopN)
-            nondet consumerAdditions = consumersToStart.map(c => Ccvt::NewTopNConsumer(c, topN))
-            // make it so we stop consumers only with small likelihood:
-            nondet stopConsumersRand = oneOf(1.to(100))
-            nondet consumersToStop = if (stopConsumersRand <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set()
-            nondet timeAdvancement = oneOf(possibleAdvancements)
-            EndAndBeginBlockForProvider(timeAdvancement, consumerAdditions, consumersToStop),
-        }
     }
 
     // INVARIANT