Skip to content

Commit

Permalink
Fix model: packets are emitted based on the timestamp of the last blo…
Browse files Browse the repository at this point in the history 
…ck, not the new block
  • Loading branch information
@p-offtermatt
p-offtermatt committed Nov 16, 2023
1 parent abc12cf commit ad25029
Show file tree
Hide file tree
Showing 2 changed files with 40 additions and 18 deletions.
17 changes: 13 additions & 4 deletions tests/difference/core/quint_model/ccv.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -413,14 +413,18 @@ 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) =>
if (consumersToStart.contains(consumer)) {
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
Expand Down Expand Up @@ -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
Expand All @@ -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
}
)
)
Expand Down
41 changes: 27 additions & 14 deletions tests/difference/core/quint_model/ccv_model.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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),
Expand Down

0 comments on commit ad25029

Please sign in to comment.