From 1414976497ad8d6285e9eef82f7d6d6e463a3def Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 4 Jul 2024 17:29:39 +0200
Subject: [PATCH 01/15] update the protocol according to #144

---
 spec/protocol-spec/replica.qnt | 163 ++++++++++++++++++---------------
 spec/protocol-spec/types.qnt   |  22 +++--
 2 files changed, 103 insertions(+), 82 deletions(-)

diff --git a/spec/protocol-spec/replica.qnt b/spec/protocol-spec/replica.qnt
index c7bf1002..8e297bae 100644
--- a/spec/protocol-spec/replica.qnt
+++ b/spec/protocol-spec/replica.qnt
@@ -106,9 +106,10 @@ module replica {
         }),
         replica_view' = CORRECT.mapBy(id => 0),
         proposer_view' = CORRECT.mapBy(id => 0),
-        // all correct replicas send TimeoutVote as their first step
+        // all correct replicas send SignedTimeoutVote as their first step
         msgs_signed_timeout' = CORRECT.map(id => {
-            vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc: HIGH_COMMIT_QC_NONE },
+            vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: None },
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
             sig: sig_of_id(id)
         }),
         msgs_signed_commit' = Set(),
@@ -131,14 +132,16 @@ module replica {
             votes: REPLICAS.map(id => sig_of_id(id)).mapBy(_ => {
                 view: 0,
                 high_vote: COMMIT_VOTE_NONE,
-                high_commit_qc: HIGH_COMMIT_QC_NONE
+                high_commit_qc_view: VIEW_NUMBER_NONE
             }),
             agg_sig: REPLICAS.map(id => sig_of_id(id)),
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
             ghost_view: 0,
         }
         pure val timeout_votes0 = REPLICAS.map(id => sig_of_id(id)).map(sig => {
             sig: sig,
-            vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc: HIGH_COMMIT_QC_NONE}, 
+            vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: VIEW_NUMBER_NONE },
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
         })
         all {
             replica_state' = CORRECT.mapBy(id => {
@@ -277,12 +280,15 @@ module replica {
             }
             nondet has_high_vote = oneOf(Bool)
             nondet has_commit_qc = oneOf(Bool)
+            nondet high_commit_qc_view = oneOf(VIEWS)
+            nondet has_high_commit_qc_view = oneOf(Bool)
             val signed_timeout_vote = {
                 vote: {
                     view: msg_view,
                     high_vote: if (has_high_vote) Some(commit_vote.vote) else COMMIT_VOTE_NONE,
-                    high_commit_qc: if (has_commit_qc) Some(commit_qc) else HIGH_COMMIT_QC_NONE,
+                    high_commit_qc_view: if (has_high_commit_qc_view) Some(high_commit_qc_view) else VIEW_NUMBER_NONE,
                 },
+                high_commit_qc: if (has_commit_qc) Some(commit_qc) else HIGH_COMMIT_QC_NONE,
                 sig: sig,
             }
             all {
@@ -294,7 +300,6 @@ module replica {
                 // add the message by a faulty replica
                 msgs_signed_timeout' = msgs_signed_timeout.union(Set(signed_timeout_vote)),
             }
-            
         },
         all {
             nondet msg_view = VIEWS.oneOf()
@@ -306,21 +311,27 @@ module replica {
             nondet commit_qc_block_hash = oneOf(ALL_BLOCKS)
             nondet commit_qc_agg_sig = REPLICAS.powerset().oneOf()
             val commit_qc_vote: CommitVote = {
-                view: commit_qc_view, block_number: commit_qc_block_number,
+                view: commit_qc_view,
+                block_number: commit_qc_block_number,
                 block_hash: commit_qc_block_hash
             }
             val commit_qc = {
                 vote: commit_qc_vote, agg_sig: commit_qc_agg_sig,
             }
-            // introduce a timeout qc
+            // Introduce a timeout qc.
+            // We recycle commit_qc when constructing timeout_qc, as commit_qc and timeout_qc
+            // are not used at the same time, see justification_case.
             nondet timeout_qc_view = VIEWS.oneOf()
             nondet timeout_qc_voters = REPLICAS.powerset().oneOf()
             nondet timeout_qc_agg_sig = timeout_qc_voters.powerset().oneOf()
             nondet timeout_qc_votes =
                 timeout_qc_voters.setOfMaps(msgs_signed_timeout.map(sv => sv.vote)).oneOf()
+            nondet has_high_commit_qc_view = oneOf(Bool)
             val timeout_qc: TimeoutQC = {
                 votes: timeout_qc_votes,
                 agg_sig: timeout_qc_agg_sig,
+                high_commit_qc:
+                    if (has_high_commit_qc_view) Some(commit_qc) else HIGH_COMMIT_QC_NONE,
                 ghost_view: timeout_qc_view,
             }
             // make new view
@@ -339,7 +350,7 @@ module replica {
                     FAULTY.contains(id),
                     msgs_signed_commit.exists(sv => sv.sig == id and sv.vote == commit_qc_vote),
                 }),
-                timeout_qc_agg_sig.forall(id => or {
+                justification_case != "commit" implies timeout_qc_agg_sig.forall(id => or {
                     FAULTY.contains(id),
                     msgs_signed_timeout.exists(sv => sv.sig == id and sv.vote == timeout_qc_votes.get(id)),
                 }),
@@ -363,15 +374,19 @@ module replica {
             val commit_qc = {
                 vote: commit_qc_vote, agg_sig: commit_qc_agg_sig,
             }
-            // introduce a timeout qc
+            // Introduce a timeout qc.
+            // We recycle commit_qc when constructing timeout_qc, as commit_qc and timeout_qc
+            // are not used at the same time, see justification_case.
             nondet timeout_qc_view = VIEWS.oneOf()
             nondet timeout_qc_voters = REPLICAS.powerset().oneOf()
             nondet timeout_qc_agg_sig = timeout_qc_voters.powerset().oneOf()
             nondet timeout_qc_votes =
                 timeout_qc_voters.setOfMaps(msgs_signed_timeout.map(sv => sv.vote)).oneOf()
+            nondet has_high_commit_qc_view = oneOf(Bool)
             val timeout_qc: TimeoutQC = {
                 votes: timeout_qc_votes,
                 agg_sig: timeout_qc_agg_sig,
+                high_commit_qc: if (has_high_commit_qc_view) Some(commit_qc) else HIGH_COMMIT_QC_NONE,
                 ghost_view: timeout_qc_view,
             }
             // non-deterministically select a block
@@ -396,7 +411,7 @@ module replica {
                     FAULTY.contains(id),
                     msgs_signed_commit.exists(sv => sv.sig == id and sv.vote == commit_qc_vote),
                 }),
-                timeout_qc_agg_sig.forall(id => or {
+                justification_case != "commit" implies timeout_qc_agg_sig.forall(id => or {
                     FAULTY.contains(id),
                     msgs_signed_timeout.exists(sv => sv.sig == id and sv.vote == timeout_qc_votes.get(id)),
                 }),
@@ -488,20 +503,20 @@ module replica {
                     // See validation below.
                     hash
                 }
-                
+
                 | None => {
                     // See state verification below.
                     unwrap_or(proposal.block, "").hash()
                 }
             }
-            
+
             // the replica vote to send
             val vote: CommitVote = {
                 view: proposal_view,
                 block_number: block_number,
                 block_hash: block_hash,
             }
-            
+
             all {
                 // Vote only if you have collected all committed blocks so far (see a check in all {...}).
                 block_number == length(self.committed_blocks),
@@ -539,7 +554,7 @@ module replica {
                     match (proposal.justification) {
                     | Commit(qc) => self1.process_commit_qc(Some(qc))
                     | Timeout(qc) => {
-                            ...self1.process_commit_qc(qc.high_qc()),
+                            ...self1.process_commit_qc(qc.high_commit_qc),
                             high_timeout_qc: max_timeout_qc(Some(qc), self1.high_timeout_qc)
                         }
                     }
@@ -612,9 +627,10 @@ module replica {
             vote: {
                 view: self.view,
                 high_vote: self.high_vote,
-                high_commit_qc: self.high_commit_qc,
+                high_commit_qc_view: self.high_commit_qc.option_map(qc => qc.vote.view),
             },
             sig: sig_of_id(id),
+            high_commit_qc: self.high_commit_qc,
         }
         all {
             // If we have already timed out, we don't need to send another timeout vote.
@@ -655,7 +671,7 @@ module replica {
 
                     | Some(qc) => all {
                         val self1 = {
-                            ...self.process_commit_qc(qc.high_qc()),
+                            ...self.process_commit_qc(qc.high_commit_qc),
                             high_timeout_qc: max_timeout_qc(qc_opt, self.high_timeout_qc)
                         }
                         start_new_view(id, self1, signed_vote.vote.view + 1, Timeout(qc)),
@@ -685,11 +701,11 @@ module replica {
                     | Commit(qc) => self.process_commit_qc(Some(qc))
 
                     | Timeout(qc) => {
-                        ...self.process_commit_qc(qc.high_qc()),
+                        ...self.process_commit_qc(qc.high_commit_qc),
                         high_timeout_qc: max_timeout_qc(Some(qc), self.high_timeout_qc)
                     }
                 }
-            
+
             if (new_view_view > self.view) {
                 start_new_view(id, self1, new_view_view, new_view.justification)
             } else {
@@ -956,6 +972,8 @@ module replica {
         if (view_signed_votes.size() < QUORUM_WEIGHT) {
             None
         } else {
+            val high_commit_qc: Option[CommitQC] = view_signed_votes.fold(HIGH_COMMIT_QC_NONE,
+                (prev_max_qc, sv) => max_commit_qc(prev_max_qc, sv.high_commit_qc))
             // Importantly, view_signed_votes does not have two votes with the same signature.
             // We check that in store_signed_timeout_all_inv.
             val qc_votes: ReplicaKey -> TimeoutVote =
@@ -963,7 +981,8 @@ module replica {
             Some({
                 votes: qc_votes,
                 agg_sig: view_signed_votes.map(v => v.sig),
-                ghost_view: view
+                high_commit_qc: high_commit_qc,
+                ghost_view: view,
             })
         }
     }
@@ -997,7 +1016,7 @@ module replica {
         match (justification) {
             | Timeout(qc) =>
                 qc.timeout_qc_verify()
-            
+
             | Commit(qc) =>
                 qc.commit_qc_verify()
         }
@@ -1030,7 +1049,7 @@ module replica {
 
     pure def signed_timeout_vote_verify(signed_vote: SignedTimeoutVote): bool = all {
         signed_vote.vote.view >= 0,
-        signed_vote.vote.high_commit_qc.option_has(qc => commit_qc_verify(qc)),
+        signed_vote.high_commit_qc.option_map(qc => qc.vote.view) == signed_vote.vote.high_commit_qc_view,
         timeout_vote_verify(signed_vote.vote)
     }
 
@@ -1047,18 +1066,17 @@ module replica {
     }
 
     // Timeout vote verification that a replica can do locally
-    // There are two invariants that are easy to check:
-    // self.view() >= self.high_vote.view() && self.high_vote.view() >= self.high_commit_qc.view()
     pure def timeout_vote_verify(vote: TimeoutVote): bool = all {
         vote.view >= 0,
         match vote.high_vote {
             | None => true
             | Some(high_vote) => and {
                     commit_vote_verify(high_vote),
+                    // There are two invariants that are easy to check but aren't required for correctness:
                     vote.view >= high_vote.view,
-                    match vote.high_commit_qc {
+                    match vote.high_commit_qc_view {
                         | None => true
-                        | Some(high_commit_qc) => high_vote.view >= high_commit_qc.vote.view
+                        | Some(v) => high_vote.view >= v
                     }
                 }
         }
@@ -1086,13 +1104,30 @@ module replica {
             qc.agg_sig.aggregate_verify(),
             // It is essential that no vote is missing
             qc.votes.keys() == qc.agg_sig,
+            // Check that all votes have the same view and get the highest commit QC view of the timeout QC.
+            val high_qc_view: Option[ViewNumber] =
+                votes.fold(VIEW_NUMBER_NONE, (prev_max_opt, v) => match (prev_max_opt) {
+                | None =>
+                    v.high_commit_qc_view
+                | Some(prev_max) =>
+                    if (v.high_commit_qc_view.option_has(qcv => qcv > prev_max)) {
+                        v.high_commit_qc_view
+                    } else {
+                        prev_max_opt
+                    }
+                })
             // Get the high commit QC of the timeout QC. We compare the high QC field of all
             // timeout votes in the QC, and get the highest one, if it exists.
             // We then need to verify that it is valid. We don't need to verify the commit QCs
             // of the other timeout votes, since they don't have any influence in the result.
-            match (qc.high_qc()) {
-                | None => true
-                | Some (high_qc) => high_qc.commit_qc_verify()
+            match (qc.high_commit_qc) {
+                | None =>
+                    high_qc_view.is_none()
+
+                | Some (high_qc) => and {
+                    high_qc_view == Some(high_qc.vote.view),
+                    commit_qc_verify(high_qc),
+                }
             }
         }
     }
@@ -1133,7 +1168,7 @@ module replica {
                 // all timeout votes in the QC, and get the highest one, if it exists.
                 match (qc_high_vote) {
                 | Some(hv) =>
-                        match (high_qc(qc)) {
+                        match (qc.high_commit_qc) {
                         | Some(hqc) =>
                             if (hv.block_number > hqc.vote.block_number) {
                                 // There was some proposal last view that might have been finalized.
@@ -1156,7 +1191,7 @@ module replica {
                         // Either the previous proposal was finalized or we know for certain
                         // that it couldn't have been finalized. Either way, we can propose
                         // a new block.
-                        match (high_qc(qc)) {
+                        match (qc.high_commit_qc) {
                             | Some(hqc) => (hqc.vote.block_number + 1, None)
                             | None => (0, None)
                         }
@@ -1193,25 +1228,6 @@ module replica {
         }
     }
 
-    /// Get the high QC of the timeout QC. We compare the high QC field of all 4f+1
-    /// timeout votes in the QC, and get the highest one.
-    pure def high_qc(qc: TimeoutQC): Option[CommitQC] = {
-        // Assumption: qc.votes does not have two different QCs for the same view.
-        qc.votes.keys().map(pk => qc.votes.get(pk)).fold(None, (max_qc_opt, v) => {
-            match (v.high_commit_qc) {
-                | None => max_qc_opt
-                | Some(hc_qc) =>
-                    // if max_qc is None, choose hc_qc, otherwise compare the views
-                    match (max_qc_opt) {
-                        | None =>
-                            Some(hc_qc)
-                        | Some(max_qc) =>
-                            if (hc_qc.vote.view > max_qc.vote.view) Some(hc_qc) else max_qc_opt
-                    }
-            }
-        })
-    }
-
     // -------------------------------------------------------------------------
     // Invariants to check
 
@@ -1266,7 +1282,11 @@ module replica {
     val no_timeout_equivocation_inv = tuples(msgs_signed_timeout, msgs_signed_timeout).forall(((m1, m2)) => or {
         not(m1.vote.view == m2.vote.view and m1.sig == m2.sig),
         FAULTY.exists(id => sig_of_id(id) == m1.sig),
-        m1.vote.high_vote == m2.vote.high_vote and m1.vote.high_commit_qc == m2.vote.high_commit_qc,
+        and {
+            m1.vote.high_vote == m2.vote.high_vote,
+            m1.high_commit_qc == m2.high_commit_qc,
+            m1.vote.high_commit_qc_view == m2.vote.high_commit_qc_view,
+        }
     })
 
     // a correct proposer should not send two new views in the same view
@@ -1305,10 +1325,10 @@ module replica {
                     // no duplicates
                     (v1.sig == v2.sig and v1.vote.view == v2.vote.view) implies (v1.vote == v2.vote),
                     // the quorums have an intersection
-                    match (v1.vote.high_commit_qc) {
+                    match (v1.high_commit_qc) {
                         | None => true
                         | Some(qc1) =>
-                            match (v2.vote.high_commit_qc) {
+                            match (v2.high_commit_qc) {
                                 | None => true
                                 | Some(qc2) => or {
                                     qc1.vote.view != qc2.vote.view,
@@ -1442,34 +1462,27 @@ module replica {
         match (qc_opt) {
             | None => true
             | Some(qc) => 
-                val signed_votes = qc.votes.keys().map(pk => {vote: qc.votes.get(pk), sig: pk })
-                val votes = signed_votes.map(v => v.vote)
+                val votes = qc.votes.keys().map(pk => qc.votes.get(pk))
                 val public_keys = qc.votes.keys()
                 and {
                     qc.ghost_view >= 0,
                     qc.agg_sig.aggregate_verify(),
-                    signed_votes.size() == qc.agg_sig.size(),
+                    votes.size() == qc.agg_sig.size(),
                     public_keys == qc.agg_sig,
-                    signed_votes.forall(v => v.signed_timeout_vote_verify()),
+                    votes.forall(v => v.timeout_vote_verify()),
                     // make sure that all votes are cast for the same view
                     votes.forall(v => qc.ghost_view == v.view),
-                    // even though quorums in the votes may slightly differ,
-                    // they must have enough votes in the intersection
-                    signed_votes.forall(v1 => signed_votes.forall(v2 => {
-                        match (v1.vote.high_commit_qc) {
-                            | None => true
-                            | Some(qc1) =>
-                                match (v2.vote.high_commit_qc) {
-                                    | None => true
-                                    | Some(qc2) => or {
-                                        qc1.vote.view != qc2.vote.view,
-                                        FAULTY.exists(id => sig_of_id(id) == v1.sig or sig_of_id(id) == v2.sig),
-                                        // TODO: use QUORUM_WEIGHT - F?
-                                        qc1.agg_sig.intersect(qc2.agg_sig).size() >= SUBQUORUM_WEIGHT,
-                                    }
-                                }
+                    // The commit quorum certificate with the highest view that all replicas in this
+                    // QC have observed, if any. It MUST match the highest `high_commit_qc_view` in `votes`.
+                    match (qc.high_commit_qc) {
+                    | None =>
+                        votes.forall(v => v.high_commit_qc_view.is_none())
+
+                    | Some(commit_qc) => and {
+                            votes.forall(v => v.view <= commit_qc.vote.view),
+                            votes.exists(v => v.view == commit_qc.vote.view)
                         }
-                    }))
+                    }
                 }
         }
     }
@@ -1527,7 +1540,7 @@ module replica {
             }
         })
     }
-    
+
     // a high vote is the highest among the votes sent by a replica
     val timeout_high_vote_is_highest_inv: bool = {
         msgs_signed_timeout.forall(tv => or {
@@ -1598,7 +1611,7 @@ module replica {
 
     // -------------------------------------------------------------------------
     // Falsy invariants to check reachability of certain states
-    
+
     // check this invariant to see an example of reaching PhaseCommit
     val phase_commit_example = CORRECT.forall(id => replica_state.get(id).phase != PhaseCommit)
 
diff --git a/spec/protocol-spec/types.qnt b/spec/protocol-spec/types.qnt
index aaeb37fe..5187798e 100644
--- a/spec/protocol-spec/types.qnt
+++ b/spec/protocol-spec/types.qnt
@@ -9,7 +9,7 @@ module types {
     type Block = str
 
     // For specification purposes, we represent a hash of a string `s` as
-    // the string `s`. This representation is collision-free, 
+    // the string `s`. This representation is collision-free,
     // and we interpret it as opaque.
     type BlockHash = str
 
@@ -98,9 +98,9 @@ module types {
             // This proposal is being proposed after a view where we timed out.
             // A timeout QC is just a collection of timeout votes (with at least
             // QUORUM_WEIGHT) for the previous view. Unlike with the Commit QC,
-            // timeout votes don't need to be identical. 
+            // timeout votes don't need to be identical.
         |   Timeout(TimeoutQC)
-        
+
 
     type CommitVote = {
         // The current view.
@@ -138,16 +138,21 @@ module types {
         view: ViewNumber,
         // The commit vote with the highest view that this replica has signed.
         high_vote: Option[CommitVote],
-        // The commit quorum certificate with the highest view that this replica
-	    // has observed.
-        high_commit_qc: Option[CommitQC],
+        // The view number of the highest commit quorum certificate that this replica
+        // has observed, if any.
+        high_commit_qc_view: Option[ViewNumber],
     }
 
+    pure val VIEW_NUMBER_NONE: Option[ViewNumber] = None
+
     type SignedTimeoutVote = {
         // The timeout.
         vote: TimeoutVote,
-        // Signature of the sender.
+        // Signature of the sender. This signature is ONLY over the vote field.
         sig: Signature,
+        // The commit quorum certificate with the highest view that this replica
+        // has observed, if any. It MUST match `high_commit_qc_view` in `vote`.
+        high_commit_qc: Option[CommitQC],
     }
 
     // If we have timeout votes with at least QUORUM_WEIGHT for the same
@@ -161,6 +166,9 @@ module types {
         // The aggregate signature of the replicas. We ignore the details here.
         // Can be something as simple as a vector of signatures.
         agg_sig: AggregateSignature,
+        // The commit quorum certificate with the highest view that all replicas in this
+        // QC have observed, if any. It MUST match the highest `high_commit_qc_view` in `votes`.
+        high_commit_qc: Option[CommitQC],
 
         // current view computed from the votes (not present in the original specification).
         ghost_view: ViewNumber,

From 3b531f72bef40f84c1ca437a87ed27058c8c7f06 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Thu, 4 Jul 2024 17:46:16 +0200
Subject: [PATCH 02/15] fix aux_timeout_qc_inv

---
 spec/protocol-spec/replica.qnt | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/spec/protocol-spec/replica.qnt b/spec/protocol-spec/replica.qnt
index 8e297bae..8c82bb47 100644
--- a/spec/protocol-spec/replica.qnt
+++ b/spec/protocol-spec/replica.qnt
@@ -627,7 +627,11 @@ module replica {
             vote: {
                 view: self.view,
                 high_vote: self.high_vote,
-                high_commit_qc_view: self.high_commit_qc.option_map(qc => qc.vote.view),
+                high_commit_qc_view:
+                    match (self.high_commit_qc) {
+                    | None => VIEW_NUMBER_NONE
+                    | Some(qc) => Some(qc.vote.view)
+                    }
             },
             sig: sig_of_id(id),
             high_commit_qc: self.high_commit_qc,
@@ -1049,7 +1053,10 @@ module replica {
 
     pure def signed_timeout_vote_verify(signed_vote: SignedTimeoutVote): bool = all {
         signed_vote.vote.view >= 0,
-        signed_vote.high_commit_qc.option_map(qc => qc.vote.view) == signed_vote.vote.high_commit_qc_view,
+        match (signed_vote.high_commit_qc) {
+        | None => signed_vote.vote.high_commit_qc_view.is_none()
+        | Some(qc) => Some(qc.vote.view) == signed_vote.vote.high_commit_qc_view
+        },
         timeout_vote_verify(signed_vote.vote)
     }
 
@@ -1467,7 +1474,6 @@ module replica {
                 and {
                     qc.ghost_view >= 0,
                     qc.agg_sig.aggregate_verify(),
-                    votes.size() == qc.agg_sig.size(),
                     public_keys == qc.agg_sig,
                     votes.forall(v => v.timeout_vote_verify()),
                     // make sure that all votes are cast for the same view

From 660672e93003cc425027236d9146a85bb2c96b16 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 5 Jul 2024 12:17:10 +0200
Subject: [PATCH 03/15] critical bugfix

---
 spec/protocol-spec/replica.qnt | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/spec/protocol-spec/replica.qnt b/spec/protocol-spec/replica.qnt
index 8c82bb47..3c529346 100644
--- a/spec/protocol-spec/replica.qnt
+++ b/spec/protocol-spec/replica.qnt
@@ -1054,8 +1054,12 @@ module replica {
     pure def signed_timeout_vote_verify(signed_vote: SignedTimeoutVote): bool = all {
         signed_vote.vote.view >= 0,
         match (signed_vote.high_commit_qc) {
-        | None => signed_vote.vote.high_commit_qc_view.is_none()
-        | Some(qc) => Some(qc.vote.view) == signed_vote.vote.high_commit_qc_view
+        | None =>
+                signed_vote.vote.high_commit_qc_view.is_none()
+        | Some(qc) => and {
+                Some(qc.vote.view) == signed_vote.vote.high_commit_qc_view,
+                commit_qc_verify(qc),
+            }
         },
         timeout_vote_verify(signed_vote.vote)
     }
@@ -1364,6 +1368,7 @@ module replica {
     // have justifications for the views below.
     val view_justification_continuous_inv = {
         VIEWS.forall(v => or {
+            v == 0,
             CORRECT.forall(id => replica_state.get(id).view < v),
             ghost_justifications.keys().exists(((id, other_view)) => other_view == v)
         })

From 70551609582ae942300996ce7194724b9c4cb4d5 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 5 Jul 2024 15:35:50 +0200
Subject: [PATCH 04/15] fix unit tests

---
 spec/protocol-spec/tests/unit_tests.qnt | 166 ++++++++++++------------
 1 file changed, 86 insertions(+), 80 deletions(-)

diff --git a/spec/protocol-spec/tests/unit_tests.qnt b/spec/protocol-spec/tests/unit_tests.qnt
index d0a525f2..52b3dc25 100644
--- a/spec/protocol-spec/tests/unit_tests.qnt
+++ b/spec/protocol-spec/tests/unit_tests.qnt
@@ -33,7 +33,8 @@ module tests {
         pure val timeout: Justification = Timeout({
             votes: Map(),
             agg_sig: Set(""),
-            ghost_view: 1
+            ghost_view: 1,
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
         })
 
         all {
@@ -80,13 +81,14 @@ module tests {
         ghost_view: 0,
         votes:
             Map(
-                "n0" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
-                "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
-                "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
-                "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
-                "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
-                "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }
-            )
+                "n0" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
+                "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
+                "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
+                "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
+                "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
+                "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }
+            ),
+        high_commit_qc: HIGH_COMMIT_QC_NONE,
     }
 
     val timeout_qc_2: TimeoutQC = {
@@ -94,13 +96,14 @@ module tests {
         ghost_view: 0,
         votes:
             Map(
-                "n0" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 0 },
-                "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
-                "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
-                "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
-                "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
-                "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }
-            )
+                "n0" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 0 },
+                "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
+                "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
+                "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
+                "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 },
+                "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 0 }
+            ),
+        high_commit_qc: HIGH_COMMIT_QC_NONE,
     }
 
     val timeout_qc_3: TimeoutQC = {
@@ -108,13 +111,14 @@ module tests {
         ghost_view: 2,
         votes:
             Map(
-                "n0" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 },
-                "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 },
-                "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 },
-                "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 },
-                "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 },
-                "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 }
-            )
+                "n0" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 },
+                "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 },
+                "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 },
+                "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 },
+                "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 },
+                "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 }
+            ),
+        high_commit_qc: HIGH_COMMIT_QC_NONE,
     }
 
     val timeout_qc_4: TimeoutQC = {
@@ -122,13 +126,14 @@ module tests {
         ghost_view: 2,
         votes:
             Map(
-                "n0" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 },
-                "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 },
-                "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 },
-                "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 },
-                "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 },
-                "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 }
-            )
+                "n0" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 },
+                "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 },
+                "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 },
+                "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 },
+                "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 },
+                "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 }
+            ),
+        high_commit_qc: HIGH_COMMIT_QC_NONE,
     }
 
     val timeout_qc_5: TimeoutQC = {
@@ -136,13 +141,14 @@ module tests {
         ghost_view: 2,
         votes:
             Map(
-                "n0" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 },
-                "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote1), view: 2 },
-                "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 },
-                "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 },
-                "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote3), view: 2 },
-                "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote3), view: 2 }
-            )
+                "n0" -> { high_commit_qc_view: Some(2), high_vote: Some(vote1), view: 2 },
+                "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote1), view: 2 },
+                "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 },
+                "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 },
+                "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote3), view: 2 },
+                "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote3), view: 2 }
+            ),
+        high_commit_qc: Some(commit_qc_1),
     }
 
     val timeout_qc_6: TimeoutQC = {
@@ -150,13 +156,14 @@ module tests {
         ghost_view: 2,
         votes:
             Map(
-                "n0" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 },
-                "n1" -> { high_commit_qc: Some(commit_qc_2), high_vote: Some(vote1), view: 2 },
-                "n2" -> { high_commit_qc: Some(commit_qc_3), high_vote: Some(vote2), view: 2 },
-                "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 },
-                "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote3), view: 2 },
-                "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote3), view: 2 }
-            )
+                "n0" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 },
+                "n1" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 },
+                "n2" -> { high_commit_qc_view: Some(2), high_vote: Some(vote2), view: 2 },
+                "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 },
+                "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote3), view: 2 },
+                "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote3), view: 2 }
+            ),
+        high_commit_qc: Some(commit_qc_1),
     }
 
     val timeout_qc_7: TimeoutQC = {
@@ -164,13 +171,14 @@ module tests {
         ghost_view: 2,
         votes:
             Map(
-                "n0" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 },
-                "n1" -> { high_commit_qc: Some(commit_qc_2), high_vote: Some(vote1), view: 2 },
-                "n2" -> { high_commit_qc: Some(commit_qc_3), high_vote: Some(vote1), view: 2 },
-                "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 },
-                "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 },
-                "n5" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(vote2), view: 2 }
-            )
+                "n0" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 },
+                "n1" -> { high_commit_qc_view: Some(2), high_vote: Some(vote1), view: 2 },
+                "n2" -> { high_commit_qc_view: Some(2), high_vote: Some(vote1), view: 2 },
+                "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 },
+                "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 },
+                "n5" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(vote2), view: 2 }
+            ),
+        high_commit_qc: Some(commit_qc_1),
     }
 
     val timeout_qc_8: TimeoutQC = {
@@ -178,13 +186,14 @@ module tests {
         ghost_view: 2,
         votes:
             Map(
-                "n0" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 },
-                "n1" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 },
-                "n2" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 },
-                "n3" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 },
-                "n4" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 },
-                "n5" -> { high_commit_qc: Some(commit_qc_1), high_vote: Some(vote1), view: 2 }
-            )
+                "n0" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 },
+                "n1" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 },
+                "n2" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 },
+                "n3" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 },
+                "n4" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 },
+                "n5" -> { high_commit_qc_view: Some(1), high_vote: Some(vote1), view: 2 }
+            ),
+        high_commit_qc: Some(commit_qc_1),
     }
 
     run high_vote_Test = {
@@ -201,15 +210,6 @@ module tests {
 
     }
 
-    run high_qc_Test = {
-        all {
-            assert(high_qc(timeout_qc_1) == HIGH_COMMIT_QC_NONE),
-            assert(high_qc(timeout_qc_5) == Some(commit_qc_1)),
-            assert(high_qc(timeout_qc_6) == Some(commit_qc_3)),
-        }
-
-    }
-
     run max_timeout_qc_Test = {
         all {
             max_timeout_qc(HIGH_TIMEOUT_QC_NONE, HIGH_TIMEOUT_QC_NONE) == HIGH_TIMEOUT_QC_NONE,
@@ -235,9 +235,10 @@ module tests {
             vote: {
                 view: 10,
                 high_vote: COMMIT_VOTE_NONE,
-                high_commit_qc: HIGH_COMMIT_QC_NONE
+                high_commit_qc_view: VIEW_NUMBER_NONE,
             },
             sig: "n1",
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
         }
     )   
      val signed_timeout_votes_2 = Set( 
@@ -245,57 +246,62 @@ module tests {
             vote: {
                 view: 10,
                 high_vote: COMMIT_VOTE_NONE,
-                high_commit_qc: HIGH_COMMIT_QC_NONE
+                high_commit_qc_view: VIEW_NUMBER_NONE,
             },
             sig: "n2",
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
         },
         {
             vote: {
                 view: 10,
                 high_vote: COMMIT_VOTE_NONE,
-                high_commit_qc: HIGH_COMMIT_QC_NONE
+                high_commit_qc_view: VIEW_NUMBER_NONE,
             },
             sig: "n3",
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
         },
         {
             vote: {
                 view: 10,
                 high_vote: COMMIT_VOTE_NONE,
-                high_commit_qc: HIGH_COMMIT_QC_NONE
+                high_commit_qc_view: VIEW_NUMBER_NONE,
             },
             sig: "n4",
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
         },
         {
             vote: {
                 view: 10,
                 high_vote: COMMIT_VOTE_NONE,
-                high_commit_qc: HIGH_COMMIT_QC_NONE
+                high_commit_qc_view: VIEW_NUMBER_NONE,
             },
             sig: "n1",
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
         },
         {
             vote: {
                 view: 10,
                 high_vote: COMMIT_VOTE_NONE,
-                high_commit_qc: HIGH_COMMIT_QC_NONE
+                high_commit_qc_view: VIEW_NUMBER_NONE,
             },
             sig: "n0",
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
         }
-
     )
 
     run get_timeout_qc_Test = {
-        val qc = {
+        val qc: TimeoutQC = {
                 ghost_view: 10,
                 agg_sig: Set("n0", "n1", "n2", "n3", "n4"),
                 votes: 
                     Map(
-                        "n0" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 },
-                        "n1" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 },
-                        "n2" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 },
-                        "n3" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 },
-                        "n4" -> { high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 }
-                    )
+                        "n0" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 },
+                        "n1" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 },
+                        "n2" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 },
+                        "n3" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 },
+                        "n4" -> { high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: COMMIT_VOTE_NONE, view: 10 }
+                    ),
+                high_commit_qc: HIGH_COMMIT_QC_NONE,
             }
         all {
             get_timeout_qc(signed_timeout_votes_1, 10) == HIGH_TIMEOUT_QC_NONE,

From e0befdc1095c08b249703c9d19a9761e396dbecb Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 5 Jul 2024 15:43:56 +0200
Subject: [PATCH 05/15] refactor tests_n6f1b0

---
 spec/protocol-spec/tests/tests_n6f1b0.qnt | 68 ++++++++++++-----------
 spec/protocol-spec/tests/tests_n6f1b1.qnt | 10 ++--
 2 files changed, 43 insertions(+), 35 deletions(-)

diff --git a/spec/protocol-spec/tests/tests_n6f1b0.qnt b/spec/protocol-spec/tests/tests_n6f1b0.qnt
index ee9edd9e..05a3f7aa 100644
--- a/spec/protocol-spec/tests/tests_n6f1b0.qnt
+++ b/spec/protocol-spec/tests/tests_n6f1b0.qnt
@@ -18,9 +18,10 @@ module tests_n6f1b0 {
 
     // an initial quorum certificate
     pure val init_timeout_qc: TimeoutQC = {
-        votes: CORRECT.mapBy(id => { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc: HIGH_COMMIT_QC_NONE}),
+        votes: CORRECT.mapBy(id => { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: VIEW_NUMBER_NONE }),
         agg_sig: CORRECT,
         ghost_view: 0,
+        high_commit_qc: HIGH_COMMIT_QC_NONE,
     }
 
     def replica_committed(id: ReplicaId): List[Block] = {
@@ -121,14 +122,15 @@ module tests_n6f1b0 {
         }
         val timeout_qc_v1: TimeoutQC = {
             votes: Map(
-                "n0" -> { view: 2, high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(commit_vote_v1_b0) },
-                "n1" -> { view: 2, high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(commit_vote_v1_b0) },
-                "n2" -> { view: 2, high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(commit_vote_v1_b0) },
-                "n3" -> { view: 2, high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(commit_vote_v1_b0) },
-                "n5" -> { view: 2, high_commit_qc: HIGH_COMMIT_QC_NONE, high_vote: Some(commit_vote_v1_b0) }
+                "n0" -> { view: 2, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(commit_vote_v1_b0) },
+                "n1" -> { view: 2, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(commit_vote_v1_b0) },
+                "n2" -> { view: 2, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(commit_vote_v1_b0) },
+                "n3" -> { view: 2, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(commit_vote_v1_b0) },
+                "n5" -> { view: 2, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: Some(commit_vote_v1_b0) }
             ), 
             agg_sig: Set("n0", "n1", "n2", "n3", "n5"),
-            ghost_view: 2
+            ghost_view: 2,
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
         }
         init_view_1_with_leader(Map(0 -> "n0", 1 -> "n5", 2 -> "n1", 3 -> "n2", 4 -> "n3", 5 -> "n4"))
             // the leader proposes, all replicas in view=1
@@ -250,15 +252,15 @@ module tests_n6f1b0 {
                 replica_state.get("n1").high_commit_qc==Some({ vote: commit_vote_v1_b0, agg_sig: Set("n0", "n1", "n2", "n3", "n5")}), unchanged_all
             })
             .expect(all_invariants)
-            .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1))
+            .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1))
             .expect(all_invariants)
-            .then(replica_receives_all_timeout_votes("n2", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1))
+            .then(replica_receives_all_timeout_votes("n2", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1))
             .expect(all_invariants)
-            .then(replica_receives_all_timeout_votes("n3", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1))
+            .then(replica_receives_all_timeout_votes("n3", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1))
             .expect(all_invariants)
-            .then(replica_receives_all_timeout_votes("n4", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1))
+            .then(replica_receives_all_timeout_votes("n4", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1))
             .expect(all_invariants)
-            .then(replica_receives_all_timeout_votes("n5", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1))
+            .then(replica_receives_all_timeout_votes("n5", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1))
             .expect(all_invariants)
             .then(all {
                 proposer_step("n1", "val_b1"),
@@ -295,26 +297,30 @@ module tests_n6f1b0 {
         })
     }
 
-    action replica_receives_all_timeout_votes(id: ReplicaId, high_vote: Option[CommitVote], high_commit_qc: Option[CommitQC], view: ViewNumber):bool = all {
-        on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n0"} ),
-        unchanged_leader_replica,
+    action replica_receives_all_timeout_votes(id: ReplicaId, high_vote: Option[CommitVote],
+            high_commit_qc_view: Option[ViewNumber], high_commit_qc: Option[CommitQC], view: ViewNumber):bool = {
+        val timeout_vote: TimeoutVote = { view: view, high_commit_qc_view: high_commit_qc_view, high_vote: high_vote }
+        all {
+            on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n0" }),
+            unchanged_leader_replica,
+        }
+        .then(all {
+            on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n1" }),
+            unchanged_leader_replica,
+        })
+        .then(all {
+            on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n2" }),
+            unchanged_leader_replica,
+        })
+        .then(all {
+            on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n3" }),
+            unchanged_leader_replica,
+        })
+        .then(all {
+            on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n4" }),
+            unchanged_leader_replica,
+        })
     }
-    .then(all {
-        on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n1"} ),
-        unchanged_leader_replica,
-    })
-    .then(all {
-        on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n2"} ),
-        unchanged_leader_replica,
-    })
-    .then(all {
-        on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n3"} ),
-        unchanged_leader_replica,
-    })
-    .then(all {
-        on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n4"} ),
-        unchanged_leader_replica,
-    })
 
     action five_replicas_get_propose(block: Block, block_number: BlockNumber,
             leader: ReplicaId, justification: Justification): bool = {
diff --git a/spec/protocol-spec/tests/tests_n6f1b1.qnt b/spec/protocol-spec/tests/tests_n6f1b1.qnt
index 49bcea9e..103ef92a 100644
--- a/spec/protocol-spec/tests/tests_n6f1b1.qnt
+++ b/spec/protocol-spec/tests/tests_n6f1b1.qnt
@@ -16,17 +16,19 @@ module tests {
     ).* from "../replica"
 
     // an initial quorum certificate from all replicas
-    val init_timeout_qc: TimeoutQC = {
-        votes: REPLICAS.mapBy(id => { view: 0, high_vote: None, high_commit_qc: None}),
-        agg_sig: REPLICAS,
+    pure val init_timeout_qc: TimeoutQC = {
+        votes: CORRECT.mapBy(id => { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: VIEW_NUMBER_NONE }),
+        agg_sig: CORRECT,
         ghost_view: 0,
+        high_commit_qc: HIGH_COMMIT_QC_NONE,
     }
 
     // an initial quorum certificate from the correct replicas
     val init_timeout_corr_qc: TimeoutQC = {
-        votes: CORRECT.mapBy(id => { view: 0, high_vote: None, high_commit_qc: None}),
+        votes: CORRECT.mapBy(id => { view: 0, high_vote: None, high_commit_qc_view: VIEW_NUMBER_NONE }),
         agg_sig: CORRECT,
         ghost_view: 0,
+        high_commit_qc: HIGH_COMMIT_QC_NONE,
     }
 
     def replica_committed(id: ReplicaId): List[Block] = {

From a44d3c299368789629ce5621fec200715956ce66 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 5 Jul 2024 15:46:57 +0200
Subject: [PATCH 06/15] refactor tests_n6f1b1

---
 spec/protocol-spec/tests/tests_n6f1b0.qnt |  2 +-
 spec/protocol-spec/tests/tests_n6f1b1.qnt | 58 ++++++++++++-----------
 2 files changed, 32 insertions(+), 28 deletions(-)

diff --git a/spec/protocol-spec/tests/tests_n6f1b0.qnt b/spec/protocol-spec/tests/tests_n6f1b0.qnt
index 05a3f7aa..b3212221 100644
--- a/spec/protocol-spec/tests/tests_n6f1b0.qnt
+++ b/spec/protocol-spec/tests/tests_n6f1b0.qnt
@@ -298,7 +298,7 @@ module tests_n6f1b0 {
     }
 
     action replica_receives_all_timeout_votes(id: ReplicaId, high_vote: Option[CommitVote],
-            high_commit_qc_view: Option[ViewNumber], high_commit_qc: Option[CommitQC], view: ViewNumber):bool = {
+            high_commit_qc_view: Option[ViewNumber], high_commit_qc: Option[CommitQC], view: ViewNumber): bool = {
         val timeout_vote: TimeoutVote = { view: view, high_commit_qc_view: high_commit_qc_view, high_vote: high_vote }
         all {
             on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n0" }),
diff --git a/spec/protocol-spec/tests/tests_n6f1b1.qnt b/spec/protocol-spec/tests/tests_n6f1b1.qnt
index 103ef92a..e6649aeb 100644
--- a/spec/protocol-spec/tests/tests_n6f1b1.qnt
+++ b/spec/protocol-spec/tests/tests_n6f1b1.qnt
@@ -38,10 +38,11 @@ module tests {
     run replicas_bootstrap_in_view0_Test = {
         pure val timeout_votes0 = CORRECT.map(id => {
             sig: sig_of_id(id),
-            vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc: HIGH_COMMIT_QC_NONE}, 
+            vote: { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: VIEW_NUMBER_NONE },
+            high_commit_qc: HIGH_COMMIT_QC_NONE, 
         })
         init_view_0_with_leader(Map(0 -> "n0", 1 -> "n0", 2 -> "n1", 3 -> "n2", 4 -> "n3"))
-            .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 0))
+            .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 0))
             .expect(all_invariants)
             .then(replica_receives_new_view("n1", Timeout(init_timeout_corr_qc)))
             .expect(all_invariants)
@@ -240,15 +241,15 @@ module tests {
             })
             .expect(all_invariants)
             // all replicas send TimeoutVote to each other, each replica gets all messages from all other replicas including itself
-            .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1))
+            .then(replica_receives_all_timeout_votes("n0", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1))
             .expect(all_invariants)
-            .then(replica_receives_all_timeout_votes("n1", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1))
+            .then(replica_receives_all_timeout_votes("n1", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1))
             .expect(all_invariants)
-            .then(replica_receives_all_timeout_votes("n2", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1))
+            .then(replica_receives_all_timeout_votes("n2", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1))
             .expect(all_invariants)
-            .then(replica_receives_all_timeout_votes("n3", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1))
+            .then(replica_receives_all_timeout_votes("n3", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1))
             .expect(all_invariants)
-            .then(replica_receives_all_timeout_votes("n4", COMMIT_VOTE_NONE, HIGH_COMMIT_QC_NONE, 1))
+            .then(replica_receives_all_timeout_votes("n4", COMMIT_VOTE_NONE, VIEW_NUMBER_NONE, HIGH_COMMIT_QC_NONE, 1))
             .expect(all_invariants)
             .then(all {
                 proposer_step("n1", "val_b1"),
@@ -301,27 +302,30 @@ module tests {
         })
     }
 
-    action replica_receives_all_timeout_votes(id: ReplicaId, high_vote: Option[CommitVote], high_commit_qc: Option[CommitQC], view: ViewNumber):bool = all {
-        on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n0"} ),
-        unchanged_leader_replica,
+    action replica_receives_all_timeout_votes(id: ReplicaId, high_vote: Option[CommitVote],
+            high_commit_qc_view: Option[ViewNumber], high_commit_qc: Option[CommitQC], view: ViewNumber): bool = {
+        val timeout_vote: TimeoutVote = { view: view, high_commit_qc_view: high_commit_qc_view, high_vote: high_vote }
+        all {
+            on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n0" }),
+            unchanged_leader_replica,
+        }
+        .then(all {
+            on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n1" }),
+            unchanged_leader_replica,
+        })
+        .then(all {
+            on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n2" }),
+            unchanged_leader_replica,
+        })
+        .then(all {
+            on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n3" }),
+            unchanged_leader_replica,
+        })
+        .then(all {
+            on_timeout(id, { vote: timeout_vote, high_commit_qc: high_commit_qc, sig: "n4" }),
+            unchanged_leader_replica,
+        })
     }
-    .then(all {
-        on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n1"} ),
-        unchanged_leader_replica,
-    })
-    .then(all {
-        on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n2"} ),
-        unchanged_leader_replica,
-    })
-    .then(all {
-        on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n3"} ),
-        unchanged_leader_replica,
-    })
-    .then(all {
-        on_timeout(id, {vote: { view: view, high_commit_qc: high_commit_qc, high_vote: high_vote}, sig: "n4"} ),
-        unchanged_leader_replica,
-    })
-    
 
     action replica_commits(id: ReplicaId, block_hash: BlockHash, block_number: BlockNumber, view: ViewNumber):bool = all {
         on_commit(id, { vote: {block_hash: block_hash, block_number: block_number, view: view }, sig:"n0"}),

From 35954804cbfb20fa3cdc84d1d8596fa6a6d7e5b8 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 5 Jul 2024 16:06:51 +0200
Subject: [PATCH 07/15] refactor tests_n6f1b2

---
 spec/protocol-spec/tests/tests_n6f1b2.qnt | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/spec/protocol-spec/tests/tests_n6f1b2.qnt b/spec/protocol-spec/tests/tests_n6f1b2.qnt
index b80cfd38..7f4a14d9 100644
--- a/spec/protocol-spec/tests/tests_n6f1b2.qnt
+++ b/spec/protocol-spec/tests/tests_n6f1b2.qnt
@@ -18,9 +18,10 @@ module tests_n6f1b2 {
 
     // an initial quorum certificate
     pure val init_timeout_qc: TimeoutQC = {
-        votes: REPLICAS.mapBy(id => { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc: HIGH_COMMIT_QC_NONE}),
+        votes: REPLICAS.mapBy(id => { view: 0, high_vote: COMMIT_VOTE_NONE, high_commit_qc_view: VIEW_NUMBER_NONE }),
         agg_sig: REPLICAS,
         ghost_view: 0,
+        high_commit_qc: HIGH_COMMIT_QC_NONE,
     }
 
     def replica_committed(id: ReplicaId): List[Block] = {
@@ -33,8 +34,8 @@ module tests_n6f1b2 {
     run disagreement_Test = {
         val high_vote_b0 = Some({ view: 1, block_number: 0, block_hash: "val_b0" })
         val high_vote_b1 = Some({ view: 1, block_number: 0, block_hash: "val_b1" })
-        val timeout_vote_b0: TimeoutVote = { view: 1, high_commit_qc: None, high_vote: high_vote_b0 }
-        val timeout_vote_b1: TimeoutVote = { view: 1, high_commit_qc: None, high_vote: high_vote_b1 }
+        val timeout_vote_b0: TimeoutVote = { view: 1, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: high_vote_b0 }
+        val timeout_vote_b1: TimeoutVote = { view: 1, high_commit_qc_view: VIEW_NUMBER_NONE, high_vote: high_vote_b1 }
         // n4 and n5 partition the correct replicas into n0, n1, n2 and n1, n2, n3
         val timeout_qc: TimeoutQC = {
             ghost_view: 1,
@@ -45,7 +46,8 @@ module tests_n6f1b2 {
                 } else {
                     timeout_vote_b1
                 }
-            })
+            }),
+            high_commit_qc: HIGH_COMMIT_QC_NONE,
         }
         val new_view_timeout: NewView = {
             sig: "n4",
@@ -123,10 +125,12 @@ module tests_n6f1b2 {
                 val timeout_vote_n4: SignedTimeoutVote = {
                     vote: timeout_vote_b1,
                     sig: "n4",
+                    high_commit_qc: HIGH_COMMIT_QC_NONE,
                 }
                 val timeout_vote_n5: SignedTimeoutVote = {
                     vote: timeout_vote_b1,
                     sig: "n5",
+                    high_commit_qc: HIGH_COMMIT_QC_NONE,
                 }
                 all {
                     msgs_signed_timeout' = msgs_signed_timeout.union(Set(timeout_vote_n4, timeout_vote_n5)),

From 5f466d8211de15dd912f5bea4458de37aa0ca880 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 5 Jul 2024 16:20:45 +0200
Subject: [PATCH 08/15] fix state_monitor

---
 spec/protocol-spec/state_monitor.qnt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/spec/protocol-spec/state_monitor.qnt b/spec/protocol-spec/state_monitor.qnt
index 08f3f153..96428489 100644
--- a/spec/protocol-spec/state_monitor.qnt
+++ b/spec/protocol-spec/state_monitor.qnt
@@ -16,7 +16,7 @@ module state_monitor {
       INVALID_BLOCKS = Set("inv_b3")
     ) as i from "./replica"
 
-    var old_replica_state: Option[ReplicaPubKey -> ReplicaState]
+    var old_replica_state: Option[ReplicaId -> ReplicaState]
 
     action init = all {
       i::init,
@@ -33,7 +33,7 @@ module state_monitor {
     // Within the same view, a replica’s phase can only change through two paths.
     // 1) Prepare→Commit→Timeout or 2) Prepare→Timeout.
     val phase_inv = {
-      def for_replica(id: ReplicaPubKey): bool = {
+      def for_replica(id: ReplicaId): bool = {
         match (old_replica_state) {
           | None =>
             true

From 864bdff8a370cf5ae5c976e308f8de4765e70b08 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Fri, 5 Jul 2024 17:32:25 +0200
Subject: [PATCH 09/15] fix all_replicas_high_timeout_qc_inv

---
 spec/protocol-spec/option.qnt  | 5 +++--
 spec/protocol-spec/replica.qnt | 6 ++++--
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/spec/protocol-spec/option.qnt b/spec/protocol-spec/option.qnt
index 3e061ca4..fcb918e2 100644
--- a/spec/protocol-spec/option.qnt
+++ b/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)
         }
     }
diff --git a/spec/protocol-spec/replica.qnt b/spec/protocol-spec/replica.qnt
index 3c529346..b0da038b 100644
--- a/spec/protocol-spec/replica.qnt
+++ b/spec/protocol-spec/replica.qnt
@@ -1418,8 +1418,10 @@ module replica {
             })
         }
 
-        replica_state.keys()
-            .forall(id => replica_state.get(id).high_timeout_qc.option_has(one_high_vote))
+        replica_state.keys().forall(id => {
+            val timeout_qc = replica_state.get(id).high_timeout_qc
+            timeout_qc.is_none() or timeout_qc.option_has(one_high_vote)
+        })
     }
 
     // There are no two quorums for different block hashes in one view.

From 4b868066482f388c5091e25649ab8b6c9cb1e7e0 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 17 Jul 2024 13:30:27 +0200
Subject: [PATCH 10/15] fix committed_blocks_have_justification_inv

---
 spec/protocol-spec/replica.qnt | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/spec/protocol-spec/replica.qnt b/spec/protocol-spec/replica.qnt
index b0da038b..f89ac1fd 100644
--- a/spec/protocol-spec/replica.qnt
+++ b/spec/protocol-spec/replica.qnt
@@ -1263,7 +1263,12 @@ module replica {
                 ghost_justifications.keys().exists(((id2, view)) => and {
                     id2 == id,
                     match (ghost_justifications.get((id2, view))) {
-                        | Timeout(qc) => false
+                        | Timeout(qc) =>
+                            qc.high_commit_qc.option_has(hqc => and {
+                                hqc.vote.block_number == block_number,
+                                hqc.vote.block_hash == block_hash,
+                                view == hqc.vote.view or view == hqc.vote.view + 1,
+                            })
                         | Commit(qc) => and {
                             qc.vote.block_number == block_number,
                             qc.vote.block_hash == block_hash,

From 6bd71a04725531fdc7503c919f2a1a79c8e3cf0f Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Tue, 23 Jul 2024 09:23:47 +0200
Subject: [PATCH 11/15] fix n7f1b0, add n7f1b1

---
 spec/protocol-spec/experiments/n7f1b0.qnt |  4 ++--
 spec/protocol-spec/experiments/n7f1b1.qnt | 14 ++++++++++++++
 2 files changed, 16 insertions(+), 2 deletions(-)
 create mode 100644 spec/protocol-spec/experiments/n7f1b1.qnt

diff --git a/spec/protocol-spec/experiments/n7f1b0.qnt b/spec/protocol-spec/experiments/n7f1b0.qnt
index b1beb6d7..43f08297 100644
--- a/spec/protocol-spec/experiments/n7f1b0.qnt
+++ b/spec/protocol-spec/experiments/n7f1b0.qnt
@@ -1,7 +1,7 @@
 // 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 +11,4 @@ module n7f1b0 {
     VALID_BLOCKS = Set("val_b0", "val_b1"),
     INVALID_BLOCKS = Set("inv_b3")
   ).* from "../replica"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n7f1b1.qnt b/spec/protocol-spec/experiments/n7f1b1.qnt
new file mode 100644
index 00000000..a710920e
--- /dev/null
+++ b/spec/protocol-spec/experiments/n7f1b1.qnt
@@ -0,0 +1,14 @@
+// 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"
+}

From 82578a74ac616334ec3848fe681a049ae2edc6df Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Sat, 27 Jul 2024 12:39:45 +0300
Subject: [PATCH 12/15] add syntax highlighting

---
 spec/protocol-spec/experiments/n6f1b0.qnt                     | 3 ++-
 .../experiments/n6f1b0_guided_no_proposing_leader.qnt         | 3 ++-
 spec/protocol-spec/experiments/n6f1b1.qnt                     | 3 ++-
 spec/protocol-spec/experiments/n6f1b1_guided_dead_lock.qnt    | 4 +++-
 spec/protocol-spec/experiments/n6f1b1_guided_two_blocks.qnt   | 4 +++-
 spec/protocol-spec/experiments/n6f1b2.qnt                     | 4 +++-
 spec/protocol-spec/experiments/n6f1b2_boxed.qnt               | 4 +++-
 spec/protocol-spec/experiments/n6f1b2_guided_agreement.qnt    | 4 +++-
 spec/protocol-spec/experiments/n6f1b3.qnt                     | 4 +++-
 spec/protocol-spec/experiments/n7f1b0.qnt                     | 2 ++
 spec/protocol-spec/experiments/n7f1b0_quided_three_blocks.qnt | 4 +++-
 spec/protocol-spec/experiments/n7f1b1.qnt                     | 2 ++
 spec/protocol-spec/guided_replica.qnt                         | 3 ++-
 spec/protocol-spec/main.qnt                                   | 3 ++-
 spec/protocol-spec/state_monitor.qnt                          | 3 ++-
 spec/protocol-spec/twins_n6f1b1.qnt                           | 3 ++-
 spec/protocol-spec/twins_n6f1b2.qnt                           | 3 ++-
 17 files changed, 41 insertions(+), 15 deletions(-)

diff --git a/spec/protocol-spec/experiments/n6f1b0.qnt b/spec/protocol-spec/experiments/n6f1b0.qnt
index 1c818d9e..9b97f80f 100644
--- a/spec/protocol-spec/experiments/n6f1b0.qnt
+++ b/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"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n6f1b0_guided_no_proposing_leader.qnt b/spec/protocol-spec/experiments/n6f1b0_guided_no_proposing_leader.qnt
index b26c1374..773b3351 100644
--- a/spec/protocol-spec/experiments/n6f1b0_guided_no_proposing_leader.qnt
+++ b/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"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n6f1b1.qnt b/spec/protocol-spec/experiments/n6f1b1.qnt
index c675ef99..62d518e5 100644
--- a/spec/protocol-spec/experiments/n6f1b1.qnt
+++ b/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"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n6f1b1_guided_dead_lock.qnt b/spec/protocol-spec/experiments/n6f1b1_guided_dead_lock.qnt
index 8d8f399a..12e7548e 100644
--- a/spec/protocol-spec/experiments/n6f1b1_guided_dead_lock.qnt
+++ b/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"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n6f1b1_guided_two_blocks.qnt b/spec/protocol-spec/experiments/n6f1b1_guided_two_blocks.qnt
index 8288ec21..a9363770 100644
--- a/spec/protocol-spec/experiments/n6f1b1_guided_two_blocks.qnt
+++ b/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"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n6f1b2.qnt b/spec/protocol-spec/experiments/n6f1b2.qnt
index 0eee87c9..c30ebf8f 100644
--- a/spec/protocol-spec/experiments/n6f1b2.qnt
+++ b/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"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n6f1b2_boxed.qnt b/spec/protocol-spec/experiments/n6f1b2_boxed.qnt
index 600b63ff..2426e0e0 100644
--- a/spec/protocol-spec/experiments/n6f1b2_boxed.qnt
+++ b/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 {
       }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n6f1b2_guided_agreement.qnt b/spec/protocol-spec/experiments/n6f1b2_guided_agreement.qnt
index a3d5b798..cf173538 100644
--- a/spec/protocol-spec/experiments/n6f1b2_guided_agreement.qnt
+++ b/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"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n6f1b3.qnt b/spec/protocol-spec/experiments/n6f1b3.qnt
index 683974bc..44cf5d9b 100644
--- a/spec/protocol-spec/experiments/n6f1b3.qnt
+++ b/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"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n7f1b0.qnt b/spec/protocol-spec/experiments/n7f1b0.qnt
index 43f08297..292e38df 100644
--- a/spec/protocol-spec/experiments/n7f1b0.qnt
+++ b/spec/protocol-spec/experiments/n7f1b0.qnt
@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and no Byzantine faults
 module n7f1b0 {
   import replica(
diff --git a/spec/protocol-spec/experiments/n7f1b0_quided_three_blocks.qnt b/spec/protocol-spec/experiments/n7f1b0_quided_three_blocks.qnt
index b0ae55e6..0a246b84 100644
--- a/spec/protocol-spec/experiments/n7f1b0_quided_three_blocks.qnt
+++ b/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"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/experiments/n7f1b1.qnt b/spec/protocol-spec/experiments/n7f1b1.qnt
index a710920e..f2da73f7 100644
--- a/spec/protocol-spec/experiments/n7f1b1.qnt
+++ b/spec/protocol-spec/experiments/n7f1b1.qnt
@@ -1,3 +1,5 @@
+// -*- mode: Bluespec; -*-
+//
 // A specification instance for n=6, f=1, and no Byzantine faults
 module n7f1b1 {
   import replica(
diff --git a/spec/protocol-spec/guided_replica.qnt b/spec/protocol-spec/guided_replica.qnt
index 0353e59c..d6558e64 100644
--- a/spec/protocol-spec/guided_replica.qnt
+++ b/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 {
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/main.qnt b/spec/protocol-spec/main.qnt
index e5f6cfa5..5eb2fad8 100644
--- a/spec/protocol-spec/main.qnt
+++ b/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"
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/state_monitor.qnt b/spec/protocol-spec/state_monitor.qnt
index 96428489..1efdd986 100644
--- a/spec/protocol-spec/state_monitor.qnt
+++ b/spec/protocol-spec/state_monitor.qnt
@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // A state monitor that allows us to compare new state against the old states.
 // For example, we compare phase transitions.
 // To do so, we save the old replica states in old_replica_state.
@@ -55,4 +56,4 @@ module state_monitor {
 
       i::CORRECT.forall(id => for_replica(id))
     }
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/twins_n6f1b1.qnt b/spec/protocol-spec/twins_n6f1b1.qnt
index 7346a948..30d3d504 100644
--- a/spec/protocol-spec/twins_n6f1b1.qnt
+++ b/spec/protocol-spec/twins_n6f1b1.qnt
@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // This is an explorative module applying the Twins approach 
 // to model byzantine behaviour with 1 faulty replicas and 5 correct replicas.
 module twins {
@@ -31,4 +32,4 @@ module twins {
 
 
   action step = i::correct_step
-}
\ No newline at end of file
+}
diff --git a/spec/protocol-spec/twins_n6f1b2.qnt b/spec/protocol-spec/twins_n6f1b2.qnt
index 46321eec..0596281a 100644
--- a/spec/protocol-spec/twins_n6f1b2.qnt
+++ b/spec/protocol-spec/twins_n6f1b2.qnt
@@ -1,3 +1,4 @@
+// -*- mode: Bluespec; -*-
 // This is an explorative module applying the Twins approach 
 // to model byzantine behaviour with 2 faulty replicas and 4 correct replicas.
 module twins {
@@ -31,4 +32,4 @@ module twins {
 
 
   action step = i::correct_step
-}
\ No newline at end of file
+}

From 445e273d6c69687c479be077f0506f076f3d7e08 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Tue, 30 Jul 2024 13:58:21 +0300
Subject: [PATCH 13/15] pin the version of quint

---
 .github/workflows/spec.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/spec.yaml b/.github/workflows/spec.yaml
index 469eb169..ebfe41ac 100644
--- a/.github/workflows/spec.yaml
+++ b/.github/workflows/spec.yaml
@@ -20,7 +20,7 @@ jobs:
           check-latest: true
 
       - name: Install quint
-        run: npm i @informalsystems/quint -g
+        run: npm i @informalsystems/quint@0.20.0 -g
 
       - name: Run test
         run: cd spec && make test

From 4fbda61daac42b1b85e306205b6d5cecc27a685b Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Tue, 30 Jul 2024 14:01:28 +0300
Subject: [PATCH 14/15] downgrade node to v20

---
 .github/workflows/spec.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/spec.yaml b/.github/workflows/spec.yaml
index ebfe41ac..050a7642 100644
--- a/.github/workflows/spec.yaml
+++ b/.github/workflows/spec.yaml
@@ -16,7 +16,7 @@ jobs:
       - name: Install node
         uses: actions/setup-node@v4
         with:
-          node-version: ">= 18"
+          node-version: 20
           check-latest: true
 
       - name: Install quint

From 519183012a5ab293187de653184f8fe117d685e2 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Tue, 30 Jul 2024 14:06:08 +0300
Subject: [PATCH 15/15] try quint 0.21.0 with node 20

---
 .github/workflows/spec.yaml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/spec.yaml b/.github/workflows/spec.yaml
index 050a7642..6c1971fb 100644
--- a/.github/workflows/spec.yaml
+++ b/.github/workflows/spec.yaml
@@ -20,7 +20,7 @@ jobs:
           check-latest: true
 
       - name: Install quint
-        run: npm i @informalsystems/quint@0.20.0 -g
+        run: npm i @informalsystems/quint@0.21.0 -g
 
       - name: Run test
         run: cd spec && make test