From 633f8bb3ff005b26eb1f22df52112a5c0a28e48a Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Fri, 29 Sep 2023 15:33:35 +0200
Subject: [PATCH] Make time module upper case

---
 .../core/quint_model/ccv_statemachine.qnt     | 28 ++++++++-----------
 .../libraries/{time.qnt => Time.qnt}          |  0
 2 files changed, 12 insertions(+), 16 deletions(-)
 rename tests/difference/core/quint_model/libraries/{time.qnt => Time.qnt} (100%)

diff --git a/tests/difference/core/quint_model/ccv_statemachine.qnt b/tests/difference/core/quint_model/ccv_statemachine.qnt
index 8f3b918f22..b8ad1a82f3 100644
--- a/tests/difference/core/quint_model/ccv_statemachine.qnt
+++ b/tests/difference/core/quint_model/ccv_statemachine.qnt
@@ -192,30 +192,26 @@ module CCVDefaultStateMachine {
                     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
+                        val oldestCommonPacket = packets1.head()
+                        val newestCommonPacket = packets1[packets1.length() - 1]
+                        // get all packets sent between the oldest and newest common packet
+                        val packetsBetween1 = packets1.select(
+                            packet => packet.sendingTime >= oldestCommonPacket.sendingTime and packet.sendingTime <= newestCommonPacket.sendingTime
+                        )
+                        val packetsBetween2 = packets2.select(
+                            packet => packet.sendingTime >= oldestCommonPacket.sendingTime and packet.sendingTime <= newestCommonPacket.sendingTime
+                        )
+                        // these should be the same on both chains
+                        packetsBetween1 == packetsBetween2
                     }
                 }
             )
         )
 
-        
-
+    // val MaturedBeforeTimeoutInv =
 
 //     \* Invariants from https://github.com/cosmos/interchain-security/blob/main/docs/quality_assurance.md
 
-// (*
-// 6.03 - Every consumer chain receives the same sequence of 
-// ValidatorSetChangePackets in the same order.
-
-// Note: consider only prefixes on received packets (ccvChannelsResolved)
-// *)
-// Inv603 == 
-//   \A c1,c2 \in LiveConsumers:
-//     \A i \in (DOMAIN ccvChannelsResolved[c1] \intersect DOMAIN ccvChannelsResolved[c2]):
-//       ccvChannelsResolved[c1][i] = ccvChannelsResolved[c2][i]
-
 // (*
 // 7.01 - For every ValidatorSetChangePacket received by a consumer chain at 
 // time t, a MaturedVSCPacket is sent back to the provider in the first block 
diff --git a/tests/difference/core/quint_model/libraries/time.qnt b/tests/difference/core/quint_model/libraries/Time.qnt
similarity index 100%
rename from tests/difference/core/quint_model/libraries/time.qnt
rename to tests/difference/core/quint_model/libraries/Time.qnt