diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md new file mode 100644 index 0000000000..0cef3bc632 --- /dev/null +++ b/tests/difference/core/quint_model/README.md @@ -0,0 +1,72 @@ +This folder contains a Quint model for the core logic of Cross-Chain Validation (CCV). + +### File structure +The files are as follows: +- ccv.qnt: Contains the type definitions, data structures, functional logic for CCV. +The core of the protocol. +- ccv_model.qnt: Contains the stateful part of the model for CCV. Very roughly speaking, this could be seen as "e2e tests". +Also contains invariants. +- ccv_test.qnt: Contains unit tests for the functional layer of CCV. +- libraries/*: Libraries that don't belong to CCV, but are used by it. + +### Model details + +To see the data structures used in the model, see the `ProtocolState` type in ccv.qnt. + +The "public" endpoints of the model are those functions that take as an input the protocol state, and return a `Result`. +Other functions are for utility. + +The parameters of the protocol are defined as consts in [ccv.qnt](ccv.qnt). + +### Tests + +To run unit tests, run +``` +quint test ccv_test.qnt +``` +and +``` +quint test ccv_model.qnt +``` + +### Invariants + +The invariants to check are in [ccv_model.qnt](ccv_model.qnt). +Check a single invariant by running +`quint run --invariant INVARIANT_NAME ccv_model.qnt`, +or all invariants one after another with the help of the script `run_invariants.sh`. +Each invariant takes about a minute to run. + +Invariants are as follows: +- [X] ValidatorUpdatesArePropagatedInv: When a validator power update is comitted on chain, a packet containing that change in voting power is sent to all running consumers. +- [X] ValidatorSetHasExistedInv: Every validator set on consumer chains is/was a validator set on the provider. +- [X] SameVscPacketsInv: Ensure that consumer chains receive the same VscPackets in the same order. +Because of nuances with starting/stopping consumers, this invariant is not as simple as it sounds. In detail: +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 in the same order. +- [X] MatureOnTimeInv: For every ValidatorSetChangePacket received by a consumer chain at +time t, a MaturedVscPacket is sent back to the provider in the first block +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 can also be model-checked by Apalache, using this command: +``` +quint verify --invariant ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv \ + ccv_model.qnt +``` + +### Sanity Checks + +Sanity checks verify that certain patterns of behaviour can appear in the model. +In detail, they are invariant checks that we expect to fail. +They usually negate the appearance of some behaviour, i.e. `not(DesirableBehaviour)`. +Then, a counterexample for this is an example trace exhibiting the behaviour. + +They are run like invariant checks, i.e. `quint run --invariant SANITY_CHECK_NAME ccv_model.qnt`. +The available sanity checks are: +- CanRunConsumer +- CanStopConsumer +- CanTimeoutConsumer +- CanSendVscPackets +- CanSendVscMaturedPackets \ No newline at end of file diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt new file mode 100644 index 0000000000..0e07b4476c --- /dev/null +++ b/tests/difference/core/quint_model/ccv.qnt @@ -0,0 +1,811 @@ +// -*- mode: Bluespec; -*- +module ccv_types { + import Time.* from "./libraries/Time" + + type Node = str + type Chain = str + type Power = int + type VscId = int + type ValidatorSet = Node -> Power + type Height = int + // a list of validator sets per blocks, ordered by recency + type VotingPowerHistory = List[ValidatorSet] + + type VscPacket = + { + // the identifier for this packet + id: VscId, + // the new validator set. in the implementation, this would be a list of validator updates + validatorSet: ValidatorSet, + // the time at which the packet was sent. used to check whether packets have timed out. + sendingTime: Time + } + + type VscMaturedPacket = + { + // the id of the VscPacket that matured + id: VscId, + // the time at which the packet was sent. used to check whether packets have timed out. + sendingTime: Time + } + + + // state that each chain needs to store, whether consumer or provider. + type ChainState = { + // Stores the list of voting powers that corresponded to voting powers + // at blocks over the chains entire existence. + // Voting powers should be ordered by recency in descending order. + votingPowerHistory: VotingPowerHistory, + + // the current validator set on each chain. + // this will be included in the next block, but might not be final yet, + // e.g. there may be more modifications in the current block. + currentValidatorSet: ValidatorSet, + + // the latest timestamp that was comitted on chain + lastTimestamp: Time, + } + + // utility function: returns a chain state that is initialized minimally. + pure def GetEmptyChainState(): ChainState = + { + votingPowerHistory: List(), + currentValidatorSet: Map(), + lastTimestamp: 0, + } + + // Defines the current state of the provider chain. Essentially, all information here is stored by the provider on-chain (or could be derived purely by information that is on-chain). + type ProviderState = + { + // the state that each chain needs to store + chainState: ChainState, + + // Stores, for each consumer chain, the list of packets that have been sent to the consumer chain + // and *have not been received yet*. + // In the implementation, this would roughly be the unacknowledged packets on an ibc channel. + outstandingPacketsToConsumer: Chain -> List[VscPacket], + + // the set of received VscMaturedPackets + receivedMaturations: Set[VscMaturedPacket], + + // Stores VscPackets which have been sent but where the provider has *not received a response yet*. + sentVscPacketsToConsumer: Chain -> List[VscPacket], + + // stores whether, in this block, the validator set has changed. + // this is needed because the validator set might be considered to have changed, even though + // it is still technically identical at our level of abstraction, e.g. a validator power change on the provider + // might leave the validator set the same because a delegation and undelegation cancel each other out. + providerValidatorSetChangedInThisBlock: bool, + + // stores, for each consumer chain, its current status - + // not consumer, running, or stopped + consumerStatus: Chain -> str, + + // a monotonic strictly increasing and positive ID that is used + // to uniquely identify the Vscs sent to the consumer chains. + runningVscId: int, + } + + // utility function: returns a provider state that is initialized minimally. + pure def GetEmptyProviderState(): ProviderState = + { + chainState: GetEmptyChainState, + outstandingPacketsToConsumer: Map(), + receivedMaturations: Set(), + sentVscPacketsToConsumer: Map(), + providerValidatorSetChangedInThisBlock: false, + consumerStatus: Map(), + runningVscId: 0, + } + + + // Defines the current state of a consumer chain. This information is accessible to that consumer on-chain. + type ConsumerState = { + // the state that each chain needs to store + chainState: ChainState, + + // Stores the maturation times for VscPackets received by this consumer + maturationTimes: VscPacket -> Time, + + // stores the received vscpackets in descending order of recency, + // i.e. newest first. + receivedVscPackets: List[VscPacket], + + // Stores the list of packets that have been sent to the provider chain by this consumer + // and have not been received yet. + // ordered by recency, so the head is the oldest packet. + // In the implementation, essentially unacknowledged IBC packets. + outstandingPacketsToProvider: List[VscMaturedPacket], + } + + // utility function: returns a consumer state that is initialized minimally. + pure def GetEmptyConsumerState(): ConsumerState = + { + chainState: GetEmptyChainState, + maturationTimes: Map(), + outstandingPacketsToProvider: List(), + receivedVscPackets: List(), + } + + // the state of the protocol consists of the composition of the state of one provider chain with potentially many consumer chains. + type ProtocolState = { + providerState: ProviderState, + // the state of each consumer chain. + // note that we assume that this contains all consumer chains that may ever exist, + // and consumer chains that are currently not running will have providerState.consumerStatus == NOT_CONSUMER or STOPPED. + consumerStates: Chain -> ConsumerState + } + + // gets a protocol state that is initialized minimally. + pure def GetEmptyProtocolState(): ProtocolState = + { + providerState: GetEmptyProviderState, + consumerStates: Map(), + } + + type Error = str + + // we return either a result or an error. + // if hasError() is true, newState may be arbitrary, but the error will be meaningful. + // if hasError() is false, error may be arbitrary, but newState will be meaningful. + type Result = { + newState: ProtocolState, + error: Error + } + + pure def Ok(newState: ProtocolState): Result = { + { + newState: newState, + error: "" + } + } + + pure def Err(msg: str): Result = { + { + newState: { + providerState: { + chainState: { + votingPowerHistory: List(), + currentValidatorSet: Map(), + lastTimestamp: 0, + }, + outstandingPacketsToConsumer: Map(), + receivedMaturations: Set(), + sentVscPacketsToConsumer: Map(), + providerValidatorSetChangedInThisBlock: false, + consumerStatus: Map(), + runningVscId: 0, + }, + consumerStates: Map(), + }, + error: msg + } + } + + pure def hasError(result: Result): bool = result.error != "" + + // possible consumer statuses + pure val STOPPED = "stopped" // the chain was once a consumer chain, but has been voluntarily dropped by the provider. + pure val TIMEDOUT = "timedout" // the chain has timed out and was dropped by the provider. This is only used for involuntary drops. + pure val RUNNING = "running" // the chain is currently a consumer chain. Running chains are those that get sent VscPackets. + pure val NOT_CONSUMER = "not consumer" // the chain has never been a consumer chain, and is available to become one. + // When a chain is dropped, it cannot become a consumer again - we assume that would be done by another consumer becoming running. + + // the provider chain. + // 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" +} + +module ccv { + // Implements the core logic of the cross-chain validation protocol. + + // Things that are not modelled: + // * Reward distribution + // * Starting/Stopping chains during execution + // * Slashes + + // Things that explicitly are modelled: + // * Validator set changes are propagated from provider to consumers + // * Vsc packets mature + + // We assume that packet receive + ack happen synchronously, + // i.e. when the packet is delivered, the ack is delivered right afterwards. + // This is because it is nontrivial in practice to get a relayer to relay a packet, but not its ack. + + import Time.* from "./libraries/Time" + import extraSpells.* from "./libraries/extraSpells" + import ccv_types.* + + + // =================== + // PROTOCOL PARAMETERS + // =================== + + // the set of all possible consumer chains. + const ConsumerChains: Set[Chain] + + // For each chain, this defines the time between the initiation of an unbonding and its maturation. + const UnbondingPeriodPerChain: Chain -> int + + // The maximum time duration between sending any VscPacket to any consumer chain and receiving the + // corresponding VscMaturedPacket, without timing out the consumer chain and consequently removing it. + const VscTimeout: int + + // The timeoutTimestamp for sent packets. Can differ by chain. + const CcvTimeout: Chain -> int + + // =================== + // PROTOCOL LOGIC contains the meat of the protocol + // functions here roughly correspond to API calls that can be triggered from external sources + // =================== + + // the power of a validator on the provider chain is changed to the given amount. We do not care how this happens, + // e.g. via undelegations, or delegations, ... + pure def votingPowerChange(currentState: ProtocolState, validator: Node, amount: int): Result = { + if (amount < 0) { + Err("Voting power changes must be nonnegative") + } else { + pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet + pure val newValidatorSet = currentValidatorSet.put(validator, amount) + // set the validator set changed flag + val newProviderState = currentState.providerState.with( + "providerValidatorSetChangedInThisBlock", true + ) + pure val tmpState = currentState.with( + "providerState", newProviderState + ) + pure val newState = setProviderValidatorSet(tmpState, newValidatorSet) + Ok(newState) + } + } + + // Delivers the next queued VscMaturedPacket from a consumer chain to the provider chain. + // Arguments are the currentState and the the consumer chain, from which the packet will be delivered. + // If this packet will time out on the provider on delivery, + // the consumer will be dropped. + // The first return is the result of the operation, the second result is a boolean + // that indicates whether the consumer timed out or not. + // If the result has an error, the second return should be ignored. + pure def deliverPacketToProvider(currentState: ProtocolState, sender: Chain): (Result, bool) = { + if (not(isRunningConsumer(sender, currentState.providerState))) { + (Err("Sender is not currently a consumer - must have 'running' status!"), false) + } else if (length(currentState.consumerStates.get(sender).outstandingPacketsToProvider) == 0) { + (Err("No outstanding packets to deliver"), false) + } else { + val packet = currentState.consumerStates.get(sender).outstandingPacketsToProvider.head() + if(packet.sendingTime + CcvTimeout.get(sender) < currentState.providerState.chainState.lastTimestamp) { + // drop consumer + val result = stopConsumers( + currentState.providerState.consumerStatus, + Set(), + Set(sender) + ) + + val newConsumerStatus = result._1 + val err = result._2 + if (err != "") { + (Err(err), false) + } else { + val newProviderState = currentState.providerState.with( + "consumerStatus", newConsumerStatus + ) + val newState = currentState.with( + "providerState", newProviderState + ) + (Ok(newState), true) // true because the packet timed out + } + } else { + // the packet has not timed out, so receive it on the provider + val result = recvPacketOnProvider(currentState, sender, packet) + val tmpState = result.newState + if (result.hasError()) { + (result, false) + } else { + (Ok(removeOutstandingPacketFromConsumer(tmpState, sender)), false) // false because the packet did not time out + } + } + } + } + + // Delivers the next queued VscPacket from the provider chain to a consumer chain. + // Arguments are the current state and the consumer chain, to which the packet will be delivered. + // If this packet will time out on the consumer on delivery, + // the consumer will be dropped. + // The first return is the result of the operation, the second result is a boolean + // that indicates whether the consumer timed out or not. + // If the result has an error, the second return should be ignored. + pure def deliverPacketToConsumer(currentState: ProtocolState, receiver: Chain): (Result, bool) = { + if (not(isRunningConsumer(receiver, currentState.providerState))) { + (Err("Receiver is not currently a consumer - must have 'running' status!"), false) + } else if (length(currentState.providerState.outstandingPacketsToConsumer.get(receiver)) == 0) { + (Err("No outstanding packets to deliver"), false) + } else { + val packet = currentState.providerState.outstandingPacketsToConsumer.get(receiver).head() + // check if the consumer timed out + if (packet.sendingTime + CcvTimeout.get(PROVIDER_CHAIN) < currentState.consumerStates.get(receiver).chainState.lastTimestamp) { + // drop consumer + val result = stopConsumers( + currentState.providerState.consumerStatus, + Set(), + Set(receiver) + ) + + val newConsumerStatus = result._1 + val err = result._2 + if (err != "") { + (Err(err), false) + } else { + val newProviderState = currentState.providerState.with( + "consumerStatus", newConsumerStatus + ) + val newState = currentState.with( + "providerState", newProviderState + ) + (Ok(newState), true) // true because the packet timed out + } + } else { + // the packet has not timed out, so receive it on the consumer + val result = recvPacketOnConsumer(currentState, receiver, packet) + val tmpState = result.newState + if (result.hasError()) { + (result, false) + } else { + (Ok(removeOutstandingPacketFromProvider(tmpState, receiver)), false) // false because the packet did not time out + } + } + } + } + + + + /// Ends a block on the provider. This means that the current validator set is committed on chain, + /// packets are queued, and the next block is started. Also, consumers that have passed + /// the VscTimeout without responding to a pending vscpacket are dropped. + pure def endAndBeginBlockForProvider( + currentState: ProtocolState, + // by how much the timestamp should be advanced, + // i.e. the timestamp for the next block is oldTimestamp + timeAdvancement + timeAdvancement: Time, + // a set of consumers that were not consumers before, but should be set to running now. + consumersToStart: Set[Chain], + // a set of consumers that were running before, but should be set to stopped now. + // This argument only needs to contain "voluntary" stops - + // forced stops, e.g. because a consumer timed out, + // will be added automatically. + consumersToStop: Set[Chain]): Result = { + // commit the current running validator set on chain + val currentProviderState = currentState.providerState + val newChainState = currentProviderState.chainState.endAndBeginBlockShared(timeAdvancement) + val providerStateAfterTimeAdvancement = currentProviderState.with( + "chainState", newChainState + ) + + val tmpState = currentState.with( + "providerState", providerStateAfterTimeAdvancement + ) + + // check for Vsc timeouts + val timedOutConsumers = getRunningConsumers(providerStateAfterTimeAdvancement).filter( + consumer => + val res = TimeoutDueToVscTimeout(tmpState, consumer) + res._1 + ) + + + // start/stop chains + val res = providerStateAfterTimeAdvancement.consumerStatus.StartStopConsumers( + consumersToStart, + consumersToStop, + timedOutConsumers + ) + val newConsumerStatus = res._1 + val err = res._2 + val providerStateAfterConsumerAdvancement = providerStateAfterTimeAdvancement.with( + "consumerStatus", newConsumerStatus + ) + + // for each consumer we just set to running, set its initial validator set to be the current one on the provider. + val newConsumerStateMap = + tmpState.consumerStates.keys().mapBy( + (consumer) => + if (consumersToStart.contains(consumer)) { + val currentConsumerState = tmpState.consumerStates.get(consumer) + val newConsumerState = currentConsumerState.with( + "chainState", currentConsumerState.chainState.with( + "currentValidatorSet", providerStateAfterConsumerAdvancement.chainState.currentValidatorSet + ) + ) + newConsumerState + } else { + currentState.consumerStates.get(consumer) + } + ) + val newState = tmpState.with( + "providerState", providerStateAfterConsumerAdvancement + ).with( + "consumerStates", newConsumerStateMap + ) + + if (err != "") { + Err(err) + } else { + val providerStateAfterSending = + if (currentProviderState.providerValidatorSetChangedInThisBlock and + // important: check this on the provider state after the consumer advancement, not on the current state. + getRunningConsumers(providerStateAfterConsumerAdvancement).size() > 0) { + providerStateAfterConsumerAdvancement.sendVscPackets() + } else { + providerStateAfterConsumerAdvancement + } + val finalState = newState.with( + "providerState", providerStateAfterSending + ) + Ok(finalState) + } + } + + pure def endAndBeginBlockForConsumer( + currentState: ProtocolState, + chain: Chain, + // by how much the timestamp of the chain should be advanced for the next block + timeAdvancement: Time): Result = { + if (not(currentState.consumerStates.keys().contains(chain))) { + // if the chain is not a consumer, return an error + Err("chain is not a consumer") + } else { + val currentConsumerState = currentState.consumerStates.get(chain) + val newChainState = currentConsumerState.chainState.endAndBeginBlockShared(timeAdvancement) + val newConsumerState = currentConsumerState.with( + "chainState", newChainState + ) + val maturedPackets = newConsumerState.maturationTimes.keys().filter( + packet => + val maturationTime = newConsumerState.maturationTimes.get(packet) + maturationTime <= newChainState.lastTimestamp + ) + val newMaturationTimes = newConsumerState.maturationTimes.mapRemoveAll(maturedPackets) + val newOutstandingPackets = newConsumerState.outstandingPacketsToProvider.concat( + maturedPackets.map( + packet => { + id: packet.id, + sendingTime: newConsumerState.chainState.lastTimestamp + } + ).toList() + ) + val newConsumerState2 = newConsumerState.with( + "maturationTimes", newMaturationTimes + ).with( + "outstandingPacketsToProvider", newOutstandingPackets + ) + val newConsumerStates = currentState.consumerStates.set(chain, newConsumerState2) + val newState = currentState.with( + "consumerStates", newConsumerStates + ) + Ok(newState) + } + } + + // =================== + // 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") + } else { + val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( + (chain) => + if (consumersToTimeout.contains(chain)) { + TIMEDOUT + } else if (consumersToStop.contains(chain)) { + STOPPED + } else { + currentConsumerStatusMap.get(chain) + } + ) + (newConsumerStatusMap, "") + } + } + + // Returns the new ConsumerStatusMap according to the consumers to start. + // The second return is an error string: If it is not equal to "", + // it contains an error message, and the first return should be ignored. + pure def startConsumers( + currentConsumerStatusMap: Chain -> str, + consumersToStart: Set[Chain]): (Chain -> str, str) = { + val nonConsumers = currentConsumerStatusMap.keys().filter( + chain => currentConsumerStatusMap.get(chain) == NOT_CONSUMER + ) + // all consumers to start must be nonConsumers right now, otherwise we have an error + if (consumersToStart.exclude(nonConsumers).size() > 0) { + (currentConsumerStatusMap, "cannot start a consumer that is stopped or already a consumer") + } else { + val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( + (chain) => + if (consumersToStart.contains(chain)) { + RUNNING + } else { + currentConsumerStatusMap.get(chain) + } + ) + (newConsumerStatusMap, "") + } + } + + pure def StartStopConsumers( + currentConsumerStatusMap: Chain -> str, + consumersToStart: Set[Chain], + consumersToStop: Set[Chain], + consumersToTimeout: Set[Chain] + ): (Chain -> str, str) = { + // check if any consumer is both started and stopped + if (consumersToStart.intersect(consumersToStop).size() > 0) { + (currentConsumerStatusMap, "Cannot start and stop a consumer at the same time") + } else { + val res1 = currentConsumerStatusMap.startConsumers(consumersToStart) + val newConsumerStatus = res1._1 + val err1 = res1._2 + val res2 = newConsumerStatus.stopConsumers(consumersToStop, consumersToTimeout) + val err2 = res2._2 + if (err1 != "") { + (currentConsumerStatusMap, err1) + } else if (err2 != "") { + (currentConsumerStatusMap, err2) + } else { + (res2._1, "") + } + } + } + + + // Takes the currentValidatorSet and puts it as the newest set of the voting history + pure def enterCurValSetIntoBlock(chainState: ChainState): ChainState = { + chainState.with( + "votingPowerHistory", chainState.votingPowerHistory.prepend( + chainState.currentValidatorSet + ) + ) + } + + // Advances the timestamp in the chainState by timeAdvancement + pure def advanceTime(chainState: ChainState, timeAdvancement: Time): ChainState = { + chainState.with( + "lastTimestamp", chainState.lastTimestamp + 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 + // * 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): 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: providerState.chainState.lastTimestamp + }) + } 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) + ) + ) + { + ...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 = currentState.consumerStates.get(receiver) + val newConsumerState = + { + ...currentConsumerState, + chainState: currentConsumerState.chainState.with( + "currentValidatorSet", packet.validatorSet + ), + maturationTimes: currentConsumerState.maturationTimes.put( + packet, + currentConsumerState.chainState.lastTimestamp + 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 + ) + 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 + ) + } + + // 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 = 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.lastTimestamp) { + (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, "") + } + } + + // =================== + // ASSUMPTIONS ON MODEL PARAMETERS + // =================== + + run UnbondingPeriodPositiveTest = + UnbondingPeriodPerChain.keys().forall(chain => UnbondingPeriodPerChain.get(chain) > 0) + + run VscTimeoutPositiveTest = + VscTimeout > 0 + + run CcvTimeoutPositiveTest = + CcvTimeout.keys().forall(chain => CcvTimeout.get(chain) > 0) + + run CcvTimeoutLargerThanUnbondingPeriodTest = + CcvTimeout.get(PROVIDER_CHAIN) > UnbondingPeriodPerChain.values().max() + + run ProviderIsNotAConsumerTest = + not(ConsumerChains.contains(PROVIDER_CHAIN)) + + // ccv timeout contains exactly consumers and provider, no other chains + run CcvTimeoutKeysTest = + CcvTimeout.keys() == ConsumerChains.union(Set(PROVIDER_CHAIN)) + + // unbonding period contains exactly consumers and provider, no other chains + run UnbondingPeriodKeysTest = + UnbondingPeriodPerChain.keys() == ConsumerChains.union(Set(PROVIDER_CHAIN)) +} diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt new file mode 100644 index 0000000000..f886fe9e85 --- /dev/null +++ b/tests/difference/core/quint_model/ccv_model.qnt @@ -0,0 +1,494 @@ +// -*- mode: Bluespec; -*- +module ccv_model { + // A basic stateful model that utilizes the CCV protocol. + import ccv_types.* from "./ccv" + import Time.* from "./libraries/Time" + import extraSpells.* from "./libraries/extraSpells" + + pure val consumerChains = Set("consumer1", "consumer2", "consumer3") + pure val chains = consumerChains.union(Set(PROVIDER_CHAIN)) + pure val unbondingPeriods = chains.mapBy(chain => 2 * Week) + pure val ccvTimeouts = chains.mapBy(chain => 3 * Week) + + pure val nodes = Set("node1", "node2", "node3", "node4", "node5", "node6", "node7", "node8", "node9", "node10") + pure val InitialValidatorSet = nodes.mapBy(node => 100) + + import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains).* from "./ccv" + + + var currentState: ProtocolState + + // a type storing the parameters used in actions. + // 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, + // so not all of these fields are relevant to each action. + type Action = + { + kind: str, + consumerChain: Chain, + timeAdvancement: Time, + consumersToStart: Set[Chain], + consumersToStop: Set[Chain], + validator: Node, + newVotingPower: int, + } + + + var trace: List[Action] + + // a few different values for time advancements. + // to keep the number of possible steps small, we only have a few different values. + // Roughly, 1s for very small advances (like between blocks), + // and then longer values for increasingly severe downtime scenarios. + // Note that these can still be combined, so in effect we can get all time advancements by any amount of seconds. + pure val timeAdvancements = Set(1 * Second, 1 * Day, 1 * Week, 4 * Week) + + pure def emptyAction = + { + kind: "", + consumerChain: "", + timeAdvancement: 0 * Second, + consumersToStart: Set(), + consumersToStop: Set(), + validator: "", + newVotingPower: 0, + } + + // step allows the most generic nondeterminism, in particular it becomes relatively likely + // that over a long enough runtime, all consumers would time out by mismatching their time advancements, + // and each endblock has a good chance to stop consumers, ... + // step is thus suited to test also unhappy paths. + action step = any { + all { + runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense + nondet chain = oneOf(runningConsumers) + nondet timeAdvancement = oneOf(timeAdvancements) + EndAndBeginBlockForConsumer(chain, timeAdvancement), + }, + + val consumerStatus = currentState.providerState.consumerStatus + nondet consumersToStart = oneOf(nonConsumers.powerset()) + nondet consumersToStop = oneOf(runningConsumers.powerset()) + nondet timeAdvancement = oneOf(timeAdvancements) + EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), + + nondet node = oneOf(nodes) + // very restricted set of voting powers. exact values are not important, + // and this keeps the state space smaller. + nondet newVotingPower = oneOf(Set(0, 50, 100)) + VotingPowerChange(node, newVotingPower), + + // try to send a packet. we could filter by chains that can actually send, + // but it's probably not much faster than just trying and failing. + all { + runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense + nondet sender = oneOf(runningConsumers) + DeliverVscMaturedPacket(sender), + }, + + // again, we could filter by chains that can actually receive, + // but it's probably not much faster than just trying and failing. + all { + runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense + nondet recciver = oneOf(runningConsumers) + DeliverVscPacket(recciver), + }, + } + + // some utility stateful vals to make invariants easier to define + val providerValidatorHistory = currentState.providerState.chainState.votingPowerHistory + val runningConsumers = getRunningConsumers(currentState.providerState) + val nonConsumers = getNonConsumers(currentState.providerState) + + action init: bool = all { + val providerState = GetEmptyProviderState + val consumerStates = ConsumerChains.mapBy(chain => GetEmptyConsumerState) + val providerStateWithConsumers = providerState.with( + "consumerStatus", + ConsumerChains.mapBy(chain => NOT_CONSUMER) + ).with( + "outstandingPacketsToConsumer", + ConsumerChains.mapBy(chain => List()) + ).with( + "sentVscPacketsToConsumer", + ConsumerChains.mapBy(chain => List()) + ).with( + // set the validator set to be the initial validator set in the history + "chainState", providerState.chainState.with( + "votingPowerHistory", List(InitialValidatorSet) + ).with( + "currentValidatorSet", InitialValidatorSet + ) + ) + currentState' = { + providerState: providerStateWithConsumers, + consumerStates: consumerStates + }, + trace' = List(emptyAction.with("kind", "init")), + } + + action VotingPowerChange(validator: Node, newVotingPower: int): bool = + val result = votingPowerChange(currentState, validator, newVotingPower) + all { + result.hasError() == false, + currentState' = result.newState, + trace' = trace.append(emptyAction.with("kind", "VotingPowerChange").with("validator", validator).with("newVotingPower", newVotingPower)) + } + + // The receiver receives the next outstanding VscPacket from the provider. + // This will time out the consumer if the packet timeout has passed on the receiver. + action DeliverVscPacket(receiver: Chain): bool = + val resultAndTimeout = deliverPacketToConsumer(currentState, receiver) + val result = resultAndTimeout._1 + all { + result.hasError() == false, + currentState' = result.newState, + trace' = trace.append(emptyAction.with("kind", "DeliverVscPacket").with("consumerChain", receiver)) + } + + // The provider receives the next outstanding VscMaturedPacket from the sender. + // This will time out the consumer if the packet timeout has passed on the provider. + action DeliverVscMaturedPacket(sender: Chain): bool = + val resultAndTimeout = deliverPacketToProvider(currentState, sender) + val result = resultAndTimeout._1 + all { + result.hasError() == false, + currentState' = result.newState, + trace' = trace.append(emptyAction.with("kind", "DeliverVscMaturedPacket").with("consumerChain", sender)) + } + + action EndAndBeginBlockForProvider( + timeAdvancement: Time, + consumersToStart: Set[Chain], + consumersToStop: Set[Chain]): bool = + val result = endAndBeginBlockForProvider(currentState, timeAdvancement, consumersToStart, consumersToStop) + all { + result.hasError() == false, + currentState' = result.newState, + trace' = trace.append(emptyAction.with("kind", "EndAndBeginBlockForProvider").with("timeAdvancement", timeAdvancement).with("consumersToStart", consumersToStart).with("consumersToStop", consumersToStop)) + } + + action EndAndBeginBlockForConsumer( + chain: Chain, + timeAdvancement: Time): bool = + val result = endAndBeginBlockForConsumer(currentState, chain, timeAdvancement) + all { + result.hasError() == false, + currentState' = result.newState, + trace' = trace.append(emptyAction.with("kind", "EndAndBeginBlockForConsumer").with("consumerChain", chain).with("timeAdvancement", timeAdvancement)) + } + + // ================== + // INVARIANT CHECKS + // ================== + + + // 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 => + currentState.consumerStates.get(chain).chainState.votingPowerHistory.toSet().forall( + validatorSet => providerValidatorHistory.toSet().contains(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 + val ValUpdatePrecondition = trace[trace.length()-1].kind == "EndAndBeginBlockForProvider" + val ValidatorUpdatesArePropagatedInv = + // 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 is in a sent packet + consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists( + packet => packet.validatorSet == 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 SameVscPacketsInv = + 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 = commonPackets.maxBy(packet => packet.sendingTime) + val oldestCommonPacket = commonPackets.minBy(packet => packet.sendingTime) + // 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 + ) + // these should be the same on both chains + packetsBetween1 == packetsBetween2 + } + } + ) + ) + + // For every ValidatorSetChangePacket received by a consumer chain at + // time t, a MaturedVscPacket is sent back to the provider in the first block + // with a timestamp >= t + UnbondingPeriod + // NOTE: because we remove the maturationTimes entry when we send the packets, + // it suffices to check that there is never an entry in maturationTimes + // that has already matured, i.e. where the maturationTime is smaller-or-equal than the lastTimestamp + val MatureOnTimeInv = + runningConsumers.forall( + consumer => { + val maturationTimes = currentState.consumerStates.get(consumer).maturationTimes + maturationTimes.keys().forall( + // check that the maturation time is in the future + packet => maturationTimes.get(packet) >= currentState.consumerStates.get(consumer).chainState.lastTimestamp + ) + } + ) + + // 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). + // Since we remove sentVscPacketsToConsumer when we receive responses for them, + // we just check that if a sentVscPacket has been sent more than + // VscTimeout ago, the consumer must have been dropped. + // In practice, when this is true, a pending unbonding can mature. + val EventuallyMatureOnProviderInv = + runningConsumers.forall( + consumer => { + val sentPackets = currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet() + sentPackets.forall( + packet => + // consumer still has time to respond + not(packet.sendingTime + VscTimeout < currentState.providerState.chainState.lastTimestamp) or + // consumer was dropped + currentState.providerState.consumerStatus.get(consumer) == STOPPED or + currentState.providerState.consumerStatus.get(consumer) == TIMEDOUT + ) + } + ) + + // ================= + // SANITY CHECKS + // ================= + // some invariants that should fail, + // to check that certain behaviours can be exhibited. + // The name of the invariants is the name of the behaviour + // we want to see, and its definition will *negate* that behaviour, so + // we expect these to fail when checked as invariants. + + // We can run consumers. + val CanRunConsumer = + not(ConsumerChains.exists( + consumer => + currentState.providerState.consumerStatus.get(consumer) == RUNNING + )) + + val CanStopConsumer = + not(ConsumerChains.exists( + consumer => + currentState.providerState.consumerStatus.get(consumer) == STOPPED + )) + + val CanTimeoutConsumer = + not(ConsumerChains.exists( + consumer => + currentState.providerState.consumerStatus.get(consumer) == TIMEDOUT + )) + + val CanSendVscPackets = + not(ConsumerChains.exists( + consumer => + currentState.providerState.outstandingPacketsToConsumer.get(consumer).length() > 0 + )) + + val CanSendVscMaturedPackets = + not(ConsumerChains.exists( + consumer => + currentState.consumerStates.get(consumer).outstandingPacketsToProvider.length() > 0 + )) + + val CanReceiveMaturations = + not(ConsumerChains.exists( + consumer => + currentState.providerState.receivedMaturations.size() > 0 + )) + + // ================== + // MANUAL TEST CASES + // ================== + // Manually written test cases to get confidence in the base operation of the protocol. + + /// Test a simple happy path where: + /// * the consumer chain is set to running + /// * a validator set change happens + /// * a block is ended on the provider, i.e. a packet is sent to the consumer + /// * the consumer receives the packet + /// * the chains wait until the unbonding period is over + /// * the consumer sends a VscMaturedPacket to the provider + /// * the provider receives the VscMaturedPacket + run HappyPathTest: bool = { + init.then( + all { + assert(currentState.providerState.consumerStatus == Map( + "consumer1" -> NOT_CONSUMER, + "consumer2" -> NOT_CONSUMER, + "consumer3" -> NOT_CONSUMER + )), + assert(currentState.providerState.outstandingPacketsToConsumer == Map( + "consumer1" -> List(), + "consumer2" -> List(), + "consumer3" -> List() + )), + assert(currentState.providerState.sentVscPacketsToConsumer == Map( + "consumer1" -> List(), + "consumer2" -> List(), + "consumer3" -> List() + )), + assert(currentState.consumerStates.keys() == consumerChains), + assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet)), + assert(currentState.providerState.chainState.currentValidatorSet == InitialValidatorSet), + assert(currentState.providerState.chainState.lastTimestamp == 0), + VotingPowerChange("node1", 50) + }) + .then( + all { + // the validator set has changed + assert(currentState.providerState.chainState.currentValidatorSet == InitialValidatorSet.put("node1", 50)), + // start consumer1 + EndAndBeginBlockForProvider(1 * Second, Set("consumer1"), Set()) + }) + .then( + all { + // consumer1 was started + assert(currentState.providerState.consumerStatus.get("consumer1") == RUNNING), + // a packet was sent to consumer1 + assert(currentState.providerState.outstandingPacketsToConsumer.get("consumer1").length() == 1), + // the validator set on the provider was entered into the history + assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet.put("node1", 50), InitialValidatorSet)), + // deliver the packet + DeliverVscPacket("consumer1") + } + ) + .then( + all { + // make sure the packet was removed from the provider + assert(currentState.providerState.outstandingPacketsToConsumer.get("consumer1").length() == 0), + // ensure the maturation time was entered on the consumer + assert(currentState.consumerStates.get("consumer1").maturationTimes.keys().size() == 1), + // the validator set was put as the current validator set + assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet == InitialValidatorSet.put("node1", 50)), + // advance time on provider until the unbonding period is over + EndAndBeginBlockForProvider(UnbondingPeriodPerChain.get("consumer1"), Set(), Set()), + } + ) + .then( + // advance time on consumer until the unbonding period is over + EndAndBeginBlockForConsumer("consumer1", UnbondingPeriodPerChain.get("consumer1")) + ) + .then( + all { + // the packet has matured, so it was sent by the consumer + assert(currentState.consumerStates.get("consumer1").outstandingPacketsToProvider.length() == 1), + // it was removed from the maturationTimes + assert(currentState.consumerStates.get("consumer1").maturationTimes.keys().size() == 0), + // receive the packet on the provider + DeliverVscMaturedPacket("consumer1") + } + ) + .then( + all { + // the packet was received on the provider + assert(currentState.providerState.receivedMaturations.size() == 1), + // the packet was removed from the consumer + assert(currentState.consumerStates.get("consumer1").outstandingPacketsToProvider.length() == 0), + VotingPowerChange("node1", 50) // just so this still has an effect + } + ) + } + + /// a manual test case for the SameVscPacketsInv, since it needs very specific behaviour to even apply. + run SameVscPacketsManualTest = + init.then( + // start all consumers except for consumer3 + EndAndBeginBlockForProvider(1 * Second, Set("consumer1", "consumer2"), Set()) + ).then( + // change voting power + VotingPowerChange("node1", 50) + ).then( + // send packet to consumer1 and consumer2 + EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + ).then( + // deliver the packets + DeliverVscPacket("consumer1") + ).then( + // deliver to consumer2 + DeliverVscPacket("consumer2") + ).then( + // start consumer3 + EndAndBeginBlockForProvider(1 * Second, Set("consumer3"), Set()) + ).then( + // do another voting power change + VotingPowerChange("node2", 50) + ).then( + // send packets + EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + ).then( + //deliver to consumer1 + DeliverVscPacket("consumer1") + ).then( + // deliver to consumer2 + DeliverVscPacket("consumer2") + ).then( + // deliver to consumer3 + DeliverVscPacket("consumer3") + ) + .then( + // the SameVscPacketInv should hold here + all { + assert(SameVscPacketsInv), + // action does not matter, but needed to have uniform effect + VotingPowerChange("node1", 50) + } + ) + + // a manual test for the EventuallyMatureOnProvider invariant + run VscTimeoutManualTest = + init + .then( + // start all consumer chains + EndAndBeginBlockForProvider(1 * Second, ConsumerChains, Set()) + ) + .then( + // change voting power + VotingPowerChange("node1", 50) + ) + .then( + // send packets + EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + ) + .then( + // advance time on provider by VscTimeout + 1 Second + EndAndBeginBlockForProvider(VscTimeout + 1 * Second, Set(), Set()) + ) + .then( + all { + // the consumer chains should have timed out + assert(ConsumerChains.forall( + chain => currentState.providerState.consumerStatus.get(chain) == TIMEDOUT + )), + VotingPowerChange("node1", 50) // action needs to be there but does not matter what it is + } + ) +} \ No newline at end of file diff --git a/tests/difference/core/quint_model/ccv_test.qnt b/tests/difference/core/quint_model/ccv_test.qnt new file mode 100644 index 0000000000..6bbe884d52 --- /dev/null +++ b/tests/difference/core/quint_model/ccv_test.qnt @@ -0,0 +1,253 @@ +// -*- mode: Bluespec; -*- + +// contains test logic for the stateless functions in the CCV module +module ccv_test { + import ccv_types.* from "./ccv" + import Time.* from "./libraries/Time" + import extraSpells.* from "./libraries/extraSpells" + + pure val consumerChains = Set("sender", "receiver") + pure val chains = consumerChains.union(Set(PROVIDER_CHAIN)) + pure val unbondingPeriods = chains.mapBy(chain => 2 * Week) + pure val ccvTimeouts = chains.mapBy(chain => 3 * Week) + + import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains).* from "./ccv" + + // negative voting powers give an error + run VotingPowerNegativeTest = + { + votingPowerChange( + GetEmptyProtocolState, + "validator", + -1 + ).hasError() + } + + run VotingPowerOkTest = + { + val result = votingPowerChange( + GetEmptyProtocolState, + "validator", + 5 + ) + not(result.hasError()) and + result.newState.providerState.chainState.currentValidatorSet.keys().contains("validator") and + result.newState.providerState.chainState.currentValidatorSet.get("validator") == 5 + } + + // voting power of 0 is allowed and applied as usual + run VotingPowerZeroTest = + { + val tmpResult = votingPowerChange( + GetEmptyProtocolState, + "validator", + 5 + ) + val finalResult = votingPowerChange( + tmpResult.newState, + "validator", + 0 + ) + not(finalResult.hasError()) and + finalResult.newState.providerState.chainState.currentValidatorSet.get("validator") == 0 + } + + run VotingPowerSetsFlagTest = + { + // change voting power + val tmpResult = votingPowerChange( + GetEmptyProtocolState, + "validator", + 5 + ) + // but then set it back to the initial value + val finalResult = votingPowerChange( + tmpResult.newState, + "validator", + 0 + ) + // still should set the flag + not(finalResult.hasError()) and + finalResult.newState.providerState.providerValidatorSetChangedInThisBlock + } + + + // make sure that VotingPowerChange ONLY changes the current validator set, not the history + run VotingPowerChangeDoesNotChangeHistoryTest = + { + val result = votingPowerChange( + GetEmptyProtocolState, + "validator", + 0 + ) + not(result.hasError()) and + result.newState.providerState.chainState.votingPowerHistory == List() + } + + // Defines a test state to test the deliverPacketToProvider function against. + pure val _DeliverPacketToProvider_TestState = + val currentState = GetEmptyProtocolState + val sender = "sender" + val providerState = currentState.providerState + val consumerState = GetEmptyConsumerState + // add the consumer to the consumerStates + val consumerStates = currentState.consumerStates.put(sender, consumerState) + val providerState2 = providerState.with( + "consumerStatus", providerState.consumerStatus.put(sender, RUNNING) + ) + val providerState3 = providerState2.with( + "outstandingPacketsToConsumer", providerState2.outstandingPacketsToConsumer.put(sender, List({ + id: 0, + validatorSet: Map(), + sendingTime: 0 + })) + ) + currentState.with( + "providerState", providerState3 + ).with( + "consumerStates", consumerStates + ) + + // add a packet on the consumer + pure val DeliverPacketToProviderHappyPathTest_testState = _DeliverPacketToProvider_TestState.with( + "consumerStates", _DeliverPacketToProvider_TestState.consumerStates.put( + "sender", _DeliverPacketToProvider_TestState.consumerStates.get("sender").with( + "outstandingPacketsToProvider", List({ + id: 0, + sendingTime: 0 + }) + ) + ) + ).with( + // put an entry into sentVscPacket on the provider that corresponds to the packet we put on the consumer + "providerState", _DeliverPacketToProvider_TestState.providerState.with( + "sentVscPacketsToConsumer", _DeliverPacketToProvider_TestState.providerState.sentVscPacketsToConsumer.put( + "sender", List({ + id: 0, + validatorSet: _DeliverPacketToProvider_TestState.providerState.chainState.currentValidatorSet, + sendingTime: 0 + }) + ) + ) + ) + + pure val DeliverPacketToProviderHappyPathTest_resultAndTimeout = deliverPacketToProvider(DeliverPacketToProviderHappyPathTest_testState, "sender") + + // test is split to be easier to pinpoint which assertion failed + run DidNotTimeOut_DeliverPacketToProviderHappyPathTest = + { + val result = DeliverPacketToProviderHappyPathTest_resultAndTimeout._1 + val timeout = DeliverPacketToProviderHappyPathTest_resultAndTimeout._2 + not(result.hasError()) and + not(timeout) + } + + run StateModificationOK_DeliverPacketToProviderHappyPathTest = + { + val result = DeliverPacketToProviderHappyPathTest_resultAndTimeout._1 + val newProviderState = result.newState.providerState + val newConsumerState = result.newState.consumerStates.get("sender") + not(result.hasError()) and + newProviderState.receivedMaturations.size() == 1 and + newConsumerState.outstandingPacketsToProvider.length() == 0 + } + + // add a packet on the consumer + pure val DeliverPacketToProviderTimeoutTest_testState = DeliverPacketToProviderHappyPathTest_testState.with( + "providerState", DeliverPacketToProviderHappyPathTest_testState.providerState.with( + "chainState", DeliverPacketToProviderHappyPathTest_testState.providerState.chainState.with( + // set the timestamp to be after the timeout + "lastTimestamp", CcvTimeout.get("sender") + 1 + ) + ) + ) + + pure val DeliverPacketToProviderTimeoutTest_resultAndTimeout = deliverPacketToProvider(DeliverPacketToProviderTimeoutTest_testState, "sender") + + run DidTimeOut_DeliverPacketToProviderTimeoutTest = + { + val result = DeliverPacketToProviderTimeoutTest_resultAndTimeout._1 + val timeout = DeliverPacketToProviderTimeoutTest_resultAndTimeout._2 + val newProviderState = result.newState.providerState + val newConsumerState = result.newState.consumerStates.get("sender") + not(result.hasError()) and + timeout + } + + run StateModificationOK_DeliverPacketToProviderTimeoutTest = + { + val result = DeliverPacketToProviderTimeoutTest_resultAndTimeout._1 + val newProviderState = result.newState.providerState + val newConsumerState = result.newState.consumerStates.get("sender") + not(result.hasError()) and + newProviderState.receivedMaturations.size() == 0 and + newProviderState.consumerStatus.get("sender") == TIMEDOUT + } + + run ConsumerStatusMapHappyPathTest = + { + val currentConsumerStatusMap = Map( + "chain1" -> NOT_CONSUMER, + "chain2" -> RUNNING, + "chain3" -> STOPPED + ) + val res = StartStopConsumers( + currentConsumerStatusMap, + Set("chain1"), + Set("chain2"), + Set() + ) + res._2 == "" and + res._1.get("chain1") == RUNNING and + res._1.get("chain2") == STOPPED and + res._1.get("chain3") == STOPPED + } + + run ConsumerStatusMapAlreadyRunningTest = + { + val currentConsumerStatusMap = Map( + "chain1" -> NOT_CONSUMER, + "chain2" -> RUNNING, + "chain3" -> STOPPED + ) + val res = StartStopConsumers( + currentConsumerStatusMap, + Set("chain2"), + Set("chain3"), + Set() + ) + res._2 == "cannot start a consumer that is stopped or already a consumer" + } + + run ConsumerStatusMapAlreadyStoppedTest = + { + val currentConsumerStatusMap = Map( + "chain1" -> NOT_CONSUMER, + "chain2" -> RUNNING, + "chain3" -> STOPPED + ) + val res = StartStopConsumers( + currentConsumerStatusMap, + Set("chain1"), + Set("chain3"), + Set() + ) + res._2 == "Cannot stop a consumer that is not running" + } + + run ChainBothInStartAndStopTest = + { + val currentConsumerStatusMap = Map( + "chain1" -> NOT_CONSUMER, + "chain2" -> RUNNING, + "chain3" -> STOPPED + ) + val res = StartStopConsumers( + currentConsumerStatusMap, + Set("chain1"), + Set("chain1"), + Set() + ) + res._2 == "Cannot start and stop a consumer at the same time" + } +} \ No newline at end of file diff --git a/tests/difference/core/quint_model/libraries/Time.qnt b/tests/difference/core/quint_model/libraries/Time.qnt new file mode 100644 index 0000000000..a85d97697d --- /dev/null +++ b/tests/difference/core/quint_model/libraries/Time.qnt @@ -0,0 +1,14 @@ +// -*- mode: Bluespec; -*- +// A simple module for time that makes timings more readable, +// e.g. 5 * Minute. +// The base unit are seconds, i.e. to get the number of seconds in a time value, just treat it as an int. +module Time { + type Time = int + + pure val Second = 1 + pure val Minute = 60 * Second + pure val Hour = 60 * Minute + pure val Day = 24 * Hour + pure val Week = 7 * Day + pure val Year = 365 * Day +} \ No newline at end of file diff --git a/tests/difference/core/quint_model/libraries/extraSpells.qnt b/tests/difference/core/quint_model/libraries/extraSpells.qnt new file mode 100644 index 0000000000..cc20c17aef --- /dev/null +++ b/tests/difference/core/quint_model/libraries/extraSpells.qnt @@ -0,0 +1,213 @@ +// -*- mode: Bluespec; -*- + +// This module is just a library with utility functions (sometimes called spells in Quint). +module extraSpells { + + pure def prepend(__list: List[a], __elem: a): List[a] = { + List(__elem).concat(__list) + } + + run prependTest = all { + assert(List(2,3,4).prepend(1) == List(1,2,3,4)), + assert(List().prepend(1) == List(1)), + } + + /// An annotation for writing preconditions. + /// - @param __cond condition to check + /// - @returns true if and only if __cond evaluates to true + pure def require(__cond: bool): bool = __cond + + run requireTest = all { + assert(require(4 > 3)), + assert(not(require(false))), + } + + /// A convenience operator that returns a string error code, + /// if the condition does not hold true. + /// + /// - @param __cond condition to check + /// - @param __error a non-empty error message + /// - @returns "", when __cond holds true; otherwise __error + pure def requires(__cond: bool, __error: str): str = { + if (__cond) "" else __error + } + + run requiresTest = all { + assert(requires(4 > 3, "4 > 3") == ""), + assert(requires(4 < 3, "false: 4 < 3") == "false: 4 < 3"), + } + + /// Compute the absolute value of an integer + /// + /// - @param __i : an integer whose absolute value we are interested in + /// - @returns |__i|, the absolute value of __i + pure def abs(__i: int): int = { + if (__i < 0) -__i else __i + } + + run absTest = all { + assert(abs(3) == 3), + assert(abs(-3) == 3), + assert(abs(0) == 0), + } + + /// Remove a set element. + /// + /// - @param __set a set to remove an element from + /// - @param __elem an element to remove + /// - @returns a new set that contains all elements of __set but __elem + pure def setRemove(__set: Set[a], __elem: a): Set[a] = { + __set.exclude(Set(__elem)) + } + + run setRemoveTest = all { + assert(Set(2, 4) == Set(2, 3, 4).setRemove(3)), + assert(Set() == Set().setRemove(3)), + } + + /// Test whether a key is present in a map + /// + /// - @param __map a map to query + /// - @param __key the key to look for + /// - @returns true if and only __map has an entry associated with __key + pure def has(__map: a -> b, __key: a): bool = { + __map.keys().contains(__key) + } + + run hasTest = all { + assert(Map(2 -> 3, 4 -> 5).has(2)), + assert(not(Map(2 -> 3, 4 -> 5).has(6))), + } + + /// Get the map value associated with a key, or the default, + /// if the key is not present. + /// + /// - @param __map the map to query + /// - @param __key the key to search for + /// - @returns the value associated with the key, if __key is + /// present in the map, and __default otherwise + pure def getOrElse(__map: a -> b, __key: a, __default: b): b = { + if (__map.has(__key)) { + __map.get(__key) + } else { + __default + } + } + + run getOrElseTest = all { + assert(Map(2 -> 3, 4 -> 5).getOrElse(2, 0) == 3), + assert(Map(2 -> 3, 4 -> 5).getOrElse(7, 11) == 11), + } + + /// Remove a map entry. + /// + /// - @param __map a map to remove an entry from + /// - @param __key the key of an entry to remove + /// - @returns a new map that contains all entries of __map + /// that do not have the key __key + pure def mapRemove(__map: a -> b, __key: a): a -> b = { + __map.keys().setRemove(__key).mapBy(__k => __map.get(__k)) + } + + run mapRemoveTest = all { + assert(Map(3 -> 4, 7 -> 8) == Map(3 -> 4, 5 -> 6, 7 -> 8).mapRemove(5)), + assert(Map() == Map().mapRemove(3)), + } + + /// Removes a set of map entry. + /// + /// - @param __map a map to remove an entry from + /// - @param __keys a set of keys to remove from the map + /// - @returns a new map that contains all entries of __map + /// that do not have a key in __keys + pure def mapRemoveAll(__map: a -> b, __keys: Set[a]): a -> b = { + __map.keys().exclude(__keys).mapBy(__k => __map.get(__k)) + } + + run mapRemoveAllTest = + val m = Map(3 -> 4, 5 -> 6, 7 -> 8) + all { + assert(m.mapRemoveAll(Set(5, 7)) == Map(3 -> 4)), + assert(m.mapRemoveAll(Set(5, 99999)) == Map(3 -> 4, 7 -> 8)), + } + + //// Returns a list of all elements of a set. + //// + //// - @param __set a set + //// - @returns a list of all elements of __set + pure def toList(__set: Set[a]): List[a] = { + __set.fold(List(), (__l, __e) => __l.append(__e)) + } + + //// Returns a set of the elements in the list. + //// + //// - @param __list a list + //// - @returns a set of the elements in __list + pure def toSet(__list: List[a]): Set[a] = { + __list.foldl(Set(), (__s, __e) => __s.union(Set(__e))) + } + + run toListAndSetTest = + all { + assert(Set(3, 2, 1).toList().toSet() == Set(1, 2, 3)), + assert(List(2,3,1).toSet() == Set(1, 2, 3)), + assert(List(2,3,1).toSet() == List(3,2,1).toSet()), + assert(toList(Set()) == List()), + assert(toSet(List()) == Set()) + } + + pure def add(__set: Set[a], elem: a): Set[a] = { + __set.union(Set(elem)) + } + + pure def values(__map: a -> b): Set[b] = { + __map.keys().fold(Set(), (__s, __k) => __s.add(__map.get(__k))) + } + run valuesTest = + all { + assert(values(Map(1 -> 2, 3 -> 4)) == Set(2, 4)), + assert(values(Map()) == Set()) + } + + // Returns the maximal element of the set. + // If the set is empty, the function call will fail at runtime. + pure def max(__set: Set[int]): int = maxBy(__set, __a => __a) + + run maxTest = + all { + assert(max(Set(1, 2, 3)) == 3), + } + + // Returns the minimal element of the set. + // If the set is empty, the function call will fail at runtime. + pure def min(__set: Set[int]): int = minBy(__set, __a => __a) + + run minTest = + all { + assert(min(Set(1, 2, 3)) == 1), + } + + // Returns the maximum element of a set, according to a given function. + // If two elements are equally large, an arbitrary one will be returned. + // If the set is empty, the function call will fail at runtime. + pure def maxBy(__set: Set[a], __f: a => int): a = { + __set.fold( + oneOf(__set), + (__m, __e) => if(__f(__m) > __f(__e)) {__m } else {__e} + ) + } + + run maxByTest = + all { + assert(maxBy(Set(1, 2, 3), __x => __x) == 3), + assert(maxBy(Set(1, 2, 3), __x => -__x) == 1), + } + + // Like maxBy, but returns the minimum element. + pure def minBy(__set: Set[a], __f: a => int): a = { + __set.fold( + oneOf(__set), + (__m, __e) => if(__f(__m) < __f(__e)) {__m } else {__e} + ) + } +} diff --git a/tests/difference/core/quint_model/run_invariants.sh b/tests/difference/core/quint_model/run_invariants.sh new file mode 100755 index 0000000000..4c65693cc0 --- /dev/null +++ b/tests/difference/core/quint_model/run_invariants.sh @@ -0,0 +1,4 @@ +#! /bin/sh + +quint test ccv_model.qnt +quint run --invariant "all{ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_model.qnt --max-steps 500 --max-samples 200 \ No newline at end of file