Continue slashing implementation

tests/mbt/driver/model_viewer.go

@@ -28,7 +28,7 @@ func ChainState(curStateExpr itf.MapExprType, chain string) itf.MapExprType {
 }
 
 func ValidatorSet(curStateExpr itf.MapExprType, chain string) itf.MapExprType {
-	return ChainState(curStateExpr, chain)["currentValidatorSet"].Value.(itf.MapExprType)
+	return ChainState(curStateExpr, chain)["currentValidatorPowerss"].Value.(itf.MapExprType)
 }
 
 func HistoricalValidatorSet(curStateExpr itf.MapExprType, chain string, index int) itf.MapExprType {

tests/mbt/model/ccv.qnt

@@ -68,25 +68,33 @@ module ccv_types {
         // Voting powers should be ordered by recency in descending order.
         votingPowerHistory: VotingPowerHistory,
 
-        // the current validator set on each chain.
-        // this will be included in the next block, but might not be final yet,
-        // e.g. there may be more modifications in the current block.
-        currentValidatorSet: ValidatorSet,
+        // the current validator powers on each chain.
+        // this will typically become the next validator set
+        // that is entered on chain, but some validators
+        // might be excluded, i.e. because they are jailed.
+        currentValidatorPowers: ValidatorSet,
 
         // the latest timestamp that was committed on chain
         lastTimestamp: Time,
 
         // the running timestamp of the current block (that will be put on chain when the block is ended)
         runningTimestamp: Time,
+
+        // Stores the times at which nodes can earliest be unjailed.
+        // If a node has no entry here, it is not jailed.
+        // If a node has a time in the past, it can be unjailed.
+        // If the time is in the future, it cannot be unjailed until that time.
+        jailedUntil: Node -> Time,
     }
 
     // utility function: returns a chain state that is initialized minimally.
     pure def GetEmptyChainState(): ChainState = 
         {
             votingPowerHistory: List(),
-            currentValidatorSet: Map(),
+            currentValidatorPowers: Map(),
             lastTimestamp: -1, // last timestamp -1 means that in the model, there was no block committed on chain yet.
             runningTimestamp: 0,
+            jailedUntil: Map(),
         }
 
     // 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).
@@ -308,15 +316,15 @@ module ccv {
     // the power of a validator on the provider chain is changed by the given amount. We do not care how this happens,
     // e.g. via undelegations, or delegations, ...
     pure def votingPowerChange(currentState: ProtocolState, validator: Node, amount: int): Result = {
-            pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet
-            pure val oldVotingPower = if (currentValidatorSet.keys().contains(validator)) currentValidatorSet.get(validator) else 0
+            pure val currentValidatorPowers = currentState.providerState.chainState.currentValidatorPowers
+            pure val oldVotingPower = if (currentValidatorPowers.keys().contains(validator)) currentValidatorPowers.get(validator) else 0
             if (amount == 0) {
                 Err("Voting power cannot change by zero!")
             } else if (oldVotingPower == 0) {
                 Err("Voting power cannot be changed for a validator that is not in the current validator set!")
             } else {
                 pure val newVotingPower = oldVotingPower + amount
-                pure val newValidatorSet = currentValidatorSet.put(validator, if(newVotingPower >= 0) newVotingPower else 0)
+                pure val newValidatorSet = currentValidatorPowers.put(validator, if(newVotingPower >= 0) newVotingPower else 0)
                 // if the new validator set contains no validators with positive voting power, the validator set is invalid
                 if (newValidatorSet.values().filter(votingPower => votingPower > 0).size() == 0) {
                     Err("Voting power change resulted in empty validator set!")
@@ -462,7 +470,7 @@ module ccv {
             (consumer) => 
             currentProviderState.applyKeyAssignmentToValSet(
                 consumer, 
-                currentProviderState.chainState.currentValidatorSet
+                currentProviderState.chainState.currentValidatorPowers
             )
         )
         // store the current validator set with the key assignments applied in the history
@@ -508,7 +516,7 @@ module ccv {
             Err(err)
         } else {
             // 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 valSet = providerStateAfterConsumerAdvancement.chainState.currentValidatorPowers
             val newConsumerStateMap =
                 tmpState.consumerStates.keys().mapBy(
                     (consumer) => 
@@ -518,7 +526,7 @@ module ccv {
                         val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer)
                         val newConsumerState: ConsumerState = currentConsumerState.with(
                             "chainState", currentConsumerState.chainState.with(
-                                "currentValidatorSet", consValSet
+                                "currentValidatorPowers", consValSet
                             ).with(
                                 "votingPowerHistory",
                                 List(consValSet)
@@ -604,7 +612,7 @@ module ccv {
     pure def assignConsumerKey(currentState: ProtocolState, consumer: Chain, providerNode: Node, consumerAddr: ConsumerAddr): Result = {
         // rule 1: validator A cannot assign consumer key K to consumer chain X
         // if there is already a validator B (B!=A) using K on the provider
-        pure val provCurValSet = currentState.providerState.chainState.currentValidatorSet
+        pure val provCurValSet = currentState.providerState.chainState.currentValidatorPowers
         if (provCurValSet.keys().exists(node => node != providerNode and node == consumerAddr)) {
             Err("validator A cannot assign consumer key K to consumer chain X
             if there is already a validator B (B!=A) using K on the provider")
@@ -638,7 +646,7 @@ module ccv {
                 }
 
                 // check whether the validator has positive power
-                pure val provValSet = currentState.providerState.chainState.currentValidatorSet
+                pure val provValSet = currentState.providerState.chainState.currentValidatorPowers
                 pure val provValPower = if (provValSet.keys().contains(providerNode)) provValSet.get(providerNode) else 0
                 pure val consumersWithAddrAssignmentChangesInThisBlock = 
                     if (provValPower > 0) {
@@ -709,12 +717,8 @@ module ccv {
                 valPower: vscPacket.validatorSet.get(consumerNode)
 
             })
-            if (downtime) {
-                Err("Downtime slashes are not yet implemented")
-            } else {
-                val newConsumerState = commitPacketOnConsumer(consumerState, packet)
-                Ok(currentState.with("consumerStates", currentState.consumerStates.set(consumer, newConsumerState)))
-            }
+            val newConsumerState = commitPacketOnConsumer(consumerState, packet)
+            Ok(currentState.with("consumerStates", currentState.consumerStates.set(consumer, newConsumerState)))
         }
     }
 
@@ -727,10 +731,9 @@ module ccv {
         }
     }
 
-    // TODO: currently this only jails, but it should eventually also slash
     pure def recvSlashPacketOnProvider(currentState: ProtocolState, sender: Chain, packet: SlashPacket): Result = {
         // determine the jail duration for the validator:
-        // if the packet is a downtime slash, the jail duration is DowntimeJailDuration
+        // if the packet is a downtime slash, the jail duration is DowntimeJailTime
         // otherwise, the validator is jailed until the DoubleSignJailTime
         val jailEndTime = if (packet.downtime) {
             packet.sendingTime + DowntimeJailTime
@@ -744,13 +747,10 @@ module ccv {
             // if there is no entry for that validator, there is no key assignment
             .getOrElse(packet.validator, packet.validator)
 
-        // TODO: implement jailing
-        // val newProviderState = currentState.providerState
-        //  .jailUntil(currentState.providerState, packet.validator, jailEndTime)
+        val newProviderState = currentState.providerState.jailUntil(packet.validator, jailEndTime)
         //  .slash(currentState.providerState, packet.validator, packet.valPower, slashFactorToBeDetermined)
 
-        // Ok(currentState.with("providerState", newProviderState))
-        Err("not implemented")
+        Ok(currentState.with("providerState", newProviderState))
     }
 
     pure def recvVscMaturedPacketOnProvider(currentState: ProtocolState, sender: Chain, packet: VscMaturedPacket): Result = {

tests/mbt/model/ccv_model.qnt

@@ -13,6 +13,7 @@ module ccv_model {
     pure val unbondingPeriods = chains.mapBy(chain => defUnbondingPeriod)
     pure val trustingPeriods = chains.mapBy(chain => defUnbondingPeriod - 1 * Hour)
     pure val ccvTimeouts = chains.mapBy(chain => 3 * Week)
+    pure val downtimeJailTime = 5 * Day
 
     pure val nodes = Set("node1", "node2", "node3", "node4", "node5", "node6", "node7", "node8", "node9", "node10")
     // possible consumer addresses that nodes can assign their key to
@@ -24,7 +25,8 @@ module ccv_model {
         CcvTimeout = ccvTimeouts,
         UnbondingPeriodPerChain = unbondingPeriods,
         ConsumerChains = consumerChains,
-        TrustingPeriodPerChain = trustingPeriods
+        TrustingPeriodPerChain = trustingPeriods,
+        DowntimeJailTime = downtimeJailTime
     ).* from "./ccv"
 
     type Parameters = {
@@ -110,7 +112,7 @@ module ccv_model {
             "chainState", providerState.chainState.with(
                 "votingPowerHistory", List(InitialValidatorSet)
             ).with(
-                "currentValidatorSet", InitialValidatorSet
+                "currentValidatorPowers", InitialValidatorSet
             )
         ).with(
             "keyAssignedValSetHistory", ConsumerChains.mapBy(chain => List(InitialValidatorSet))
@@ -495,15 +497,15 @@ module ccv_model {
                 )),
                 assert(currentState.consumerStates.keys() == consumerChains),
                 assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet)),
-                assert(currentState.providerState.chainState.currentValidatorSet == InitialValidatorSet),
+                assert(currentState.providerState.chainState.currentValidatorPowers == InitialValidatorSet),
                 assert(currentState.providerState.chainState.lastTimestamp == -1),
                 assert(currentState.providerState.chainState.runningTimestamp == 0),
                 VotingPowerChange("node1", 50)
             })
             .then(
             all {
                 // the validator set has changed
-                assert(currentState.providerState.chainState.currentValidatorSet == InitialValidatorSet.put("node1", 150)),
+                assert(currentState.providerState.chainState.currentValidatorPowers == InitialValidatorSet.put("node1", 150)),
                 // start consumer1
                 EndAndBeginBlockForProvider(1 * Second, Set("consumer1"), Set())
             })
@@ -532,7 +534,7 @@ module ccv_model {
                     // ensure the maturation time was entered on the consumer
                     assert(currentState.consumerStates.get("consumer1").maturationTimes.length() == 1),
                     // the validator set was put as the current validator set
-                    assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet == InitialValidatorSet.put("node1", 200)),
+                    assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorPowers == InitialValidatorSet.put("node1", 200)),
                     // advance time on provider and consumer until unbonding period is over - ensure that the consumer and provider
                     // stay in sync relative to each other
                     // We want to make sure the steps we make are shorter the trusting period,
@@ -700,10 +702,10 @@ module ccv_model {
     action ConsumerInitiatedSlashDet(
         consumer: Chain,
         consumerNode: Node,
-        vscId: VscId
+        vscId: VscId,
+        isDowntime: bool
     ): bool = {
-        // only support double-sign slashes for now, so supply 'true' for downtime
-        val result = sendSlashRequest(currentState, consumer, consumerNode, vscId, false)
+        val result = sendSlashRequest(currentState, consumer, consumerNode, vscId, isDowntime)
         all {
             hasError(result) == false,
             currentState' = result.newState,
@@ -739,8 +741,10 @@ module ccv_model {
             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)
+            ConsumerInitiatedSlashDet(consumer, validator, vscId, isDowntime)
         }
     }
 
@@ -853,7 +857,7 @@ module ccv_model {
                     // either the key is the nodes key itself (B == A)
                     consAddr == node or
                     // or the consAddr must not be a validator on the provider
-                    not(currentState.providerState.chainState.currentValidatorSet.keys().contains(consAddr))
+                    not(currentState.providerState.chainState.currentValidatorPowers.keys().contains(consAddr))
             )
         )
 
@@ -882,7 +886,7 @@ module ccv_model {
     val CanHaveConsumerAddresses =
         not(consumerChains.exists(
             consumer => 
-                currentState.consumerStates.get(consumer).chainState.currentValidatorSet.keys().exists(
+                currentState.consumerStates.get(consumer).chainState.currentValidatorPowers.keys().exists(
                     addr => addr.in(consumerAddresses)
                 )
         ))
@@ -913,8 +917,8 @@ module ccv_model {
         .then(
             all {
                 // the key should be present in the valset on the consumer, and the node itself should not
-                assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet.getOrElse("node1", 0) == 0),
-                assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet.get("consAddr1") == 100),
+                assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorPowers.getOrElse("node1", 0) == 0),
+                assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorPowers.get("consAddr1") == 100),
                 // try some key assignments that should fail/succeed without committing to state
                 val res = assignConsumerKey(currentState, "consumer1", "node1", "consAddr1")
                 // fail - key already assigned (even if it is the same node)

tests/mbt/model/ccv_test.qnt

@@ -19,7 +19,7 @@ module ccv_test {
             GetEmptyProtocolState.with(
                 "providerState", GetEmptyProtocolState.providerState.with(
                     "chainState", GetEmptyProtocolState.providerState.chainState.with(
-                        "currentValidatorSet", GetEmptyProtocolState.providerState.chainState.currentValidatorSet.put(
+                        "currentValidatorPowers", GetEmptyProtocolState.providerState.chainState.currentValidatorPowers.put(
                             "validator", 5
                         ).put(
                             "validator2", 5
@@ -46,8 +46,8 @@ module ccv_test {
             5
         )
         not(result.hasError()) and
-        result.newState.providerState.chainState.currentValidatorSet.keys().contains("validator") and
-        result.newState.providerState.chainState.currentValidatorSet.get("validator") == 10
+        result.newState.providerState.chainState.currentValidatorPowers.keys().contains("validator") and
+        result.newState.providerState.chainState.currentValidatorPowers.get("validator") == 10
     }
 
     // voting power of 0 is allowed and applied as usual
@@ -59,7 +59,7 @@ module ccv_test {
             -5
         )
         not(finalResult.hasError()) and
-        finalResult.newState.providerState.chainState.currentValidatorSet.get("validator") == 0
+        finalResult.newState.providerState.chainState.currentValidatorPowers.get("validator") == 0
     }
 
     run VotingPowerSetsFlagTest =
@@ -109,7 +109,7 @@ module ccv_test {
             5
         )
         not(result.hasError()) and
-        result.newState.providerState.chainState.currentValidatorSet.get("validator") == 0 and
+        result.newState.providerState.chainState.currentValidatorPowers.get("validator") == 0 and
         result2.hasError()
     }
 
@@ -127,7 +127,7 @@ module ccv_test {
             -5
         )
         not(result.hasError()) and
-        result.newState.providerState.chainState.currentValidatorSet.get("validator") == 0 and
+        result.newState.providerState.chainState.currentValidatorPowers.get("validator") == 0 and
         result2.hasError()
     }
 
@@ -175,7 +175,7 @@ module ccv_test {
             "sentVscPacketsToConsumer", _DeliverPacketToProvider_TestState.providerState.sentVscPacketsToConsumer.put(
                 "sender", List({
                     id: 0,
-                    validatorSet: _DeliverPacketToProvider_TestState.providerState.chainState.currentValidatorSet,
+                    validatorSet: _DeliverPacketToProvider_TestState.providerState.chainState.currentValidatorPowers,
                     sendingTime: 0,
                     timeoutTime: CcvTimeout.get("sender")
                 })