myxce/.kiro/specs/raft-log-replication/research.md

Research Log: raft-log-replication

Discovery Scope

Extension of an existing, implemented pure-C library (src/lib/raft/raft.{c,h} + raft_sim.c). Discovery type: Extension / integration-focused — the architecture pattern (pure state machine + callback ports + deterministic simulator) already exists and is authoritative; this feature adds the log half of raft/raft.tla to it. No external dependency research needed (the library is free-standing C with only errno.h/stdint.h/string.h).

Authoritative Sources

Source	Use
.kiro/specs/raft-log-replication/brief.md	Problem, approach, Authoritative shared callback contract (binding, reproduced verbatim in design), TLA+ action→entry-point map
raft/raft.tla	Canonical log actions: ClientRequest (246), AppendEntries (204), HandleAppendEntriesRequest (327), HandleAppendEntriesResponse (393), UpdateTerm (406), BecomeLeader (229)
.kiro/specs/ha-term-safety/TLA-gap-analysis.md	Gaps G1–G6; this spec closes G1/G2/G3/G5
src/lib/raft/raft.{c,h}	Existing election core style: raft_config_t extensibility, persist-before-act, NULL-checked required callbacks, status-code returns, XCE_TESTING sim
.kiro/steering/roadmap.md (Raft TLA+ Conformance series)	Family policy: preserve PreVote, priority leadership, sync commit-barrier + persist-before-ACK, controller-never-self-terminates

Key Findings

1. The library must NOT store entry bytes. The election core already declines to store (term, voted_for) bytes — the caller restores them via raft_config_t and the library writes via on_persist. The log follows the same discipline: the library tracks only log_len + per-peer next_index/match_index; entry terms come from on_get_entry_term, bytes live in the adapter/simulator. This keeps raft_state_t fixed-size and the core pure/deterministic (simulator-verifiable). Decision: no per-entry array in raft_state_t.

2. Index ↔ LSN is 1:1 and 1-based. raft.tla logs are 1-based; the controller WAL LSN is the natural mapping. Settling this in the contract (R1.2) means the controller adapter and simulator address entries identically. on_get_entry_term(0) / prevLogIndex==0 → term 0 is the absent sentinel, matching raft.tla's prevLogTerm == 0 when prevLogIndex == 0.

3. UpdateTerm must precede logOk on the AE path (G5). The bug-851 mechanism: a rejoined standby never adopted the leader's term from heartbeats, re-elected at a stale+1 term, and reused a term → two leaders/term. raft.tla Receive applies UpdateTerm before any handler. Decision: the request handler applies term adoption first, unconditionally, including for 0-entry heartbeats — otherwise a higher-term request could be rejected for a log mismatch and never advance the term (R6.4).

4. leader_commit is carried but not acted on. Commit advance (G4) is raft-commit-safety. To avoid a later signature change (a Revalidation Trigger for all downstream consumers), the AppendEntries entry points accept leader_commit opaquely now and ignore it. This stabilizes the wire/sim shape across the two specs. Decision (build-vs-defer): include the parameter, defer the behavior.

5. (term, index) truncation replaces the LSN-only reconcile. The controller's ha_convergence.c truncates by a committed-boundary heuristic (G3) and cannot see same-LSN/different-term divergence. The library's conflict branch (on_truncate_from(index) + re-append) is the exact raft.tla semantics. The heavy controller swap is ha-term-safety; this spec owns the library decision + the simulator proof.

Synthesis Outcomes

• Generalization found: the existing "pure core, I/O via callbacks, restore-state-via-config, never-read-storage" pattern generalizes cleanly from election state to log state. No new architectural concept is introduced — only new ports and new pure transitions.
• Build-vs-adopt: adopt the canonical raft.tla algorithm verbatim (it is the verified reference). Build only the C translation + the in-memory simulator backing. No third-party Raft library is imported (the project's constraint is a free-standing, simulator-verifiable core).
• Simplification: keep the "≤1 entry per AppendEntries" raft.tla simplification rather than batching — it minimizes atomic regions, matches the spec exactly, and keeps the simulator's Log Matching assertion tractable. Batching is an adapter-side optimization that can be layered later without changing the core contract.
• Risk: a future signature change to the four callbacks or the three entry points cascades to three downstream specs (logged as Revalidation Triggers). Mitigated by reproducing the brief's contract verbatim and by accepting leader_commit now.