From ad2502965586eced274cdcf96248be58550fe094 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Thu, 16 Nov 2023 13:09:13 +0100 Subject: [PATCH] Fix model: packets are emitted based on the timestamp of the last block, not the new block --- tests/difference/core/quint_model/ccv.qnt | 17 ++++++-- .../difference/core/quint_model/ccv_model.qnt | 41 ++++++++++++------- 2 files changed, 40 insertions(+), 18 deletions(-) diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt index 6e0275abe7..5087098e3d 100644 --- a/tests/difference/core/quint_model/ccv.qnt +++ b/tests/difference/core/quint_model/ccv.qnt @@ -413,6 +413,7 @@ module ccv { ) // for each consumer we just set to running, set its initial validator set to be the current one on the provider. + val valSet = providerStateAfterConsumerAdvancement.chainState.currentValidatorSet val newConsumerStateMap = tmpState.consumerStates.keys().mapBy( (consumer) => @@ -420,7 +421,10 @@ module ccv { val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer) val newConsumerState: ConsumerState = currentConsumerState.with( "chainState", currentConsumerState.chainState.with( - "currentValidatorSet", providerStateAfterConsumerAdvancement.chainState.currentValidatorSet + "currentValidatorSet", valSet + ).with( + "votingPowerHistory", + List(valSet) ) ) newConsumerState @@ -462,6 +466,7 @@ module ccv { Err("chain is not a consumer") } else { val currentConsumerState: ConsumerState = currentState.consumerStates.get(chain) + val oldChainState: ChainState = currentConsumerState.chainState val newChainState: ChainState = currentConsumerState.chainState.endAndBeginBlockShared(timeAdvancement) val newConsumerState: ConsumerState = currentConsumerState.with( "chainState", newChainState @@ -470,19 +475,23 @@ module ccv { pair => val packet = pair._1 val maturationTime = pair._2 - maturationTime <= newChainState.lastTimestamp + // 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 ).transform(pair => pair._1) val newMaturationTimes = newConsumerState.maturationTimes.select( pair => val packet = pair._1 val maturationTime = pair._2 - maturationTime > newChainState.lastTimestamp + // 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 ) val newOutstandingPackets = newConsumerState.outstandingPacketsToProvider.concat( maturedPackets.transform( packet => { id: packet.id, - sendingTime: newConsumerState.chainState.lastTimestamp + sendingTime: oldChainState.lastTimestamp } ) ) diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt index 80e414e3fa..b580be32a5 100644 --- a/tests/difference/core/quint_model/ccv_model.qnt +++ b/tests/difference/core/quint_model/ccv_model.qnt @@ -338,24 +338,26 @@ module ccv_model { ) // For every ValidatorSetChangePacket received by a consumer chain at - // time t, a MaturedVscPacket is sent back to the provider in the first block + // time t, a MaturedVscPacket is sent back to the provider when we end the first block // with a timestamp >= t + UnbondingPeriod // NOTE: because we remove the maturationTimes entry when we send the packets, - // it suffices to check that there is never an entry in maturationTimes - // that has already matured, i.e. where the maturationTime is smaller-or-equal than the lastTimestamp + // it suffices to check that after we end/begin a block, there is never an entry in maturationTimes + // that has already matured, i.e. where the maturationTime is smaller-or-equal than the + // timestamp of the block we just ended + val MaturationPrecondition = trace[trace.length()-1].kind == "EndAndBeginBlockForConsumer" + val ConsumerWithPotentialMaturations = trace[trace.length()-1].consumerChain + val lastTimeAdvancement = trace[trace.length()-1].timeAdvancement + val lastBlockTime = currentState.consumerStates.get(ConsumerWithPotentialMaturations).chainState.lastTimestamp - lastTimeAdvancement val MatureOnTimeInv = - runningConsumers.forall( - consumer => { - val maturationTimes = currentState.consumerStates.get(consumer).maturationTimes - maturationTimes.listForAll( - // check that the maturation time is in the future - pair => - val maturationTime = pair._2 - maturationTime >= currentState.consumerStates.get(consumer).chainState.lastTimestamp - ) - } + MaturationPrecondition + implies + currentState.consumerStates.get(ConsumerWithPotentialMaturations).maturationTimes.toSet().forall( + pair => + val maturationTime = pair._2 + maturationTime > lastBlockTime ) + // If we send a VscPacket, this is eventually responded to by all consumers // that were running at the time the packet was sent (and are still running). // Since we remove sentVscPacketsToConsumer when we receive responses for them, @@ -500,7 +502,18 @@ module ccv_model { ) .then( all { - // the packet has matured, so it was sent by the consumer + // the packet has not matured yet - the timestamp for the current block is after the naturation time, + // but packets are only sent on EndBlock + assert(currentState.consumerStates.get("consumer1").outstandingPacketsToProvider.length() == 0), + // the packet is still waiting to mature + assert(currentState.consumerStates.get("consumer1").maturationTimes.length() == 1), + // end another block, this time after the time has been reached + EndAndBeginBlockForConsumer("consumer1", 1 * Second) + } + ) + .then( + all { + // the packet now 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.length() == 0),