From a90e79db8520c8db2fa838ac64f4cffe9b591b72 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt <57488781+p-offtermatt@users.noreply.github.com> Date: Wed, 24 Jan 2024 11:19:03 +0100 Subject: [PATCH 1/8] Update tests/mbt/model/ccv.qnt Co-authored-by: insumity --- tests/mbt/model/ccv.qnt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index c46449be9d..a8ca3ad641 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -229,7 +229,7 @@ module ccv_types { pure val PROVIDER_CHAIN = "provider" // Takes the current provider state and validator set and returns - // the validator set under the current the key assignments for the given consumer, as stored in the provider state. + // 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, From dc62877da6c7f1227acf7b65a0f451cb9802a1e3 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt <57488781+p-offtermatt@users.noreply.github.com> Date: Wed, 24 Jan 2024 13:18:15 +0100 Subject: [PATCH 2/8] Update tests/mbt/model/ccv.qnt Co-authored-by: insumity --- tests/mbt/model/ccv.qnt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index a8ca3ad641..3ab37cb980 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -117,7 +117,7 @@ module ccv_types { //(old key to 0 power, new key to current power) keyAssignmentReplacements: Chain -> (Node -> (ConsumerAddr, Power)), - // Stores the mapping from VSC ids to consumer validators addresses. Needed for pruning ValidatorByConsumerAddr. + // Stores the mapping from VSC ids to consumer validators addresses. Needed for pruning validatorByConsumerAddr. consumerAddrsToPrune: Chain -> VscId -> List[ConsumerAddr], // For every sent VSCPacket, stores the key assignments that were applied to send it. From e7c220de980bed60007adb15545523a0fe5db98a Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Thu, 25 Jan 2024 15:22:22 +0100 Subject: [PATCH 3/8] Incorporate review comments --- tests/mbt/driver/mbt_test.go | 2 +- tests/mbt/model/README.md | 9 +++----- tests/mbt/model/ccv.qnt | 35 ++++++++++++++---------------- tests/mbt/model/ccv_model.qnt | 6 ++--- testutil/integration/validators.go | 6 ----- 5 files changed, 23 insertions(+), 35 deletions(-) diff --git a/tests/mbt/driver/mbt_test.go b/tests/mbt/driver/mbt_test.go index b9e691d9da..a55d870dda 100644 --- a/tests/mbt/driver/mbt_test.go +++ b/tests/mbt/driver/mbt_test.go @@ -124,7 +124,7 @@ func RunItfTrace(t *testing.T, path string) { // generate keys that can be assigned on consumers, according to the ConsumerAddresses in the trace consumerAddressesExpr := params["ConsumerAddresses"].Value.(itf.ListExprType) - consumerPrivVals, err := integration.CreateSigners(len(consumerAddressesExpr)) + _, _, consumerPrivVals, err := integration.CreateValidators(len(consumerAddressesExpr)) require.NoError(t, err, "Error creating consumer signers") consumerAddrNamesToPrivVals := make(map[string]cmttypes.PrivValidator, len(consumerAddressesExpr)) diff --git a/tests/mbt/model/README.md b/tests/mbt/model/README.md index 909f0c7e45..57f5b2eda9 100644 --- a/tests/mbt/model/README.md +++ b/tests/mbt/model/README.md @@ -31,6 +31,7 @@ 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 @@ -48,10 +49,6 @@ As an optional module, it can also include KeyAssignment. To run with key assignment, specify the step flag: `--step stepKeyAssignment`. -Key assignment allows an additional action: - -* `KeyAssignment(chain: Chain, validator: Node, consumerAddr: ConsumerAddr)`: 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. - KeyAssignment also needs some different invariants, see below. #### ccv_boundeddrift.qnt @@ -107,8 +104,8 @@ with a timestamp >= t + UnbondingPeriod on that consumer. 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: Replaces ValidatorSetHasExistedInv. Validator sets are checked for equality under key assignment when checking whether they have existed. -- [X] SameVscPacketsKeyAssignmentInv: Replaces SameVscPacketsInv. VscPackets are checked for equality under key assignment when ensuring consumers receive the same ones. +- [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 diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index 3ab37cb980..7fc6058b23 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -101,14 +101,15 @@ module ccv_types { runningVscId: int, // For every consumer chain, stores the consumer address assigned by each validator. - validatorConsumerPubKey: Chain -> (Node -> ConsumerAddr), + validatorConsumerAddr: Chain -> (Node -> ConsumerAddr), + + // For every consumer chain, holds the provider validator for each assigned consumer address. + validatorByConsumerAddr: Chain -> (ConsumerAddr -> Node), // 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, - // For every consumer chain, holds the provider validator for each assigned consumer key. - validatorByConsumerAddr: Chain -> (ConsumerAddr -> Node), // Stores the key assignments that need to be replaced in the current block. // Needed to apply the key assignments received in a block to the validator updates sent to the consumer chains. @@ -134,7 +135,7 @@ module ccv_types { providerValidatorSetChangedInThisBlock: false, consumerStatus: Map(), runningVscId: 0, - validatorConsumerPubKey: Map(), + validatorConsumerAddr: Map(), keyAssignedValSetHistory: Map(), validatorByConsumerAddr: Map(), keyAssignmentReplacements: Map(), @@ -250,15 +251,15 @@ module ccv_types { // set old key to 0 pure val oldToZero = (oldConsAddr, 0) // set new key to current power - pure val newToPower = (providerState.validatorConsumerPubKey.getOrElse(consumer, Map()).getOrElse(node, node), power) + pure val newToPower = (providerState.validatorConsumerAddr.getOrElse(consumer, Map()).getOrElse(node, node), power) Set(oldToZero, newToPower) } else { // no replacement // check if the validator has a key assigned - pure val validatorConsumerPubKey = providerState.validatorConsumerPubKey.getOrElse(consumer, Map()) - if (validatorConsumerPubKey.keys().contains(node)) { + pure val validatorConsumerAddr = providerState.validatorConsumerAddr.getOrElse(consumer, Map()) + if (validatorConsumerAddr.keys().contains(node)) { // the validator has a key assigned - pure val consAddr = validatorConsumerPubKey.get(node) + pure val consAddr = validatorConsumerAddr.get(node) Set((consAddr, power)) } else { // the validator has no key assigned @@ -526,12 +527,8 @@ module ccv { // run the shared core chainState logic val newChainState = currentProviderState.chainState.endAndBeginBlockShared(timeAdvancement) - val providerStateAfterTimeAdvancement = currentProviderState.with( - "chainState", newChainState - ).with( - "keyAssignedValSetHistory", newKeyAssignedValSetHistory - ) - + val providerStateAfterTimeAdvancement = + {...currentProviderState, chainState: newChainState, keyAssignedValSetHistory: newKeyAssignedValSetHistory} val tmpState = currentState.with( "providerState", providerStateAfterTimeAdvancement ) @@ -677,7 +674,7 @@ module ccv { // this key can be assigned // get the old assigned key - pure val consKeyByVal = currentState.providerState.validatorConsumerPubKey.getOrElse(consumer, Map()) + pure val consKeyByVal = currentState.providerState.validatorConsumerAddr.getOrElse(consumer, Map()) pure val p = if (consKeyByVal.keys().contains(providerNode)) { // providerNode had previously assigned a consumer key (consKeyByVal.get(providerNode), true) @@ -721,9 +718,9 @@ module ccv { ) ) - pure val newValidatorConsumerPubKey = currentState.providerState.validatorConsumerPubKey.put( + pure val newvalidatorConsumerAddr = currentState.providerState.validatorConsumerAddr.put( consumer, - currentState.providerState.validatorConsumerPubKey.getOrElse(consumer, Map()).put( + currentState.providerState.validatorConsumerAddr.getOrElse(consumer, Map()).put( providerNode, consumerAddr ) @@ -738,7 +735,7 @@ module ccv { ) pure val newProviderState = tmpStateAfterKeyAssignmentReplacement.providerState.with( - "validatorConsumerPubKey", newValidatorConsumerPubKey + "validatorConsumerAddr", newvalidatorConsumerAddr ).with( "validatorByConsumerAddr", newValidatorByConsumerAddr ) @@ -928,7 +925,7 @@ module ccv { // remember the key assignments that were applied to send the packets keyAssignmentsForVSCPackets: providerState.keyAssignmentsForVSCPackets.put( providerState.runningVscId, - providerState.validatorConsumerPubKey + providerState.validatorConsumerAddr ) } } diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt index 12eca0fa8c..a52a882528 100644 --- a/tests/mbt/model/ccv_model.qnt +++ b/tests/mbt/model/ccv_model.qnt @@ -238,7 +238,7 @@ module ccv_model { // UTILITY FUNCTIONS // ================== - pure def removeZeroPowers(valSet: Node -> int): Node -> int = + pure def removeZeroPowers(valSet: ValidatorSet): ValidatorSet = valSet.keys().fold( Map(), (acc, node) => @@ -793,7 +793,7 @@ module ccv_model { val NoProviderReuse = consumerChains.forall( consumer => - val valConsPk = currentState.providerState.validatorConsumerPubKey.getOrElse(consumer, Map()) + val valConsPk = currentState.providerState.validatorConsumerAddr.getOrElse(consumer, Map()) valConsPk.keys().forall( node => val consAddr = valConsPk.get(node) @@ -808,7 +808,7 @@ module ccv_model { val NoDuplicationOnSameConsumer = consumerChains.forall( consumer => - val valConsPk = currentState.providerState.validatorConsumerPubKey.getOrElse(consumer, Map()) + val valConsPk = currentState.providerState.validatorConsumerAddr.getOrElse(consumer, Map()) valConsPk.keys().forall( node => val consAddr = valConsPk.get(node) diff --git a/testutil/integration/validators.go b/testutil/integration/validators.go index 24429371b4..2fca9e5390 100644 --- a/testutil/integration/validators.go +++ b/testutil/integration/validators.go @@ -8,12 +8,6 @@ import ( tmtypes "github.com/cometbft/cometbft/types" ) -// creates n signers. does not return a validator set, just only the PrivValidators by their addresses -func CreateSigners(n int) (map[string]tmtypes.PrivValidator, error) { - _, _, signersByAddress, err := CreateValidators(n) - return signersByAddress, err -} - func CreateValidators(n int) ( *tmtypes.ValidatorSet, []types.ValidatorUpdate, map[string]tmtypes.PrivValidator, error, ) { From 7377eece919e3d72772bd59f30809a8341be2192 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 26 Jan 2024 11:46:13 +0100 Subject: [PATCH 4/8] Refactor keyAssignmentReplacement --- tests/mbt/model/ccv.qnt | 154 +++++++++++++--------------------- tests/mbt/model/ccv_model.qnt | 13 ++- 2 files changed, 63 insertions(+), 104 deletions(-) diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index 7fc6058b23..7d2185f91f 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -101,24 +101,22 @@ module ccv_types { runningVscId: int, // For every consumer chain, stores the consumer address assigned by each validator. - validatorConsumerAddr: Chain -> (Node -> ConsumerAddr), + validatorToConsumerAddr: Chain -> (Node -> ConsumerAddr), // For every consumer chain, holds the provider validator for each assigned consumer address. - validatorByConsumerAddr: Chain -> (ConsumerAddr -> Node), + // 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 key assignments that need to be replaced in the current block. - // Needed to apply the key assignments received in a block to the validator updates sent to the consumer chains. - // This is necessary because - // a key assignment itself triggers validator updates - //(old key to 0 power, new key to current power) - keyAssignmentReplacements: Chain -> (Node -> (ConsumerAddr, Power)), - - // Stores the mapping from VSC ids to consumer validators addresses. Needed for pruning validatorByConsumerAddr. + // 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. @@ -135,12 +133,12 @@ module ccv_types { providerValidatorSetChangedInThisBlock: false, consumerStatus: Map(), runningVscId: 0, - validatorConsumerAddr: Map(), + validatorToConsumerAddr: Map(), keyAssignedValSetHistory: Map(), - validatorByConsumerAddr: Map(), - keyAssignmentReplacements: Map(), + consumerAddrToValidator: Map(), consumerAddrsToPrune: Map(), - keyAssignmentsForVSCPackets: Map() + keyAssignmentsForVSCPackets: Map(), + consumersWithAddrAssignmentChangesInThisBlock: Set() } @@ -236,43 +234,22 @@ module ccv_types { consumer: Chain, valSet: ValidatorSet ): ValidatorSet = { - // map each validator in the valSet to a set of - // new updates. necessary to allow one validator to generate multiple updates, - // which in turn is needed when someone changes keys - // (set old key to 0, new key to current power) - pure val newValSet = valSet.keys().map( + // map each validator to a tuple of (consumer address, voting power) + valSet.keys().map( (node) => pure val power = valSet.get(node) - pure val keyAssignmentReplacements = providerState.keyAssignmentReplacements.getOrElse(consumer, Map()) - if(keyAssignmentReplacements.keys().contains(node)) { - // there is a KeyAssignmentReplacement - pure val replacement = keyAssignmentReplacements.get(node) - pure val oldConsAddr = replacement._1 - // set old key to 0 - pure val oldToZero = (oldConsAddr, 0) - // set new key to current power - pure val newToPower = (providerState.validatorConsumerAddr.getOrElse(consumer, Map()).getOrElse(node, node), power) - Set(oldToZero, newToPower) + // 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 { - // no replacement - // check if the validator has a key assigned - pure val validatorConsumerAddr = providerState.validatorConsumerAddr.getOrElse(consumer, Map()) - if (validatorConsumerAddr.keys().contains(node)) { - // the validator has a key assigned - pure val consAddr = validatorConsumerAddr.get(node) - Set((consAddr, power)) - } else { - // the validator has no key assigned - // use the default key - Set((node, power)) - } + // the validator has no key assigned + // use the default key + (node, power) } - ) - // flatten the map of sets into a set - pure val flattened = newValSet.flatten() - - // create a map from the set - flattened.fold( + ).fold( // fold the (addr,pow) tuples into a map addr -> pow Map(), (acc, pair) => acc.put(pair._1, pair._2) ) @@ -534,18 +511,9 @@ module ccv { ) - // send vsc packets + // send vsc packets (will be a noop if no sends are necessary) val providerStateAfterSending = - if ((currentProviderState.providerValidatorSetChangedInThisBlock or - currentProviderState.keyAssignmentReplacements.keys().exists( - consumer => currentProviderState.keyAssignmentReplacements.get(consumer).keys().size() > 0)) 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) // start/stop chains @@ -667,14 +635,14 @@ module ccv { } 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.validatorByConsumerAddr.getOrElse(consumer, Map()) + 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 { // this key can be assigned // get the old assigned key - pure val consKeyByVal = currentState.providerState.validatorConsumerAddr.getOrElse(consumer, Map()) + 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) @@ -696,48 +664,40 @@ module ccv { // 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 newKeyAssignmentReplacement = - if (provValPower > 0 and - not(currentState.providerState.keyAssignmentReplacements. - getOrElse(consumer, Map()).keys().contains(providerNode))) { - // the validator has positive power and is not already in the key assignment replacements - currentState.providerState.keyAssignmentReplacements.put( - consumer, - currentState.providerState.keyAssignmentReplacements.getOrElse(consumer, Map()).put( - providerNode, - (oldConsAddr, provValPower) - ) - ) + 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 { - currentState.providerState.keyAssignmentReplacements - + // 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( - "keyAssignmentReplacements", newKeyAssignmentReplacement + "consumersWithAddrAssignmentChangesInThisBlock", consumersWithAddrAssignmentChangesInThisBlock ) ) - pure val newvalidatorConsumerAddr = currentState.providerState.validatorConsumerAddr.put( + pure val newvalidatorToConsumerAddr = currentState.providerState.validatorToConsumerAddr.put( consumer, - currentState.providerState.validatorConsumerAddr.getOrElse(consumer, Map()).put( + currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()).put( providerNode, consumerAddr ) ) - pure val newValidatorByConsumerAddr = currentState.providerState.validatorByConsumerAddr.put( + pure val newconsumerAddrToValidator = currentState.providerState.consumerAddrToValidator.put( consumer, - currentState.providerState.validatorByConsumerAddr.getOrElse(consumer, Map()).put( + currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()).put( consumerAddr, providerNode ) ) pure val newProviderState = tmpStateAfterKeyAssignmentReplacement.providerState.with( - "validatorConsumerAddr", newvalidatorConsumerAddr + "validatorToConsumerAddr", newvalidatorToConsumerAddr ).with( - "validatorByConsumerAddr", newValidatorByConsumerAddr + "consumerAddrToValidator", newconsumerAddrToValidator ) Ok( @@ -878,15 +838,14 @@ module ccv { // 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. + // 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. pure def sendVscPackets(providerState: ProviderState, sendingTimestamp: Time): ProviderState = { val newSentPacketsPerConsumer = ConsumerChains.mapBy( (consumer) => - // if validator set changed (or a key assignment needs to be replaced) and the consumer is running, send a packet + // 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.keyAssignmentReplacements.getOrElse(consumer, Map()).keys().size() > 0) + providerState.consumersWithAddrAssignmentChangesInThisBlock.contains(consumer)) and isRunningConsumer(consumer, providerState)) { List({ @@ -904,13 +863,13 @@ module ccv { ) val newOutstandingPacketsToConsumer = ConsumerChains.mapBy( (consumer) => - providerState.outstandingPacketsToConsumer.get(consumer).concat( + providerState.outstandingPacketsToConsumer.getOrElse(consumer, List()).concat( newSentPacketsPerConsumer.get(consumer) ) ) val newSentVscPackets = ConsumerChains.mapBy( (consumer) => - providerState.sentVscPacketsToConsumer.get(consumer).concat( + providerState.sentVscPacketsToConsumer.getOrElse(consumer, List()).concat( newSentPacketsPerConsumer.get(consumer) ) ) @@ -918,14 +877,15 @@ module ccv { ...providerState, outstandingPacketsToConsumer: newOutstandingPacketsToConsumer, sentVscPacketsToConsumer: newSentVscPackets, - providerValidatorSetChangedInThisBlock: false, runningVscId: providerState.runningVscId + 1, - // key assignment replacements were performed, so we can clear them - keyAssignmentReplacements: Map(), + // 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.validatorConsumerAddr + providerState.validatorToConsumerAddr ) } } @@ -996,7 +956,7 @@ module ccv { // actually do the pruning pure val senderValByConsAddr = - newState.providerState.validatorByConsumerAddr.getOrElse(sender, Map()) + newState.providerState.consumerAddrToValidator.getOrElse(sender, Map()) pure val newSenderValByConsAddr = senderValByConsAddr.keys().filter( consAddr => not(consumerAddrsToPrune.contains(consAddr)) @@ -1006,9 +966,9 @@ module ccv { // update the provider state pure val newProviderState2 = newState.providerState.with( - // update the validatorByConsumerAddr map to remove the pruned keys - "validatorByConsumerAddr", - newState.providerState.validatorByConsumerAddr.put(sender, newSenderValByConsAddr) + // 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", diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt index a52a882528..81b1fa28ba 100644 --- a/tests/mbt/model/ccv_model.qnt +++ b/tests/mbt/model/ccv_model.qnt @@ -793,7 +793,7 @@ module ccv_model { val NoProviderReuse = consumerChains.forall( consumer => - val valConsPk = currentState.providerState.validatorConsumerAddr.getOrElse(consumer, Map()) + val valConsPk = currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) valConsPk.keys().forall( node => val consAddr = valConsPk.get(node) @@ -808,7 +808,7 @@ module ccv_model { val NoDuplicationOnSameConsumer = consumerChains.forall( consumer => - val valConsPk = currentState.providerState.validatorConsumerAddr.getOrElse(consumer, Map()) + val valConsPk = currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) valConsPk.keys().forall( node => val consAddr = valConsPk.get(node) @@ -823,7 +823,7 @@ module ccv_model { val CanAssignConsumerKey = not(consumerChains.exists( consumer => - currentState.providerState.validatorByConsumerAddr.getOrElse(consumer, Map()).keys().size() > 0 + currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()).keys().size() > 0 )) val CanHaveConsumerAddresses = @@ -860,7 +860,7 @@ module ccv_model { .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.get("node1") == 0), + 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") @@ -897,9 +897,8 @@ module ccv_model { // the old key should have been pruned all { // check that pruning has been performed nicely - assert(currentState.providerState.validatorByConsumerAddr.get("consumer1").get("consAddr1") == "node1"), - assert(currentState.providerState.consumerAddrsToPrune.get("consumer1").get(0).length() == 0), - assert(currentState.providerState.keyAssignmentReplacements.getOrElse("consumer1", Map()).keys().size() == 0), + 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) } From b7aca7c9e27cdc4561b89bae334e538f61d55325 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 26 Jan 2024 13:31:20 +0100 Subject: [PATCH 5/8] Start refactoring a few things --- tests/mbt/model/ccv.qnt | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index 7d2185f91f..9d3a1eda18 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -273,9 +273,11 @@ module ccv_types { // for each node in the valset, reverse its key assignment valSetWithAssignment.keys().map( - (node) => - pure val power = valSetWithAssignment.get(node) - pure val consAddr = reverseAssignment.getOrElse(node, node) + (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 @@ -539,7 +541,7 @@ module ccv { tmpState.consumerStates.keys().mapBy( (consumer) => if (consumersToStart.contains(consumer)) { - // modified by the key assignments for the 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( From b36bf35ab0efc81deba5b7bfa43452317a0806fa Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 26 Jan 2024 13:41:13 +0100 Subject: [PATCH 6/8] Refactor, take into account comments --- tests/mbt/model/ccv.qnt | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index 9d3a1eda18..cbd664b326 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -489,7 +489,7 @@ module ccv { res._1 ) - // store the valSet under the current key assignments + // for each consumer chain, apply the key assignment to the current validator set val currentValSets = ConsumerChains.mapBy( (consumer) => currentProviderState.applyKeyAssignmentToValSet( @@ -497,11 +497,12 @@ module ccv { 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()).prepend( - currentValSets.get(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 @@ -843,15 +844,17 @@ module ccv { // 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. pure def sendVscPackets(providerState: ProviderState, sendingTimestamp: Time): ProviderState = { - val newSentPacketsPerConsumer = ConsumerChains.mapBy( + val newSentPacketsPerConsumer = ConsumerChains.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 @@ -860,6 +863,7 @@ module ccv { timeoutTime: sendingTimestamp + CcvTimeout.get(PROVIDER_CHAIN) }) } else { + // no packet to be sent, so empty list List() } ) @@ -958,11 +962,14 @@ module ccv { // 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) ) From 36867d51312c92eed9e5b8868aab2c9e306116c9 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 26 Jan 2024 14:28:31 +0100 Subject: [PATCH 7/8] Refactor utility functions to type module --- tests/mbt/model/ccv.qnt | 1386 ++++++++++++++++++++------------------- 1 file changed, 699 insertions(+), 687 deletions(-) diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index cbd664b326..efe865ee4e 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -287,543 +287,118 @@ module ccv_types { ) } - -} - -module ccv { - // Implements the core logic of the cross-chain validation protocol. - - // Things that are not modelled: - // * Reward distribution - // * Slashes - - // Things that explicitly are modelled: - // * Validator set changes are propagated from provider to consumers - // * Vsc packets mature - - // We assume that packet receive + ack happen synchronously, - // i.e. when the packet is delivered, the ack is delivered right afterwards. - // This is because it is nontrivial in practice to get a relayer to relay a packet, but not its ack. - - import Time.* from "./libraries/Time" - import extraSpells.* from "./libraries/extraSpells" - import ccv_types.* - - // =================== - // PROTOCOL PARAMETERS + // UTILITY FUNCTIONS + // which do not hold the core logic of the protocol, but are still part of it // =================== - // the set of all possible consumer chains. - const ConsumerChains: Set[Chain] - - // For each chain, this defines the time between the initiation of an unbonding and its maturation. - const UnbondingPeriodPerChain: Chain -> int - - // The maximum time duration between sending any VscPacket to any consumer chain and receiving the - // corresponding VscMaturedPacket, without timing out the consumer chain and consequently removing it. - const VscTimeout: int - - // The timeoutTimestamp for sent packets. Can differ by chain. - const CcvTimeout: Chain -> int + // 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, []) - // 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 + pure val newConsAddrsToPrune = consumerAddrsToPrune.put(vscId, prevConsAddrs.append(oldConsAddr)) - // =================== - // PROTOCOL LOGIC contains the meat of the protocol - // functions here roughly correspond to API calls that can be triggered from external sources - // =================== - - // the power of a validator on the provider chain is changed by the given amount. We do not care how this happens, - // e.g. via undelegations, or delegations, ... - pure def votingPowerChange(currentState: ProtocolState, validator: Node, amount: int): Result = { - pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet - pure val oldVotingPower = if (currentValidatorSet.keys().contains(validator)) currentValidatorSet.get(validator) else 0 - if (amount == 0) { - Err("Voting power cannot change by zero!") - } else if (oldVotingPower == 0) { - Err("Voting power cannot be changed for a validator that is not in the current validator set!") - } else { - pure val newVotingPower = oldVotingPower + amount - pure val newValidatorSet = currentValidatorSet.put(validator, if(newVotingPower >= 0) newVotingPower else 0) - // if the new validator set contains no validators with positive voting power, the validator set is invalid - if (newValidatorSet.values().filter(votingPower => votingPower > 0).size() == 0) { - Err("Voting power change resulted in empty validator set!") - } else { - // set the validator set changed flag - val newProviderState = currentState.providerState.with( - "providerValidatorSetChangedInThisBlock", true - ) - pure val tmpState = currentState.with( - "providerState", newProviderState - ) - pure val newState = setProviderValidatorSet(tmpState, newValidatorSet) - Ok(newState) - } - } + currentState.with( + "providerState", + currentState.providerState.with( + "consumerAddrsToPrune", + currentState.providerState.consumerAddrsToPrune.put(consumer, newConsAddrsToPrune) + ) + ) } - // Delivers the next queued VscMaturedPacket from a consumer chain to the provider chain. - // Arguments are the currentState and the the consumer chain, from which the packet will be delivered. - // If this packet will time out on the provider on delivery, - // the consumer will be dropped. - // The first return is the result of the operation, the second result is a boolean - // that indicates whether the consumer timed out or not. - // If the result has an error, the second return should be ignored. - pure def deliverPacketToProvider(currentState: ProtocolState, sender: Chain): (Result, bool) = { - if (not(isRunningConsumer(sender, currentState.providerState))) { - (Err("Sender is not currently a consumer - must have 'running' status!"), false) - } else if (length(currentState.consumerStates.get(sender).outstandingPacketsToProvider) == 0) { - (Err("No outstanding packets to deliver"), false) - } else { - val packet = currentState.consumerStates.get(sender).outstandingPacketsToProvider.head() - if(packet.timeoutTime <= currentState.providerState.chainState.runningTimestamp) { - // drop consumer - val result = stopConsumers( - currentState.providerState.consumerStatus, - Set(), - Set(sender) + // 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) + } ) - - val newConsumerStatus = result._1 - val err = result._2 - if (err != "") { - (Err(err), false) - } else { - val newProviderState = currentState.providerState.with( - "consumerStatus", newConsumerStatus - ) - val newState: ProtocolState = currentState.with( - "providerState", newProviderState - ) - (Ok(newState), true) // true because the packet timed out - } + (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 { - // the packet has not timed out, so receive it on the provider - val result = recvPacketOnProvider(currentState, sender, packet) - val tmpState = result.newState - if (result.hasError()) { - (result, false) - } else { - (Ok(removeOutstandingPacketFromConsumer(tmpState, sender)), false) // false because the packet did not time out - } + val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( + (chain) => + if (consumersToStart.contains(chain)) { + RUNNING + } else { + currentConsumerStatusMap.get(chain) + } + ) + (newConsumerStatusMap, "") } } - } - // Delivers the next queued VscPacket from the provider chain to a consumer chain. - // Arguments are the current state and the consumer chain, to which the packet will be delivered. - // If this packet will time out on the consumer on delivery, - // the consumer will be dropped. - // The first return is the result of the operation, the second result is a boolean - // that indicates whether the consumer timed out or not. - // If the result has an error, the second return should be ignored. - pure def deliverPacketToConsumer(currentState: ProtocolState, receiver: Chain): (Result, bool) = { - if (not(isRunningConsumer(receiver, currentState.providerState))) { - (Err("Receiver is not currently a consumer - must have 'running' status!"), false) - } else if (length(currentState.providerState.outstandingPacketsToConsumer.get(receiver)) == 0) { - (Err("No outstanding packets to deliver"), false) + 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 packet = currentState.providerState.outstandingPacketsToConsumer.get(receiver).head() - // check if the consumer timed out - if (packet.timeoutTime <= currentState.consumerStates.get(receiver).chainState.runningTimestamp) { - // drop consumer - val result = stopConsumers( - currentState.providerState.consumerStatus, - Set(), - Set(receiver) - ) - - val newConsumerStatus = result._1 - val err = result._2 - if (err != "") { - (Err(err), false) - } else { - val newProviderState = currentState.providerState.with( - "consumerStatus", newConsumerStatus - ) - val newState: ProtocolState = currentState.with( - "providerState", newProviderState - ) - (Ok(newState), true) // true because the packet timed out - } + 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 { - // the packet has not timed out, so receive it on the consumer - val result = recvPacketOnConsumer(currentState, receiver, packet) - val tmpState = result.newState - if (result.hasError()) { - (result, false) - } else { - (Ok(removeOutstandingPacketFromProvider(tmpState, receiver)), false) // false because the packet did not time out - } + (res2._1, "") } } } - - /// Ends a block on the provider. This means that the current validator set is committed on chain, - /// packets are queued, and the next block is started. Also, consumers that have passed - /// the VscTimeout without responding to a pending vscpacket are dropped. - pure def endAndBeginBlockForProvider( - currentState: ProtocolState, - // by how much the timestamp should be advanced, - // i.e. the timestamp for the next block is oldTimestamp + timeAdvancement - timeAdvancement: Time, - // a set of consumers that were not consumers before, but should be set to running now. - consumersToStart: Set[Chain], - // a set of consumers that were running before, but should be set to stopped now. - // This argument only needs to contain "voluntary" stops - - // forced stops, e.g. because a consumer timed out, - // will be added automatically. - consumersToStop: Set[Chain]): Result = { - val currentProviderState = currentState.providerState - - // check for vsc timeouts - val timedOutConsumers = getRunningConsumers(currentProviderState).filter( - consumer => - val res = TimeoutDueToVscTimeout(currentState, consumer) - 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, chainState: newChainState, keyAssignedValSetHistory: newKeyAssignedValSetHistory} - val tmpState = currentState.with( - "providerState", providerStateAfterTimeAdvancement - ) - - - // send vsc packets (will be a noop if no sends are necessary) - val providerStateAfterSending = - providerStateAfterTimeAdvancement.sendVscPackets(currentProviderState.chainState.runningTimestamp) - - - // start/stop chains - val res = providerStateAfterSending.consumerStatus.StartStopConsumers( - consumersToStart, - consumersToStop, - timedOutConsumers - ) - val newConsumerStatus = res._1 - val err = res._2 - val providerStateAfterConsumerAdvancement = providerStateAfterSending.with( - "consumerStatus", newConsumerStatus - ).with( - "providerValidatorSetChangedInThisBlock", false - ) - - 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... - 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", consValSet - ).with( - "votingPowerHistory", - List(consValSet) - ).with( - "lastTimestamp", - providerStateAfterConsumerAdvancement.chainState.lastTimestamp - ).with( - "runningTimestamp", - providerStateAfterConsumerAdvancement.chainState.runningTimestamp - ) - ) - newConsumerState - } else { - currentState.consumerStates.get(consumer) - } - ) - val newState = tmpState.with( - "providerState", providerStateAfterConsumerAdvancement - ).with( - "consumerStates", newConsumerStateMap - ) - - Ok(newState) - } - } - - pure def endAndBeginBlockForConsumer( - currentState: ProtocolState, - chain: Chain, - // by how much the timestamp of the chain should be advanced for the next block - timeAdvancement: Time): Result = { - if (not(currentState.consumerStates.keys().contains(chain))) { - // if the chain is not a consumer, return an error - Err("chain is not a consumer") - } else { - val currentConsumerState: ConsumerState = currentState.consumerStates.get(chain) - val oldChainState: ChainState = currentConsumerState.chainState - val newChainState: ChainState = currentConsumerState.chainState.endAndBeginBlockShared(timeAdvancement) - val newConsumerState: ConsumerState = currentConsumerState.with( - "chainState", newChainState - ) - val maturedPackets = newConsumerState.maturationTimes.select( - pair => - val packet = pair._1 - val maturationTime: Time = pair._2 - // important: this uses the last committed timestamp, not the running timestamp! - maturationTime <= newChainState.lastTimestamp - ).transform(pair => pair._1) - val newMaturationTimes = newConsumerState.maturationTimes.select( - pair => - val packet = pair._1 - val maturationTime: Time = pair._2 - // important: this uses the last committed timestamp, not the running timestamp! - - maturationTime > newChainState.lastTimestamp - ) - val newOutstandingPackets = newConsumerState.outstandingPacketsToProvider.concat( - maturedPackets.transform( - packet => { - id: packet.id, - // it is important to use the oldChainState here, since this happens during EndBlock - sendingTime: oldChainState.runningTimestamp, - timeoutTime: oldChainState.runningTimestamp + CcvTimeout.get(chain) - } - ) - ) - val newConsumerState2: ConsumerState = newConsumerState.with( - "maturationTimes", newMaturationTimes - ).with( - "outstandingPacketsToProvider", newOutstandingPackets - ) - val newConsumerStates = currentState.consumerStates.set(chain, newConsumerState2) - val newState: ProtocolState = currentState.with( - "consumerStates", newConsumerStates - ) - Ok(newState) - } - } - - // 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 { - // 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 { - // 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 - ) - ) - - pure val newvalidatorToConsumerAddr = currentState.providerState.validatorToConsumerAddr.put( - consumer, - currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()).put( - providerNode, - consumerAddr - ) - ) - - pure val newconsumerAddrToValidator = currentState.providerState.consumerAddrToValidator.put( - consumer, - currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()).put( - consumerAddr, - providerNode - ) - ) - - pure val newProviderState = tmpStateAfterKeyAssignmentReplacement.providerState.with( - "validatorToConsumerAddr", newvalidatorToConsumerAddr - ).with( - "consumerAddrToValidator", newconsumerAddrToValidator - ) - - Ok( - tmpStateAfterKeyAssignmentReplacement.with( - "providerState", newProviderState - ) - ) - } - } - } - - // =================== - // UTILITY FUNCTIONS - // which do not hold the core logic of the protocol, but are still part of it - // =================== - - // 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 - ) - ) - } + // 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 = @@ -843,8 +418,12 @@ module ccv { // * 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. - pure def sendVscPackets(providerState: ProviderState, sendingTimestamp: Time): ProviderState = { - val newSentPacketsPerConsumer = ConsumerChains.mapBy( // compute, for each consumer, a list of new packets to be sent + // 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.getRunningConsumers().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 @@ -860,20 +439,20 @@ module ccv { providerState.chainState.currentValidatorSet ), sendingTime: sendingTimestamp, - timeoutTime: sendingTimestamp + CcvTimeout.get(PROVIDER_CHAIN) + timeoutTime: sendingTimestamp + ccvTimeout }) } else { // no packet to be sent, so empty list List() } ) - val newOutstandingPacketsToConsumer = ConsumerChains.mapBy( + val newOutstandingPacketsToConsumer = providerState.getRunningConsumers().mapBy( (consumer) => providerState.outstandingPacketsToConsumer.getOrElse(consumer, List()).concat( newSentPacketsPerConsumer.get(consumer) ) ) - val newSentVscPackets = ConsumerChains.mapBy( + val newSentVscPackets = providerState.getRunningConsumers().mapBy( (consumer) => providerState.sentVscPacketsToConsumer.getOrElse(consumer, List()).concat( newSentPacketsPerConsumer.get(consumer) @@ -896,201 +475,634 @@ module ccv { } } - // 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) + // 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 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.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, "") + } + } + + +} + +module ccv { + // Implements the core logic of the cross-chain validation protocol. + + // Things that are not modelled: + // * Reward distribution + // * Slashes + + // Things that explicitly are modelled: + // * Validator set changes are propagated from provider to consumers + // * Vsc packets mature + + // We assume that packet receive + ack happen synchronously, + // i.e. when the packet is delivered, the ack is delivered right afterwards. + // This is because it is nontrivial in practice to get a relayer to relay a packet, but not its ack. + + import Time.* from "./libraries/Time" + import extraSpells.* from "./libraries/extraSpells" + import ccv_types.* + + + // =================== + // PROTOCOL PARAMETERS + // =================== + + // the set of all possible consumer chains. + const ConsumerChains: Set[Chain] + + // For each chain, this defines the time between the initiation of an unbonding and its maturation. + const UnbondingPeriodPerChain: Chain -> int + + // The maximum time duration between sending any VscPacket to any consumer chain and receiving the + // corresponding VscMaturedPacket, without timing out the consumer chain and consequently removing it. + const VscTimeout: int + + // 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 + + // =================== + // PROTOCOL LOGIC contains the meat of the protocol + // functions here roughly correspond to API calls that can be triggered from external sources + // =================== + + // the power of a validator on the provider chain is changed by the given amount. We do not care how this happens, + // e.g. via undelegations, or delegations, ... + pure def votingPowerChange(currentState: ProtocolState, validator: Node, amount: int): Result = { + pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet + pure val oldVotingPower = if (currentValidatorSet.keys().contains(validator)) currentValidatorSet.get(validator) else 0 + if (amount == 0) { + Err("Voting power cannot change by zero!") + } else if (oldVotingPower == 0) { + Err("Voting power cannot be changed for a validator that is not in the current validator set!") + } else { + pure val newVotingPower = oldVotingPower + amount + pure val newValidatorSet = currentValidatorSet.put(validator, if(newVotingPower >= 0) newVotingPower else 0) + // if the new validator set contains no validators with positive voting power, the validator set is invalid + if (newValidatorSet.values().filter(votingPower => votingPower > 0).size() == 0) { + Err("Voting power change resulted in empty validator set!") + } else { + // set the validator set changed flag + val newProviderState = currentState.providerState.with( + "providerValidatorSetChangedInThisBlock", true + ) + pure val tmpState = currentState.with( + "providerState", newProviderState + ) + pure val newState = setProviderValidatorSet(tmpState, newValidatorSet) + Ok(newState) } - 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 = { + // Delivers the next queued VscMaturedPacket from a consumer chain to the provider chain. + // Arguments are the currentState and the the consumer chain, from which the packet will be delivered. + // If this packet will time out on the provider on delivery, + // the consumer will be dropped. + // The first return is the result of the operation, the second result is a boolean + // that indicates whether the consumer timed out or not. + // If the result has an error, the second return should be ignored. + pure def deliverPacketToProvider(currentState: ProtocolState, sender: Chain): (Result, bool) = { 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") + (Err("Sender is not currently a consumer - must have 'running' status!"), false) + } else if (length(currentState.consumerStates.get(sender).outstandingPacketsToProvider) == 0) { + (Err("No outstanding packets to deliver"), false) } 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) + val packet = currentState.consumerStates.get(sender).outstandingPacketsToProvider.head() + if(packet.timeoutTime <= currentState.providerState.chainState.runningTimestamp) { + // drop consumer + val result = stopConsumers( + currentState.providerState.consumerStatus, + Set(), + Set(sender) ) - // 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() + val newConsumerStatus = result._1 + val err = result._2 + if (err != "") { + (Err(err), false) + } else { + val newProviderState = currentState.providerState.with( + "consumerStatus", newConsumerStatus ) - ) - ) + val newState: ProtocolState = currentState.with( + "providerState", newProviderState + ) + (Ok(newState), true) // true because the packet timed out + } + } else { + // the packet has not timed out, so receive it on the provider + val result = recvPacketOnProvider(currentState, sender, packet) + val tmpState = result.newState + if (result.hasError()) { + (result, false) + } else { + (Ok(removeOutstandingPacketFromConsumer(tmpState, sender)), false) // false because the packet did not time out + } + } + } + } - // update the state - pure val newState2 = newState.with( - "providerState", newProviderState2 - ) + // Delivers the next queued VscPacket from the provider chain to a consumer chain. + // Arguments are the current state and the consumer chain, to which the packet will be delivered. + // If this packet will time out on the consumer on delivery, + // the consumer will be dropped. + // The first return is the result of the operation, the second result is a boolean + // that indicates whether the consumer timed out or not. + // If the result has an error, the second return should be ignored. + pure def deliverPacketToConsumer(currentState: ProtocolState, receiver: Chain): (Result, bool) = { + if (not(isRunningConsumer(receiver, currentState.providerState))) { + (Err("Receiver is not currently a consumer - must have 'running' status!"), false) + } else if (length(currentState.providerState.outstandingPacketsToConsumer.get(receiver)) == 0) { + (Err("No outstanding packets to deliver"), false) + } else { + val packet = currentState.providerState.outstandingPacketsToConsumer.get(receiver).head() + // check if the consumer timed out + if (packet.timeoutTime <= currentState.consumerStates.get(receiver).chainState.runningTimestamp) { + // drop consumer + val result = stopConsumers( + currentState.providerState.consumerStatus, + Set(), + Set(receiver) + ) - Ok(newState2) + val newConsumerStatus = result._1 + val err = result._2 + if (err != "") { + (Err(err), false) + } else { + val newProviderState = currentState.providerState.with( + "consumerStatus", newConsumerStatus + ) + val newState: ProtocolState = currentState.with( + "providerState", newProviderState + ) + (Ok(newState), true) // true because the packet timed out + } + } else { + // the packet has not timed out, so receive it on the consumer + val result = recvPacketOnConsumer(currentState, receiver, packet, UnbondingPeriodPerChain.get(receiver)) + val tmpState = result.newState + if (result.hasError()) { + (result, false) + } else { + (Ok(removeOutstandingPacketFromProvider(tmpState, receiver)), false) // false because the packet did not time out + } + } } } - // 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 + + + /// Ends a block on the provider. This means that the current validator set is committed on chain, + /// packets are queued, and the next block is started. Also, consumers that have passed + /// the VscTimeout without responding to a pending vscpacket are dropped. + pure def endAndBeginBlockForProvider( + currentState: ProtocolState, + // by how much the timestamp should be advanced, + // i.e. the timestamp for the next block is oldTimestamp + timeAdvancement + timeAdvancement: Time, + // a set of consumers that were not consumers before, but should be set to running now. + consumersToStart: Set[Chain], + // a set of consumers that were running before, but should be set to stopped now. + // This argument only needs to contain "voluntary" stops - + // forced stops, e.g. because a consumer timed out, + // will be added automatically. + consumersToStop: Set[Chain]): Result = { + val currentProviderState = currentState.providerState + + // check for vsc timeouts + val timedOutConsumers = getRunningConsumers(currentProviderState).filter( + 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 ) - val newConsumerStates = currentState.consumerStates.set(sender, newConsumerState) - val newState = currentState.with( - "consumerStates", newConsumerStates + + // run the shared core chainState logic + val newChainState = currentProviderState.chainState.endAndBeginBlockShared(timeAdvancement) + val providerStateAfterTimeAdvancement = + {...currentProviderState, chainState: newChainState, keyAssignedValSetHistory: newKeyAssignedValSetHistory} + val tmpState = currentState.with( + "providerState", providerStateAfterTimeAdvancement ) - 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) + // send vsc packets (will be a noop if no sends are necessary) + val providerStateAfterSending = + providerStateAfterTimeAdvancement.sendVscPackets( + currentProviderState.chainState.runningTimestamp, + CcvTimeout.get(PROVIDER_CHAIN) + ) + + + // start/stop chains + val res = providerStateAfterSending.consumerStatus.StartStopConsumers( + consumersToStart, + consumersToStop, + timedOutConsumers ) - val newState = currentState.with( - "providerState", newProviderState + val newConsumerStatus = res._1 + val err = res._2 + val providerStateAfterConsumerAdvancement = providerStateAfterSending.with( + "consumerStatus", newConsumerStatus + ).with( + "providerValidatorSetChangedInThisBlock", false ) - 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 + 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... + 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", consValSet + ).with( + "votingPowerHistory", + List(consValSet) + ).with( + "lastTimestamp", + providerStateAfterConsumerAdvancement.chainState.lastTimestamp + ).with( + "runningTimestamp", + providerStateAfterConsumerAdvancement.chainState.runningTimestamp + ) + ) + newConsumerState + } else { + currentState.consumerStates.get(consumer) + } + ) + val newState = tmpState.with( + "providerState", providerStateAfterConsumerAdvancement + ).with( + "consumerStates", newConsumerStateMap ) - ) - } - // 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 + Ok(newState) + } } - // 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 - ) - } + pure def endAndBeginBlockForConsumer( + currentState: ProtocolState, + chain: Chain, + // by how much the timestamp of the chain should be advanced for the next block + timeAdvancement: Time): Result = { + if (not(currentState.consumerStates.keys().contains(chain))) { + // if the chain is not a consumer, return an error + Err("chain is not a consumer") + } else { + val currentConsumerState: ConsumerState = currentState.consumerStates.get(chain) + val oldChainState: ChainState = currentConsumerState.chainState + val newChainState: ChainState = currentConsumerState.chainState.endAndBeginBlockShared(timeAdvancement) + val newConsumerState: ConsumerState = currentConsumerState.with( + "chainState", newChainState + ) + val maturedPackets = newConsumerState.maturationTimes.select( + pair => + val packet = pair._1 + val maturationTime: Time = pair._2 + // important: this uses the last committed timestamp, not the running timestamp! + maturationTime <= newChainState.lastTimestamp + ).transform(pair => pair._1) + val newMaturationTimes = newConsumerState.maturationTimes.select( + pair => + val packet = pair._1 + val maturationTime: Time = pair._2 + // important: this uses the last committed timestamp, not the running timestamp! - // 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 - ) + maturationTime > newChainState.lastTimestamp + ) + val newOutstandingPackets = newConsumerState.outstandingPacketsToProvider.concat( + maturedPackets.transform( + packet => { + id: packet.id, + // it is important to use the oldChainState here, since this happens during EndBlock + sendingTime: oldChainState.runningTimestamp, + timeoutTime: oldChainState.runningTimestamp + CcvTimeout.get(chain) + } + ) + ) + val newConsumerState2: ConsumerState = newConsumerState.with( + "maturationTimes", newMaturationTimes + ).with( + "outstandingPacketsToProvider", newOutstandingPackets + ) + val newConsumerStates = currentState.consumerStates.set(chain, newConsumerState2) + val newState: ProtocolState = currentState.with( + "consumerStates", newConsumerStates + ) + Ok(newState) + } } - // 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!") + // 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 { - 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, "") + // 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 { + // 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 { - // no timeout yet, it has not been VscTimeout since that packet was sent - (false, "") + (providerNode, false) } - } else { - // no packet has been sent yet, so no timeout - (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 { + // 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 + ) + ) + + pure val newvalidatorToConsumerAddr = currentState.providerState.validatorToConsumerAddr.put( + consumer, + currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()).put( + providerNode, + consumerAddr + ) + ) + + pure val newconsumerAddrToValidator = currentState.providerState.consumerAddrToValidator.put( + consumer, + currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()).put( + consumerAddr, + providerNode + ) + ) + + pure val newProviderState = tmpStateAfterKeyAssignmentReplacement.providerState.with( + "validatorToConsumerAddr", newvalidatorToConsumerAddr + ).with( + "consumerAddrToValidator", newconsumerAddrToValidator + ) + + Ok( + tmpStateAfterKeyAssignmentReplacement.with( + "providerState", newProviderState + ) + ) } } + } // =================== // ASSUMPTIONS ON MODEL PARAMETERS From 5aec1023ce662a3b3b619f88fdbcd26790665853 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 26 Jan 2024 14:37:45 +0100 Subject: [PATCH 8/8] Minor refactor --- tests/mbt/model/ccv.qnt | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index efe865ee4e..9aa8c7612a 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -227,6 +227,12 @@ module ccv_types { // whether a chain is the provider or not pure val PROVIDER_CHAIN = "provider" + // =================== + // UTILITY FUNCTIONS + // which do not hold the core logic of the protocol, but are invoked by it + // =================== + + // 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( @@ -287,11 +293,6 @@ module ccv_types { ) } - // =================== - // UTILITY FUNCTIONS - // which do not hold the core logic of the protocol, but are still part of it - // =================== - // 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 = {