From f28d074ce70ebc9c37c08d34388f8ffbb9abcc59 Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Fri, 29 Sep 2023 16:05:32 +0200
Subject: [PATCH] Add invariants

---
 tests/difference/core/quint_model/README.md   | 18 ++++++++--
 .../core/quint_model/ccv_statemachine.qnt     | 36 ++++++++++++++++++-
 2 files changed, 50 insertions(+), 4 deletions(-)

diff --git a/tests/difference/core/quint_model/README.md b/tests/difference/core/quint_model/README.md
index 910cbe7232..6d1ad8d2be 100644
--- a/tests/difference/core/quint_model/README.md
+++ b/tests/difference/core/quint_model/README.md
@@ -20,6 +20,18 @@ 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`
-- 
\ No newline at end of file
+The invariants I am checking are in ccv_statemachine.qnt.
+Check a single invariant by running
+`quint run --invariant INVARIANT_NAME ccv_statemachine.qnt --main CCVDefaultStateMachine`,
+or all invariants by running this command:
+
+Invariants 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.
+- ValidatorSetHasExistedInv: Every validator set on consumer chains is/was a validator set on the provider.
+- SameVSCPacketsInv: Ensure that consumer chains receive the same VSCPackets in the same order.
+Because of nuances with starting/stopping consumers, this invariant is not as simple as it sounds. In detail:
+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 in the same order.
+- MatureOnTimeInv: For every ValidatorSetChangePacket received by a consumer chain at 
+time t, a MaturedVSCPacket is sent back to the provider in the first block 
+with a timestamp >= t + UnbondingPeriod on that consumer.
diff --git a/tests/difference/core/quint_model/ccv_statemachine.qnt b/tests/difference/core/quint_model/ccv_statemachine.qnt
index b8ad1a82f3..4a6ac2e558 100644
--- a/tests/difference/core/quint_model/ccv_statemachine.qnt
+++ b/tests/difference/core/quint_model/ccv_statemachine.qnt
@@ -208,7 +208,41 @@ module CCVDefaultStateMachine {
             )
         )
 
-    // val MaturedBeforeTimeoutInv =
+    // For every ValidatorSetChangePacket received by a consumer chain at 
+    // time t, a MaturedVSCPacket is sent back to the provider in the first block 
+    // with a timestamp >= t + UnbondingPeriod
+    // NOTE: because we remove the maturationTimes entry when we send the packets,
+    // it suffices to check that there is never an entry in maturationTimes
+    // that is older than the current time minus the unbonding period.
+    val MatureOnTimeInv =
+        runningConsumers.forall(
+            consumer => {
+                val maturationTimes = currentState.consumerStates.get(consumer).maturationTimes
+                maturationTimes.keys().forall(
+                    packet => packet.sendingTime + UnbondingPeriodPerChain.get(consumer) <= currentState.providerState.chainState.lastTimestamp
+                )
+            }
+        )
+
+    // If we send a VSCPacket, this is eventually responded to by all consumers
+    // that were running at the time the packet was sent (and are still running).
+    // Since we remove sentVSCPackets when we receive responses for them,
+    // we just check that if a sentVSCPacket has been sent more than
+    // VSCTimeout ago, the consumer must have been dropped.
+    // In practice, when this is true, a pending unbonding can mature.
+    val EventuallyMatureOnProviderInv =
+        runningConsumers.forall(
+            consumer => {
+                val sentPackets = currentState.providerState.sentVSCPackets.get(consumer).toSet()
+                sentPackets.forall(
+                    packet =>
+                        // consumer still has time to respond
+                        currentState.providerState.chainState.lastTimestamp <= packet.sendingTime + VscTimeout or
+                        // consumer was dropped due to inactivity
+                        currentState.providerState.consumerStatus.get(consumer) == STOPPED
+                )
+            }
+        )
 
 //     \* Invariants from https://github.com/cosmos/interchain-security/blob/main/docs/quality_assurance.md