diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md new file mode 100644 index 0000000000..30de96350f --- /dev/null +++ b/tests/difference/core/quint_model/README.md @@ -0,0 +1,20 @@ +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. + diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt index 65a3418e4e..fbb9b08fed 100644 --- a/tests/difference/core/quint_model/ccv.qnt +++ b/tests/difference/core/quint_model/ccv.qnt @@ -1,5 +1,5 @@ module CCVTypes { - import Time.* from "./Time" + import Time.* from "./libraries/Time" type Node = str type Chain = str @@ -213,8 +213,8 @@ module CCV { // 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 extraSpells.* from "./extraSpells" - import Time.* from "./Time" + import Time.* from "./libraries/Time" + import extraSpells.* from "./libraries/extraSpells" import CCVTypes.* @@ -788,412 +788,3 @@ module CCV { run UnbondingPeriodKeysTest = UnbondingPeriodPerChain.keys() == ConsumerChains.union(Set(PROVIDER_CHAIN)) } - - -module CCVDefaultStateMachine { - // A basic state machine that utilizes the CCV protocol. - import Time.* from "./Time" - import CCVTypes.* - import extraSpells.* from "./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).* - - - var currentState: ProtocolState - - 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 - } - } - - action VotingPowerChange(validator: Node, newVotingPower: int): bool = - val result = votingPowerChange(currentState, validator, newVotingPower) - all { - result.hasError == false, - currentState' = result.newState, - } - - // 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, - } - - // 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, - } - - 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, - } - - action EndAndBeginBlockForConsumer( - chain: Chain, - timeAdvancement: Time): bool = - val result = endAndBeginBlockForConsumer(currentState, chain, timeAdvancement) - all { - result.hasError == false, - currentState' = result.newState, - } - - // 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 - } - ) - } - - -} - -// contains test logic for the stateless functions in the CCV module -module CCVLogicTest { - import CCVTypes.* - import Time.* from "./Time" - import extraSpells.* from "./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).* - - // 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 = getNewConsumerStatusMap( - 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 = getNewConsumerStatusMap( - currentConsumerStatusMap, - Set("chain2"), - Set("chain3") - ) - res._2 == "Cannot start a consumer that is already running" - } - - run ConsumerStatusMapAlreadyStoppedTest = - { - val currentConsumerStatusMap = Map( - "chain1" -> UNUSED, - "chain2" -> RUNNING, - "chain3" -> STOPPED - ) - val res = getNewConsumerStatusMap( - 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 = getNewConsumerStatusMap( - currentConsumerStatusMap, - Set("chain1"), - Set("chain1") - ) - res._2 == "Cannot start and stop a consumer at the same time" - } -} 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..142db75431 --- /dev/null +++ b/tests/difference/core/quint_model/ccv_statemachine.qnt @@ -0,0 +1,220 @@ +module CCVDefaultStateMachine { + // A basic state machine that utilizes the CCV protocol. + import Time.* from "./libraries/time" + import extraSpells.* from "./libraries/extraSpells" + import CCVTypes.* from "./ccv" + + 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 + + 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 + } + } + + action VotingPowerChange(validator: Node, newVotingPower: int): bool = + val result = votingPowerChange(currentState, validator, newVotingPower) + all { + result.hasError == false, + currentState' = result.newState, + } + + // 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, + } + + // 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, + } + + 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, + } + + action EndAndBeginBlockForConsumer( + chain: Chain, + timeAdvancement: Time): bool = + val result = endAndBeginBlockForConsumer(currentState, chain, timeAdvancement) + all { + result.hasError == false, + currentState' = result.newState, + } + + 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(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(1 * Second, 1 * Day, 1 * Week, 1 * Month) + EndAndBeginBlockForConsumer(chain, timeAdvancement), + + val runningConsumers = currentState.providerState.consumerStatus.filter((chain, status) => status == RUNNING).keys() + val unusedConsumers = currentState.providerState.consumerStatus.filter((chain, status) => status == UNUSED).keys() + nondet consumersToStart = oneOf(runningConsumers.powerset()) + nondet consumersToStop = oneOf(unusedConsumers.powerset()) + nondet timeAdvancement = oneOf(1 * Second, 1 * Day, 1 * Week, 1 * Month) + 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), + } + + // ================== + // 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 + } + ) + } +} \ 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..31c46c0e62 --- /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 = getNewConsumerStatusMap( + 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 = getNewConsumerStatusMap( + currentConsumerStatusMap, + Set("chain2"), + Set("chain3") + ) + res._2 == "Cannot start a consumer that is already running" + } + + run ConsumerStatusMapAlreadyStoppedTest = + { + val currentConsumerStatusMap = Map( + "chain1" -> UNUSED, + "chain2" -> RUNNING, + "chain3" -> STOPPED + ) + val res = getNewConsumerStatusMap( + 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 = getNewConsumerStatusMap( + 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/extraSpells.qnt b/tests/difference/core/quint_model/libraries/extraSpells.qnt similarity index 100% rename from tests/difference/core/quint_model/extraSpells.qnt rename to tests/difference/core/quint_model/libraries/extraSpells.qnt diff --git a/tests/difference/core/quint_model/time.qnt b/tests/difference/core/quint_model/libraries/time.qnt similarity index 100% rename from tests/difference/core/quint_model/time.qnt rename to tests/difference/core/quint_model/libraries/time.qnt