Make state printing more robust

tests/difference/core/quint_model/driver/common.go

@@ -1,96 +1,16 @@
 package main
 
-import (
-	"time"
-
-	sdk "github.com/cosmos/cosmos-sdk/types"
-	stakingtypes "github.com/cosmos/cosmos-sdk/x/staking/types"
-
-	tmproto "github.com/cometbft/cometbft/proto/tendermint/types"
-	tmtypes "github.com/cometbft/cometbft/types"
-)
-
 const (
 	P = "provider"
-	C = "consumer"
 )
 
-// ValStates represents the total delegation
-// and bond status of a validator
-type ValStates struct {
-	Delegation           []int
-	Tokens               []int
-	ValidatorExtraTokens []int
-	Status               []stakingtypes.BondStatus
-}
-
-type InitState struct {
-	PKSeeds                []string
-	NumValidators          int
-	MaxValidators          int
-	InitialDelegatorTokens int
-	SlashDoublesign        sdk.Dec
-	SlashDowntime          sdk.Dec
-	UnbondingP             time.Duration
-	UnbondingC             time.Duration
-	Trusting               time.Duration
-	MaxClockDrift          time.Duration
-	BlockInterval          time.Duration
-	ConsensusParams        *tmproto.ConsensusParams
-	ValStates              ValStates
-	MaxEntries             int
-}
-
-var initStateVar InitState
-
-func init() {
-	//	tokens === power
-	sdk.DefaultPowerReduction = sdk.NewInt(1)
-	initStateVar = InitState{
-		PKSeeds: []string{
-			// Fixed seeds are used to create the private keys for validators.
-			// The seeds are chosen to ensure that the resulting validators are
-			// sorted in descending order by the staking module.
-			"bbaaaababaabbaabababbaabbbbbbaaa",
-			"abbbababbbabaaaaabaaabbbbababaab",
-			"bbabaabaabbbbbabbbaababbbbabbbbb",
-			"aabbbabaaaaababbbabaabaabbbbbbba",
-		},
-		NumValidators:          4,
-		MaxValidators:          2,
-		InitialDelegatorTokens: 10000000000000,
-		SlashDoublesign:        sdk.NewDec(0),
-		SlashDowntime:          sdk.NewDec(0),
-		UnbondingP:             time.Second * 70,
-		UnbondingC:             time.Second * 50,
-		Trusting:               time.Second * 49,
-		MaxClockDrift:          time.Second * 10000,
-		BlockInterval:          time.Second * 6,
-		ValStates: ValStates{
-			Delegation:           []int{4000, 3000, 2000, 1000},
-			Tokens:               []int{5000, 4000, 3000, 2000},
-			ValidatorExtraTokens: []int{1000, 1000, 1000, 1000},
-			Status: []stakingtypes.BondStatus{
-				stakingtypes.Bonded, stakingtypes.Bonded,
-				stakingtypes.Unbonded, stakingtypes.Unbonded,
-			},
-		},
-		MaxEntries: 1000000,
-		ConsensusParams: &tmproto.ConsensusParams{
-			Block: &tmproto.BlockParams{
-				MaxBytes: 9223372036854775807,
-				MaxGas:   9223372036854775807,
-			},
-			Evidence: &tmproto.EvidenceParams{
-				MaxAgeNumBlocks: 302400,
-				MaxAgeDuration:  504 * time.Hour, // 3 weeks is the max duration
-				MaxBytes:        10000,
-			},
-			Validator: &tmproto.ValidatorParams{
-				PubKeyTypes: []string{
-					tmtypes.ABCIPubKeyTypeEd25519,
-				},
-			},
-		},
+// getIndexOfString returns the index of the first occurrence of the given string
+// in the given slice, or -1 if the string is not found.
+func getIndexOfString(s string, slice []string) int {
+	for i, v := range slice {
+		if v == s {
+			return i
+		}
 	}
+	return -1
 }

tests/difference/core/quint_model/driver/core.go

@@ -20,6 +20,8 @@ import (
 	simibc "github.com/cosmos/interchain-security/v3/testutil/simibc"
 	consumerkeeper "github.com/cosmos/interchain-security/v3/x/ccv/consumer/keeper"
 	providerkeeper "github.com/cosmos/interchain-security/v3/x/ccv/provider/keeper"
+
+	cmttypes "github.com/cometbft/cometbft/types"
 )
 
 // Define a new type for ChainIds to be more explicit
@@ -42,7 +44,8 @@ type Driver struct {
 	simibcs map[ChainId]*simibc.RelayedPath
 
 	// keep around validators for easy access
-	valAddresses []sdk.ValAddress
+	validators []*cmttypes.Validator
+	valNames   []string
 }
 
 // ctx returns the sdk.Context for the chain
@@ -101,7 +104,7 @@ func (s *Driver) delegator() sdk.AccAddress {
 
 // validator returns the address for the validator with id (ix) i
 func (s *Driver) validator(i int64) sdk.ValAddress {
-	return s.valAddresses[i]
+	return sdk.ValAddress(s.validators[i].Address)
 }
 
 // consAddr returns the ConsAdd for the validator with id (ix) i
@@ -120,13 +123,21 @@ func (s *Driver) isJailed(i int64) bool {
 // consumerPower returns the power on the consumer chain chain for
 // validator with id (ix) i
 func (s *Driver) consumerPower(i int64, chain ChainId) (int64, error) {
-	v, found := s.consumerKeeper(chain).GetCCValidator(s.ctx(C), s.validator(i))
+	v, found := s.consumerKeeper(chain).GetCCValidator(s.ctx(chain), s.validator(i))
 	if !found {
 		return 0, fmt.Errorf("GetCCValidator(%v) -> !found", s.validator(i))
 	}
 	return v.Power, nil
 }
 
+// consumerTokens returns the number of tokens that the validator with
+// id (ix) i has delegated to it in total on the provider chain
+func (s *Driver) providerPower(i int64) int64 {
+	v, found := s.providerStakingKeeper().GetValidator(s.ctx(P), s.validator(i))
+	require.True(s.t, found, "GetValidator(%v) -> !found", s.validator(i))
+	return v.BondedTokens().Int64()
+}
+
 // delegation returns the number of delegated tokens in the delegation from
 // the delegator account to the validator with id (ix) i
 func (s *Driver) delegation(i int64) int64 {
@@ -147,7 +158,9 @@ func (s *Driver) validatorStatus(i int64) stakingtypes.BondStatus {
 // id (ix) i has delegated to it in total on the provider chain
 func (s *Driver) providerTokens(i int64) int64 {
 	v, found := s.providerStakingKeeper().GetValidator(s.ctx(P), s.validator(i))
-	require.True(s.t, found, "GetValidator(%v) -> !found", s.validator(i))
+	if !found {
+		return 0
+	}
 	return v.Tokens.Int64()
 }
 
@@ -199,14 +212,14 @@ func (s *Driver) consumerSlash(val sdk.ConsAddress, h int64, isDowntime bool, ch
 	if isDowntime {
 		kind = stakingtypes.Infraction_INFRACTION_DOWNTIME
 	}
-	ctx := s.ctx(C)
+	ctx := s.ctx(chain)
 	before := len(ctx.EventManager().Events())
 	s.consumerKeeper(chain).SlashWithInfractionReason(ctx, val, h, 0, sdk.Dec{}, kind)
 	// consumer module emits packets on slash, so these must be collected.
 	evts := ctx.EventManager().Events()
 	packets := simibc.ParsePacketsFromEvents(evts[before:])
 	if len(packets) > 0 {
-		s.path(chain).Outboxes.AddPacket(C, packets[0])
+		s.path(chain).Outboxes.AddPacket(string(chain), packets[0])
 	}
 }
 
@@ -240,6 +253,10 @@ func (s *Driver) getStateString() string {
 	return state.String()
 }
 
+func (s *Driver) isProviderChain(chain ChainId) bool {
+	return chain == "provider"
+}
+
 func (s *Driver) getChainStateString(chain ChainId) string {
 	ctx := s.ctx(chain)
 
@@ -249,18 +266,36 @@ func (s *Driver) getChainStateString(chain ChainId) string {
 	// Get the current block time
 	blockTime := ctx.BlockTime()
 
-	// Get the validator set for the current block
-	validatorSet := s.validatorSet(chain)
-
 	// Build the chain info string
 	var chainInfo strings.Builder
 	chainInfo.WriteString(fmt.Sprintf("  Height: %d\n", height))
 	chainInfo.WriteString(fmt.Sprintf("  Time: %s\n", blockTime))
 
+	if !s.isProviderChain(chain) {
+		// Check whether the chain is in the consumer chains on the provider
+
+		consumerChains := s.providerKeeper().GetAllConsumerChains(s.providerCtx())
+
+		found := false
+		for _, consumerChain := range consumerChains {
+			if consumerChain.ChainId == string(chain) {
+				found = true
+			}
+		}
+
+		if found {
+			chainInfo.WriteString("...is currently a consumer chain")
+		} else {
+			chainInfo.WriteString("...is currently not a consumer chain")
+		}
+	}
+
 	// Build the validator info string
 	var validatorInfo strings.Builder
-	for _, validator := range validatorSet {
-		validatorInfo.WriteString(fmt.Sprintf("    Validator %s: power=%d\n", validator.GetOperator().String(), validator.BondedTokens()))
+	for index, valName := range s.valNames {
+		power := s.providerPower(int64(index))
+
+		validatorInfo.WriteString(fmt.Sprintf("    Validator %s: power=%d\n", valName, power))
 	}
 
 	chainInfo.WriteString(validatorInfo.String())
@@ -273,15 +308,16 @@ func (s *Driver) endAndBeginBlock(chain ChainId, timeAdvancement time.Duration,
 	})
 }
 
-func newDriver(t *testing.T, valAddresses []sdk.ValAddress) *Driver {
+func newDriver(t *testing.T, validators []*cmttypes.Validator, valNames []string) *Driver {
 	t.Log("Creating coordinator")
 	coordinator := ibctesting.NewCoordinator(t, 0) // start without chains, which we add later
 
 	suite := &Driver{
-		t:            t,
-		coordinator:  coordinator,
-		simibcs:      make(map[ChainId]*simibc.RelayedPath),
-		valAddresses: valAddresses,
+		t:           t,
+		coordinator: coordinator,
+		simibcs:     make(map[ChainId]*simibc.RelayedPath),
+		validators:  validators,
+		valNames:    valNames,
 	}
 	return suite
 }

tests/difference/core/quint_model/driver/mbt_test.go

@@ -6,7 +6,6 @@ import (
 	"time"
 
 	cmttypes "github.com/cometbft/cometbft/types"
-	"github.com/cosmos/cosmos-sdk/types"
 	"github.com/cosmos/interchain-security/v3/testutil/integration"
 	"github.com/informalsystems/itf-go/itf"
 	"github.com/stretchr/testify/require"
@@ -136,14 +135,8 @@ func TestItfTrace(t *testing.T) {
 		nodes[i] = addressMap[valName]
 	}
 
-	valAddresses := make([]types.ValAddress, len(valNames))
-	for i, valNode := range nodes {
-		pbVal := cmttypes.TM2PB.Validator(valNode)
-		valAddresses[i] = pbVal.Address
-	}
-
-	driver := newDriver(t, valAddresses)
-	driver.setupChains(modelParams, valSet, signers, nodes, consumers)
+	driver := newDriver(t, nodes, valNames)
+	driver.setupChains(modelParams, valSet, signers, nodes, valNames, consumers)
 
 	t.Log("Started chains")
 
@@ -161,12 +154,18 @@ func TestItfTrace(t *testing.T) {
 		switch actionKind {
 		case "init":
 			t.Log("Initializing...")
-			t.Logf(driver.getStateString())
 		case "VotingPowerChange":
 			node := lastAction["validator"].Value.(string)
 			newVotingPower := lastAction["newVotingPower"].Value.(int64)
 			t.Logf("Setting provider voting power of %v to %v", node, newVotingPower)
 
+			// valIndex := getIndexOfString(node, valNames)
+
+			// // set the voting power of the validator
+
+			// // get the previous voting power of that validator
+			// prevVotingPower := driver.validato
+
 		case "EndAndBeginBlockForProvider":
 			timeAdvancement := lastAction["timeAdvancement"].Value.(int64)
 			consumersToStart := lastAction["consumersToStart"].Value.(itf.ListExprType)
@@ -190,6 +189,8 @@ func TestItfTrace(t *testing.T) {
 			log.Fatalf("Error loading trace file %s, step %v: do not know action type %s",
 				path, index, actionKind)
 		}
+
+		t.Logf("Current actual state: %s", driver.getStateString())
 	}
 	t.FailNow()
 }

tests/difference/core/quint_model/driver/setup.go

@@ -54,6 +54,7 @@ func getAppBytesAndSenders(
 	initialValSet *cmttypes.ValidatorSet,
 	// the list of nodes that will be created, even ones that have no voting power initially
 	nodes []*cmttypes.Validator,
+	valNames []string,
 ) ([]byte, []ibctesting.SenderAccount) {
 	accounts := []authtypes.GenesisAccount{}
 	balances := []banktypes.Balance{}
@@ -124,13 +125,15 @@ func getAppBytesAndSenders(
 		delShares := sdk.NewDec(tokens.Int64()) // as many shares as tokens
 
 		validator := stakingtypes.Validator{
-			OperatorAddress:   sdk.ValAddress(val.Address).String(),
-			ConsensusPubkey:   pkAny,
-			Jailed:            false,
-			Status:            valStatus,
-			Tokens:            tokens,
-			DelegatorShares:   delShares,
-			Description:       stakingtypes.Description{},
+			OperatorAddress: sdk.ValAddress(val.Address).String(),
+			ConsensusPubkey: pkAny,
+			Jailed:          false,
+			Status:          valStatus,
+			Tokens:          tokens,
+			DelegatorShares: delShares,
+			Description: stakingtypes.Description{
+				Moniker: valNames[i],
+			},
 			UnbondingHeight:   int64(0),
 			UnbondingTime:     time.Unix(0, 0).UTC(),
 			Commission:        stakingtypes.NewCommission(sdk.ZeroDec(), sdk.ZeroDec(), sdk.ZeroDec()),
@@ -207,12 +210,13 @@ func newChain(
 	validators *cmttypes.ValidatorSet,
 	signers map[string]cmttypes.PrivValidator,
 	nodes []*cmttypes.Validator,
+	valNames []string,
 ) *ibctesting.TestChain {
 	app, genesis := appInit()
 
 	baseapp.SetChainID(chainID)(app.GetBaseApp())
 
-	stateBytes, senderAccounts := getAppBytesAndSenders(chainID, modelParams, app, genesis, validators, nodes)
+	stateBytes, senderAccounts := getAppBytesAndSenders(chainID, modelParams, app, genesis, validators, nodes, valNames)
 
 	protoConsParams := ConsensusParams.ToProto()
 	app.InitChain(
@@ -345,12 +349,13 @@ func (s *Driver) setupChains(
 	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)
+	providerChain := newChain(s.t, params, s.coordinator, icstestingutils.ProviderAppIniter, "provider", valSet, signers, nodes, valNames)
 	s.coordinator.Chains["provider"] = providerChain
 
 	providerHeader, _ := simibc.EndBlock(providerChain, func() {})
@@ -359,7 +364,7 @@ func (s *Driver) setupChains(
 	// 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)
+		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)