ccfraft!AdvanceCommitIndex advance to the smalles possible index, whe…

…reas raft.h advances to the largest possible one.

Originally found in #5798.

tla/consensus/ccfraft.tla

@@ -678,24 +678,34 @@ AdvanceCommitIndex(i) ==
                         required_quorum == Quorums[config_servers]
                         agree_servers == {k \in config_servers : matchIndex[i][k] >= idx}
                     IN (IF i \in config_servers THEN {i} ELSE {}) \cup agree_servers \in required_quorum
-            \* We want to get the smallest such index forward that is a signature
-            \* This index must be from the current term, 
-            \* as explained by Figure 8 and Section 5.4.2 of https://raft.github.io/raft.pdf
-            \* See find_highest_possible_committable_index in raft.h
-            new_index == SelectInSubSeq(log[i], commitIndex[i]+1, Len(log[i]),
-                LAMBDA e : e.contentType = TypeSignature /\ e.term = currentTerm[i])
+            \* The function find_highest_possible_committable_index in raft.h returns the largest committable index
+            \* in the current term (Figure 8 and Section 5.4.2 of https://raft.github.io/raft.pdf explains why it has
+            \* to be the *current* term).  Finding the largest index is an (mplementation-level) optimization that
+            \* reduces the number of AdvanceCommitIndex calls, but this optimization also shrinks this spec's state-space.
+            \*
+            \* Theoretically, any committable index in the current term works, i.e., highestCommittableIndex could be
+            \* defined non-deterministically as:
+            \*       \E idx \in { j \in (commitIndex[i]+1)..Len(log[i]) : /\ log[i][j].term = currentTerm[i] 
+            \*                                                            /\ log[i][j].contentType = TypeSignature }
+            \*          /\ HasConsensusWatermark(idx)
+            \*          /\ ...
+            \* 
+            \* Max({0} \cup {...}) to default to 0 if no committable index is found.
+            highestCommittableIndex == Max({0} \cup { j \in (commitIndex[i]+1)..Len(log[i]) : 
+                                                                    /\ log[i][j].term = currentTerm[i] 
+                                                                    /\ log[i][j].contentType = TypeSignature
+                                                                    /\ HasConsensusWatermark(j) })
         IN
-        /\ HasConsensusWatermark(new_index)
-         \* only advance if necessary (this is basically a sanity check after the Min above)
-        /\ commitIndex[i] < new_index
-        /\ commitIndex' = [commitIndex EXCEPT ![i] = new_index]
+         \* only advance if necessary (this is basically a sanity)
+        /\ commitIndex[i] < highestCommittableIndex
+        /\ commitIndex' = [commitIndex EXCEPT ![i] = highestCommittableIndex]
         /\ committableIndices' = [ committableIndices EXCEPT ![i] = @ \ 0..commitIndex'[i] ]
         \* If commit index surpasses the next configuration, pop configs, and retire as leader if removed
         /\ IF /\ Cardinality(DOMAIN configurations[i]) > 1
-              /\ new_index >= NextConfigurationIndex(i)
+              /\ highestCommittableIndex >= NextConfigurationIndex(i)
            THEN
               LET new_configurations == RestrictDomain(configurations[i], 
-                                            LAMBDA c : c >= LastConfigurationToIndex(i, new_index))
+                                            LAMBDA c : c >= LastConfigurationToIndex(i, highestCommittableIndex))
               IN
               /\ configurations' = [configurations EXCEPT ![i] = new_configurations]
               \* Retire if i is not in active configuration anymore