Fix initial validator set in model and driver

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,42 @@ 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,
+					&initialValSet,
 					consumerSigners,
 					nodes,
 					valNames,
 					driver.providerChain(),
 					topN,
+					validatorsToOptIn,
 				)
 			}
 
@@ -690,7 +723,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

@@ -32,6 +32,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 +311,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 +347,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)
 
@@ -387,6 +388,11 @@ 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)
+	}
+
 	// 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))
@@ -443,6 +449,7 @@ func (s *Driver) setupConsumer(
 	valNames []string,
 	providerChain *ibctesting.TestChain,
 	topN int64,
+	validatorsToOptIn []*providertypes.ProviderConsAddress,
 ) {
 	s.t.Logf("Starting consumer %v", chain)
 
@@ -455,14 +462,15 @@ func (s *Driver) setupConsumer(
 	consumerChain := newChain(s.t, params, s.coordinator, icstestingutils.ConsumerAppIniter(initValUpdates), chain, valSet, signers, nodes, valNames)
 	s.coordinator.Chains[chain] = consumerChain
 
-	path := s.ConfigureNewPath(consumerChain, providerChain, params, uint32(topN))
+	valUpdates := cmttypes.TM2PB.ValidatorUpdates(valSet)
+
+	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 +487,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)
     }
 }
 
@@ -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

tests/mbt/model/ccv_model.qnt

@@ -240,7 +240,7 @@ module ccv_model {
 
         val consumerStatus = currentState.providerState.consumerStatus
         nondet consumersToStart = oneOf(nonConsumers.powerset())
-        val consumerAdditions = consumersToStart.map(chain => NewFullConsumer(chain))
+        val consumerAdditions = consumersToStart.map(chain => NewFullConsumer(chain, Set()))
         nondet consumersToStop = oneOf(runningConsumers.powerset())
         nondet timeAdvancement = oneOf(timeAdvancements)
         EndAndBeginBlockForProvider(timeAdvancement, consumerAdditions, consumersToStop),
@@ -321,7 +321,9 @@ module ccv_model {
             assert(newest(Set(packet1, packet2, packet3)) == packet3),
             assert(newest(Set(packet3, packet2, packet1)) == packet3),
         }
-    }        
+    }
+
+    val currentProviValSet = currentState.providerState.chainState.currentValidatorSet
 
     // ==================
     // INVARIANT CHECKS
@@ -528,7 +530,7 @@ module ccv_model {
                 // the validator set has changed
                 assert(currentState.providerState.chainState.currentValidatorSet == InitialValidatorSet.put("node1", 150)),
                 // start consumer1
-                EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer1")), Set())
+                EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer1", Set())), Set())
             })
             .then(
                 all {
@@ -606,7 +608,7 @@ module ccv_model {
     run SameVscPacketsManualTest =
         init.then(
             // start all consumers except for consumer3
-            EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer1"), NewFullConsumer("consumer2")), Set())
+            EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer1", Set()), NewFullConsumer("consumer2", Set())), Set())
         ).then(
             // change voting power
             VotingPowerChange("node1", 50)
@@ -621,7 +623,7 @@ module ccv_model {
             DeliverVscPacket("consumer2")
         ).then(
             // start consumer3
-            EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer3")), Set())
+            EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer3", Set())), Set())
         ).then(
             // do another voting power change
             VotingPowerChange("node2", 50)
@@ -652,7 +654,7 @@ module ccv_model {
         init
         .then(
             // start all consumer chains
-            EndAndBeginBlockForProvider(1 * Second, ConsumerChains.map(c => NewFullConsumer(c)), Set())
+            EndAndBeginBlockForProvider(1 * Second, ConsumerChains.map(c => NewFullConsumer(c, Set())), Set())
         )
         .then(
             // change voting power
@@ -865,7 +867,7 @@ module ccv_model {
         init
         .then(
             // start all consumer chains
-            EndAndBeginBlockForProvider(1 * Second, consumerChains.map(c => NewFullConsumer(c)), Set())
+            EndAndBeginBlockForProvider(1 * Second, consumerChains.map(c => NewFullConsumer(c, Set())), Set())
         )
         .then(
             // node 1 assigns a key on consumer1
@@ -937,7 +939,7 @@ module ccv_model {
             VotingPowerChange("node1", 50)
         )
         .then(
-            EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer1"), NewFullConsumer("consumer2")), Set())
+            EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer1", Set()), NewFullConsumer("consumer2", Set())), Set())
         ).then(
             all {
                 ValidatorSetHasExistedKeyAssignmentInv,

tests/mbt/model/ccv_test.qnt

@@ -248,7 +248,7 @@ module ccv_test {
         )
         val res = StartStopConsumers(
             GetEmptyProviderState.with("consumerStatus", currentConsumerStatusMap),
-            Set(NewOptInConsumer("chain1")),
+            Set(NewOptInConsumer("chain1", Set())),
             Set("chain2"),
             Set()
         )
@@ -267,7 +267,7 @@ module ccv_test {
         )
         val res = StartStopConsumers(
             GetEmptyProviderState.with("consumerStatus", currentConsumerStatusMap),
-            Set(NewOptInConsumer("chain2")),
+            Set(NewOptInConsumer("chain2", Set())),
             Set("chain3"),
             Set()
         )
@@ -283,7 +283,7 @@ module ccv_test {
         )
         val res = StartStopConsumers(
             GetEmptyProviderState.with("consumerStatus", currentConsumerStatusMap),
-            Set(NewOptInConsumer("chain1")),
+            Set(NewOptInConsumer("chain1", Set())),
             Set("chain3"),
             Set()
         )
@@ -299,7 +299,7 @@ module ccv_test {
         )
         val res = StartStopConsumers(
             GetEmptyProviderState.with("consumerStatus", currentConsumerStatusMap),
-            Set(NewOptInConsumer("chain1")),
+            Set(NewOptInConsumer("chain1", Set())),
             Set("chain1"),
             Set()
         )

tests/mbt/model/ccv_utils.qnt

@@ -491,4 +491,27 @@ module ccv_utils {
                     acc.put(node, valSet.get(node))
                 }
         )
+
+    // For each new consumer addition, opts in all the validators that voted yes.
+    pure def OptInYesVoters(providerState: ProviderState, consumers: Set[ConsumerAdditionMsg]): ProviderState = {
+        val consumerToYesVoters = 
+            consumers.fold(
+                Map(),
+                (acc, consumer) => acc.put(consumer.chain, consumer.yesVoters)
+            )
+        providerState.with(
+            "optedInVals",
+            providerState.optedInVals.keys().mapBy(
+                (consumer) => 
+                val prevOptedInVals = providerState.optedInVals.get(consumer)
+                prevOptedInVals.union(consumerToYesVoters.getOrElse(consumer, Set()))
+            )
+        )
+    }
+
+    pure def IsEmptyValSet(valSet: ValidatorSet): bool = {
+        valSet.keys().filter(
+            node => valSet.get(node) > 0
+        ).size() == 0
+    }
 }