Remove min and max functions

tests/difference/core/quint_model/ccv.qnt

@@ -478,7 +478,7 @@ module ccv {
                         }
                     ).toList()
                 )
-                val newConsumerState2 = newConsumerState.with(
+                val newConsumerState2: ConsumerState = newConsumerState.with(
                     "maturationTimes", newMaturationTimes
                 ).with(
                     "outstandingPacketsToProvider", newOutstandingPackets
@@ -801,7 +801,9 @@ module ccv {
         CcvTimeout.keys().forall(chain => CcvTimeout.get(chain) > 0)
 
     run CcvTimeoutLargerThanUnbondingPeriodTest =
-        CcvTimeout.get(PROVIDER_CHAIN) > UnbondingPeriodPerChain.values().max()
+        UnbondingPeriodPerChain.values().forall(
+            value => CcvTimeout.get(PROVIDER_CHAIN) > value
+        )
 
     run ProviderIsNotAConsumerTest =
         not(ConsumerChains.contains(PROVIDER_CHAIN))

tests/difference/core/quint_model/ccv_model.qnt

@@ -205,6 +205,63 @@ module ccv_model {
             params' = params,
         }
 
+    // ==================
+    // UTILITY FUNCTIONS
+    // ==================
+
+    pure def earliest(packets: Set[VscPacket]): VscPacket =
+        val latestPossiblePacket: VscPacket = {
+            id: 0,
+            validatorSet: Map(),
+            sendingTime: 9999999999999 * Second,
+        }
+        packets.fold(
+            latestPossiblePacket,
+            (res, pack) => if(res.sendingTime < pack.sendingTime) { res } else { pack }
+        )
+
+    pure def latest(packets: Set[VscPacket]): VscPacket =
+        val earliestPossiblePacket: VscPacket = {
+            id: 0,
+            validatorSet: Map(),
+            sendingTime: -9999999999 * Second,
+        }
+        packets.fold(
+            earliestPossiblePacket,
+            (res, pack) => if(res.sendingTime >= pack.sendingTime) { res } else { pack }
+        )
+
+    // run maxByTest =
+    // all {
+    //   assert(maxBy(Set(1, 2, 3), __x => __x) == 3),
+    //   assert(maxBy(Set(1, 2, 3), __x => -__x) == 1),
+    // }
+    run earliestLatestTest = {
+    val packet1 = {
+            id: 1,
+            validatorSet: Map(),
+            sendingTime: 1 * Second,
+        }
+
+        val packet2 = {
+            id: 2,
+            validatorSet: Map(),
+            sendingTime: 2 * Second,
+        }
+
+        val packet3 = {
+            id: 3,
+            validatorSet: Map(),
+            sendingTime: 3 * Second,
+        }
+        all {
+            assert(earliest(Set(packet1, packet2, packet3)) == packet1),
+            assert(earliest(Set(packet3, packet2, packet1)) == packet1),
+            assert(latest(Set(packet1, packet2, packet3)) == packet3),
+            assert(latest(Set(packet3, packet2, packet1)) == packet3),
+        }
+    }
+
     // ==================
     // INVARIANT CHECKS
     // ==================
@@ -251,8 +308,8 @@ module ccv_model {
                     if (commonPackets.size() == 0) {
                         true // they don't share any packets, so nothing to check
                     } else {
-                        val newestCommonPacket = commonPackets.maxBy(packet => packet.sendingTime)
-                        val oldestCommonPacket = commonPackets.minBy(packet => packet.sendingTime)
+                        val newestCommonPacket = commonPackets.latest()
+                        val oldestCommonPacket = commonPackets.earliest()
                         // 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

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

@@ -168,46 +168,4 @@ module extraSpells {
         assert(values(Map(1 -> 2, 3 -> 4)) == Set(2, 4)),
         assert(values(Map()) == Set())
     }
-
-    // Returns the maximal element of the set.
-    // If the set is empty, the function call will fail at runtime.
-    pure def max(__set: Set[int]): int = maxBy(__set, __a => __a)
-
-    run maxTest =
-    all {
-        assert(max(Set(1, 2, 3)) == 3),
-    }
-
-    // Returns the minimal element of the set.
-    // If the set is empty, the function call will fail at runtime.
-    pure def min(__set: Set[int]): int = minBy(__set, __a => __a)
-
-    run minTest =
-    all {
-        assert(min(Set(1, 2, 3)) == 1),
-    }
-
-    // Returns the maximum element of a set, according to a given function.
-    // If two elements are equally large, an arbitrary one will be returned.
-    // If the set is empty, the function call will fail at runtime.
-    pure def maxBy(__set: Set[a], __f: a => int): a = {
-      __set.fold(
-        oneOf(__set),
-        (__m, __e) => if(__f(__m) > __f(__e)) {__m } else {__e}
-      )
-    }
-
-    run maxByTest =
-    all {
-      assert(maxBy(Set(1, 2, 3), __x => __x) == 3),
-      assert(maxBy(Set(1, 2, 3), __x => -__x) == 1),
-    }
-
-    // Like maxBy, but returns the minimum element.
-    pure def minBy(__set: Set[a], __f: a => int): a = {
-      __set.fold(
-        oneOf(__set),
-        (__m, __e) => if(__f(__m) < __f(__e)) {__m } else {__e}
-      )
-    }
 }