feat(raft-log-replication): init leader progress on becoming leader (task 2.2)

next_index[j]=log_len+1, match_index[j]=0 for every peer at both win paths
(single-node RAFT_ELECTED_IMMEDIATELY in raft_start_election; multi-node
RAFT_BECAME_LEADER in raft_on_vote_reply) via shared raft_init_leader_progress
helper (raft.tla BecomeLeader, Req 3.1). Suite green under ASAN.
This commit is contained in:
Rongsong Shen 2026-06-21 15:40:26 +00:00
parent d70f2507c3
commit 6ea89569fa
3 changed files with 87 additions and 1 deletions

View file

@ -39,7 +39,7 @@
- _Boundary: raft.c, test_raft.c_
- _Depends: 1.3_
- [ ] 2.2 RED+GREEN: leader progress initialized on becoming leader
- [x] 2.2 RED+GREEN: leader progress initialized on becoming leader
- Test: after a node becomes leader, `next_index[j] == log_len + 1` and `match_index[j] == 0` for every peer (raft.tla BecomeLeader)
- Implement the `next_index`/`match_index` initialization on the win path (`raft_start_election` single-node + the multi-node become-leader transition)
- Observable completion: assertion on `next_index`/`match_index` after election passes; no regression in election tests