Add timeout timestamps to packets

cosmos · Nov 29, 2023 · 1433ee4 · 1433ee4
1 parent 3286e09
commit 1433ee4
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 8 deletions.
diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
@@ -17,16 +17,21 @@ module ccv_types {
             id: VscId,
             // the new validator set. in the implementation, this would be a list of validator updates
             validatorSet: ValidatorSet,
-            // the time at which the packet was sent. used to check whether packets have timed out.
-            sendingTime: Time
+            // the time at which the packet was sent.
+            sendingTime: Time,
+            // the time (on the receiver) at which the packet will time out
+            timeoutTime: Time
+
         }
 
     type VscMaturedPacket = 
         {
             // the id of the VscPacket that matured
             id: VscId,
-            // the time at which the packet was sent. used to check whether packets have timed out.
-            sendingTime: Time
+            // the time at which the packet was sent.
+            sendingTime: Time,
+            // the time (on the receiver) at which the packet will time out
+            timeoutTime: Time
         }
 
 
@@ -276,7 +281,7 @@ module ccv {
             (Err("No outstanding packets to deliver"), false)
         } else {
             val packet = currentState.consumerStates.get(sender).outstandingPacketsToProvider.head()
-            if(packet.sendingTime + CcvTimeout.get(sender) < currentState.providerState.chainState.runningTimestamp) {
+            if(packet.timeoutTime <= currentState.providerState.chainState.runningTimestamp) {
                 // drop consumer
                 val result = stopConsumers(
                     currentState.providerState.consumerStatus,
@@ -325,7 +330,7 @@ module ccv {
         } else {
             val packet = currentState.providerState.outstandingPacketsToConsumer.get(receiver).head()
             // check if the consumer timed out
-            if (packet.sendingTime + CcvTimeout.get(PROVIDER_CHAIN) < currentState.consumerStates.get(receiver).chainState.runningTimestamp) {
+            if (packet.timeoutTime <= currentState.consumerStates.get(receiver).chainState.runningTimestamp) {
                 // drop consumer
                 val result = stopConsumers(
                     currentState.providerState.consumerStatus,
@@ -492,7 +497,8 @@ module ccv {
                     maturedPackets.transform(
                         packet => {
                             id: packet.id, 
-                            sendingTime: newChainState.runningTimestamp
+                            sendingTime: newChainState.runningTimestamp,
+                            timeoutTime: newChainState.runningTimestamp + CcvTimeout.get(chain)
                         }
                     )
                 )
@@ -632,7 +638,8 @@ module ccv {
                 List({
                         id: providerState.runningVscId,
                         validatorSet: providerState.chainState.currentValidatorSet,
-                          sendingTime: providerState.chainState.runningTimestamp
+                        sendingTime: providerState.chainState.runningTimestamp,
+                        timeoutTime: providerState.chainState.runningTimestamp + CcvTimeout.get(PROVIDER_CHAIN)
                 })
             } else {
                 List()

diff --git a/tests/difference/core/quint_model/ccv_model.qnt b/tests/difference/core/quint_model/ccv_model.qnt
@@ -230,6 +230,7 @@ module ccv_model {
             id: 0,
             validatorSet: Map(),
             sendingTime: 9999999999999 * Second,
+            timeoutTime: 9999999999999 * Second,
         }
         packets.fold(
             latestPossiblePacket,
@@ -241,6 +242,7 @@ module ccv_model {
             id: 0,
             validatorSet: Map(),
             sendingTime: -9999999999 * Second,
+            timeoutTime: -9999999999 * Second,
         }
         packets.fold(
             earliestPossiblePacket,
@@ -257,18 +259,21 @@ module ccv_model {
             id: 1,
             validatorSet: Map(),
             sendingTime: 1 * Second,
+            timeoutTime: 1 * Second,
         }
 
         val packet2 = {
             id: 2,
             validatorSet: Map(),
             sendingTime: 2 * Second,
+            timeoutTime: 2 * Second,
         }
 
         val packet3 = {
             id: 3,
             validatorSet: Map(),
             sendingTime: 3 * Second,
+            timeoutTime: 3 * Second,
         }
         all {
             assert(earliest(Set(packet1, packet2, packet3)) == packet1),