test(raft-sim-conformance): conformance Restart persistence test (task 4.3)

This commit is contained in:
Rongsong Shen 2026-06-24 14:05:19 +00:00
parent b5b7e01b92
commit 5f67be4fa3
2 changed files with 117 additions and 1 deletions

View file

@ -113,7 +113,7 @@
- _Boundary: raft_sim.c, test_raft.c_
- _Depends: 2.2, 3.5, 4.1_
- [ ] 4.3 RED+GREEN: Restart preserves persisted `term`/`votedFor`/log
- [x] 4.3 RED+GREEN: Restart preserves persisted `term`/`votedFor`/log
- Test: a Restart action re-inits a node while keeping `node.log[]`, recovered `log_len`, and last-persisted `(term, votedFor)`; volatile state resets per `raft.tla` `Restart`
- Implement the Restart branch (feed `initial_log_len` + restored `(term, votedFor)` into `raft_init`)
- Observable completion: a restarted node retains its log and term; no invariant violation results from the restart alone
@ -227,3 +227,11 @@
legitimate scenario surfaces it, report BLOCKED with the upstream cause rather than
working around it. Seed 3 is clean over 600 steps and is used only to prove the 4.2
scheduler mechanism reaches all action kinds.
- **UPDATE (post-4.2): bug-1095/1096 FIXED in raft.c** (commit `fix(raft): vote-reply
per-peer dedup + stale-term drop`). `raft_on_vote_reply` now tracks grants in a per-peer
`vote_replies[]` set (idempotent under DuplicateMessage) and drops stale-term replies
(DropStaleResponse), mirroring the existing pre-vote idiom; 47 raft / 264 lib tests pass.
The library is now correct, so downstream tasks (5.x scenarios, 6.1 M-seed sweep, 7.2
correct-direction) CAN and MUST assert zero invariant violations on the correct build.
The user authorized this cross-boundary fix. The deliberately-broken-build fault switch
(task 7) remains the way to deliberately re-introduce a divergence for the negative test.