lei.chen/myxce
1
0
Fork 1
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

docs(specs): gap re-validation 2026-06-24 (5 HA/raft specs)

Browse source 
/kiro-validate-gap gap-focused sweep. Per-spec gap analysis written to each
spec's research.md (3 new, 2 appended), grounded in file:line evidence:

- config-upgrade-snapshot (new): real open gap — transport + (term,lsn) marker
  + COW substrate exist, but the entity-bearing snapshot PAYLOAD does not
  (16-byte LSN sentinel). HARD-blocked on entity-bearing-snapshots. Closes
  bug-857. Effort L (XL incl. blocker) / Risk High.
- raft-commit-safety (new): CLOSED — G4 Figure-8 commit (raft.c:733) + G6 vote
  freshness (raft.c:157) done, full sim coverage; the "(0,0) stopgap / broken
  build" concern is stale (build green, real vote tuple at cluster.c:435).
- raft-sim-conformance (new): mostly open — raft.tla is reference-only; only
  1 of 4 invariants (Log Matching) checked in code. Missing PRNG/replay,
  message-fault bag, scheduler, 3 invariant checkers, fault switches,
  scenarios. Effort L / Risk Medium.
- ha-repl-hardening (append): RESCOPE/superseded — 31/33 EARS closed; Req 2.3
  + Req 6 obsolete (CTRL_PRIMARY_COMMITTING removed). Residual: docs only.
- ha-convergence-recovery (append): done bar Task 8 (live E2E); bug-1028
  post-failover availability resolved 2026-06-23.

Skipped ha-elect-ctx-lifecycle (no requirements.md).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MSxwb2Xt5F84ATgiAZnH8V
This commit is contained in:
Rongsong Shen 2026-06-24 10:04:06 +00:00
parent 50b976aedc
commit 05febbc9a7
5 changed files with 570 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

177
.kiro/specs/config-upgrade-snapshot/research.md Normal file
View file

@ -0,0 +1,177 @@
# Gap Analysis — config-upgrade-snapshot (2026-06-24)
## Scope
Make a configuration upgrade install one identical, **entity-bearing** state snapshot
(with the new config embedded) on every member at the config-change marker's
`(term, lsn)` boundary, replacing today's config-push + restart + per-node WAL
replay (which can materialize divergent state — **bug-857**). Closes bug-857.
> **GATING BLOCKER (hard dependency): `entity-bearing-snapshots`.**
> Today snapshots carry **zero entity state** (an LSN sentinel). This spec
> *consumes* an entity-bearing snapshot it cannot produce. It **cannot reach a
> testable GREEN until `entity-bearing-snapshots` lands or is co-scoped.** Every
> "Missing" below traces back to this one absence. See §"Gating Blocker".
---
## Requirement-to-Asset Map
### R1 — Full snapshot at the config-change boundary
| Need | Existing asset (file:line) | Gap |
|------|----------------------------|-----|
| Materialize a snapshot at the marker's `(term,lsn)` | `persist_checkpoint` / `write_snapshot` (`persist.c:1247-1291`) writes a checkpoint snapshot at `checkpoint_lsn` | **Missing** — snapshot is a 16-byte sentinel (`"XCESNAP\0"` + LSN + optional 41-byte config-ref tail); carries no entities. No way to pin it to the marker boundary vs. an arbitrary checkpoint LSN. |
| Snapshot pins identical materialized state | dual-zarray COW: `xzarray_freeze`/`xzarray_thaw` (`zarray.c:695-757`), `test_zarray_cow.c` | **Missing (dormant)** — built + unit-tested but **no production callers**: `kvmgr.c:297` `vfreeze=NULL /* wired in P0-2 */`, `vthaw=NULL`. |
| No member re-derives via replay | upgrade path `do_upgrade_config_with_bytes` (`config_repl.c:1495-1677`); NOTICE at step 9 (`config_repl.c:1641-1655`) | **Constraint (current behavior is the bug)** — step 9 sets `restart_requested`; on restart each node replays its own pre-upgrade WAL under the new config (config-dependent via `lost_and_found`). This is exactly what R1.3 forbids. |
| Transfer out-of-band, not in WAL payloads | `ha_handle_snapshot_chunk` (`ha.c:2424-2515`) + `persist_load_snapshot` (`persist.c:1594`); `OPCode_snapshotTransfer` dispatch-gated (`ha.c:2842/2874/2962`) | **Exists (reusable transport)** — chunked, size-checked, atomic `snap.part`→rename, then `persist_load_snapshot`. Reusable as-is; it only ever moves a sentinel today. |
### R2 — Configuration embedded in the upgrade snapshot
| Need | Existing asset (file:line) | Gap |
|------|----------------------------|-----|
| Embed new config in snapshot (one artifact) | snapshot config-ref tail (`persist.c:1263-1274`, read-back `1581-1590`): `{present, version_tag(8), sha256(32)}` | **Partial / Missing** — only a `{tag, sha}` **reference** is embedded, not the config **bytes** and not the entity state. Need the actual config bytes + entities in one installable artifact. |
| Supersede ha-term-safety R7 config-push for upgrades | R7 out-of-band byte push driven from `config_commit_change` (`config_repl.c:478-510`) | **Missing** — upgrade still uses the R7 interim byte-push path; no branch that delivers config via the snapshot instead. |
| Keep config bytes out of WAL payloads | `WAL_CONFIG_MARKER` is `{version_tag, sha256}` only — `config_marker_encode` (`config_repl.c:40-69`), bytes never in WAL | **Already satisfied** — marker carries no bytes; invariant holds today. |
### R3 — Activation gating
| Need | Existing asset (file:line) | Gap |
|------|----------------------------|-----|
| Don't serve/activate new config until snapshot installed | install-before-activate already structural in `ha_handle_snapshot_chunk` (rename+load on full receipt) | **Partial** — transport installs before load, but there is **no activation gate** tying "config active" to "upgrade snapshot for this `(term,lsn)` installed." Today activation = restart-then-replay. |
| Verify embedded config vs marker content hash | `config_committed_marker` (`config_repl.c:216`) yields `{tag, sha}`; hash-verify-before-activate already the rule for R7 byte push (steering `ha-async-io.md` §per-entry-term) | **Missing for snapshot** — the verify-against-marker logic exists for the byte-push artifact; must be extended to the snapshot-embedded config. |
| Reject + keep retrying on mismatch (no self-terminate) | loud-fence-and-stay-alive invariant (`controller/CLAUDE.md` "Process Lifecycle") | **Constraint** — reject path MUST be a loud serve-fence + retry, never `exit`/`abort`. New code must honor this. |
### R4 — Post-upgrade consistency invariant
| Need | Existing asset (file:line) | Gap |
|------|----------------------------|-----|
| Identical materialized state across members | none — no entity snapshot to compare | **Missing** — depends entirely on R1/R2 landing. |
| Identical active config across members | `config_committed_marker` derives committed config from `(term,lsn)` | **Partial** — config identity is reachable via the marker; **state** identity is not. |
| Invariant holds across upgrade × failover interleave | Raft `(term,lsn)` reconcile + promotion-truncate (`ha-term-safety`, `raft.c`) | **Unknown** — needs design: how a mid-upgrade snapshot interacts with promotion-truncate and catch-up streaming when a leader dies mid-install. |
### R5 — Reproduction and regression
| Need | Existing asset (file:line) | Gap |
|------|----------------------------|-----|
| Reproduce bug-857 divergence (RED) | `waldump` (`testsuite/waldump.{c,h}`), `/xce-test-ha` chaotic-multi-kill soak, planned `snapdump`/`walcompare` (roadmap Hardening §) | **Partial** — waldump exists; `snapdump`/`walcompare` (entity-less-snapshot + WAL-divergence detectors) are **unbuilt** and are the natural assertion tools here. |
| Pass on fixed code | — | **Missing** — fix does not exist yet. |
---
## Gating Blocker — entity-bearing-snapshots (hard, explicit)
This is the single dependency that gates the whole spec.
- **Evidence it's absent:** `write_snapshot` (`persist.c:1247`) and `load_snapshot`
(`persist.c:1555`) handle only magic + LSN + a `{tag,sha}` config-ref tail —
**no job/queue/host/resource entities**. The header comment literally says
*"Full Cap'n Proto serialization is Task 11 when recovery needs to read it back."*
- **Why it blocks:** R1.1, R2.1, R4.1 all require an artifact that carries
materialized entity state. Without it, "install the same snapshot on every member"
delivers an empty sentinel — divergence is unavoidable.
- **What's already paid down (de-risks it):** the COW substrate exists
(`xzarray_freeze`/`thaw`, `zarray.c:695-757`, O(1) freeze, GC-filtered thaw,
unit-tested) and the **transport** is reusable (`ha_handle_snapshot_chunk` +
`persist_load_snapshot`). What's missing is the **payload**: serialize entities
under per-object locks during the freeze window into the snapshot file, and
deserialize them on `load_snapshot`. COW is single-generation/slot-level only —
one consumer owns freeze/thaw (roadmap §entity-bearing-snapshots).
**Consequence for this spec:** requirements/design can proceed, but **tasks cannot
reach implementation** until `entity-bearing-snapshots` is implemented or
co-scoped. `spec.json.blocked_on` already records this.
Also depends on **`ha-term-safety` R7** for the `(term,lsn)` config-change marker
that the snapshot anchors on — that marker machinery **is implemented**
(`config_commit_change`, `config_committed_marker`, persisted config-ref).
---
## Implementation Approach Options
### Option A — Extend the existing checkpoint/upgrade path
Wire `vfreeze`/`vthaw` into `kvmgr`, teach `write_snapshot`/`load_snapshot` to
serialize/deserialize entities, and in `do_upgrade_config_with_bytes` (after the
marker commits, before restart) checkpoint an entity-bearing snapshot at the
marker `(term,lsn)`, embed the config bytes, stream it via `snapshot_transfer_s`,
and gate activation on install. Drop the per-node-replay restart for the upgrade case.
- ✅ Reuses the live transport + COW; minimal new files; one consistent snapshot format.
- ✅ Naturally supersedes the R7 byte-push for upgrades.
- ❌ Bloats `persist.c` snapshot codec and the already-large `config_repl.c` upgrade path.
- ❌ Couples the generic checkpoint snapshot format to upgrade-specific embedding
(config bytes) unless cleanly factored.
### Option B — New "upgrade snapshot" component
A dedicated module owns: materialize-at-marker, embed config, drive transport,
activation gate, and the mismatch fence — leaving `persist.c` to expose only an
entity (de)serialize primitive and `config_repl.c` to call into it.
- ✅ Clean separation; upgrade-specific logic isolated and unit-testable.
- ✅ Keeps `config_repl.c`/`persist.c` from growing further.
- ❌ More wiring across persist ↔ new module ↔ ha transport ↔ config_repl.
- ❌ Risk of a second snapshot-format path diverging from the generic checkpoint one.
### Option C — Hybrid (recommended)
1. **Foundation (in/with `entity-bearing-snapshots`):** wire COW into kvmgr and add
the generic entity (de)serialize to `write_snapshot`/`load_snapshot` — *Option A
style*, shared by recovery + state transfer.
2. **Upgrade layer (this spec):** a thin new helper (Option B style) that, given an
entity-bearing snapshot capability, materializes at the marker `(term,lsn)`,
embeds the config bytes, streams via the existing transport, and adds the
activation gate + hash-verify-vs-marker + loud-fence-on-mismatch. Replace the
step-9 restart/replay for the upgrade case; keep restart/replay as the fallback
only until the foundation lands.
- ✅ Generic snapshot work is reused (recovery, faster rebuild) — not upgrade-only.
- ✅ Upgrade-specific gating/verification stays isolated and testable.
- ✅ Phased: foundation can land + be validated before the upgrade layer flips on.
- ❌ Requires careful coordination across the two specs (format ownership, ordering).
---
## Effort & Risk
| Dimension | Rating | One-line justification |
|-----------|--------|------------------------|
| **This spec alone** (assuming entity-bearing snapshots exist) | **L (1–2 wks)** | Transport + marker + COW exist; new work is materialize-at-marker, config embed, activation gate, hash-verify, mismatch-fence, and the failover-interleave regression. |
| **Including the gating dependency** | **XL (2+ wks)** | `entity-bearing-snapshots` is itself non-trivial (entity serialization under per-object locks, COW wiring, recovery read-back) and must land first. |
| **Risk** | **High** | Hard blocker not yet started; touches consensus-adjacent state at a `(term,lsn)` boundary interleaved with failover (R4.3); snapshot/promotion-truncate/catch-up interaction is unverified; must preserve the never-self-terminate invariant. |
---
## Recommendations for Design Phase
**Preferred approach:** **Option C (Hybrid)** — land entity-bearing snapshots as a
shared foundation (COW into kvmgr + generic entity (de)serialize in
`write_snapshot`/`load_snapshot`), then add a thin upgrade layer that materializes
at the marker, embeds the config, reuses `snapshot_transfer_s`, and adds activation
gating + hash-verify + loud-fence.
**Key decisions to settle in design:**
1. **Spec sequencing** — co-scope `entity-bearing-snapshots` into this spec's
delivery, or hard-gate this spec behind it? (Recommend gate; promote to design
only once the foundation has a tasks plan — matches `roadmap.md`.)
2. **Snapshot format** — one unified entity-bearing format used by both recovery and
upgrade, with the config-bytes embed as an optional section? Avoid a second format.
3. **Materialize-at-marker semantics** — snapshot must reflect state at *exactly* the
marker `(term,lsn)`, not "latest checkpoint." Define how the freeze window aligns
to the committed marker LSN.
4. **Activation gate** — bind "new config active" to "upgrade snapshot for this
`(term,lsn)` installed + hash-verified vs `config_committed_marker`"; mismatch ⇒
loud serve-fence + retry (never exit — `controller/CLAUDE.md`).
5. **Retire the per-node restart/replay** for the upgrade case (step 9,
`config_repl.c:1657-1676`) once the snapshot path is proven.
**Research-Needed (carry forward):**
- Upgrade × failover interleave (R4.3): how does a mid-upgrade entity snapshot
interact with promotion-truncate, `(term,lsn)` reconcile, and ACK-driven catch-up
if the leader dies mid-install? Define the recovery story.
- COW single-generation constraint vs. a checkpoint racing an upgrade snapshot
(only one freeze/thaw consumer allowed — `zarray.c` / roadmap note).
- Build `snapdump` + `walcompare` (roadmap Hardening §) first — they are the RED/GREEN
assertion tools for R5 (entity-less snapshot detection + cross-node WAL/state diff).

53
.kiro/specs/ha-convergence-recovery/research.md
View file

@ -163,3 +163,56 @@ Run this spec's deferred **Task 8** (Option A) on a real-fs cluster with instrum
### Related ### Related
- controller-status `ctrlstatus` is the diagnostic tool here (answers in every role incl. fenced/no-quorum; term/commit/apply visible; responder timestamp for log correlation) — use it to watch the churn live. - controller-status `ctrlstatus` is the diagnostic tool here (answers in every role incl. fenced/no-quorum; term/commit/apply visible; responder timestamp for log correlation) — use it to watch the churn live.
- The failover-exhaustion error rendering crashed (`xce_strerror_r` global-buffer-overflow, bug-827, fixed in libxce `utils.c`) — rebuild before re-observing so the client prints a clean `not-ready` instead of aborting. - The failover-exhaustion error rendering crashed (`xce_strerror_r` global-buffer-overflow, bug-827, fixed in libxce `utils.c`) — rebuild before re-observing so the client prints a clean `not-ready` instead of aborting.
---
## Gap Analysis (re-validation) — 2026-06-24
**Framing**: Third re-validation pass, verified against the on-disk code in this worktree (`raft_tla`). Primary question: is **bug-1028** (post-failover availability — new primary stuck in catch-up loop, not serving) addressed in code or still open, and has the spec's status changed since the 2026-06-18/06-20 audits. Spec phase = `tasks-generated`, all three approval gates green, `ready_for_implementation=true`; roadmap.md:30 marks the spec `[x]` done.
**Verdict**: STILL PARTIAL on the spec's own task list (Task 8 live E2E remains the lone open item), but the **bug-1028 availability concern is RESOLVED in code** — fixed 2026-06-23 in the term-safety domain, NOT in this spec's self-restart machinery. Two of the three differentials raised in the 2026-06-20 live finding have since been closed by sibling specs. The convergence-recovery production code is intact and unchanged in substance; one anchor evolved materially (rejoin self-restart retired by ha-term-safety).
### bug-1028 disposition (the headline question)
bug-1028 = "after a clean failover the new primary never becomes available to serve clients (wait-primary times out); standby[0] never converges." This is **FIXED (2026-06-23)** and the fix is live:
- **Root cause** (per buglog bug-1028): `ha_stream_wal_to_standby` (config_repl.c) stamped each streamed entry's term and the AppendEntries `prev_log_term` from the raw on-disk `hdr.term`, while the standby's `logOk` (`raft_on_append_entries_request`) and the library send path source terms from the authoritative per-LSN index (`persist_entry_term`). The term mismatch made `logOk` reject the catch-up stream forever → standby stuck in catch-up → new primary never reaches commit quorum → never serves. This is a **term-safety / catch-up-correctness** defect, distinct from bug-828 (data safety) and bug-854 (client discovery).
- **Fix verified in code**: `ha_stream_wal_to_standby` now takes `const persist_t *p` (config_repl.h:394-395, config_repl.c:2032-2033); all three former `hdr.term` source sites use `p ? persist_entry_term(p, hdr.lsn) : hdr.term` (config_repl.c:2125, 2143, 2197). Both production callers pass `&c->persist`: the heartbeat-driven streamer (ha.c:2734-2739, explicit "bug-1028" comment) and the ACK-driven continuation (config_repl.c:2283, this spec's Req 5 component). bug-1067 layered on top (leader-current-term AE header @8) for the cross-term catch-up case.
- **Bearing on this spec**: bug-1028's "stuck not serving" is the live manifestation that the 2026-06-20 finding flagged as possibly owned here (differential #1: demotion self-restart churn). It was NOT a convergence self-restart defect — it was the streamer's term source. This spec's Req 5 continuation **consumed the same fix** (its config_repl.c streamer call passes `&c->persist`), so the catch-up component is correct, but ownership of the bug sits with ha-term-safety / raft-log-replication.
### Material drift since the 2026-06-18 audit (Constraint)
The 2026-06-18 map listed Req 2.1-2.3 rejoin reconciliation as MET via `ha_rejoin_reconcile_fn` (a delaymgr truncate+self-restart task). **ha-term-safety task 3.2 RETIRED that** (ha_convergence.c:254-280): `ha_rejoin_reconcile` is now a no-op that only retains the CtrlHelloReply hook for recording the learned boundary. Divergent-suffix reconciliation is now owned by the raft library's term-aware `on_truncate_from` (driven by `raft_on_append_entries_request`'s (term,lsn) log-matching), which truncates exactly the divergent suffix and never a committed-prefix entry — replacing the old term-blind LSN-watermark truncate+restart. Until reconciled, the existing promotion-time fence keeps the member non-promotable WITHOUT self-restarting. This **removes** the rejoin self-restart loop (differential #1 / #2 of the 2026-06-20 live finding) as a churn source.
The **demotion** convergence half (Req 1.x) is UNCHANGED and still active: `raft_cb_become_follower` reads prior role (ha.c:1274), and on PRIMARY→follower disables hooks inline + WARN-logs + calls `ha_schedule_demotion_convergence` (ha.c:1277-1304) → `ha_demotion_convergence_fn` truncates above committed then `ha_self_restart` execv's (ha_convergence.c:144-180, 82-120). So a *demoted ex-primary* still self-restarts; a *rejoining standby* no longer does.
### Requirement-to-Asset Map (delta only — full map in the 2026-06-18 section)
| Req (criteria) | Status now | Note / gap tag |
|---|---|---|
| 1.1-1.7 demotion truncate+self-restart | MET (unchanged) | ha_convergence.c:82-211; scheduled ha.c:1277-1304 |
| 2.1-2.3 rejoin reconcile | MET-by-different-mechanism | **Constraint**: self-restart path retired by ha-term-safety 3.2; now library `on_truncate_from`. Acceptance intent (converge a log running ahead, never lose committed prefix) still satisfied, by a stronger term-aware primitive |
| 2.4 single outcome, never retroactive | PARTIAL | in-process MET; cross-node = Task 8 |
| 3.1-3.4 egress watermark filter | MET (unchanged) | egress.c:47-109; sched.c consumers |
| 5.1-5.3 ACK-driven continuation | MET; **also carries the bug-1028 fix** | config_repl.c:2032+ streamer now term-correct via `persist_entry_term`; single-flight `catchup_inflight[]` ha.h:204 |
| 7.1 re-inclusion at parity | MET (unchanged) | `repl_complete_catchup` |
| 8.1-8.3 quorum transition logging | MET (unchanged) | `ha_log_quorum_transition` ha_convergence.c:340+ |
| 9.1-9.2 degraded service | MET (unchanged) | dispatch-gate allowlist |
| Task 8 live 3-node E2E | OPEN (Missing — env-dependent) | only residual gap |
### Options A/B/C (for closing the residual gap)
- **Option A — Run Task 8 live E2E now** (recommended). Both former E2E blockers are now satisfied: ha-single-leader-role landed (direct CTRL_PRIMARY) AND bug-1028 (the very symptom Task 8 would have hit) is fixed, so a clean failover should now serve. Execute `/xce-deploy-ha` 3-node, run the four scenarios, record converged-outcome + WARN-log assertions. Closes 2.4/8.1/8.2/9.1/9.2 end-to-end. Effort LOW-MEDIUM, Risk LOW. Pairs naturally with `/xce-test-ha` soak which already exists in this worktree.
- **Option B — Ship on unit coverage, defer Task 8 to infra** (current de-facto state). All production code complete + regression-pinned; bug-1028 closed independently. Effort ZERO, Risk LOW-MEDIUM (integration-surface bugs surface in deploy/soak not CI). Consistent with sibling ha-wal-replication 5.4.
- **Option C — Automated multi-process E2E harness in CI**. Out of this spec's scope; the `/xce-test-ha` soak skill is the seed. Effort HIGH, Risk LOW; pays off across the HA family.
### Effort / Risk
- **Closing the spec**: Effort **S** (Task 8 is mechanical scenario scripting, no code/design uncertainty), Risk **Low** (all logic unit-green; bug-1028 — the integration-surface risk that mattered — is already fixed).
- **No new production work is indicated by this re-validation.** The one "change" since 2026-06-18 (rejoin self-restart retirement) was delivered by ha-term-safety, not owed here, and strictly de-risks the availability story.
### Recommendations for design phase
- **Preferred**: Option A. With bug-1028 fixed and ha-single-leader-role landed, run the deferred Task 8 against a real-fs `/xce-deploy-ha` cluster (or piggyback on `/xce-test-ha`) to convert 2.4/8.x/9.x from in-process MET to end-to-end MET, then mark the spec fully complete and the roadmap `[x]` is fully earned.
- **Update spec text (low priority docs)**: annotate Req 2.1-2.3 in requirements/design to reflect that rejoin reconciliation is now the library's term-aware `on_truncate_from` (ha-term-safety 3.2), not a self-restart — so a future reader does not re-derive the retired delaymgr path. The acceptance intent is unchanged; only the mechanism moved.
- **Research-Needed (carry forward)**: when Task 8 runs, capture per-node/per-term quorum transitions, demotion-convergence entries, and committed-LSN advance to confirm (a) no demotion self-restart churn under transient quorum flaps and (b) the rule-out of the overlayfs `fdatasync errno=5` artifact (bug-795) on real fs. These were the open differentials from the 2026-06-20 live finding; bug-1028's fix retires the catch-up-loop differential, leaving only demotion-churn and fsync-env to confirm empirically.

122
.kiro/specs/ha-repl-hardening/research.md
View file

@ -464,3 +464,125 @@ gap remains.
worth scheduling is **Item 1 (doc reconciliation)** — the requirements/design now misdescribe the worth scheduling is **Item 1 (doc reconciliation)** — the requirements/design now misdescribe the
live FSM after `ha-single-leader-role`, which will mislead future readers and any live FSM after `ha-single-leader-role`, which will mislead future readers and any
`/kiro-verify-completion` run that checks prose against code. Items 2–5 are optional hardening. `/kiro-verify-completion` run that checks prose against code. Items 2–5 are optional hardening.
---
# Gap Analysis (re-validation) — 2026-06-24
> Re-validation pass. spec.json `phase=implemented` (all 41 sub-tasks `[x]`). This pass re-verifies
> every EARS criterion against the code **as on disk** after the heavy `ha-term-safety` rework
> (commits 004a40b…b77d412, tasks 1.1–4.3) plus bug-828/991/1028/1060/1067 fixes landed since the
> 2026-06-18 audit. Question answered: does this spec still hold, and how much of it is now owned by
> sibling specs?
## Headline Finding
**Still functionally complete; now LARGELY SUPERSEDED in mechanism, but its data-plane code is the
live load-bearing path.** Two distinct things are true at once:
1. **The control-plane *design* of this spec (Req 2.3 / Req 6: `CTRL_PRIMARY_COMMITTING` role +
60 s `committing_timeout_ms` degraded fallback + COMMITTING→PRIMARY-on-majority) is GONE.**
`grep -rn CTRL_PRIMARY_COMMITTING src/controller/*.{c,h}` → 0 hits; `committing_timeout` → 0 hits.
Removed by `ha-single-leader-role` and replaced by a stronger, continuous mechanism
(own-term WAL_NOOP + `writable_lsn` gate `ha_arm_own_term_gate` ha.c:107/1206; per-op write
quorum `ha_has_write_quorum` ha.c:2781 → `-XCE_ERR_NOT_READY`; vote-derived
`ha_compute_safe_committed_lsn` ha.c:510). This is **documentation drift**, not a functional gap —
identical to the 2026-06-18 finding and **still unactioned**.
2. **The data-plane *code* of this spec (Req 1,3,4,5,7) is intact, hardened, and is the path every
sibling spec builds on.** It was NOT rewritten away — `ha-term-safety` routes through it:
- WAL catch-up payload apply: `ha_apply_single_entry` ha.c:2044 → `persist_wal_write_replicated`
(fsync, idempotent) ha.c:2056 THEN `apply_wal_entry` ha.c:2081 (entity restore). Config markers
also flow here (ha.c:2168). Header-only application remains gone.
- Batched streaming: `send_wal_batch` config_repl.c:2005, `WAL_STREAM_BATCH_ENTRIES`=256 /
`_BYTES`=64 KB (config_repl.c:1981-1982); batch flush loop config_repl.c:2071-2173.
- Snapshot raw payload: `ha_send_snapshot_to_standby` config_repl.c:2425 →
`xce_snapshot_chunk_req_raw` config_repl.c:2496 (real bytes).
- Per-standby convergence: `ha_process_standby_state` ha.c:2592 (sets
`standby_reported_tag/_lsn/_converged`, ha.c:2600-2607); reset on term entry ha.c:1115-1117;
fed from `OPCode_reply` stateReport at ha.c:4620.
- `safe_committed_lsn` (this spec's Flow 0, tasks 4.1/4.2) is *explicitly cited by code* as
ha-repl-hardening: ha.c:940 "Task 4.1 (ha-repl-hardening)".
bug-1028 (FIXED 2026-06-23) was inside this very streaming path (`ha_stream_wal_to_standby` gained
a `const persist_t *p` param) — confirming the path is live and maintained, not dead.
## Which sibling spec now owns what
| Concern | Originating in ha-repl-hardening | Now owned / superseded by |
|---|---|---|
| Heartbeat stateReport (Req 1) | yes | retained as-is; consumed by `ha-heartbeat-committed-propagation` (adds committed+term stamp) |
| Per-standby convergence tracking (Req 2.1/2.2/2.5) | yes | retained as-is |
| Majority threshold `n_peers/2` (Req 2.3) | yes | reconciled + **absorbed** into `ha_has_write_quorum` / `safe_committed_lsn` (raft-commit-safety, ha-term-safety) |
| WAL catch-up payload apply (Req 3) | yes | retained; now also drives `ha-term-safety` config-marker apply + bug-991 lsn-advance fix |
| Snapshot transfer (Req 4) | yes | retained as-is |
| Batch WAL transfer (Req 5) | yes | retained; bug-1028 hardened the streamer signature |
| COMMITTING gate (Req 6) | yes | **SUPERSEDED & DELETED** by `ha-single-leader-role` (own-term gate) + `ha-commit-durability` (durable-commit fence) |
| Flow 0 safe commit point (tasks 4.1/4.2) | yes | retained; extended by `raft-commit-safety` (Figure-8) + `ha-term-safety` (per-entry term, (term,lsn) reconcile) — the LSN-only safe point is now term-aware upstream |
## Requirement-to-Asset Map (delta vs 2026-06-18 — only changes noted)
All 31 CLOSED criteria from 2026-06-18 remain CLOSED (assets re-verified, line numbers shifted +~860
in ha.c / +~560 in config_repl.c due to ha-term-safety growth; spot-checked above). No regression.
| Req / AC | Change since 2026-06-18 | Status |
|---|---|---|
| **3.x** payload apply | Path unchanged in shape; bug-991 fix made the three live-apply setters advance applied_lsn to the LAST-held LSN (correctness hardening). | CLOSED (hardened) |
| **5.x** batch streaming | bug-1028 added `const persist_t *p` to `ha_stream_wal_to_standby` (off-by-one / hdr-source fix). | CLOSED (hardened) |
| **Flow 0** safe commit | Now also gated by ha-term-safety per-entry term + bug-1060 promotion-truncate floor `max(safe_lsn,durable_tip)` (prevents new leader truncating its own committed log) + bug-1067 AE header-term separation. | CLOSED (strengthened upstream) |
| **6.4 / 7.5** COMMITTING timeout/WARN | Still OBSOLETE (no COMMITTING). | N/A (superseded) |
**Score: 31/33 CLOSED, 2 OBSOLETE-by-supersession (6.4, 7.5). Effective 33/33. No CRITICAL/HIGH
functional gap. Unchanged from 2026-06-18, now re-confirmed post ha-term-safety.**
## Disposition: RESCOPE (close as data-plane-complete + supersede the control-plane prose)
This spec should **not** be reopened for new feature work and should **not** be deleted. Recommended
disposition:
- **Keep `phase=implemented`.** Every acceptance criterion is satisfied or satisfied-by-replacement.
- **CLOSE-as-superseded the control plane (Req 2.3 + Req 6 entirely).** Their mechanism was
deliberately replaced. Carry a one-line "SUPERSEDED by ha-single-leader-role / ha-commit-durability"
banner on Req 6 and on the Introduction's COMMITTING references.
- **RETAIN the data plane (Req 1,3,4,5,7 + Flow 0) as the canonical owner.** No sibling spec
re-implements WAL-catch-up payload apply, batching, snapshot transfer, or stateReport — they all
consume this code. If anything, this spec is now the *foundation*, not the obsolete layer.
The 2026-06-09 project-memory note ("data plane MISSING, critical, bugs 335-338") is **stale** — it
was closed by the reopened 7.x payload series (audited 2026-06-18) and is unaffected by later work.
## Residual / Deferred (all LOW, none blocking — unchanged + re-confirmed)
1. **Documentation drift (HIGH-doc, LOW-code) — STILL OPEN.** requirements.md Req 6 + Introduction +
design.md describe `CTRL_PRIMARY_COMMITTING` / `committing_timeout_ms` / 60 s degraded fallback,
none of which exist. This is the *only* item worth scheduling. A `/kiro-verify-completion` run that
checks prose-vs-code will flag Req 6 falsely.
2. **Req 5.2 "configurable" batch size** is compile-time `#define`, not `ha_config_t`. Defensible.
3. **`ha_compute_oldest_wal_lsn`** opendir/readdir per heartbeat reply per standby. Perf-only.
4. **Direct unit tests** for `ha_process_standby_state` / `ha_evaluate_repl_action` /
`ha_send_snapshot_to_standby` — coverage is integration-weighted (test_config_repl.c,
test_convergence_verification.c), not absent.
5. **E2E entity-state assertion** (submitted job visible on promoted standby post-failover) — the
live HA soak (`/xce-test-ha`) now exercises this end-to-end, partially discharging the gap; a
pinned unit/E2E assertion is still nice-to-have.
## Effort / Risk for the one schedulable item
| Item | Option | Effort | Risk |
|---|---|---|---|
| Doc reconciliation: remove COMMITTING from requirements.md Req 6 + Introduction + design.md; document own-term gate + write-quorum + safe_committed_lsn as the real Req 6 mechanism; cross-link ha-single-leader-role / ha-commit-durability / ha-term-safety | **A (recommended):** rewrite Req 6 + Introduction (S, 0.5–1d). **B:** one-line SUPERSEDED banner (XS, <0.5d). | A: S · B: XS | Low (docs only) |
## Recommendation
1. **No open implementation work.** Spec is functionally complete and is the live owner of the HA
replication data plane. Mark project-memory note (2026-06-09 "data plane MISSING") as resolved.
2. **Schedule only the doc reconciliation (Residual #1).** It has been flagged in two prior audits
(2026-06-09 doc-drift, 2026-06-18 Item 1) and remains unactioned. Either rewrite Req 6 (Option A)
or banner it (Option B). Everything else is optional hardening.
3. **Treat this spec as RESCOPED:** control plane CLOSED-as-superseded; data plane RETAINED-as-owner.
## Research Needed
- None new. Prior research items (typemap `Data` encoding, snapshot wire format, ownership boundary
with ha-config-bootstrap task 7.6 / live `repl_broadcast`) were all resolved by the payload series
and ha-term-safety task 3.4 (`repl_broadcast` now carries leader term, term-0 live send retired).

53
.kiro/specs/raft-commit-safety/research.md Normal file
View file

@ -0,0 +1,53 @@
# Gap Analysis — raft-commit-safety (2026-06-24)
> Scope: the **commit-safety (G4 Figure-8 commit advance) + election-freshness (G6 `(lastLogTerm,lastLogIndex)` vote/PreVote)** half of `raft/raft.tla`, in `src/lib/raft` only. Boundary owns the library entry points + callbacks; the controller barrier/durability, config markers/snapshot, and conformance harness are owned elsewhere (`ha-term-safety`, `raft-sim-conformance`). HARD dep: `raft-log-replication`.
## Executive Summary
This spec is **DONE**. All tasks 1.1–8.1 are `[x]` in `tasks.md`, and the actual code confirms it: the library half (G4 commit-advance + G6 vote/PreVote freshness) is implemented in `src/lib/raft/{raft.h,raft.c,raft_sim.c}`, fully tested in `src/lib/testsuite/test_raft.c`, and **already consumed by the controller** via the `ha-term-safety` adapter. The historical "(0,0) stopgap disables G6 / build broken" state recorded in project memory is **stale** — it has been superseded: the controller build is green (later commits `bug-1060`/`bug-1067` build on top of it), the wire schema carries `last_log_term`/`last_log_index`, and `cluster.c` feeds the real candidate tuple into `raft_on_vote_request`. **No unsafe stopgap remains in this spec's surface.**
## Requirement-to-Asset Map
| Req | Asset (file:line) | Status |
|-----|-------------------|--------|
| **R1** Library-owned `commit_index` + current-term advance (G4) | `raft.h:62` (`commit_index`), `raft.h:199` (`initial_commit_index`), `raft.c:733` `raft_advance_commit` — leader-only `-EPERM` (`raft.c:738`), `Max(agreeIndexes)` scan (`raft.c:740`), current-term gate before advance, monotonic | **DONE** |
| **R2** `on_commit_advanced` callback triggers barrier (no durability in lib) | `raft.h:169` decl (REQUIRED), `raft.c:58` NULL-check `-EINVAL` at init, `raft.c:780` fired once on strict advance; AE-reply does not advance (`test_ae_reply_does_not_advance_commit`) | **DONE** |
| **R3** `(lastLogTerm,lastLogIndex)` binding-vote freshness (G6) | `raft.c:157` `raft_log_ok`, applied in `raft_on_vote_request` (`raft.c:234`) BEFORE `on_vote_eligible`; extended sig `raft.h:267` | **DONE** |
| **R4** Same freshness on PreVote, side-effect-free | `raft_on_pre_vote_request` (`raft.c:291` `raft_log_ok`), no state mutation / no `on_persist`; sig `raft.h:329` | **DONE** |
| **R5** Preserve sync commit barrier + durability as policy | Library returns status codes only; barrier remains in controller `commit.c`/`ha.c`; `on_commit_advanced` is trigger-only | **DONE** |
| **R6** Deterministic Figure-8 + Leader Completeness + freshness sim | `test_raft.c`: `test_advance_commit_figure8_hold_previous_term` (2765), `test_sim_7_1_figure8_commit_refusal` (4095), `test_sim_7_2_leader_completeness_across_changes` (4161), `test_sim_7_3_freshness_gate_lexicographic` (4245), `test_sim_7_4_on_commit_advanced_trigger_semantics` (4345); all `RUN_TEST`-registered | **DONE** |
No gaps tagged Missing/Unknown within the spec boundary.
## Downstream Consumption (out-of-scope here, but verified present)
The controller integration that routes the WAL/commit barrier through the library is owned by **`ha-term-safety`**, and it is wired:
- **Wire schema**: `src/schema/controller.capnp:833-834` adds `lastLogTerm @4` / `lastLogIndex @5` to the RequestVote message.
- **Vote path**: `src/controller/cluster.c:395-396,435-436` reads the candidate's `last_log_term`/`last_log_index` from the wire and passes the real tuple into `raft_on_vote_request(...)`. **No `(0,0)` stopgap** — the application freshness gate (`config_tag`/`durable_floor`) is layered IN ADDITION to the library `logOk`, not in place of it.
- **PreVote path**: `cluster.c:489,533` plumbs the same tuple into `raft_on_pre_vote_request`.
- **Commit source**: `src/controller/ha.c:1686` `ha_cb_commit_advanced_stub` (name is legacy — it is a real, wired callback) calls `commit_set_raft_commit_index(...)`, making the library's current-term-gated `commit_index` the steady-state commit SOURCE; the term-blind `ha_compute_safe_committed_lsn` is no longer the steady-state driver. Callback table at `ha.c:1741`.
- **Build state**: green. Later commits `61e1391 fix bug-1060 bug-1067` and the `ha-term-safety` series build on top of the extended vote signature, confirming the earlier "vote-signature extension BROKE cluster.c" condition is resolved.
## Options (retrospective — for any follow-up only)
- **Option A — Extend existing (CHOSEN, complete).** The library log/election core already existed (`raft-library` + `raft-log-replication`); this spec extended `raft.{c,h}` with one new action, one callback, and two freshness args. Trade-off accepted: keeps everything in the pure library, no new TU. ✅ minimal surface, leverages existing callback contract.
- **Option B — Library owns `logOk` (CHOSEN for freshness plumbing).** Vote/PreVote signatures gained `cand_last_log_term`/`cand_last_log_index` and the library now owns the `logOk` decision (formerly the caller/dispatcher's). This is the "freshness-decision locus move" called out in R5.4. ✅ single authoritative predicate (`raft_log_ok`) shared by both paths.
- **Option C — Hybrid / new component.** Not needed; rejected implicitly. A separate commit module would have split the `commit_index` invariant away from the log model it depends on.
## Effort & Risk
- **Effort: S (already delivered).** Remaining work for *this spec* = none. Verification re-run only.
- **Risk: Low.** Pure, synchronous, deterministic library code with full simulator coverage (Figure-8 hold/release, Leader Completeness across forced leader changes, lexicographic freshness, trigger-fire-count). No I/O, no threads; controller integration validated downstream by `ha-term-safety` live soak.
## Recommendations for design phase
- **No further design needed for raft-commit-safety.** Treat as closed; G4/G6 of bug-851 are addressed at the library layer.
- **Carry-forward (owned elsewhere, not this spec):**
- `ha-term-safety` owns the controller wiring already in place — keep the bug-828/854/991/1060/1067 follow-ups there.
- `raft-sim-conformance` owns the full TLC trace-check harness (Leader Completeness oracle) — this spec only seeds the deterministic sim assertions it will consume.
- **Stale-memory correction (research item closed):** the project-memory note "vote-signature extension BROKE the controller build (cluster.c); (0,0) stopgap unsafe—disables G6" is **no longer current**. Verified 2026-06-24: build green, real tuple wired, no stopgap. Update the memory entry accordingly.
## Research-Needed
- None within this spec's boundary. (Open HA items — bug-828 residual / bug-854 client discovery — are tracked under `ha-term-safety`, not here.)

165
.kiro/specs/raft-sim-conformance/research.md Normal file
View file

@ -0,0 +1,165 @@
# Gap Analysis — raft-sim-conformance (2026-06-24)
Analyzed per `.claude/skills/kiro-validate-gap/rules/gap-analysis.md`. Scope: a single
feature — an in-process, deterministic, seed-driven harness that drives N `src/lib/raft`
library instances through `raft.tla`-`Next`-equivalent transitions and asserts the four
Raft safety invariants every step (the "use the verified spec as an oracle" payoff;
acceptance bar = catch a bug-851-class divergence on a deliberately-broken build, pass on
the correct build).
## 1. Current State Investigation
### Authoritative spec
- `raft/raft.tla` — Diego Ongaro's canonical Raft (abstract spec; ends `raft.tla:471`).
All `Next` actions present and located: `Restart` (167), `Timeout` (178),
`RequestVote` (190), `AppendEntries` (204), `BecomeLeader` (229), `ClientRequest` (246),
`AdvanceCommitIndex` (259), `Receive` (421) with `UpdateTerm` (406) and
`DropStaleResponse` (415), `DuplicateMessage` (443), `DropMessage` (448),
`Next` disjunction (454). The `.tla` file carries NO embedded invariant `THEOREM` block;
the four safety invariants (Election Safety, Log Matching, Leader Completeness, State
Machine Safety) are tracked prose-side in `src/controller/CLAUDE.md`. **No TLC config
(`*.cfg`), no `tla2tools`/TLC tooling exists in-repo** — the spec is a reference
document, not a model-checked artifact today.
### How the C library is checked against raft.tla today
- **It is not, automatically.** Conformance is enforced by hand: `src/controller/CLAUDE.md`
holds the TLA+ variable→code and action→code mapping plus a manual "Protocol
Verification Checklist." There is no trace generation, no invariant checker that runs
per-step, and no randomized simulation that asserts the four invariants.
- `src/controller/raft/` does **not** exist; the library lives at `src/lib/raft/`
(`raft.c` 33 KB, `raft.h` 30 KB, `raft_sim.c` 18 KB). Per `src/controller/CLAUDE.md`,
the controller's `raft.c` was election-only; the full election+log+commit protocol now
lives in the **library** `src/lib/raft` (deps `raft-log-replication` +
`raft-commit-safety` landed — callbacks present and exercised in `test_raft.c`).
### Existing harness (`src/lib/raft/raft_sim.c`, `XCE_TESTING`-gated)
Already present (the election + partial log layer it was grown to for the dependency
specs), all consuming published library entry points verbatim:
- `raft_sim_init`, `raft_sim_deliver_pending` (vote RPC routing via
`raft_on_vote_request`/`_reply`), `raft_sim_deliver_append_entries` (AE routing via
`raft_on_append_entries_request`/`_reply`), `raft_sim_start_all_elections`,
`raft_sim_fire_timeout`, `raft_sim_partition`, `raft_sim_advance_commit`
(`raft_advance_commit`), `raft_sim_restart_node` (models Restart, preserves persisted
term/votedFor/log/commit_index), and **one** invariant checker:
`raft_sim_check_log_matching` (`raft_sim.c:424`).
- In-memory adapter callbacks already back the four log callbacks + `on_commit_advanced`
into per-node `raft_sim_node_t` (`log[]`, `log_count`, `commit_index`,
`commit_advanced_count`, `trace_buf`). The library holds no entry bytes — the simulator
owns storage, exactly as the dependency design anticipated.
- `raft.h` `XCE_TESTING` section (`raft.h:432+`) already defines `raft_sim_rpc_t`,
`raft_sim_entry_t`, `raft_sim_ae_t`, `raft_sim_node_t`, `raft_sim_cluster_t`, and bounds
`RAFT_SIM_MAX_NODES=8`, `RAFT_SIM_MAX_LOG=64`, `RAFT_SIM_ENTRY_LEN=16`,
`RAFT_SIM_MAX_AE=64`.
- `test_raft.c` (7011 lines) already exercises election + AE + commit + a
hand-built partition/catch-up convergence path and both directions of
`raft_sim_check_log_matching` (pass-on-converged / fail-on-divergence).
### All library entry points the harness needs already exist in `raft.h`
`raft_log_append`, `raft_send_append_entries`, `raft_advance_commit`,
`raft_on_append_entries_request`/`_reply`, `raft_on_vote_request`/`_reply`, `raft_init`,
`raft_start_election`, `raft_on_election_timeout`, `raft_snapshot` — all declared.
**Constraint:** `raft_snapshot_t` (`raft.h:69-76`) exposes term/role/voted_for/votes only —
NOT log or commit_index. So Election Safety can read from `raft_snapshot`, but Log
Matching / Leader Completeness / State Machine Safety MUST read the harness-owned
in-memory `log[]`/`commit_index`/`applied[]` (Req 3.6 "observable per-node state only" is
satisfied by the in-memory mirror, not by reaching into `raft.c`).
### Spec phase state
`spec.json` = `tasks-generated`, all 3 gates auto-approved (`-y`), `ready_for_implementation`.
`tasks.md` has 8 task groups (1.1–8.1); **every task box is unchecked `[ ]`** — none of
the conformance machinery is implemented. The brief/requirements/design are complete and
internally consistent.
## 2. Requirement-to-Asset Map (gaps tagged Missing / Unknown / Constraint)
| Req | Need | Existing asset | Gap |
|-----|------|----------------|-----|
| 1.1–1.6 Deterministic seeded driver | Seeded PRNG (SplitMix64), `(N,seed)` byte-identical replay, message bag, action trace buffer, no threads/sockets/wall-clock | `raft_sim_init` (no seed/PRNG); synchronous already | **Missing**: PRNG, `seed`, `raft_sim_conformance_init`, bag (`bag[]`/`bag_count`), trace buffer, `raft_sim_run` replay. Constraint: must extend the existing `raft_sim_cluster_t`/`_node_t`, not rewrite. |
| 2.1–2.6 Drive `raft.tla` Next actions via library entry points | `Restart`/`Timeout`/`RequestVote`/`BecomeLeader`/`ClientRequest`/`AppendEntries`/`AdvanceCommitIndex`/`Receive`(UpdateTerm+DropStaleResponse)/`Duplicate`/`Drop` through published API | Vote+AE delivery, restart, advance-commit, partition all wired verbatim to library handlers | **Missing**: unified `raft_sim_step` scheduler selecting only *enabled* actions; `ClientRequest` via `raft_log_append`; bag-based `Duplicate`/`Drop` (current delivery drains a queue, no per-message drop/dup/reorder). UpdateTerm/DropStaleResponse are already inside the library handlers (consumed, not re-modeled). |
| 3.1–3.6 Per-step assertion of all four invariants | Election Safety, Log Matching, Leader Completeness, State Machine Safety; first-failure halt; observable-state-only | Only `raft_sim_check_log_matching` exists | **Missing**: `raft_sim_check_election_safety`, `_leader_completeness`, `_state_machine_safety`, `_check_all` (first-failure composer); `applied[]` per-node state machine view. |
| 4.1–4.5 Targeted adversarial scenarios | partition/heal, restart-churn, drop/dup/reorder, Figure-8, stale-rejoin (bug-851 G5) | A hand-built partition/catch-up test exists in `test_raft.c` (not a reusable named scenario) | **Missing**: 5 named `raft_sim_scenario_*` entry points asserting all four invariants throughout. |
| 5.1–5.4 Failure-trace capture/replay | seed+N+failing-invariant+ordered action trace dump; quiet-on-success; replay reproducibility | per-node `trace_buf` (string events only, not structured actions) | **Missing**: structured `raft_sim_action_t` trace + `raft_sim_dump_trace`; replay tie-in to `raft_sim_run`. |
| 6.1–6.4 CI-runnable target | M-seed sweep + all scenarios in `src/lib/testsuite`, ASAN/UBSAN-clean, bounded runtime | `test_raft.c` already builds/runs under `XCE_TESTING` + sanitizers | **Missing**: the sweep harness + bounds; mechanics (test entry point, sanitizer build) already exist. Low-risk. |
| 7.1–7.4 Deliberately-broken-build negative test | compile-time fault switches (`RAFT_SIM_BREAK_TERM_STAMP`, `RAFT_SIM_BREAK_TRUNCATE`) confined to adapter; both-directions assert | none | **Missing**. **Constraint**: switches must live in the *adapter* (`raft_sim.c` callbacks), never `raft.c` — the boundary forbids touching protocol code. This is the acceptance teeth. |
| 8.1–8.3 Optional TLC-consumable trace export | spec-named machine-readable record stream, off by default | none | **Missing** (optional `[ ]*`, deferred). **Unknown/Research**: no TLC tooling in-repo to actually consume it — export format can be written but cross-checking against `raft.tla` via TLC is unproven. |
### Cross-cutting findings
- **Currently CHECKED against raft.tla (in code):** Log Matching only (one checker,
`raft_sim.c:424`), and only on hand-driven clusters — not per-step, not over randomized
runs. Election Safety / Leader Completeness / State Machine Safety are **UNCHECKED in
code** (asserted only by prose checklist). Of the `Next` actions, Restart / Timeout /
RequestVote / AppendEntries / AdvanceCommitIndex / Receive are *driven* by the existing
sim; `ClientRequest`, per-message `Duplicate`/`Drop`/reorder, and a unified
enabled-action scheduler are **not yet driven**.
- **raft.tla does NOT model durability** (restores `log` intact on Restart,
`raft.tla:165-174`) — so the harness, like the spec, cannot and should not assert the
commit-durability invariant (that rests on `ha-commit-durability` tests). This correctly
scopes the harness to the four safety invariants only. Confirmed against memory.
## 3. Implementation Approach Options
### Option A — Extend `raft_sim.c` / `test_raft.c` in place (spec's chosen path)
Add PRNG, bag, action trace, three new checkers + composer, `raft_sim_step`/`_run`, five
scenarios, fault switches — all inside the existing `XCE_TESTING` sim section and test
file. Reuse `raft_sim_node_t`/`_cluster_t` (extend with `bag[]`, `applied[]`, `seed`,
`trace[]`).
- ✅ Matches the spec boundary exactly (owns `raft_sim.c` + `raft.h` XCE_TESTING + `test_raft.c`); reuses the verbatim-library-entry-point pattern already proven by the dependency specs; no protocol change; sanitizer/CI plumbing already in place.
- ❌ `raft_sim.c` grows well past the existing 18 KB (toward the 800-line guideline ceiling); `test_raft.c` is already 7011 lines.
### Option B — New `raft_conformance.c` / `test_raft_conformance.c` modules
Put the harness (PRNG, bag, scheduler, checkers, scenarios, fault switches) in dedicated
files; keep `raft_sim.c` as the thin election/AE adapter.
- ✅ Honors "many small files"; isolates the oracle from the dependency-era sim; easier to read/maintain; keeps `test_raft.c` from ballooning further.
- ❌ Deviates from the spec's stated file boundary ("owns `raft_sim.c` … ONLY"); needs a meson build wiring change and a boundary-note update; minor duplication of the in-memory adapter.
### Option C — Hybrid (recommended)
Keep the in-memory adapter callbacks, bag, PRNG, and the **four checkers** in
`raft_sim.c`/`raft.h` (they are genuinely "simulator" primitives and reuse existing node
state). Lift the **scheduler + five scenarios + M-seed sweep + negative test** into a
new `test_raft_conformance.c` (or a clearly-fenced section) so `test_raft.c` does not grow
unbounded. Fault switches stay in `raft_sim.c` (adapter) per boundary.
- ✅ Best file-size/cohesion balance; preserves the "harness drives only published entry points" boundary; checkers stay reusable; the heavy scenario/sweep code is isolated.
- ❌ Splits ownership across two test files — needs a one-line boundary amendment in `tasks.md`/`design.md` (Allowed Dependencies already permit a new test file under `src/lib/testsuite`).
## 4. Effort & Risk
- **Effort: L (1–2 weeks).** Eight task groups; the hard parts are the seeded scheduler
with enabled-action selection (4.2), deterministic byte-identical replay (4.4/1.6), the
three new invariant checkers (3.1/3.3/3.4) and the bug-851 Figure-8 / stale-rejoin
scenarios (5.4/5.5). Substantial scaffolding already exists (adapter callbacks,
partition, restart, Log Matching, AE/vote delivery), which pulls it down from XL.
- **Risk: Medium.** Mitigants: all library entry points exist and are stable; deps landed;
no protocol change; synchronous/no-I/O design removes concurrency risk; the negative
test self-validates checker sensitivity. Residual risk: (a) determinism leaks (pointer
values / iteration order in action selection) — must be audited (Req 1.2); (b) the
Figure-8 and stale-rejoin scenarios must be precise enough to actually exercise the
bug-851 mechanism (else the oracle's "teeth" are blunt); (c) keeping fixed-size bounds
(`RAFT_SIM_MAX_*`) large enough for randomized runs without blowing the CI time/ASAN
budget. The optional TLC export (Req 8) is **Unknown** — no in-repo TLC to validate it.
## 5. Recommendations for Design Phase
- **Preferred approach: Option C (hybrid)** — checkers + bag + PRNG + fault switches in
`raft_sim.c`/`raft.h`; scheduler + scenarios + sweep + negative test in a new
`src/lib/testsuite/test_raft_conformance.c`. Amend the `tasks.md`/`design.md` file
boundary with that one new test file (design "Allowed Dependencies" already permits it).
If strict adherence to the stated single-file boundary is required, fall back to
Option A and accept the file-size growth (flag a `clang-format`/size exception).
- **Key decisions to lock:** (1) PRNG = SplitMix64 inlined, single `cluster.seed` source —
forbid any wall-clock/address input (Req 1.2); (2) invariant checkers read ONLY
harness-owned in-memory state (`log[]`/`commit_index`/`applied[]`) + `raft_snapshot`
(role/term) — never `raft.c` internals (Req 3.6); (3) `ClientRequest` drives
`raft_log_append` on a forced leader; `Duplicate`/`Drop`/reorder mutate ONLY the bag
(Req 2.5); (4) fault switches confined to adapter callbacks, default-off, never set in
the default CI run (Req 7.3).
- **Research items to carry forward:** (a) **TLC consumability (Req 8)** — no
`tla2tools`/`.cfg` exists in-repo; decide whether to add TLC tooling or keep Req 8 as a
documented-format-only deferral. (b) confirm `RAFT_SIM_MAX_LOG=64` / step bounds are
large enough for randomized convergence yet inside the ASAN/UBSAN CI budget (Req 6.4).
(c) verify the existing per-node `applied[]`/state-machine view needs adding (not present
in current `raft_sim_node_t`) for State Machine Safety (Req 3.4).
- **Dependency watch:** harness consumes `raft-log-replication` + `raft-commit-safety`
callback signatures verbatim; per design "Revalidation Triggers," any change to
`on_persist_entry`/`on_get_entry_term`/`on_send_append_entries`/`on_truncate_from`/
`on_commit_advanced` or the `(lastLogTerm,lastLogIndex)` freshness contract re-validates
this spec.