docs(ha-commit-durability): pin durable-backed freshness-floor formula + election safety/liveness verification (task 4.1)

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

@@ -310,6 +310,131 @@ Key decisions: corruption is never silently accepted (Req 2.1). A truncated memb
 - Validation: simulate a node restarting truncated; assert it is denied promotion until catch-up, then re-enabled (Req 2.2/2.6).
 - Risks: interaction with `ha-single-leader-role` own-term gate and `ha-prevote` — re-verify the combined eligibility predicate against `raft.tla`.
 
+### Freshness-Floor Formula (task 4.1)
+
+> **Status:** PINNED (task 4.1, gating). This section is the authoritative contract that tasks **4.2** (implement the floor in `ha.c`/`cluster.c`) and **4.3** (promotion gate) implement against. **Verification method:** this is a **manual conceptual-alignment + Protocol Verification Checklist** argument, NOT a TLC run — there is no TLA+ toolchain in this environment (no `tla2tools.jar`/TLC/java). The argument maps the formula to `raft/raft.tla`'s `mlastLogIndex`/`LastTerm` semantics and to the `src/controller/CLAUDE.md` checklist. Per the spec scope note, `raft.tla` validates the **election/freshness logic** this change touches; it does **not** validate the *durability* of the floor — that is verified by tests 3.4 / 2.x, because `raft.tla` assumes a durable log (see Non-Goals and §5.3 of the broader Raft model).
+
+#### 1. The pinned formula
+
+Let, on member `M`:
+- `durable_floor(M) = persist_durable_floor(M)` — the durable WAL tip (task 3.4): the highest LSN whose bytes are `fdatasync`'d locally, re-derived on recovery as the **highest intact replayed LSN** (the truncation boundary on `RECOVER_TRUNCATED`, the clean tip on `RECOVER_CLEAN`). This is a durable **last-log index**, not the commit position.
+- `learned_committed(M) = last_known_committed_lsn(M)` — the volatile learned cluster commit high-water (a hint, possibly stale across a truncating restart).
+- `learned_tag(M) = committed_config_tag(M)`, `local_tag(M) = config_version_tag` — the config epoch (compared first; unchanged by this task).
+
+**(a) What a candidate ADVERTISES (`mlastLogIndex` analog):**
+
+```
+cand_lsn = durable_floor(M)            // NOT max(applied_lsn, learned_committed)
+cand_tag = max(local_tag, learned_tag) // config epoch, unchanged
+```
+
+The candidate advertises **exactly its durable WAL tip**. It does **not** advertise `applied_lsn` (which can exceed the durable tip — entries applied to volatile state but not yet `fdatasync`'d) and does **not** advertise `learned_committed` (a hint that, after a truncating restart, can exceed the durable tip the node actually holds). This is the core change: a candidate may only claim a log position it can durably back. `cand_tag` is unchanged — config-epoch freshness is orthogonal to log durability.
+
+**(b) What a voter uses as its freshness FLOOR (the reconciliation):**
+
+```
+voter_floor_lsn = max( durable_floor(M), learned_committed(M) )
+voter_floor_tag = max( local_tag(M), learned_tag(M) )      // unchanged
+```
+
+The voter floor is the **max of its own durable tip and its learned cluster-committed high-water**. This is the precise reconciliation of the durable-derived floor against the existing `max(applied_lsn, last_known_committed_lsn)`:
+- `applied_lsn` is **replaced** by `durable_floor` (a node must not demand of a candidate a position it itself only holds volatilely; and symmetrically must not under-advertise — see §3/§4). Note `applied_lsn` and `durable_floor` use **different conventions and are not directly comparable as raw counters**: `applied_lsn` is advanced to `last_good_lsn + 1` (a *next-expected* index; `ha.c:1234/1253`), whereas `durable_floor`/`durable_lsn` is the actual durable LSN *watermark* (the highest LSN whose bytes are `fdatasync`'d). We therefore do **not** rely on a raw `durable_floor ≤ applied_lsn` inequality. The claim that this term never raises the floor beyond what is reachable rests entirely on the `D*` argument in §4: the voter floor's local-state contribution `durable_floor(v)` is bounded above by `D*` (the most-durable reachable candidate's tip) by definition of `D*`, so swapping in `durable_floor` cannot push the floor above some reachable candidate ⇒ cannot newly induce livelock (§4).
+- `learned_committed` is **retained** as the safety backstop established by bug-339: a voter must never grant to a candidate below what the cluster has already **committed**, even if this voter's own durable tip is colder. Committed entries are now durable on a majority (Req 1/2.x), so at least a majority of voters carry that committed LSN in their `durable_floor` *and* every voter that learned the commit carries it in `learned_committed` — keeping the floor at the committed high-water on the voter side closes the window where a lagging voter would otherwise grant to a sub-committed candidate.
+
+**(c) The exact comparison (candidate ≥ voter floor — `logOk` analog):**
+
+```
+grant_freshness(cand, voter) ==
+       cand_tag >  voter_floor_tag
+    \/ ( cand_tag == voter_floor_tag  /\  cand_lsn >= voter_floor_lsn )
+```
+
+i.e. deny iff `cand_tag < voter_floor_tag`, or `cand_tag == voter_floor_tag && cand_lsn < voter_floor_lsn`. Term-then-index ordering, matching raft's `LastTerm`-then-`mlastLogIndex` lexicographic order; here the config epoch (`tag`) is the high-order key (raft's `LastTerm`) and the durable LSN is the low-order key (raft's `mlastLogIndex`). Equality at both ⇒ grant (a node at least as fresh, including exactly as fresh, is grantable — preserves the existing `>=` semantics and idempotent re-grant).
+
+**Candidate and voter use DIFFERENT quantities — this is the load-bearing distinction, and the implementation must keep the two paths separate:**
+
+| Role | Site(s) | Quantity it must produce | How |
+|------|---------|--------------------------|-----|
+| **Candidate** (advertised `cand_lsn`) | `ha.c:3660-3666` (real-vote snapshot), `ha.c:3735-3741` (PreVote snapshot) | **bare `durable_floor(M)`** — NOT folded with `learned_committed` | snapshot `persist_durable_floor(p)` **directly** into `cand_lsn`; do **NOT** route the advertised LSN through `ha_vote_self_freshness` |
+| **Voter** (freshness floor `voter_floor_lsn`) | `cluster.c:388-395` (real-vote), `cluster.c:471-475` (PreVote), `ha.c:2243` (legacy test gate) | **`max(durable_floor(M), learned_committed(M))`** — the backstop is retained | keep calling `ha_vote_self_freshness`, changing only its `local_lsn` input from `applied_lsn` to `durable_floor(M)`; the function still folds in `last_known_committed_lsn` |
+
+**Why the candidate must NOT reuse `ha_vote_self_freshness`.** That function (`ha.c:2127-2142`) *unconditionally* computes `*out_lsn = max(local_applied_lsn, last_known_committed_lsn)`. Feeding it `durable_floor` as the local input therefore yields `max(durable_floor, learned_committed)` — **not** the bare `durable_floor` §1a/§3 require. A truncated node with `durable_floor = 4` but a stale volatile `learned_committed = 8` would then advertise `cand_lsn = 8` and **win** — exactly the truncated-candidate-wins hole this task closes (§5a). So 4.2 must give the candidate sites a **candidate-only path** that calls `persist_durable_floor(p)` directly and assigns it to `cand_lsn`, bypassing the `learned_committed` fold. (The candidate's `cand_tag` is still `max(local_tag, learned_tag)`; only the **LSN axis** must bypass the fold.) The two PreVote/real-vote candidate snapshots currently call `ha_vote_self_freshness` for both fields — 4.2 splits the LSN field off onto the bare-`durable_floor` path while leaving the tag field on the existing max.
+
+**Why safety lives on the advertisement axis and the backstop lives on the voter axis.** The candidate must not **over-advertise** beyond durable state — that is the safety requirement (§3): pinning `cand_lsn = durable_floor` is what denies a truncated candidate. The `learned_committed` backstop belongs on the **voter** axis (§3 dual guard): a voter must refuse any candidate below the cluster-committed boundary it learned, even when the voter's own durable tip momentarily lags. Folding `learned_committed` into the *candidate* advertisement would defeat the very safety property it protects on the *voter* side; folding it into the *voter* floor is exactly the bug-339 backstop. raft.tla confirms the split: `RequestVote` sends `mlastLogIndex |-> Len(log[i])` — the **bare candidate log length**, with no committed term folded into the candidate's advertisement; the committed-high-water guard lives only on the voter's `logOk` floor. This recipe is now internally consistent with §1a (bare candidate `durable_floor`), §3 (quorum-intersection on the advertised `durable_floor`), and §4 (voter floor bounded by `D*`).
+
+**(d) `safe_committed_lsn` is UNCHANGED and still from voter replies.** This floor governs only **vote granting / advertisement**. The post-election `safe_committed_lsn` is still computed by `ha_compute_safe_committed_lsn` from the `peerLastLogLsn` values in the `RequestVoteReply` set (`ha.c:480/562`), never from this floor and never from a stale ctrlhello (CLAUDE.md "Post-Election Safe Commit Point"). The reply's `peer_last_log_lsn` (`cluster.c:426`) now carries the durable-backed `voter_floor_lsn`, which is *more* conservative (never above a durable position), so the elected leader's `safe_committed_lsn` is if anything tightened, never loosened — `persist_truncate_wal_above(safe_committed_lsn)` still only removes entries strictly above a majority-backed point.
+
+#### 2. raft.tla alignment
+
+`raft.tla` (`HandleRequestVoteRequest`, lines 284-289):
+
+```
+logOk == \/ m.mlastLogTerm > LastTerm(log[i])
+         \/ /\ m.mlastLogTerm = LastTerm(log[i])
+            /\ m.mlastLogIndex >= Len(log[i])
+```
+
+Mapping:
+- `Len(log[i])` (voter's last-log **index**) ↔ `voter_floor_lsn` on the durable axis. Our durable WAL tip `persist_durable_floor` is the faithful analog of `Len(log[i])`: in `raft.tla` the log is **restored intact from stable storage** on restart (the model has no volatile-vs-durable distinction — every entry in `log[i]` is durable by assumption). By making committed entries durable on a majority (2.x) and deriving the advertised/floor index from `persist_durable_floor` (the on-disk tip) rather than a volatile `applied_lsn`, our `cand_lsn`/`voter_floor_lsn` become the genuine "length of the durable log," so the `mlastLogIndex >= Len(log[i])` comparison holds with the same meaning the model assigns it.
+- `m.mlastLogIndex` (candidate's advertised index) ↔ `cand_lsn = durable_floor(candidate)` — exactly raft's `mlastLogIndex |-> Len(log[i])` in `RequestVote` (line 196): the candidate advertises *its own log length*, which in our durable-log mapping is its durable tip. The pre-change code advertised `max(applied_lsn, learned_committed)`, which could exceed `Len(durable log)` — an over-advertisement raft.tla cannot express (in the model you cannot advertise an index beyond `Len(log[i])`). The fix restores faithfulness to the model.
+- `LastTerm(log[i])` / `m.mlastLogTerm` ↔ the config epoch `tag`. XCE folds per-entry Raft terms into a monotone config-version tag (single-writer log; term changes ride the config epoch); the high-order lexicographic key is preserved. This task does not change tag handling.
+
+**Caveat (restated):** `raft.tla` does **not** model durability — it assumes `log[i]` survives restart intact, so it cannot itself prove that `persist_durable_floor` *is* durable. That property (the WAL-tip derivation is genuinely on stable storage and survives an ungraceful kill) is the subject of tests 3.4 and 2.x, not this alignment argument. What `raft.tla` *does* validate — and what this section argues we faithfully implement — is the election/freshness **logic**: with our durable tip standing in for `Len(log)`, the `logOk` predicate and the Leader-Completeness proof carry over.
+
+#### 3. Leader Completeness (safety) — a truncated/behind candidate cannot win
+
+Claim: under this formula, any candidate that wins an election holds **all committed entries** (raft's Leader Completeness).
+
+Argument:
+1. By Req 1/2.x, an entry committed at LSN `L` is `fdatasync`'d on a **majority** `Q_L` of members; each member in `Q_L` has `durable_floor ≥ L` (durability is a contiguous prefix watermark — CLAUDE.md Commit Ordering — so a durable tip ≥ L implies all entries ≤ L are durable on that member).
+2. A candidate `C` needs votes from a **majority** `Q_v`. Any two majorities intersect: `Q_L ∩ Q_v ≠ ∅`, so at least one voter `v` has `durable_floor(v) ≥ L`, hence `voter_floor_lsn(v) ≥ durable_floor(v) ≥ L`.
+3. For `v` to grant, the comparison requires `cand_lsn ≥ voter_floor_lsn(v) ≥ L`. Since `cand_lsn = durable_floor(C)` (the candidate cannot advertise above its durable tip), `durable_floor(C) ≥ L` — `C` durably holds entry `L` (again by the prefix-watermark property, all entries ≤ L).
+4. Therefore a candidate whose durable tip is **below** the committed high-water `L` (a truncated or behind node) is denied by every voter in the intersection and **cannot assemble a majority**. The pre-change bug was that `C` could advertise `learned_committed` (or volatile `applied_lsn`) above its durable tip and thereby satisfy step 3 *without durably holding `L`* — winning, then truncating committed work away. Pinning `cand_lsn = durable_floor(C)` closes exactly that hole.
+
+The retained `learned_committed` term in the *voter* floor (§1b) is the dual guard: even a voter whose own durable tip momentarily lags `L` (e.g. just rejoined) still refuses a candidate below the cluster-committed `L` it learned, so the safety margin does not depend on which majority voted.
+
+#### 4. Liveness (no election livelock) — the most-durable candidate can always win
+
+Claim: the formula is not "too high" — among any available majority, the member holding the **longest durable log** can always be elected; the floor is always satisfiable by some reachable candidate, so there is no bug-339-style infinite election loop.
+
+Argument:
+1. Let `D* = max{ durable_floor(m) : m in an available majority A }`, achieved by member `C*`. `C*` advertises `cand_lsn = D*`.
+2. The committed high-water `L` satisfies `L ≤ D*`: `L` is durable on a majority, that majority intersects `A`, so some member of `A` has `durable_floor ≥ L`, hence `D* ≥ L`.
+3. For any voter `v ∈ A`: `voter_floor_lsn(v) = max(durable_floor(v), learned_committed(v))`. We have `durable_floor(v) ≤ D*` by definition of `D*`. And `learned_committed(v) ≤ L ≤ D*` — a member never *learns* a committed LSN above the true committed high-water (`learned_committed` is a lower-or-equal estimate of `L`, advanced only from majority-acked commits / leader heartbeats). Therefore `voter_floor_lsn(v) ≤ D* = cand_lsn(C*)`, so the comparison `cand_lsn ≥ voter_floor_lsn(v)` **holds for every** `v ∈ A`, and `C*` is grantable by the whole majority.
+4. Hence the floor is always satisfiable by the most-durable reachable candidate ⇒ an election can always complete ⇒ no livelock.
+
+Why this avoids the bug-339 pattern specifically: bug-339 was an *infinite* loop because the RDHUP failover path advertised a **stale `committed_lsn`** that no longer matched the floor the (other) voters demanded — the advertiser claimed a position it could not satisfy against the floor, so it kept losing and retrying. Under the pinned formula **no node advertises a position it cannot durably back** (`cand_lsn = durable_floor`), and the voter floor is bounded above by `D*` (step 3, because both `durable_floor(v) ≤ D*` and `learned_committed(v) ≤ L ≤ D*`). The floor is therefore always met by `C*`. The earlier bug-339 fix pinned the voter floor to `max(applied_lsn, last_known_committed_lsn)`; this task swaps the local-state term from the volatile `applied_lsn` to the durable `durable_floor`. Per §1b we do **not** rest on a raw `durable_floor ≤ applied_lsn` comparison (the two use different counter conventions); instead, the no-livelock guarantee rests solely on the `D*` bound of §4 — `durable_floor(v) ≤ D*` for every reachable voter `v` — so the swapped-in term can never push the voter floor above the most-durable reachable candidate `C*`. It therefore cannot reintroduce a too-high (livelock) floor while it closes the too-low (safety) hole on the advertisement side.
+
+> **The safety/liveness tension is resolved, not papered over.** The "too low ⇒ truncated node wins" failure lives on the **advertisement** axis (what a candidate may claim) and is fixed by `cand_lsn = durable_floor` (§3). The "too high ⇒ livelock" failure lives on the **voter-floor** axis (what a voter demands) and is avoided because the voter floor is bounded above by `D*`, the most-durable reachable candidate's tip (§4). The two fixes act on different sides of the same comparison, so there is no contradiction: §3 raises the *floor for under-durable candidates* without raising it *beyond the best available candidate*.
+
+#### 5. The two required cases
+
+**(a) Truncated-candidate DENIED.** Node `T` restarts; its WAL hit a CRC break at LSN 5, so `replay_wal` returns `RECOVER_TRUNCATED` with `durable_floor(T) = 4` (highest intact replayed LSN). Cluster committed high-water `L = 8` (entries 5–8 are durable on the surviving majority `Q`). `T` becomes a candidate and advertises `cand_lsn = durable_floor(T) = 4` (it **cannot** advertise the stale `learned_committed = 8` it may still hold in volatile state — that is exactly the over-advertisement the formula forbids). Any voter `v ∈ Q` has `durable_floor(v) ≥ 8`, so `voter_floor_lsn(v) ≥ 8 > 4 = cand_lsn` ⇒ every such voter **denies** (§1c). `T` cannot reach a majority ⇒ not elected (Leader Completeness preserved, §3). Independently, the promotion fence (task 4.3) bars `T` from `raft_cb_become_leader` because `persist_recovery_truncated(T)` is true and `durable_floor(T) < L` — so even a degenerate quorum cannot promote it. `T` instead catches up from a healthy peer to `durable_floor ≥ 8`, then becomes both grantable and promotable (Req 2.6 / Boot Policy Decision Table row 3).
+
+**(b) Longest-durable-log STILL ELECTS (no livelock).** Three nodes; the primary committed through **LSN 8**, so `L = 8`. Because committed ⇒ durable on a majority (Req 1/2.x), at least two of the three members hold `durable_floor ≥ 8`; the primary then died. The two survivors are `A` and `B`.
+
+- *Sub-case L=8 is consistent with both survivors:* the committing majority for `L = 8` was some 2-of-3 set. If the dead primary was **not** in that majority, then both survivors `A` and `B` were in it ⇒ both have `durable_floor ≥ 8`. If the dead primary **was** in it, then exactly one of the two acking members survives; say `A` has `durable_floor = 8` while `B` ended cleanly one entry behind at `durable_floor = 7` (it appended/acked 8 against an earlier *uncommitted* round but its flusher had not advanced past 7 at crash — `B` is `RECOVER_CLEAN`, just behind, not truncated). Either way **some survivor has `durable_floor ≥ 8`**, so `D* ≥ 8`.
+
+Take the tighter sub-case (`A=8`, `B=7`), where `D* = 8` achieved by `A`. `A` advertises bare `cand_lsn = durable_floor(A) = 8`. Voter `B`: `voter_floor_lsn(B) = max(durable_floor=7, learned_committed(B) ≤ L = 8)`. Here `learned_committed(B) ≤ 8`; if `B` had learned the `L = 8` commit then `voter_floor_lsn(B) = 8 = cand_lsn(A)` ⇒ `B` grants (equality grants, §1c); if `B` only learned up to 7 then `voter_floor_lsn(B) = 7 < 8` ⇒ `B` also grants. **Either way `B` grants `A`**, `A` self-grants ⇒ majority ⇒ **`A` is elected** (no livelock — consistent with §4 step 3, `voter_floor_lsn(v) ≤ D*`). Symmetrically `B` cannot win if `A` participates: `B` advertises bare `cand_lsn = 7`, and `A`'s `voter_floor_lsn = max(8, learned_committed_A ≤ 8) = 8 > 7` ⇒ `A` denies `B`, steering the election to the most-durable node `A` (§4).
+
+**The dangerous-looking livelock state is UNREACHABLE.** The only way `A` could fail to be grantable by a majority is if some voter `v` had `voter_floor_lsn(v) > cand_lsn(A) = D*` — which by §4 step 3 requires `learned_committed(v) > D*`. But `learned_committed(v) ≤ L` (a node never learns a committed LSN above the true high-water) and `L ≤ D*` (committed ⇒ durable on a majority that intersects the survivors ⇒ some survivor has `durable_floor ≥ L`, so `D* ≥ L`). Hence `learned_committed(v) ≤ L ≤ D*` for every survivor `v`, so no survivor can demand a floor above `D*`, and a two-equal-tip-but-high-`learned_committed` deadlock (both survivors `durable_floor = 5`, both `learned_committed = 8`) **cannot arise when `L = 8` is genuinely committed**: `L = 8` committed forces some survivor to `durable_floor ≥ 8 > 5`, contradicting "both tips = 5". This is precisely the property §4 needs the case to demonstrate.
+
+The elected `A` then computes `safe_committed_lsn` from the vote replies (durable-backed `peer_last_log_lsn` of `A`=8, `B`=7 ⇒ majority-backed safe point), unchanged by this task.
+
+#### 6. Protocol Verification Checklist pass (`src/controller/CLAUDE.md`)
+
+Walking the relevant items under the pinned formula:
+
+- **Freshness gate — candidate `lastLogTerm >= voter` AND `lastLogIndex >= voter`:** HOLDS. The comparison (§1c) is `cand_tag >= voter_floor_tag` (term axis) AND, at equal tag, `cand_lsn >= voter_floor_lsn` (index axis) — exactly the checklist's two-key gate, now with `lastLogIndex` meaning the **durable** tip on both sides.
+- **`safe_committed_lsn` derived from voter replies, not stale ctrlhello:** HOLDS, UNCHANGED. This task does not touch `ha_compute_safe_committed_lsn`; it still reads `votes[].peer_last_log_lsn` (§1d). The floor change makes those replies durable-backed (more conservative), never sourced from a ctrlhello.
+- **`commitIndex` / `committed_lsn` monotonic, contiguous prefix:** HOLDS, UNCHANGED. The floor affects election only; commit advancement is untouched here (it is task 2.x). The freshness floor never writes `committed_lsn`.
+- **WAL truncation on promotion only removes entries above the safe commit point:** HOLDS. `persist_truncate_wal_above(safe_committed_lsn)` is unchanged; the durable-backed (tightened) `safe_committed_lsn` means truncation is, if anything, more conservative.
+- **`durable_lsn` is a prefix watermark (never a per-entry set):** HOLDS and is RELIED UPON — the Leader-Completeness argument (§3) and liveness argument (§4) both use "durable tip ≥ L ⇒ all entries ≤ L durable," which is exactly the prefix-watermark property the checklist asserts. `cand_lsn`/`voter_floor_lsn` are single LSNs (watermarks), not sets.
+- **(post `ha-commit-durability`) a member counts toward the commit majority only at its durably-persisted LSN; acknowledged ⇒ durable on a majority:** the *election-side* analog HOLDS here — a member contributes to a **vote-grant** (and advertises) only at its durably-persisted LSN. The commit-majority arithmetic side is task 2.x; this task makes the freshness/advertisement side durable-backed so the two are consistent.
+- **`votedFor` updated atomically before granting; `currentTerm` monotonic:** UNCHANGED by this task (term/vote bookkeeping in `raft_on_vote_request` is untouched); the floor change only gates *whether* `grant` is reached.
+
+**Concern / caveat (restated):** `raft.tla` validates the freshness/election **logic** above; it does **not** validate that `persist_durable_floor` is genuinely durable (the model assumes a durable log). That durability is verified by tests 3.4 (durable-floor re-derivation on recovery) and 2.x (acknowledged ⇒ durable). No safety/liveness contradiction was found — the formula simultaneously satisfies Leader Completeness (§3) and no-livelock (§4) because the two pressures act on opposite sides of the comparison.
+
 ### Runtime / Test — DurabilityConfig + TestSeam
 
 | Field | Detail |

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

@@ -78,7 +78,7 @@
   - _Boundary: RecoveryIntegrity_
 
 - [ ] 4. Promotion fence and durable-backed freshness
-- [ ] 4.1 (P) Pin the freshness-floor formula and re-verify election safety and liveness
+- [x] 4.1 (P) Pin the freshness-floor formula and re-verify election safety and liveness
   - Define the exact reconciliation of the durable-derived freshness floor against the existing in-memory floor — the durable quantity is the durable **last-log index** (WAL tip), not the commit position — then re-check it against `raft/raft.tla` for Leader Completeness AND liveness (no election livelock) plus the Protocol Verification Checklist (gating item; analysis only, no shared source files).
   - Scope of the raft.tla check: it validates the **election/freshness logic** (the `mlastLogIndex`/`LastTerm` semantics this change touches), which raft.tla models directly. It does NOT validate the *durability* of that floor — raft.tla assumes a durable log (see 5.3). The durability of the WAL-tip derivation is verified by tests (3.4), not by raft.tla.
   - Observable: the pinned formula is recorded and the model/checklist verification passes for both a truncated-candidate-denied case and a longest-durable-log-still-elects case.
@@ -131,3 +131,4 @@
 - 3.2: DECISION-ONLY (no production change). Boot Policy Decision Table recorded in design.md §"Boot Policy Decision Table (task 3.2)" — 7 rows over {verdict CLEAN/TRUNCATED × at-above/below HWM × peer reachable × bounded-catch-up succeeds/fails} + snapshot-sentinel + empty-first-boot. Outcomes: ELIGIBLE / FENCE+CATCH-UP→ELIGIBLE / bounded FATAL. AUTHORITATIVE INVARIANT: never a silent indefinite fence — every truncated/behind member resolves to exactly one terminal (catch-up→ELIGIBLE, or BOUNDED FATAL). Snapshot-sentinel is NEVER FATAL on a legitimate sentinel. 7 skeleton tests in test_commit_durability.c (row1,2,3,4,4b,5,6) are `TEST_IGNORE_MESSAGE`-skipped (PENDING 3.3/4.3) so the suite stays GREEN — they are the RED contract 3.3 (FATAL rows) and 4.3 (fence/eligible rows) turn green. NOTE: pre-existing ASAN leaks in unrelated tests (test_demotion_convergence, ha_start_election_async, ha_rdhup_integration) make the STANDALONE controller_unit_test exit=1, but meson reports Fail:0 — don't be fooled by standalone exit code.
 - 3.3: FATAL branch = pure decision `persist_recover_decision(recover_policy_inputs_t) → recover_decision_t {ELIGIBLE, FENCE, FATAL}` (persist.c) + action `persist_recover_fatal_if_unrecoverable()` which logs the truncation boundary (`durable_floor_lsn`/`cluster_hwm_lsn` + window ms) at ERROR then terminates via `persist_fatal_hook` (extern `void(*)(const char*)`, NULL in prod → `tlog_exit(); abort()`; mirrors `ha_fatal_hook`; tests install it to capture instead of abort). FATAL ONLY for bounded-unrecoverable + NO healthy peer (rows 4/4b); a reachable peer NEVER FATALs (gated behind `if (!healthy_peer_reachable)`); eligibility rows 1/2/6 never FATAL. Bound = FINITE `DEFAULT_RECOVERY_CATCHUP_WINDOW_MS=30000` (persist.h) — keys off the `catch_up_succeeded` bounded-window result, never an indefinite wait. Turned 3.2 skeleton rows 4/4b GREEN + added `test_boot_policy_peer_reachable_never_fatal`; rows 1/2/3/5/6 stay IGNORE (FENCE→ELIGIBLE is 4.3). DEFERRED to 4.3/5.x: wiring this decision into the live boot/promotion path (3.3 is the unit-tested decision + terminate only; no ha.c/cluster.c edits).
 - 3.4: On recovery, `persist_recover` publishes the durable floor = highest intact replayed LSN (recovered WAL tip = `current_lsn-1` after `replay_wal`) into `durable_lsn` via `atomic_store` (ASSIGN, NOT max — so a truncating restart lands at the LOWER intact tip, never over-advertising; this is the crux of Req 2.3). Added `persist_durable_floor()` (NULL-safe thin accessor) as the seam task 4.2 consumes. Floor is the durable LAST-LOG INDEX (WAL tip), NOT the commit position (`committed_lsn`) and NOT a volatile in-memory value. Invariant-safe (recovery/init-time; recovered entries are CRC-validated on-disk = genuinely durable; preserves `durable_lsn <= current_lsn-1`). 4.2 (ha.c/cluster.c) CONSUMES this floor in `ha_vote_self_freshness` — 3.4 only PUBLISHES (persistence-only). Phase 3 (recovery integrity) COMPLETE.
+- 4.1: ANALYSIS-ONLY (no .c/.h). Pinned freshness-floor formula in design.md §"Freshness-Floor Formula (task 4.1)" — THE CONTRACT 4.2 implements. CANDIDATE advertises BARE `cand_lsn = persist_durable_floor(p)` (durable WAL tip) — sites ha.c:3660-3666 (real-vote) + ha.c:3735-3741 (PreVote) must call `persist_durable_floor` DIRECTLY, BYPASSING `ha_vote_self_freshness` on the LSN axis (that fn unconditionally folds in `last_known_committed_lsn` → `max(durable_floor, learned)` = the truncated-candidate-wins bug). VOTER floor = `max(durable_floor, last_known_committed_lsn)` — sites cluster.c:388-395/471-475 + ha.c:2243 keep `ha_vote_self_freshness` with `local_lsn=durable_floor` (the learned_committed backstop stays on the VOTER axis only). Grant iff `cand_tag > floor_tag OR (==tag AND cand_lsn >= floor_lsn)` (term-then-index, matches raft.tla `LastTerm`/`mlastLogIndex |-> Len(log)`). `cand_tag`/`floor_tag` = `max(local_tag, learned_tag)`. SAFETY (Leader Completeness): quorum intersection Q_L∩Q_v ⇒ truncated candidate (durable tip < committed L) denied. LIVENESS (no bug-339 livelock): rests on D* (max durable tip in reachable majority); `durable_floor(v) ≤ D*` and `learned_committed(v) ≤ L ≤ D*`, so the most-durable candidate is always grantable. `safe_committed_lsn` STAYS voter-reply-sourced (unchanged). CAVEAT: raft.tla validates election/freshness LOGIC only, NOT durability (no TLC run — no toolchain; conceptual alignment) — durability verified by 2.x/3.4 tests. (1 remediation: candidate-vs-voter contradiction + §5b example fixed.)