From aafa601a2930685bfdbe89c11c2dd922871f980c Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@konnov.phd>
Date: Wed, 27 Nov 2024 14:17:11 +0100
Subject: [PATCH] use create_justification, as in the informal spec

---
 spec/protocol-spec/replica.qnt | 48 +++++++++++++++++++++++++++++-----
 1 file changed, 42 insertions(+), 6 deletions(-)

diff --git a/spec/protocol-spec/replica.qnt b/spec/protocol-spec/replica.qnt
index f89ac1fd..ea44d11c 100644
--- a/spec/protocol-spec/replica.qnt
+++ b/spec/protocol-spec/replica.qnt
@@ -601,7 +601,7 @@ module replica {
 
                     | Some(qc) => {
                         val self1 = self.process_commit_qc(Some(qc))
-                        start_new_view(id, self1, signed_vote.vote.view + 1, Commit(qc))
+                        start_new_view(id, self1, signed_vote.vote.view + 1)
                     }
                 },
 
@@ -678,7 +678,7 @@ module replica {
                             ...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)),
+                        start_new_view(id, self1, signed_vote.vote.view + 1),
                     }
                 },
                 // unchanged variables
@@ -711,7 +711,7 @@ module replica {
                 }
 
             if (new_view_view > self.view) {
-                start_new_view(id, self1, new_view_view, new_view.justification)
+                start_new_view(id, self1, new_view_view)
             } else {
                 all {
                     replica_state' = replica_state,
@@ -731,7 +731,8 @@ module replica {
     // A step by the proposer for replica_id.
     // We pass new_block, which is used a substitute for: self.create_proposal(block_number).
     action proposer_step(replica_id: ReplicaId, new_block: Block): bool = all {
-        val replica_state_view = replica_state.get(replica_id).view
+        val replica = replica_state.get(replica_id)
+        val replica_state_view = replica.view
         val proposer_state_view = proposer_view.get(replica_id)
         all {
             // Check if we are in a new view and we are the leader.
@@ -745,7 +746,7 @@ module replica {
             // Get the justification for this view. If we have both a commit QC
             // and a timeout QC for this view (highly unlikely), we should prefer
             // to use the commit QC.
-            val justification = ghost_justifications.get((replica_id, replica_state_view))
+            val justification = replica.create_justification()
             // Get the block number and check if this must be a reproposal.
             val block_and_hash = justification.get_implied_block()
             val block_number = block_and_hash._1
@@ -798,8 +799,9 @@ module replica {
     }
 
     // a correct replica changes to a new view
-    action start_new_view(id: ReplicaId, self: ReplicaState, view: ViewNumber, justification: Justification): bool = {
+    action start_new_view(id: ReplicaId, self: ReplicaState, view: ViewNumber): bool = {
         // make sure that we do not go out of bounds with the new view
+        val justification = self.create_justification()
         all {
             VIEWS.contains(view),
             // switch to the Prepare phase
@@ -1016,6 +1018,26 @@ module replica {
         }
     }
 
+    def create_justification(self: ReplicaState): Justification = {
+        // We always have a timeout QC, at least, for the view 0.
+        // However, the type checker needs a well-typed value. Hence, use empty_tqc.
+        val empty_tqc: TimeoutQC = {
+            votes: Map(), agg_sig: Set(), high_commit_qc: None, ghost_view: 0
+        }
+        val high_tqc = self.high_timeout_qc.unwrap_or(empty_tqc)
+        match (self.high_commit_qc) {
+        | None =>
+            Timeout(high_tqc)
+
+        | Some(cqc) =>
+            if (cqc.vote.view >= high_tqc.ghost_view) {
+                Commit(cqc)
+            } else {
+                Timeout(high_tqc)
+            }
+        }
+    }    
+
     def justification_verify(justification: Justification): bool = {
         match (justification) {
             | Timeout(qc) =>
@@ -1675,4 +1697,18 @@ module replica {
     val views_over_2_example = CORRECT.forall(id => {
         replica_state.get(id).view <= 2
     })
+
+    // check this falsy invariant to see an example of a replica having
+    // both a high commit QC and a timeout QC for the same view
+    val high_commit_and_timeout_qc_example = CORRECT.forall(id => {
+        val self = replica_state.get(id)
+        match (self.high_commit_qc) {
+        | None => true
+        | Some(cqc) =>
+            match (self.high_timeout_qc) {
+            | None => true
+            | Some(tqc) => cqc.vote.view != tqc.ghost_view
+            }
+        }
+    })
 }
\ No newline at end of file