Skip to content

Commit

Permalink
Add trusting period
Browse files Browse the repository at this point in the history
  • Loading branch information
p-offtermatt committed Nov 6, 2023
1 parent 50231fb commit 2d29208
Show file tree
Hide file tree
Showing 6 changed files with 501 additions and 617 deletions.
5 changes: 5 additions & 0 deletions tests/difference/core/quint_model/ccv.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -235,6 +235,11 @@ module ccv {
// The timeoutTimestamp for sent packets. Can differ by chain.
const CcvTimeout: Chain -> int

// The trusting period on each chain.
// If headers on a channel between two chains are not updated within this period,
// they expire and the channel will be closed.
const TrustingPeriodPerChain: Chain -> int // TODO: USE THIS!

// ===================
// PROTOCOL LOGIC contains the meat of the protocol
// functions here roughly correspond to API calls that can be triggered from external sources
Expand Down
5 changes: 4 additions & 1 deletion tests/difference/core/quint_model/ccv_model.qnt
Original file line number Diff line number Diff line change
Expand Up @@ -8,17 +8,19 @@ module ccv_model {
pure val consumerChains = Set("consumer1", "consumer2", "consumer3")
pure val chains = consumerChains.union(Set(PROVIDER_CHAIN))
pure val unbondingPeriods = chains.mapBy(chain => 2 * Week)
pure val trustingPeriods = chains.mapBy(chain => 1 * Week)
pure val ccvTimeouts = chains.mapBy(chain => 3 * Week)

pure val nodes = Set("node1", "node2", "node3", "node4", "node5", "node6", "node7", "node8", "node9", "node10")
pure val InitialValidatorSet = nodes.mapBy(node => 100)

import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains).* from "./ccv"
import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains, TrustingPeriodPerChain = trustingPeriods).* from "./ccv"

type Parameters = {
VscTimeout: Time,
CcvTimeout: Chain -> Time,
UnbondingPeriodPerChain: Chain -> Time,
TrustingPeriodPerChain: Chain -> Time, // TODO: integrate trusting period in logic
ConsumerChains: Set[Chain],
Nodes: Set[Node],
InitialValidatorSet: Node -> int,
Expand Down Expand Up @@ -143,6 +145,7 @@ module ccv_model {
ConsumerChains: ConsumerChains,
Nodes: nodes,
InitialValidatorSet: InitialValidatorSet,
TrustingPeriodPerChain: TrustingPeriodPerChain,
}
}

Expand Down
132 changes: 49 additions & 83 deletions tests/difference/core/quint_model/driver/core.go
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ package main

import (
"fmt"
"strings"
"testing"
"time"

Expand Down Expand Up @@ -29,6 +30,7 @@ type ModelParams struct {
VscTimeout time.Duration
CcvTimeout map[ChainId]time.Duration
UnbondingPeriodPerChain map[ChainId]time.Duration
TrustingPeriodPerChain map[ChainId]time.Duration
}

type Driver struct {
Expand All @@ -55,7 +57,7 @@ func (s *Driver) path(chain ChainId) *simibc.RelayedPath {

// chain returns the TestChain for a given chain identifier
func (s *Driver) chain(chain ChainId) *ibctesting.TestChain {
return s.path(chain).Chain(string(chain))
return s.coordinator.GetChain(string(chain))
}

func (s *Driver) providerChain() *ibctesting.TestChain {
Expand Down Expand Up @@ -151,9 +153,9 @@ func (s *Driver) providerTokens(i int64) int64 {

func (s *Driver) validatorSet(chain ChainId) []stakingtypes.Validator {
if chain == P {
return s.providerStakingKeeper().GetLastValidators(s.ctx(P))
return s.providerStakingKeeper().GetAllValidators(s.ctx(P))
} else {
return s.consumerKeeper(chain).GetAllValidators(s.ctx(C))
return s.consumerKeeper(chain).GetAllValidators(s.ctx(chain))
}
}

Expand Down Expand Up @@ -222,6 +224,50 @@ func (s *Driver) deliver(chain ChainId, numPackets int) {
s.path(chain).DeliverPackets(string(chain), numPackets)
}

func (s *Driver) getStateString() string {
var state strings.Builder

state.WriteString("Provider\n")
state.WriteString(s.getChainStateString("provider"))
state.WriteString("\n")

for chain := range s.simibcs {
state.WriteString(fmt.Sprintf("Chain %s\n", chain))
state.WriteString(s.getChainStateString(chain))
state.WriteString("\n")
}

return state.String()
}

func (s *Driver) getChainStateString(chain ChainId) string {
ctx := s.ctx(chain)

// Get the current block height
height := ctx.BlockHeight()

// 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))

// 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()))
}

chainInfo.WriteString(validatorInfo.String())

return chainInfo.String()
}

func (s *Driver) endAndBeginBlock(chain ChainId, timeAdvancement time.Duration, preCommitCallback func()) {
s.path(chain).EndAndBeginBlock(string(chain), timeAdvancement, func() {
})
Expand All @@ -239,83 +285,3 @@ func newDriver(t *testing.T, valAddresses []sdk.ValAddress) *Driver {
}
return suite
}

// // The state of the data returned is equivalent to the state of two chains
// // after a full handshake, but the precise order of steps used to reach the
// // state does not necessarily mimic the order of steps that happen in a
// // live scenario.
// func GetZeroState(
// suite *suite.Suite,
// initState InitState,
// ) (path *ibctesting.Path, addrs []sdk.ValAddress, heightLastCommitted, timeLastCommitted int64) {
// b := Builder{initState: initState, suite: suite}

// b.createProviderAndConsumer()

// b.setProviderParams()

// // This is the simplest way to initialize the slash meter
// // after a change to the param value.
// b.providerKeeper().InitializeSlashMeter(b.providerCtx())

// b.addExtraProviderValidators()

// // Commit the additional validators
// b.coordinator.CommitBlock(b.provider())

// b.configurePath()

// // Create a client for the provider chain to use, using ibc go testing.
// b.createProvidersLocalClient()

// // Manually create a client for the consumer chain to and bootstrap
// // via genesis.
// clientState := b.createConsumersLocalClientGenesis()

// consumerGenesis := b.createConsumerGenesis(clientState)

// b.consumerKeeper().InitGenesis(b.consumerCtx(), consumerGenesis)

// // Client ID is set in InitGenesis and we treat it as a block box. So
// // must query it to use it with the endpoint.
// clientID, _ := b.consumerKeeper().GetProviderClientID(b.consumerCtx())
// b.consumerEndpoint().ClientID = clientID

// // Handshake
// b.coordinator.CreateConnections(b.path)
// b.coordinator.CreateChannels(b.path)

// // Usually the consumer sets the channel ID when it receives a first VSC packet
// // to the provider. For testing purposes, we can set it here. This is because
// // we model a blank slate: a provider and consumer that have fully established
// // their channel, and are ready for anything to happen.
// b.consumerKeeper().SetProviderChannel(b.consumerCtx(), b.consumerEndpoint().ChannelID)

// // Catch up consumer height to provider height. The provider was one ahead
// // from committing additional validators.
// simibc.EndBlock(b.consumer(), func() {})

// simibc.BeginBlock(b.consumer(), initState.BlockInterval)
// simibc.BeginBlock(b.provider(), initState.BlockInterval)

// // Commit a block on both chains, giving us two committed headers from
// // the same time and height. This is the starting point for all our
// // data driven testing.
// lastProviderHeader, _ := simibc.EndBlock(b.provider(), func() {})
// lastConsumerHeader, _ := simibc.EndBlock(b.consumer(), func() {})

// // Want the height and time of last COMMITTED block
// heightLastCommitted = b.provider().CurrentHeader.Height
// timeLastCommitted = b.provider().CurrentHeader.Time.Unix()

// // Get ready to update clients.
// simibc.BeginBlock(b.provider(), initState.BlockInterval)
// simibc.BeginBlock(b.consumer(), initState.BlockInterval)

// // Update clients to the latest header. Now everything is ready to go!
// // Ignore errors for brevity. Everything is checked in Assuptions test.
// _ = simibc.UpdateReceiverClient(b.consumerEndpoint(), b.providerEndpoint(), lastConsumerHeader)
// _ = simibc.UpdateReceiverClient(b.providerEndpoint(), b.consumerEndpoint(), lastProviderHeader)

// return b.path, b.valAddresses, heightLastCommitted, timeLastCommitted
// }
31 changes: 23 additions & 8 deletions tests/difference/core/quint_model/driver/mbt_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import (
"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"
)

// Given a map from node names to voting powers, create a validator set with the right voting powers.
Expand Down Expand Up @@ -61,11 +62,21 @@ func TestItfTrace(t *testing.T) {
log.Fatalf("Error loading trace file: %s", err)
}

if trace.Vars[0] != "currentState" ||
trace.Vars[1] != "params" ||
trace.Vars[2] != "trace" {
t.Fatalf("Error loading trace file %s: Variables should be currentState, params, trace but are %s",
path, trace.Vars)
expectedVarNames := []string{"currentState", "params", "trace"}

varNames := make(map[string]bool, len(expectedVarNames))
// populate the set
for _, varName := range trace.Vars {
varNames[varName] = true
}

// sanity check: there are as many var names as we expect
require.Equal(t, len(expectedVarNames), len(varNames), "Expected %v var names, got %v", expectedVarNames, varNames)

// sanity check: each expected var name should be in the set
for _, expectedVarName := range expectedVarNames {
_, ok := varNames[expectedVarName]
require.True(t, ok, "Expected var name %v not found in actual var names %v", expectedVarName, varNames)
}

t.Log("Reading params...")
Expand All @@ -92,16 +103,19 @@ func TestItfTrace(t *testing.T) {
vscTimeout := time.Duration(params["VscTimeout"].Value.(int64))

unbondingPeriodPerChain := make(map[ChainId]time.Duration, len(consumers))
trustingPeriodPerChain := make(map[ChainId]time.Duration, len(consumers))
ccvTimeoutPerChain := make(map[ChainId]time.Duration, len(consumers))
for _, consumer := range chains {
unbondingPeriodPerChain[ChainId(consumer)] = time.Duration(params["UnbondingPeriodPerChain"].Value.(itf.MapExprType)[consumer].Value.(int64))
ccvTimeoutPerChain[ChainId(consumer)] = time.Duration(params["CcvTimeout"].Value.(itf.MapExprType)[consumer].Value.(int64))
unbondingPeriodPerChain[ChainId(consumer)] = time.Duration(params["UnbondingPeriodPerChain"].Value.(itf.MapExprType)[consumer].Value.(int64)) * time.Second
trustingPeriodPerChain[ChainId(consumer)] = time.Duration(params["TrustingPeriodPerChain"].Value.(itf.MapExprType)[consumer].Value.(int64)) * time.Second
ccvTimeoutPerChain[ChainId(consumer)] = time.Duration(params["CcvTimeout"].Value.(itf.MapExprType)[consumer].Value.(int64)) * time.Second
}

modelParams := ModelParams{
VscTimeout: vscTimeout,
CcvTimeout: ccvTimeoutPerChain,
UnbondingPeriodPerChain: unbondingPeriodPerChain,
TrustingPeriodPerChain: trustingPeriodPerChain,
}

valExprs := params["Nodes"].Value.(itf.ListExprType)
Expand Down Expand Up @@ -146,7 +160,8 @@ func TestItfTrace(t *testing.T) {
actionKind := lastAction["kind"].Value.(string)
switch actionKind {
case "init":
// start the chain(s)
t.Log("Initializing...")
t.Logf(driver.getStateString())
case "VotingPowerChange":
node := lastAction["validator"].Value.(string)
newVotingPower := lastAction["newVotingPower"].Value.(int64)
Expand Down
Loading

0 comments on commit 2d29208

Please sign in to comment.