mbt from main

Makefile

@@ -129,9 +129,6 @@ test-trace:
 # Note: this is *not* using the Quint models to test the system,
 # this tests/verifies the Quint models *themselves*.
 verify-models:
-	quint test tests/mbt/model/ccv_test.qnt;\
-	quint test tests/mbt/model/ccv_model.qnt;\
-	quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" tests/mbt/model/ccv_model.qnt --max-steps 200 --max-samples 200
 	cd tests/mbt/model;\
 	../run_invariants.sh
 
@@ -245,4 +242,4 @@ build-docs:
 ###############################################################################
 
 e2e-traces:
-	cd tests/e2e; go test -timeout 30s -run ^TestWriteExamples -v
+	cd tests/e2e; go test -timeout 30s -run ^TestWriteExamples -v

go.mod

@@ -169,6 +169,7 @@ require (
 require (
 	github.com/informalsystems/itf-go v0.0.1
 	github.com/spf13/viper v1.16.0
+	golang.org/x/mod v0.11.0
 	google.golang.org/genproto/googleapis/api v0.0.0-20231212172506-995d672761c0
 )
 

tests/e2e/config.go

@@ -4,8 +4,6 @@ import (
 	"fmt"
 	"strconv"
 	"time"
-
-	"golang.org/x/mod/semver"
 )
 
 var (
@@ -262,105 +260,6 @@ func SlashThrottleTestConfig() TestConfig {
 	return tr
 }
 
-// CompatibilityTestConfig returns a test configuration for a given version of a consumer and provider
-func CompatibilityTestConfig(providerVersion, consumerVersion string) TestConfig {
-	// Base configuration is the default
-	testCfg := DefaultTestConfig()
-
-	// get version dependent validator configs
-	testCfg.validatorConfigs = getValidatorConfigFromVersion(providerVersion, consumerVersion)
-
-	var providerConfig, consumerConfig ChainConfig
-	if !semver.IsValid(consumerVersion) {
-		fmt.Println("Using default provider chain config")
-		consumerConfig = testCfg.chainConfigs[ChainID("consu")]
-	} else if semver.Compare(consumerVersion, "v3.0.0") < 0 {
-		fmt.Println("Using consumer chain config for v2.0.0")
-		consumerConfig = ChainConfig{
-			ChainId:        ChainID("consu"),
-			AccountPrefix:  "cosmos",
-			BinaryName:     "interchain-security-cd",
-			IpPrefix:       "7.7.8",
-			VotingWaitTime: 20,
-			GenesisChanges: ".app_state.gov.voting_params.voting_period = \"20s\" | " +
-				".app_state.slashing.params.signed_blocks_window = \"15\" | " +
-				".app_state.slashing.params.min_signed_per_window = \"0.500000000000000000\" | " +
-				".app_state.slashing.params.downtime_jail_duration = \"2s\" | " +
-				".app_state.slashing.params.slash_fraction_downtime = \"0.010000000000000000\"",
-		}
-	} else if semver.Compare(consumerVersion, "v4.0.0") < 0 {
-		fmt.Println("Using consumer chain config for v3.x.x")
-		consumerConfig = ChainConfig{
-			ChainId:        ChainID("consu"),
-			AccountPrefix:  "cosmos",
-			BinaryName:     "interchain-security-cd",
-			IpPrefix:       "7.7.8",
-			VotingWaitTime: 20,
-			GenesisChanges: ".app_state.gov.params.voting_period = \"20s\" | " +
-				".app_state.slashing.params.signed_blocks_window = \"15\" | " +
-				".app_state.slashing.params.min_signed_per_window = \"0.500000000000000000\" | " +
-				".app_state.slashing.params.downtime_jail_duration = \"60s\" | " +
-				".app_state.slashing.params.slash_fraction_downtime = \"0.010000000000000000\"",
-		}
-	} else {
-		fmt.Println("Using default consumer chain config")
-		consumerConfig = testCfg.chainConfigs[ChainID("consu")]
-	}
-
-	// Get the provider chain config for a specific version
-	if !semver.IsValid(providerVersion) {
-		fmt.Println("Using default provider chain config")
-		providerConfig = testCfg.chainConfigs[ChainID("provi")]
-	} else if semver.Compare(providerVersion, "v3.0.0") < 0 {
-		fmt.Println("Using provider chain config for v2.x.x")
-		providerConfig = ChainConfig{
-			ChainId:        ChainID("provi"),
-			AccountPrefix:  "cosmos",
-			BinaryName:     "interchain-security-pd",
-			IpPrefix:       "7.7.7",
-			VotingWaitTime: 20,
-			GenesisChanges: ".app_state.gov.voting_params.voting_period = \"20s\" | " +
-				// Custom slashing parameters for testing validator downtime functionality
-				// See https://docs.cosmos.network/main/modules/slashing/04_begin_block.html#uptime-tracking
-				".app_state.slashing.params.signed_blocks_window = \"10\" | " +
-				".app_state.slashing.params.min_signed_per_window = \"0.500000000000000000\" | " +
-				".app_state.slashing.params.downtime_jail_duration = \"2s\" | " +
-				".app_state.slashing.params.slash_fraction_downtime = \"0.010000000000000000\" | " +
-				".app_state.provider.params.slash_meter_replenish_fraction = \"1.0\" | " + // This disables slash packet throttling
-				".app_state.provider.params.slash_meter_replenish_period = \"3s\"",
-		}
-	} else if semver.Compare(providerVersion, "v4.0.0") <= 0 {
-		fmt.Println("Using provider chain config for v3.x.x")
-		providerConfig = ChainConfig{
-			ChainId:        ChainID("provi"),
-			AccountPrefix:  "cosmos",
-			BinaryName:     "interchain-security-pd",
-			IpPrefix:       "7.7.7",
-			VotingWaitTime: 20,
-			GenesisChanges: ".app_state.gov.params.voting_period = \"20s\" | " +
-				// Custom slashing parameters for testing validator downtime functionality
-				// See https://docs.cosmos.network/main/modules/slashing/04_begin_block.html#uptime-tracking
-				".app_state.slashing.params.signed_blocks_window = \"10\" | " +
-				".app_state.slashing.params.min_signed_per_window = \"0.500000000000000000\" | " +
-				".app_state.slashing.params.downtime_jail_duration = \"60s\" | " +
-				".app_state.slashing.params.slash_fraction_downtime = \"0.010000000000000000\" | " +
-				".app_state.provider.params.slash_meter_replenish_fraction = \"1.0\" | " + // This disables slash packet throttling
-				".app_state.provider.params.slash_meter_replenish_period = \"3s\"",
-		}
-	} else {
-		fmt.Println("Using default provider chain config")
-		providerConfig = testCfg.chainConfigs[ChainID("provi")]
-	}
-
-	testCfg.chainConfigs[ChainID("consu")] = consumerConfig
-	testCfg.chainConfigs[ChainID("provi")] = providerConfig
-	testCfg.name = string(CompatibilityTestCfg)
-	testCfg.containerConfig.InstanceName = fmt.Sprintf("%s_%s-%s",
-		testCfg.containerConfig.InstanceName,
-		consumerVersion, providerVersion)
-	return testCfg
-}
-
 func DefaultTestConfig() TestConfig {
 	tr := TestConfig{
 		name: "default",

tests/mbt/driver/core.go

@@ -20,6 +20,7 @@ import (
 	abcitypes "github.com/cometbft/cometbft/abci/types"
 	cmttypes "github.com/cometbft/cometbft/types"
 
+	"github.com/cometbft/cometbft/proto/tendermint/crypto"
 	appConsumer "github.com/cosmos/interchain-security/v4/app/consumer"
 	appProvider "github.com/cosmos/interchain-security/v4/app/provider"
 	simibc "github.com/cosmos/interchain-security/v4/testutil/simibc"
@@ -127,9 +128,13 @@ func (s *Driver) consumerPower(i int64, chain ChainId) (int64, error) {
 	return v.Power, nil
 }
 
+func (s *Driver) stakingValidator(i int64) (stakingtypes.Validator, bool) {
+	return s.providerStakingKeeper().GetValidator(s.ctx(PROVIDER), s.validator(i))
+}
+
 // providerPower returns the power(=number of bonded tokens) of the i-th validator on the provider.
 func (s *Driver) providerPower(i int64) (int64, error) {
-	v, found := s.providerStakingKeeper().GetValidator(s.ctx(PROVIDER), s.validator(i))
+	v, found := s.stakingValidator(i)
 	if !found {
 		return 0, fmt.Errorf("validator with id %v not found on provider", i)
 	} else {
@@ -374,6 +379,14 @@ func (s *Driver) setTime(chain ChainId, newTime time.Time) {
 	testChain.App.BeginBlock(abcitypes.RequestBeginBlock{Header: testChain.CurrentHeader})
 }
 
+func (s *Driver) AssignKey(chain ChainId, valIndex int64, value crypto.PublicKey) error {
+	stakingVal, found := s.stakingValidator(valIndex)
+	if !found {
+		return fmt.Errorf("validator with id %v not found on provider", valIndex)
+	}
+	return s.providerKeeper().AssignConsumerKey(s.providerCtx(), string(chain), stakingVal, value)
+}
+
 // DeliverPacketToConsumer delivers a packet from the provider to the given consumer recipient.
 // It updates the client before delivering the packet.
 // Since the channel is ordered, the packet that is delivered is the first packet in the outbox.

tests/mbt/driver/generate_more_traces.sh

@@ -9,4 +9,5 @@ go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -in
 echo "Generating synced traces with maturations"
 go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 20 -numSteps 300 -numSamples 20
 echo "Generating long synced traces without invariants"
-go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -traceFolder traces/sync_noinv -numTraces 20 -numSteps 500 -numSamples 1
+go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -traceFolder traces/sync_noinv -numTraces 20 -numSteps 500 -numSamples 1
+go run ./... -modelPath=../model/ccv_boundeddrift.qnt --step stepBoundedDriftKeyAssignment --traceFolder traces/bound_key -numTraces 20 -numSteps 100 -numSamples 20

tests/mbt/driver/generate_traces.sh

@@ -9,4 +9,5 @@ go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -in
 echo "Generating synced traces with maturations"
 go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -invariant CanReceiveMaturations -traceFolder traces/sync_mat -numTraces 1 -numSteps 300 -numSamples 20
 echo "Generating long synced traces without invariants"
-go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -traceFolder traces/sync_noinv -numTraces 1 -numSteps 500 -numSamples 1
+go run ./... -modelPath=../model/ccv_sync.qnt -init initSync -step stepSync -traceFolder traces/sync_noinv -numTraces 1 -numSteps 500 -numSamples 1
+go run ./... -modelPath=../model/ccv_boundeddrift.qnt --step stepBoundedDriftKeyAssignment --traceFolder traces/bound_key -numTraces 1 -numSteps 100 -numSamples 20