Start adjusting behaviour for started/stopped consumers

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

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,17 +167,98 @@ 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)
 			t.Log("EndAndBeginBlockForConsumer", consumerChain, timeAdvancement)
 
 			// 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")

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
+}

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 {