Change Error type to string

cosmos · Oct 16, 2023 · 86324b7 · 86324b7
1 parent 70cd774
commit 86324b7
Show file tree

Hide file tree

Showing 2 changed files with 27 additions and 38 deletions.
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
@@ -143,9 +143,7 @@ module ccv_types {
             consumerStates: Map(),
         }
 
-    type Error = {
-        message: str
-    }
+    type Error = str
 
     // we return either a result or an error.
     // if hasError() is true, newState may be arbitrary, but the error will be meaningful.
@@ -158,9 +156,7 @@ module ccv_types {
     pure def Ok(newState: ProtocolState): Result = {
         {
             newState: newState,
-            error: {
-                message: ""
-            }
+            error: ""
         }
     }
 
@@ -182,13 +178,11 @@ module ccv_types {
                 },
                 consumerStates: Map(),
             },
-            error: {
-                message: msg
-            }
+            error: msg
         }
     }
 
-    pure def hasError(result: Result): bool = result.error.message != ""
+    pure def hasError(result: Result): bool = result.error != ""
 
     // possible consumer statuses
     pure val STOPPED = "stopped" // the chain was once a consumer chain, but has been voluntarily dropped by the provider.
@@ -306,7 +300,7 @@ module ccv {
                 val result = recvPacketOnProvider(currentState, sender, packet)
                 val tmpState = result.newState
                 if (result.hasError()) {
-                    (Err(result.error.message), false)
+                    (result, false)
                 } else {
                     (Ok(removeOutstandingPacketFromConsumer(tmpState, sender)), false) // false because the packet did not time out
                 }
@@ -355,7 +349,7 @@ module ccv {
                 val result = recvPacketOnConsumer(currentState, receiver, packet)
                 val tmpState = result.newState
                 if (result.hasError()) {
-                    (Err(result.error.message), false)
+                    (result, false)
                 } else {
                     (Ok(removeOutstandingPacketFromProvider(tmpState, receiver)), false) // false because the packet did not time out
                 }
@@ -652,21 +646,18 @@ module ccv {
             // update the running validator set, but not the history yet,
             // as that only happens when the next block is started
             val currentConsumerState = currentState.consumerStates.get(receiver)
-            val newConsumerState = currentConsumerState.with(
-                "chainState",
-                currentConsumerState.chainState.with(
-                    "currentValidatorSet", packet.validatorSet
-                )
-            ).with(
-                "maturationTimes",
-                currentConsumerState.maturationTimes.put(
-                    packet, 
-                    currentConsumerState.chainState.lastTimestamp + UnbondingPeriodPerChain.get(receiver)
-                )
-            ).with(
-                "receivedVscPackets",
-                currentConsumerState.receivedVscPackets.prepend(packet)
-            )
+            val newConsumerState = 
+                {
+                    ...currentConsumerState,
+                    chainState: currentConsumerState.chainState.with(
+                        "currentValidatorSet", packet.validatorSet
+                    ),
+                    maturationTimes: currentConsumerState.maturationTimes.put(
+                        packet, 
+                        currentConsumerState.chainState.lastTimestamp + UnbondingPeriodPerChain.get(receiver)
+                    ),
+                    receivedVscPackets: currentConsumerState.receivedVscPackets.prepend(packet)
+                }
             val newConsumerStates = currentState.consumerStates.set(receiver, newConsumerState)
             val newState = currentState.with(
                 "consumerStates", newConsumerStates

diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt
@@ -198,18 +198,16 @@ module ccv_model {
     val ValUpdatePrecondition = trace[trace.length()-1].kind == "EndAndBeginBlockForProvider"
     val ValidatorUpdatesArePropagatedInv = 
         // when the provider has just entered a validator set into a block...
-        if (ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock) {
-            val providerValSetInCurBlock = providerValidatorHistory.head()
-            // ... for each consumer that is running then ...
-            runningConsumers.forall(
-                // ...the validator set is in a sent packet
-                consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists(
-                    packet => packet.validatorSet == providerValSetInCurBlock
-                )
+        ValUpdatePrecondition and currentState.providerState.providerValidatorSetChangedInThisBlock
+            implies
+        val providerValSetInCurBlock = providerValidatorHistory.head()
+        // ... for each consumer that is running then ...
+        runningConsumers.forall(
+            // ...the validator set is in a sent packet
+            consumer => currentState.providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists(
+                packet => packet.validatorSet == providerValSetInCurBlock
             )
-        } else {
-            true
-        }
+        )
 
     // Every consumer chain receives the same sequence of 
     // ValidatorSetChangePackets in the same order.