From a71ccb8fd1331ef0679cd0fdc539bde1a59149ef Mon Sep 17 00:00:00 2001
From: Josef Widder <josef@informal.systems>
Date: Wed, 24 Apr 2024 13:58:00 +0200
Subject: [PATCH] added temporal block properties

---
 specs/quint/specs/reset.qnt | 33 +++++++++++++++++++++++++++++++--
 1 file changed, 31 insertions(+), 2 deletions(-)

diff --git a/specs/quint/specs/reset.qnt b/specs/quint/specs/reset.qnt
index 1874b8a46..dc23e8b0a 100644
--- a/specs/quint/specs/reset.qnt
+++ b/specs/quint/specs/reset.qnt
@@ -431,7 +431,7 @@ def invalidated (b: L2Block) : bool =
     L1.last().provenHeight < b.height and
     L1.last().l2forkID > b.forkID
 
-def valid (b: L2Block, t: Time) : bool = 
+def valid (b: L2Block) : bool = 
     match makeProof(L2, b.height, L1) {
         | Invalid => false
         | None => false
@@ -441,11 +441,40 @@ def valid (b: L2Block, t: Time) : bool =
                                 bp) // whether a proof is accepted is time-dependend
     }
 
-// If a block is finalized it stays finalized
+
+
+// If a block is finalized it stays finalized (that is, it is never removed from L2)
+temporal stableFinalized = always(
+    L2.toSet().forall(b => 
+        (finalized(b) implies always(finalized(b)))
+))
+
 // If a block is invalidated it will eventually not be in L2 anymore
+temporal invalidatedRemoved = always(
+    L2.toSet().forall(b => 
+        (invalidated(b) implies eventually(not(decided(b))))
+))
+
 // If a block is invalidated it will never be finalized
+temporal invalidatedNeverFinalized = always(
+    L2.toSet().forall(b => 
+        (invalidated(b) implies always(not(finalized(b))))
+))
+
 // If a block is valid then there is an execution where it is finalized (it need not be finalized in all executions)
+// should fail to be verified. A counterexample will give a trace where a valid block eventually becomes finalized
+temporal validHasNoPathtoFinalized = always(
+    L2.toSet().forall(b => 
+        (valid(b) implies always(not(finalized(b))))
+))
+
 // If a block is valid then eventually it will be invalidated or finalized
+temporal validProgress = always(
+    L2.toSet().forall(b => 
+        (valid(b) implies eventually(finalized(b) or invalidated(b))))
+)
+
+
 
 // For every height there is eventually a finalized block of that height