docs(ha-commit-durability): flip bug-661 KNOWN GAP to GUARANTEED + re-verify protocol checklist (task 5.3)

.kiro/specs/ha-commit-durability/tasks.md

@@ -118,7 +118,7 @@
   - _Requirements: 1.1, 1.5, 2.2, 2.3, 2.6_
   - _Depends: 5.1, 4.3, 1.3_
 
-- [ ] 5.3 Re-verify the formal safety checklist and flip the durability gap note
+- [x] 5.3 Re-verify the formal safety checklist and flip the durability gap note
   - Re-run the `raft/raft.tla` alignment and the Protocol Verification Checklist (commit rule, leader completeness, `commitIndex` monotonic) against the integrated implementation.
   - IMPORTANT — raft.tla does NOT model durability: it restores `log` intact from "stable storage" on restart (`raft.tla:165-174`), i.e. it assumes what bug-661 violates. A passing TLC/alignment run on the unmodified spec therefore does NOT prove the commit-durability invariant. That invariant is verified by the unit/integration/E2E tests (2.x, 5.1, 5.2) plus the manual checklist — not by raft.tla. Do not conclude durability is proven from raft.tla alone. Formal durability proof would require extending raft.tla with a durable-vs-volatile log model (out of scope unless explicitly opted in).
   - Update `src/controller/CLAUDE.md`: convert the "Commit Durability — KNOWN GAP (bug-661)" note into the now-true guarantee and tick the post-`ha-commit-durability` checklist item.
@@ -145,3 +145,4 @@
 - 4.4: Closed the 5.2-soak liveness gap. `raft_cb_become_leader` NO LONGER FATALs synchronously — on FENCE / would-be-FATAL (truncated or durable_floor < HWM) it calls `ha_arm_promotion_fence_timer` (sets `in_catch_up`, schedules a one-shot `delay_task_ms(&c->delaymgr, ha_promotion_fence_window_ms(), 1, promotion_fence_timeout_fn, ctx)`) and RETURNS without becoming primary. The timer callback (`promotion_fence_timeout_fn`, ha.c:702) re-reads LIVE state after the window: caught-up (`!truncated && durable_floor>=HWM`) → release fence, NO FATAL (Req 2.6); peer reachable (`repl_active_standby_count>0`) OR durable_floor advanced past the arm-time baseline → progress possible, leave fenced (existing catch-up machinery / next promotion-gate ELIGIBLE releases it), NO FATAL; ONLY still-truncated/behind + no-peer + no-progress → 3.3 `persist_recover_fatal_if_unrecoverable` (Req 2.4). UAF-safe cancel (`ha_cancel_promotion_fence_timer`: cancelled flag + atomic-exchange the stored ctx; handle cleared before the cancelled-check, mirrors `raft_election_timeout_fn`); cancelled in `ha_fini`; fail-loud if `delay_task_ms` itself fails (never fence indefinitely). Test window seam `ha_set_promotion_fence_window_ms` + driver `ha_arm_promotion_fence_timer_for_test`. 3 tests (defers-fatal-to-timer, released-on-catchup-no-fatal, cancel-prevents-fatal) with RED proof (re-injecting sync FATAL → 3 fails). Reviewed MAIN CONTEXT (subagent spend limit): suite :FAIL:==0, /tmp fsync-able this run. NOTE: this is the bounded-window timer 4.3/5.1 deferred; with it, 5.2's soak should keep the cluster available (truncated rejoiners catch up, not die).
 - REWORK (2026-06-18, user invariant — a controller MUST NEVER self-terminate): tasks 3.3/4.3/4.4 had implemented Req 2.4 "fail loud" as a SELF-ABORT (`persist_recover_fatal_if_unrecoverable → tlog_exit(); abort()` + `persist_fatal_hook`). That violated the invariant (a self-exited controller needs MANUAL admin recovery + leaves quorum degraded; a live retrying node self-heals when a peer returns) and was the true root cause of the 5.2 soak quorum collapse. CORRECTED: removed the abort/exit terminal entirely. New: `persist_recover_loud_fence_if_unrecoverable(persist_t*)` (NO abort) logs a loud operator-visible ERROR (truncation boundary vs cluster HWM) + sets sticky `_Atomic bool recovery_unrecoverable` (accessors `persist_recovery_unrecoverable`/`persist_clear_recovery_unrecoverable`); the member STAYS ALIVE, permanently non-promotable/fenced (`in_catch_up` + the sticky flag both consulted by the promotion gate), and KEEPS RETRYING catch-up. Decision enum `RECOVER_DECISION_FATAL` → `RECOVER_DECISION_FENCE_UNRECOVERABLE` (non-terminating). 4.4 timer no longer aborts — it re-emits the loud operator alert + re-arms (operator visibility), never exits. Flag + fence CLEAR automatically on catch-up (not truncated AND durable_floor ≥ HWM) → re-eligible (Req 2.6), fully automatic. `persist_fatal_hook` removed. Verified: grep/nm show NO abort/exit/tlog_exit on the recovery path; ASAN suite :FAIL:==0; reworked tests (row4/4b → loud_fence, unrecoverable-stays-alive-loud, released-on-catchup, cancel-stops-realert) PASS. Spec updated: requirements.md Req 2.4 + design.md (decision table rows 4/4b, RecoveryIntegrity, traceability, FATAL-vs-fence open question) reworded "FATAL/terminate" → "LOUD PERMANENT FENCE (non-promotable, stays alive, keeps retrying — NEVER self-exit)". PROJECT-WIDE GUIDANCE added: `src/controller/CLAUDE.md` §"Process Lifecycle (DESIGN INVARIANT)" + `.kiro/steering/ha-async-io.md` — controllers never self-terminate. (`ha_self_restart` execv-restart in convergence/demotion is a SEPARATE primitive, untouched.)
 - 5.2: PASS on the reworked (no-self-exit) build. (a) DETERMINISTIC E2E flipped RED→GREEN, stable 3/3 runs / 9-9 probes — in-window primary fdatasync ≥1 (=2) precedes the ack ("durable-before-ack"), the inverse of 1.3's unfixed RED. (b) ROLLING SIGKILL soak (6 rounds) exit 0 = ZERO acknowledged-job loss, cluster stayed continuously available, 0 self-terminations (the no-self-exit rework removed the abort that collapsed quorum in the first attempt). Validation-only (no production code). NOTE: ran in-sandbox via background+poll on a worktree deploy dir (avoids /tmp overlay EIO); the earlier collapse was the abort terminal, now corrected — a host re-run is still good practice but the in-sandbox soak now passes with the fix.
+- 5.3: Formal re-verification (conceptual — no TLA+ toolchain in env; project practice = manual alignment + the CLAUDE.md Protocol Verification Checklist). Checklist walked against the integrated impl, all hold: votedFor/currentTerm (untouched); `commitIndex`/`committed_lsn` monotonic + never exceeds `durable_lsn` (2.2/2.4 debug-assert); leader commits via per-entry majority ack (unchanged); `safe_committed_lsn` from voter replies (untouched, 4.2/4.3); WAL truncation only above the safe point + `durable_lsn` clamped on truncate; freshness gate term-then-index with durable-backed LSN (4.1 pinned vs raft.tla `mlastLogIndex`/`LastTerm`; candidate bare `durable_floor`, voter floor `max(durable_floor, learned)`); contiguous-prefix commit; `durable_lsn` prefix watermark; causal-order append; and the NEW item — a member counts toward the commit majority only at its durable LSN, acknowledged⇒durable-on-majority — now TRUE. raft.tla alignment: the election/freshness logic maps faithfully; raft.tla does NOT model durability (assumes a durable log, restores `log` intact on restart `raft.tla:165-174`) so it CANNOT prove the commit-durability invariant — that invariant is backed by tests 2.x/5.1 + the deterministic RED→GREEN E2E + the zero-loss/available soak (5.2), NOT by raft.tla. `src/controller/CLAUDE.md`: "Commit Durability — KNOWN GAP (bug-661)" flipped to "GUARANTEED / CLOSED (landed 2026-06-18)" with the mechanism list (incl. the no-self-exit loud fence); the post-`ha-commit-durability` checklist item ticked `[x]`. ALL 17 tasks (1.1–5.3) + the no-self-exit rework COMPLETE.

src/controller/CLAUDE.md

@@ -78,7 +78,7 @@ The file `raft/raft.tla` contains Diego Ongaro's TLA+ specification of the Raft
 
 **Commit Ordering** (contiguous, in log order — RULE): `committed_lsn` advances only as a contiguous prefix in LSN/append order; entries are never committed or reordered out of log order. The single-writer append lock (`p->lock`) is the serialization point. Durability flushing (incl. group-commit batching) makes a contiguous **prefix** durable only — `durable_lsn` is a prefix watermark, never a per-entry set, so a later entry can never be durable while an earlier one is not. Log order must preserve **causal dependencies** (append a cause before its effect — e.g. job submit before job start); independent concurrent events take an arbitrary but consistent total order, which is linearizable via the single serialization point plus commit-gated reply. Out-of-order / parallel commit is NOT supported by this single-log architecture (it would require per-entity logs with dependency tracking — explicitly out of scope).
 
-**Commit Durability** (acknowledged ⇒ durable on a majority — TARGET RULE): when the controller replies success to a client, the operation's entry must be `fdatasync`'d on a fault-tolerant majority (the acking member + ⌊N/2⌋ others); a member counts toward the commit majority for an LSN only once that LSN is durable locally (self caps at `durable_lsn`, not the appended tip). **KNOWN GAP — bug-661, spec `ha-commit-durability` (in progress, 2026-06-18):** the commit majority currently counts the primary's *appended* (page-cache) tip via `majority_candidate_locked`, and primary fsync is async (`fsync_worker` timer), so "committed" does NOT yet imply durable-on-a-majority — an acknowledged entry can be durable on a single member and lost across failover. Until that spec lands, do not assume an acked operation survives a crash of the acking minority.
+**Commit Durability** (acknowledged ⇒ durable on a majority — GUARANTEED): when the controller replies success to a client, the operation's entry is `fdatasync`'d on a fault-tolerant majority (the acking member + ⌊N/2⌋ others); a member counts toward the commit majority for an LSN only once that LSN is durable locally (self caps at `durable_lsn`, not the appended tip). **CLOSED — bug-661, spec `ha-commit-durability` (landed 2026-06-18).** Mechanisms: `majority_candidate_locked` caps the primary self-contribution at `persist_durable_lsn` (not `highest_appended_lsn`); `fsync_worker` is a demand-driven group-commit flusher that advances `durable_lsn` only after a successful `fdatasync` and wakes the commit eval (fail-loud rc-gate — `durable_lsn` never advances on `fdatasync` error); the standby `fdatasync`s before its WalAck and the ACK is gated on that sync's success; recovery distinguishes a clean vs corruption-truncated WAL (`recover_verdict_t`) and re-derives the durable floor (WAL tip); the vote/PreVote freshness floor and a candidate's advertised position are durable-backed (candidate advertises bare `persist_durable_floor`, voter floor = `max(durable_floor, last_known_committed_lsn)`), and a pre-promotion gate fences a recovery-truncated/behind member (it catches up before leading; if genuinely unrecoverable it stays a loud, non-promotable, *alive* fence — never self-exits — and self-heals on peer return). Verified by unit/integration tests (2.x, 5.1), the deterministic ack-before-fdatasync gap E2E (RED→GREEN), and the rolling-failover soak (zero acked-job loss, cluster stays available) — NOT by `raft.tla`, which assumes a durable log (restores `log` intact from stable storage on restart, `raft.tla:165-174`) and so cannot model the durability invariant; that invariant rests on these tests + this checklist.
 
 ### Post-Election Safe Commit Point (Critical)
 
@@ -105,7 +105,7 @@ When modifying HA protocol code (election, replication, heartbeat), verify:
 - [ ] `committed_lsn` advances only as a contiguous LSN-ordered prefix — no out-of-order or per-entry commit
 - [ ] Durability flushing makes a contiguous prefix durable; `durable_lsn` is a prefix watermark (never a per-entry set)
 - [ ] Causal dependencies are appended in order (cause before effect, e.g. submit before start)
-- [ ] (post `ha-commit-durability`) a member counts toward the commit majority only at its durably-persisted LSN; acknowledged ⇒ durable on a majority
+- [x] (post `ha-commit-durability`, landed 2026-06-18) a member counts toward the commit majority only at its durably-persisted LSN; acknowledged ⇒ durable on a majority
 
 ## HA Design Constraints