Replace difftests with model-based testing using Quint

go.mod

@@ -1,6 +1,8 @@
 module github.com/cosmos/interchain-security/v3
 
-go 1.20
+go 1.21.1
+
+toolchain go1.21.3
 
 require (
 	cosmossdk.io/errors v1.0.0
@@ -171,6 +173,7 @@ require (
 )
 
 require (
+github.com/informalsystems/itf-go v0.0.1 // indirect
 	cosmossdk.io/log v1.2.1 // indirect
 	github.com/cockroachdb/errors v1.10.0 // indirect
 	github.com/cockroachdb/logtags v0.0.0-20230118201751-21c54148d20b // indirect

go.sum

@@ -774,6 +774,8 @@ github.com/influxdata/promql/v2 v2.12.0/go.mod h1:fxOPu+DY0bqCTCECchSRtWfc+0X19y
 github.com/influxdata/roaring v0.4.13-0.20180809181101-fc520f41fab6/go.mod h1:bSgUQ7q5ZLSO+bKBGqJiCBGAl+9DxyW63zLTujjUlOE=
 github.com/influxdata/tdigest v0.0.0-20181121200506-bf2b5ad3c0a9/go.mod h1:Js0mqiSBE6Ffsg94weZZ2c+v/ciT8QRHFOap7EKDrR0=
 github.com/influxdata/usage-client v0.0.0-20160829180054-6d3895376368/go.mod h1:Wbbw6tYNvwa5dlB6304Sd+82Z3f7PmVZHVKU637d4po=
+github.com/informalsystems/itf-go v0.0.1 h1:lVvdg3v+IMWOsVfIvOOGy1hHFO5KxoS8b8EiwKLbQDg=
+github.com/informalsystems/itf-go v0.0.1/go.mod h1:wgqaQ/yl2kbNlgw6GaleuHEefpZvkZo6Hc0jc8cGG9M=
 github.com/jackpal/go-nat-pmp v1.0.2/go.mod h1:QPH045xvCAeXUZOxsnwmrtiCoxIr9eob+4orBN1SBKc=
 github.com/jedisct1/go-minisign v0.0.0-20190909160543-45766022959e/go.mod h1:G1CVv03EnqU1wYL2dFwXxW2An0az9JTl/ZsqXQeBlkU=
 github.com/jessevdk/go-flags v0.0.0-20141203071132-1679536dcc89/go.mod h1:4FA24M0QyGHXBuZZK/XkWh8h0e1EYbRYJSGM75WSRxI=

tests/difference/core/quint_model/ccv_model.qnt

@@ -15,6 +15,16 @@ module ccv_model {
 
     import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains).* from "./ccv"
 
+    type Parameters = {
+        VscTimeout: Time,
+        CcvTimeout: Chain -> Time,
+        UnbondingPeriodPerChain: Chain -> Time,
+        ConsumerChains: Set[Chain],
+        Nodes: Set[Node],
+        InitialValidatorSet: Node -> int,
+    }
+
+    var params: Parameters
 
     var currentState: ProtocolState
 
@@ -126,14 +136,23 @@ module ccv_model {
             consumerStates: consumerStates
         },
         trace' = List(emptyAction.with("kind", "init")),
+        params' = {
+            VscTimeout: VscTimeout,
+            CcvTimeout: CcvTimeout,
+            UnbondingPeriodPerChain: UnbondingPeriodPerChain,
+            ConsumerChains: ConsumerChains,
+            Nodes: nodes,
+            InitialValidatorSet: InitialValidatorSet,
+        }
     }
 
     action VotingPowerChange(validator: Node, newVotingPower: int): bool = 
         val result = votingPowerChange(currentState, validator, newVotingPower)
         all {
             result.hasError() == false,
             currentState' = result.newState,
-            trace' = trace.append(emptyAction.with("kind", "VotingPowerChange").with("validator", validator).with("newVotingPower", newVotingPower))
+            trace' = trace.append(emptyAction.with("kind", "VotingPowerChange").with("validator", validator).with("newVotingPower", newVotingPower)),
+            params' = params,
         }
 
     // The receiver receives the next outstanding VscPacket from the provider.
@@ -144,7 +163,8 @@ module ccv_model {
         all {
             result.hasError() == false,
             currentState' = result.newState,
-            trace' = trace.append(emptyAction.with("kind", "DeliverVscPacket").with("consumerChain", receiver))
+            trace' = trace.append(emptyAction.with("kind", "DeliverVscPacket").with("consumerChain", receiver)),
+            params' = params,
         }
 
     // The provider receives the next outstanding VscMaturedPacket from the sender.
@@ -155,7 +175,8 @@ module ccv_model {
         all {
             result.hasError() == false,
             currentState' = result.newState,
-            trace' = trace.append(emptyAction.with("kind", "DeliverVscMaturedPacket").with("consumerChain", sender))
+            trace' = trace.append(emptyAction.with("kind", "DeliverVscMaturedPacket").with("consumerChain", sender)),
+            params' = params,
         }
 
     action EndAndBeginBlockForProvider(
@@ -166,7 +187,8 @@ module ccv_model {
         all {
             result.hasError() == false,
             currentState' = result.newState,
-            trace' = trace.append(emptyAction.with("kind", "EndAndBeginBlockForProvider").with("timeAdvancement", timeAdvancement).with("consumersToStart", consumersToStart).with("consumersToStop", consumersToStop))
+            trace' = trace.append(emptyAction.with("kind", "EndAndBeginBlockForProvider").with("timeAdvancement", timeAdvancement).with("consumersToStart", consumersToStart).with("consumersToStop", consumersToStop)),
+            params' = params,
         }
 
     action EndAndBeginBlockForConsumer(
@@ -176,7 +198,8 @@ module ccv_model {
         all {
             result.hasError() == false,
             currentState' = result.newState,
-            trace' = trace.append(emptyAction.with("kind", "EndAndBeginBlockForConsumer").with("consumerChain", chain).with("timeAdvancement", timeAdvancement))
+            trace' = trace.append(emptyAction.with("kind", "EndAndBeginBlockForConsumer").with("consumerChain", chain).with("timeAdvancement", timeAdvancement)),
+            params' = params,
         }
 
     // ==================

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

@@ -0,0 +1,96 @@
+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,
+				},
+			},
+		},
+	}
+}