From d60b880e3605dce895a3550163c22a7f4319e360 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt <57488781+p-offtermatt@users.noreply.github.com> Date: Mon, 29 Jan 2024 10:45:31 +0100 Subject: [PATCH] test: add key assignment to model and driver (#1573) * Start implementing key assignment in Quint * Update model * Update model * Update model * Add key assignment to functional layer * Start writing test for key assignment * Continue adding key assignment to model * Fix some behaviours in key assignment logic * Pull key assignment into its own module * Split key assignment into extra module * Start updating invariants for key assignment * Update key assignment spec * Merge key assignment into main model * Update spec, fix bug * Fix map building for key assignment * Fix key assignment invariants * Update driver to include key assignment * Fix key assignment in bounded steps * Finish key assignment integration in driver * Update clients every block * Add key assignment to invariant check * Use key assignment in its step * Revert changes to extraSpells * Add check to avoid empty set of running consumers * Update tests/mbt/model/ccv.qnt Co-authored-by: insumity * Update tests/mbt/model/ccv.qnt Co-authored-by: insumity * Incorporate review comments * Refactor keyAssignmentReplacement * Start refactoring a few things * Refactor, take into account comments * Refactor utility functions to type module * Minor refactor * Refactor utils into own file * Add key assignment invariant checks to make target * Add empty-list-handling to inv * Start refactoring keys of sentVscPackets map * Fix keys for packet map * Fix path to model * Add more comments, remove unnecessary disjuncts --------- Co-authored-by: insumity --- Makefile | 3 +- tests/mbt/driver/core.go | 15 +- tests/mbt/driver/generate_more_traces.sh | 3 +- tests/mbt/driver/generate_traces.sh | 3 +- tests/mbt/driver/mbt_test.go | 125 +++++-- tests/mbt/driver/stats.go | 2 + tests/mbt/model/README.md | 20 +- tests/mbt/model/ccv.qnt | 444 +++++++--------------- tests/mbt/model/ccv_boundeddrift.qnt | 14 +- tests/mbt/model/ccv_model.qnt | 307 ++++++++++++++- tests/mbt/model/ccv_test.qnt | 1 + tests/mbt/model/ccv_utils.qnt | 456 +++++++++++++++++++++++ tests/mbt/run_invariants.sh | 3 +- 13 files changed, 1042 insertions(+), 354 deletions(-) create mode 100644 tests/mbt/model/ccv_utils.qnt diff --git a/Makefile b/Makefile index 350c66f8af..7c30540cd3 100644 --- a/Makefile +++ b/Makefile @@ -131,7 +131,8 @@ test-trace: 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 + quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" tests/mbt/model/ccv_model.qnt --max-steps 200 --max-samples 200;\ + quint run --invariant "all{ValidatorUpdatesArePropagatedKeyAssignmentInv,ValidatorSetHasExistedKeyAssignmentInv,SameVscPacketsKeyAssignmentInv,MatureOnTimeInv,EventuallyMatureOnProviderInv,KeyAssignmentRulesInv}" tests/mbt/model/ccv_model.qnt --step stepKeyAssignment --max-steps 200 --max-samples 200 diff --git a/tests/mbt/driver/core.go b/tests/mbt/driver/core.go index f9f1e12e05..b9a4293df1 100644 --- a/tests/mbt/driver/core.go +++ b/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" @@ -123,9 +124,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 { @@ -370,6 +375,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. diff --git a/tests/mbt/driver/generate_more_traces.sh b/tests/mbt/driver/generate_more_traces.sh index 9af4da82e9..40589bb83b 100755 --- a/tests/mbt/driver/generate_more_traces.sh +++ b/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 \ No newline at end of file +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 \ No newline at end of file diff --git a/tests/mbt/driver/generate_traces.sh b/tests/mbt/driver/generate_traces.sh index ca0a6ba973..9f1134fb26 100755 --- a/tests/mbt/driver/generate_traces.sh +++ b/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 \ No newline at end of file +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 \ No newline at end of file diff --git a/tests/mbt/driver/mbt_test.go b/tests/mbt/driver/mbt_test.go index 78f9e7910f..a55d870dda 100644 --- a/tests/mbt/driver/mbt_test.go +++ b/tests/mbt/driver/mbt_test.go @@ -15,10 +15,13 @@ import ( "github.com/kylelemons/godebug/pretty" "github.com/stretchr/testify/require" - sdktypes "github.com/cosmos/cosmos-sdk/types" - cmttypes "github.com/cometbft/cometbft/types" + tmencoding "github.com/cometbft/cometbft/crypto/encoding" + "github.com/cosmos/interchain-security/v4/testutil/integration" + + sdktypes "github.com/cosmos/cosmos-sdk/types" + providertypes "github.com/cosmos/interchain-security/v4/x/ccv/provider/types" ) @@ -69,6 +72,7 @@ func TestMBT(t *testing.T) { t.Logf("Number of sent packets: %v", stats.numSentPackets) t.Logf("Number of blocks: %v", stats.numBlocks) t.Logf("Number of transactions: %v", stats.numTxs) + t.Logf("Number of key assignments: %v", stats.numKeyAssignments) t.Logf("Average summed block time delta passed per trace: %v", stats.totalBlockTimePassedPerTrace/time.Duration(numTraces)) } @@ -117,6 +121,21 @@ func RunItfTrace(t *testing.T, path string) { t.Log("Chains are: ", chains) + // generate keys that can be assigned on consumers, according to the ConsumerAddresses in the trace + consumerAddressesExpr := params["ConsumerAddresses"].Value.(itf.ListExprType) + + _, _, consumerPrivVals, err := integration.CreateValidators(len(consumerAddressesExpr)) + require.NoError(t, err, "Error creating consumer signers") + + consumerAddrNamesToPrivVals := make(map[string]cmttypes.PrivValidator, len(consumerAddressesExpr)) + realAddrsToModelConsAddrs := make(map[string]string, len(consumerAddressesExpr)) + i := 0 + for address, privVal := range consumerPrivVals { + consumerAddrNamesToPrivVals[consumerAddressesExpr[i].Value.(string)] = privVal + realAddrsToModelConsAddrs[address] = consumerAddressesExpr[i].Value.(string) + i++ + } + // create params struct vscTimeout := time.Duration(params["VscTimeout"].Value.(int64)) * time.Second @@ -145,6 +164,15 @@ func RunItfTrace(t *testing.T, path string) { valSet, addressMap, signers, err := CreateValSet(initialValSet) require.NoError(t, err, "Error creating validator set") + // get the set of signers for consumers: the validator signers, plus signers for the assignable addresses + consumerSigners := make(map[string]cmttypes.PrivValidator, 0) + for consAddr, consPrivVal := range consumerPrivVals { + consumerSigners[consAddr] = consPrivVal + } + for consAddr, signer := range signers { + consumerSigners[consAddr] = signer + } + // get a slice of validators in the right order nodes := make([]*cmttypes.Validator, len(valNames)) for i, valName := range valNames { @@ -211,6 +239,10 @@ func RunItfTrace(t *testing.T, path string) { // and then increment the rest of the time runningConsumersBefore := driver.runningConsumers() driver.endAndBeginBlock("provider", 1*time.Nanosecond) + for _, consumer := range driver.runningConsumers() { + UpdateProviderClientOnConsumer(t, driver, consumer.ChainId) + } + driver.endAndBeginBlock("provider", time.Duration(timeAdvancement)*time.Second-1*time.Nanosecond) runningConsumersAfter := driver.runningConsumers() @@ -243,7 +275,7 @@ func RunItfTrace(t *testing.T, path string) { consumer.Value.(string), modelParams, driver.providerChain().Vals, - signers, + consumerSigners, nodes, valNames, driver.providerChain(), @@ -268,11 +300,8 @@ func RunItfTrace(t *testing.T, path string) { if len(consumersToStart) > 0 && consumer.ChainId == consumersToStart[len(consumersToStart)-1].Value.(string) { continue } - consumerChainId := consumer.ChainId - driver.path(ChainId(consumerChainId)).AddClientHeader(PROVIDER, driver.providerHeader()) - err := driver.path(ChainId(consumerChainId)).UpdateClient(consumerChainId, false) - require.True(t, err == nil, "Error updating client from %v on provider: %v", consumerChainId, err) + UpdateProviderClientOnConsumer(t, driver, consumer.ChainId) } case "EndAndBeginBlockForConsumer": @@ -286,13 +315,12 @@ func RunItfTrace(t *testing.T, path string) { _ = headerBefore driver.endAndBeginBlock(ChainId(consumerChain), 1*time.Nanosecond) + UpdateConsumerClientOnProvider(t, driver, consumerChain) + driver.endAndBeginBlock(ChainId(consumerChain), time.Duration(timeAdvancement)*time.Second-1*time.Nanosecond) // update the client on the provider - consumerHeader := driver.chain(ChainId(consumerChain)).LastHeader - driver.path(ChainId(consumerChain)).AddClientHeader(consumerChain, consumerHeader) - err := driver.path(ChainId(consumerChain)).UpdateClient(PROVIDER, false) - require.True(t, err == nil, "Error updating client from %v on provider: %v", consumerChain, err) + UpdateConsumerClientOnProvider(t, driver, consumerChain) case "DeliverVscPacket": consumerChain := lastAction["consumerChain"].Value.(string) @@ -328,8 +356,26 @@ func RunItfTrace(t *testing.T, path string) { expectError = false driver.DeliverPacketFromConsumer(ChainId(consumerChain), expectError) } - default: + case "KeyAssignment": + consumerChain := lastAction["consumerChain"].Value.(string) + node := lastAction["validator"].Value.(string) + consumerAddr := lastAction["consumerAddr"].Value.(string) + + t.Log("KeyAssignment", consumerChain, node, consumerAddr) + stats.numKeyAssignments++ + valIndex := getIndexOfString(node, valNames) + assignedPrivVal := consumerAddrNamesToPrivVals[consumerAddr] + assignedKey, err := assignedPrivVal.GetPubKey() + require.NoError(t, err, "Error getting pubkey") + + protoPubKey, err := tmencoding.PubKeyToProto(assignedKey) + require.NoError(t, err, "Error converting pubkey to proto") + + error := driver.AssignKey(ChainId(consumerChain), int64(valIndex), protoPubKey) + require.NoError(t, error, "Error assigning key") + + default: log.Fatalf("Error loading trace file %s, step %v: do not know action type %s", path, index, actionKind) } @@ -364,7 +410,7 @@ func RunItfTrace(t *testing.T, path string) { require.Equal(t, modelRunningConsumers, actualRunningConsumers, "Running consumers do not match") // check validator sets - provider current validator set should be the one from the staking keeper - CompareValidatorSets(t, driver, currentModelState, actualRunningConsumers) + CompareValidatorSets(t, driver, currentModelState, actualRunningConsumers, realAddrsToModelConsAddrs) // check times - sanity check that the block times match the ones from the model CompareTimes(driver, actualRunningConsumers, currentModelState, timeOffset) @@ -383,7 +429,27 @@ func RunItfTrace(t *testing.T, path string) { t.Log("🟢 Trace is ok!") } -func CompareValidatorSets(t *testing.T, driver *Driver, currentModelState map[string]itf.Expr, consumers []string) { +func UpdateProviderClientOnConsumer(t *testing.T, driver *Driver, consumerChainId string) { + driver.path(ChainId(consumerChainId)).AddClientHeader(PROVIDER, driver.providerHeader()) + err := driver.path(ChainId(consumerChainId)).UpdateClient(consumerChainId, false) + require.True(t, err == nil, "Error updating client from %v on provider: %v", consumerChainId, err) +} + +func UpdateConsumerClientOnProvider(t *testing.T, driver *Driver, consumerChain string) { + consumerHeader := driver.chain(ChainId(consumerChain)).LastHeader + driver.path(ChainId(consumerChain)).AddClientHeader(consumerChain, consumerHeader) + err := driver.path(ChainId(consumerChain)).UpdateClient(PROVIDER, false) + require.True(t, err == nil, "Error updating client from %v on provider: %v", consumerChain, err) +} + +func CompareValidatorSets( + t *testing.T, + driver *Driver, + currentModelState map[string]itf.Expr, + consumers []string, + // a map from real addresses to the names of those consumer addresses in the model + keyAddrsToModelConsAddrName map[string]string, +) { t.Helper() modelValSet := ValidatorSet(currentModelState, "provider") @@ -407,23 +473,28 @@ func CompareValidatorSets(t *testing.T, driver *Driver, currentModelState map[st pubkey, err := val.ConsPubKey() require.NoError(t, err, "Error getting pubkey") - consAddr := providertypes.NewConsumerConsAddress(sdktypes.ConsAddress(pubkey.Address().Bytes())) + consAddrModelName, ok := keyAddrsToModelConsAddrName[pubkey.Address().String()] + if ok { // the node has a key assigned, use the name of the consumer address in the model + consumerCurValSet[consAddrModelName] = val.Power + } else { // the node doesn't have a key assigned yet, get the validator moniker + consAddr := providertypes.NewConsumerConsAddress(sdktypes.ConsAddress(pubkey.Address().Bytes())) - // the consumer vals right now are CrossChainValidators, for which we don't know their mnemonic - // so we need to find the mnemonic of the consumer val now to enter it by name in the map + // the consumer vals right now are CrossChainValidators, for which we don't know their mnemonic + // so we need to find the mnemonic of the consumer val now to enter it by name in the map - // get the address on the provider that corresponds to the consumer address - providerConsAddr, found := driver.providerKeeper().GetValidatorByConsumerAddr(driver.providerCtx(), consumer, consAddr) - if !found { - providerConsAddr = providertypes.NewProviderConsAddress(consAddr.Address) - } + // get the address on the provider that corresponds to the consumer address + providerConsAddr, found := driver.providerKeeper().GetValidatorByConsumerAddr(driver.providerCtx(), consumer, consAddr) + if !found { + providerConsAddr = providertypes.NewProviderConsAddress(consAddr.Address) + } - // get the validator for that address on the provider - providerVal, found := driver.providerStakingKeeper().GetValidatorByConsAddr(driver.providerCtx(), providerConsAddr.Address) - require.True(t, found, "Error getting provider validator") + // get the validator for that address on the provider + providerVal, found := driver.providerStakingKeeper().GetValidatorByConsAddr(driver.providerCtx(), providerConsAddr.Address) + require.True(t, found, "Error getting provider validator") - // use the moniker of that validator - consumerCurValSet[providerVal.GetMoniker()] = val.Power + // use the moniker of that validator + consumerCurValSet[providerVal.GetMoniker()] = val.Power + } } require.NoError(t, CompareValSet(modelValSet, consumerCurValSet), "Validator sets do not match for consumer %v", consumer) } diff --git a/tests/mbt/driver/stats.go b/tests/mbt/driver/stats.go index 0d397571be..8b4c95a3dd 100644 --- a/tests/mbt/driver/stats.go +++ b/tests/mbt/driver/stats.go @@ -16,4 +16,6 @@ type Stats struct { numTxs int totalBlockTimePassedPerTrace time.Duration + + numKeyAssignments int } diff --git a/tests/mbt/model/README.md b/tests/mbt/model/README.md index f53900e77f..57f5b2eda9 100644 --- a/tests/mbt/model/README.md +++ b/tests/mbt/model/README.md @@ -31,16 +31,25 @@ All the logic in EndBlock/BeginBlock happens here, like updating the validator s * `EndAndBeginBlockForConsumer(chain: Chain, timeAdvancement: Time)`: On the consumer `chain`, ends the current block, and begins a new one. Again, all the logic in EndBlock/BeginBlock happens here, like validator set change maturations. * `DeliverVscPacket(receiver: Chain)`: Delivers a pending VSCPacket from the provider to the consumer `receiver`. * `DeliverVscMaturedPacket(receiver: Chain)`: Delivers a pending VSCMaturedPacket from the consumer `receiver` to the provider. +* `KeyAssignment(chain: Chain, validator: Node, consumerAddr: ConsumerAddr)` (only when running with `--step stepKeyAssignment`): Assigns the `consumerAddr` to the `validator` on the `chain`. Note that we use "key" and "consumerAddr" pretty much interchangeably, as the model makes no differentiation between private keys, public keys, addresses, etc, as it doesn't model the cryptography. ### State machines There are 3 different "state machine layers" that can be put on top of the core logic. +Some layers include extra logic, need other invariants, ... #### ccv_model.qnt This is the most general state machine layer. It allows the most behaviour, in particular it allows abitrary clock drift between chains, it allows starting and stopping consumer chains during runtime, etc. This layer is most useful for model checking, because it encompasses the most behaviour. +As an optional module, it can also include KeyAssignment. + +##### KeyAssignment + +To run with key assignment, specify the step flag: `--step stepKeyAssignment`. + +KeyAssignment also needs some different invariants, see below. #### ccv_boundeddrift.qnt This state machine layer is more restricted to generate more interesting traces: @@ -94,6 +103,13 @@ with a timestamp >= t + UnbondingPeriod on that consumer. - [X] EventuallyMatureOnProviderInv: If we send a VscPacket, this is eventually responded to by all consumers that were running at the time the packet was sent (and are still running). +Invariants only relevant when running with key assignment (`--step stepKeyAssignment`): +- [X] ValidatorSetHasExistedKeyAssignmentInv: Should replace ValidatorSetHasExistedInv when running with `--step stepKeyAssignment`. Validator sets are checked for equality under key assignment when checking whether they have existed. +- [X] SameVscPacketsKeyAssignmentInv: Should replace SameVscPacketsInv when running with `--step stepKeyAssignment`. VscPackets are checked for equality under key assignment when ensuring consumers receive the same ones. +- [X] KeyAssignmentRulesInv: Ensures the rules of key assignment are never violated. The two rules relevant for the model are: 1) validator A cannot assign consumer key K to consumer chain X if there is already a validator B (B!=A) +using K on the provider, and 2) validator A cannot assign consumer key K to consumer chain X if there is already a validator B using K on X + + Invariants can also be model-checked by Apalache, using this command: ``` quint verify --invariant ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv \ @@ -113,4 +129,6 @@ The available sanity checks are: - CanStopConsumer - CanTimeoutConsumer - CanSendVscPackets -- CanSendVscMaturedPackets \ No newline at end of file +- CanSendVscMaturedPackets +- CanAssignConsumerKey (only with `--step stepKeyAssignment`) +- CanHaveConsumerAddresses (only with `--step stepKeyAssignment`) \ No newline at end of file diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index 6d9450b6f0..0e42436c50 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -1,6 +1,7 @@ // -*- mode: Bluespec; -*- module ccv_types { import Time.* from "./libraries/Time" + import extraSpells.* from "./libraries/extraSpells" type Node = str type Chain = str @@ -11,6 +12,11 @@ module ccv_types { // a list of validator sets per blocks, ordered by recency type VotingPowerHistory = List[ValidatorSet] + // For key assignment, to differentiate Nodes + // (on the provider) from the assigned + // keys/addresses on consumers + type ConsumerAddr = str + type VscPacket = { // the identifier for this packet @@ -93,6 +99,28 @@ module ccv_types { // a monotonic strictly increasing and positive ID that is used // to uniquely identify the Vscs sent to the consumer chains. runningVscId: int, + + // For every consumer chain, stores the consumer address assigned by each validator. + validatorToConsumerAddr: Chain -> (Node -> ConsumerAddr), + + // For every consumer chain, holds the provider validator for each assigned consumer address. + // Note that this is *not* precisely the reverse of validatorToConsumerAddr, + // because when a validator changes their consumer addr, + // the old one stays in this map until pruned. + consumerAddrToValidator: Chain -> (ConsumerAddr -> Node), + + // For every consumer chain, stores whether the key assignment for the consumer chain has changed in this block. + consumersWithAddrAssignmentChangesInThisBlock: Set[Chain], + + // the history of validator sets on the provider, but with the key assignments applied. + // This is needed to check invariants about the validator set when key assignments are in play. + keyAssignedValSetHistory: Chain -> VotingPowerHistory, + + // Stores the mapping from VSC ids to consumer validators addresses. Needed for pruning consumerAddrToValidator. + consumerAddrsToPrune: Chain -> VscId -> List[ConsumerAddr], + + // For every sent VSCPacket, stores the key assignments that were applied to send it. + keyAssignmentsForVSCPackets: VscId -> (Chain -> (Node -> ConsumerAddr)) } // utility function: returns a provider state that is initialized minimally. @@ -105,6 +133,12 @@ module ccv_types { providerValidatorSetChangedInThisBlock: false, consumerStatus: Map(), runningVscId: 0, + validatorToConsumerAddr: Map(), + keyAssignedValSetHistory: Map(), + consumerAddrToValidator: Map(), + consumerAddrsToPrune: Map(), + keyAssignmentsForVSCPackets: Map(), + consumersWithAddrAssignmentChangesInThisBlock: Set() } @@ -212,6 +246,7 @@ module ccv { import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" import ccv_types.* + import ccv_utils.* from "./ccv_utils" // =================== @@ -356,7 +391,7 @@ module ccv { } } else { // the packet has not timed out, so receive it on the consumer - val result = recvPacketOnConsumer(currentState, receiver, packet) + val result = recvPacketOnConsumer(currentState, receiver, packet, UnbondingPeriodPerChain.get(receiver)) val tmpState = result.newState if (result.hasError()) { (result, false) @@ -389,32 +424,41 @@ module ccv { // check for vsc timeouts val timedOutConsumers = getRunningConsumers(currentProviderState).filter( consumer => - val res = TimeoutDueToVscTimeout(currentState, consumer) + val res = TimeoutDueToVscTimeout(currentState, consumer, VscTimeout) res._1 ) + // for each consumer chain, apply the key assignment to the current validator set + val currentValSets = ConsumerChains.mapBy( + (consumer) => + currentProviderState.applyKeyAssignmentToValSet( + consumer, + currentProviderState.chainState.currentValidatorSet + ) + ) + // store the current validator set with the key assignments applied in the history + val newKeyAssignedValSetHistory = currentValSets.keys().mapBy( + (consumer) => + currentProviderState.keyAssignedValSetHistory + .getOrElse(consumer, List()) // get the existing history (empty list if no history yet) + .prepend(currentValSets.get(consumer)) // prepend the current validator set with key assignments applied + ) // run the shared core chainState logic val newChainState = currentProviderState.chainState.endAndBeginBlockShared(timeAdvancement) - val providerStateAfterTimeAdvancement = currentProviderState.with( - "chainState", newChainState - ) - + val providerStateAfterTimeAdvancement = + {...currentProviderState, chainState: newChainState, keyAssignedValSetHistory: newKeyAssignedValSetHistory} val tmpState = currentState.with( "providerState", providerStateAfterTimeAdvancement ) - // send vsc packets + // send vsc packets (will be a noop if no sends are necessary) val providerStateAfterSending = - if (currentProviderState.providerValidatorSetChangedInThisBlock and - // important: check this on the provider state after the consumer advancement, not on the current state. - getRunningConsumers(providerStateAfterTimeAdvancement).size() > 0) { - // need to use the old timestamp because this happens during EndBlock - providerStateAfterTimeAdvancement.sendVscPackets(currentProviderState.chainState.runningTimestamp) - } else { - providerStateAfterTimeAdvancement - } + providerStateAfterTimeAdvancement.sendVscPackets( + currentProviderState.chainState.runningTimestamp, + CcvTimeout.get(PROVIDER_CHAIN) + ) // start/stop chains @@ -434,19 +478,21 @@ module ccv { if (err != "") { Err(err) } else { - // for each consumer we just set to running, set its initial validator set to be the current one on the provider. + // for each consumer we just set to running, set its initial validator set to be the current one on the provider... val valSet = providerStateAfterConsumerAdvancement.chainState.currentValidatorSet val newConsumerStateMap = tmpState.consumerStates.keys().mapBy( (consumer) => if (consumersToStart.contains(consumer)) { + // ...modified by the key assignments for the consumer + val consValSet = applyKeyAssignmentToValSet(providerStateAfterConsumerAdvancement, consumer, valSet) val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer) val newConsumerState: ConsumerState = currentConsumerState.with( "chainState", currentConsumerState.chainState.with( - "currentValidatorSet", valSet + "currentValidatorSet", consValSet ).with( "votingPowerHistory", - List(valSet) + List(consValSet) ).with( "lastTimestamp", providerStateAfterConsumerAdvancement.chainState.lastTimestamp @@ -523,308 +569,90 @@ module ccv { } } - // =================== - // UTILITY FUNCTIONS - // which do not hold the core logic of the protocol, but are still part of it - // =================== - - // Returns the new ConsumerStatusMap according to the consumers to stop - // and the consumers to time out. - // If a consumer is both stopped and timed out, it will be timed out. - // The second return is an error string: If it is not equal to "", - // it contains an error message, and the first return should be ignored. - pure def stopConsumers( - currentConsumerStatusMap: Chain -> str, - consumersToStop: Set[Chain], - consumersToTimeout: Set[Chain]): (Chain -> str, str) = { - val runningConsumers = currentConsumerStatusMap.keys().filter( - chain => currentConsumerStatusMap.get(chain) == RUNNING - ) - // all consumers to stop must be running right now, else we have an error - if (consumersToStop.exclude(runningConsumers).size() > 0) { - (currentConsumerStatusMap, "Cannot stop a consumer that is not running") + // Validator providerNode assigns their address for the consumer to be the consumerAddress. + pure def assignConsumerKey(currentState: ProtocolState, consumer: Chain, providerNode: Node, consumerAddr: ConsumerAddr): Result = { + // rule 1: validator A cannot assign consumer key K to consumer chain X + // if there is already a validator B (B!=A) using K on the provider + pure val provCurValSet = currentState.providerState.chainState.currentValidatorSet + if (provCurValSet.keys().exists(node => node != providerNode and node == consumerAddr)) { + Err("validator A cannot assign consumer key K to consumer chain X + if there is already a validator B (B!=A) using K on the provider") + } else { + // rule 2: validator A cannot assign consumer key K to consumer chain X if + // there is already a validator B using K on X + pure val valByConsAddr = currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()) + if (valByConsAddr.keys().contains(consumerAddr)) { + Err("consumer key is already in use on the consumer chain") } else { - val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( - (chain) => - if (consumersToTimeout.contains(chain)) { - TIMEDOUT - } else if (consumersToStop.contains(chain)) { - STOPPED + // this key can be assigned + + // get the old assigned key + pure val consKeyByVal = currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) + pure val p = if (consKeyByVal.keys().contains(providerNode)) { + // providerNode had previously assigned a consumer key + (consKeyByVal.get(providerNode), true) + } else { + (providerNode, false) + } + // the consumer address that was previously associated with the node + pure val oldConsAddr = p._1 + // whether the old address was explicitly assigned, or the default key + pure val prevAssigned = p._2 + + // set the old address for pruning, if it was assigned + pure val tmpState = if (prevAssigned) { + AppendConsumerAddrToPrune(currentState, oldConsAddr, consumer) + } else { + currentState + } + + // check whether the validator has positive power + pure val provValSet = currentState.providerState.chainState.currentValidatorSet + pure val provValPower = if (provValSet.keys().contains(providerNode)) provValSet.get(providerNode) else 0 + pure val consumersWithAddrAssignmentChangesInThisBlock = + if (provValPower > 0) { + // if the consumer has positive power, the relevant key assignment for the consumer changed + currentState.providerState.consumersWithAddrAssignmentChangesInThisBlock.union(Set(consumer)) } else { - currentConsumerStatusMap.get(chain) + // otherwise, the consumer doesn't need to know about the change, so no change + currentState.providerState.consumersWithAddrAssignmentChangesInThisBlock } + pure val tmpStateAfterKeyAssignmentReplacement = tmpState.with( + "providerState", tmpState.providerState.with( + "consumersWithAddrAssignmentChangesInThisBlock", consumersWithAddrAssignmentChangesInThisBlock + ) ) - (newConsumerStatusMap, "") - } - } - - // Returns the new ConsumerStatusMap according to the consumers to start. - // The second return is an error string: If it is not equal to "", - // it contains an error message, and the first return should be ignored. - pure def startConsumers( - currentConsumerStatusMap: Chain -> str, - consumersToStart: Set[Chain]): (Chain -> str, str) = { - val nonConsumers = currentConsumerStatusMap.keys().filter( - chain => currentConsumerStatusMap.get(chain) == NOT_CONSUMER - ) - // all consumers to start must be nonConsumers right now, otherwise we have an error - if (consumersToStart.exclude(nonConsumers).size() > 0) { - (currentConsumerStatusMap, "cannot start a consumer that is stopped or already a consumer") - } else { - val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( - (chain) => - if (consumersToStart.contains(chain)) { - RUNNING - } else { - currentConsumerStatusMap.get(chain) - } + + pure val newvalidatorToConsumerAddr = currentState.providerState.validatorToConsumerAddr.put( + consumer, + currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()).put( + providerNode, + consumerAddr + ) ) - (newConsumerStatusMap, "") - } - } - - pure def StartStopConsumers( - currentConsumerStatusMap: Chain -> str, - consumersToStart: Set[Chain], - consumersToStop: Set[Chain], - consumersToTimeout: Set[Chain] - ): (Chain -> str, str) = { - // check if any consumer is both started and stopped - if (consumersToStart.intersect(consumersToStop).size() > 0) { - (currentConsumerStatusMap, "Cannot start and stop a consumer at the same time") - } else { - val res1 = currentConsumerStatusMap.startConsumers(consumersToStart) - val newConsumerStatus = res1._1 - val err1 = res1._2 - val res2 = newConsumerStatus.stopConsumers(consumersToStop, consumersToTimeout) - val err2 = res2._2 - if (err1 != "") { - (currentConsumerStatusMap, err1) - } else if (err2 != "") { - (currentConsumerStatusMap, err2) - } else { - (res2._1, "") - } - } - } - - - // Takes the currentValidatorSet and puts it as the newest set of the voting history - pure def enterCurValSetIntoBlock(chainState: ChainState): ChainState = { - chainState.with( - "votingPowerHistory", chainState.votingPowerHistory.prepend( - chainState.currentValidatorSet - ) - ) - } - - // Advances the timestamp in the chainState by timeAdvancement - pure def advanceTime(chainState: ChainState, timeAdvancement: Time): ChainState = - { - ...chainState, - lastTimestamp: chainState.runningTimestamp, - runningTimestamp: chainState.runningTimestamp + timeAdvancement, - } - // common logic to update the chain state, used by both provider and consumers. - pure def endAndBeginBlockShared(chainState: ChainState, timeAdvancement: Time): ChainState = { - chainState.enterCurValSetIntoBlock().advanceTime(timeAdvancement) - } - - // returns the providerState with the following modifications: - // * sends VscPackets to all running consumers, using the provided timestamp as sending time - // * increments the runningVscId - // This should only be called when the provider chain is ending a block, - // and only when the running validator set is considered to have changed - // and there is a consumer to send a packet to. - pure def sendVscPackets(providerState: ProviderState, sendingTimestamp: Time): ProviderState = { - val newSentPacketsPerConsumer = ConsumerChains.mapBy( - (consumer) => - // if validator set changed and the consumer is running, send a packet - if (providerState.providerValidatorSetChangedInThisBlock and - isRunningConsumer(consumer, providerState)) { - List({ - id: providerState.runningVscId, - validatorSet: providerState.chainState.currentValidatorSet, - sendingTime: sendingTimestamp, - timeoutTime: sendingTimestamp + CcvTimeout.get(PROVIDER_CHAIN) - }) - } else { - List() - } - ) - val newOutstandingPacketsToConsumer = ConsumerChains.mapBy( - (consumer) => - providerState.outstandingPacketsToConsumer.get(consumer).concat( - newSentPacketsPerConsumer.get(consumer) - ) - ) - val newSentVscPackets = ConsumerChains.mapBy( - (consumer) => - providerState.sentVscPacketsToConsumer.get(consumer).concat( - newSentPacketsPerConsumer.get(consumer) + pure val newconsumerAddrToValidator = currentState.providerState.consumerAddrToValidator.put( + consumer, + currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()).put( + consumerAddr, + providerNode ) ) - { - ...providerState, - outstandingPacketsToConsumer: newOutstandingPacketsToConsumer, - sentVscPacketsToConsumer: newSentVscPackets, - providerValidatorSetChangedInThisBlock: false, - runningVscId: providerState.runningVscId + 1, - } - } - // receives a given packet (sent by the provider) on the consumer. The arguments are the consumer chain that is receiving the packet, and the packet itself. - // To receive a packet, modify the running validator set (not the one entered into the block yet, - // but the candidate that would be put into the block if it ended now) - // and store the maturation time for the packet. - pure def recvPacketOnConsumer(currentState: ProtocolState, receiver: Chain, packet: VscPacket): Result = { - if(not(isRunningConsumer(receiver, currentState.providerState))) { - Err("Receiver is not currently a consumer - must have 'running' status!") - } else { - // update the running validator set, but not the history yet, - // as that only happens when the next block is started - val currentConsumerState: ConsumerState = currentState.consumerStates.get(receiver) - val newConsumerState: ConsumerState = - { - ...currentConsumerState, - chainState: currentConsumerState.chainState.with( - "currentValidatorSet", packet.validatorSet - ), - maturationTimes: currentConsumerState.maturationTimes.append( - ( - packet, - currentConsumerState.chainState.runningTimestamp + UnbondingPeriodPerChain.get(receiver) - ) - ), - receivedVscPackets: currentConsumerState.receivedVscPackets.prepend(packet) - } - val newConsumerStates = currentState.consumerStates.set(receiver, newConsumerState) - val newState = currentState.with( - "consumerStates", newConsumerStates - ) - Ok(newState) - } - } - - // receives a given packet on the provider. The arguments are the consumer chain that sent the packet, and the packet itself. - // To receive a packet, add it to the list of received maturations. - pure def recvPacketOnProvider(currentState: ProtocolState, sender: Chain, packet: VscMaturedPacket): Result = { - if (not(isRunningConsumer(sender, currentState.providerState))) { - Err("Sender is not currently a consumer - must have 'running' status!") - } else if (currentState.providerState.sentVscPacketsToConsumer.get(sender).head().id != packet.id) { - // the packet is not the oldest sentVscPacket, something went wrong - Err("Received maturation is not for the oldest sentVscPacket") - } else { - val currentReceivedMaturations = currentState.providerState.receivedMaturations - val newReceivedMaturations = currentReceivedMaturations.union(Set(packet)) - val newProviderState = currentState.providerState.with( - "receivedMaturations", newReceivedMaturations - ) - // prune the sentVscPacket - val newSentVscPacket = currentState.providerState.sentVscPacketsToConsumer.get(sender).tail() - val newState = currentState.with( - "providerState", - {...newProviderState, - sentVscPacketsToConsumer: currentState.providerState.sentVscPacketsToConsumer.set(sender, newSentVscPacket) - } - ) - Ok(newState) - } - } - - // removes the oldest outstanding packet from the consumer. on-chain, this would happen when the packet is acknowledged. - // only the oldest packet can be removed, since we model ordered channels. - pure def removeOutstandingPacketFromConsumer(currentState: ProtocolState, sender: Chain): ProtocolState = { - val currentOutstandingPackets = currentState.consumerStates.get(sender).outstandingPacketsToProvider - val newOutstandingPackets = currentOutstandingPackets.tail() - val newConsumerState = currentState.consumerStates.get(sender).with( - "outstandingPacketsToProvider", newOutstandingPackets - ) - val newConsumerStates = currentState.consumerStates.set(sender, newConsumerState) - val newState = currentState.with( - "consumerStates", newConsumerStates - ) - newState - } - - // removes the oldest outstanding packet (to the given consumer) from the provider. - // on-chain, this would happen when the packet is acknowledged. - // only the oldest packet can be removed, since we model ordered channels. - pure def removeOutstandingPacketFromProvider(currentState: ProtocolState, receiver: Chain): ProtocolState = { - val currentOutstandingPackets = currentState.providerState.outstandingPacketsToConsumer.get(receiver) - val newOutstandingPackets = currentOutstandingPackets.tail() - val newProviderState = currentState.providerState.with( - "outstandingPacketsToConsumer", - currentState.providerState.outstandingPacketsToConsumer.set(receiver, newOutstandingPackets) - ) - val newState = currentState.with( - "providerState", newProviderState - ) - newState - } - - // Returns a ProtocolState where the current validator set on the provider is set to - // newValidatorSet. - pure def setProviderValidatorSet(currentState: ProtocolState, newValidatorSet: ValidatorSet): ProtocolState = { - pure val newChainState = currentState.providerState.chainState.with( - "currentValidatorSet", newValidatorSet - ) - currentState.with( - "providerState", - currentState.providerState.with( - "chainState", newChainState - ) - ) - } - - // Returns true if the given chain is currently a running consumer, false otherwise. - pure def isRunningConsumer(chain: Chain, providerState: ProviderState): bool = { - val status = providerState.consumerStatus.get(chain) - status == RUNNING - } - - // Returns the set of all consumer chains that currently have the status RUNNING. - pure def getRunningConsumers(providerState: ProviderState): Set[Chain] = { - providerState.consumerStatus.keys().filter( - chain => providerState.consumerStatus.get(chain) == RUNNING - ) - } - - // Returns the set of all consumer chains that currently have the status NOT_CONSUMER. - pure def getNonConsumers(providerState: ProviderState): Set[Chain] = { - providerState.consumerStatus.keys().filter( - chain => providerState.consumerStatus.get(chain) == NOT_CONSUMER - ) - } + pure val newProviderState = tmpStateAfterKeyAssignmentReplacement.providerState.with( + "validatorToConsumerAddr", newvalidatorToConsumerAddr + ).with( + "consumerAddrToValidator", newconsumerAddrToValidator + ) - // Returns whether the consumer has timed out due to the VscTimeout, and an error message. - // If the second return is not equal to "", the first return should be ignored. - // If it is equal to "", the first return will be true if the consumer has timed out and should be dropped, - // or false otherwise. - pure def TimeoutDueToVscTimeout(currentState: ProtocolState, consumer: Chain): (bool, str) = - // check for errors: the consumer is not running - if (not(isRunningConsumer(consumer, currentState.providerState))) { - (false, "Consumer is not currently a consumer - must have 'running' status!") - } else { - val providerState = currentState.providerState - val consumerState: ConsumerState = currentState.consumerStates.get(consumer) - - // has a packet been sent on the provider more than VscTimeout ago, but we have not received an answer since then? - val sentVscPacketsToConsumer = providerState.sentVscPacketsToConsumer.get(consumer) - if(sentVscPacketsToConsumer.length() > 0) { - val oldestSentVscPacket = sentVscPacketsToConsumer.head() // if length is 0, this is undefined, but we check for this before we use it - if(oldestSentVscPacket.sendingTime + VscTimeout < providerState.chainState.runningTimestamp) { - (true, "") - } else { - // no timeout yet, it has not been VscTimeout since that packet was sent - (false, "") - } - } else { - // no packet has been sent yet, so no timeout - (false, "") + Ok( + tmpStateAfterKeyAssignmentReplacement.with( + "providerState", newProviderState + ) + ) } } + } // =================== // ASSUMPTIONS ON MODEL PARAMETERS diff --git a/tests/mbt/model/ccv_boundeddrift.qnt b/tests/mbt/model/ccv_boundeddrift.qnt index 21a53074c0..24db1d3eaf 100644 --- a/tests/mbt/model/ccv_boundeddrift.qnt +++ b/tests/mbt/model/ccv_boundeddrift.qnt @@ -1,6 +1,7 @@ module ccv_boundeddrift { import ccv_model.* from "ccv_model" import ccv_types as Ccvt from "ccv" + import ccv_utils.* from "ccv_utils" import ccv from "ccv" import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" @@ -32,7 +33,7 @@ module ccv_boundeddrift { // Given the name of a chain, gets a set with the chain states of all other chains. def GetOtherChainStates(advancingChain: Ccvt::Chain): Set[Ccvt::ChainState] = - val runCons = ccv::getRunningConsumers(currentState.providerState) + val runCons = getRunningConsumers(currentState.providerState) if (advancingChain == Ccvt::PROVIDER_CHAIN) { runCons.map(c => currentState.consumerStates.get(c).chainState) } else { @@ -48,7 +49,7 @@ module ccv_boundeddrift { } def GetRunningChainStates(): Set[Ccvt::ChainState] = - val runCons = ccv::getRunningConsumers(currentState.providerState) + val runCons = getRunningConsumers(currentState.providerState) val consumerChainStates = runCons.map(c => currentState.consumerStates.get(c).chainState) consumerChainStates.union(Set(currentState.providerState.chainState)) @@ -80,13 +81,18 @@ module ccv_boundeddrift { val consumerStatus = currentState.providerState.consumerStatus nondet consumersToStart = oneOf(nonConsumers.powerset()) // make it so we stop consumers only with small likelihood: - nondet stopConsumers = oneOf(1.to(100)) - nondet consumersToStop = if (stopConsumers <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set() + nondet stopConsumersRand = oneOf(1.to(100)) + nondet consumersToStop = if (stopConsumersRand <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set() nondet timeAdvancement = oneOf(possibleAdvancements) EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), } } + action stepBoundedDriftKeyAssignment = any { + stepBoundedDrift, + nondetKeyAssignment, + } + // INVARIANT // The maxDrift between chains is never exceeded. // This *should* be ensured by the step function. diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt index fba4ddea6c..eb4e266184 100644 --- a/tests/mbt/model/ccv_model.qnt +++ b/tests/mbt/model/ccv_model.qnt @@ -4,6 +4,7 @@ module ccv_model { import ccv_types.* from "./ccv" import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" + import ccv_utils.* from "./ccv_utils" pure val consumerChainList = List("consumer1", "consumer2", "consumer3") pure val consumerChains = consumerChainList.toSet() @@ -14,6 +15,8 @@ module ccv_model { pure val ccvTimeouts = chains.mapBy(chain => 3 * Week) pure val nodes = Set("node1", "node2", "node3", "node4", "node5", "node6", "node7", "node8", "node9", "node10") + // possible consumer addresses that nodes can assign their key to + pure val consumerAddresses = Set("consAddr1", "consAddr2", "consAddr3", "consAddr4", "consAddr5", "consAddr6", "consAddr7", "consAddr8", "consAddr9", "consAddr10") pure val InitialValidatorSet = nodes.mapBy(node => 100) import ccv( @@ -31,6 +34,7 @@ module ccv_model { TrustingPeriodPerChain: Chain -> Time, ConsumerChains: Set[Chain], Nodes: Set[Node], + ConsumerAddresses: Set[ConsumerAddr], InitialValidatorSet: Node -> int, } @@ -56,6 +60,7 @@ module ccv_model { consumersToStop: Set[Chain], validator: Node, changeAmount: int, + consumerAddr: ConsumerAddr, } @@ -70,7 +75,7 @@ module ccv_model { // otherwise connections will break down. pure val timeAdvancements = Set(1 * Second, 1 * Day, 1 * Week - 1 * Hour) - pure def emptyAction = + pure def emptyAction: Action = { kind: "", consumerChain: "", @@ -79,6 +84,7 @@ module ccv_model { consumersToStop: Set(), validator: "", changeAmount: 0, + consumerAddr: "", } @@ -106,6 +112,8 @@ module ccv_model { ).with( "currentValidatorSet", InitialValidatorSet ) + ).with( + "keyAssignedValSetHistory", ConsumerChains.mapBy(chain => List(InitialValidatorSet)) ) currentState' = { providerState: providerStateWithConsumers, @@ -120,6 +128,7 @@ module ccv_model { Nodes: nodes, InitialValidatorSet: InitialValidatorSet, TrustingPeriodPerChain: TrustingPeriodPerChain, + ConsumerAddresses: consumerAddresses, } } @@ -179,6 +188,7 @@ module ccv_model { params' = params, } + // stepCommon is the core functionality of steps that does not have anything to do with time. action stepCommon = any { nondet node = oneOf(nodes) @@ -229,6 +239,17 @@ module ccv_model { // UTILITY FUNCTIONS // ================== + pure def removeZeroPowers(valSet: ValidatorSet): ValidatorSet = + valSet.keys().fold( + Map(), + (acc, node) => + if (valSet.get(node) == 0) { + acc + } else { + acc.put(node, valSet.get(node)) + } + ) + pure def oldest(packets: Set[VscPacket]): VscPacket = val newestPossiblePacket: VscPacket = { id: 0, @@ -290,9 +311,11 @@ module ccv_model { // Every validator set on any consumer chain MUST either be or have been // a validator set on the provider chain. val ValidatorSetHasExistedInv = - runningConsumers.forall(chain => + runningConsumers.forall(chain => // for all running consumers currentState.consumerStates.get(chain).chainState.votingPowerHistory.toSet().forall( + // go through all its historical and current validator sets validatorSet => providerValidatorHistory.toSet().contains(validatorSet) + // and check that they are also historical or current validator sets on the provider ) ) @@ -310,10 +333,6 @@ module ccv_model { consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists( packet => packet.validatorSet == providerValSetInCurBlock ) - // or the consumer was just started, which we detect by the consumer having a timestamp of 0 - // and the consumer having the validator set that was just sent in the block - or - (currentState.consumerStates.get(consumer).chainState.lastTimestamp == 0 and currentState.consumerStates.get(consumer).chainState.currentValidatorSet == providerValSetInCurBlock) ) // Every consumer chain receives the same sequence of @@ -360,8 +379,11 @@ module ccv_model { val lastTimeAdvancement = trace[trace.length()-1].timeAdvancement val lastBlockTime = currentState.consumerStates.get(ConsumerWithPotentialMaturations).chainState.lastTimestamp - lastTimeAdvancement val MatureOnTimeInv = + // if a consumer ended a block MaturationPrecondition implies + // then all matured packets need to have been processed and removed from the packets + // waiting to mature currentState.consumerStates.get(ConsumerWithPotentialMaturations).maturationTimes.toSet().forall( pair => val maturationTime = pair._2 @@ -378,7 +400,7 @@ module ccv_model { val EventuallyMatureOnProviderInv = runningConsumers.forall( consumer => { - val sentPackets = currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet() + val sentPackets = currentState.providerState.sentVscPacketsToConsumer.getOrElse(consumer, List()).toSet() sentPackets.forall( packet => // consumer still has time to respond @@ -390,6 +412,7 @@ module ccv_model { } ) + // ================= // SANITY CHECKS // ================= @@ -421,7 +444,7 @@ module ccv_model { val CanSendVscPackets = not(ConsumerChains.exists( consumer => - currentState.providerState.outstandingPacketsToConsumer.get(consumer).length() > 0 + currentState.providerState.outstandingPacketsToConsumer.getOrElse(consumer, List()).length() > 0 )) val CanReceiveVscPackets = @@ -489,7 +512,7 @@ module ccv_model { // consumer1 was started assert(currentState.providerState.consumerStatus.get("consumer1") == RUNNING), // but no packet was sent to consumer 1 - assert(currentState.providerState.outstandingPacketsToConsumer.get("consumer1").length() == 0), + assert(currentState.providerState.outstandingPacketsToConsumer.getOrElse("consumer1", List()).length() == 0), // the validator set on the provider was entered into the history assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet.put("node1", 150), InitialValidatorSet)), // change voting power on provider again @@ -632,4 +655,270 @@ module ccv_model { VotingPowerChange("node1", 50) // action needs to be there but does not matter what it is } ) + + + // ===== KEY ASSIGNMENT ======= + action stepKeyAssignment = + any { + step, + nondetKeyAssignment, + } + + action nondetKeyAssignment = + all { + runningConsumers.size() > 0, + nondet node = oneOf(nodes) + nondet consumerAddr = oneOf(consumerAddresses) + nondet consumer = oneOf(runningConsumers) + KeyAssignment(consumer, node, consumerAddr), + } + + action KeyAssignment( + chain: Chain, + validator: Node, + consumerAddr: ConsumerAddr + ): bool = + val result = assignConsumerKey(currentState, chain, validator, consumerAddr) + all { + hasError(result) == false, + currentState' = result.newState, + trace' = trace.append( + {...emptyAction, + kind: "KeyAssignment", + consumerChain: chain, + validator: validator, + consumerAddr: consumerAddr + } + ), + params' = params, + } + + // invariants for key assignment - some invariants are in addition, some need to be adjusted from the original model + + // Every validator set on any consumer chain MUST either be or have been + // a validator set on the provider chain, under the key assignment at the time. + val providerKeyAssignedValSetHistory = currentState.providerState.keyAssignedValSetHistory + + val ValidatorSetHasExistedKeyAssignmentInv = + runningConsumers.forall(chain => // for every running consumer + currentState.consumerStates.get(chain).chainState.votingPowerHistory.toSet().forall( + // for every validator set the consumer ever had + validatorSet => providerKeyAssignedValSetHistory.getOrElse(chain, List()).toSet().exists( + // that validator set needs to also have existed on the provider + provValSet => removeZeroPowers(provValSet) == removeZeroPowers(validatorSet) + ) + ) + ) + + // Any update in the power of a validator on the provider + // MUST be present in a ValidatorSetChangePacket that is sent to all registered consumer chains, + // and the key assignment of each validator should be applied in that VSCPacket. + val ValidatorUpdatesArePropagatedKeyAssignmentInv = + // when the provider has just entered a validator set into a block... + ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock + implies + val providerValSetInCurBlock = providerValidatorHistory.head() + // ... for each consumer that is running then ... + runningConsumers.forall( + // ...the validator set under key assignment is in a sent packet... + val providerState = currentState.providerState + consumer => providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists( + packet => + packet.validatorSet == + applyKeyAssignmentToValSet(providerState, consumer, providerValSetInCurBlock) + ) + ) + + // Every consumer chain receives the same sequence of + // ValidatorSetChangePackets in the same order. + // NOTE: since not all consumer chains are running all the time, + // we need a slightly weaker invariant: + // For consumer chains c1, c2, if both c1 and c2 received a packet p1 sent at t1 and a packet p2 sent at t2, + // then both have received ALL packets that were sent between t1 and t2. + val SameVscPacketsKeyAssignmentInv = + runningConsumers.forall( + consumer1 => runningConsumers.forall( + consumer2 => { + val packets1 = currentState.consumerStates.get(consumer1).receivedVscPackets + val packets2 = currentState.consumerStates.get(consumer2).receivedVscPackets + val commonPackets = packets1.toSet().intersect(packets2.toSet()) + if (commonPackets.size() == 0) { + true // they don't share any packets, so nothing to check + } else { + val newestCommonPacket = newest(commonPackets) + val oldestCommonPacket = oldest(commonPackets) + // get all packets sent between the oldest and newest common packet + val packetsBetween1 = packets1.select( + packet => packet.sendingTime >= oldestCommonPacket.sendingTime and packet.sendingTime <= newestCommonPacket.sendingTime + ) + val packetsBetween2 = packets2.select( + packet => packet.sendingTime >= oldestCommonPacket.sendingTime and packet.sendingTime <= newestCommonPacket.sendingTime + ) + + // revert key assignments + val packetsBetween1noKeyAssignment = packetsBetween1.foldl( + List(), + (acc, packet) => + acc.concat(List({...packet, + validatorSet: revertKeyAssignment( + currentState.providerState.keyAssignmentsForVSCPackets + .getOrElse(packet.id, Map()) + .getOrElse(consumer1, Map()), + packet.validatorSet) + })) + ) + + val packetsBetween2noKeyAssignment = packetsBetween2.foldl( + List(), (acc, packet) => + acc.concat(List({...packet, + validatorSet: revertKeyAssignment( + currentState.providerState.keyAssignmentsForVSCPackets + .getOrElse(packet.id, Map()) + .getOrElse(consumer2, Map()), + packet.validatorSet) + })) + ) + // check that the packets between the common packets are equal + // when key assignment is reversed + packetsBetween1noKeyAssignment == packetsBetween2noKeyAssignment + } + } + ) + ) + + + // Rules for key assignment: + val KeyAssignmentRulesInv = + NoProviderReuse and NoDuplicationOnSameConsumer + + // validator A cannot assign consumer key K to consumer chain X if there is already a validator B (B!=A) using K on the provider + val NoProviderReuse = + consumerChains.forall( + consumer => + val valConsPk = currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) + valConsPk.keys().forall( + node => + val consAddr = valConsPk.get(node) + // either the key is the nodes key itself (B == A) + consAddr == node or + // or the consAddr must not be a validator on the provider + not(currentState.providerState.chainState.currentValidatorSet.keys().contains(consAddr)) + ) + ) + + // validator A cannot assign consumer key K to consumer chain X if there is already a validator B using K on X + val NoDuplicationOnSameConsumer = + consumerChains.forall( + consumer => + val valConsPk = currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) + valConsPk.keys().forall( + node => + val consAddr = valConsPk.get(node) + // no other node may use consAddr + not(valConsPk.keys().exists( + otherNode => otherNode != node and valConsPk.get(otherNode) == consAddr + )) + ) + ) + + // sanity checks + val CanAssignConsumerKey = + not(consumerChains.exists( + consumer => + currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()).keys().size() > 0 + )) + + val CanHaveConsumerAddresses = + not(consumerChains.exists( + consumer => + currentState.consumerStates.get(consumer).chainState.currentValidatorSet.keys().exists( + addr => addr.in(consumerAddresses) + ) + )) + + // == tests for key assignment == + run KeyAssignmentTest = + init + .then( + // start all consumer chains + EndAndBeginBlockForProvider(1 * Second, consumerChains, Set()) + ) + .then( + // node 1 assigns a key on consumer1 + KeyAssignment("consumer1", "node1", "consAddr1") + ) + .then( + // end and begin block to make sure the key assignment is processed and the packet is sent + EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + ) + .then( + // receive the packet on the consumer + DeliverVscPacket("consumer1") + ) + .then( + // end and begin block to make sure the packet is processed + EndAndBeginBlockForConsumer("consumer1", 1 * Second) + ) + .then( + all { + // the key should be present in the valset on the consumer, and the node itself should not + assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet.getOrElse("node1", 0) == 0), + assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet.get("consAddr1") == 100), + // try some key assignments that should fail/succeed without comitting to state + val res = assignConsumerKey(currentState, "consumer1", "node1", "consAddr1") + // fail - key already assigned (even if it is the same node) + assert(hasError(res)), + val res2 = assignConsumerKey(currentState, "consumer1", "node2", "consAddr1") + // fail - key assigned to other node + assert(hasError(res2)), + val res3 = assignConsumerKey(currentState, "consumer2", "node2", "consAddr1") + // ok - may reuse the key on a different consumer + assert(not(hasError(res3))), + val res4 = assignConsumerKey(currentState, "consumer1", "node2", "node1") + // fail - may not reuse a provider key of a different val + assert(hasError(res4)), + val res5 = assignConsumerKey(currentState, "consumer1", "node1", "consAddr2") + // ok - assigning unused key to node + assert(not(hasError(res5))), + val res6 = assignConsumerKey(currentState, "consumer1", "node1", "node1") + // ok - going back to original key + assert(not(hasError(res6))), + // mature the vsc packet on the consumer + EndAndBeginBlockForConsumer("consumer1", unbondingPeriods.get("consumer1") + 1 * Hour) + } + ) + .then( + // End a block to send the maturation + EndAndBeginBlockForConsumer("consumer1", 1 * Second) + ) + .then( + // deliver the vsc matured packet to the provider + DeliverVscMaturedPacket("consumer1") + ) + .then( + // the old key should have been pruned + all { + // check that pruning has been performed nicely + assert(currentState.providerState.consumerAddrToValidator.get("consumer1").get("consAddr1") == "node1"), + assert(currentState.providerState.consumerAddrsToPrune.get("consumer1").getOrElse(0, List()).length() == 0), + // action does not matter + VotingPowerChange("node1", 50) + } + ) + + run KeyAssignmentInvTest = + init.then( + KeyAssignment("consumer3", "node3", "consAddr6") + ).then( + VotingPowerChange("node1", 50) + ) + .then( + EndAndBeginBlockForProvider(1 * Second, Set("consumer1", "consumer2"), Set()) + ).then( + all { + ValidatorSetHasExistedKeyAssignmentInv, + // action doesn't matter + VotingPowerChange("node1", 50) + } + ) } \ No newline at end of file diff --git a/tests/mbt/model/ccv_test.qnt b/tests/mbt/model/ccv_test.qnt index 4dae28ec03..62ab03b5e0 100644 --- a/tests/mbt/model/ccv_test.qnt +++ b/tests/mbt/model/ccv_test.qnt @@ -5,6 +5,7 @@ module ccv_test { import ccv_types.* from "./ccv" import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" + import ccv_utils.* from "./ccv_utils" pure val consumerChains = Set("sender", "receiver") pure val chains = consumerChains.union(Set(PROVIDER_CHAIN)) diff --git a/tests/mbt/model/ccv_utils.qnt b/tests/mbt/model/ccv_utils.qnt new file mode 100644 index 0000000000..4d881828ef --- /dev/null +++ b/tests/mbt/model/ccv_utils.qnt @@ -0,0 +1,456 @@ +// This file contains utility functions for ccv.qnt +// that are not part of the API/core logic of ccv, but still relevant +// for the functional logic of the protocol. +module ccv_utils { + import ccv_types.* from "./ccv" + import extraSpells.* from "./libraries/extraSpells" + import Time.* from "./libraries/Time" + + + // Takes the current provider state and validator set and returns + // the validator set under the current key assignments for the given consumer, as stored in the provider state. + pure def applyKeyAssignmentToValSet( + providerState: ProviderState, + consumer: Chain, + valSet: ValidatorSet + ): ValidatorSet = { + // map each validator to a tuple of (consumer address, voting power) + valSet.keys().map( + (node) => + pure val power = valSet.get(node) + // check if the validator has a key assigned + pure val validatorToConsumerAddr = providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) + if (validatorToConsumerAddr.keys().contains(node)) { + // the validator has a key assigned + pure val consAddr = validatorToConsumerAddr.get(node) + (consAddr, power) + } else { + // the validator has no key assigned + // use the default key + (node, power) + } + ).fold( // fold the (addr,pow) tuples into a map addr -> pow + Map(), + (acc, pair) => acc.put(pair._1, pair._2) + ) + } + + // Takes a validator set, to which a key assignment has been applied, and reverts it, + // i.e. returns the original validator set. + // This also filters out validators that are assigned 0 power. + pure def revertKeyAssignment( + keyAssignment: Node -> ConsumerAddr, + valSetWithAssignment: ValidatorSet + ): ValidatorSet = { + // get an assignment from consumer addr to nodes + pure val reverseAssignment = keyAssignment.keys().map( + (consAddr) => + (keyAssignment.get(consAddr), consAddr) + ).fold( + Map(), + (acc, pair) => acc.put(pair._1, pair._2) + ) + + // for each node in the valset, reverse its key assignment + valSetWithAssignment.keys().map( + (addr) => + pure val power = valSetWithAssignment.get(addr) + // if the addr has a key assigned, use that. otherwise, the addr doesn't have a key assigned, + // and therefore *is* the key that should be used. + pure val consAddr = reverseAssignment.getOrElse(addr, addr) + (consAddr, power) + ).filter( + pair => pair._2 > 0 + ).fold( + Map(), + (acc, pair) => acc.put(pair._1, pair._2) + ) + } + + // Appends the key assignment for the given oldConsAddr on the consumer by a validator + // to be pruned when a VscMaturedPacket for the current runningVscId is received from the consumer. + pure def AppendConsumerAddrToPrune(currentState: ProtocolState, oldConsAddr: ConsumerAddr, consumer: Chain): ProtocolState = { + pure val vscId = currentState.providerState.runningVscId + pure val consumerAddrsToPrune = currentState.providerState.consumerAddrsToPrune.getOrElse(consumer, Map()) + pure val prevConsAddrs = consumerAddrsToPrune.getOrElse(oldConsAddr, Map()).getOrElse(vscId, []) + + pure val newConsAddrsToPrune = consumerAddrsToPrune.put(vscId, prevConsAddrs.append(oldConsAddr)) + + currentState.with( + "providerState", + currentState.providerState.with( + "consumerAddrsToPrune", + currentState.providerState.consumerAddrsToPrune.put(consumer, newConsAddrsToPrune) + ) + ) + } + + // Returns the new ConsumerStatusMap according to the consumers to stop + // and the consumers to time out. + // If a consumer is both stopped and timed out, it will be timed out. + // The second return is an error string: If it is not equal to "", + // it contains an error message, and the first return should be ignored. + pure def stopConsumers( + currentConsumerStatusMap: Chain -> str, + consumersToStop: Set[Chain], + consumersToTimeout: Set[Chain]): (Chain -> str, str) = { + val runningConsumers = currentConsumerStatusMap.keys().filter( + chain => currentConsumerStatusMap.get(chain) == RUNNING + ) + // all consumers to stop must be running right now, else we have an error + if (consumersToStop.exclude(runningConsumers).size() > 0) { + (currentConsumerStatusMap, "Cannot stop a consumer that is not running") + } else { + val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( + (chain) => + if (consumersToTimeout.contains(chain)) { + TIMEDOUT + } else if (consumersToStop.contains(chain)) { + STOPPED + } else { + currentConsumerStatusMap.get(chain) + } + ) + (newConsumerStatusMap, "") + } + } + + // Returns the new ConsumerStatusMap according to the consumers to start. + // The second return is an error string: If it is not equal to "", + // it contains an error message, and the first return should be ignored. + pure def startConsumers( + currentConsumerStatusMap: Chain -> str, + consumersToStart: Set[Chain]): (Chain -> str, str) = { + val nonConsumers = currentConsumerStatusMap.keys().filter( + chain => currentConsumerStatusMap.get(chain) == NOT_CONSUMER + ) + // all consumers to start must be nonConsumers right now, otherwise we have an error + if (consumersToStart.exclude(nonConsumers).size() > 0) { + (currentConsumerStatusMap, "cannot start a consumer that is stopped or already a consumer") + } else { + val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( + (chain) => + if (consumersToStart.contains(chain)) { + RUNNING + } else { + currentConsumerStatusMap.get(chain) + } + ) + (newConsumerStatusMap, "") + } + } + + pure def StartStopConsumers( + currentConsumerStatusMap: Chain -> str, + consumersToStart: Set[Chain], + consumersToStop: Set[Chain], + consumersToTimeout: Set[Chain] + ): (Chain -> str, str) = { + // check if any consumer is both started and stopped + if (consumersToStart.intersect(consumersToStop).size() > 0) { + (currentConsumerStatusMap, "Cannot start and stop a consumer at the same time") + } else { + val res1 = currentConsumerStatusMap.startConsumers(consumersToStart) + val newConsumerStatus = res1._1 + val err1 = res1._2 + val res2 = newConsumerStatus.stopConsumers(consumersToStop, consumersToTimeout) + val err2 = res2._2 + if (err1 != "") { + (currentConsumerStatusMap, err1) + } else if (err2 != "") { + (currentConsumerStatusMap, err2) + } else { + (res2._1, "") + } + } + } + + + // Takes the currentValidatorSet and puts it as the newest set of the voting history + pure def enterCurValSetIntoBlock(chainState: ChainState): ChainState = { + chainState.with( + "votingPowerHistory", chainState.votingPowerHistory.prepend( + chainState.currentValidatorSet + ) + ) + } + + // Advances the timestamp in the chainState by timeAdvancement + pure def advanceTime(chainState: ChainState, timeAdvancement: Time): ChainState = + { + ...chainState, + lastTimestamp: chainState.runningTimestamp, + runningTimestamp: chainState.runningTimestamp + timeAdvancement, + } + + // common logic to update the chain state, used by both provider and consumers. + pure def endAndBeginBlockShared(chainState: ChainState, timeAdvancement: Time): ChainState = { + chainState.enterCurValSetIntoBlock().advanceTime(timeAdvancement) + } + + // returns the providerState with the following modifications: + // * sends VscPackets to all running consumers, using the provided timestamp as sending time + // * increments the runningVscId + // This should only be called when the provider chain is ending a block. + // If no vsc packets need to be sent, this will be a noop. + // the ccv timeout should be the ccv timeout for the provider chain. + pure def sendVscPackets( + providerState: ProviderState, + sendingTimestamp: Time, + ccvTimeout: Time): ProviderState = { + val newSentPacketsPerConsumer = providerState.getConsumers().mapBy( // compute, for each consumer, a list of new packets to be sent + (consumer) => + // if validator set changed or the key assignments for this chain changed, and the consumer is running, send a packet + if ((providerState.providerValidatorSetChangedInThisBlock or + providerState.consumersWithAddrAssignmentChangesInThisBlock.contains(consumer)) + and + isRunningConsumer(consumer, providerState)) { + // send a packet, i.e. use a list with one element (the packet to be sent) + List({ + id: providerState.runningVscId, + // apply key assignment to the current validator set + validatorSet: providerState.applyKeyAssignmentToValSet( + consumer, + providerState.chainState.currentValidatorSet + ), + sendingTime: sendingTimestamp, + timeoutTime: sendingTimestamp + ccvTimeout + }) + } else { + // no packet to be sent, so empty list + List() + } + ) + val newOutstandingPacketsToConsumer = providerState.getConsumers().mapBy( + (consumer) => + providerState.outstandingPacketsToConsumer.getOrElse(consumer, List()).concat( + newSentPacketsPerConsumer.get(consumer) + ) + ) + val newSentVscPackets = providerState.getConsumers().mapBy( + (consumer) => + providerState.sentVscPacketsToConsumer.getOrElse(consumer, List()).concat( + newSentPacketsPerConsumer.get(consumer) + ) + ) + { + ...providerState, + outstandingPacketsToConsumer: newOutstandingPacketsToConsumer, + sentVscPacketsToConsumer: newSentVscPackets, + runningVscId: providerState.runningVscId + 1, + // we ended the block and processed that the valset or key assignments changed, + // so reset the flags + providerValidatorSetChangedInThisBlock: false, + consumersWithAddrAssignmentChangesInThisBlock: Set(), + // remember the key assignments that were applied to send the packets + keyAssignmentsForVSCPackets: providerState.keyAssignmentsForVSCPackets.put( + providerState.runningVscId, + providerState.validatorToConsumerAddr + ) + } + } + + // receives a given packet (sent by the provider) on the consumer. The arguments are the consumer chain that is receiving the packet, and the packet itself, + // as well as the unbonding period for the consumer chain. + // To receive a packet, modify the running validator set (not the one entered into the block yet, + // but the candidate that would be put into the block if it ended now) + // and store the maturation time for the packet. + pure def recvPacketOnConsumer( + currentState: ProtocolState, + receiver: Chain, + packet: VscPacket, + receiverUnbondingPeriod: Time): Result = { + if(not(isRunningConsumer(receiver, currentState.providerState))) { + Err("Receiver is not currently a consumer - must have 'running' status!") + } else { + // update the running validator set, but not the history yet, + // as that only happens when the next block is started + val currentConsumerState: ConsumerState = currentState.consumerStates.get(receiver) + val newConsumerState: ConsumerState = + { + ...currentConsumerState, + chainState: currentConsumerState.chainState.with( + "currentValidatorSet", packet.validatorSet + ), + maturationTimes: currentConsumerState.maturationTimes.append( + ( + packet, + currentConsumerState.chainState.runningTimestamp + receiverUnbondingPeriod + ) + ), + receivedVscPackets: currentConsumerState.receivedVscPackets.prepend(packet) + } + val newConsumerStates = currentState.consumerStates.set(receiver, newConsumerState) + val newState = currentState.with( + "consumerStates", newConsumerStates + ) + Ok(newState) + } + } + + // receives a given packet on the provider. The arguments are the consumer chain that sent the packet, and the packet itself. + // To receive a packet, add it to the list of received maturations. + pure def recvPacketOnProvider(currentState: ProtocolState, sender: Chain, packet: VscMaturedPacket): Result = { + if (not(isRunningConsumer(sender, currentState.providerState))) { + Err("Sender is not currently a consumer - must have 'running' status!") + } else if (currentState.providerState.sentVscPacketsToConsumer.get(sender).head().id != packet.id) { + // the packet is not the oldest sentVscPacket, something went wrong + Err("Received maturation is not for the oldest sentVscPacket") + } else { + val currentReceivedMaturations = currentState.providerState.receivedMaturations + val newReceivedMaturations = currentReceivedMaturations.union(Set(packet)) + val newProviderState = currentState.providerState.with( + "receivedMaturations", newReceivedMaturations + ) + // prune the sentVscPacket + val newSentVscPacket = currentState.providerState.sentVscPacketsToConsumer.get(sender).tail() + val newState = currentState.with( + "providerState", + {...newProviderState, + sentVscPacketsToConsumer: currentState.providerState.sentVscPacketsToConsumer.set(sender, newSentVscPacket) + } + ) + + // prune assigned keys that are no longer needed + + // get the keys that should be pruned + pure val consumerAddrsToPrune = + currentState.providerState.consumerAddrsToPrune + .getOrElse(sender, Map()) + .getOrElse(packet.id, List()).toSet() + + // actually do the pruning + pure val senderValByConsAddr = + // for the sender chain, get the consAddrToValidator mapping + newState.providerState.consumerAddrToValidator.getOrElse(sender, Map()) + pure val newSenderValByConsAddr = + senderValByConsAddr.keys().filter( + // filter out the assigned keys that should be pruned + consAddr => not(consumerAddrsToPrune.contains(consAddr)) + ).mapBy( + // rebuild the map with the pruned keys removed + consAddr => senderValByConsAddr.get(consAddr) + ) + + // update the provider state + pure val newProviderState2 = newState.providerState.with( + // update the consumerAddrToValidator map to remove the pruned keys + "consumerAddrToValidator", + newState.providerState.consumerAddrToValidator.put(sender, newSenderValByConsAddr) + ).with( + // delete the consumer addresses to prune, since they are pruned now + "consumerAddrsToPrune", + newState.providerState.consumerAddrsToPrune.put( + sender, + newState.providerState.consumerAddrsToPrune.getOrElse(sender, Map()).put( + packet.id, + List() + ) + ) + ) + + // update the state + pure val newState2 = newState.with( + "providerState", newProviderState2 + ) + + Ok(newState2) + } + } + + // removes the oldest outstanding packet from the consumer. on-chain, this would happen when the packet is acknowledged. + // only the oldest packet can be removed, since we model ordered channels. + pure def removeOutstandingPacketFromConsumer(currentState: ProtocolState, sender: Chain): ProtocolState = { + val currentOutstandingPackets = currentState.consumerStates.get(sender).outstandingPacketsToProvider + val newOutstandingPackets = currentOutstandingPackets.tail() + val newConsumerState = currentState.consumerStates.get(sender).with( + "outstandingPacketsToProvider", newOutstandingPackets + ) + val newConsumerStates = currentState.consumerStates.set(sender, newConsumerState) + val newState = currentState.with( + "consumerStates", newConsumerStates + ) + newState + } + + // removes the oldest outstanding packet (to the given consumer) from the provider. + // on-chain, this would happen when the packet is acknowledged. + // only the oldest packet can be removed, since we model ordered channels. + pure def removeOutstandingPacketFromProvider(currentState: ProtocolState, receiver: Chain): ProtocolState = { + val currentOutstandingPackets = currentState.providerState.outstandingPacketsToConsumer.get(receiver) + val newOutstandingPackets = currentOutstandingPackets.tail() + val newProviderState = currentState.providerState.with( + "outstandingPacketsToConsumer", + currentState.providerState.outstandingPacketsToConsumer.set(receiver, newOutstandingPackets) + ) + val newState = currentState.with( + "providerState", newProviderState + ) + newState + } + + // Returns a ProtocolState where the current validator set on the provider is set to + // newValidatorSet. + pure def setProviderValidatorSet(currentState: ProtocolState, newValidatorSet: ValidatorSet): ProtocolState = { + pure val newChainState = currentState.providerState.chainState.with( + "currentValidatorSet", newValidatorSet + ) + currentState.with( + "providerState", + currentState.providerState.with( + "chainState", newChainState + ) + ) + } + + // Returns true if the given chain is currently a running consumer, false otherwise. + pure def isRunningConsumer(chain: Chain, providerState: ProviderState): bool = { + val status = providerState.consumerStatus.get(chain) + status == RUNNING + } + + // Returns the set of all consumer chains. + pure def getConsumers(providerState: ProviderState): Set[Chain] = providerState.consumerStatus.keys() + + // Returns the set of all consumer chains that currently have the status RUNNING. + pure def getRunningConsumers(providerState: ProviderState): Set[Chain] = { + providerState.consumerStatus.keys().filter( + chain => providerState.consumerStatus.get(chain) == RUNNING + ) + } + + // Returns the set of all consumer chains that currently have the status NOT_CONSUMER. + pure def getNonConsumers(providerState: ProviderState): Set[Chain] = { + providerState.consumerStatus.keys().filter( + chain => providerState.consumerStatus.get(chain) == NOT_CONSUMER + ) + } + + // Returns whether the consumer has timed out due to the vscTimeout, and an error message. + // If the second return is not equal to "", the first return should be ignored. + // If it is equal to "", the first return will be true if the consumer has timed out and should be dropped, + // or false otherwise. + pure def TimeoutDueToVscTimeout(currentState: ProtocolState, consumer: Chain, vscTimeout: Time): (bool, str) = + // check for errors: the consumer is not running + if (not(isRunningConsumer(consumer, currentState.providerState))) { + (false, "Consumer is not currently a consumer - must have 'running' status!") + } else { + val providerState = currentState.providerState + val consumerState: ConsumerState = currentState.consumerStates.get(consumer) + + // has a packet been sent on the provider more than vscTimeout ago, but we have not received an answer since then? + val sentVscPacketsToConsumer = providerState.sentVscPacketsToConsumer.getOrElse(consumer, List()) + if(sentVscPacketsToConsumer.length() > 0) { + val oldestSentVscPacket = sentVscPacketsToConsumer.head() // if length is 0, this is undefined, but we check for this before we use it + if(oldestSentVscPacket.sendingTime + vscTimeout < providerState.chainState.runningTimestamp) { + (true, "") + } else { + // no timeout yet, it has not been vscTimeout since that packet was sent + (false, "") + } + } else { + // no packet has been sent yet, so no timeout + (false, "") + } + } +} \ No newline at end of file diff --git a/tests/mbt/run_invariants.sh b/tests/mbt/run_invariants.sh index 613664aeae..df22b97702 100755 --- a/tests/mbt/run_invariants.sh +++ b/tests/mbt/run_invariants.sh @@ -2,4 +2,5 @@ quint test ccv_model.qnt quint test ccv_test.qnt -quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_model.qnt --max-steps 200 --max-samples 200 \ No newline at end of file +quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_model.qnt --max-steps 200 --max-samples 200 +quint run --invariant "all{ValidatorUpdatesArePropagatedKeyAssignmentInv,ValidatorSetHasExistedKeyAssignmentInv,SameVscPacketsKeyAssignmentInv,MatureOnTimeInv,EventuallyMatureOnProviderInv,KeyAssignmentRulesInv}" ccv_model.qnt --step stepKeyAssignment --max-steps 200 --max-samples 200 \ No newline at end of file