diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md new file mode 100644 index 0000000000..6d1ad8d2be --- /dev/null +++ b/tests/difference/core/quint_model/README.md @@ -0,0 +1,37 @@ +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_statemachine.qnt: Contains the state machine layer 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. +- libararies/*: 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. + +### Invariants + +The invariants I am checking are in ccv_statemachine.qnt. +Check a single invariant by running +`quint run --invariant INVARIANT_NAME ccv_statemachine.qnt --main CCVDefaultStateMachine`, +or all invariants by running this command: + +Invariants are as follows: +- ValidatorUpdatesArePropagated: When a validator power update is comitted on chain, a packet containing that change in voting power is sent to all running consumers. +- ValidatorSetHasExistedInv: Every validator set on consumer chains is/was a validator set on the provider. +- 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. +- 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. diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt new file mode 100644 index 0000000000..72a0e0d933 --- /dev/null +++ b/tests/difference/core/quint_model/ccv.qnt @@ -0,0 +1,846 @@ +module CCVTypes { + 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 which VSC Packets have been sent to compare with receivedMaturations to detect timeouts due to non-responsiveness + sentVSCPackets: 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 - + // unused, 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(), + sentVSCPackets: 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 == UNUSED or STOPPED. + consumerStates: Chain -> ConsumerState + } + + // gets a protocol state that is initialized minimally. + pure def GetEmptyProtocolState(): ProtocolState = + { + providerState: GetEmptyProviderState, + consumerStates: Map(), + } + + type Error = { + message: 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 = { + hasError: bool, + newState: ProtocolState, + error: Error + } + + pure def Ok(newState: ProtocolState): Result = { + { + hasError: false, + newState: newState, + error: { + message: "" + } + } + } + + pure def Err(msg: str): Result = { + { + hasError: true, + newState: { + providerState: { + chainState: { + votingPowerHistory: List(), + currentValidatorSet: Map(), + lastTimestamp: 0, + }, + outstandingPacketsToConsumer: Map(), + receivedMaturations: Set(), + sentVSCPackets: Map(), + providerValidatorSetChangedInThisBlock: false, + consumerStatus: Map(), + runningVscId: 0, + }, + consumerStates: Map(), + }, + error: { + message: msg + } + } + } + + // possible consumer statuses + pure val STOPPED = "stopped" // the chain was once a consumer chain, but has been dropped by the provider. + pure val RUNNING = "running" // the chain is currently a consumer chain. Running chains are those that get sent VSCPackets. + pure val UNUSED = "unused" // 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 CCVTypes.* + + + // =================== + // 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 positive") + } else { + pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet + pure val newValidatorSet = getUpdatedValidatorSet(currentValidatorSet, 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. + // Only argument is 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(isCurrentlyConsumer(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 the packet has timed out, drop the consumer. its state doesn't matter anymore + val timeout = CcvTimeout.get(sender) + if(packet.sendingTime + CcvTimeout.get(sender) < currentState.providerState.chainState.lastTimestamp) { + // drop consumer + val result = stopConsumers( + currentState.providerState.consumerStatus, + 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) { + (Err(result.error.message), false) + } else { + val result2 = removeOutstandingPacketFromConsumer(tmpState, sender) + val tmpState2 = result2.newState + val err2 = result2.error + if (result2.hasError) { + (Err(err2.message), false) + } else { + (Ok(tmpState2), false) // false because the packet did not time out + } + } + } + } + } + + // 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 + ) + + // Delivers the next queued VSCPacket from the provider chain to a consumer chain. + // Only argument is 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(isCurrentlyConsumer(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(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) { + (Err(result.error.message), false) + } else { + val result2 = removeOutstandingPacketFromProvider(tmpState, receiver) + val tmpState2 = result2.newState + val err2 = result2.error + if (result2.hasError) { + (Err(err2.message), false) + } else { + (Ok(tmpState2), 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 unused 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 + ) + + // check for VSC timeouts + val timedOutConsumers = getRunningConsumers(providerStateAfterTimeAdvancement).filter( + consumer => + val res = TimeoutDueToVSCTimeout(currentState, consumer) + res._1 + ) + + // start/stop chains + val res = providerStateAfterTimeAdvancement.consumerStatus.StartStopConsumers( + consumersToStart, + consumersToStop + ) + val newConsumerStatus = res._1 + val err = res._2 + val providerStateAfterConsumerAdvancement = providerStateAfterTimeAdvancement.with( + "consumerStatus", newConsumerStatus + ) + 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 newState = currentState.with( + "providerState", providerStateAfterSending + ) + Ok(newState) + } + } + + pure def endAndBeginBlockForConsumer( + currentState: ProtocolState, + chain: Chain, + // by how much the timestamp of the chain should be advanced for the next block + timeAdvancement: Time): Result = { + if (not(currentState.consumerStates.keys().contains(chain))) { + Err("chain is not a consumer") + } else { + // if the chain is not a consumer, return an error + 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 + // =================== + + pure def getRunningConsumersFromMap(consumerStatus: Chain -> str): Set[Chain] = { + consumerStatus.keys().filter( + chain => consumerStatus.get(chain) == RUNNING + ) + } + + pure def getStoppedConsumersFromMap(consumerStatus: Chain -> str): Set[Chain] = { + consumerStatus.keys().filter( + chain => consumerStatus.get(chain) == STOPPED + ) + } + + // Returns the new ConsumerStatusMap according to the consumers to stop. + // 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]): (Chain -> str, str) = { + val runningConsumers = currentConsumerStatusMap.keys().filter( + chain => currentConsumerStatusMap.get(chain) == RUNNING + ) + // if a consumer is both started and stopped, this is an error + // if a consumer is stopped, it must be running + if (consumersToStop.exclude(runningConsumers).size() > 0) { + (currentConsumerStatusMap, "Cannot stop a consumer that is not running") + } else { + // if a consumer is started, it must be unused + val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( + (chain) => + 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 unusedConsumers = currentConsumerStatusMap.keys().filter( + chain => currentConsumerStatusMap.get(chain) == UNUSED + ) + // if a consumer is both started and stopped, this is an error + // if a consumer is stopped, it must be running + if (consumersToStart.exclude(unusedConsumers).size() > 0) { + (currentConsumerStatusMap, "cannot start a consumer that is not unused") + } else { + // if a consumer is started, it must be unused + 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] + ): (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) + 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 + isCurrentlyConsumer(consumer, providerState)) { + List({ + id: providerState.runningVscId, + validatorSet: providerState.chainState.currentValidatorSet, + sendingTime: providerState.chainState.lastTimestamp + }) + } else { + List() + } + ) + providerState.with( + // send VSCPackets to consumers + "outstandingPacketsToConsumer", + ConsumerChains.mapBy( + (consumer) => + providerState.outstandingPacketsToConsumer.get(consumer).concat( + newSentPacketsPerConsumer.get(consumer) + ) + ) + ).with( + // update the sent VSCPackets + "sentVSCPackets", + ConsumerChains.mapBy( + (consumer) => + providerState.sentVSCPackets.get(consumer).concat( + newSentPacketsPerConsumer.get(consumer) + ) + ) + ).with( + // the validator set has not changed yet in the new block + "providerValidatorSetChangedInThisBlock", false + ).with( + "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(isCurrentlyConsumer(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.with( + "chainState", + currentConsumerState.chainState.with( + "currentValidatorSet", packet.validatorSet + ) + ).with( + "maturationTimes", + currentConsumerState.maturationTimes.put( + packet, + currentConsumerState.chainState.lastTimestamp + UnbondingPeriodPerChain.get(receiver) + ) + ).with( + "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(isCurrentlyConsumer(sender, currentState.providerState))) { + Err("Sender is not currently a consumer - must have 'running' status!") + } else if (currentState.providerState.sentVSCPackets.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.sentVSCPackets.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): Result = { + 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 + ) + Ok(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): Result = { + 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 + ) + Ok(newState) + } + + // Updates the given oldValidatorSet by setting the validator to newVotingPower. + // If newVotingPower is zero, the validator is removed. + pure def getUpdatedValidatorSet(oldValidatorSet: ValidatorSet, validator: Node, newVotingPower: int): ValidatorSet = + if (newVotingPower > 0) + oldValidatorSet.put(validator, newVotingPower) + else + oldValidatorSet.mapRemove(validator) + + // 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 isCurrentlyConsumer(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 UNUSED. + pure def getUnusedConsumers(providerState: ProviderState): Set[Chain] = { + providerState.consumerStatus.keys().filter( + chain => providerState.consumerStatus.get(chain) == UNUSED + ) + } + + // 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(isCurrentlyConsumer(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 sentVSCPackets = providerState.sentVSCPackets.get(consumer) + val oldestSentVSCPacket = sentVSCPackets.head() // if length is 0, this is undefined, but we check for this before we use it + if(sentVSCPackets.length() > 0 and oldestSentVSCPacket.sendingTime + VscTimeout < providerState.chainState.lastTimestamp) { + (true, "") + } else { + // no timeout yet, it has not been VscTimeout since that packet was sent + (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_statemachine.qnt b/tests/difference/core/quint_model/ccv_statemachine.qnt new file mode 100644 index 0000000000..4a6ac2e558 --- /dev/null +++ b/tests/difference/core/quint_model/ccv_statemachine.qnt @@ -0,0 +1,364 @@ +module CCVDefaultStateMachine { + // A basic state machine that utilizes the CCV protocol. + import CCVTypes.* 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 + + // bookkeeping + var lastAction: str + + // some utility stateful vals to make invariants easier to define + val providerValidatorHistory = currentState.providerState.chainState.votingPowerHistory + val runningConsumers = getRunningConsumers(currentState.providerState) + val unusedConsumers = getUnusedConsumers(currentState.providerState) + + action init: bool = all { + val providerState = GetEmptyProviderState + val consumerStates = ConsumerChains.mapBy(chain => GetEmptyConsumerState) + val providerStateWithConsumers = providerState.with( + "consumerStatus", + ConsumerChains.mapBy(chain => UNUSED) + ).with( + "outstandingPacketsToConsumer", + ConsumerChains.mapBy(chain => List()) + ).with( + "sentVSCPackets", + 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 + }, + lastAction' = "init" + } + + action VotingPowerChange(validator: Node, newVotingPower: int): bool = + val result = votingPowerChange(currentState, validator, newVotingPower) + all { + result.hasError == false, + currentState' = result.newState, + lastAction' = "VotingPowerChange" + } + + // 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, + lastAction' = "DeliverVSCPacket" + } + + // 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, + lastAction' = "DeliverVSCMaturedPacket" + } + + 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, + lastAction' = "EndAndBeginBlockForProvider" + } + + action EndAndBeginBlockForConsumer( + chain: Chain, + timeAdvancement: Time): bool = + val result = endAndBeginBlockForConsumer(currentState, chain, timeAdvancement) + all { + result.hasError == false, + currentState' = result.newState, + lastAction' = "EndAndBeginBlockForConsumer" + } + + // 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) + + action step = any { + nondet node = oneOf(nodes) + // very restricted set of voting powers. exact values are not important, + // and this keeps the state space smaller. + // 0 for getting a validator out of the validator set, and two non-zero values + nondet newVotingPower = oneOf(Set(0, 50, 100)) + VotingPowerChange(node, newVotingPower), + + nondet chain = oneOf(consumerChains) + // 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. + nondet timeAdvancement = oneOf(timeAdvancements) + EndAndBeginBlockForConsumer(chain, timeAdvancement), + + val consumerStatus = currentState.providerState.consumerStatus + nondet consumersToStart = oneOf(runningConsumers.powerset()) + nondet consumersToStop = oneOf(unusedConsumers.powerset()) + nondet timeAdvancement = oneOf(timeAdvancements) + EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), + + // + // 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. + nondet sender = oneOf(consumerChains) + DeliverVSCMaturedPacket(sender), + + // again, we could filter by chains that can actually receive, + // but it's probably not much faster than just trying and failing. + nondet recciver = oneOf(consumerChains) + DeliverVSCPacket(recciver), + } + + // ================== + // 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 ValidatorUpdatesArePropagated = + // when the provider has just entered a validator set into a block... + if (lastAction == "EndAndBeginBlockForProvider") { + val providerValSetInCurBlock = providerValidatorHistory.head() + // ... for each consumer that is running then ... + runningConsumers.forall( + // ...the validator set is in a sent packet + consumer => currentState.providerState.sentVSCPackets.get(consumer).toSet().exists( + packet => packet.validatorSet == providerValSetInCurBlock + ) + ) + } else { + true + } + + // 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 oldestCommonPacket = packets1.head() + val newestCommonPacket = packets1[packets1.length() - 1] + // 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 is older than the current time minus the unbonding period. + val MatureOnTimeInv = + runningConsumers.forall( + consumer => { + val maturationTimes = currentState.consumerStates.get(consumer).maturationTimes + maturationTimes.keys().forall( + packet => packet.sendingTime + UnbondingPeriodPerChain.get(consumer) <= currentState.providerState.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 sentVSCPackets 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.sentVSCPackets.get(consumer).toSet() + sentPackets.forall( + packet => + // consumer still has time to respond + currentState.providerState.chainState.lastTimestamp <= packet.sendingTime + VscTimeout or + // consumer was dropped due to inactivity + currentState.providerState.consumerStatus.get(consumer) == STOPPED + ) + } + ) + +// \* Invariants from https://github.com/cosmos/interchain-security/blob/main/docs/quality_assurance.md + +// (* +// 7.01 - 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 + +// Modification: not necessarily _first_ block with that timestamp, +// since we don't model height _and_ time. Also, only true for ACTIVE chains. +// *) +// Inv701 == +// boundedDrift => MaturedBeforeTimeout + +// (* +// 7.02 - If an unbonding operation resulted in a ValidatorSetChangePacket sent +// to all registered consumer chains, then it cannot complete before receiving +// matching MaturedVSCPackets from these consumer chains +// (unless some of these consumer chains are removed) + +// We can define change completion, but we don't model it. Best approximation: +// *) +// Inv702 == +// boundedDrift => EventuallyMatureOnProvider + + // ================== + // 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" -> UNUSED, + "consumer2" -> UNUSED, + "consumer3" -> UNUSED + )), + assert(currentState.providerState.outstandingPacketsToConsumer == Map( + "consumer1" -> List(), + "consumer2" -> List(), + "consumer3" -> List() + )), + assert(currentState.providerState.sentVSCPackets == 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), + currentState' = currentState, // just so this still has an effect + lastAction' = "HappyPathTest" + } + ) + } +} \ 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..d84d8f0ea4 --- /dev/null +++ b/tests/difference/core/quint_model/ccv_test.qnt @@ -0,0 +1,225 @@ +// contains test logic for the stateless functions in the CCV module +module CCVTest { + import CCVTypes.* 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 + } + + // validators that get zero voting power are removed + run VotingPowerZeroTest = + { + val tmpResult = votingPowerChange( + GetEmptyProtocolState, + "validator", + 5 + ) + val finalResult = votingPowerChange( + tmpResult.newState, + "validator", + 0 + ) + not(finalResult.hasError) and + not(finalResult.newState.providerState.chainState.currentValidatorSet.keys().contains("validator")) + } + + 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() + } + + // 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( + "sentVSCPackets", _DeliverPacketToProvider_TestState.providerState.sentVSCPackets.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 timedOut = DeliverPacketToProviderHappyPathTest_resultAndTimeout._2 + 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 timedOut = DeliverPacketToProviderTimeoutTest_resultAndTimeout._2 + val newProviderState = result.newState.providerState + val newConsumerState = result.newState.consumerStates.get("sender") + not(result.hasError) and + timedOut + } + + run StateModificationOK_DeliverPacketToProviderTimeoutTest = + { + val result = DeliverPacketToProviderTimeoutTest_resultAndTimeout._1 + val timedOut = DeliverPacketToProviderTimeoutTest_resultAndTimeout._2 + 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") == STOPPED + } + + run ConsumerStatusMapHappyPathTest = + { + val currentConsumerStatusMap = Map( + "chain1" -> UNUSED, + "chain2" -> RUNNING, + "chain3" -> STOPPED + ) + val res = StartStopConsumers( + currentConsumerStatusMap, + Set("chain1"), + Set("chain2") + ) + 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" -> UNUSED, + "chain2" -> RUNNING, + "chain3" -> STOPPED + ) + val res = StartStopConsumers( + currentConsumerStatusMap, + Set("chain2"), + Set("chain3") + ) + res._2 == "cannot start a consumer that is not unused" + } + + run ConsumerStatusMapAlreadyStoppedTest = + { + val currentConsumerStatusMap = Map( + "chain1" -> UNUSED, + "chain2" -> RUNNING, + "chain3" -> STOPPED + ) + val res = StartStopConsumers( + currentConsumerStatusMap, + Set("chain1"), + Set("chain3") + ) + res._2 == "Cannot stop a consumer that is not running" + } + + run ChainBothInStartAndStopTest = + { + val currentConsumerStatusMap = Map( + "chain1" -> UNUSED, + "chain2" -> RUNNING, + "chain3" -> STOPPED + ) + val res = StartStopConsumers( + currentConsumerStatusMap, + Set("chain1"), + Set("chain1") + ) + 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..8497d8e1d3 --- /dev/null +++ b/tests/difference/core/quint_model/libraries/Time.qnt @@ -0,0 +1,13 @@ +// 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..54b5feca09 --- /dev/null +++ b/tests/difference/core/quint_model/libraries/extraSpells.qnt @@ -0,0 +1,246 @@ +// 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 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 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()) + } + + pure def Max(__set: Set[int]): int = { + __set.fold(0, (__m, __e) => max(__m, __e)) + } + + run MaxTest = + all { + assert(Max(Set(1, 2, 3)) == 3), + assert(Max(Set()) == 0) + } + + pure def HasSubsequence(__this: List[a], __other: List[a]): bool = { + if(__other.length() > __this.length()) { + false + } else { + 0.to(__this.length() - __other.length()) // go through all possible starting points of __other in __this + .exists( + __start => __this.slice(__start, __start + __other.length()) == __other + ) + } + } + + run HasSubsequenceTest = + all { + assert(List(1, 2, 3, 4).HasSubsequence(List(1, 2))), + assert(List(1, 2, 3, 4).HasSubsequence(List(2, 3))), + assert(List(1, 2, 3, 4).HasSubsequence(List(3, 4))), + assert(List(1, 2, 3, 4).HasSubsequence(List(1, 2, 3))), + assert(not(List(1, 2, 3, 4).HasSubsequence(List(1, 3)))), + assert(not(List().HasSubsequence(List(1)))), + assert(List().HasSubsequence(List())), + assert(List(1).HasSubsequence(List())), + assert(List(1).HasSubsequence(List(1))), + } + + // Returns the maximum element of a set, according to a given function. + // __i should be part of the set if it is nonempty. If the set is empty, __i will be returned. + // If two elements are equally large, an arbitrary one will be returned. + pure def MaxBy(__set: Set[a], __f: a => int, __i: a): a = { + __set.fold( + __i, + (__m, __e) => if(__f(__m) > __f(__e)) {__m } else {__e} + ) + } + + run MaxByTest = + all { + assert(MaxBy(Set(1, 2, 3), __x => __x, 0) == 3), + assert(MaxBy(Set(1, 2, 3), __x => -__x, 0) == 1), + assert(MaxBy(Set(), __x => __x, 0) == 0), + } + + // Like MaxBy, but returns the minimum element. + pure def MinBy(__set: Set[a], __f: a => int, __i: a): a = { + __set.fold( + __i, + (__m, __e) => if(__f(__m) < __f(__e)) {__m } else {__e} + ) + } +}