Start implementing endBlock functionality

tests/difference/core/quint_model/extraSpells.qnt

@@ -16,4 +16,43 @@ module extraSpells {
             assert(m.mapRemoveAll(Set(5, 7)) == Map(3 -> 4)),
             assert(m.mapRemoveAll(Set(5, 99999)) == Map(3 -> 4, 7 -> 8)),
         }
+
+    pure def listSorted(__list: List[a], __lt: (a, a) => bool): List[a] = {
+    pure def __countSmaller(__j: int): int = {
+      pure val __jth = __list[__j]
+      __list.indices().filter(__i =>
+        __lt(__list[__i], __jth) or (__list[__i] == __jth and __i < __j)
+      )
+      .size()
+    }
+
+    pure val __permutation = __list.indices().mapBy(__i => __countSmaller(__i))
+        __list.foldl([], (__l, __i) => __l.append(__list[__permutation.get(__i)]))
+    }
+
+    //// Returns a list of all elements of a set.
+    ////
+    //// - @param __set a set
+    //// - @returns a list of all elements of __set
+    pure def toList(__set: Set[a]): List[a] = {
+        __set.fold(List(), (__l, __e) => __l.append(__e))
+    }
+
+    //// Returns a set of the elements in the list.
+    ////
+    //// - @param __list a list
+    //// - @returns a set of the elements in __list
+    pure def toSet(__list: List[a]): Set[a] = {
+        __list.foldl(Set(), (__s, __e) => __s.union(Set(__e)))
+    }
+
+    run toListAndSetTest =
+    all {
+        assert(Set(3, 2, 1).toList().toSet() == Set(1, 2, 3)),
+        assert(List(2,3,1).toSet() == Set(1, 2, 3)),
+        assert(List(2,3,1).toSet() == List(3,2,1).toSet()),
+        assert(toList(Set()) == List()),
+        assert(toSet(List()) == Set())
+    }
+
 }

tests/difference/core/quint_model/model.qnt

@@ -1,4 +1,10 @@
 // -*- mode: Bluespec; -*-
+
+// Design notes:
+// The spec is modular.
+// The various modules generally have actions and variables.
+// The internal state may be read, but not modified, by other modules.
+// In turn, *all* public actions of modules should specify behavior for /all/ variables of the module.
 module common {
     type Validator = str
     type Chain = str
@@ -75,7 +81,7 @@ module ibc {
     // 1) Exactly 1 of the "is[X]Packet" fields will be true.
     // 2) If the is[X]Packet field is false, the [x]Data field is an empty set.
     // 3) If the is[X]Packet field is true, the [x]Data field is a singleton set.
-    type Packet = 
+    type Packet =
     {isVscPacket: bool, vscPacketData: Set[VSCPacketData],
     isSlashPacket: bool, slashPacketData: Set[SlashPacketData],
     isVSCMaturedPacket: bool, vscMaturedPacketData: Set[VSCMaturedPacketData]
@@ -96,11 +102,36 @@ module ibc {
         isSlashPacket: false, slashPacketData: Set(),
         isVSCMaturedPacket: true, vscMaturedPacketData: Set({id: id})}
 
+    // Returns the VSCPacketData of a packet.
+    // If the packet is not a VSC packet, this function will give undefined output.
+    pure def GetVSCData(packet: Packet): VSCPacketData =
+        packet.vscPacketData.chooseSome()
+
+    // Returns the SlashPacketData of a packet.
+    // If the packet is not a Slash packet, this function will give undefined output.
+    pure def GetSlashData(packet: Packet): SlashPacketData =
+        packet.slashPacketData.chooseSome()
+
+    // Returns the VSCMaturedPacketData of a packet.
+    // If the packet is not a VSCMatured packet, this function will give undefined output.
+    pure def GetVSCMaturedData(packet: Packet): VSCMaturedPacketData =
+        packet.vscMaturedPacketData.chooseSome()
+
     // Queue of outstanding packets from the consumer to the provider.
     var ConsumerToProviderChannel: List[Packet]
+
+    // Queue of uncommitted packets from the consumer to the provider.
+    // These packets will be put in the ConsumerToProviderChannel when
+    // the consumer ends a block.
+    var UncommitedConsumerToProviderChannel: List[Packet]
+
     // Queue of outstanding packets from the provider to the consumer.
     var ProviderToConsumerChannel: List[Packet]
 
+    // These packets will be put in the ConsumerToProviderChannel when
+    // the provider ends a block.
+    var UncommitedProviderToConsumerChannel: List[Packet]
+
     // description taken from the old difftest model:
     // noop. We do not explicitly model the client update process
     // but we must call this function at appropriate times in order
@@ -109,11 +140,40 @@ module ibc {
     // clients in the SUT will expire, and the test will fail.
     action UpdateClient(chain: Chain): bool = true
 
-
+    action QueuePacket(packet: Packet, receiver: Chain): bool =
+        any {
+            all {
+            receiver == Provider,
+            UncommitedConsumerToProviderChannel' = UncommitedConsumerToProviderChannel.append(packet),
+            UncommitedProviderToConsumerChannel' = UncommitedProviderToConsumerChannel
+        },
+        all {
+            receiver == Consumer,
+            UncommitedProviderToConsumerChannel' = UncommitedProviderToConsumerChannel.append(packet),
+            UncommitedConsumerToProviderChannel' = UncommitedConsumerToProviderChannel
+        }
+    }
+
+    // Puts uncomitted packets into their respective
+    // channels and clears the uncommitted channels.
+    action IBC_EndBlock(chain: Chain): bool = all {
+        UncommitedConsumerToProviderChannel' = List(),
+        UncommitedProviderToConsumerChannel' = List(),
+        ConsumerToProviderChannel' = ConsumerToProviderChannel.concat(UncommitedConsumerToProviderChannel),
+        ProviderToConsumerChannel' = ProviderToConsumerChannel.concat(UncommitedProviderToConsumerChannel)
+    }
 }
 
-// Staking models the staking module with a single delegator, but multiple validators.
-module staking {
+module slashing_state {
+    import common.*
+    // Stores, for each validator, until when it is jailed.
+    // If this is less than the current time, the validator is not jailed.
+    var jailed: Validator -> int
+
+    val jailTime: int = 50
+}
+
+module staking_state {
     import common.*
 
     type Undelegation = {validator: Validator, amount: int, startTime: Timestamp}
@@ -124,25 +184,67 @@ module staking {
 
     // The amount of unbonded tokens of the single delegator.
     var delegatorTokens: int
-    // The total stake of the validator. Includes, but may exceed, the delegationAmount (e.g. validators can have self-delegations).
+    // The amount delegated to each validator by the single delegator.
     var delegationAmounts: Validator -> int
     // The total stake of the validator. Includes, but may exceed, the delegationAmount (e.g. validators can have self-delegations).
     var validatorPower: Validator -> int
      // A queue of pending undelegations (i.e. unbondings).
     var undelegationsQueue: List[Undelegation]
-
+    // The status of the validators, either Bonded, Unbonded, or Unbonding.
     var validatorStatus: Validator -> string
 
+    val MaxValidators: int = 100
+
+    var currentValidatorSet: Set[Validator]
+}
+
+module slashing {
+    import common.*
+    import ccv_packets.*
+    import slashing_state.*
+    import staking_state.*
+
+    // For now, just jails the validator.
+    action SlashValidator(validator: Validator): bool = all {
+        JailUntil(validator, providerState.time + jailTime)
+    }
+
+    action JailUntil(validator: Validator, time: Timestamp): bool = 
+        jailed' = jailed.set(validator, time)
+
+    action SlashingNoop(): bool = 
+        jailed' = jailed
+
+    action OnRecvSlash(data: SlashPacketData): bool = all {
+        // TODO: soft opt out https://github.com/cosmos/interchain-security/blob/main/docs/docs/adrs/adr-009-soft-opt-out.md
+        if(validatorStatus.get(data.validator) == Unbonded) {
+            // noop, the validator is unbonded so cannot be slashed anymore
+            SlashingNoop
+        } else {
+            // tell the slashing module to slash the validator
+            SlashValidator(data.validator)
+        }
+    }
+}
+
+// Staking models the staking module with a single delegator, but multiple validators.
+module staking {
+    import common.*
+    import slashing_state.*
+    import staking_state.*
+    import basicSpells.* from "./basicSpells"
+    import extraSpells.* from "./extraSpells"
 
     // Constructor for undelegations.
     pure def NewUndelegation(validator: Validator, amount: int, startTime: Timestamp): Undelegation =
         {validator: validator, amount: amount, startTime: startTime}
 
     // Delegates an amount of tokens from the single delegator to the validator
     action Delegate(validator: Validator, amount: int): bool = all {
-        delegatorTokens' = delegatorTokens + amount,
+        delegatorTokens' = delegatorTokens - amount, // unbonded tokens are decreased because we bond tokens
         delegationAmounts' = delegationAmounts.setBy(validator, (oldDelegation => oldDelegation + amount)),
-        validatorPower' = validatorPower.setBy(validator, (oldBalance => oldBalance + amount))
+        validatorPower' = validatorPower.setBy(validator, (oldBalance => oldBalance + amount)),
+        currentValidatorSet' = currentValidatorSet
     }
 
     // Undelegates tokens (delegated by the single delegator) from a validator.
@@ -153,6 +255,7 @@ module staking {
             // thus, the undelegation should not proceed.
             delegationAmounts' = delegationAmounts,
             undelegationsQueue' = undelegationsQueue,
+            currentValidatorSet' = currentValidatorSet
         },
         all {
             // happy path: the undelegation amount is at most the delegated amount.
@@ -162,39 +265,42 @@ module staking {
             // keep the undelegation in the queue until unbonding is complete
             undelegationsQueue' = 
                 undelegationsQueue.append(NewUndelegation(validator, undelegationAmount, providerState.time)),
+            currentValidatorSet' = currentValidatorSet,
             // TODO: call hooks for undelegate
         }
     }
-}
-
-module slashing {
-    import common.*
 
-    // Stores, for each validator, until when it is jailed.
-    // If this is less than the current time, the validator is not jailed.
-    var jailed: Validator -> int
-
-    val jailTime: int = 50
-
-    // For now, just jails the validator.
-    action SlashValidator(validator: Validator): bool = all {
-        JailUntil(validator, providerState.time + jailTime)
+    action Staking_EndBlock(chain: Chain): bool = all {
+        ComputeValUpdates(chain),
+        // ApplyMatureUnbondings(chain),
     }
 
-    action JailUntil(validator: Validator, time: Timestamp): bool = 
-        jailed' = jailed.set(validator, time)
-
-    action __slashing_noop(): bool = 
-        jailed' = jailed
+    action ComputeValUpdates(chain: Chain): bool = 
+        val potentialValidators = 
+            validatorPower.keys().filter(validator => validatorPower.get(validator) > 0 and jailed.getOrElse(validator, 0) <= providerState.time)
+        val potentialValidatorList = potentialValidators.toList()
+        def HasMorePower(this: Validator, other: Validator): bool = validatorPower.get(this) > validatorPower.get(other)
+        val sortedValidatorList = potentialValidatorList.listSorted(HasMorePower)
+        val newValidators = sortedValidatorList.slice(0, MaxValidators)
+        val newValidatorSet = newValidators.toSet()
+        all {
+        currentValidatorSet' = newValidatorSet,
+        // set all new validators to bonded
+        validatorStatus' = validatorStatus.keys().union(newValidatorSet).mapBy(validator => 
+            if(newValidatorSet.contains(validator)) Bonded else validatorStatus.get(validator)),
+    }
 }
 
+
 module ccv_provider {
     import common.*
     import ibc.*
     import ccv_packets.*
     import ccv_common.*
     import basicSpells.* from "./basicSpells"
     import extraSpells.* from "./extraSpells"
+    import slashing.*
+    import staking.*
 
     // Enables accessing, for every unbonding operation,
     // the set of consumer chains that are still unbonding.
@@ -210,13 +316,17 @@ module ccv_provider {
     // Matures all unbondings associated with the vscId of the given VSCMaturedPacketData.
     // Remove the unbonding operations from the unbondingOps map.
     // Add the 
-    action OnRecvVSCMaturedPacket(data: VSCMaturedPacketData): bool = all {
+    action OnRecvVSCMatured(data: VSCMaturedPacketData): bool = all {
         matureUnbondingOps' = matureUnbondingOps.union(vscToUnbondingOps.get(data.id)),
         unbondingOps'  = unbondingOps.mapRemoveAll(vscToUnbondingOps.get(data.id)),
         vscToUnbondingOps' = vscToUnbondingOps.mapRemove(data.id),
     }
-
-
+
+    action CCVProviderNoop: bool = all {
+        unbondingOps' = unbondingOps,
+        vscToUnbondingOps' = vscToUnbondingOps,
+        matureUnbondingOps' = matureUnbondingOps,
+    }
 }
 
 
@@ -226,6 +336,7 @@ module ccv_consumer {
     import ccv_packets.*
     import staking.*
     import slashing.*
+    import staking_state.*
 
     // outstandingDowntime.get(valAddr) = true entails that the consumer chain sent a request to slash for downtime the validator with address valAddr.
     // outstandingDowntime.get(valAddr) is set to false once the consumer chain receives a confirmation that the downtime slash request was received by the provider chain, 
@@ -266,27 +377,23 @@ module ccv_consumer {
     action OnRecvVSC(data: VSCPacketData): bool = all {
         HtoVSC' = HtoVSC.put(consumerState.height + 1, data.id),
         receivedVSCs' = receivedVSCs.append(data),
+        outstandingDowntime' = outstandingDowntime,
     }
 
-    action OnRecvSlash(data: SlashPacketData): bool = all {
-        // TODO: soft opt out https://github.com/cosmos/interchain-security/blob/main/docs/docs/adrs/adr-009-soft-opt-out.md
-        if(validatorStatus.get(data.validator) == Unbonded) {
-            // noop, the validator is unbonded so cannot be slashed anymore
-            __slashing_noop()
-        } else {
-            // tell the slashing module to slash the validator
-            // SlashValidator(data.validator)
-            jailed' = jailed.set(data.validator, 50)
-        }
+    action CCVConsumerNoop(): bool = all {
+        HtoVSC' = HtoVSC,
+        receivedVSCs' = receivedVSCs,
+        outstandingDowntime' = outstandingDowntime,
     }
-
 }
 
+// Actions of the main module always touch all the other modules.
 module main {
     import common.*
     import ibc.*
     import ccv_consumer.*
     import ccv_provider.*
+    import slashing.*
 
      // Delivers the next pending packet to the given chain.
     action DeliverPacket(receiver: Chain): bool = all {
@@ -307,24 +414,30 @@ module main {
     }
 
     // Delivers a specific packet to the given chain.
-    action DeliverPacketToChain(receiver: Chain, packet: Packet): bool = all {
-        if(packet.isVscPacket) {
-            all {
-                receiver == Consumer,
-                OnRecvVSC(packet.vscPacketData)
-            }
-        } else if(packet.isSlashPacket) {
+    action DeliverPacketToChain(receiver: Chain, packet: Packet): bool =
+        any {
             all {
+                packet.isSlashPacket,
                 receiver == Provider,
-                // DeliverSlashPacket(receiver, packet.slashPacketData)
-            }
-        } else { // packet.isVSCMaturedPacket
+                OnRecvSlash(packet.GetSlashData()),
+                CCVProviderNoop,
+                CCVConsumerNoop
+            },
             all {
+                packet.isVscPacket,
+                receiver == Consumer,
+                OnRecvVSC(packet.GetVSCData()),
+                SlashingNoop,
+                CCVProviderNoop
+            },
+            all {
+                packet.isVSCMaturedPacket,
                 receiver == Provider,
-                // DeliverVSCMaturedPacket(receiver, packet.vscMaturedPacketData)
+                OnRecvVSCMatured(packet.GetVSCMaturedData()),
+                CCVConsumerNoop,
+                SlashingNoop
             }
         }
-    }
 
     pure val SlashTypes = Set("downtime", "equivocation")