From 13a32fcb5898d361105cd055600674b629b64000 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Wed, 11 Oct 2023 11:39:06 +0200 Subject: [PATCH] Rename modules to have same name as files --- tests/difference/core/quint_model/ccv.qnt | 6 +- .../core/quint_model/ccv_statemachine.qnt | 181 +++++++++++------- .../difference/core/quint_model/ccv_test.qnt | 6 +- 3 files changed, 114 insertions(+), 79 deletions(-) diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt index dd9107695d..2b975d6c53 100644 --- a/tests/difference/core/quint_model/ccv.qnt +++ b/tests/difference/core/quint_model/ccv.qnt @@ -1,5 +1,5 @@ // -*- mode: Bluespec; -*- -module CCVTypes { +module ccv_types { import Time.* from "./libraries/Time" type Node = str @@ -204,7 +204,7 @@ module CCVTypes { pure val PROVIDER_CHAIN = "provider" } -module CCV { +module ccv { // Implements the core logic of the cross-chain validation protocol. // Things that are not modelled: @@ -222,7 +222,7 @@ module CCV { import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" - import CCVTypes.* + import ccv_types.* // =================== diff --git a/tests/difference/core/quint_model/ccv_statemachine.qnt b/tests/difference/core/quint_model/ccv_statemachine.qnt index a15ed2c830..26e365a398 100644 --- a/tests/difference/core/quint_model/ccv_statemachine.qnt +++ b/tests/difference/core/quint_model/ccv_statemachine.qnt @@ -1,7 +1,7 @@ // -*- mode: Bluespec; -*- -module CCVDefaultStateMachine { +module ccv_statemachine { // A basic state machine that utilizes the CCV protocol. - import CCVTypes.* from "./ccv" + import ccv_types.* from "./ccv" import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" @@ -13,13 +13,98 @@ module CCVDefaultStateMachine { 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" + import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains).* from "./ccv" var currentState: ProtocolState + + + pure def ACTIONS = Set( + "VotingPowerChange", + "DeliverVscPacket", + "DeliverVscMaturedPacket", + "EndAndBeginBlockForProvider", + "EndAndBeginBlockForConsumer" + ) + + // a type storing the parameters used in actions. + // this is used in the trace to store + // the name of the last action, plus the parameters we passed to it. + // Note: This type holds ALL parameters that are used in ANY action, + // so not all of these fields are relevant to each action. + type Action = + { + kind: str, + consumerChain: Chain, + timeAdvancement: Time, + consumersToStart: Set[Chain], + consumersToStop: Set[Chain], + validator: Node, + newVotingPower: int, + } - // bookkeeping - var trace: List[str] + + var trace: List[Action] + + // a few different values for time advancements. + // to keep the number of possible steps small, we only have a few different values. + // Roughly, 1s for very small advances (like between blocks), + // and then longer values for increasingly severe downtime scenarios. + // Note that these can still be combined, so in effect we can get all time advancements by any amount of seconds. + pure val timeAdvancements = Set(1 * Second, 1 * Day, 1 * Week, 4 * Week) + + pure def emptyAction = + { + kind: "", + consumerChain: "", + timeAdvancement: 0 * Second, + consumersToStart: Set(), + consumersToStop: Set(), + validator: "", + newVotingPower: 0, + } + + // step allows the most generic nondeterminism, in particular it becomes relatively likely + // that over a long enough runtime, all consumers would time out by mismatching their time advancements, + // and each endblock has a good chance to stop consumers, ... + // step is thus suited to test also unhappy paths. + action step = any { + all { + runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense + nondet chain = oneOf(runningConsumers) + nondet timeAdvancement = oneOf(timeAdvancements) + EndAndBeginBlockForConsumer(chain, timeAdvancement), + }, + + val consumerStatus = currentState.providerState.consumerStatus + nondet consumersToStart = oneOf(nonConsumers.powerset()) + nondet consumersToStop = oneOf(runningConsumers.powerset()) + nondet timeAdvancement = oneOf(timeAdvancements) + EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), + + nondet node = oneOf(nodes) + // very restricted set of voting powers. exact values are not important, + // and this keeps the state space smaller. + // 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), + + // try to send a packet. we could filter by chains that can actually send, + // but it's probably not much faster than just trying and failing. + all { + runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense + nondet sender = oneOf(runningConsumers) + DeliverVscMaturedPacket(sender), + }, + + // again, we could filter by chains that can actually receive, + // but it's probably not much faster than just trying and failing. + all { + runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense + nondet recciver = oneOf(runningConsumers) + DeliverVscPacket(recciver), + }, + } // some utility stateful vals to make invariants easier to define val providerValidatorHistory = currentState.providerState.chainState.votingPowerHistory @@ -50,7 +135,7 @@ module CCVDefaultStateMachine { providerState: providerStateWithConsumers, consumerStates: consumerStates }, - trace' = List("init") + trace' = List(emptyAction.with("kind", "init")), } action VotingPowerChange(validator: Node, newVotingPower: int): bool = @@ -58,7 +143,7 @@ module CCVDefaultStateMachine { all { result.hasError == false, currentState' = result.newState, - trace' = trace.append("VotingPowerChange") + trace' = trace.append(emptyAction.with("kind", "VotingPowerChange").with("validator", validator).with("newVotingPower", newVotingPower)) } // The receiver receives the next outstanding VscPacket from the provider. @@ -69,7 +154,7 @@ module CCVDefaultStateMachine { all { result.hasError == false, currentState' = result.newState, - trace' = trace.append("DeliverVscPacket") + trace' = trace.append(emptyAction.with("kind", "DeliverVscPacket").with("consumerChain", receiver)) } // The provider receives the next outstanding VscMaturedPacket from the sender. @@ -80,7 +165,7 @@ module CCVDefaultStateMachine { all { result.hasError == false, currentState' = result.newState, - trace' = trace.append("DeliverVscMaturedPacket") + trace' = trace.append(emptyAction.with("kind", "DeliverVscMaturedPacket").with("consumerChain", sender)) } action EndAndBeginBlockForProvider( @@ -91,7 +176,7 @@ module CCVDefaultStateMachine { all { result.hasError == false, currentState' = result.newState, - trace' = trace.append("EndAndBeginBlockForProvider") + trace' = trace.append(emptyAction.with("kind", "EndAndBeginBlockForProvider").with("timeAdvancement", timeAdvancement).with("consumersToStart", consumersToStart).with("consumersToStop", consumersToStop)) } action EndAndBeginBlockForConsumer( @@ -101,58 +186,9 @@ module CCVDefaultStateMachine { all { result.hasError == false, currentState' = result.newState, - trace' = trace.append("EndAndBeginBlockForConsumer") + trace' = trace.append(emptyAction.with("kind", "EndAndBeginBlockForConsumer").with("consumerChain", chain).with("timeAdvancement", timeAdvancement)) } - // 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) - - // step allows the most generic nondeterminism, in particular it becomes relatively likely - // that over a long enough runtime, all consumers would time out by mismatching their time advancements, - // and each endblock has a good chance to stop consumers, ... - // step is thus suited to test also unhappy paths. - action step = any { - all { - runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense - nondet chain = oneOf(runningConsumers) - nondet timeAdvancement = oneOf(timeAdvancements) - EndAndBeginBlockForConsumer(chain, timeAdvancement), - }, - - val consumerStatus = currentState.providerState.consumerStatus - nondet consumersToStart = oneOf(nonConsumers.powerset()) - nondet consumersToStop = oneOf(runningConsumers.powerset()) - nondet timeAdvancement = oneOf(timeAdvancements) - EndAndBeginBlockForProvider(timeAdvancement, consumersToStart, consumersToStop), - - nondet node = oneOf(nodes) - // very restricted set of voting powers. exact values are not important, - // and this keeps the state space smaller. - // 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), - - // try to send a packet. we could filter by chains that can actually send, - // but it's probably not much faster than just trying and failing. - all { - runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense - nondet sender = oneOf(runningConsumers) - DeliverVscMaturedPacket(sender), - }, - - // again, we could filter by chains that can actually receive, - // but it's probably not much faster than just trying and failing. - all { - runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense - nondet recciver = oneOf(runningConsumers) - DeliverVscPacket(recciver), - }, - } - // ================== // INVARIANT CHECKS // ================== @@ -169,7 +205,7 @@ module CCVDefaultStateMachine { // Any update in the power of a validator on the provider // MUST be present in a ValidatorSetChangePacket that is sent to all registered consumer chains - val ValUpdatePrecondition = trace[trace.length()-1] == "EndAndBeginBlockForProvider" + val ValUpdatePrecondition = trace[trace.length()-1].kind == "EndAndBeginBlockForProvider" val ValidatorUpdatesArePropagatedInv = // when the provider has just entered a validator set into a block... if (ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock) { @@ -389,8 +425,7 @@ module CCVDefaultStateMachine { 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 - trace' = trace.append("HappyPathTest") + VotingPowerChange("node1", 50) // just so this still has an effect } ) } @@ -436,7 +471,7 @@ module CCVDefaultStateMachine { all { assert(SameVscPacketsInv), // action does not matter, but needed to have uniform effect - step + VotingPowerChange("node1", 50) } ) @@ -459,13 +494,13 @@ module CCVDefaultStateMachine { // advance time on provider by VscTimeout + 1 Second EndAndBeginBlockForProvider(VscTimeout + 5 * Second, Set(), Set()) ) - // .then( - // all { - // // the consumer chains should have timed out - // assert(ConsumerChains.forall( - // chain => currentState.providerState.consumerStatus.get(chain) == TIMEDOUT - // )), - // VotingPowerChange("node2", 50)// action needs to be there but does not matter - // } - // ) + .then( + all { + // the consumer chains should have timed out + assert(ConsumerChains.forall( + chain => currentState.providerState.consumerStatus.get(chain) == TIMEDOUT + )), + VotingPowerChange("node1", 50) // action needs to be there but does not matter what it is + } + ) } \ No newline at end of file diff --git a/tests/difference/core/quint_model/ccv_test.qnt b/tests/difference/core/quint_model/ccv_test.qnt index 9493e69d6a..b21653ae6f 100644 --- a/tests/difference/core/quint_model/ccv_test.qnt +++ b/tests/difference/core/quint_model/ccv_test.qnt @@ -1,8 +1,8 @@ // -*- mode: Bluespec; -*- // contains test logic for the stateless functions in the CCV module -module CCVTest { - import CCVTypes.* from "./ccv" +module ccv_test { + import ccv_types.* from "./ccv" import Time.* from "./libraries/Time" import extraSpells.* from "./libraries/extraSpells" @@ -11,7 +11,7 @@ module CCVTest { 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" + import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains).* from "./ccv" // negative voting powers give an error run VotingPowerNegativeTest =