WIP: Fast path

Signed-off-by: Markus Alexander Kuppe <[email protected]>

pirateship.tla

@@ -301,6 +301,10 @@ CheckViewStability(p) ==
         \A q \in Q: 
             prepareQC'[p][q] >= SelectInSeq(log[p], inView)
 
+HighestUnanimity(l, v) ==
+    LET idx == SelectLastInSeq(l, LAMBDA e: e.byzQCVotes = R /\ e.view = v)
+    IN IF idx = 0 THEN {0} ELSE l[idx].byzQC
+
 \* Primary p receiving votes from replica r
 \* Compare: src/consensus/steady_state.rs#do_process_vote
 ReceiveVote(p, r) ==
@@ -323,9 +327,11 @@ ReceiveVote(p, r) ==
     /\ IF viewStable'[p] THEN 
             /\ crashCommitIndex' = [crashCommitIndex EXCEPT ![p] = 
                 MaxQuorum(CQ, log[p], prepareQC'[p], @)]
-            \* Compare: ssrc/consensus/commit.rs#maybe_byzantine_commit
-            /\ byzCommitIndex' = [byzCommitIndex EXCEPT ![p] = 
-                HighestByzQC(SubSeq(log[p],1,MaxQuorum(BQ, log[p], prepareQC'[p], 0)))]
+            \* Compare: src/consensus/commit.rs#maybe_byzantine_commit
+            /\ LET bci == HighestByzQC(SubSeq(log[p], 1, MaxQuorum(BQ, log[p], prepareQC'[p], 0)))
+                    \* Compare: src/consensus/commit.rs#maybe_byzantine_commit_by_fast_path
+                    bciFastPath == HighestUnanimity(log[p], view[p])
+               IN byzCommitIndex' = [byzCommitIndex EXCEPT ![p] = Max(bciFastPath \cup {bci}) ]
         ELSE UNCHANGED <<crashCommitIndex, byzCommitIndex>>
     /\ UNCHANGED <<view, log, primary, byzActions>>