From 333756e10f0d2ede3dacbb53b4785ce70d7d541d Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Tue, 20 Feb 2024 10:58:04 +0100 Subject: [PATCH] Rename DeliverVscMaturedPacket to DeliverPacketToProvider --- tests/mbt/driver/mbt_test.go | 4 +- tests/mbt/model/README.md | 2 +- tests/mbt/model/ccv.qnt | 48 ++++++++++++++++-- tests/mbt/model/ccv_model.qnt | 92 +++++++++++++++++++++++++++-------- tests/mbt/model/ccv_utils.qnt | 24 ++++++++- 5 files changed, 143 insertions(+), 27 deletions(-) diff --git a/tests/mbt/driver/mbt_test.go b/tests/mbt/driver/mbt_test.go index a55d870dda..336c75b180 100644 --- a/tests/mbt/driver/mbt_test.go +++ b/tests/mbt/driver/mbt_test.go @@ -339,9 +339,9 @@ func RunItfTrace(t *testing.T, path string) { expectError = false driver.DeliverPacketToConsumer(ChainId(consumerChain), expectError) } - case "DeliverVscMaturedPacket": + case "DeliverPacketToProvider": consumerChain := lastAction["consumerChain"].Value.(string) - t.Log("DeliverVscMaturedPacket", consumerChain) + t.Log("DeliverPacketToProvider", consumerChain) var expectError bool if ConsumerStatus(currentModelState, consumerChain) == TIMEDOUT_STATUS { diff --git a/tests/mbt/model/README.md b/tests/mbt/model/README.md index fc864bce35..b8ce579440 100644 --- a/tests/mbt/model/README.md +++ b/tests/mbt/model/README.md @@ -30,7 +30,7 @@ The model has these actions: All the logic in EndBlock/BeginBlock happens here, like updating the validator set, sending packets, etc. * `EndAndBeginBlockForConsumer(chain: Chain, timeAdvancement: Time)`: On the consumer `chain`, ends the current block, and begins a new one. Again, all the logic in EndBlock/BeginBlock happens here, like validator set change maturations. * `DeliverVscPacket(receiver: Chain)`: Delivers a pending VSCPacket from the provider to the consumer `receiver`. -* `DeliverVscMaturedPacket(receiver: Chain)`: Delivers a pending VSCMaturedPacket from the consumer `receiver` to the provider. +* `DeliverPacketToProvider(sender: Chain)`: Delivers a pending packet from the consumer `sender` to the provider. * `KeyAssignment(chain: Chain, validator: Node, consumerAddr: ConsumerAddr)` (only when running with `--step stepKeyAssignment`): Assigns the `consumerAddr` to the `validator` on the `chain`. Note that we use "key" and "consumerAddr" pretty much interchangeably, as the model makes no differentiation between private keys, public keys, addresses, etc, as it doesn't model the cryptography. ### State machines diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index d0406695e0..9ac9485042 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -26,7 +26,11 @@ module ccv_types { // the time at which the packet was sent. sendingTime: Time, // the time (on the receiver) at which the packet will time out - timeoutTime: Time + timeoutTime: Time, + // acknowledged downtime slashes, i.e. validators that + // the provider was requested to slash for downtime, and has + // slashed since the last VscPacket. + downtimeSlashAcks: List[ConsumerAddr] } type VscMaturedPacket = @@ -149,6 +153,11 @@ module ccv_types { // For every sent VSCPacket, stores the key assignments that were applied to send it. keyAssignmentsForVSCPackets: VscId -> (Chain -> (Node -> ConsumerAddr)), + + // downtimeSlashRequests[chainId] contains all the validator addresses for which the provider chain + // received slash requests for downtime from the consumer chain with chainId + // in this block. used to acknowledge slash requests upon EndBlock. + downtimeSlashRequests: Chain -> List[ConsumerAddr] } // utility function: returns a provider state that is initialized minimally. @@ -167,6 +176,7 @@ module ccv_types { consumerAddrsToPrune: Map(), keyAssignmentsForVSCPackets: Map(), consumersWithAddrAssignmentChangesInThisBlock: Set(), + downtimeSlashRequests: Map(), } @@ -193,6 +203,12 @@ module ccv_types { // and will thus be considered "sent" when the block ends. // these are moved to the outstandingPackets list when the block ends. packetsToSendOnEndBlock: List[Packet], + + // Stores the validators on the consumer that the consumer has sent a downtime slash request for. + // These are cleared when the provider acknowledges the downtime slashes. + // We keep this set to disallow sending multiple downtime slashes for the same validator + // before the first downtime slash is acknowledged. + outstandingDowntime: Set[ConsumerAddr], } // utility function: returns a consumer state that is initialized minimally. @@ -203,6 +219,7 @@ module ccv_types { outstandingPacketsToProvider: List(), receivedVscPackets: List(), packetsToSendOnEndBlock: List(), + outstandingDowntime: Set(), } // the state of the protocol consists of the composition of the state of one provider chain with potentially many consumer chains. @@ -520,6 +537,8 @@ module ccv { "consumerStatus", newConsumerStatus ).with( "providerValidatorSetChangedInThisBlock", false + ).with( + "downtimeSlashRequests", Map() ) if (err != "") { @@ -609,7 +628,11 @@ module ccv { "outstandingPacketsToProvider", newOutstandingPackets.concat(newConsumerState.packetsToSendOnEndBlock) ).with( "packetsToSendOnEndBlock", List() + ).with( + // clear the list of outstanding downtime slashes + "outstandingDowntime", Set() ) + val newConsumerStates = currentState.consumerStates.set(chain, newConsumerState2) val newState: ProtocolState = currentState.with( "consumerStates", newConsumerStates @@ -713,10 +736,12 @@ module ccv { consumerNode: Node, vscId: VscId, downtime: bool): Result = { + val consumerState = currentState.consumerStates.get(consumer) if (not(isRunningConsumer(consumer, currentState.providerState))) { Err("Consumer is not currently a consumer - must have 'running' status!") + } else if (downtime and consumerState.outstandingDowntime.contains(consumerNode)) { + Err("Consumer already has outstanding downtime for validator!") } else { - val consumerState = currentState.consumerStates.get(consumer) val vscPacket = consumerState.receivedVscPackets.select(packet => packet.id == vscId)[0] val packet = Slash({ validator: consumerNode, @@ -727,7 +752,10 @@ module ccv { valPower: vscPacket.validatorSet.get(consumerNode) }) - val newConsumerState = commitPacketOnConsumer(consumerState, packet) + val newConsumerState = + commitPacketOnConsumer(consumerState, packet) + // add the consumer address to the list of outstanding slashes + .with("outstandingDowntime", consumerState.outstandingDowntime.union(Set(consumerNode))) Ok(currentState.with("consumerStates", currentState.consumerStates.set(consumer, newConsumerState))) } } @@ -767,7 +795,19 @@ module ccv { .jailUntil(packet.validator, jailEndTime) .slash(packet.validator, packet.valPower, slashFactor) - Ok(currentState.with("providerState", newProviderState)) + if (packet.downtime) { + // if the packet is for downtime, add the consumer address to the list of acknowledged slashes + // for the sender chain of this slash packet + val newDowntimeSlashRequests = newProviderState.downtimeSlashRequests + .getOrElse(sender, List()) + .append(packet.validator) + val newProviderState2 = newProviderState.with( + "downtimeSlashRequests", newProviderState.downtimeSlashRequests.put(sender, newDowntimeSlashRequests) + ) + Ok(currentState.with("providerState", newProviderState2)) + } else { + Ok(currentState.with("providerState", newProviderState)) + } } pure def recvVscMaturedPacketOnProvider(currentState: ProtocolState, sender: Chain, packet: VscMaturedPacket): Result = { diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt index 414f543140..654746bff5 100644 --- a/tests/mbt/model/ccv_model.qnt +++ b/tests/mbt/model/ccv_model.qnt @@ -162,15 +162,15 @@ module ccv_model { params' = params, } - // The provider receives the next outstanding VscMaturedPacket from the sender. + // The provider receives the next outstanding packet from the sender. // This will time out the consumer if the packet timeout has passed on the provider. - action DeliverVscMaturedPacket(sender: Chain): bool = + action DeliverPacketToProvider(sender: Chain): bool = val resultAndTimeout = deliverPacketToProvider(currentState, sender) val result = resultAndTimeout._1 all { result.hasError() == false, currentState' = result.newState, - trace' = trace.append(emptyAction.with("kind", "DeliverVscMaturedPacket").with("consumerChain", sender)), + trace' = trace.append(emptyAction.with("kind", "DeliverPacketToProvider").with("consumerChain", sender)), params' = params, } @@ -211,7 +211,7 @@ module ccv_model { all { runningConsumers.size() > 0, // ensure there is a running consumer, otherwise this action does not make sense nondet sender = oneOf(runningConsumers) - DeliverVscMaturedPacket(sender), + DeliverPacketToProvider(sender), }, // again, we could filter by chains that can actually receive, @@ -221,6 +221,8 @@ module ccv_model { nondet receiver = oneOf(runningConsumers) DeliverVscPacket(receiver), }, + + ConsumerInitiatedSlash } // step allows the most generic nondeterminism, in particular it becomes relatively likely @@ -265,6 +267,7 @@ module ccv_model { validatorSet: Map(), sendingTime: 9999999999999 * Second, timeoutTime: 9999999999999 * Second, + downtimeSlashAcks: List(), } packets.fold( newestPossiblePacket, @@ -277,6 +280,7 @@ module ccv_model { validatorSet: Map(), sendingTime: -9999999999 * Second, timeoutTime: -9999999999 * Second, + downtimeSlashAcks: List(), } packets.fold( oldestPossiblePacket, @@ -289,6 +293,7 @@ module ccv_model { validatorSet: Map(), sendingTime: 1 * Second, timeoutTime: 1 * Second, + downtimeSlashAcks: List(), } val packet2 = { @@ -296,6 +301,7 @@ module ccv_model { validatorSet: Map(), sendingTime: 2 * Second, timeoutTime: 2 * Second, + downtimeSlashAcks: List(), } val packet3 = { @@ -303,6 +309,7 @@ module ccv_model { validatorSet: Map(), sendingTime: 3 * Second, timeoutTime: 3 * Second, + downtimeSlashAcks: List(), } all { assert(oldest(Set(packet1, packet2, packet3)) == packet1), @@ -462,14 +469,23 @@ module ccv_model { val CanSendVscMaturedPackets = not(ConsumerChains.exists( consumer => - currentState.consumerStates.get(consumer).outstandingPacketsToProvider.length() > 0 + currentState.consumerStates.get(consumer) + .outstandingPacketsToProvider + .select(IsVscMaturedPacket).length() > 0 )) - val canSendSlashPacket = + val CanSendSlashPacket = not(ConsumerChains.exists( consumer => - currentState.consumerStates.get(consumer).receivedVscPackets.size() > 0 + currentState.consumerStates.get(consumer) + .outstandingPacketsToProvider + .select(IsSlashPacket).length() > 0 )) + + val CanJail = + not( + currentState.providerState.chainState.jailedUntil.keys().size() > 0 + ) val CanReceiveMaturations = not(ConsumerChains.exists( @@ -579,7 +595,7 @@ module ccv_model { // it was removed from the maturationTimes assert(currentState.consumerStates.get("consumer1").maturationTimes.length() == 0), // receive the packet on the provider - DeliverVscMaturedPacket("consumer1") + DeliverPacketToProvider("consumer1") } ) .then( @@ -748,16 +764,19 @@ module ccv_model { val consumerState = currentState.consumerStates.get(consumer) // ...by getting all received vsc packets... val rcvdVscPackets = consumerState.receivedVscPackets - // ...picking one of the packets... - nondet packet = oneOf(rcvdVscPackets.toSet()) - val vscId = packet.id - val valSet = packet.validatorSet.keys() - // ...and picking one of the validators in the packet - nondet validator = oneOf(valSet) - // finally, choose whether to slash for downtime or double-signing - nondet isDowntime = oneOf(Set(true, false)) - // then we can invoke the deterministic slash - ConsumerInitiatedSlashDet(consumer, validator, vscId, isDowntime) + all { + rcvdVscPackets.length() > 0, + // ...picking one of the packets... + nondet packet = oneOf(rcvdVscPackets.toSet()) + val vscId = packet.id + val valSet = packet.validatorSet.keys() + // ...and picking one of the validators in the packet + nondet validator = oneOf(valSet) + // finally, choose whether to slash for downtime or double-signing + nondet isDowntime = oneOf(Set(true, false)) + // then we can invoke the deterministic slash + ConsumerInitiatedSlashDet(consumer, validator, vscId, isDowntime) + } } } @@ -961,7 +980,7 @@ module ccv_model { ) .then( // deliver the vsc matured packet to the provider - DeliverVscMaturedPacket("consumer1") + DeliverPacketToProvider("consumer1") ) .then( // the old key should have been pruned @@ -989,4 +1008,39 @@ module ccv_model { VotingPowerChange("node1", 50) } ) + + run DoubleDowntimeSlashTest = + init.then( + // start all consumer chains + EndAndBeginBlockForProvider(1 * Second, consumerChains, Set()) + ).then( + // change voting power + VotingPowerChange("node1", 50) + ).then( + // end a block on the provider + EndAndBeginBlockForProvider(1 * Second, Set(), Set()) + ).then( + val vscId = currentState.providerState.sentVscPacketsToConsumer.get("consumer1").head().id + // deliver the vsc packet to consumer1 + DeliverVscPacket("consumer1").then( + // end a block on consumer 1 + EndAndBeginBlockForConsumer("consumer1", 1 * Second) + ).then( + // slash for downtime on consumer1 + ConsumerInitiatedSlashDet("consumer1", "node1", vscId, true) + ).then( + // node1 has outstanding downtime already + ConsumerInitiatedSlashDet("consumer1", "node1", vscId, true).fail() + ).then( + // deliver the slash request to the provider + DeliverPacketToProvider("consumer1") + ).then( + // the provider should have jailed node1 + all { + assert(currentState.providerState.chainState.jailedUntil.keys().contains("node1")), + // action does not matter + VotingPowerChange("node1", 50) + } + ) + ) } \ No newline at end of file diff --git a/tests/mbt/model/ccv_utils.qnt b/tests/mbt/model/ccv_utils.qnt index ca3aaf37ec..412366db88 100644 --- a/tests/mbt/model/ccv_utils.qnt +++ b/tests/mbt/model/ccv_utils.qnt @@ -225,7 +225,8 @@ module ccv_utils { providerState.chainState.currentValidatorPowers ), sendingTime: sendingTimestamp, - timeoutTime: sendingTimestamp + ccvTimeout + timeoutTime: sendingTimestamp + ccvTimeout, + downtimeSlashAcks: providerState.downtimeSlashRequests.getOrElse(consumer, []) }) } else { // no packet to be sent, so empty list @@ -435,6 +436,27 @@ module ccv_utils { } } + pure def IsVscPacket(packet: Packet): bool = { + match packet { + | Vsc(_) => true + | _ => false + } + } + + pure def IsSlashPacket(packet: Packet): bool = { + match packet { + | Slash(_) => true + | _ => false + } + } + + pure def IsVscMaturedPacket(packet: Packet): bool = { + match packet { + | VscMatured(_) => true + | _ => false + } + } + // Commits a packet on the consumer, which will then be sent when a block is ended. // Internally, prepends the packet to the senders packetsToSendOnEndBlock list. pure def commitPacketOnConsumer(senderState: ConsumerState, packet: Packet): ConsumerState = {