Rename DeliverVscMaturedPacket to DeliverPacketToProvider

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 {

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

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 = {

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,20 +293,23 @@ module ccv_model {
                 validatorSet: Map(),
                 sendingTime: 1 * Second,
                 timeoutTime: 1 * Second,
+                downtimeSlashAcks: List(),
             }
 
         val packet2 = {
             id: 2,
             validatorSet: Map(),
             sendingTime: 2 * Second,
             timeoutTime: 2 * Second,
+            downtimeSlashAcks: List(),
         }
 
         val packet3 = {
             id: 3,
             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)
+                }
+            )
+        )
 }

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 = {