Fix model and randomly run invariant checks

tests/difference/core/quint_model/README.md

@@ -20,27 +20,34 @@ The parameters of the protocol are defined as consts in ccv.qnt.
 
 ### Tests
 
-To run unit tests, run `quint test ccv_test.qnt`.
+To run unit tests, run 
+```
+quint test ccv_test.qnt --main CCVTest
+```
+and 
+```
+quint test ccv_statemachine.qnt --main CCVDefaultStateMachine
+```
 
 ### Invariants
 
-The invariants I am checking are in ccv_statemachine.qnt.
+The invariants to check are in ccv_statemachine.qnt.
 Check a single invariant by running
 `quint run --invariant INVARIANT_NAME ccv_statemachine.qnt --main CCVDefaultStateMachine`,
 or all invariants one after another with the help of the script `run_invariants.sh`.
 Each invariant takes about a minute to run.
 
 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.
+- [X] ValidatorUpdatesArePropagated: When a validator power update is comitted on chain, a packet containing that change in voting power is sent to all running consumers.
+- [X] ValidatorSetHasExistedInv: Every validator set on consumer chains is/was a validator set on the provider.
+- [X] 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 
+- [X] 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.
-- [ ] EventuallyMatureOnProviderInv: If we send a VSCPacket, this is eventually responded to by all consumers
+- [X] EventuallyMatureOnProviderInv: 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).
 
 ### Sanity Checks

tests/difference/core/quint_model/ccv.qnt

@@ -405,9 +405,9 @@ module CCV {
 
 
 
-    // Ends a block on the provider. This means that the current validator set is committed on chain,
-    // packets are queued, and the next block is started. Also, consumers that have passed
-    // the VSCTimeout without responding to a pending vscpacket are dropped.
+    /// Ends a block on the provider. This means that the current validator set is committed on chain,
+    /// packets are queued, and the next block is started. Also, consumers that have passed
+    /// the VSCTimeout without responding to a pending vscpacket are dropped.
     pure def endAndBeginBlockForProvider(
         currentState: ProtocolState,
         // by how much the timestamp should be advanced,
@@ -427,13 +427,18 @@ module CCV {
             "chainState", newChainState
         )
 
+        val tmpState = currentState.with(
+            "providerState", providerStateAfterTimeAdvancement
+        )
+
         // check for VSC timeouts
         val timedOutConsumers = getRunningConsumers(providerStateAfterTimeAdvancement).filter(
             consumer => 
-            val res = TimeoutDueToVSCTimeout(currentState, consumer)
+            val res = TimeoutDueToVSCTimeout(tmpState, consumer)
             res._1
         )
 
+
         // start/stop chains
         val res = providerStateAfterTimeAdvancement.consumerStatus.StartStopConsumers(
             consumersToStart,
@@ -448,10 +453,10 @@ module CCV {
 
         // for each consumer we just set to running, set its initial validator set to be the current one on the provider.
         val newConsumerStateMap =
-            currentState.consumerStates.keys().mapBy(
+            tmpState.consumerStates.keys().mapBy(
                 (consumer) => 
                 if (consumersToStart.contains(consumer)) {
-                    val currentConsumerState = currentState.consumerStates.get(consumer)
+                    val currentConsumerState = tmpState.consumerStates.get(consumer)
                     val newConsumerState = currentConsumerState.with(
                         "chainState", currentConsumerState.chainState.with(
                             "currentValidatorSet", providerStateAfterConsumerAdvancement.chainState.currentValidatorSet
@@ -462,7 +467,7 @@ module CCV {
                     currentState.consumerStates.get(consumer)
                 }
             )
-        val newState = currentState.with(
+        val newState = tmpState.with(
             "providerState", providerStateAfterConsumerAdvancement
         ).with(
             "consumerStates", newConsumerStateMap

tests/difference/core/quint_model/ccv_statemachine.qnt

@@ -199,8 +199,8 @@ module CCVDefaultStateMachine {
                     if (commonPackets.size() == 0) {
                         true // they don't share any packets, so nothing to check
                     } else {
-                        val oldestCommonPacket = packets1.head()
-                        val newestCommonPacket = packets1[packets1.length() - 1]
+                        val newestCommonPacket = commonPackets.MaxBy(packet => packet.sendingTime)
+                        val oldestCommonPacket = commonPackets.MinBy(packet => packet.sendingTime)
                         // 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
@@ -220,13 +220,14 @@ module CCVDefaultStateMachine {
     // 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.
+    // that has already matured, i.e. where the maturationTime is smaller-or-equal than the lastTimestamp
     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
+                    // check that the maturation time is in the future
+                    packet => maturationTimes.get(packet) >= currentState.consumerStates.get(consumer).chainState.lastTimestamp
                 )
             }
         )
@@ -244,7 +245,7 @@ module CCVDefaultStateMachine {
                 sentPackets.forall(
                     packet =>
                         // consumer still has time to respond
-                        currentState.providerState.chainState.lastTimestamp <= packet.sendingTime + VscTimeout or
+                        not(packet.sendingTime + VscTimeout < currentState.providerState.chainState.lastTimestamp) or
                         // consumer was dropped
                         currentState.providerState.consumerStatus.get(consumer) == STOPPED or
                         currentState.providerState.consumerStatus.get(consumer) == TIMEDOUT
@@ -291,20 +292,26 @@ module CCVDefaultStateMachine {
             consumer => 
                 currentState.consumerStates.get(consumer).outstandingPacketsToProvider.length() > 0
         ))
+
+    val CanReceiveMaturations =
+        not(ConsumerChains.exists(
+            consumer => 
+                currentState.providerState.receivedMaturations.size() > 0
+        ))
 
     // ==================
     // MANUAL TEST CASES
     // ==================
     // Manually written test cases to get confidence in the base operation of the protocol.
 
-    // Test a simple happy path where:
-    // * the consumer chain is set to running
-    // * a validator set change happens
-    // * a block is ended on the provider, i.e. a packet is sent to the consumer
-    // * the consumer receives the packet
-    // * the chains wait until the unbonding period is over
-    // * the consumer sends a VSCMaturedPacket to the provider
-    // * the provider receives the VSCMaturedPacket
+    /// Test a simple happy path where:
+    /// * the consumer chain is set to running
+    /// * a validator set change happens
+    /// * a block is ended on the provider, i.e. a packet is sent to the consumer
+    /// * the consumer receives the packet
+    /// * the chains wait until the unbonding period is over
+    /// * the consumer sends a VSCMaturedPacket to the provider
+    /// * the provider receives the VSCMaturedPacket
     run HappyPathTest: bool = { 
         init.then(
             all {
@@ -385,4 +392,78 @@ module CCVDefaultStateMachine {
                 }
             )
         }
+
+    /// a manual test case for the SameVSCPacketsInv, since it needs very specific behaviour to even apply.
+    run SameVSCPacketsManualTest =
+        init.then(
+            // start all consumers except for consumer3
+            EndAndBeginBlockForProvider(1 * Second, Set("consumer1", "consumer2"), Set())
+        ).then(
+            // change voting power
+            VotingPowerChange("node1", 50)
+        ).then(
+            // send packet to consumer1 and consumer2
+            EndAndBeginBlockForProvider(1 * Second, Set(), Set())
+        ).then(
+            // deliver the packets
+            DeliverVSCPacket("consumer1")
+        ).then(
+            // deliver to consumer2
+            DeliverVSCPacket("consumer2")
+        ).then(
+            // start consumer3
+            EndAndBeginBlockForProvider(1 * Second, Set("consumer3"), Set())
+        ).then(
+            // do another voting power change
+            VotingPowerChange("node2", 50)
+        ).then(
+            // send packets
+            EndAndBeginBlockForProvider(1 * Second, Set(), Set())
+        ).then(
+            //deliver to consumer1
+            DeliverVSCPacket("consumer1")
+        ).then(
+            // deliver to consumer2
+            DeliverVSCPacket("consumer2")
+        ).then(
+            // deliver to consumer3
+            DeliverVSCPacket("consumer3")
+        )
+        .then(
+            // the SameVSCPacketInv should hold here
+            all {
+                assert(SameVSCPacketsInv),
+                // action does not matter, but needed to have uniform effect
+                step
+            }
+        )
+
+    // a manual test for the EventuallyMatureOnProvider invariant
+    run VSCTimeoutManualTest =
+        init
+        .then(
+            // start all consumer chains
+            EndAndBeginBlockForProvider(1 * Second, ConsumerChains, Set())
+        )
+        .then(
+            // change voting power
+            VotingPowerChange("node1", 50)
+        )
+        .then(
+            // send packets
+            EndAndBeginBlockForProvider(1 * Second, Set(), Set())
+        )
+        .then(
+            // advance time on provider by VSCTimeout + 1 Second
+            EndAndBeginBlockForProvider(VscTimeout + 5 * Second, Set(), Set())
+        )
+        // .then(
+        //     all {
+        //         // the consumer chains should have timed out
+        //         assert(ConsumerChains.forall(
+        //             chain => currentState.providerState.consumerStatus.get(chain) == TIMEDOUT
+        //         )),
+        //         VotingPowerChange("node2", 50)// action needs to be there but does not matter
+        //     }
+        // )
 }

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

@@ -248,9 +248,9 @@ module extraSpells {
     }
 
     // Like MaxBy, but returns the minimum element.
-    pure def MinBy(__set: Set[a], __f: a => int, __i: a): a = {
+    pure def MinBy(__set: Set[a], __f: a => int): a = {
       __set.fold(
-        __i,
+        oneOf(__set),
         (__m, __e) => if(__f(__m) < __f(__e)) {__m } else {__e}
       )
     }

tests/difference/core/quint_model/run_invariants.sh

@@ -1 +1 @@
-quint run --invariant "all{ValidatorUpdatesArePropagated,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 200000 --max-samples 200 --out out.log
+quint run --invariant "all{ValidatorUpdatesArePropagated,ValidatorSetHasExistedInv,SameVSCPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv}" ccv_statemachine.qnt --main CCVDefaultStateMachine --max-steps 500 --max-samples 200 --out out.log