diff --git a/Makefile b/Makefile index 350c66f8af..04df703370 100644 --- a/Makefile +++ b/Makefile @@ -131,7 +131,9 @@ test-trace: verify-models: quint test tests/mbt/model/ccv_test.qnt;\ quint test tests/mbt/model/ccv_model.qnt;\ - quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" tests/mbt/model/ccv_model.qnt --max-steps 200 --max-samples 200 + quint test tests/mbt/model/ccv_pss_test.qnt;\ + quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" tests/mbt/model/ccv_model.qnt --max-steps 200 --max-samples 200;\ + quint run --invariant "all{ValidatorUpdatesArePropagatedKeyAssignmentInv,ValidatorSetHasExistedKeyAssignmentInv,SameVscPacketsKeyAssignmentInv,MatureOnTimeInv,EventuallyMatureOnProviderInv,KeyAssignmentRulesInv}" tests/mbt/model/ccv_model.qnt --step stepKeyAssignment --max-steps 200 --max-samples 200 diff --git a/tests/mbt/model/README.md b/tests/mbt/model/README.md index f53900e77f..d466605bda 100644 --- a/tests/mbt/model/README.md +++ b/tests/mbt/model/README.md @@ -31,16 +31,31 @@ All the logic in EndBlock/BeginBlock happens here, like updating the validator s * `EndAndBeginBlockForConsumer(chain: Chain, timeAdvancement: Time)`: On the consumer `chain`, ends the current block, and begins a new one. Again, all the logic in EndBlock/BeginBlock happens here, like validator set change maturations. * `DeliverVscPacket(receiver: Chain)`: Delivers a pending VSCPacket from the provider to the consumer `receiver`. * `DeliverVscMaturedPacket(receiver: Chain)`: Delivers a pending VSCMaturedPacket from the consumer `receiver` to the provider. +* `KeyAssignment(chain: Chain, validator: Node, consumerAddr: ConsumerAddr)` (only when running with `--step stepKeyAssignment`): Assigns the `consumerAddr` to the `validator` on the `chain`. Note that we use "key" and "consumerAddr" pretty much interchangeably, as the model makes no differentiation between private keys, public keys, addresses, etc, as it doesn't model the cryptography. ### State machines There are 3 different "state machine layers" that can be put on top of the core logic. +Some layers include extra logic, need other invariants, ... #### ccv_model.qnt This is the most general state machine layer. It allows the most behaviour, in particular it allows abitrary clock drift between chains, it allows starting and stopping consumer chains during runtime, etc. This layer is most useful for model checking, because it encompasses the most behaviour. +As an optional module, it can also include KeyAssignment. + +##### KeyAssignment + +To run with key assignment, specify the step flag: `--step stepKeyAssignment`. + +KeyAssignment also needs some different invariants, see below. + +#### Partial Set Security + +To run with Partial Set Security, specify the step flag `--step stepBoundedDriftKeyAndPSS`. +This runs both PSS and Key Assignment. +It also requires running with `ccv_boundeddrift.qnt`, see below. #### ccv_boundeddrift.qnt This state machine layer is more restricted to generate more interesting traces: @@ -66,10 +81,7 @@ traces are not very useful for testing. To run unit tests, run ``` -quint test ccv_test.qnt -``` -and -``` +quint test ccv_test.qnt; quint test ccv_model.qnt ``` @@ -94,6 +106,13 @@ with a timestamp >= t + UnbondingPeriod on that consumer. - [X] EventuallyMatureOnProviderInv: If we send a VscPacket, this is eventually responded to by all consumers that were running at the time the packet was sent (and are still running). +Invariants only relevant when running with key assignment (`--step stepKeyAssignment`): +- [X] ValidatorSetHasExistedKeyAssignmentInv: Should replace ValidatorSetHasExistedInv when running with `--step stepKeyAssignment`. Validator sets are checked for equality under key assignment when checking whether they have existed. +- [X] SameVscPacketsKeyAssignmentInv: Should replace SameVscPacketsInv when running with `--step stepKeyAssignment`. VscPackets are checked for equality under key assignment when ensuring consumers receive the same ones. +- [X] KeyAssignmentRulesInv: Ensures the rules of key assignment are never violated. The two rules relevant for the model are: 1) validator A cannot assign consumer key K to consumer chain X if there is already a validator B (B!=A) +using K on the provider, and 2) validator A cannot assign consumer key K to consumer chain X if there is already a validator B using K on X + + Invariants can also be model-checked by Apalache, using this command: ``` quint verify --invariant ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv \ @@ -113,4 +132,10 @@ The available sanity checks are: - CanStopConsumer - CanTimeoutConsumer - CanSendVscPackets -- CanSendVscMaturedPackets \ No newline at end of file +- CanSendVscMaturedPackets +- CanAssignConsumerKey (only with `--step stepKeyAssignment`) +- CanHaveConsumerAddresses (only with `--step stepKeyAssignment`) +- CanOptIn (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`) +- CanOptOut (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`) +- CanFailOptOut (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`) +- CanHaveOptIn (only with `--step stepBoundedDriftKeyAndPSS` on `ccv_boundeddrift.qnt`) \ No newline at end of file diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index 6d9450b6f0..f780e4c9d5 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -1,6 +1,7 @@ // -*- mode: Bluespec; -*- module ccv_types { import Time.* from "./libraries/Time" + import extraSpells.* from "./libraries/extraSpells" type Node = str type Chain = str @@ -11,6 +12,11 @@ module ccv_types { // a list of validator sets per blocks, ordered by recency type VotingPowerHistory = List[ValidatorSet] + // For key assignment, to differentiate Nodes + // (on the provider) from the assigned + // keys/addresses on consumers + type ConsumerAddr = str + type VscPacket = { // the identifier for this packet @@ -93,6 +99,39 @@ module ccv_types { // a monotonic strictly increasing and positive ID that is used // to uniquely identify the Vscs sent to the consumer chains. runningVscId: int, + + // For every consumer chain, stores the consumer address assigned by each validator. + validatorToConsumerAddr: Chain -> (Node -> ConsumerAddr), + + // For every consumer chain, holds the provider validator for each assigned consumer address. + // Note that this is *not* precisely the reverse of validatorToConsumerAddr, + // because when a validator changes their consumer addr, + // the old one stays in this map until pruned. + consumerAddrToValidator: Chain -> (ConsumerAddr -> Node), + + // For every consumer chain, stores whether the key assignment for the consumer chain has changed in this block. + consumersWithAddrAssignmentChangesInThisBlock: Set[Chain], + + // the history of validator sets on the provider, but with the key assignments applied. + // This is needed to check invariants about the validator set when key assignments are in play. + keyAssignedValSetHistory: Chain -> VotingPowerHistory, + + // Stores the mapping from VSC ids to consumer validators addresses. Needed for pruning consumerAddrToValidator. + consumerAddrsToPrune: Chain -> VscId -> List[ConsumerAddr], + + // For every sent VSCPacket, stores the key assignments that were applied to send it. + keyAssignmentsForVSCPackets: VscId -> (Chain -> (Node -> ConsumerAddr)), + + // For each consumer chain, + // stores the set of validators that are opted into running the chain. + optedInVals: Chain -> Set[Node], + + // for each consumer, stores the top N for that consumer. + // The top N% of the validator set by voting power + // is obliged to run a topN chain. + // If the chain is a pure opt-in chain (where noone is forced to run it), + // this is 0. + topNByConsumer: Chain -> int, } // utility function: returns a provider state that is initialized minimally. @@ -105,6 +144,14 @@ module ccv_types { providerValidatorSetChangedInThisBlock: false, consumerStatus: Map(), runningVscId: 0, + validatorToConsumerAddr: Map(), + keyAssignedValSetHistory: Map(), + consumerAddrToValidator: Map(), + consumerAddrsToPrune: Map(), + keyAssignmentsForVSCPackets: Map(), + optedInVals: Map(), + topNByConsumer: Map(), + consumersWithAddrAssignmentChangesInThisBlock: Set() } @@ -192,6 +239,33 @@ module ccv_types { // given as a pure val so that we can switch cases based on // whether a chain is the provider or not pure val PROVIDER_CHAIN = "provider" + + // A record that keeps the information needed to add a new consumer. + // In particular, holds: + // the chain name/identifier, + // and the top N factor for the chain. + type ConsumerAdditionMsg = { + chain: Chain, + topN: int + } + + // Creates a new ConsumerAdditionMsg with a given top N. + pure def NewTopNConsumer(chain: Chain, topN: int): ConsumerAdditionMsg = { + { + chain: chain, + topN: topN + } + } + + // Creates a new ConsumerAdditionMsg with topN = 0. + pure def NewOptInConsumer(chain: Chain): ConsumerAdditionMsg = { + NewTopNConsumer(chain, 0) + } + + // Creates a new ConsumerAdditionMsg with top N = 100%. + pure def NewFullConsumer(chain: Chain): ConsumerAdditionMsg = { + NewTopNConsumer(chain, 100) + } } module ccv { @@ -212,6 +286,8 @@ module ccv { import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" import ccv_types.* + import ccv_pss.* from "./ccv_pss" + import ccv_utils.* from "./ccv_utils" // =================== @@ -356,7 +432,7 @@ module ccv { } } else { // the packet has not timed out, so receive it on the consumer - val result = recvPacketOnConsumer(currentState, receiver, packet) + val result = recvPacketOnConsumer(currentState, receiver, packet, UnbondingPeriodPerChain.get(receiver)) val tmpState = result.newState if (result.hasError()) { (result, false) @@ -378,81 +454,96 @@ module ccv { // 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], + consumersToStart: Set[ConsumerAdditionMsg], // 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 + val curValSet = currentProviderState.chainState.currentValidatorSet // check for vsc timeouts val timedOutConsumers = getRunningConsumers(currentProviderState).filter( consumer => - val res = TimeoutDueToVscTimeout(currentState, consumer) + val res = TimeoutDueToVscTimeout(currentState, consumer, VscTimeout) res._1 ) - // run the shared core chainState logic val newChainState = currentProviderState.chainState.endAndBeginBlockShared(timeAdvancement) - val providerStateAfterTimeAdvancement = currentProviderState.with( - "chainState", newChainState - ) - + val providerStateAfterTimeAdvancement = + {...currentProviderState, chainState: newChainState} val tmpState = currentState.with( "providerState", providerStateAfterTimeAdvancement ) - // send vsc packets + // send vsc packets (will be a noop if no sends are necessary) val providerStateAfterSending = - if (currentProviderState.providerValidatorSetChangedInThisBlock and - // important: check this on the provider state after the consumer advancement, not on the current state. - getRunningConsumers(providerStateAfterTimeAdvancement).size() > 0) { - // need to use the old timestamp because this happens during EndBlock - providerStateAfterTimeAdvancement.sendVscPackets(currentProviderState.chainState.runningTimestamp) - } else { - providerStateAfterTimeAdvancement - } + providerStateAfterTimeAdvancement.sendVscPackets( + currentProviderState.chainState.runningTimestamp, + CcvTimeout.get(PROVIDER_CHAIN) + ) // start/stop chains - val res = providerStateAfterSending.consumerStatus.StartStopConsumers( + val res = providerStateAfterSending.StartStopConsumers( consumersToStart, consumersToStop, timedOutConsumers ) - val newConsumerStatus = res._1 + val providerStateAfterConsumerAdvancement = res._1.with("providerValidatorSetChangedInThisBlock", false) val err = res._2 - val providerStateAfterConsumerAdvancement = providerStateAfterSending.with( - "consumerStatus", newConsumerStatus - ).with( - "providerValidatorSetChangedInThisBlock", false - ) + + val consumerAdditions = consumersToStart.map(consumer => consumer.chain) + + // for each running consumer chain, opt in validators that are in the top N + val providerStateAfterPSS = providerStateAfterConsumerAdvancement.endBlockPSS() 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 + // for each consumer chain, apply the key assignment to the current validator set + val currentValSets = getRunningConsumers(providerStateAfterPSS).mapBy( + (consumer) => + providerStateAfterPSS.applyKeyAssignmentToValSet( + consumer, + // get the validator set after partial set security has been applied + GetPSSValidatorSet(providerStateAfterPSS, curValSet, consumer) + ) + ) + + // store the current validator set with the key assignments applied in the history + val newKeyAssignedValSetHistory = currentValSets.keys().mapBy( + (consumer) => + providerStateAfterPSS.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 providerStateAfterStoringValSets = providerStateAfterPSS.with( + "keyAssignedValSetHistory", newKeyAssignedValSetHistory + ) + val newConsumerStateMap = tmpState.consumerStates.keys().mapBy( (consumer) => - if (consumersToStart.contains(consumer)) { + if (consumerAdditions.contains(consumer)) { val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer) + // correctly set the state for the new consumer val newConsumerState: ConsumerState = currentConsumerState.with( "chainState", currentConsumerState.chainState.with( - "currentValidatorSet", valSet + "currentValidatorSet", currentValSets.get(consumer) ).with( "votingPowerHistory", - List(valSet) + List(currentValSets.get(consumer)) ).with( "lastTimestamp", - providerStateAfterConsumerAdvancement.chainState.lastTimestamp + providerStateAfterStoringValSets.chainState.lastTimestamp ).with( "runningTimestamp", - providerStateAfterConsumerAdvancement.chainState.runningTimestamp + providerStateAfterStoringValSets.chainState.runningTimestamp ) ) newConsumerState @@ -461,7 +552,7 @@ module ccv { } ) val newState = tmpState.with( - "providerState", providerStateAfterConsumerAdvancement + "providerState", providerStateAfterStoringValSets ).with( "consumerStates", newConsumerStateMap ) @@ -523,308 +614,90 @@ module ccv { } } - // =================== - // UTILITY FUNCTIONS - // which do not hold the core logic of the protocol, but are still part of it - // =================== - - // Returns the new ConsumerStatusMap according to the consumers to stop - // and the consumers to time out. - // If a consumer is both stopped and timed out, it will be timed out. - // The second return is an error string: If it is not equal to "", - // it contains an error message, and the first return should be ignored. - pure def stopConsumers( - currentConsumerStatusMap: Chain -> str, - consumersToStop: Set[Chain], - consumersToTimeout: Set[Chain]): (Chain -> str, str) = { - val runningConsumers = currentConsumerStatusMap.keys().filter( - chain => currentConsumerStatusMap.get(chain) == RUNNING - ) - // all consumers to stop must be running right now, else we have an error - if (consumersToStop.exclude(runningConsumers).size() > 0) { - (currentConsumerStatusMap, "Cannot stop a consumer that is not running") + // Validator providerNode assigns their address for the consumer to be the consumerAddress. + pure def assignConsumerKey(currentState: ProtocolState, consumer: Chain, providerNode: Node, consumerAddr: ConsumerAddr): Result = { + // rule 1: validator A cannot assign consumer key K to consumer chain X + // if there is already a validator B (B!=A) using K on the provider + pure val provCurValSet = currentState.providerState.chainState.currentValidatorSet + if (provCurValSet.keys().exists(node => node != providerNode and node == consumerAddr)) { + Err("validator A cannot assign consumer key K to consumer chain X + if there is already a validator B (B!=A) using K on the provider") + } else { + // rule 2: validator A cannot assign consumer key K to consumer chain X if + // there is already a validator B using K on X + pure val valByConsAddr = currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()) + if (valByConsAddr.keys().contains(consumerAddr)) { + Err("consumer key is already in use on the consumer chain") } else { - val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( - (chain) => - if (consumersToTimeout.contains(chain)) { - TIMEDOUT - } else if (consumersToStop.contains(chain)) { - STOPPED + // this key can be assigned + + // get the old assigned key + pure val consKeyByVal = currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) + pure val p = if (consKeyByVal.keys().contains(providerNode)) { + // providerNode had previously assigned a consumer key + (consKeyByVal.get(providerNode), true) + } else { + (providerNode, false) + } + // the consumer address that was previously associated with the node + pure val oldConsAddr = p._1 + // whether the old address was explicitly assigned, or the default key + pure val prevAssigned = p._2 + + // set the old address for pruning, if it was assigned + pure val tmpState = if (prevAssigned) { + AppendConsumerAddrToPrune(currentState, oldConsAddr, consumer) + } else { + currentState + } + + // check whether the validator has positive power + pure val provValSet = currentState.providerState.chainState.currentValidatorSet + pure val provValPower = if (provValSet.keys().contains(providerNode)) provValSet.get(providerNode) else 0 + pure val consumersWithAddrAssignmentChangesInThisBlock = + if (provValPower > 0) { + // if the consumer has positive power, the relevant key assignment for the consumer changed + currentState.providerState.consumersWithAddrAssignmentChangesInThisBlock.union(Set(consumer)) } else { - currentConsumerStatusMap.get(chain) + // otherwise, the consumer doesn't need to know about the change, so no change + currentState.providerState.consumersWithAddrAssignmentChangesInThisBlock } + pure val tmpStateAfterKeyAssignmentReplacement = tmpState.with( + "providerState", tmpState.providerState.with( + "consumersWithAddrAssignmentChangesInThisBlock", consumersWithAddrAssignmentChangesInThisBlock + ) ) - (newConsumerStatusMap, "") - } - } - - // Returns the new ConsumerStatusMap according to the consumers to start. - // The second return is an error string: If it is not equal to "", - // it contains an error message, and the first return should be ignored. - pure def startConsumers( - currentConsumerStatusMap: Chain -> str, - consumersToStart: Set[Chain]): (Chain -> str, str) = { - val nonConsumers = currentConsumerStatusMap.keys().filter( - chain => currentConsumerStatusMap.get(chain) == NOT_CONSUMER - ) - // all consumers to start must be nonConsumers right now, otherwise we have an error - if (consumersToStart.exclude(nonConsumers).size() > 0) { - (currentConsumerStatusMap, "cannot start a consumer that is stopped or already a consumer") - } else { - val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( - (chain) => - if (consumersToStart.contains(chain)) { - RUNNING - } else { - currentConsumerStatusMap.get(chain) - } + + pure val newvalidatorToConsumerAddr = currentState.providerState.validatorToConsumerAddr.put( + consumer, + currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()).put( + providerNode, + consumerAddr + ) ) - (newConsumerStatusMap, "") - } - } - - pure def StartStopConsumers( - currentConsumerStatusMap: Chain -> str, - consumersToStart: Set[Chain], - consumersToStop: Set[Chain], - consumersToTimeout: Set[Chain] - ): (Chain -> str, str) = { - // check if any consumer is both started and stopped - if (consumersToStart.intersect(consumersToStop).size() > 0) { - (currentConsumerStatusMap, "Cannot start and stop a consumer at the same time") - } else { - val res1 = currentConsumerStatusMap.startConsumers(consumersToStart) - val newConsumerStatus = res1._1 - val err1 = res1._2 - val res2 = newConsumerStatus.stopConsumers(consumersToStop, consumersToTimeout) - val err2 = res2._2 - if (err1 != "") { - (currentConsumerStatusMap, err1) - } else if (err2 != "") { - (currentConsumerStatusMap, err2) - } else { - (res2._1, "") - } - } - } - - // Takes the currentValidatorSet and puts it as the newest set of the voting history - pure def enterCurValSetIntoBlock(chainState: ChainState): ChainState = { - chainState.with( - "votingPowerHistory", chainState.votingPowerHistory.prepend( - chainState.currentValidatorSet - ) - ) - } - - // Advances the timestamp in the chainState by timeAdvancement - pure def advanceTime(chainState: ChainState, timeAdvancement: Time): ChainState = - { - ...chainState, - lastTimestamp: chainState.runningTimestamp, - runningTimestamp: chainState.runningTimestamp + timeAdvancement, - } - - // common logic to update the chain state, used by both provider and consumers. - pure def endAndBeginBlockShared(chainState: ChainState, timeAdvancement: Time): ChainState = { - chainState.enterCurValSetIntoBlock().advanceTime(timeAdvancement) - } - - // returns the providerState with the following modifications: - // * sends VscPackets to all running consumers, using the provided timestamp as sending time - // * increments the runningVscId - // This should only be called when the provider chain is ending a block, - // and only when the running validator set is considered to have changed - // and there is a consumer to send a packet to. - pure def sendVscPackets(providerState: ProviderState, sendingTimestamp: Time): ProviderState = { - val newSentPacketsPerConsumer = ConsumerChains.mapBy( - (consumer) => - // if validator set changed and the consumer is running, send a packet - if (providerState.providerValidatorSetChangedInThisBlock and - isRunningConsumer(consumer, providerState)) { - List({ - id: providerState.runningVscId, - validatorSet: providerState.chainState.currentValidatorSet, - sendingTime: sendingTimestamp, - timeoutTime: sendingTimestamp + CcvTimeout.get(PROVIDER_CHAIN) - }) - } else { - List() - } - ) - val newOutstandingPacketsToConsumer = ConsumerChains.mapBy( - (consumer) => - providerState.outstandingPacketsToConsumer.get(consumer).concat( - newSentPacketsPerConsumer.get(consumer) - ) - ) - val newSentVscPackets = ConsumerChains.mapBy( - (consumer) => - providerState.sentVscPacketsToConsumer.get(consumer).concat( - newSentPacketsPerConsumer.get(consumer) + pure val newconsumerAddrToValidator = currentState.providerState.consumerAddrToValidator.put( + consumer, + currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()).put( + consumerAddr, + providerNode ) ) - { - ...providerState, - outstandingPacketsToConsumer: newOutstandingPacketsToConsumer, - sentVscPacketsToConsumer: newSentVscPackets, - providerValidatorSetChangedInThisBlock: false, - runningVscId: providerState.runningVscId + 1, - } - } - // receives a given packet (sent by the provider) on the consumer. The arguments are the consumer chain that is receiving the packet, and the packet itself. - // To receive a packet, modify the running validator set (not the one entered into the block yet, - // but the candidate that would be put into the block if it ended now) - // and store the maturation time for the packet. - pure def recvPacketOnConsumer(currentState: ProtocolState, receiver: Chain, packet: VscPacket): Result = { - if(not(isRunningConsumer(receiver, currentState.providerState))) { - Err("Receiver is not currently a consumer - must have 'running' status!") - } else { - // update the running validator set, but not the history yet, - // as that only happens when the next block is started - val currentConsumerState: ConsumerState = currentState.consumerStates.get(receiver) - val newConsumerState: ConsumerState = - { - ...currentConsumerState, - chainState: currentConsumerState.chainState.with( - "currentValidatorSet", packet.validatorSet - ), - maturationTimes: currentConsumerState.maturationTimes.append( - ( - packet, - currentConsumerState.chainState.runningTimestamp + UnbondingPeriodPerChain.get(receiver) - ) - ), - receivedVscPackets: currentConsumerState.receivedVscPackets.prepend(packet) - } - val newConsumerStates = currentState.consumerStates.set(receiver, newConsumerState) - val newState = currentState.with( - "consumerStates", newConsumerStates - ) - Ok(newState) - } - } - - // receives a given packet on the provider. The arguments are the consumer chain that sent the packet, and the packet itself. - // To receive a packet, add it to the list of received maturations. - pure def recvPacketOnProvider(currentState: ProtocolState, sender: Chain, packet: VscMaturedPacket): Result = { - if (not(isRunningConsumer(sender, currentState.providerState))) { - Err("Sender is not currently a consumer - must have 'running' status!") - } else if (currentState.providerState.sentVscPacketsToConsumer.get(sender).head().id != packet.id) { - // the packet is not the oldest sentVscPacket, something went wrong - Err("Received maturation is not for the oldest sentVscPacket") - } else { - val currentReceivedMaturations = currentState.providerState.receivedMaturations - val newReceivedMaturations = currentReceivedMaturations.union(Set(packet)) - val newProviderState = currentState.providerState.with( - "receivedMaturations", newReceivedMaturations - ) - // prune the sentVscPacket - val newSentVscPacket = currentState.providerState.sentVscPacketsToConsumer.get(sender).tail() - val newState = currentState.with( - "providerState", - {...newProviderState, - sentVscPacketsToConsumer: currentState.providerState.sentVscPacketsToConsumer.set(sender, newSentVscPacket) - } - ) - Ok(newState) - } - } - - // removes the oldest outstanding packet from the consumer. on-chain, this would happen when the packet is acknowledged. - // only the oldest packet can be removed, since we model ordered channels. - pure def removeOutstandingPacketFromConsumer(currentState: ProtocolState, sender: Chain): ProtocolState = { - val currentOutstandingPackets = currentState.consumerStates.get(sender).outstandingPacketsToProvider - val newOutstandingPackets = currentOutstandingPackets.tail() - val newConsumerState = currentState.consumerStates.get(sender).with( - "outstandingPacketsToProvider", newOutstandingPackets - ) - val newConsumerStates = currentState.consumerStates.set(sender, newConsumerState) - val newState = currentState.with( - "consumerStates", newConsumerStates - ) - newState - } - - // removes the oldest outstanding packet (to the given consumer) from the provider. - // on-chain, this would happen when the packet is acknowledged. - // only the oldest packet can be removed, since we model ordered channels. - pure def removeOutstandingPacketFromProvider(currentState: ProtocolState, receiver: Chain): ProtocolState = { - val currentOutstandingPackets = currentState.providerState.outstandingPacketsToConsumer.get(receiver) - val newOutstandingPackets = currentOutstandingPackets.tail() - val newProviderState = currentState.providerState.with( - "outstandingPacketsToConsumer", - currentState.providerState.outstandingPacketsToConsumer.set(receiver, newOutstandingPackets) - ) - val newState = currentState.with( - "providerState", newProviderState - ) - newState - } - - // Returns a ProtocolState where the current validator set on the provider is set to - // newValidatorSet. - pure def setProviderValidatorSet(currentState: ProtocolState, newValidatorSet: ValidatorSet): ProtocolState = { - pure val newChainState = currentState.providerState.chainState.with( - "currentValidatorSet", newValidatorSet - ) - currentState.with( - "providerState", - currentState.providerState.with( - "chainState", newChainState - ) - ) - } - - // Returns true if the given chain is currently a running consumer, false otherwise. - pure def isRunningConsumer(chain: Chain, providerState: ProviderState): bool = { - val status = providerState.consumerStatus.get(chain) - status == RUNNING - } - - // Returns the set of all consumer chains that currently have the status RUNNING. - pure def getRunningConsumers(providerState: ProviderState): Set[Chain] = { - providerState.consumerStatus.keys().filter( - chain => providerState.consumerStatus.get(chain) == RUNNING - ) - } - - // Returns the set of all consumer chains that currently have the status NOT_CONSUMER. - pure def getNonConsumers(providerState: ProviderState): Set[Chain] = { - providerState.consumerStatus.keys().filter( - chain => providerState.consumerStatus.get(chain) == NOT_CONSUMER - ) - } + pure val newProviderState = tmpStateAfterKeyAssignmentReplacement.providerState.with( + "validatorToConsumerAddr", newvalidatorToConsumerAddr + ).with( + "consumerAddrToValidator", newconsumerAddrToValidator + ) - // Returns whether the consumer has timed out due to the VscTimeout, and an error message. - // If the second return is not equal to "", the first return should be ignored. - // If it is equal to "", the first return will be true if the consumer has timed out and should be dropped, - // or false otherwise. - pure def TimeoutDueToVscTimeout(currentState: ProtocolState, consumer: Chain): (bool, str) = - // check for errors: the consumer is not running - if (not(isRunningConsumer(consumer, currentState.providerState))) { - (false, "Consumer is not currently a consumer - must have 'running' status!") - } else { - val providerState = currentState.providerState - val consumerState: ConsumerState = currentState.consumerStates.get(consumer) - - // has a packet been sent on the provider more than VscTimeout ago, but we have not received an answer since then? - val sentVscPacketsToConsumer = providerState.sentVscPacketsToConsumer.get(consumer) - if(sentVscPacketsToConsumer.length() > 0) { - val oldestSentVscPacket = sentVscPacketsToConsumer.head() // if length is 0, this is undefined, but we check for this before we use it - if(oldestSentVscPacket.sendingTime + VscTimeout < providerState.chainState.runningTimestamp) { - (true, "") - } else { - // no timeout yet, it has not been VscTimeout since that packet was sent - (false, "") - } - } else { - // no packet has been sent yet, so no timeout - (false, "") + Ok( + tmpStateAfterKeyAssignmentReplacement.with( + "providerState", newProviderState + ) + ) } } + } // =================== // ASSUMPTIONS ON MODEL PARAMETERS diff --git a/tests/mbt/model/ccv_boundeddrift.qnt b/tests/mbt/model/ccv_boundeddrift.qnt index 21a53074c0..f99f92d350 100644 --- a/tests/mbt/model/ccv_boundeddrift.qnt +++ b/tests/mbt/model/ccv_boundeddrift.qnt @@ -1,9 +1,11 @@ module ccv_boundeddrift { import ccv_model.* from "ccv_model" import ccv_types as Ccvt from "ccv" + import ccv_utils.* from "ccv_utils" import ccv from "ccv" import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" + import ccv_pss_model.* from "ccv_pss_model" // The boundeddrift module has its own step function. @@ -32,7 +34,7 @@ module ccv_boundeddrift { // Given the name of a chain, gets a set with the chain states of all other chains. def GetOtherChainStates(advancingChain: Ccvt::Chain): Set[Ccvt::ChainState] = - val runCons = ccv::getRunningConsumers(currentState.providerState) + val runCons = getRunningConsumers(currentState.providerState) if (advancingChain == Ccvt::PROVIDER_CHAIN) { runCons.map(c => currentState.consumerStates.get(c).chainState) } else { @@ -48,7 +50,7 @@ module ccv_boundeddrift { } def GetRunningChainStates(): Set[Ccvt::ChainState] = - val runCons = ccv::getRunningConsumers(currentState.providerState) + val runCons = getRunningConsumers(currentState.providerState) val consumerChainStates = runCons.map(c => currentState.consumerStates.get(c).chainState) consumerChainStates.union(Set(currentState.providerState.chainState)) @@ -59,19 +61,22 @@ module ccv_boundeddrift { stepCommon, // allow actions that do not influence time // advance a block for a consumer - all { - runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense - nondet chain = runningConsumers.oneOf() - val maxAdv = findMaxTimeAdvancement(GetChainState(chain), GetOtherChainStates(chain), maxDrift) - val possibleAdvancements = timeAdvancements.filter(t => t <= maxAdv) - all { - possibleAdvancements.size() > 0, // ensure there is a possible advancement, otherwise this action does not make sense - nondet timeAdvancement = possibleAdvancements.oneOf() - EndAndBeginBlockForConsumer(chain, timeAdvancement), - } - }, + stepBoundedDriftConsumer, // advance a block for the provider + stepBoundedDriftProvider + } + + action stepBoundedDriftProvider: bool = { + stepBoundedDriftProvider_helper(allFullConsumers) + } + + action stepBoundedDriftProviderPSS: bool = { + stepBoundedDriftProvider_helper(variousPossibleTopN) + } + + // As an argument, takes a function that, when invoked, gives a top N value to use for a new consumer chain. + action stepBoundedDriftProvider_helper(topNOracle: Set[int]): bool = { val maxAdv = findMaxTimeAdvancement(GetChainState(Ccvt::PROVIDER_CHAIN), GetOtherChainStates(Ccvt::PROVIDER_CHAIN), maxDrift) val possibleAdvancements = timeAdvancements.filter(t => t <= maxAdv) all { @@ -79,14 +84,42 @@ module ccv_boundeddrift { // advance a block for the provider val consumerStatus = currentState.providerState.consumerStatus nondet consumersToStart = oneOf(nonConsumers.powerset()) + nondet topN = oneOf(topNOracle) + nondet consumerAdditions = consumersToStart.map(c => Ccvt::NewTopNConsumer(c, topN)) // make it so we stop consumers only with small likelihood: - nondet stopConsumers = oneOf(1.to(100)) - nondet consumersToStop = if (stopConsumers <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set() + nondet stopConsumersRand = oneOf(1.to(100)) + nondet consumersToStop = if (stopConsumersRand <= consumerStopChance) oneOf(runningConsumers.powerset()) else Set() nondet timeAdvancement = oneOf(possibleAdvancements) - EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), + EndAndBeginBlockForProvider(timeAdvancement, consumerAdditions, consumersToStop), } } + action stepBoundedDriftConsumer = all { + runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense + nondet chain = runningConsumers.oneOf() + val maxAdv = findMaxTimeAdvancement(GetChainState(chain), GetOtherChainStates(chain), maxDrift) + val possibleAdvancements = timeAdvancements.filter(t => t <= maxAdv) + all { + possibleAdvancements.size() > 0, // ensure there is a possible advancement, otherwise this action does not make sense + nondet timeAdvancement = possibleAdvancements.oneOf() + EndAndBeginBlockForConsumer(chain, timeAdvancement), + } + } + + action stepBoundedDriftKeyAssignment = any { + stepBoundedDrift, + nondetKeyAssignment, + } + + action stepBoundedDriftKeyAndPSS = any { + stepCommon, + stepBoundedDriftProviderPSS, + stepBoundedDriftConsumer, + nondetKeyAssignment, + StepOptIn, + StepOptOut, + } + // INVARIANT // The maxDrift between chains is never exceeded. // This *should* be ensured by the step function. diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt index fba4ddea6c..dc6cd10188 100644 --- a/tests/mbt/model/ccv_model.qnt +++ b/tests/mbt/model/ccv_model.qnt @@ -4,6 +4,7 @@ module ccv_model { import ccv_types.* from "./ccv" import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" + import ccv_utils.* from "./ccv_utils" pure val consumerChainList = List("consumer1", "consumer2", "consumer3") pure val consumerChains = consumerChainList.toSet() @@ -14,6 +15,8 @@ module ccv_model { pure val ccvTimeouts = chains.mapBy(chain => 3 * Week) pure val nodes = Set("node1", "node2", "node3", "node4", "node5", "node6", "node7", "node8", "node9", "node10") + // possible consumer addresses that nodes can assign their key to + pure val consumerAddresses = Set("consAddr1", "consAddr2", "consAddr3", "consAddr4", "consAddr5", "consAddr6", "consAddr7", "consAddr8", "consAddr9", "consAddr10") pure val InitialValidatorSet = nodes.mapBy(node => 100) import ccv( @@ -31,6 +34,7 @@ module ccv_model { TrustingPeriodPerChain: Chain -> Time, ConsumerChains: Set[Chain], Nodes: Set[Node], + ConsumerAddresses: Set[ConsumerAddr], InitialValidatorSet: Node -> int, } @@ -42,7 +46,13 @@ module ccv_model { var currentState: ProtocolState - // a type storing the parameters used in actions. + // a type storing the parameters used in actions, + // as well as return values that are not visible from the state, + // i.e. errors. + // Note that whether an error is returned, + // or whether the action is simply not possible when an error occurs, is + // a design choice that is different for each action, + // or can depend on the type of error. // this is used in the trace to store // the name of the last action, plus the parameters we passed to it. // Note: This type holds ALL parameters that are used in ANY action, @@ -52,10 +62,12 @@ module ccv_model { kind: str, consumerChain: Chain, timeAdvancement: Time, - consumersToStart: Set[Chain], + consumersToStart: Set[ConsumerAdditionMsg], consumersToStop: Set[Chain], validator: Node, changeAmount: int, + consumerAddr: ConsumerAddr, + expectedError: str, // if the action returns an error, it goes here. } @@ -70,7 +82,7 @@ module ccv_model { // otherwise connections will break down. pure val timeAdvancements = Set(1 * Second, 1 * Day, 1 * Week - 1 * Hour) - pure def emptyAction = + pure def emptyAction: Action = { kind: "", consumerChain: "", @@ -79,6 +91,8 @@ module ccv_model { consumersToStop: Set(), validator: "", changeAmount: 0, + consumerAddr: "", + expectedError: "", } @@ -106,6 +120,8 @@ module ccv_model { ).with( "currentValidatorSet", InitialValidatorSet ) + ).with( + "keyAssignedValSetHistory", ConsumerChains.mapBy(chain => List(InitialValidatorSet)) ) currentState' = { providerState: providerStateWithConsumers, @@ -120,6 +136,7 @@ module ccv_model { Nodes: nodes, InitialValidatorSet: InitialValidatorSet, TrustingPeriodPerChain: TrustingPeriodPerChain, + ConsumerAddresses: consumerAddresses, } } @@ -158,7 +175,7 @@ module ccv_model { action EndAndBeginBlockForProvider( timeAdvancement: Time, - consumersToStart: Set[Chain], + consumersToStart: Set[ConsumerAdditionMsg], consumersToStop: Set[Chain]): bool = val result = endAndBeginBlockForProvider(currentState, timeAdvancement, consumersToStart, consumersToStop) all { @@ -179,6 +196,7 @@ module ccv_model { params' = params, } + // stepCommon is the core functionality of steps that does not have anything to do with time. action stepCommon = any { nondet node = oneOf(nodes) @@ -218,17 +236,14 @@ module ccv_model { val consumerStatus = currentState.providerState.consumerStatus nondet consumersToStart = oneOf(nonConsumers.powerset()) + val consumerAdditions = consumersToStart.map(chain => NewFullConsumer(chain)) nondet consumersToStop = oneOf(runningConsumers.powerset()) nondet timeAdvancement = oneOf(timeAdvancements) - EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), + EndAndBeginBlockForProvider(timeAdvancement, consumerAdditions, consumersToStop), stepCommon } - // ================== - // UTILITY FUNCTIONS - // ================== - pure def oldest(packets: Set[VscPacket]): VscPacket = val newestPossiblePacket: VscPacket = { id: 0, @@ -290,9 +305,11 @@ module ccv_model { // Every validator set on any consumer chain MUST either be or have been // a validator set on the provider chain. val ValidatorSetHasExistedInv = - runningConsumers.forall(chain => + runningConsumers.forall(chain => // for all running consumers currentState.consumerStates.get(chain).chainState.votingPowerHistory.toSet().forall( + // go through all its historical and current validator sets validatorSet => providerValidatorHistory.toSet().contains(validatorSet) + // and check that they are also historical or current validator sets on the provider ) ) @@ -310,10 +327,6 @@ module ccv_model { consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists( packet => packet.validatorSet == providerValSetInCurBlock ) - // or the consumer was just started, which we detect by the consumer having a timestamp of 0 - // and the consumer having the validator set that was just sent in the block - or - (currentState.consumerStates.get(consumer).chainState.lastTimestamp == 0 and currentState.consumerStates.get(consumer).chainState.currentValidatorSet == providerValSetInCurBlock) ) // Every consumer chain receives the same sequence of @@ -360,8 +373,11 @@ module ccv_model { val lastTimeAdvancement = trace[trace.length()-1].timeAdvancement val lastBlockTime = currentState.consumerStates.get(ConsumerWithPotentialMaturations).chainState.lastTimestamp - lastTimeAdvancement val MatureOnTimeInv = + // if a consumer ended a block MaturationPrecondition implies + // then all matured packets need to have been processed and removed from the packets + // waiting to mature currentState.consumerStates.get(ConsumerWithPotentialMaturations).maturationTimes.toSet().forall( pair => val maturationTime = pair._2 @@ -378,7 +394,7 @@ module ccv_model { val EventuallyMatureOnProviderInv = runningConsumers.forall( consumer => { - val sentPackets = currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet() + val sentPackets = currentState.providerState.sentVscPacketsToConsumer.getOrElse(consumer, List()).toSet() sentPackets.forall( packet => // consumer still has time to respond @@ -390,6 +406,7 @@ module ccv_model { } ) + // ================= // SANITY CHECKS // ================= @@ -421,7 +438,7 @@ module ccv_model { val CanSendVscPackets = not(ConsumerChains.exists( consumer => - currentState.providerState.outstandingPacketsToConsumer.get(consumer).length() > 0 + currentState.providerState.outstandingPacketsToConsumer.getOrElse(consumer, List()).length() > 0 )) val CanReceiveVscPackets = @@ -482,14 +499,14 @@ module ccv_model { // the validator set has changed assert(currentState.providerState.chainState.currentValidatorSet == InitialValidatorSet.put("node1", 150)), // start consumer1 - EndAndBeginBlockForProvider(1 * Second, Set("consumer1"), Set()) + EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer1")), Set()) }) .then( all { // consumer1 was started assert(currentState.providerState.consumerStatus.get("consumer1") == RUNNING), // but no packet was sent to consumer 1 - assert(currentState.providerState.outstandingPacketsToConsumer.get("consumer1").length() == 0), + assert(currentState.providerState.outstandingPacketsToConsumer.getOrElse("consumer1", List()).length() == 0), // the validator set on the provider was entered into the history assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet.put("node1", 150), InitialValidatorSet)), // change voting power on provider again @@ -559,7 +576,7 @@ module ccv_model { run SameVscPacketsManualTest = init.then( // start all consumers except for consumer3 - EndAndBeginBlockForProvider(1 * Second, Set("consumer1", "consumer2"), Set()) + EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer1"), NewFullConsumer("consumer2")), Set()) ).then( // change voting power VotingPowerChange("node1", 50) @@ -574,7 +591,7 @@ module ccv_model { DeliverVscPacket("consumer2") ).then( // start consumer3 - EndAndBeginBlockForProvider(1 * Second, Set("consumer3"), Set()) + EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer3")), Set()) ).then( // do another voting power change VotingPowerChange("node2", 50) @@ -605,7 +622,7 @@ module ccv_model { init .then( // start all consumer chains - EndAndBeginBlockForProvider(1 * Second, ConsumerChains, Set()) + EndAndBeginBlockForProvider(1 * Second, ConsumerChains.map(c => NewFullConsumer(c)), Set()) ) .then( // change voting power @@ -632,4 +649,270 @@ module ccv_model { VotingPowerChange("node1", 50) // action needs to be there but does not matter what it is } ) + + + // ===== KEY ASSIGNMENT ======= + action stepKeyAssignment = + any { + step, + nondetKeyAssignment, + } + + action nondetKeyAssignment = + all { + runningConsumers.size() > 0, + nondet node = oneOf(nodes) + nondet consumerAddr = oneOf(consumerAddresses) + nondet consumer = oneOf(runningConsumers) + KeyAssignment(consumer, node, consumerAddr), + } + + action KeyAssignment( + chain: Chain, + validator: Node, + consumerAddr: ConsumerAddr + ): bool = + val result = assignConsumerKey(currentState, chain, validator, consumerAddr) + all { + hasError(result) == false, + currentState' = result.newState, + trace' = trace.append( + {...emptyAction, + kind: "KeyAssignment", + consumerChain: chain, + validator: validator, + consumerAddr: consumerAddr + } + ), + params' = params, + } + + // invariants for key assignment - some invariants are in addition, some need to be adjusted from the original model + + // Every validator set on any consumer chain MUST either be or have been + // a validator set on the provider chain, under the key assignment at the time. + val providerKeyAssignedValSetHistory = currentState.providerState.keyAssignedValSetHistory + + val ValidatorSetHasExistedKeyAssignmentInv = + runningConsumers.forall(chain => // for every running consumer + currentState.consumerStates.get(chain).chainState.votingPowerHistory.toSet().forall( + // for every validator set the consumer ever had + validatorSet => providerKeyAssignedValSetHistory.getOrElse(chain, List()).toSet().exists( + // that validator set needs to also have existed on the provider + provValSet => removeZeroPowers(provValSet) == removeZeroPowers(validatorSet) + ) + ) + ) + + // Any update in the power of a validator on the provider + // MUST be present in a ValidatorSetChangePacket that is sent to all registered consumer chains, + // and the key assignment of each validator should be applied in that VSCPacket. + val ValidatorUpdatesArePropagatedKeyAssignmentInv = + // when the provider has just entered a validator set into a block... + ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock + implies + val providerValSetInCurBlock = providerValidatorHistory.head() + // ... for each consumer that is running then ... + runningConsumers.forall( + // ...the validator set under key assignment is in a sent packet... + val providerState = currentState.providerState + consumer => providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists( + packet => + packet.validatorSet == + applyKeyAssignmentToValSet(providerState, consumer, providerValSetInCurBlock) + ) + ) + + // Every consumer chain receives the same sequence of + // ValidatorSetChangePackets in the same order. + // NOTE: since not all consumer chains are running all the time, + // we need a slightly weaker invariant: + // For consumer chains c1, c2, if both c1 and c2 received a packet p1 sent at t1 and a packet p2 sent at t2, + // then both have received ALL packets that were sent between t1 and t2. + val SameVscPacketsKeyAssignmentInv = + runningConsumers.forall( + consumer1 => runningConsumers.forall( + consumer2 => { + val packets1 = currentState.consumerStates.get(consumer1).receivedVscPackets + val packets2 = currentState.consumerStates.get(consumer2).receivedVscPackets + val commonPackets = packets1.toSet().intersect(packets2.toSet()) + if (commonPackets.size() == 0) { + true // they don't share any packets, so nothing to check + } else { + val newestCommonPacket = newest(commonPackets) + val oldestCommonPacket = oldest(commonPackets) + // get all packets sent between the oldest and newest common packet + val packetsBetween1 = packets1.select( + packet => packet.sendingTime >= oldestCommonPacket.sendingTime and packet.sendingTime <= newestCommonPacket.sendingTime + ) + val packetsBetween2 = packets2.select( + packet => packet.sendingTime >= oldestCommonPacket.sendingTime and packet.sendingTime <= newestCommonPacket.sendingTime + ) + + // revert key assignments + val packetsBetween1noKeyAssignment = packetsBetween1.foldl( + List(), + (acc, packet) => + acc.concat(List({...packet, + validatorSet: revertKeyAssignment( + currentState.providerState.keyAssignmentsForVSCPackets + .getOrElse(packet.id, Map()) + .getOrElse(consumer1, Map()), + packet.validatorSet) + })) + ) + + val packetsBetween2noKeyAssignment = packetsBetween2.foldl( + List(), (acc, packet) => + acc.concat(List({...packet, + validatorSet: revertKeyAssignment( + currentState.providerState.keyAssignmentsForVSCPackets + .getOrElse(packet.id, Map()) + .getOrElse(consumer2, Map()), + packet.validatorSet) + })) + ) + // check that the packets between the common packets are equal + // when key assignment is reversed + packetsBetween1noKeyAssignment == packetsBetween2noKeyAssignment + } + } + ) + ) + + + // Rules for key assignment: + val KeyAssignmentRulesInv = + NoProviderReuse and NoDuplicationOnSameConsumer + + // validator A cannot assign consumer key K to consumer chain X if there is already a validator B (B!=A) using K on the provider + val NoProviderReuse = + consumerChains.forall( + consumer => + val valConsPk = currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) + valConsPk.keys().forall( + node => + val consAddr = valConsPk.get(node) + // either the key is the nodes key itself (B == A) + consAddr == node or + // or the consAddr must not be a validator on the provider + not(currentState.providerState.chainState.currentValidatorSet.keys().contains(consAddr)) + ) + ) + + // validator A cannot assign consumer key K to consumer chain X if there is already a validator B using K on X + val NoDuplicationOnSameConsumer = + consumerChains.forall( + consumer => + val valConsPk = currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) + valConsPk.keys().forall( + node => + val consAddr = valConsPk.get(node) + // no other node may use consAddr + not(valConsPk.keys().exists( + otherNode => otherNode != node and valConsPk.get(otherNode) == consAddr + )) + ) + ) + + // sanity checks + val CanAssignConsumerKey = + not(consumerChains.exists( + consumer => + currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()).keys().size() > 0 + )) + + val CanHaveConsumerAddresses = + not(consumerChains.exists( + consumer => + currentState.consumerStates.get(consumer).chainState.currentValidatorSet.keys().exists( + addr => addr.in(consumerAddresses) + ) + )) + + // == tests for key assignment == + run KeyAssignmentTest = + init + .then( + // start all consumer chains + EndAndBeginBlockForProvider(1 * Second, consumerChains.map(c => NewFullConsumer(c)), Set()) + ) + .then( + // node 1 assigns a key on consumer1 + KeyAssignment("consumer1", "node1", "consAddr1") + ) + .then( + // end and begin block to make sure the key assignment is processed and the packet is sent + EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + ) + .then( + // receive the packet on the consumer + DeliverVscPacket("consumer1") + ) + .then( + // end and begin block to make sure the packet is processed + EndAndBeginBlockForConsumer("consumer1", 1 * Second) + ) + .then( + all { + // the key should be present in the valset on the consumer, and the node itself should not + assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet.getOrElse("node1", 0) == 0), + assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet.get("consAddr1") == 100), + // try some key assignments that should fail/succeed without comitting to state + val res = assignConsumerKey(currentState, "consumer1", "node1", "consAddr1") + // fail - key already assigned (even if it is the same node) + assert(hasError(res)), + val res2 = assignConsumerKey(currentState, "consumer1", "node2", "consAddr1") + // fail - key assigned to other node + assert(hasError(res2)), + val res3 = assignConsumerKey(currentState, "consumer2", "node2", "consAddr1") + // ok - may reuse the key on a different consumer + assert(not(hasError(res3))), + val res4 = assignConsumerKey(currentState, "consumer1", "node2", "node1") + // fail - may not reuse a provider key of a different val + assert(hasError(res4)), + val res5 = assignConsumerKey(currentState, "consumer1", "node1", "consAddr2") + // ok - assigning unused key to node + assert(not(hasError(res5))), + val res6 = assignConsumerKey(currentState, "consumer1", "node1", "node1") + // ok - going back to original key + assert(not(hasError(res6))), + // mature the vsc packet on the consumer + EndAndBeginBlockForConsumer("consumer1", unbondingPeriods.get("consumer1") + 1 * Hour) + } + ) + .then( + // End a block to send the maturation + EndAndBeginBlockForConsumer("consumer1", 1 * Second) + ) + .then( + // deliver the vsc matured packet to the provider + DeliverVscMaturedPacket("consumer1") + ) + .then( + // the old key should have been pruned + all { + // check that pruning has been performed nicely + assert(currentState.providerState.consumerAddrToValidator.get("consumer1").get("consAddr1") == "node1"), + assert(currentState.providerState.consumerAddrsToPrune.get("consumer1").getOrElse(0, List()).length() == 0), + // action does not matter + VotingPowerChange("node1", 50) + } + ) + + run KeyAssignmentInvTest = + init.then( + KeyAssignment("consumer3", "node3", "consAddr6") + ).then( + VotingPowerChange("node1", 50) + ) + .then( + EndAndBeginBlockForProvider(1 * Second, Set(NewFullConsumer("consumer1"), NewFullConsumer("consumer2")), Set()) + ).then( + all { + ValidatorSetHasExistedKeyAssignmentInv, + // action doesn't matter + VotingPowerChange("node1", 50) + } + ) } \ No newline at end of file diff --git a/tests/mbt/model/ccv_pss.qnt b/tests/mbt/model/ccv_pss.qnt new file mode 100644 index 0000000000..4759fe6b34 --- /dev/null +++ b/tests/mbt/model/ccv_pss.qnt @@ -0,0 +1,157 @@ +// This module contains logic for PSS (Partial Set Security). +// PSS is a variant/extension of CCV that +// allows for only a subset of the validator set +// to secure a consumer chain. +// Not all logic related to PSS is inside this module, as some logic is +// too tightly coupled with the core CCV logic, +// which is instead found in ccv.qnt +module ccv_pss { + import ccv_types.* from "./ccv" + import extraSpells.* from "./libraries/extraSpells" + import ccv_utils.* from "./ccv_utils" + + // Given a base validator set, an N for a top N chain, and a set of validators that have opted in to the chain, + // returns the validator set that should be sent to the chain. + // Assumes that the value for N is valid. + pure def GetPSSValidatorSet(providerState: ProviderState, origValSet: ValidatorSet, consumer: Chain): ValidatorSet = { + pure val optedInVals = providerState.optedInVals.getOrElse(consumer, Set()) + GetPSSValidatorSet_helper(origValSet, optedInVals) + } + + pure def GetPSSValidatorSet_helper(origValSet: ValidatorSet, optedInVals: Set[Node]): ValidatorSet = { + origValSet.mapFilter(v => optedInVals.contains(v)) + } + + // Given a validator set and N, returns the top N% of validators by power. + // Note that in the edge case of multiple validators having the same power, + // this will always include all validators with the same power as the lowest top N validator. + pure def GetTopNVals(origValSet: ValidatorSet, N: int): Set[Node] = { + // == sort validators by power == + // define a comparator that compares validators by power + pure def powerCompare(a: Node, b: Node): Ordering = { + pure val powA = origValSet.get(a) + pure val powB = origValSet.get(b) + intCompare(powB, powA) + } + // get a sorted list of validators by power + pure val sortedVals = origValSet.keys().toSortedList(powerCompare) + + // == compute the threshold of how much power the top N have == + pure val totalPower = origValSet.mapValuesSum() + pure val topNPower = totalPower * N / 100 + + // == construct the validator set by going through the sorted vals == + pure val res = sortedVals.foldl( + // accumulator carries 4 values: + // * set of vals in top N (starts with empty set) + // * total power added so far (starts with 0) + // * whether we should add the next validator if it has the same power as the previous one, + // regardless of total power (starts with false) + // * the power of the last validator added (starts with 0) + (Set(), 0, false, 0), + (acc, validator) => + pure val curValSet = acc._1 + pure val accPower = acc._2 + pure val shouldAddSamePow = acc._3 + pure val lastPow = acc._4 + + pure val validatorPower = origValSet.get(validator) + if (validatorPower == lastPow and shouldAddSamePow) { + // we should add the validator because it has the same power as the previous one, + // and we add regardless of total power because we need to include all + // vals with the same power if we include one of them + pure val newAccPower = accPower + validatorPower + (curValSet.union(Set(validator)), newAccPower, true, validatorPower) + } else if (validatorPower > 0 and accPower < topNPower) { + // if we don't have enough power yet, add the validator to the set + pure val newAccPower = accPower + validatorPower + (curValSet.union(Set(validator)), newAccPower, true, validatorPower) + } else { + // if we have enough power and we also are done adding + // all validators with the same power as the lowest top N validator, + // don't add them + (curValSet, accPower, false, 0) + } + ) + res._1 + } + + // Opts a validator in for a consumer chain the provider. + // Possible before the consumer chain starts running, + // and will then be applied when the consumer chain starts running. + pure def OptIn(currentState: ProtocolState, consumer: Chain, validator: Node): Result = { + pure val optedInVals = currentState.providerState.optedInVals.get(consumer) + pure val newOptedInVals = optedInVals.union(Set(validator)) + Ok({ + ...currentState, + providerState: { + ...currentState.providerState, + optedInVals: currentState.providerState.optedInVals.put(consumer, newOptedInVals) + } + }) + } + + // Returns true if the given validator is in the top N for the given consumer chain, + // and false otherwise. + pure def IsTopN(currentState: ProtocolState, validator: Node, consumer: Chain): bool = { + val proviValSet = currentState.providerState.chainState.currentValidatorSet + val N = currentState.providerState.topNByConsumer.get(consumer) + + val topNValSet = GetTopNVals(proviValSet, N) + + topNValSet.contains(validator) + } + + // Returns true if the given validator has opted in to the given consumer chain, + pure def IsOptedIn(currentState: ProtocolState, validator: Node, consumer: Chain): bool = { + currentState.providerState.optedInVals.getOrElse(consumer, Set()).contains(validator) + } + + // Opts a validator out. Safe to call before the consumer chain even runs. + // Will not stop the validator set from being forced to validate when in the top N. + // Validators that are in the top N will not be able to opt out, and + // an error will be returned. + // Similarly, if the validator is not opted in, an error will be returned. + pure def OptOut(currentState: ProtocolState, consumer: Chain, validator: Node): Result = { + if (currentState.IsTopN(validator, consumer)) { + Err("Cannot opt out a validator that is in the top N") + } else if (not(currentState.IsOptedIn(validator, consumer))) { + Err("Cannot opt out a validator that is not opted in") + } else { + pure val optedInVals = currentState.providerState.optedInVals.get(consumer) + pure val newOptedInVals = optedInVals.exclude(Set(validator)) + Ok({ + ...currentState, + providerState: { + ...currentState.providerState, + optedInVals: currentState.providerState.optedInVals.put(consumer, newOptedInVals) + } + }) + } + } + + // Runs the PSS logic that needs to run on endblock. + // Concretely, this will forcefully opt in all validators that are in the top N + // for each chain. + pure def endBlockPSS(providerState: ProviderState): ProviderState = { + val runningConsumers = providerState.getRunningConsumers() + runningConsumers.fold( + providerState, + (acc, consumer) => endBlockPSS_helper(acc, consumer) + ) + } + + // Runs the PSS logic for a single consumer. + // Should only be run for running chains. + pure def endBlockPSS_helper(providerState: ProviderState, consumer: Chain): ProviderState = { + val proviValSet = providerState.chainState.currentValidatorSet + val topNVals = GetTopNVals(proviValSet, providerState.topNByConsumer.get(consumer)) + val prevOptedInVals = providerState.optedInVals.getOrElse(consumer, Set()) + // opt in all the top N validators, i.e. union the top N vals with the previous opted in vals + val newOptedInVals = providerState.optedInVals.put(consumer, prevOptedInVals.union(topNVals)) + { + ...providerState, + optedInVals: newOptedInVals + } + } +} \ No newline at end of file diff --git a/tests/mbt/model/ccv_pss_model.qnt b/tests/mbt/model/ccv_pss_model.qnt new file mode 100644 index 0000000000..76c4873b43 --- /dev/null +++ b/tests/mbt/model/ccv_pss_model.qnt @@ -0,0 +1,113 @@ +module ccv_pss_model { + import ccv_types.* from "./ccv" + import ccv_model.* from "./ccv_model" + import ccv_pss.* from "./ccv_pss" + import extraSpells.* from "./libraries/extraSpells" + + action StepOptIn(): bool = { + all { + runningConsumers.size() > 0, + nondet consumer = oneOf(runningConsumers) + nondet validator = oneOf(nodes) + OptIn_Deterministic(consumer, validator) + } + } + + action OptIn_Deterministic(consumer: Chain, validator: Node): bool = { + val res = OptIn(currentState, consumer, validator) + all { + currentState' = res.newState, + trace' = trace.append( + { + ...emptyAction, + kind: "OptIn", + consumerChain: consumer, + validator: validator, + expectedError: res.error + } + ), + params' = params, + } + } + + action StepOptOut(): bool = { + all { + runningConsumers.size() > 0, + nondet consumer = oneOf(runningConsumers) + nondet validator = oneOf(nodes) + OptOut_Deterministic(consumer, validator) + } + } + + action OptOut_Deterministic(consumer: Chain, validator: Node): bool = { + val res = OptOut(currentState, consumer, validator) + all { + currentState' = res.newState, + trace' = trace.append( + { + ...emptyAction, + kind: "OptOut", + consumerChain: consumer, + validator: validator, + expectedError: res.error + } + ), + params' = params, + } + } + + // Different sets of possible values for the topN parameter. + val allFullConsumers: Set[int] = Set(100) + val allOptIn: Set[int] = Set(0) + // only choose a few values for top N here to not make the "edge cases" of 0 and 100 too unlikely + val variousPossibleTopN: Set[int] = Set(0, 50, 70, 80, 90, 100) + + // INVARIANTS + + // For a consumer chain with a given top N value, + // the total VP on the consumer is at least N% of the total VP of some historical val set on the provider. + val AtLeastTopNPower: bool = + runningConsumers.forall(consumer => { + val topN = currentState.providerState.topNByConsumer.get(consumer) + val totalPowerConsu = currentState.consumerStates.get(consumer).chainState.currentValidatorSet.mapValuesSum() + currentState.providerState.chainState.votingPowerHistory.toSet().exists( + valSet => { + val totalPowerProvi = valSet.mapValuesSum() + + totalPowerConsu >= totalPowerProvi * topN / 100 + } + ) + }) + + // SANITY CHECKS + + val CanOptIn = { + not( + trace[length(trace)-1].kind == "OptIn" + and + trace[length(trace)-1].expectedError == "" + ) + } + + val CanOptOut = { + not( + trace[length(trace)-1].kind == "OptOut" + and + trace[length(trace)-1].expectedError == "" + ) + } + + val CanFailOptOut = { + not( + trace[length(trace)-1].kind == "OptOut" + and + trace[length(trace)-1].expectedError != "" + ) + } + + val CanHaveOptIn = { + currentState.providerState.topNByConsumer.keys().exists(consumer => { + currentState.providerState.topNByConsumer.get(consumer) != 100 + }) + } +} \ No newline at end of file diff --git a/tests/mbt/model/ccv_pss_test.qnt b/tests/mbt/model/ccv_pss_test.qnt new file mode 100644 index 0000000000..2a84f6dbd4 --- /dev/null +++ b/tests/mbt/model/ccv_pss_test.qnt @@ -0,0 +1,34 @@ +// This module contains logic for PSS (Partial Set Security). +// PSS is a variant/extension of CCV that +// allows for only a subset of the validator set +// to secure a consumer chain. +// Not all logic related to PSS is inside this module, as some logic is +// too tightly coupled with the core CCV logic, +// which is instead found in ccv.qnt +module ccv_pss_test { + import ccv_types.* from "./ccv" + import extraSpells.* from "./libraries/extraSpells" + import ccv_utils.* from "./ccv_utils" + import ccv_pss.* from "./ccv_pss" + + run TopNTest = + val valSet = + Map("d" -> 25, "c1" -> 15, "c" -> 15, "b2" -> 10, "b1" -> 10, "b" -> 10, "a2" -> 5, "a1" -> 5, "a" -> 5) + // total power: 5*3 + 10*3 + 15*2 + 25 = 100 + all + { + assert(GetTopNVals(valSet, 0) == Set()), + assert(GetTopNVals(valSet, 1) == Set("d")), + assert(GetTopNVals(valSet, 10) == Set("d")), + assert(GetTopNVals(valSet, 25) == Set("d")), + // if one validator with a power is included, all validators with that power need to be included + assert(GetTopNVals(valSet, 26) == Set("d", "c1", "c")), + assert(GetTopNVals(valSet, 45) == Set("d", "c1", "c")), + assert(GetTopNVals(valSet, 55) == Set("d", "c1", "c")), + assert(GetTopNVals(valSet, 56) == Set("d", "c1", "c", "b2", "b1", "b")), + assert(GetTopNVals(valSet, 85) == Set("d", "c1", "c", "b2", "b1", "b")), + assert(GetTopNVals(valSet, 86) == valSet.keys()), + assert(GetTopNVals(valSet, 95) == valSet.keys()), + assert(GetTopNVals(valSet, 100) == valSet.keys()), + } +} \ No newline at end of file diff --git a/tests/mbt/model/ccv_sync.qnt b/tests/mbt/model/ccv_sync.qnt index d828b88a76..8af76693b8 100644 --- a/tests/mbt/model/ccv_sync.qnt +++ b/tests/mbt/model/ccv_sync.qnt @@ -25,7 +25,7 @@ module ccv_sync { action initSync = all { init.then( - EndAndBeginBlockForProvider(1 * Second, consumerChains, Set()) + EndAndBeginBlockForProvider(1 * Second, consumerChains.map(c => ccvt::NewFullConsumer(c)), Set()) ), QueuedChainsToEndBlock' = consumerChainList.foldl( List(), diff --git a/tests/mbt/model/ccv_test.qnt b/tests/mbt/model/ccv_test.qnt index 4dae28ec03..1aeb50067d 100644 --- a/tests/mbt/model/ccv_test.qnt +++ b/tests/mbt/model/ccv_test.qnt @@ -5,6 +5,7 @@ module ccv_test { import ccv_types.* from "./ccv" import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" + import ccv_utils.* from "./ccv_utils" pure val consumerChains = Set("sender", "receiver") pure val chains = consumerChains.union(Set(PROVIDER_CHAIN)) @@ -241,15 +242,15 @@ module ccv_test { "chain3" -> STOPPED ) val res = StartStopConsumers( - currentConsumerStatusMap, - Set("chain1"), + GetEmptyProviderState.with("consumerStatus", currentConsumerStatusMap), + Set(NewOptInConsumer("chain1")), Set("chain2"), Set() ) res._2 == "" and - res._1.get("chain1") == RUNNING and - res._1.get("chain2") == STOPPED and - res._1.get("chain3") == STOPPED + res._1.consumerStatus.get("chain1") == RUNNING and + res._1.consumerStatus.get("chain2") == STOPPED and + res._1.consumerStatus.get("chain3") == STOPPED } run ConsumerStatusMapAlreadyRunningTest = @@ -260,8 +261,8 @@ module ccv_test { "chain3" -> STOPPED ) val res = StartStopConsumers( - currentConsumerStatusMap, - Set("chain2"), + GetEmptyProviderState.with("consumerStatus", currentConsumerStatusMap), + Set(NewOptInConsumer("chain2")), Set("chain3"), Set() ) @@ -276,8 +277,8 @@ module ccv_test { "chain3" -> STOPPED ) val res = StartStopConsumers( - currentConsumerStatusMap, - Set("chain1"), + GetEmptyProviderState.with("consumerStatus", currentConsumerStatusMap), + Set(NewOptInConsumer("chain1")), Set("chain3"), Set() ) @@ -292,8 +293,8 @@ module ccv_test { "chain3" -> STOPPED ) val res = StartStopConsumers( - currentConsumerStatusMap, - Set("chain1"), + GetEmptyProviderState.with("consumerStatus", currentConsumerStatusMap), + Set(NewOptInConsumer("chain1")), Set("chain1"), Set() ) diff --git a/tests/mbt/model/ccv_utils.qnt b/tests/mbt/model/ccv_utils.qnt new file mode 100644 index 0000000000..b80400c3f7 --- /dev/null +++ b/tests/mbt/model/ccv_utils.qnt @@ -0,0 +1,487 @@ +// This file contains utility functions for ccv.qnt +// that are not part of the API/core logic of ccv, but still relevant +// for the functional logic of the protocol. +module ccv_utils { + import ccv_types.* from "./ccv" + import extraSpells.* from "./libraries/extraSpells" + import Time.* from "./libraries/Time" + + + // Takes the current provider state and validator set and returns + // the validator set under the current key assignments for the given consumer, as stored in the provider state. + pure def applyKeyAssignmentToValSet( + providerState: ProviderState, + consumer: Chain, + valSet: ValidatorSet + ): ValidatorSet = { + // map each validator to a tuple of (consumer address, voting power) + valSet.keys().map( + (node) => + pure val power = valSet.get(node) + // check if the validator has a key assigned + pure val validatorToConsumerAddr = providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) + if (validatorToConsumerAddr.keys().contains(node)) { + // the validator has a key assigned + pure val consAddr = validatorToConsumerAddr.get(node) + (consAddr, power) + } else { + // the validator has no key assigned + // use the default key + (node, power) + } + ).fold( // fold the (addr,pow) tuples into a map addr -> pow + Map(), + (acc, pair) => acc.put(pair._1, pair._2) + ) + } + + // Takes a validator set, to which a key assignment has been applied, and reverts it, + // i.e. returns the original validator set. + // This also filters out validators that are assigned 0 power. + pure def revertKeyAssignment( + keyAssignment: Node -> ConsumerAddr, + valSetWithAssignment: ValidatorSet + ): ValidatorSet = { + // get an assignment from consumer addr to nodes + pure val reverseAssignment = keyAssignment.keys().map( + (consAddr) => + (keyAssignment.get(consAddr), consAddr) + ).fold( + Map(), + (acc, pair) => acc.put(pair._1, pair._2) + ) + + // for each node in the valset, reverse its key assignment + valSetWithAssignment.keys().map( + (addr) => + pure val power = valSetWithAssignment.get(addr) + // if the addr has a key assigned, use that. otherwise, the addr doesn't have a key assigned, + // and therefore *is* the key that should be used. + pure val consAddr = reverseAssignment.getOrElse(addr, addr) + (consAddr, power) + ).filter( + pair => pair._2 > 0 + ).fold( + Map(), + (acc, pair) => acc.put(pair._1, pair._2) + ) + } + + // Appends the key assignment for the given oldConsAddr on the consumer by a validator + // to be pruned when a VscMaturedPacket for the current runningVscId is received from the consumer. + pure def AppendConsumerAddrToPrune(currentState: ProtocolState, oldConsAddr: ConsumerAddr, consumer: Chain): ProtocolState = { + pure val vscId = currentState.providerState.runningVscId + pure val consumerAddrsToPrune = currentState.providerState.consumerAddrsToPrune.getOrElse(consumer, Map()) + pure val prevConsAddrs = consumerAddrsToPrune.getOrElse(oldConsAddr, Map()).getOrElse(vscId, []) + + pure val newConsAddrsToPrune = consumerAddrsToPrune.put(vscId, prevConsAddrs.append(oldConsAddr)) + + currentState.with( + "providerState", + currentState.providerState.with( + "consumerAddrsToPrune", + currentState.providerState.consumerAddrsToPrune.put(consumer, newConsAddrsToPrune) + ) + ) + } + + // Returns the new ConsumerStatusMap according to the consumers to stop + // and the consumers to time out. + // If a consumer is both stopped and timed out, it will be timed out. + // The second return is an error string: If it is not equal to "", + // it contains an error message, and the first return should be ignored. + pure def stopConsumers( + currentConsumerStatusMap: Chain -> str, + consumersToStop: Set[Chain], + consumersToTimeout: Set[Chain]): (Chain -> str, str) = { + val runningConsumers = currentConsumerStatusMap.keys().filter( + chain => currentConsumerStatusMap.get(chain) == RUNNING + ) + // all consumers to stop must be running right now, else we have an error + if (consumersToStop.exclude(runningConsumers).size() > 0) { + (currentConsumerStatusMap, "Cannot stop a consumer that is not running") + } else { + val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( + (chain) => + if (consumersToTimeout.contains(chain)) { + TIMEDOUT + } else if (consumersToStop.contains(chain)) { + STOPPED + } else { + currentConsumerStatusMap.get(chain) + } + ) + (newConsumerStatusMap, "") + } + } + + // Returns the new ConsumerStatusMap according to the consumers to start. + // The second return is an error string: If it is not equal to "", + // it contains an error message, and the first return should be ignored. + pure def startConsumers( + currentConsumerStatusMap: Chain -> str, + consumersToStart: Set[Chain]): (Chain -> str, str) = { + val nonConsumers = currentConsumerStatusMap.keys().filter( + chain => currentConsumerStatusMap.get(chain) == NOT_CONSUMER + ) + // all consumers to start must be nonConsumers right now, otherwise we have an error + if (consumersToStart.exclude(nonConsumers).size() > 0) { + (currentConsumerStatusMap, "cannot start a consumer that is stopped or already a consumer") + } else { + val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( + (chain) => + if (consumersToStart.contains(chain)) { + RUNNING + } else { + currentConsumerStatusMap.get(chain) + } + ) + (newConsumerStatusMap, "") + } + } + + pure def StartStopConsumers( + currentProviderState: ProviderState, + consumersToStart: Set[ConsumerAdditionMsg], + consumersToStop: Set[Chain], + consumersToTimeout: Set[Chain] + ): (ProviderState, str) = { + val consumerAdditions = consumersToStart.map( + msg => msg.chain + ) + // check if any consumer is both started and stopped + if (consumerAdditions.intersect(consumersToStop).size() > 0) { + (currentProviderState, "Cannot start and stop a consumer at the same time") + } else { + val res1 = currentProviderState.consumerStatus.startConsumers(consumerAdditions) + val newConsumerStatus = res1._1 + val err1 = res1._2 + val res2 = newConsumerStatus.stopConsumers(consumersToStop, consumersToTimeout) + val err2 = res2._2 + // set the top N values in the provider correctly + + if (err1 != "") { + (currentProviderState, err1) + } else if (err2 != "") { + (currentProviderState, err2) + } else { + (currentProviderState + .with("consumerStatus", res2._1) + .SetTopNValues(consumersToStart), "") + } + } + } + + + // 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( + removeZeroPowers(chainState.currentValidatorSet) + ) + ) + } + + // Advances the timestamp in the chainState by timeAdvancement + pure def advanceTime(chainState: ChainState, timeAdvancement: Time): ChainState = + { + ...chainState, + lastTimestamp: chainState.runningTimestamp, + runningTimestamp: chainState.runningTimestamp + timeAdvancement, + } + + // common logic to update the chain state, used by both provider and consumers. + pure def endAndBeginBlockShared(chainState: ChainState, timeAdvancement: Time): ChainState = { + chainState.enterCurValSetIntoBlock().advanceTime(timeAdvancement) + } + + // returns the providerState with the following modifications: + // * sends VscPackets to all running consumers, using the provided timestamp as sending time + // * increments the runningVscId + // This should only be called when the provider chain is ending a block. + // If no vsc packets need to be sent, this will be a noop. + // the ccv timeout should be the ccv timeout for the provider chain. + pure def sendVscPackets( + providerState: ProviderState, + sendingTimestamp: Time, + ccvTimeout: Time): ProviderState = { + val newSentPacketsPerConsumer = providerState.getConsumers().mapBy( // compute, for each consumer, a list of new packets to be sent + (consumer) => + // if validator set changed or the key assignments for this chain changed, and the consumer is running, send a packet + if ((providerState.providerValidatorSetChangedInThisBlock or + providerState.consumersWithAddrAssignmentChangesInThisBlock.contains(consumer)) + and + isRunningConsumer(consumer, providerState)) { + // send a packet, i.e. use a list with one element (the packet to be sent) + List({ + id: providerState.runningVscId, + // apply key assignment to the current validator set + validatorSet: providerState.applyKeyAssignmentToValSet( + consumer, + providerState.chainState.currentValidatorSet + ), + sendingTime: sendingTimestamp, + timeoutTime: sendingTimestamp + ccvTimeout + }) + } else { + // no packet to be sent, so empty list + List() + } + ) + val newOutstandingPacketsToConsumer = providerState.getConsumers().mapBy( + (consumer) => + providerState.outstandingPacketsToConsumer.getOrElse(consumer, List()).concat( + newSentPacketsPerConsumer.get(consumer) + ) + ) + val newSentVscPackets = providerState.getConsumers().mapBy( + (consumer) => + providerState.sentVscPacketsToConsumer.getOrElse(consumer, List()).concat( + newSentPacketsPerConsumer.get(consumer) + ) + ) + { + ...providerState, + outstandingPacketsToConsumer: newOutstandingPacketsToConsumer, + sentVscPacketsToConsumer: newSentVscPackets, + runningVscId: providerState.runningVscId + 1, + // we ended the block and processed that the valset or key assignments changed, + // so reset the flags + providerValidatorSetChangedInThisBlock: false, + consumersWithAddrAssignmentChangesInThisBlock: Set(), + // remember the key assignments that were applied to send the packets + keyAssignmentsForVSCPackets: providerState.keyAssignmentsForVSCPackets.put( + providerState.runningVscId, + providerState.validatorToConsumerAddr + ) + } + } + + // receives a given packet (sent by the provider) on the consumer. The arguments are the consumer chain that is receiving the packet, and the packet itself, + // as well as the unbonding period for the consumer chain. + // To receive a packet, modify the running validator set (not the one entered into the block yet, + // but the candidate that would be put into the block if it ended now) + // and store the maturation time for the packet. + pure def recvPacketOnConsumer( + currentState: ProtocolState, + receiver: Chain, + packet: VscPacket, + receiverUnbondingPeriod: Time): Result = { + if(not(isRunningConsumer(receiver, currentState.providerState))) { + Err("Receiver is not currently a consumer - must have 'running' status!") + } else { + // update the running validator set, but not the history yet, + // as that only happens when the next block is started + val currentConsumerState: ConsumerState = currentState.consumerStates.get(receiver) + val newConsumerState: ConsumerState = + { + ...currentConsumerState, + chainState: currentConsumerState.chainState.with( + "currentValidatorSet", packet.validatorSet + ), + maturationTimes: currentConsumerState.maturationTimes.append( + ( + packet, + currentConsumerState.chainState.runningTimestamp + receiverUnbondingPeriod + ) + ), + receivedVscPackets: currentConsumerState.receivedVscPackets.prepend(packet) + } + val newConsumerStates = currentState.consumerStates.set(receiver, newConsumerState) + val newState = currentState.with( + "consumerStates", newConsumerStates + ) + Ok(newState) + } + } + + // receives a given packet on the provider. The arguments are the consumer chain that sent the packet, and the packet itself. + // To receive a packet, add it to the list of received maturations. + pure def recvPacketOnProvider(currentState: ProtocolState, sender: Chain, packet: VscMaturedPacket): Result = { + if (not(isRunningConsumer(sender, currentState.providerState))) { + Err("Sender is not currently a consumer - must have 'running' status!") + } else if (currentState.providerState.sentVscPacketsToConsumer.get(sender).head().id != packet.id) { + // the packet is not the oldest sentVscPacket, something went wrong + Err("Received maturation is not for the oldest sentVscPacket") + } else { + val currentReceivedMaturations = currentState.providerState.receivedMaturations + val newReceivedMaturations = currentReceivedMaturations.union(Set(packet)) + val newProviderState = currentState.providerState.with( + "receivedMaturations", newReceivedMaturations + ) + // prune the sentVscPacket + val newSentVscPacket = currentState.providerState.sentVscPacketsToConsumer.get(sender).tail() + val newState = currentState.with( + "providerState", + {...newProviderState, + sentVscPacketsToConsumer: currentState.providerState.sentVscPacketsToConsumer.set(sender, newSentVscPacket) + } + ) + + // prune assigned keys that are no longer needed + + // get the keys that should be pruned + pure val consumerAddrsToPrune = + currentState.providerState.consumerAddrsToPrune + .getOrElse(sender, Map()) + .getOrElse(packet.id, List()).toSet() + + // actually do the pruning + pure val senderValByConsAddr = + // for the sender chain, get the consAddrToValidator mapping + newState.providerState.consumerAddrToValidator.getOrElse(sender, Map()) + pure val newSenderValByConsAddr = + senderValByConsAddr.keys().filter( + // filter out the assigned keys that should be pruned + consAddr => not(consumerAddrsToPrune.contains(consAddr)) + ).mapBy( + // rebuild the map with the pruned keys removed + consAddr => senderValByConsAddr.get(consAddr) + ) + + // update the provider state + pure val newProviderState2 = newState.providerState.with( + // update the consumerAddrToValidator map to remove the pruned keys + "consumerAddrToValidator", + newState.providerState.consumerAddrToValidator.put(sender, newSenderValByConsAddr) + ).with( + // delete the consumer addresses to prune, since they are pruned now + "consumerAddrsToPrune", + newState.providerState.consumerAddrsToPrune.put( + sender, + newState.providerState.consumerAddrsToPrune.getOrElse(sender, Map()).put( + packet.id, + List() + ) + ) + ) + + // update the state + pure val newState2 = newState.with( + "providerState", newProviderState2 + ) + + Ok(newState2) + } + } + + // removes the oldest outstanding packet from the consumer. on-chain, this would happen when the packet is acknowledged. + // only the oldest packet can be removed, since we model ordered channels. + pure def removeOutstandingPacketFromConsumer(currentState: ProtocolState, sender: Chain): ProtocolState = { + val currentOutstandingPackets = currentState.consumerStates.get(sender).outstandingPacketsToProvider + val newOutstandingPackets = currentOutstandingPackets.tail() + val newConsumerState = currentState.consumerStates.get(sender).with( + "outstandingPacketsToProvider", newOutstandingPackets + ) + val newConsumerStates = currentState.consumerStates.set(sender, newConsumerState) + val newState = currentState.with( + "consumerStates", newConsumerStates + ) + newState + } + + // removes the oldest outstanding packet (to the given consumer) from the provider. + // on-chain, this would happen when the packet is acknowledged. + // only the oldest packet can be removed, since we model ordered channels. + pure def removeOutstandingPacketFromProvider(currentState: ProtocolState, receiver: Chain): ProtocolState = { + val currentOutstandingPackets = currentState.providerState.outstandingPacketsToConsumer.get(receiver) + val newOutstandingPackets = currentOutstandingPackets.tail() + val newProviderState = currentState.providerState.with( + "outstandingPacketsToConsumer", + currentState.providerState.outstandingPacketsToConsumer.set(receiver, newOutstandingPackets) + ) + val newState = currentState.with( + "providerState", newProviderState + ) + newState + } + + // Returns a ProtocolState where the current validator set on the provider is set to + // newValidatorSet. + pure def setProviderValidatorSet(currentState: ProtocolState, newValidatorSet: ValidatorSet): ProtocolState = { + pure val newChainState = currentState.providerState.chainState.with( + "currentValidatorSet", newValidatorSet + ) + currentState.with( + "providerState", + currentState.providerState.with( + "chainState", newChainState + ) + ) + } + + // Returns true if the given chain is currently a running consumer, false otherwise. + pure def isRunningConsumer(chain: Chain, providerState: ProviderState): bool = { + val status = providerState.consumerStatus.get(chain) + status == RUNNING + } + + // Returns the set of all consumer chains. + pure def getConsumers(providerState: ProviderState): Set[Chain] = providerState.consumerStatus.keys() + + // Returns the set of all consumer chains that currently have the status RUNNING. + pure def getRunningConsumers(providerState: ProviderState): Set[Chain] = { + providerState.consumerStatus.keys().filter( + chain => providerState.consumerStatus.get(chain) == RUNNING + ) + } + + // Returns the set of all consumer chains that currently have the status NOT_CONSUMER. + pure def getNonConsumers(providerState: ProviderState): Set[Chain] = { + providerState.consumerStatus.keys().filter( + chain => providerState.consumerStatus.get(chain) == NOT_CONSUMER + ) + } + + // Returns whether the consumer has timed out due to the vscTimeout, and an error message. + // If the second return is not equal to "", the first return should be ignored. + // If it is equal to "", the first return will be true if the consumer has timed out and should be dropped, + // or false otherwise. + pure def TimeoutDueToVscTimeout(currentState: ProtocolState, consumer: Chain, vscTimeout: Time): (bool, str) = + // check for errors: the consumer is not running + if (not(isRunningConsumer(consumer, currentState.providerState))) { + (false, "Consumer is not currently a consumer - must have 'running' status!") + } else { + val providerState = currentState.providerState + val consumerState: ConsumerState = currentState.consumerStates.get(consumer) + + // has a packet been sent on the provider more than vscTimeout ago, but we have not received an answer since then? + val sentVscPacketsToConsumer = providerState.sentVscPacketsToConsumer.getOrElse(consumer, List()) + if(sentVscPacketsToConsumer.length() > 0) { + val oldestSentVscPacket = sentVscPacketsToConsumer.head() // if length is 0, this is undefined, but we check for this before we use it + if(oldestSentVscPacket.sendingTime + vscTimeout < providerState.chainState.runningTimestamp) { + (true, "") + } else { + // no timeout yet, it has not been vscTimeout since that packet was sent + (false, "") + } + } else { + // no packet has been sent yet, so no timeout + (false, "") + } + } + + // Sets the top N values on the provider chain for the given consumer chains, + // taken as consumerAdditionMsgs = chains with the top N values. + // If a chain in the set is already present, the old value will be overwritten. + pure def SetTopNValues(providerState: ProviderState, consumers: Set[ConsumerAdditionMsg]): ProviderState = + providerState.with( + "topNByConsumer", + consumers.fold( + providerState.topNByConsumer, + (acc, consumer) => acc.put(consumer.chain, consumer.topN) + ) + ) + + // From a validator set, removes all validators with zero power. + pure def removeZeroPowers(valSet: ValidatorSet): ValidatorSet = + valSet.keys().fold( + Map(), + (acc, node) => + if (valSet.get(node) == 0) { + acc + } else { + acc.put(node, valSet.get(node)) + } + ) +} \ No newline at end of file diff --git a/tests/mbt/model/libraries/extraSpells.qnt b/tests/mbt/model/libraries/extraSpells.qnt index 9167bb4bcb..6ab4063ad3 100644 --- a/tests/mbt/model/libraries/extraSpells.qnt +++ b/tests/mbt/model/libraries/extraSpells.qnt @@ -139,6 +139,72 @@ module extraSpells { __set.fold(List(), (__l, __e) => __l.append(__e)) } + /// The type of orderings between comparable things + // Follows https://hackage.haskell.org/package/base-4.19.0.0/docs/Data-Ord.html#t:Ordering + // and we think there are likely benefits to using 3 constant values rather than the more + // common integer range in Apalache. + type Ordering = + | EQ + | LT + | GT + + /// Comparison of integers + pure def intCompare(__a: int, __b:int): Ordering = { + if (__a < __b) + { LT } + else if (__a > __b) + { GT } + else + { EQ } + } + + /// Assuming `__l` is sorted according to `__cmp`, returns a list with the element `__x` + /// inserted in order. + /// + /// If `__l` is not sorted, `__x` will be inserted after the first element less than + /// or equal to it. + /// + /// - @param __l a sorted list + /// - @param __x an element to be inserted + /// - @param __cmp an operator defining an `Ordering` of the elemnts of type `a` + /// - @returns a sorted list that includes `__x` + pure def sortedListInsert(__l: List[a], __x: a, __cmp: (a, a) => Ordering): List[a] = { + // We need to track whether __x has been inserted, and the accumulator for the new list + val __init = { is_inserted: false, acc: List() } + + val __result = __l.foldl(__init, (__state, __y) => + if (__state.is_inserted) + { ...__state, acc: __state.acc.append(__y) } + else + match __cmp(__x, __y) { + | GT => { ...__state, acc: __state.acc.append(__y) } + | _ => { is_inserted: true, acc: __state.acc.append(__x).append(__y) } + }) + + if (not(__result.is_inserted)) + // If __x was not inserted, it was GT than every other element, so it goes at the end + __result.acc.append(__x) + else + __result.acc + } + + run sortedListInsertTest = all { + assert(List().sortedListInsert(3, intCompare) == List(3)), + assert(List(1,2,4).sortedListInsert(3, intCompare) == List(1,2,3,4)), + assert(List(4,1,2).sortedListInsert(3, intCompare) == List(3,4,1,2)), + assert(List(1,2,3).sortedListInsert(4, intCompare) == List(1,2,3,4)), + } + + //// Returns a list of all elements of a set. + //// The ordering will be arbitrary. + //// + //// - @param __set a set + //// - @param __cmp an operator defining an `Ordering` of the elemnts of type `a` + //// - @returns a sorted list of all elements of __set + pure def toSortedList(__set: Set[a], __cmp: (a, a) => Ordering): List[a] = { + __set.fold(List(), (__l, __e) => __l.sortedListInsert(__e, __cmp)) + } + //// Returns a set of the elements in the list. //// //// - @param __list a list @@ -207,4 +273,59 @@ module extraSpells { assert(not(listForAll(List(1, 2, 3), __x => __x > 1))), assert(listForAll(List(), __x => __x > 0)), } + + /// Compute the sum of the values over all entries in a map. + /// + /// - @param myMap a map from keys to integers + /// - @returns the sum; when the map is empty, the sum is 0. + pure def mapValuesSum(myMap: a -> int): int = { + myMap.keys().fold(0, ((sum, i) => sum + myMap.get(i))) + } + + run mapValuesSumTest = all { + assert(Map().mapValuesSum() == 0), + assert(2.to(5).mapBy(i => i * 2).mapValuesSum() == 28), + assert(Map(2 -> -4, 4 -> 2).mapValuesSum() == -2), + } + + /// Returns a map of a subset of keys and values from a map, + // where only those keys are included for which the given __f + // returns true. + pure def mapFilter(__map: a -> b, __f: a => bool): a -> b = { + __map.keys().filter(e => __f(e)).mapBy(__k => __map.get(__k)) + } + + /// Compute the maximum of two integers. + /// + /// - @param __i first integer + /// - @param __j second integer + /// - @returns the maximum of __i and __j + pure def max(__i: int, __j: int): int = { + if (__i > __j) __i else __j + } + + run maxTest = all { + assert(max(3, 4) == 4), + assert(max(6, 3) == 6), + assert(max(10, 10) == 10), + assert(max(-3, -5) == -3), + assert(max(-5, -3) == -3), + } + + /// Compute the minimum of two integers. + /// + /// - @param __i first integer + /// - @param __j second integer + /// - @returns the minimum of __i and __j + pure def min(__i: int, __j: int): int = { + if (__i < __j) __i else __j + } + + run minTest = all { + assert(min(3, 4) == 3), + assert(min(6, 3) == 3), + assert(min(10, 10) == 10), + assert(min(-3, -5) == -5), + assert(min(-5, -3) == -5), + } } \ No newline at end of file diff --git a/tests/mbt/model/run_invariants.sh b/tests/mbt/model/run_invariants.sh new file mode 100755 index 0000000000..df22b97702 --- /dev/null +++ b/tests/mbt/model/run_invariants.sh @@ -0,0 +1,6 @@ +#!/bin/bash + +quint test ccv_model.qnt +quint test ccv_test.qnt +quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_model.qnt --max-steps 200 --max-samples 200 +quint run --invariant "all{ValidatorUpdatesArePropagatedKeyAssignmentInv,ValidatorSetHasExistedKeyAssignmentInv,SameVscPacketsKeyAssignmentInv,MatureOnTimeInv,EventuallyMatureOnProviderInv,KeyAssignmentRulesInv}" ccv_model.qnt --step stepKeyAssignment --max-steps 200 --max-samples 200 \ No newline at end of file diff --git a/tests/mbt/run_invariants.sh b/tests/mbt/run_invariants.sh deleted file mode 100755 index 613664aeae..0000000000 --- a/tests/mbt/run_invariants.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/bash - -quint test ccv_model.qnt -quint test ccv_test.qnt -quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_model.qnt --max-steps 200 --max-samples 200 \ No newline at end of file