Refactored TimeoutQC to contain just one CommitQC (#144)

## What ❔

Refactored (in the informal spec) `TimeoutQC`, `SignedTimeoutVote` and
`TimeoutVote` so that `TimeoutQC` contains only one `CommitQC` (the high
QC).

## Why ❔

It reduces the state space which should help with model checking.

---------

Co-authored-by: Igor Konnov <[email protected]>

spec/informal-spec/replica.rs

@@ -165,7 +165,7 @@ fn on_proposal(self, proposal: Proposal) {
     match proposal.justification {
         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);
             self.high_timeout_qc = max(Some(qc), self.high_timeout_qc);
         }
     };
@@ -177,7 +177,7 @@ fn on_proposal(self, proposal: Proposal) {
 // Processed an (already verified) commit_qc received from the network
 // as part of some message. It bumps the local high_commit_qc and if
 // we have the proposal corresponding to this qc, we append it to the committed_blocks.
-fn process_commit_qc(self, qc_opt: Option[CommitQC]) {
+fn process_commit_qc(self, qc_opt: Option<CommitQC>) {
     if let Some(qc) = qc_opt {
         self.high_commit_qc = max(Some(qc), self.high_commit_qc);
         let Some(block) = self.cached_proposals.get((qc.vote.block_number,qc.vote.block_hash)) else { return };
@@ -218,7 +218,7 @@ fn on_timeout(self, sig_vote: SignedTimeoutVote) {
 
     // Check if we now have a timeout QC for this view.
     if let Some(qc) = self.get_timeout_qc(sig_vote.view()) {
-        self.process_commit_qc(qc.high_qc());
+        self.process_commit_qc(qc.high_commit_qc);
         self.high_timeout_qc = max(Some(qc), self.high_timeout_qc);
         self.start_new_view(sig_vote.view() + 1);
     }
@@ -235,7 +235,7 @@ fn on_new_view(self, new_view: NewView) {
     match new_view.justification {
         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);
             self.high_timeout_qc = max(Some(qc), self.high_timeout_qc);
         }
     };

spec/informal-spec/types.rs

@@ -77,7 +77,7 @@ impl Justification {
 
                 // 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.
-                let high_qc: Option<CommitQC> = qc.high_qc();
+                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)
@@ -154,16 +154,19 @@ struct TimeoutVote {
     view: ViewNumber,
     // The commit vote with the highest view that this replica has signed, if any.
     high_vote: Option<CommitVote>,
-    // The commit quorum certificate with the highest view that this replica
+    // The view number of the highest commit quorum certificate that this replica
     // has observed, if any.
-    high_commit_qc: Option<CommitQC>,
+    high_commit_qc_view: Option<ViewNumber>,
 }
 
 struct 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>,
 }
 
 impl SignedTimeoutVote {
@@ -172,9 +175,10 @@ impl SignedTimeoutVote {
     }
 
     fn verify(self) -> bool {
-        // Technically, only the signature needs to be verified. But if we wish, there are two invariants that are easy to check:
-        // self.view() >= self.high_vote.view() && self.high_vote.view() >= self.high_commit_qc.view()
-        self.verify_sig()
+        // If we wish, there are two invariants that are easy to check but aren't required for correctness:
+        // self.view() >= self.high_vote.view() && self.high_vote.view() >= self.high_commit_qc_view
+        self.vote.high_commit_qc_view == self.high_commit_qc.map(|x| x.view()) && self.verify_sig()
+          && self.high_commit_qc.map(|qc| qc.verify())
     }
 }
 
@@ -189,6 +193,9 @@ struct TimeoutQC {
     // 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>,
 }
 
 impl TimeoutQC {
@@ -197,27 +204,27 @@ impl TimeoutQC {
     }
 
     fn verify(self) -> bool {
-        // Check that all votes have the same view.
-        for (_, vote) in votes {
-            if vote.view != self.view() {
-                return false;
-            }
-        }
+        // Check that all votes have the same view and get the highest commit QC view of the timeout QC.
+        let high_qc_view = None;
 
-        // 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.
-        if let Some(high_qc) = self.high_qc() {
-            if !high_qc.verify() {
+        for (_, vote) in self.votes {
+            if vote.view != self.view() {
                 return false;
             }
+            high_qc_view = max(high_qc_view, vote.high_commit_qc_view);
         }
-
 
         // In here we need to not only check the signature, but also that
         // it has enough weight beyond it.
-        self.verify_agg_sig(QUORUM_WEIGHT)
+        if !self.verify_agg_sig(QUORUM_WEIGHT) {
+            return false;
+        }
+
+        // We check that the high commit QC view matches the high commit QC that we have, and we verify the QC.
+        match self.high_commit_qc {
+            Some(high_qc) => high_qc_view == Some(high_qc.view()) && high_qc.verify();
+            None => high_qc_view.is_none();
+        }
     }
 
     fn high_vote(self) -> Option<CommitVote> {
@@ -245,16 +252,6 @@ impl TimeoutQC {
             None
         }
     }
-
-    fn high_qc(self) -> Option<CommitQC> {
-        let high_qc = None;
-
-        for (_, vote) in votes {
-            high_qc = max(high_qc, vote.high_commit_qc);
-        }
-
-        high_qc
-    }
 }
 
 struct NewView {