# Implementation Plan

> **TDD-mandatory** (`testing.md`): every checker, scheduler action, and scenario lands as
> a RED test in `src/lib/testsuite/test_raft.c` (with the `raft_sim.c` backing) that fails
> before the harness logic exists and passes after. Build/run library tests via
> `/xce-build lib`. All harness code is `XCE_TESTING`-gated.
>
> **Spec boundary** (applies to ALL tasks): this spec owns `src/lib/raft/raft_sim.c`, the
> `XCE_TESTING` sim section of `src/lib/raft/raft.h`, and the conformance tests in
> `src/lib/testsuite/test_raft.c` ONLY. It does **NOT** modify the protocol
> implementation: no task changes `raft.c` protocol logic or any protocol declaration in
> `raft.h`, and no task edits a controller file. The harness drives the published library
> entry points and consumes the `raft-log-replication` + `raft-commit-safety` callback
> contract **verbatim**.
>
> **Depends** (whole spec): `raft-log-replication` (log model + AppendEntries entry points
> + the four callbacks), `raft-commit-safety` (`raft_advance_commit`, `on_commit_advanced`,
> `(lastLogTerm, lastLogIndex)` freshness). If those signatures change, re-validate per the
> design's Revalidation Triggers.

## 1. Harness types and in-memory adapter backing

- [x] 1.1 Extend the `XCE_TESTING` sim section of `raft.h` with the harness data types
  - Add `raft_sim_msg_kind_t`, `raft_sim_msg_t` (vote/AE req+rsp union fields), `raft_sim_log_entry_t {term, value}`, `raft_sim_action_t {kind, actor, msg_index, term, index}`, and the `RAFT_SIM_MAX_LOG/MSGS/STEPS` bounds
  - Extend `raft_sim_node_t` with `log[]`, `log_len`, `commit_index`, `applied[]`, and a persisted-`(term, votedFor)` shadow for Restart; extend `raft_sim_cluster_t` with `bag[]`+`bag_count`, PRNG state, `seed`, and `trace[]`+`trace_len`
  - Observable completion: `raft.h` compiles under `XCE_TESTING`; no protocol declaration changed; `sizeof(raft_sim_cluster_t)` grows by the new fixed arrays
  - _Requirements: 1.1, 1.3, 2.5_
  - _Boundary: raft.h (XCE_TESTING section only)_

- [x] 1.2 Implement the seeded PRNG and the in-memory adapter callbacks
  - Add a small inlined deterministic generator (e.g. SplitMix64) seeded by `cluster.seed`; add `on_persist_entry` → `node.log[]`, `on_get_entry_term` → term|0, `on_truncate_from` → shrink `log_len`, `on_commit_advanced` → set `commit_index` + apply into `applied[]`; route `on_send_vote_request`/`on_send_append_entries` to a bag push
  - Add `raft_sim_conformance_init(c, n, timeout, seed)` wiring all six callbacks + the bag
  - Observable completion: a test initializes a cluster, drives one `raft_log_append` on a forced leader, and reads the entry back via the in-memory log and `on_get_entry_term`
  - _Requirements: 1.1, 1.2, 2.1_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 1.1_

## 2. Message bag (mirrors raft.tla `messages`)

- [x] 2.1 RED+GREEN: bag push/deliver routes vote and AppendEntries RPCs through the library handlers
  - Test: pushing a vote-req and an AE-req then delivering them invokes `raft_on_vote_request` / `raft_on_append_entries_request`, and the handler reply is pushed back as a `*_RSP` message
  - Implement `raft_sim_bag_push` and `raft_sim_bag_deliver(i)` (route by `kind`, honor `node.partition`, push replies)
  - Observable completion: delivered requests produce matching responses in the bag; partitioned endpoints are not delivered
  - _Requirements: 2.2, 2.4_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 1.2_

- [x] 2.2 RED+GREEN: Drop / Duplicate / Reorder mutate only the bag
  - Test: `raft_sim_bag_drop`/`_duplicate` change bag multiplicity without mutating any node's term/role/log; reorder delivers in a PRNG-chosen order
  - Implement the three bag operations (mirroring `raft.tla:443`/`448` `UNCHANGED` of non-message vars)
  - Observable completion: node snapshots are identical before/after a drop or duplicate of an undelivered message
  - _Requirements: 2.5_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 2.1_

## 3. The four invariant checkers (TDD against hand-built clusters)

- [x] 3.1 RED+GREEN: Election Safety checker (P)
  - Test: a cluster with two `LEADER` nodes at the same term fails; a single-leader-per-term cluster passes
  - Implement `raft_sim_check_election_safety` over roles+terms read from `raft_snapshot`
  - Observable completion: both directions assert correctly
  - _Requirements: 3.1, 3.6_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 1.1_

- [x] 3.2 RED+GREEN: Log Matching checker (P)
  - Test: two logs sharing `(idx, term)` but differing earlier fail; identical-prefix logs pass
  - Implement `raft_sim_check_log_matching` (pairwise; shared `(idx, term)` ⇒ identical `1..idx`)
  - Observable completion: both directions assert correctly
  - _Requirements: 3.2, 3.6_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 1.1_

- [x] 3.3 RED+GREEN: Leader Completeness checker (P)
  - Test: a committed `(index, term)` absent from a higher-term leader's log fails; present passes
  - Implement `raft_sim_check_leader_completeness` using `commit_index` + per-node logs, tracking the highest-term leader to date
  - Observable completion: both directions assert correctly
  - _Requirements: 3.3, 3.6_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 1.1_

- [x] 3.4 RED+GREEN: State Machine Safety checker (P)
  - Test: divergent `applied[k]` across two nodes fails; identical applied prefixes pass
  - Implement `raft_sim_check_state_machine_safety` over `applied[]`
  - Observable completion: both directions assert correctly
  - _Requirements: 3.4, 3.6_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 1.1_

- [x] 3.5 RED+GREEN: `raft_sim_check_all` returns the first failing invariant and halts
  - Test: a cluster violating two invariants reports the first; a clean cluster returns OK
  - Implement `raft_sim_check_all` composing 3.1–3.4 in a fixed order
  - Observable completion: first-failure semantics verified
  - _Requirements: 3.5_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 3.1, 3.2, 3.3, 3.4_

## 4. Action scheduler and trace recorder

- [x] 4.1 RED+GREEN: trace recorder records every action before it is applied
  - Test: after a fixed step sequence, `cluster.trace[]` holds the actions in order; `raft_sim_dump_trace` prints seed, n, and the ordered actions
  - Implement `raft_sim_action_t` recording (R1.4) + `raft_sim_dump_trace` (R5.1, R5.2); quiet on success unless `RAFT_SIM_VERBOSE` (R5.4)
  - Observable completion: a recorded trace round-trips to a readable dump
  - _Requirements: 1.4, 5.1, 5.2, 5.4_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 1.1_

- [x] 4.2 RED+GREEN: `raft_sim_step` drives one Next-equivalent action through the library and checks invariants
  - Test: stepping reaches each enabled action kind over a run; every step calls `raft_sim_check_all`; a forced violation halts with a trace dump and a `<0` return
  - Implement the seeded scheduler dispatch (Restart, Timeout, RequestVote/BecomeLeader via vote delivery, ClientRequest, AppendEntries via `raft_send_append_entries`, AdvanceCommitIndex via `raft_advance_commit`, Receive via bag deliver, Duplicate/Drop) selecting only **enabled** actions, driving **only** library entry points
  - Observable completion: a multi-step run touches log append, AE replication, commit advance, and message faults; invariants checked each step
  - _Requirements: 2.1, 2.2, 2.3, 2.4, 2.6, 3.5_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 2.2, 3.5, 4.1_

- [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
  - _Requirements: 2.1_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 4.2_

- [x] 4.4 RED+GREEN: deterministic replay from `(n, seed, max_steps)`
  - Test: two runs with the same `(n, seed, max_steps)` reach identical final per-node + bag state and an identical recorded trace
  - Implement `raft_sim_run(c, max_steps)` and confirm no wall-clock/address/uninitialized input leaks into choices
  - Observable completion: byte-identical replay verified across two runs
  - _Requirements: 1.5, 1.6, 5.3_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 4.2_

## 5. Targeted adversarial scenarios

- [x] 5.1 Partition/heal scenario (P)
  - Implement `raft_sim_scenario_partition_heal`: isolate a minority during appends, heal, drain the bag; assert all four invariants throughout and after convergence
  - Observable completion: scenario passes with zero violations on the correct build
  - _Requirements: 4.1_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 4.2_

- [x] 5.2 Restart-churn scenario (P)
  - Implement `raft_sim_scenario_restart_churn`: restart nodes mid-replication preserving persisted state; assert re-convergence with no violation
  - Observable completion: scenario passes; restarted nodes converge to the leader's prefix
  - _Requirements: 4.2_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 4.3_

- [x] 5.3 Drop/duplicate/reorder scenario (P)
  - Implement `raft_sim_scenario_drop_dup_reorder`: perturb bag delivery order + multiplicity; assert idempotent convergence with all four invariants held
  - Observable completion: scenario passes; duplicated AE is a no-op (already-have branch)
  - _Requirements: 4.3_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 4.2_

- [x] 5.4 Figure-8 scenario
  - Implement `raft_sim_scenario_figure8`: a previous-term entry on a quorum, a leader change; assert the entry is NOT reported committed until a current-term entry commits (Leader Completeness / State Machine Safety preserved)
  - Observable completion: the previous-term entry's `commit_index` does not cover it until a current-term commit
  - _Requirements: 4.4_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 4.2_

- [x] 5.5 Stale-rejoin scenario (bug-851 G5)
  - Implement `raft_sim_scenario_stale_rejoin`: a term-lagging node rejoins under a higher-term leader; assert it adopts the higher term from the AE/heartbeat path and does not re-elect at a reused term (Election Safety preserved)
  - Observable completion: the rejoining node's term advances via AE; no duplicate-term leader appears
  - _Requirements: 4.5_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 4.2_

## 6. CI batch and randomized seed sweep

- [x] 6.1 RED+GREEN: randomized M-seed sweep with zero violations
  - Test: run `raft_sim_run` for a fixed `max_steps` across M seeds (M ≥ configured minimum) plus all targeted scenarios; fail if any seed/scenario violates any invariant
  - Implement the sweep harness in `test_raft.c`; bound `max_steps`, M, and array sizes so the target fits the library test-suite budget
  - Observable completion: the full batch runs clean and within budget
  - _Requirements: 6.1, 6.2, 6.4_
  - _Boundary: test_raft.c_
  - _Depends: 5.1, 5.2, 5.3, 5.4, 5.5_

- [x] 6.2 Verify the conformance batch is ASAN/UBSAN-clean
  - Run the conformance batch under the library test sanitizer build; fix any leak/overflow/UB in the harness (fixed-size arrays, no allocation)
  - Observable completion: `/xce-build lib` sanitizer run reports no memory errors, leaks, or UB for the conformance target
  - _Requirements: 6.3_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 6.1_

## 7. Deliberately-broken-build negative test (the oracle's teeth)

- [x] 7.1 RED+GREEN: compile-time fault switch emulates the bug-851 defects in the adapter
  - Implement `RAFT_SIM_BREAK_TERM_STAMP` (adapter `on_persist_entry` writes term 0) and `RAFT_SIM_BREAK_TRUNCATE` (adapter `on_truncate_from` no-op), confined to the test/harness build configuration; default off
  - Observable completion: with a macro off, scenarios are clean; the macro is not set in the default CI run and does not touch `raft.c`
  - _Requirements: 7.1, 7.3_
  - _Boundary: raft_sim.c_
  - _Depends: 5.4, 5.5_

- [x] 7.2 RED+GREEN: negative test asserts both directions
  - Test: under the broken configuration the Figure-8 / divergent-suffix scenario triggers a Log Matching / Leader Completeness / State Machine Safety violation (with trace dump); under the correct configuration the same scenario passes — both asserted in one test
  - Observable completion: the broken build is caught and the correct build passes, proving checker sensitivity
  - _Requirements: 7.1, 7.2, 7.4_
  - _Boundary: test_raft.c_
  - _Depends: 7.1_

## 8. Optional TLC-consumable trace export

- [x]* 8.1 TLC-consumable trace export (deferred; off by default)
  - Implement `raft_sim_export_trace` gated by `RAFT_SIM_EXPORT`: per step, emit the action + tracked `raft.tla` variables (`messages` summary, per-node `currentTerm`/`state`/`log`/`commitIndex`) named per `raft/raft.tla`, in a stable line-oriented format; off by default
  - Observable completion: with `RAFT_SIM_EXPORT` set, a run emits a stable, spec-named record stream; default runs emit nothing extra
  - _Requirements: 8.1, 8.2, 8.3_
  - _Boundary: raft_sim.c, test_raft.c_
  - _Depends: 4.2_
```

## Implementation Notes

- **Task 4.2 — UPSTREAM raft.c BUG SURFACED (bug-1095/1096, bug-851 family).** While building
  the scheduler, the conformance oracle detected a real split-brain defect in `raft.c`
  `raft_on_vote_reply`: (1) vote grants are tallied with a plain counter that ignores
  `from_idx`, so a legitimate `DuplicateMessage` of a vote-response double-counts toward
  quorum; (2) there is no stale-term (`mterm < currentTerm`) reply drop. In `raft.tla`
  `votesGranted` is a SET (idempotent under the legal Duplicate action) and
  `DropStaleResponse` discards stale replies — so a correct implementation must tolerate
  both. Result: two leaders at the same term (Election Safety violation) on some seeds.
  This is OUT OF THIS SPEC'S BOUNDARY (raft.c protocol logic, owned by raft-core /
  ha-term-safety). The harness must NOT mask it (R2.6). **Consequence for downstream
  tasks:** any task asserting "zero invariant violations on the correct build" (5.x targeted
  scenarios, 6.1 M-seed sweep, 7.2 correct-direction) may surface this defect. Implementers
  of those tasks MUST NOT weaken the oracle or hand-pick seeds to hide the bug; if a
  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.
- **Task 5.1 — scenario commit-propagation pattern (applies to 5.2–5.5).** A follower's
  `commit_index`/`applied[]` only advance when it RECEIVES an AppendEntries carrying a
  `leader_commit` greater than its own (the library applies it). A scenario that replicates
  entries and calls `raft_advance_commit` on the LEADER, but never sends a follow-up
  AE/heartbeat round afterward, leaves followers at `commit_index=0` — making any per-follower
  commit-prefix / State-Machine-Safety / Leader-Completeness assertion VACUOUS on the follower
  side (5.1 has this weakness; Log Matching still validates log convergence there). For
  commit-critical scenarios — ESPECIALLY 5.4 (Figure-8) where follower commit advancement is
  the whole point — after `raft_advance_commit` on the leader, drive ANOTHER AppendEntries
  round so followers observe the new `leader_commit` and advance, then assert follower
  `commit_index`/`applied[]` actually moved. Do NOT assert convergence via a loop bounded by
  `min(commit_index)` when followers are at 0 (it silently passes). 5.1 was accepted as-is
  (meets R4.1 via throughout-checking + log matching); 5.2–5.5 should propagate commit so
  their commit assertions are non-vacuous.
- **CORRECTION (task 5.2, confirmed): this library uses a LEADER-ONLY commit model.**
  `raft_on_append_entries_request` does `(void)leader_commit;` (raft.c:646-655) — a FOLLOWER
  never advances its `commit_index`/`applied[]` from AppendEntries; `on_commit_advanced`
  fires ONLY on the leader via `raft_advance_commit` (raft.c:816). This is intended XCE
  design (follower commit visibility is a controller/heartbeat concern — see
  ha-heartbeat-committed-propagation — not the raft library). CONSEQUENCE for scenarios: a
  follow-up AE round does NOT advance follower commit; do NOT assert follower
  `commit_index == leader commit_index`. Assert re-convergence over the LOG instead
  (every node's `log_count` reaches the leader's tip + per-entry term match / Log Matching),
  and assert leader-side commit via `leader.commit_index`. For 5.4 (Figure-8), the property
  under test is LEADER-side (the leader must not mark a previous-term entry committed until a
  current-term entry commits) — driven by `raft_advance_commit` on the leader, which works.
  applied[]/SM-Safety is exercised across leader CHANGES (each node accumulates applied[]
  while it is leader). This SUPERSEDES the follower-commit-propagation guidance above.
- **PROCESS FIX (task 5.3 commit e445404 was BROKEN).** That commit captured the
  drop_dup_reorder decl (raft.h) + test (test_raft.c) but NOT its implementation in
  raft_sim.c — a stray `git checkout` (a reviewer cleaning up the `src/build` symlink)
  reverted the uncommitted impl between review and commit, so the lib build was broken
  (undefined reference) from e445404 onward. Detected during task 5.4. The exact
  implementation was recovered (byte-identical) and re-inserted into raft_sim.c; it is
  committed together with task 5.4. LESSON: after every task commit, verify `git show
  --stat` includes every expected source file (raft_sim.c was silently absent from
  e445404's stat). Reviewers must use targeted `git checkout <path>` (never `git checkout .`
  / `git stash`) so uncommitted impl is never reverted.