Skip to content

Commit

Permalink
Rename modules to have same name as files
Browse files Browse the repository at this point in the history
  • Loading branch information
@p-offtermatt
p-offtermatt committed Oct 11, 2023
1 parent 90f6652 commit 13a32fc
Show file tree
Hide file tree
Showing 3 changed files with 114 additions and 79 deletions.
6 changes: 3 additions & 3 deletions tests/difference/core/quint_model/ccv.qnt
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// -*- mode: Bluespec; -*-
module CCVTypes {
module ccv_types {
import Time.* from "./libraries/Time"

type Node = str
Expand Down Expand Up @@ -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:
Expand All @@ -222,7 +222,7 @@ module CCV {

import Time.* from "./libraries/Time"
import extraSpells.* from "./libraries/extraSpells"
import CCVTypes.*
import ccv_types.*


// ===================
Expand Down
181 changes: 108 additions & 73 deletions tests/difference/core/quint_model/ccv_statemachine.qnt
View file
Original file line number Diff line number Diff line change
@@ -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"

Expand All @@ -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
Expand Down Expand Up @@ -50,15 +135,15 @@ module CCVDefaultStateMachine {
providerState: providerStateWithConsumers,
consumerStates: consumerStates
},
trace' = List("init")
trace' = List(emptyAction.with("kind", "init")),
}

action VotingPowerChange(validator: Node, newVotingPower: int): bool =
val result = votingPowerChange(currentState, validator, newVotingPower)
all {
result.hasError == false,
currentState' = result.newState,
trace' = trace.append("VotingPowerChange")
trace' = trace.append(emptyAction.with("kind", "VotingPowerChange").with("validator", validator).with("newVotingPower", newVotingPower))
}

// The receiver receives the next outstanding VscPacket from the provider.
Expand All @@ -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.
Expand All @@ -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(
Expand All @@ -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(
Expand All @@ -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
// ==================
Expand All @@ -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) {
Expand Down Expand Up @@ -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
}
)
}
Expand Down Expand Up @@ -436,7 +471,7 @@ module CCVDefaultStateMachine {
all {
assert(SameVscPacketsInv),
// action does not matter, but needed to have uniform effect
step
VotingPowerChange("node1", 50)
}
)

Expand All @@ -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
}
)
}
6 changes: 3 additions & 3 deletions tests/difference/core/quint_model/ccv_test.qnt
View file
Original file line number Diff line number Diff line change
@@ -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"

Expand All @@ -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 =
Expand Down

0 comments on commit 13a32fc

Please sign in to comment.