myxce/.kiro/specs/raft-log-replication
Rongsong Shen 9c1a034aa8 test(raft-log-replication): simulator invariant tests (tasks 9.1-9.4)
9.1 replication + partition catch-up: 3-entry quorum replication then Log Matching;
   isolate a follower, heal, assert next_index walks back, catch-up, Log Matching.
9.2 divergent-suffix truncation (G3): follower with a same-index/different-term tail
   converges via conflict-truncate; byte-for-byte prefix equality + Log Matching.
9.3 drop/dup/reorder convergence: dropped AE recovered; duplicate already-have AE is
   a no-op; genuine out-of-order delivery (entry-3 AE before entry-2) rejected via the
   logOk gap with no phantom gap; converges + Log Matching (Req 8.3).
9.4 chaotic-churn G5/bug-851 regression: stale-term node rejoins under a higher-term
   leader, adopts the term via the AE/heartbeat UpdateTerm path (load-bearing: would
   fail as stale-reject if UpdateTerm-on-AE regressed), voted_for cleared, no second
   leader, and a post-converge election campaigns strictly above the old term (cannot
   reuse). Log Matching holds throughout.

Review-applied: genuine reorder in 9.3; active re-election + voted_for assertions in
9.4. ASAN green (219 tests).
2026-06-21 17:06:05 +00:00
..
brief.md checkpoint: bug-851 root cause + raft TLA+ conformance spec family 2026-06-21 14:02:15 +00:00
design.md feat(raft-log-replication): header contract — log model, callbacks, entry points (tasks 1.1-1.3) 2026-06-21 14:15:15 +00:00
requirements.md checkpoint: bug-851 root cause + raft TLA+ conformance spec family 2026-06-21 14:02:15 +00:00
research.md checkpoint: bug-851 root cause + raft TLA+ conformance spec family 2026-06-21 14:02:15 +00:00
spec.json checkpoint: bug-851 root cause + raft TLA+ conformance spec family 2026-06-21 14:02:15 +00:00
tasks.md test(raft-log-replication): simulator invariant tests (tasks 9.1-9.4) 2026-06-21 17:06:05 +00:00