refactor: use create_justification in the quint specification as in the informal spec

spec/informal-spec/replica.rs

@@ -245,7 +245,7 @@ impl ReplicaState {
         self.phase = Phase::Prepare;
 
         // Send a new view message to the other replicas, for synchronization.
-        let new_view = NewView::new(self.get_justification(view));
+        let new_view = NewView::new(self.create_justification());
 
         self.send(new_view);
     }
@@ -260,4 +260,4 @@ impl ReplicaState {
             Justification::Timeout(self.high_timeout_qc.unwrap())
         }
     }
-}
+}

spec/informal-spec/types.rs

@@ -72,7 +72,7 @@ impl Justification {
         match self {
             Commit(qc) => {
                 // The previous proposal was finalized, so we can propose a new block.
-                (qc.block_number + 1, None)
+                (qc.vote.block_number + 1, None)
             }
             Timeout(qc) => {
                 // Get the high vote of the timeout QC, if it exists. We check if there are
@@ -88,7 +88,7 @@ impl Justification {
                 let high_qc: Option<CommitQC> = qc.high_commit_qc;
 
                 if high_vote.is_some()
-                    && (high_qc.is_none() || high_vote.block_number > high_qc.block_number)
+                    && (high_qc.is_none() || high_vote.block_number > high_qc.vote.block_number)
                 {
                     // There was some proposal last view that might have been finalized.
                     // We need to repropose it.
@@ -98,7 +98,7 @@ impl Justification {
                     // that it couldn't have been finalized. Either way, we can propose
                     // a new block.
                     let block_number = match high_qc {
-                        Some(qc) => qc.block_number + 1,
+                        Some(qc) => qc.vote.block_number + 1,
                         None => 0,
                     };
 

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
+            }
+        }
+    })
 }