Refactor the Quint specification after #144 (#146)

## What ❔

Following the pseudo-code updates in #144, this PR introduces updates in
the Quint specification, namely, moving `CommitQC` into `TimeoutQC` and
storing only `high_commit_qc_view` in `TimeoutVote` instead of storing
`high_commit_qc`.

## Why ❔

This update speeds-up model checking times dramatically, as `CommitQC`
fields in `TimeoutVote` were a major bottleneck.

~This change has broken multiple invariants. Hence, we have to further
fix the specification and the invariants before merging.~

Preliminary experiments show that the model checking times have improved
dramatically. For instance, we were able to find the expected violation
of agreement for `N=6`, `F=1`, and `B=2`.

---------

Co-authored-by: Bruno França <[email protected]>

.github/workflows/spec.yaml

@@ -16,11 +16,11 @@ jobs:
       - name: Install node
         uses: actions/setup-node@v4
         with:
-          node-version: ">= 18"
+          node-version: 20
           check-latest: true
 
       - name: Install quint
-        run: npm i @informalsystems/quint -g
+        run: npm i @informalsystems/quint@0.21.0 -g
 
       - name: Run test
         run: cd spec && make test

spec/protocol-spec/experiments/n6f1b0.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // A specification instance for n=6, f=1, and no Byzantine faults
 module n6f1b0 {
   import replica(
@@ -11,4 +12,4 @@ module n6f1b0 {
     VALID_BLOCKS = Set("val_b0", "val_b1"),
     INVALID_BLOCKS = Set("inv_b3")
   ).* from "../replica"
-}
+}

spec/protocol-spec/experiments/n6f1b0_guided_no_proposing_leader.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // A specification instance for n=6, f=1, and 1 Byzantine fault
 //
 // Due to import/export limitations of Quint, use the definitions starting with g_:
@@ -38,4 +39,4 @@ module n6f1b1_two_blocks {
 
     ]
   ).* from "../guided_replica"
-}
+}

spec/protocol-spec/experiments/n6f1b1.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // A specification instance for n=6, f=1, and 1 Byzantine fault
 module n6f1b1 {
   import replica(
@@ -11,4 +12,4 @@ module n6f1b1 {
     VALID_BLOCKS = Set("val_b0", "val_b1"),
     INVALID_BLOCKS = Set("inv_b3")
   ).* from "../replica"
-}
+}

spec/protocol-spec/experiments/n6f1b1_guided_dead_lock.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 1 Byzantine fault
 //
 /// Test a liveness issue where some validators have the HighQC but don't have the block payload and have to wait for it,
@@ -42,4 +44,4 @@ module n6f1b1_two_blocks {
             OnProposalStep("n1"), OnProposalStep("n2"), OnProposalStep("n3"), OnProposalStep("n4"), OnProposalStep("n5"),
         ]
     ).* from "../guided_replica"
-}
+}

spec/protocol-spec/experiments/n6f1b1_guided_two_blocks.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 1 Byzantine fault
 //
 // Due to import/export limitations of Quint, use the definitions starting with g_:
@@ -29,4 +31,4 @@ module n6f1b1_two_blocks {
       OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"),
     ]
   ).* from "../guided_replica"
-}
+}

spec/protocol-spec/experiments/n6f1b2.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 2 Byzantine faults
 module n6f1b2 {
   import replica(
@@ -11,4 +13,4 @@ module n6f1b2 {
     VALID_BLOCKS = Set("val_b0", "val_b1"),
     INVALID_BLOCKS = Set("inv_b3")
   ).* from "../replica"
-}
+}

spec/protocol-spec/experiments/n6f1b2_boxed.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 2 Byzantine faults.
 // We box the number of different steps.
 module n6f1b2_boxed {
@@ -137,4 +139,4 @@ module n6f1b2_boxed {
       }
     }
   }
-}
+}

spec/protocol-spec/experiments/n6f1b2_guided_agreement.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 2 Byzantine faults
 //
 // Due to import/export limitations of Quint, use the definitions starting with g_:
@@ -32,4 +34,4 @@ module n6f1b2_agreement {
       OnCommitStep("n3"), OnCommitStep("n3"), OnCommitStep("n3"), OnCommitStep("n3"), OnCommitStep("n3"),
     ]
   ).* from "../guided_replica"
-}
+}

spec/protocol-spec/experiments/n6f1b3.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and 3 Byzantine faults
 module n6f1b0 {
   import replica(
@@ -11,4 +13,4 @@ module n6f1b0 {
     VALID_BLOCKS = Set("val_b0", "val_b1"),
     INVALID_BLOCKS = Set("inv_b3")
   ).* from "../replica"
-}
+}

spec/protocol-spec/experiments/n7f1b0.qnt

@@ -1,7 +1,9 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and no Byzantine faults
 module n7f1b0 {
   import replica(
-    CORRECT = Set("n0", "n1", "n2", "n3", "n4", "n5", "n5"),
+    CORRECT = Set("n0", "n1", "n2", "n3", "n4", "n5", "n6"),
     FAULTY = Set(),
     WEIGHTS = Map("n0"->1, "n1"->1, "n2"->1, "n3"->1, "n4"->1, "n5"->1, "n6"->1),
     REPLICA_KEYS = Map("n0"->"n0", "n1"->"n1", "n2"->"n2", "n3"->"n3", "n4"->"n4", "n5"->"n5", "n6"->"n6"),
@@ -11,4 +13,4 @@ module n7f1b0 {
     VALID_BLOCKS = Set("val_b0", "val_b1"),
     INVALID_BLOCKS = Set("inv_b3")
   ).* from "../replica"
-}
+}

spec/protocol-spec/experiments/n7f1b0_quided_three_blocks.qnt

@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=7, f=1, and 0 byzantine nodes.
 //
 // Due to import/export limitations of Quint, use the definitions starting with g_:
@@ -63,4 +65,4 @@ module n6f1b1_two_blocks {
             OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), OnCommitStep("n0"), 
         ]
     ).* from "../guided_replica"
-}
+}

spec/protocol-spec/experiments/n7f1b1.qnt

@@ -0,0 +1,16 @@
+// -*- mode: Bluespec; -*-
+//
+// A specification instance for n=6, f=1, and no Byzantine faults
+module n7f1b1 {
+  import replica(
+    CORRECT = Set("n0", "n1", "n2", "n3", "n4", "n5"),
+    FAULTY = Set("n6"),
+    WEIGHTS = Map("n0"->1, "n1"->1, "n2"->1, "n3"->1, "n4"->1, "n5"->1, "n6"->1),
+    REPLICA_KEYS = Map("n0"->"n0", "n1"->"n1", "n2"->"n2", "n3"->"n3", "n4"->"n4", "n5"->"n5", "n6"->"n6"),
+    N = 7,
+    F = 1,
+    VIEWS = 0.to(3),
+    VALID_BLOCKS = Set("val_b0", "val_b1"),
+    INVALID_BLOCKS = Set("inv_b3")
+  ).* from "../replica"
+}

spec/protocol-spec/guided_replica.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // A restriction of replica.qnt to guide the model checker's search
 module guided_replica {
     import types.* from "./types"
@@ -139,4 +140,4 @@ module guided_replica {
             }
         }
     }
-}
+}

spec/protocol-spec/main.qnt

@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 /// A few handy small models that are good for debugging and inspection
 module main {
     // A specification instance for n=6, f=1, and 1 Byzantine fault
@@ -12,4 +13,4 @@ module main {
         VALID_BLOCKS = Set("val_b0", "val_b1"),
         INVALID_BLOCKS = Set("inv_b3")
   ) .* from "./replica"
-}
+}

spec/protocol-spec/option.qnt

@@ -28,10 +28,11 @@ module option {
         }
     }
 
-    // if is Some(e), test whether `pred(e)` holds true
+    // If is Some(e), test whether `pred(e)` holds true.
+    // If None, return false.
     def option_has(opt: Option[a], pred: a => bool): bool = {
         match (opt) {
-            | None => true
+            | None => false
             | Some(e) => pred(e)
         }
     }