Skip to content

Commit

Permalink
Add test case for expired clients
Browse files Browse the repository at this point in the history
  • Loading branch information
@p-offtermatt
p-offtermatt committed Nov 27, 2023
1 parent 2d130df commit 8f31705
Show file tree
Hide file tree
Showing 3 changed files with 58 additions and 24 deletions.
46 changes: 25 additions & 21 deletions tests/difference/core/quint_model/ccv.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,10 +43,11 @@ module ccv_types {
currentValidatorSet: ValidatorSet,


// TODO: split into lastTimestamp and runningTimestamp
// TODO: check how expiry needs to work (checks own chains runningTimestamp, but for foreign chain it's tracking the last comitted timestamp)
// the latest timestamp that was comitted on chain
lastTimestamp: Time,

// the running timestamp of the current block (that will be put on chain when the block is ended)
runningTimestamp: Time,
}

// utility function: returns a chain state that is initialized minimally.
Expand All @@ -55,6 +56,7 @@ module ccv_types {
votingPowerHistory: List(),
currentValidatorSet: Map(),
lastTimestamp: 0,
runningTimestamp: 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).
Expand Down Expand Up @@ -277,7 +279,7 @@ module ccv {
(Err("No outstanding packets to deliver"), false)
} else {
val packet = currentState.consumerStates.get(sender).outstandingPacketsToProvider.head()
if(packet.sendingTime + CcvTimeout.get(sender) < currentState.providerState.chainState.lastTimestamp) {
if(packet.sendingTime + CcvTimeout.get(sender) < currentState.providerState.chainState.runningTimestamp) {
// drop consumer
val result = stopConsumers(
currentState.providerState.consumerStatus,
Expand Down Expand Up @@ -327,7 +329,7 @@ module ccv {
} 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) {
if (packet.sendingTime + CcvTimeout.get(PROVIDER_CHAIN) < currentState.consumerStates.get(receiver).chainState.runningTimestamp) {
// drop consumer
val result = stopConsumers(
currentState.providerState.consumerStatus,
Expand Down Expand Up @@ -399,8 +401,7 @@ module ccv {

val expiredConsumers = getRunningConsumers(providerStateAfterTimeAdvancement).filter(
consumer =>
val res = TimeoutDueToVscTimeout(tmpState, consumer)
res._1
providerStateAfterTimeAdvancement.chainState.runningTimestamp > tmpState.consumerStates.get(consumer).chainState.lastTimestamp + TrustingPeriodPerChain.get("provider")
).exclude(timedOutConsumers)

// send vsc packets
Expand Down Expand Up @@ -448,6 +449,9 @@ module ccv {
).with(
"lastTimestamp",
providerStateAfterConsumerAdvancement.chainState.lastTimestamp
).with(
"runningTimestamp",
providerStateAfterConsumerAdvancement.chainState.runningTimestamp
)
)
newConsumerState
Expand Down Expand Up @@ -484,29 +488,28 @@ module ccv {
pair =>
val packet = pair._1
val maturationTime: Time = pair._2
// important that the old chain state is used here, because sending packets happens on EndBlock,
// but the new timestamp only appears after BeginBlock
maturationTime <= oldChainState.lastTimestamp
// important: this uses the last comitted timestamp, not the running timestamp!
maturationTime <= newChainState.lastTimestamp
).transform(pair => pair._1)
val newMaturationTimes = newConsumerState.maturationTimes.select(
pair =>
val packet = pair._1
val maturationTime: Time = pair._2
// important that the old chain state is used here, because sending packets happens on EndBlock,
// but the new timestamp only appears after BeginBlock
maturationTime > oldChainState.lastTimestamp
// important: this uses the last comitted timestamp, not the running timestamp!

maturationTime > newChainState.lastTimestamp
)
val newOutstandingPackets = newConsumerState.outstandingPacketsToProvider.concat(
maturedPackets.transform(
packet => {
id: packet.id,
sendingTime: oldChainState.lastTimestamp
sendingTime: newChainState.runningTimestamp
}
)
)
// checks whether the local client for the provider chain has expired on the consumer
val clientExpired =
if (newChainState.lastTimestamp > currentState.providerState.chainState.lastTimestamp + TrustingPeriodPerChain.get(chain)) {
if (newChainState.runningTimestamp > currentState.providerState.chainState.lastTimestamp + TrustingPeriodPerChain.get(chain)) {
true
} else {
false
Expand Down Expand Up @@ -626,10 +629,11 @@ module ccv {
}

// Advances the timestamp in the chainState by timeAdvancement
pure def advanceTime(chainState: ChainState, timeAdvancement: Time): ChainState = {
chainState.with(
"lastTimestamp", chainState.lastTimestamp + timeAdvancement
)
pure def advanceTime(chainState: ChainState, timeAdvancement: Time): ChainState =
{
lastTimestamp: chainState.runningTimestamp,
runningTimestamp: chainState.runningTimestamp + timeAdvancement,
...chainState
}

// common logic to update the chain state, used by both provider and consumers.
Expand All @@ -652,7 +656,7 @@ module ccv {
List({
id: providerState.runningVscId,
validatorSet: providerState.chainState.currentValidatorSet,
sendingTime: providerState.chainState.lastTimestamp
sendingTime: providerState.chainState.runningTimestamp
})
} else {
List()
Expand Down Expand Up @@ -699,7 +703,7 @@ module ccv {
maturationTimes: currentConsumerState.maturationTimes.append(
(
packet,
currentConsumerState.chainState.lastTimestamp + UnbondingPeriodPerChain.get(receiver)
currentConsumerState.chainState.runningTimestamp + UnbondingPeriodPerChain.get(receiver)
)
),
receivedVscPackets: currentConsumerState.receivedVscPackets.prepend(packet)
Expand Down Expand Up @@ -816,7 +820,7 @@ module ccv {
val sentVscPacketsToConsumer = providerState.sentVscPacketsToConsumer.get(consumer)
if(sentVscPacketsToConsumer.length() > 0) {
val oldestSentVscPacket = sentVscPacketsToConsumer.head() // if length is 0, this is undefined, but we check for this before we use it
if(oldestSentVscPacket.sendingTime + VscTimeout < providerState.chainState.lastTimestamp) {
if(oldestSentVscPacket.sendingTime + VscTimeout < providerState.chainState.runningTimestamp) {
(true, "")
} else {
// no timeout yet, it has not been VscTimeout since that packet was sent
Expand Down
31 changes: 28 additions & 3 deletions tests/difference/core/quint_model/ccv_model.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,13 +18,11 @@ module ccv_model {

import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains, TrustingPeriodPerChain = trustingPeriods).* from "./ccv"

// TODO: introduce max clock drift to produce traces with bounded drift

type Parameters = {
VscTimeout: Time,
CcvTimeout: Chain -> Time,
UnbondingPeriodPerChain: Chain -> Time,
TrustingPeriodPerChain: Chain -> Time, // TODO: integrate trusting period in logic
TrustingPeriodPerChain: Chain -> Time,
ConsumerChains: Set[Chain],
Nodes: Set[Node],
InitialValidatorSet: Node -> int,
Expand Down Expand Up @@ -615,4 +613,31 @@ module ccv_model {
VotingPowerChange("node1", 50) // action needs to be there but does not matter what it is
}
)

// check that when the running timestamp of a chain and the last timestamp of a counterparty differ by more than the trusting period,
// the client is expired
run ExpiredClientTest =
init.then(
EndAndBeginBlockForProvider(1 * Second, Set("consumer1"), Set())
).then(
20.reps(
i => all {
{
// if the trusting period has passed
(currentState.consumerStates.get("consumer1").chainState.lastTimestamp + TrustingPeriodPerChain.get("provider") < currentState.providerState.chainState.runningTimestamp or
currentState.providerState.chainState.lastTimestamp + TrustingPeriodPerChain.get("consumer1") < currentState.consumerStates.get("consumer1").chainState.runningTimestamp)
implies
(currentState.consumerStates.get("consumer1").localClientExpired or
currentState.providerState.consumerStatus.get("consumer1") == EXPIRED or
currentState.providerState.consumerStatus.get("consumer1") == TIMEDOUT)
},
any {
// advance time on the provider
EndAndBeginBlockForProvider(1 * Week, Set(), Set()),
// advance time on the consumer
EndAndBeginBlockForConsumer("consumer1", 1 * Week),
}
}
)
)
}
5 changes: 5 additions & 0 deletions tests/difference/core/quint_model/ccv_test.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ module ccv_test {
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 trustingPeriods = chains.mapBy(chain => 2 * Week - 1 * Hour)

import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains).* from "./ccv"

Expand Down Expand Up @@ -195,6 +196,7 @@ module ccv_test {
currentConsumerStatusMap,
Set("chain1"),
Set("chain2"),
Set(),
Set()
)
res._2 == "" and
Expand All @@ -214,6 +216,7 @@ module ccv_test {
currentConsumerStatusMap,
Set("chain2"),
Set("chain3"),
Set(),
Set()
)
res._2 == "cannot start a consumer that is stopped or already a consumer"
Expand All @@ -230,6 +233,7 @@ module ccv_test {
currentConsumerStatusMap,
Set("chain1"),
Set("chain3"),
Set(),
Set()
)
res._2 == "Cannot stop a consumer that is not running"
Expand All @@ -246,6 +250,7 @@ module ccv_test {
currentConsumerStatusMap,
Set("chain1"),
Set("chain1"),
Set(),
Set()
)
res._2 == "Cannot start and stop a consumer at the same time"
Expand Down

0 comments on commit 8f31705

Please sign in to comment.