diff --git a/tests/mbt/driver/mbt_test.go b/tests/mbt/driver/mbt_test.go index 67923b76da..c48538b300 100644 --- a/tests/mbt/driver/mbt_test.go +++ b/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 } diff --git a/tests/mbt/driver/setup.go b/tests/mbt/driver/setup.go index 6408f0e873..8247a212f1 100644 --- a/tests/mbt/driver/setup.go +++ b/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) } diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index 6941dc8a73..9f95abf1df 100644 --- a/tests/mbt/model/ccv.qnt +++ b/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 ) diff --git a/tests/mbt/model/ccv_boundeddrift.qnt b/tests/mbt/model/ccv_boundeddrift.qnt index 2552304816..03665a0ea1 100644 --- a/tests/mbt/model/ccv_boundeddrift.qnt +++ b/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 diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt index fcd7897de1..4bb368ae3f 100644 --- a/tests/mbt/model/ccv_model.qnt +++ b/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, diff --git a/tests/mbt/model/ccv_test.qnt b/tests/mbt/model/ccv_test.qnt index af49ecfa14..5ab2dcd8bc 100644 --- a/tests/mbt/model/ccv_test.qnt +++ b/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() ) diff --git a/tests/mbt/model/ccv_utils.qnt b/tests/mbt/model/ccv_utils.qnt index 4e4582fd06..ff02244e10 100644 --- a/tests/mbt/model/ccv_utils.qnt +++ b/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 + } } \ No newline at end of file