From c94b8a2836eacd08b256c840f0ef9166a246ceb0 Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Mon, 29 Jan 2024 10:33:16 +0100
Subject: [PATCH] Add more comments, remove unnecessary disjuncts

---
 tests/mbt/model/ccv_model.qnt | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/tests/mbt/model/ccv_model.qnt b/tests/mbt/model/ccv_model.qnt
index 476b6365eb..eb4e266184 100644
--- a/tests/mbt/model/ccv_model.qnt
+++ b/tests/mbt/model/ccv_model.qnt
@@ -311,9 +311,11 @@ module ccv_model {
     // Every validator set on any consumer chain MUST either be or have been 
     // a validator set on the provider chain.
     val ValidatorSetHasExistedInv =
-        runningConsumers.forall(chain =>
+        runningConsumers.forall(chain => // for all running consumers
             currentState.consumerStates.get(chain).chainState.votingPowerHistory.toSet().forall(
+                // go through all its historical and current validator sets
                 validatorSet => providerValidatorHistory.toSet().contains(validatorSet)
+                // and check that they are also historical or current validator sets on the provider
             )
         )
 
@@ -331,10 +333,6 @@ module ccv_model {
             consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists(
                 packet => packet.validatorSet == providerValSetInCurBlock
             )
-            // or the consumer was just started, which we detect by the consumer having a timestamp of 0
-            // and the consumer having the validator set that was just sent in the block
-            or 
-            (currentState.consumerStates.get(consumer).chainState.lastTimestamp == 0 and currentState.consumerStates.get(consumer).chainState.currentValidatorSet == providerValSetInCurBlock)
         )
 
     // Every consumer chain receives the same sequence of 
@@ -381,8 +379,11 @@ module ccv_model {
     val lastTimeAdvancement = trace[trace.length()-1].timeAdvancement
     val lastBlockTime = currentState.consumerStates.get(ConsumerWithPotentialMaturations).chainState.lastTimestamp - lastTimeAdvancement
     val MatureOnTimeInv =
+        // if a consumer ended a block
         MaturationPrecondition
         implies
+        // then all matured packets need to have been processed and removed from the packets
+        // waiting to mature
         currentState.consumerStates.get(ConsumerWithPotentialMaturations).maturationTimes.toSet().forall(
             pair => 
             val maturationTime = pair._2 
@@ -699,9 +700,11 @@ module ccv_model {
     val providerKeyAssignedValSetHistory = currentState.providerState.keyAssignedValSetHistory
 
     val ValidatorSetHasExistedKeyAssignmentInv =
-        runningConsumers.forall(chain =>
+        runningConsumers.forall(chain => // for every running consumer
             currentState.consumerStates.get(chain).chainState.votingPowerHistory.toSet().forall(
+                // for every validator set the consumer ever had
                 validatorSet => providerKeyAssignedValSetHistory.getOrElse(chain, List()).toSet().exists(
+                    // that validator set needs to also have existed on the provider
                     provValSet => removeZeroPowers(provValSet) == removeZeroPowers(validatorSet)
                 )
             )
@@ -724,10 +727,6 @@ module ccv_model {
                     packet.validatorSet == 
                     applyKeyAssignmentToValSet(providerState, consumer, providerValSetInCurBlock)
             )
-            // or the consumer was just started, which we detect by the consumer having a timestamp of 0
-            // and the consumer having the validator set that was just sent in the block
-            or 
-            (currentState.consumerStates.get(consumer).chainState.lastTimestamp == 0 and currentState.consumerStates.get(consumer).chainState.currentValidatorSet == providerValSetInCurBlock)
         )
 
     // Every consumer chain receives the same sequence of 
@@ -779,6 +778,8 @@ module ccv_model {
                                     packet.validatorSet)
                             }))
                         )
+                        // check that the packets between the common packets are equal
+                        // when key assignment is reversed
                         packetsBetween1noKeyAssignment == packetsBetween2noKeyAssignment
                     }
                 }