diff --git a/tests/difference/core/quint_model/driver/core.go b/tests/difference/core/quint_model/driver/core.go index 6fb993b2c4..68d6f6fcd6 100644 --- a/tests/difference/core/quint_model/driver/core.go +++ b/tests/difference/core/quint_model/driver/core.go @@ -7,6 +7,7 @@ import ( "testing" "time" + tendermint "github.com/cosmos/ibc-go/v7/modules/light-clients/07-tendermint" ibctesting "github.com/cosmos/ibc-go/v7/testing" "github.com/stretchr/testify/require" @@ -15,6 +16,7 @@ import ( stakingkeeper "github.com/cosmos/cosmos-sdk/x/staking/keeper" stakingtypes "github.com/cosmos/cosmos-sdk/x/staking/types" consumertypes "github.com/cosmos/interchain-security/v3/x/ccv/consumer/types" + providertypes "github.com/cosmos/interchain-security/v3/x/ccv/provider/types" appConsumer "github.com/cosmos/interchain-security/v3/app/consumer" appProvider "github.com/cosmos/interchain-security/v3/app/provider" @@ -23,6 +25,7 @@ import ( consumerkeeper "github.com/cosmos/interchain-security/v3/x/ccv/consumer/keeper" providerkeeper "github.com/cosmos/interchain-security/v3/x/ccv/provider/keeper" + abcitypes "github.com/cometbft/cometbft/abci/types" cmttypes "github.com/cometbft/cometbft/types" ) @@ -96,7 +99,17 @@ func (s *Driver) height(chain ChainId) int64 { // time returns the time of the current header of chain func (s *Driver) time(chain ChainId) time.Time { - return s.chain(chain).CurrentHeader.Time + testChain := s.chain(chain) + return testChain.CurrentHeader.Time +} + +func (s *Driver) allTimes() map[ChainId]time.Time { + chains := s.coordinator.Chains + times := make(map[ChainId]time.Time, len(chains)) + for _, chain := range chains { + times[ChainId(chain.ChainID)] = chain.CurrentHeader.Time + } + return times } // delegator retrieves the address for the delegator account @@ -385,7 +398,8 @@ func (s *Driver) getChainStateString(chain ChainId) string { // as witnessed by events, and adds them to the correct paths. // It also updates the client header on the paths // that involve the chain. -func (s *Driver) endAndBeginBlock(chain ChainId, timeAdvancement time.Duration) { +// Returns the header of the chain. +func (s *Driver) endAndBeginBlock(chain ChainId, timeAdvancement time.Duration) *tendermint.Header { testChain, found := s.coordinator.Chains[string(chain)] require.True(s.t, found, "chain %s not found", chain) @@ -408,17 +422,29 @@ func (s *Driver) endAndBeginBlock(chain ChainId, timeAdvancement time.Duration) for _, path := range s.simibcs { if path.InvolvesChain(string(chain)) { - path.AddClientHeader(string(chain), header) path.Outboxes.Commit(string(chain)) } } simibc.BeginBlock(testChain, timeAdvancement) + return header +} - for _, path := range s.simibcs { - if path.InvolvesChain(string(chain)) { - path.UpdateClient(path.Counterparty(string(chain))) - } +func (s *Driver) runningConsumers() []providertypes.Chain { + return s.providerKeeper().GetAllConsumerChains(s.providerCtx()) +} + +func (s *Driver) setTime(chain ChainId, newTime time.Time) { + testChain, found := s.coordinator.Chains[string(chain)] + require.True(s.t, found, "chain %s not found", chain) + + testChain.CurrentHeader.Time = newTime + testChain.App.BeginBlock(abcitypes.RequestBeginBlock{Header: testChain.CurrentHeader}) +} + +func (s *Driver) setAllTimes(newTimes map[ChainId]time.Time) { + for chain, newTime := range newTimes { + s.setTime(chain, newTime) } } @@ -445,6 +471,16 @@ func (s *Driver) DeliverAcks() { } } +// stopConsumer stops a given consumer chain. +func (s *Driver) stopConsumer(chain ChainId) { + // stop the consumer chain on the provider + s.providerKeeper().StopConsumerChain(s.providerCtx(), string(chain), true) + // delete the chain from the coordinator + delete(s.coordinator.Chains, string(chain)) + // delete the path from the driver + delete(s.simibcs, chain) +} + // newDriver creates a new Driver object. // It creates a new coordinator, but does not start any chains. // The caller must call setupChains to start the chains and diff --git a/tests/difference/core/quint_model/driver/mbt_test.go b/tests/difference/core/quint_model/driver/mbt_test.go index 2b8dee82a9..89de31135c 100644 --- a/tests/difference/core/quint_model/driver/mbt_test.go +++ b/tests/difference/core/quint_model/driver/mbt_test.go @@ -5,6 +5,7 @@ import ( "log" "os" "reflect" + "sort" "testing" "time" @@ -16,7 +17,7 @@ import ( "github.com/stretchr/testify/require" ) -const verbose = false +const verbose = true func TestMBT(t *testing.T) { dirEntries, err := os.ReadDir("traces") @@ -114,15 +115,14 @@ func RunItfTrace(t *testing.T, path string) { } driver := newDriver(t, nodes, valNames) - driver.setupChains(modelParams, valSet, signers, nodes, valNames, consumers) + + driver.setupProvider(modelParams, valSet, signers, nodes, valNames) // remember the time offsets to be able to compare times to the model // this is necessary because the system needs to do many steps to initialize the chains, // which is abstracted away in the model timeOffsets := make(map[ChainId]time.Time, len(chains)) - for _, chain := range chains { - timeOffsets[ChainId(chain)] = driver.time(ChainId(chain)) - } + timeOffsets[Provider] = driver.time(Provider) t.Log("Started chains") @@ -167,8 +167,81 @@ func RunItfTrace(t *testing.T, path string) { // and then increment the rest of the time] // TODO: start and stop consumers - driver.endAndBeginBlock("provider", 1) - driver.endAndBeginBlock("provider", time.Duration(timeAdvancement)*time.Second-1) + driver.endAndBeginBlock("provider", time.Duration(timeAdvancement)*time.Second-1*time.Nanosecond) + driver.endAndBeginBlock("provider", 1*time.Nanosecond) + + // save the last timestamp for each chain, + // because setting up chains will modify timestamps + // when the coordinator is starting chains + lastTimestamps := driver.allTimes() + // start consumers + for _, consumer := range consumersToStart { + driver.setupConsumer( + consumer.Value.(string), + modelParams, + driver.providerChain().Vals, + signers, + nodes, + valNames, + driver.providerChain(), + ) + lastTimestamps[ChainId(consumer.Value.(string))] = driver.time(ChainId(consumer.Value.(string))) + } + + // stop consumers + for _, consumer := range consumersToStop { + consumerChain := ChainId(consumer.Value.(string)) + driver.stopConsumer(consumerChain) + + // remove the consumer from timestamps map and time offsets + delete(lastTimestamps, consumerChain) + delete(timeOffsets, consumerChain) + } + + // remove the stopped consumers from the timestamps + for _, consumer := range consumersToStop { + consumerChain := ChainId(consumer.Value.(string)) + delete(lastTimestamps, consumerChain) + delete(timeOffsets, consumerChain) + } + + // restore the old timestamps, but increment by 1 nanosecond to avoid duplicate timestamps in headers + for chain, oldTimestamp := range lastTimestamps { + // if the chain was stopped, we don't need to restore the timestamp + driver.setTime(ChainId(chain), oldTimestamp.Add(1*time.Nanosecond)) + // also set the offset for each chain correctly - offset is incremented by 1 nanosecond + timeOffsets[ChainId(chain)] = timeOffsets[ChainId(chain)].Add(1 * time.Nanosecond) + } + + // set the timeOffsets for the newly started chains + for _, consumer := range consumersToStart { + consumerChain := ChainId(consumer.Value.(string)) + timeOffsets[consumerChain] = driver.time(consumerChain) + } + + // need to produce another block to fix messed up times because the provider comitted blocks with + // times that were fixed by the coordinator + driver.endAndBeginBlock("provider", 0) + providerHeader := driver.providerChain().LastHeader + + // same for the consumers that were started + for _, consumer := range consumersToStart { + consumerChainId := string(consumer.Value.(string)) + driver.endAndBeginBlock(ChainId(consumerChainId), 0) + } + + // for all connected consumers, update the clients... + // unless it was the last consumer to be started, in which case it already has the header + for _, consumer := range driver.runningConsumers() { + if len(consumersToStart) > 0 && consumer.ChainId == consumersToStart[len(consumersToStart)-1].Value.(string) { + continue + } + consumerChainId := string(consumer.ChainId) + + driver.path(ChainId(consumerChainId)).AddClientHeader(Provider, providerHeader) + driver.path(ChainId(consumerChainId)).UpdateClient(consumerChainId) + } + case "EndAndBeginBlockForConsumer": consumerChain := lastAction["consumerChain"].Value.(string) timeAdvancement := lastAction["timeAdvancement"].Value.(int64) @@ -176,8 +249,16 @@ func RunItfTrace(t *testing.T, path string) { // as in EndAndBeginBlockForProvider, we need to produce 2 blocks, // while still honoring the time advancement - driver.endAndBeginBlock(ChainId(consumerChain), 1) - driver.endAndBeginBlock(ChainId(consumerChain), time.Duration(timeAdvancement)*time.Second-1) + headerBefore := driver.chain(ChainId(consumerChain)).LastHeader + _ = headerBefore + + driver.endAndBeginBlock(ChainId(consumerChain), time.Duration(timeAdvancement)*time.Second-1*time.Nanosecond) + driver.endAndBeginBlock(ChainId(consumerChain), 1*time.Nanosecond) + + // update the client on the provider + consumerHeader := driver.chain(ChainId(consumerChain)).LastHeader + driver.path(ChainId(consumerChain)).AddClientHeader(consumerChain, consumerHeader) + driver.path(ChainId(consumerChain)).UpdateClient(Provider) case "DeliverVscPacket": consumerChain := lastAction["consumerChain"].Value.(string) t.Log("DeliverVscPacket", consumerChain) @@ -204,24 +285,38 @@ func RunItfTrace(t *testing.T, path string) { currentModelState := state.VarValues["currentState"].Value.(itf.MapExprType) // check that the actual state is the same as the model state - // check validator sets - provider current validator set should be the one from the staking keeper + // compare the running consumers + modelRunningConsumers := RunningConsumers(currentModelState) + + systemRunningConsumers := driver.runningConsumers() + actualRunningConsumers := make([]string, len(systemRunningConsumers)) + for i, chain := range systemRunningConsumers { + actualRunningConsumers[i] = chain.ChainId + } - // provider - // consumers - current validator set does not correspond to anything, - // we can only check the head of the voting power history - // no assignment found, so providerConsAddr is the consumerConsAddr + // sort the slices so that we can compare them + sort.Slice(modelRunningConsumers, func(i, j int) bool { + return modelRunningConsumers[i] < modelRunningConsumers[j] + }) + sort.Slice(actualRunningConsumers, func(i, j int) bool { + return actualRunningConsumers[i] < actualRunningConsumers[j] + }) + + require.Equal(t, modelRunningConsumers, actualRunningConsumers, "Running consumers do not match") + + // check validator sets - provider current validator set should be the one from the staking keeper t.Log("Comparing validator sets") - CompareValidatorSets(t, driver, currentModelState, consumers, index) + CompareValidatorSets(t, driver, currentModelState, actualRunningConsumers, index) t.Log("Validator sets match") // check times - sanity check that the block times match the ones from the model t.Log("Comparing timestamps") - CompareTimes(t, driver, consumers, currentModelState, timeOffsets) + CompareTimes(t, driver, actualRunningConsumers, currentModelState, timeOffsets) t.Log("Timestamps match") // check sent packets: we check that the package queues in the model and the system have the same length. t.Log("Comparing packet queues") - for _, consumer := range consumers { + for _, consumer := range actualRunningConsumers { ComparePacketQueues(t, driver, currentModelState, consumer) } t.Log("Packet queues match") diff --git a/tests/difference/core/quint_model/driver/model_viewer.go b/tests/difference/core/quint_model/driver/model_viewer.go index b293effbb9..e72363b313 100644 --- a/tests/difference/core/quint_model/driver/model_viewer.go +++ b/tests/difference/core/quint_model/driver/model_viewer.go @@ -55,3 +55,17 @@ func PacketQueue(curStateExpr itf.MapExprType, sender string, receiver string) i return consumerState["outstandingPacketsToProvider"].Value.([]itf.Expr) } } + +// RunningConsumers returns a slice containing the names of the consumers +// that are currently running. +func RunningConsumers(curStateExpr itf.MapExprType) []string { + exprSlice := ProviderState(curStateExpr)["consumerStatus"].Value.(itf.MapExprType) + runningConsumers := make([]string, 0) + for consumer, statusExpr := range exprSlice { + status := statusExpr.Value.(string) + if status == "running" { + runningConsumers = append(runningConsumers, consumer) + } + } + return runningConsumers +} diff --git a/tests/difference/core/quint_model/driver/setup.go b/tests/difference/core/quint_model/driver/setup.go index 381f5560e2..da755546fc 100644 --- a/tests/difference/core/quint_model/driver/setup.go +++ b/tests/difference/core/quint_model/driver/setup.go @@ -6,6 +6,7 @@ import ( "testing" "time" + "cosmossdk.io/math" abcitypes "github.com/cometbft/cometbft/abci/types" cmtproto "github.com/cometbft/cometbft/proto/tendermint/types" cmttypes "github.com/cometbft/cometbft/types" @@ -17,6 +18,7 @@ import ( clienttypes "github.com/cosmos/ibc-go/v7/modules/core/02-client/types" commitmenttypes "github.com/cosmos/ibc-go/v7/modules/core/23-commitment/types" ibctmtypes "github.com/cosmos/ibc-go/v7/modules/light-clients/07-tendermint" + tendermint "github.com/cosmos/ibc-go/v7/modules/light-clients/07-tendermint" icstestingutils "github.com/cosmos/interchain-security/v3/testutil/ibc_testing" "github.com/cosmos/interchain-security/v3/testutil/integration" simibc "github.com/cosmos/interchain-security/v3/testutil/simibc" @@ -140,10 +142,13 @@ func getAppBytesAndSenders( for i, val := range nodes { _, valSetVal := initialValSet.GetByAddress(val.Address.Bytes()) + var tokens math.Int if valSetVal == nil { - log.Panicf("error getting validator with address %v from valSet %v", val, initialValSet) + tokens = sdk.NewInt(0) + } else { + tokens = sdk.NewInt(valSetVal.VotingPower) } - tokens := sdk.NewInt(valSetVal.VotingPower) + sumBonded = sumBonded.Add(tokens) pk, err := cryptocodec.FromTmPubKeyInterface(val.PubKey) @@ -394,32 +399,47 @@ func (s *Driver) ConfigureNewPath(consumerChain *ibctesting.TestChain, providerC return path } -func (s *Driver) setupChains( +func (s *Driver) providerHeader() *tendermint.Header { + return s.coordinator.Chains["provider"].LastHeader +} + +func (s *Driver) setupProvider( params ModelParams, valSet *cmttypes.ValidatorSet, // the initial validator set 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, - consumers []string, // a list of consumer chain names ) { - initValUpdates := cmttypes.TM2PB.ValidatorUpdates(valSet) // start provider s.t.Log("Creating provider chain") providerChain := newChain(s.t, params, s.coordinator, icstestingutils.ProviderAppIniter, "provider", valSet, signers, nodes, valNames) s.coordinator.Chains["provider"] = providerChain - providerHeader, _ := simibc.EndBlock(providerChain, func() {}) + // produce a first block + simibc.EndBlock(providerChain, func() {}) simibc.BeginBlock(providerChain, 0) +} + +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, +) { + s.t.Logf("Starting consumer %v", chain) + + initValUpdates := cmttypes.TM2PB.ValidatorUpdates(valSet) // start consumer chains - for _, chain := range consumers { - s.t.Logf("Creating consumer chain %v", chain) - consumerChain := newChain(s.t, params, s.coordinator, icstestingutils.ConsumerAppIniter(initValUpdates), chain, valSet, signers, nodes, valNames) - s.coordinator.Chains[chain] = consumerChain + s.t.Logf("Creating consumer chain %v", chain) + 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, providerHeader) - s.simibcs[ChainId(chain)] = simibc.MakeRelayedPath(s.t, path) - } + path := s.ConfigureNewPath(consumerChain, providerChain, params, s.providerHeader()) + s.simibcs[ChainId(chain)] = simibc.MakeRelayedPath(s.t, path) } func createConsumerGenesis(modelParams ModelParams, providerChain *ibctesting.TestChain, consumerClientState *ibctmtypes.ClientState) *consumertypes.GenesisState { diff --git a/testutil/simibc/relayed_path.go b/testutil/simibc/relayed_path.go index b5ba476305..8c2b79bc3d 100644 --- a/testutil/simibc/relayed_path.go +++ b/testutil/simibc/relayed_path.go @@ -21,6 +21,7 @@ type RelayedPath struct { // have been committed to that chain. The headers are used to update the // client of the counterparty chain. clientHeaders map[string][]*ibctmtypes.Header + // TODO: Make this private and expose methods to add packets and acks. // Currently, packets and acks are added directly to the outboxes, // but we should hide this implementation detail.