From 7cb07bb51957833848674ed904c9ebcee0c11cc4 Mon Sep 17 00:00:00 2001
From: Heidi Howard <1835251+heidihoward@users.noreply.github.com>
Date: Mon, 8 Jan 2024 15:25:31 +0000
Subject: [PATCH] `NextIndex` is not updated on successful AE response (#5895)

---
 tla/consensus/MCccfraft.cfg             |  1 -
 tla/consensus/MCccfraftWithReconfig.cfg |  1 -
 tla/consensus/SIMccfraft.cfg            |  2 --
 tla/consensus/ccfraft.tla               | 11 +++++++++--
 4 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/tla/consensus/MCccfraft.cfg b/tla/consensus/MCccfraft.cfg
index c6912cdd79c9..ba40fc88c7be 100644
--- a/tla/consensus/MCccfraft.cfg
+++ b/tla/consensus/MCccfraft.cfg
@@ -77,6 +77,5 @@ INVARIANTS
     MonoLogInv
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
-    MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
diff --git a/tla/consensus/MCccfraftWithReconfig.cfg b/tla/consensus/MCccfraftWithReconfig.cfg
index 572632045965..54e38a3af00d 100644
--- a/tla/consensus/MCccfraftWithReconfig.cfg
+++ b/tla/consensus/MCccfraftWithReconfig.cfg
@@ -77,6 +77,5 @@ INVARIANTS
     MonoLogInv
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
-    MatchIndexLowerBoundNextIndexInv
     CommitCommittableIndices
     CommittableIndicesAreKnownSignaturesInv
diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
index c778561b2650..4a85864280f4 100644
--- a/tla/consensus/SIMccfraft.cfg
+++ b/tla/consensus/SIMccfraft.cfg
@@ -77,8 +77,6 @@ INVARIANTS
     NoLeaderBeforeInitialTerm
     LogConfigurationConsistentInv
 
-    MatchIndexLowerBoundNextIndexInv
-
     CommitCommittableIndices
 
     CommittableIndicesAreKnownSignaturesInv
diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
index 566cca9efe25..a69382e809f2 100644
--- a/tla/consensus/ccfraft.tla
+++ b/tla/consensus/ccfraft.tla
@@ -273,7 +273,10 @@ CandidateVarsTypeInv ==
     /\ VotesGrantedTypeInv
 
 \* The following variables are used only on leaders:
-\* The next entry to send to each follower.
+
+\* The next entry to send to each follower, called sent_idx in raft.h
+\* In CCF, the leader updates nextIndex optimically when an AE message is dispatched
+\* In contrast, in Raft the leader only updates nextIndex when an AE response is received
 VARIABLE nextIndex
 
 \* nextIndex cannot be zero as its the index of the first log
@@ -921,7 +924,8 @@ HandleAppendEntriesResponse(i, j, m) ==
           /\ m.success \* successful
           \* max(...) because why would we ever want to go backwards on a success response?!
           /\ matchIndex' = [matchIndex EXCEPT ![i][j] = max(@, m.lastLogIndex)]
-          /\ nextIndex'  = [nextIndex  EXCEPT ![i][j] = max(@, m.lastLogIndex + 1)]
+          \* nextIndex is unchanged on successful AE response as it was already updated when the AE was dispatched
+          /\ UNCHANGED nextIndex
        \/ /\ \lnot m.success \* not successful
           /\ LET tm == FindHighestPossibleMatch(log[i], m.lastLogIndex, m.term)
              IN nextIndex' = [nextIndex EXCEPT ![i][j] = max(min(tm, nextIndex[i][j]-1), matchIndex[i][j]) + 1 ]
@@ -1243,6 +1247,9 @@ NoLeaderBeforeInitialTerm ==
     \A i \in Servers :
         currentTerm[i] < StartTerm => state[i] # Leader
 
+\* MatchIndexLowerBoundNextIndexInv is not currently an invariant but 
+\* we might wish to add it in the future. This could be achieved by updating 
+\* nextIndex to max of current nextIndex and matchIndex when an AE ACK is received.
 MatchIndexLowerBoundNextIndexInv ==
     \A i,j \in Servers :
         state[i] = Leader =>