From 8f31705f1d9a8fa2a8cf9cc510e0109698c48305 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Mon, 27 Nov 2023 17:35:22 +0100 Subject: [PATCH] Add test case for expired clients --- tests/difference/core/quint_model/ccv.qnt | 46 ++++++++++--------- .../difference/core/quint_model/ccv_model.qnt | 31 +++++++++++-- .../difference/core/quint_model/ccv_test.qnt | 5 ++ 3 files changed, 58 insertions(+), 24 deletions(-) diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt index bc252522a5..c0f7137412 100644 --- a/tests/difference/core/quint_model/ccv.qnt +++ b/tests/difference/core/quint_model/ccv.qnt @@ -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. @@ -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). @@ -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, @@ -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, @@ -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 @@ -448,6 +449,9 @@ module ccv { ).with( "lastTimestamp", providerStateAfterConsumerAdvancement.chainState.lastTimestamp + ).with( + "runningTimestamp", + providerStateAfterConsumerAdvancement.chainState.runningTimestamp ) ) newConsumerState @@ -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 @@ -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. @@ -652,7 +656,7 @@ module ccv { List({ id: providerState.runningVscId, validatorSet: providerState.chainState.currentValidatorSet, - sendingTime: providerState.chainState.lastTimestamp + sendingTime: providerState.chainState.runningTimestamp }) } else { List() @@ -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) @@ -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 diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt index 45035ddfdd..f0f200e7a8 100644 --- a/tests/difference/core/quint_model/ccv_model.qnt +++ b/tests/difference/core/quint_model/ccv_model.qnt @@ -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, @@ -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), + } + } + ) + ) } \ 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 56320b12f0..477d0dc419 100644 --- a/tests/difference/core/quint_model/ccv_test.qnt +++ b/tests/difference/core/quint_model/ccv_test.qnt @@ -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" @@ -195,6 +196,7 @@ module ccv_test { currentConsumerStatusMap, Set("chain1"), Set("chain2"), + Set(), Set() ) res._2 == "" and @@ -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" @@ -230,6 +233,7 @@ module ccv_test { currentConsumerStatusMap, Set("chain1"), Set("chain3"), + Set(), Set() ) res._2 == "Cannot stop a consumer that is not running" @@ -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"