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

Requirements Document

Introduction

src/lib/raft/raft.{c,h} is today an election-only Raft library: it implements terms, votes, leader election, and PreVote with a pure callback interface (raft_callbacks_t, raft_state_t) and a deterministic simulator (raft_sim.c). It has no log, no AppendEntries, and no commit. The replicated log is instead hand-rolled across the controller (persist.c WAL, repl.c catch-up streaming, ha.c, ha_convergence.c) and violates the log invariants of raft/raft.tla (Ongaro's canonical Raft TLA+ spec). That split root-caused bug-851: silent committed-prefix divergence under chaotic failover. The authoritative gap analysis is .kiro/specs/ha-term-safety/TLA-gap-analysis.md (gaps G1–G6).

This feature extends the library so it owns the replicated log, strictly mirroring the raft.tla log actions, while keeping the core pure / synchronous / deterministic (no I/O, no threads) so it remains independently verifiable in the simulator against the Raft safety invariants. All side effects flow through new callbacks that a controller adapter implements over the existing WAL/repl transport. The feature closes exactly the four log-half gaps:

• G1 — per-entry term is dead today (WAL hdr.term always 0; p->term never set from ha->term). The library log model gives every entry a real uint64_t term, set to the leader's current term at append time (raft.tla ClientRequest, line 246).
• G2 — replication matches LSN contiguity only; there is no prevLogTerm check. The library enforces the logOk predicate (raft.tla AppendEntries line 204 / HandleAppendEntriesRequest line 327): prevLogIndex == 0 ∨ log[prevLogIndex].term == prevLogTerm.
• G3 — no (term, index) conflict truncation; reconcile truncates by a committed-boundary heuristic and cannot detect same-index/different-term divergence. The library implements the TLA+ conflict branch: delete the divergent entry and everything after it.
• G5 — a node adopts a higher term only on vote RPCs; the AppendEntries/heartbeat path never advances currentTerm. The library applies raft.tla UpdateTerm (line 406) on every incoming RPC including AppendEntries/heartbeat: a strictly higher term ⇒ adopt term, clear vote, step down to follower.

Commit-index advance (AdvanceCommitIndex, G4) and (lastLogTerm, lastLogIndex) vote freshness (G6) are out of scope and are closed by the downstream raft-commit-safety spec. The full conformance harness is raft-sim-conformance. The controller-side wiring of WAL / commit-barrier / snapshot onto these callbacks is owned by ha-term-safety. This spec's contract (the new callbacks and entry points below) is consumed verbatim by all three downstream specs.

Boundary Context

• In scope:

  • A per-node log model inside the library where every entry carries a uint64_t term (G1), with the log index 1-based (TLA+) and mapping 1:1 to the controller WAL LSN.
  • ClientRequest append: raft_log_append(...) appends [term ↦ currentTerm, value] on the leader (raft.tla line 246).
  • AppendEntries send: per-peer nextIndex / matchIndex leader state; emission of prevLogIndex, prevLogTerm, ≤1 entry, and leaderCommit via the on_send_append_entries callback (raft.tla line 204).
  • HandleAppendEntriesRequest: the logOk prevLogTerm match (G2), reject (stale term / ¬logOk), candidate→follower on equal term, and the accept branch's three sub-cases — already-have, conflict-truncate, append-by-(term, index) (G3) (raft.tla line 327).
  • HandleAppendEntriesResponse: success advances nextIndex / matchIndex; failure decrements nextIndex (floored at 1) (raft.tla line 393).
  • UpdateTerm applied on every incoming RPC including AppendEntries/heartbeat (G5) (raft.tla line 406).
  • The shared callback contract: on_persist_entry, on_get_entry_term, on_send_append_entries, on_truncate_from (pure protocol decisions in the library; I/O in the controller adapter).
  • The controller adapter only at the seam: it stamps the WAL hdr.term from ha->term, carries the term in the repl envelope, reads it back on recovery, and routes (term, index) match/truncate decisions back into the library.
  • Simulator coverage in raft_sim.c that drives AppendEntries across partitions, message drop/dup/reorder, and restarts, asserting the Log Matching invariant and divergent-suffix truncation.

• Out of scope (owned elsewhere):

  • AdvanceCommitIndex / commit-index advance and the Figure-8 current-term commit rule (G4) → raft-commit-safety.
  • RequestVote / PreVote freshness becoming (lastLogTerm, lastLogIndex) instead of LSN-only (G6) → raft-commit-safety.
  • The full conformance / TLC trace-check harness → raft-sim-conformance.
  • Configuration-change markers in the unified log + the upgrade snapshot → ha-term-safety.
  • Async vtask I/O, fan-out replication scheduling, the synchronous commit barrier, persist-before-ACK durability, and snapshot transport → controller callback adapters (ha-term-safety), not the pure core.
  • The heavy controller wiring of WAL / repl / recovery onto the callbacks → ha-term-safety (this spec defines only the seam contract and a thin adapter description).

• Adjacent expectations:

  • Builds on the implemented election core (raft-library); all existing election callbacks and behaviour are unchanged.
  • Preserves as policy (must NOT be canonicalized away): PreVote, priority leadership, persist-before-ACK durability + the synchronous commit barrier (consumed downstream), and "controller never self-terminates" (the library returns statuses; the controller owns liveness/fencing — the library never aborts a process).
  • Feeds raft-commit-safety (commit + freshness), raft-sim-conformance (verification harness), and ha-term-safety (XCE integration + regression). Its protocol invariants R1–R5 there are realized by this library spec rather than by patching the controller directly.

Requirements

Requirement 1: Library-owned log model with per-entry term (closes G1)

Objective: As a consumer of the raft library, I want the library to own a log where every entry carries the term under which it was created, so that entries from different terms are distinguishable and Raft log-matching becomes possible.

Acceptance Criteria

1. The Raft Library shall maintain, per node, a 1-based log index whose value at index i includes the uint64_t term recorded for the entry at that index, mirroring raft.tla log[i][...].term.
2. The Raft Library shall expose the log index as identical to the controller WAL LSN (index 1 ↔ LSN 1), so callbacks and the adapter address entries by a single shared (term, index) identity.
3. When the leader appends a client value, the Raft Library shall record the leader's current currentTerm as that entry's term, mirroring raft.tla ClientRequest (entry == [term ↦ currentTerm[i], value ↦ v]).
4. The Raft Library shall not record a fixed or zero placeholder term for any entry created while a valid term is in effect (the G1 defect).
5. While persisting or overwriting an entry, the Raft Library shall delegate the durable write to the on_persist_entry(ctx, index, term, entry, len) callback and shall not itself perform any I/O.
6. When the library needs the term of a local entry at a given index, it shall obtain it via the on_get_entry_term(ctx, index) callback, treating a return of 0 as "no entry at that index" consistent with raft.tla prevLogTerm == 0 when prevLogIndex == 0.

Requirement 2: ClientRequest append on the leader (raft.tla ClientRequest, line 246)

Objective: As a controller acting as primary, I want a single library entry point to append a new log entry stamped with the current term, so that the library — not hand-rolled controller code — owns log growth.

Acceptance Criteria

1. When raft_log_append(...) is called while the node's role is RAFT_LEADER, the Raft Library shall append one entry at index Len(log) + 1 with term equal to currentTerm, mirroring raft.tla ClientRequest.
2. If raft_log_append(...) is called while the node's role is not RAFT_LEADER, then the Raft Library shall reject the append and report a non-success status without mutating the log.
3. When appending, the Raft Library shall invoke on_persist_entry for the new (index, term, entry) before reporting success, preserving the persist-before-act ordering used by the existing election path's on_persist.
4. The Raft Library shall return the assigned 1-based index to the caller on a successful append, so the controller adapter can map it to the WAL LSN.
5. The Raft Library shall not, in this spec, advance any commit index as a side effect of append (commit advance is owned by raft-commit-safety).

Requirement 3: AppendEntries emission with per-peer next/match index (raft.tla AppendEntries, line 204)

Objective: As a primary replicating to standbys, I want the library to own per-peer replication progress and emit correctly-formed AppendEntries, so that replication carries the (prevLogIndex, prevLogTerm) needed for log-matching.

Acceptance Criteria

1. The Raft Library shall maintain, per peer, a nextIndex and a matchIndex (the raft.tla leaderVars), initialized on becoming leader to nextIndex = Len(log) + 1 and matchIndex = 0 for every peer, mirroring raft.tla BecomeLeader.
2. When the library emits an AppendEntries to peer j, it shall compute prevLogIndex = nextIndex[j] - 1 and prevLogTerm = (prevLogIndex > 0) ? term-at-prevLogIndex : 0, mirroring raft.tla AppendEntries.
3. When the library emits an AppendEntries to peer j, it shall send at most one entry, constrained by the end of the log (SubSeq(log, nextIndex[j], Min(Len(log), nextIndex[j]))), via the on_send_append_entries(ctx, peer_idx, prevLogIndex, prevLogTerm, leaderCommit, ...) callback.
4. The Raft Library shall pass the leader commit value through on_send_append_entries as an opaque leaderCommit argument and shall not itself interpret or advance commit (commit handling is owned downstream).
5. While the node's role is not RAFT_LEADER, the Raft Library shall not emit AppendEntries for that node.

Requirement 4: HandleAppendEntriesRequest — logOk, reject, step-down, accept (raft.tla line 327; closes G2, G3)

Objective: As a standby receiving replication, I want the library to accept, reject, or conflict-truncate strictly by (term, index) matching, so that Log Matching holds and divergent suffixes are truncated.

Acceptance Criteria

1. When raft_on_append_entries_request(...) is processed, the Raft Library shall compute logOk = (prevLogIndex == 0) ∨ (prevLogIndex ≤ Len(log) ∧ on_get_entry_term(prevLogIndex) == prevLogTerm), mirroring the raft.tla logOk predicate (closes G2).
2. If the request term is less than currentTerm, or the term equals currentTerm and the node is a follower and ¬logOk, then the Raft Library shall reject the request and report failure with matchIndex = 0, mirroring the raft.tla reject branch.
3. When the request term equals currentTerm and the node is a candidate, the Raft Library shall transition the node to follower (return-to-follower branch) without otherwise mutating the log.
4. When the request term equals currentTerm, the node is a follower, and logOk holds, and the incoming entry already matches the local entry at index = prevLogIndex + 1 (same term, or no entries sent), the Raft Library shall treat the request as already-satisfied and report success with matchIndex = prevLogIndex + len(entries) without rewriting the log.
5. When logOk holds and the local entry at index = prevLogIndex + 1 exists with a different term than the incoming entry, the Raft Library shall delete the divergent entry and all entries after it via on_truncate_from(ctx, index), mirroring the raft.tla conflict branch (closes G3).
6. When logOk holds and the local log ends exactly at prevLogIndex (no entry at prevLogIndex + 1), the Raft Library shall append the incoming entry via on_persist_entry and report success, mirroring the raft.tla no-conflict append branch.
7. The Raft Library shall return a reply carrying success/failure and the resulting matchIndex so the leader can update its per-peer progress, and shall not perform transport I/O itself (the adapter sends the reply).

Requirement 5: HandleAppendEntriesResponse — advance/decrement progress (raft.tla line 393)

Objective: As a primary processing replication replies, I want the library to advance or back off per-peer progress, so that a lagging or divergent follower is walked back to the matching point.

Acceptance Criteria

1. When raft_on_append_entries_reply(...) reports success, the Raft Library shall set nextIndex[peer] = matchIndex + 1 and matchIndex[peer] = reply.matchIndex, mirroring raft.tla HandleAppendEntriesResponse success.
2. If raft_on_append_entries_reply(...) reports failure, then the Raft Library shall set nextIndex[peer] = Max(nextIndex[peer] - 1, 1) and leave matchIndex[peer] unchanged, mirroring the raft.tla failure branch.
3. The Raft Library shall apply a reply only when the reply term equals currentTerm, ignoring stale-term responses, consistent with raft.tla HandleAppendEntriesResponse / DropStaleResponse.
4. The Raft Library shall not, in this spec, recompute or advance any commit index from updated matchIndex values (owned by raft-commit-safety).

Requirement 6: UpdateTerm on every RPC including AppendEntries/heartbeat (raft.tla line 406; closes G5)

Objective: As any cluster member, I want a strictly-higher term on any incoming RPC — vote, AppendEntries, or heartbeat — to advance my term and step me down, so that a rejoined node can never act or re-elect at a stale term and two leaders can never share a term.

Acceptance Criteria

1. When an incoming AppendEntries or heartbeat RPC carries a term strictly greater than currentTerm, the Raft Library shall set currentTerm to that term, clear voted_for, and transition to follower, mirroring raft.tla UpdateTerm (closes G5).
2. While adopting a higher term from any RPC, the Raft Library shall persist the new (term, voted_for) via the existing on_persist callback before processing the rest of the RPC, preserving the durability ordering already used on the vote path.
3. When a node that was leader adopts a higher term from an AppendEntries/heartbeat RPC, the Raft Library shall fire on_become_follower so the controller HA FSM steps down (mirroring the existing higher-term step-down already wired for vote RPCs).
4. The Raft Library shall apply the term-adoption check on the AppendEntries path before the logOk / accept-reject logic, so a higher-term request is never rejected merely because the local log does not match.
5. The Raft Library shall not, on equal or lower term, alter currentTerm or voted_for from the AppendEntries path (term adoption is strictly-greater-than only), consistent with raft.tla.

Requirement 7: Shared callback contract and pure-core / adapter split

Objective: As a downstream spec author (raft-commit-safety, raft-sim-conformance, ha-term-safety), I want the new callbacks and entry points fixed verbatim and the library kept pure, so that I can depend on a stable seam without re-deriving the protocol.

Acceptance Criteria

1. The Raft Library shall define the required callback int on_persist_entry(void *ctx, uint64_t index, uint64_t term, const void *entry, size_t len) to durably append or overwrite the entry at index.
2. The Raft Library shall define the required callback uint64_t on_get_entry_term(void *ctx, uint64_t index) returning the term of the local entry at index, or 0 when absent.
3. The Raft Library shall define the required callback int on_send_append_entries(void *ctx, int peer_idx, uint64_t prev_log_index, uint64_t prev_log_term, uint64_t leader_commit, ...) carrying an entries handle, to transmit one AppendEntries.
4. The Raft Library shall define the required callback int on_truncate_from(void *ctx, uint64_t index) to delete local entries in index..end.
5. The Raft Library shall keep all four callbacks free of protocol decisions: the library decides what/whether to persist, send, or truncate; the controller adapter only performs the I/O (WAL write, transport, recovery read-back).
6. The Raft Library shall leave all existing election callbacks (on_send_vote_request, on_become_leader, on_become_follower, on_persist, on_schedule_timeout, on_cancel_timeout, on_start_election_after_delay, optional on_vote_eligible / on_send_pre_vote_request / on_trace) and their behaviour unchanged.
7. The controller adapter shall implement the four callbacks over the existing WAL/repl transport — stamping hdr.term from ha->term, carrying the term in the repl envelope, reading it back on recovery, and routing (term, index) match/truncate decisions to the library — while the heavy controller wiring lives in ha-term-safety as a downstream consumer.

Requirement 8: Deterministic Log Matching verification in the simulator

Objective: As a maintainer, I want the deterministic simulator to drive replication under adversarial conditions and assert Raft Log Matching, so that the log-half implementation is verifiable without a live cluster.

Acceptance Criteria

1. The Raft Simulator shall route AppendEntries requests and responses synchronously between nodes (mirroring its existing vote-RPC routing), honoring per-node partition flags.
2. The Raft Simulator shall provide an in-memory per-node log backing the four new callbacks, so a node can append, read entry terms, send, and truncate deterministically.
3. The Raft Simulator shall exercise message drop, duplication, and reordering of AppendEntries, plus node restart, while replication proceeds.
4. The Raft Simulator shall assert the Log Matching invariant after replication: for any two nodes and any index i, if both hold an entry at i with the same term, then their entire prefixes through i are byte-identical.
5. When a follower holds a divergent suffix (same index, different term) and then receives the leader's AppendEntries, the Raft Simulator shall assert that the follower truncates the divergent suffix and converges to the leader's prefix.
6. While driving chaotic leadership churn (a stale-term node rejoining under a higher-term leader), the Raft Simulator shall assert that the rejoining node adopts the higher term from the AppendEntries/heartbeat path (G5) and does not re-elect at a reused term.