Skip to content

Commit

Permalink
Start adding mbt using Quint model
Browse files Browse the repository at this point in the history
  • Loading branch information
p-offtermatt committed Oct 19, 2023
1 parent 3989e17 commit a4840fc
Show file tree
Hide file tree
Showing 9 changed files with 21,060 additions and 6 deletions.
5 changes: 4 additions & 1 deletion go.mod
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -177,6 +179,7 @@ require (
github.com/cockroachdb/redact v1.1.5 // indirect
github.com/getsentry/sentry-go v0.23.0 // indirect
github.com/google/s2a-go v0.1.4 // indirect
github.com/informalsystems/itf-go v0.0.1 // indirect
github.com/kr/pretty v0.3.1 // indirect
github.com/kr/text v0.2.0 // indirect
github.com/mattn/go-colorable v0.1.13 // indirect
Expand Down
2 changes: 2 additions & 0 deletions go.sum
Original file line number Diff line number Diff line change
Expand Up @@ -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=
Expand Down
33 changes: 28 additions & 5 deletions tests/difference/core/quint_model/ccv_model.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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(
Expand All @@ -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(
Expand All @@ -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,
}

// ==================
Expand Down
96 changes: 96 additions & 0 deletions tests/difference/core/quint_model/driver/common.go
Original file line number Diff line number Diff line change
@@ -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,
},
},
},
}
}
Loading

0 comments on commit a4840fc

Please sign in to comment.