myxce/.kiro/specs/raft-commit-safety
Rongsong Shen 62a927b419 test(raft-commit-safety): simulator invariant tests (tasks 7.1-7.4)
7.1 Figure-8 commit refusal (G4): prior-term entry at a genuine quorum HELD (only the
   current-term gate keeps commit_index at 0), then a current-term entry advances over
   both (indirect commit) with one fire. Closes the Req 6.3 two-phase coverage.
7.2 Leader Completeness: committed prefix on {0,1}; node 0 fails; the stale node 2 is
   DENIED by the freshness gate so only the up-to-date node 1 can win — and it holds the
   full committed prefix (term+bytes).
7.3 freshness lexicographic (vote + prevote): stale-term-higher-index DENIED,
   fresher-term-lower-index GRANTED, tie decided by index; prevote side-effect-free.
7.4 on_commit_advanced trigger: fire-count tracks STRICT advances — held(0)/advance(1)/
   no-op-redrive(1)/advance(2)/non-leader(2).

Test-only (sim_set_log_entry local helper); reviewed in-parent (transient API 529 on the
review subagent). ASAN green (243 tests).
2026-06-22 00:41:11 +00:00
..
brief.md checkpoint: bug-851 root cause + raft TLA+ conformance spec family 2026-06-21 14:02:15 +00:00
design.md checkpoint: bug-851 root cause + raft TLA+ conformance spec family 2026-06-21 14:02:15 +00:00
requirements.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-commit-safety): simulator invariant tests (tasks 7.1-7.4) 2026-06-22 00:41:11 +00:00