TV for startup followed by join (#5839)

tests/raft_scenarios/startup_2nodes

@@ -0,0 +1,14 @@
+start_node,0
+assert_is_primary,0
+emit_signature,2
+
+assert_is_primary,0
+assert_commit_idx,0,2
+
+trust_node,2,1
+emit_signature,2
+
+dispatch_all
+# periodic_all,10
+# dispatch_all
+# assert_commit_idx,0,4

tla/consensus/Traceccfraft.tla

@@ -176,7 +176,8 @@ IsSendAppendEntries ==
                 /\ IsAppendEntriesRequest(msg, j, i, logline)
                 \* There is now one more message of this type.
                 /\ Network!OneMoreMessage(msg)
-          /\ logline.msg.sent_idx = sentIndex[i][j]
+\* TODO revisit once nextIndex-related changes are merged in the spec
+\*          /\ logline.msg.sent_idx = nextIndex[i][j]
           /\ logline.msg.match_idx = matchIndex[i][j]
     /\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.state.committable_indices)
 

tla/consensus/ccfraft.tla

@@ -645,6 +645,12 @@ ChangeConfigurationInt(i, newConfiguration) ==
     \* i.e., be re-added to a new configuration.  Instead, the node has to rejoin with a
     \* "fresh" identity (compare sec 6.2, page 8, https://arxiv.org/abs/2310.11559).
     /\ \A s \in newConfiguration: s \notin removedFromConfiguration
+    \* See raft.h:2401, nodes are only sent future entries initially, they will NACK if necessary.
+    \* This is because they are expected to start from a fairly recent snapshot, not from scratch.
+    /\ LET
+        addedNodes == newConfiguration \ CurrentConfiguration(i)
+        newSentIndex == [ k \in Servers |-> IF k \in addedNodes THEN Len(log[i]) ELSE sentIndex[i][k]]
+       IN sentIndex' = [sentIndex EXCEPT ![i] = newSentIndex]
     \* Keep track of running reconfigurations to limit state space
     /\ reconfigurationCount' = reconfigurationCount + 1
     /\ removedFromConfiguration' = removedFromConfiguration \cup (CurrentConfiguration(i) \ newConfiguration)
@@ -653,7 +659,7 @@ ChangeConfigurationInt(i, newConfiguration) ==
                                              configuration |-> newConfiguration,
                                              contentType |-> TypeReconfiguration])]
     /\ configurations' = [configurations EXCEPT ![i] = configurations[i] @@ Len(log'[i]) :> newConfiguration]
-    /\ UNCHANGED <<messageVars, serverVars, candidateVars, leaderVars, commitIndex, committableIndices>>
+    /\ UNCHANGED <<messageVars, serverVars, candidateVars, matchIndex, commitIndex, committableIndices>>
 
 ChangeConfiguration(i) ==
     \* Reconfigure to any *non-empty* subset of servers.  ChangeConfigurationInt checks that the new
@@ -940,7 +946,8 @@ HandleAppendEntriesResponse(i, j, m) ==
 UpdateTerm(i, j, m) ==
     /\ m.term > currentTerm[i]
     /\ currentTerm'    = [currentTerm EXCEPT ![i] = m.term]
-    /\ state'          = [state       EXCEPT ![i] = IF @ \in {Leader, Candidate} THEN Follower ELSE @]
+    \* See become_aware_of_new_term() in raft.h:1915
+    /\ state'          = [state       EXCEPT ![i] = IF @ \in {Leader, Candidate, None} THEN Follower ELSE @]
     /\ votedFor'       = [votedFor    EXCEPT ![i] = Nil]
     \* See rollback(last_committable_index()) in raft::become_follower
     /\ log'            = [log         EXCEPT ![i] = SubSeq(@, 1, LastCommittableIndex(i))]
@@ -1224,13 +1231,14 @@ MonoLogInv ==
 LogConfigurationConsistentInv ==
     \A i \in Servers :
         \/ state[i] = None
+        \* Follower, but no known configurations yet
+        \/ /\ state[i] = Follower
+           /\ Cardinality(DOMAIN configurations[i]) = 0
         \/
             \* Configurations should have associated reconfiguration txs in the log
             /\ \A idx \in DOMAIN (configurations[i]) : 
                 /\ log[i][idx].contentType = TypeReconfiguration            
                 /\ log[i][idx].configuration = configurations[i][idx]
-            \* Current configuration should be committed
-            /\ commitIndex[i] >= CurrentConfigurationIndex(i)
             \* Pending configurations should not be committed yet
             /\ Cardinality(DOMAIN configurations[i]) > 1 
                 => commitIndex[i] < NextConfigurationIndex(i)
@@ -1252,7 +1260,6 @@ NoLeaderBeforeInitialTerm ==
 \* 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.
 MatchIndexLowerBoundSentIndexInv ==
-
     \A i,j \in Servers :
         state[i] = Leader =>
             sentIndex[i][j] >= matchIndex[i][j]