Continue implementing slashing

tests/mbt/model/ccv.qnt

@@ -308,6 +308,16 @@ module ccv {
     // The jail time for a downtime infraction.
     const DowntimeJailTime: int
 
+    // The *end time* for double sign infractions.
+    // Note this is *not* the jail duration, but the *end time*.
+    // (This is because essentially double signs should jail forever.)
+    const DoubleSignJailEndTime: int
+
+    // The slash factors for downtime and double sign infractions,
+    // given as a percentage value between 0 and 100.
+    const DowntimeSlashPercentage: int
+    const DoubleSignSlashPercentage: int
+
     // ===================
     // PROTOCOL LOGIC contains the meat of the protocol
     // functions here roughly correspond to API calls that can be triggered from external sources
@@ -738,17 +748,24 @@ module ccv {
         val jailEndTime = if (packet.downtime) {
             packet.sendingTime + DowntimeJailTime
         } else {
-            packet.sendingTime + CcvTimeout.get(sender)
+            packet.sendingTime + DoubleSignJailEndTime
         }
         // map the validator to its address on the provider
         // (in general, the validator is a consumer address and could be an assigned one)
         val providerVal = currentState.providerState.consumerAddrToValidator
             .get(sender)
             // if there is no entry for that validator, there is no key assignment
             .getOrElse(packet.validator, packet.validator)
+
+        val slashFactor = if (packet.downtime) {
+            DowntimeSlashPercentage
+        } else {
+            DoubleSignSlashPercentage
+        }
 
-        val newProviderState = currentState.providerState.jailUntil(packet.validator, jailEndTime)
-        //  .slash(currentState.providerState, packet.validator, packet.valPower, slashFactorToBeDetermined)
+        val newProviderState = currentState.providerState
+            .jailUntil(packet.validator, jailEndTime)
+            .slash(packet.validator, packet.valPower, slashFactor)
 
         Ok(currentState.with("providerState", newProviderState))
     }

tests/mbt/model/ccv_model.qnt

@@ -14,6 +14,10 @@ module ccv_model {
     pure val trustingPeriods = chains.mapBy(chain => defUnbondingPeriod - 1 * Hour)
     pure val ccvTimeouts = chains.mapBy(chain => 3 * Week)
     pure val downtimeJailTime = 5 * Day
+
+    // taken from the sdk, jail time ends at maximum of a certain datatype
+    // see https://github.com/cosmos/cosmos-sdk/blob/03d578b9de5136ffc658f2b0c07434373b07b7da/x/evidence/types/params.go#L11 
+    pure val doubleSignJailEndTime = 253402300799
 
     pure val nodes = Set("node1", "node2", "node3", "node4", "node5", "node6", "node7", "node8", "node9", "node10")
     // possible consumer addresses that nodes can assign their key to
@@ -26,7 +30,10 @@ module ccv_model {
         UnbondingPeriodPerChain = unbondingPeriods,
         ConsumerChains = consumerChains,
         TrustingPeriodPerChain = trustingPeriods,
-        DowntimeJailTime = downtimeJailTime
+        DowntimeJailTime = downtimeJailTime,
+        DoubleSignJailEndTime = doubleSignJailEndTime,
+        DowntimeSlashPercentage = 5,
+        DoubleSignSlashPercentage = 10
     ).* from "./ccv"
 
     type Parameters = {
@@ -457,6 +464,12 @@ module ccv_model {
             consumer => 
                 currentState.consumerStates.get(consumer).outstandingPacketsToProvider.length() > 0
         ))
+
+    val canSendSlashPacket = 
+        not(ConsumerChains.exists(
+            consumer => 
+                currentState.consumerStates.get(consumer).receivedVscPackets.size() > 0
+        ))
 
     val CanReceiveMaturations =
         not(ConsumerChains.exists(

tests/mbt/model/ccv_test.qnt

@@ -13,7 +13,17 @@ module ccv_test {
     pure val ccvTimeouts = chains.mapBy(chain => 3 * Week)
     pure val trustingPeriods = chains.mapBy(chain => 2 * Week - 1 * Hour)
 
-    import ccv(VscTimeout = 5 * Week, CcvTimeout = ccvTimeouts, UnbondingPeriodPerChain = unbondingPeriods, ConsumerChains = consumerChains, TrustingPeriodPerChain=trustingPeriods).* from "./ccv"
+    import ccv(
+        VscTimeout = 5 * Week,
+        CcvTimeout = ccvTimeouts,
+        UnbondingPeriodPerChain = unbondingPeriods,
+        ConsumerChains = consumerChains,
+        TrustingPeriodPerChain=trustingPeriods,
+        DowntimeJailTime=4*Day,
+        DoubleSignJailEndTime=9999 * 50 * Week,
+        DowntimeSlashPercentage = 5,
+        DoubleSignSlashPercentage = 10    
+    ).* from "./ccv"
 
     val votingPowerTestInitState = 
             GetEmptyProtocolState.with(