Snapshot error

tests/difference/core/quint_model/README.md

@@ -21,4 +21,5 @@ The parameters of the protocol are defined as consts in ccv.qnt.
 ### Invariants
 
 The invariants I am checking are in ccv_statemachine.qnt, and are as follows:
-- ValidatorUpdatesArePropagated: When a validator power update is comitted on chain, a packet containing that change in voting power is sent to all running consumers. Check via `quint run --invariant ValidatorUpdatesArePropagated ccv_statemachine.qnt --main CCVDefaultStateMachine`
+- ValidatorUpdatesArePropagated: When a validator power update is comitted on chain, a packet containing that change in voting power is sent to all running consumers. Check via `quint run --invariant ValidatorUpdatesArePropagated ccv_statemachine.qnt --main CCVDefaultStateMachine`
+- 

tests/difference/core/quint_model/ccv.qnt

@@ -106,6 +106,10 @@ module CCVTypes {
         // Stores the maturation times for VSCPackets received by this consumer
         maturationTimes: VSCPacket -> Time,
 
+        // stores the received vscpackets in descending order of recency,
+        // i.e. newest first.
+        receivedVSCPackets: List[VSCPacket],
+
         // Stores the list of packets that have been sent to the provider chain by this consumer
         // and have not been received yet.
         // ordered by recency, so the head is the oldest packet.
@@ -119,6 +123,7 @@ module CCVTypes {
             chainState: GetEmptyChainState,
             maturationTimes: Map(),
             outstandingPacketsToProvider: List(),
+            receivedVSCPackets: List(),
         }
 
     // the state of the protocol consists of the composition of the state of one provider chain with potentially many consumer chains.
@@ -681,6 +686,9 @@ module CCV {
                     packet, 
                     currentConsumerState.chainState.lastTimestamp + UnbondingPeriodPerChain.get(receiver)
                 )
+            ).with(
+                "receivedVSCPackets",
+                currentConsumerState.receivedVSCPackets.prepend(packet)
             )
             val newConsumerStates = currentState.consumerStates.set(receiver, newConsumerState)
             val newState = currentState.with(

tests/difference/core/quint_model/ccv_statemachine.qnt

@@ -153,7 +153,7 @@ module CCVDefaultStateMachine {
     // Every validator set on any consumer chain MUST either be or have been 
     // a validator set on the provider chain.
     val ValidatorSetHasExistedInv =
-        ConsumerChains.forall(chain =>
+        runningConsumers.forall(chain =>
             currentState.consumerStates.get(chain).chainState.votingPowerHistory.toSet().forall(
                 validatorSet => providerValidatorHistory.toSet().contains(validatorSet)
             )
@@ -176,24 +176,34 @@ module CCVDefaultStateMachine {
             true
         }
 
+    // Every consumer chain receives the same sequence of 
+    // ValidatorSetChangePackets in the same order.
+    // NOTE: since not all consumer chains are running all the time,
+    // we need a slightly weaker invariant:
+    // For consumer chains c1, c2, if both c1 and c2 received a packet p1 sent at t1 and a packet p2 sent at t2,
+    // then both have received ALL packets that were sent between t1 and t2.
+    val SameVSCPacketsInv =
+        runningConsumers.forall(
+            consumer1 => runningConsumers.forall(
+                consumer2 => {
+                    val packets1 = currentState.consumerStates.get(consumer1).receivedVSCPackets
+                    val packets2 = currentState.consumerStates.get(consumer2).receivedVSCPackets
+                    val commonPackets = packets1.toSet().intersect(packets2.toSet())
+                    if (commonPackets.size() == 0) {
+                        true // they don't share any packets, so nothing to check
+                    } else {
+                        // get oldest common packet
+                        val oldestCommonPacket = commonPackets.MinBy(packet => packet.sendingTime, packets1.head())
+                        false
+                    }
+                }
+            )
+        )
 
-//     \* Invariants from https://github.com/cosmos/interchain-security/blob/main/docs/quality_assurance.md
+        
 
-// (*
-// 6.02 - Any update in the power of a validator val on the provider, as a result of
-// - (increase) Delegate() / Redelegate() to val
-// - (increase) val joining the provider validator set
-// - (decrease) Undelegate() / Redelegate() from val
-// - (decrease) Slash(val)
-// - (decrease) val leaving the provider validator set
-// MUST be present in a ValidatorSetChangePacket that is sent to all registered consumer chains
-// *)
-// Inv602 ==
-//   \A packet \in DOMAIN votingPowerHist:
-//     \A c \in LiveConsumers:
-//       LET packetsToC == PacketOrder(c) IN
-//       \E i \in DOMAIN packetsToC:
-//         packetsToC[i] = packet
+
+//     \* Invariants from https://github.com/cosmos/interchain-security/blob/main/docs/quality_assurance.md
 
 // (*
 // 6.03 - Every consumer chain receives the same sequence of 

tests/difference/core/quint_model/libraries/extraSpells.qnt

@@ -194,4 +194,53 @@ module extraSpells {
         assert(Max(Set(1, 2, 3)) == 3),
         assert(Max(Set()) == 0)
     }
+
+    pure def HasSubsequence(__this: List[a], __other: List[a]): bool = {
+      if(__other.length() > __this.length()) {
+        false
+      } else {
+        0.to(__this.length() - __other.length()) // go through all possible starting points of __other in __this
+        .exists(
+          __start => __this.slice(__start, __start + __other.length()) == __other
+        )
+      }
+    }
+
+    run HasSubsequenceTest =
+    all {
+      assert(List(1, 2, 3, 4).HasSubsequence(List(1, 2))),
+      assert(List(1, 2, 3, 4).HasSubsequence(List(2, 3))),
+      assert(List(1, 2, 3, 4).HasSubsequence(List(3, 4))),
+      assert(List(1, 2, 3, 4).HasSubsequence(List(1, 2, 3))),
+      assert(not(List(1, 2, 3, 4).HasSubsequence(List(1, 3)))),
+      assert(not(List().HasSubsequence(List(1)))),
+      assert(List().HasSubsequence(List())),
+      assert(List(1).HasSubsequence(List())),
+      assert(List(1).HasSubsequence(List(1))),
+    }
+
+    // Returns the maximum element of a set, according to a given function.
+    // __i should be part of the set if it is nonempty. If the set is empty, __i will be returned.
+    // If two elements are equally large, an arbitrary one will be returned.
+    pure def MaxBy(__set: Set[a], __f: a => int, __i: a): a = {
+      __set.fold(
+        __i,
+        (__m, __e) => if(__f(__m) > __f(__e)) {__m } else {__e}
+      )
+    }
+
+    run MaxByTest =
+    all {
+      assert(MaxBy(Set(1, 2, 3), __x => __x, 0) == 3),
+      assert(MaxBy(Set(1, 2, 3), __x => -__x, 0) == 1),
+      assert(MaxBy(Set(), __x => __x, 0) == 0),
+    }
+
+    // Like MaxBy, but returns the minimum element.
+    pure def MinBy(__set: Set[a], __f: a => int, __i: a): a = {
+      __set.fold(
+        __i,
+        (__m, __e) => if(__f(__m) < __f(__e)) {__m } else {__e}
+      )
+    }
 }