Remove message sends for consumers that were started in this block

cosmos · Nov 23, 2023 · 436aec4 · 436aec4
1 parent db16905
commit 436aec4
Show file tree

Hide file tree

Showing 2 changed files with 55 additions and 44 deletions.
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
@@ -399,60 +399,61 @@ module ccv {
             res._1
         )
 
+        // send vsc packets
+        val providerStateAfterSending =
+            if (currentProviderState.providerValidatorSetChangedInThisBlock and 
+                // important: check this on the provider state after the consumer advancement, not on the current state.
+                getRunningConsumers(providerStateAfterTimeAdvancement).size() > 0) {
+                    providerStateAfterTimeAdvancement.sendVscPackets()
+                } else {
+                    providerStateAfterTimeAdvancement
+                }
+
 
         // start/stop chains
-        val res = providerStateAfterTimeAdvancement.consumerStatus.StartStopConsumers(
+        val res = providerStateAfterSending.consumerStatus.StartStopConsumers(
             consumersToStart,
             consumersToStop,
             timedOutConsumers
         )
         val newConsumerStatus = res._1
         val err = res._2
-        val providerStateAfterConsumerAdvancement = providerStateAfterTimeAdvancement.with(
+        val providerStateAfterConsumerAdvancement = providerStateAfterSending.with(
             "consumerStatus", newConsumerStatus
-        )
-
-        // for each consumer we just set to running, set its initial validator set to be the current one on the provider.
-        val valSet = providerStateAfterConsumerAdvancement.chainState.currentValidatorSet
-        val newConsumerStateMap =
-            tmpState.consumerStates.keys().mapBy(
-                (consumer) => 
-                if (consumersToStart.contains(consumer)) {
-                    val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer)
-                    val newConsumerState: ConsumerState = currentConsumerState.with(
-                        "chainState", currentConsumerState.chainState.with(
-                            "currentValidatorSet", valSet
-                        ).with(
-                            "votingPowerHistory",
-                            List(valSet)
-                        )
-                    )
-                    newConsumerState
-                } else {
-                    currentState.consumerStates.get(consumer)
-                }
-            )
-        val newState = tmpState.with(
-            "providerState", providerStateAfterConsumerAdvancement
         ).with(
-            "consumerStates", newConsumerStateMap
+            "providerValidatorSetChangedInThisBlock", false
         )
 
         if (err != "") {
             Err(err)
         } else {
-            val providerStateAfterSending =
-            if (currentProviderState.providerValidatorSetChangedInThisBlock and 
-                // important: check this on the provider state after the consumer advancement, not on the current state.
-                getRunningConsumers(providerStateAfterConsumerAdvancement).size() > 0) {
-                    providerStateAfterConsumerAdvancement.sendVscPackets()
-                } else {
-                    providerStateAfterConsumerAdvancement
-                }
-            val finalState = newState.with(
-                "providerState", providerStateAfterSending
+            // for each consumer we just set to running, set its initial validator set to be the current one on the provider.
+            val valSet = providerStateAfterConsumerAdvancement.chainState.currentValidatorSet
+            val newConsumerStateMap =
+                tmpState.consumerStates.keys().mapBy(
+                    (consumer) => 
+                    if (consumersToStart.contains(consumer)) {
+                        val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer)
+                        val newConsumerState: ConsumerState = currentConsumerState.with(
+                            "chainState", currentConsumerState.chainState.with(
+                                "currentValidatorSet", valSet
+                            ).with(
+                                "votingPowerHistory",
+                                List(valSet)
+                            )
+                        )
+                        newConsumerState
+                    } else {
+                        currentState.consumerStates.get(consumer)
+                    }
+                )
+            val newState = tmpState.with(
+                "providerState", providerStateAfterConsumerAdvancement
+            ).with(
+                "consumerStates", newConsumerStateMap
             )
-            Ok(finalState)
+
+            Ok(newState)
         }
     }
 

diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt
@@ -299,10 +299,14 @@ module ccv_model {
         val providerValSetInCurBlock = providerValidatorHistory.head()
         // ... for each consumer that is running then ...
         runningConsumers.forall(
-            // ...the validator set is in a sent packet
+            // ...the validator set is in a sent packet...
             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 
@@ -476,12 +480,18 @@ module ccv_model {
                 all {
                     // consumer1 was started
                     assert(currentState.providerState.consumerStatus.get("consumer1") == RUNNING),
-                    // a packet was sent to consumer1
-                    assert(currentState.providerState.outstandingPacketsToConsumer.get("consumer1").length() == 1),
+                    // but no packet was sent to consumer 1
+                    assert(currentState.providerState.outstandingPacketsToConsumer.get("consumer1").length() == 0),
                     // the validator set on the provider was entered into the history
                     assert(currentState.providerState.chainState.votingPowerHistory == List(InitialValidatorSet.put("node1", 150), InitialValidatorSet)),
-                    // deliver the packet
-                    DeliverVscPacket("consumer1")
+                    // change voting power on provider again
+                    VotingPowerChange("node1", 50).then(
+                        // end another block
+                        EndAndBeginBlockForProvider(1 * Second, Set(), Set())
+                    ).then(
+                        // deliver packet to consumer1
+                        DeliverVscPacket("consumer1")
+                    )
                 }
             )
             .then(
@@ -491,7 +501,7 @@ module ccv_model {
                     // ensure the maturation time was entered on the consumer
                     assert(currentState.consumerStates.get("consumer1").maturationTimes.length() == 1),
                     // the validator set was put as the current validator set
-                    assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet == InitialValidatorSet.put("node1", 150)),
+                    assert(currentState.consumerStates.get("consumer1").chainState.currentValidatorSet == InitialValidatorSet.put("node1", 200)),
                     // advance time on provider until the unbonding period is over
                     EndAndBeginBlockForProvider(UnbondingPeriodPerChain.get("consumer1"), Set(), Set()),
                 }