next_base_seq: exhaustion must be representable — saturation returned a minted coordinate

.claude/board/EPIPHANIES.md

@@ -1,3 +1,142 @@
+## 2026-08-31 — E-A-REVIEW-REMEDY-HAS-A-SHELF-LIFE-1 — the same edit was correct in one PR and a violation in the next
+
+**Status:** FINDING — caught by CodeRabbit on PR #1123, one PR after it raised
+the finding whose remedy it then had to reject.
+**Confidence:** measured — the identical one-line edit, applied twice.
+
+CodeRabbit flagged MD018 on PR #1122: an `EPIPHANIES.md` line beginning `#1120`
+reads as a heading. Valid, and at that moment the entry was **new and
+unmerged**, so editing it was ordinary drafting.
+
+The fix landed one PR later. By then the entry had **merged to `main`**, and
+`CLAUDE.md`'s governance rule applies to it:
+
+> The governance files are APPEND-ONLY (prepend new entries; never edit past
+> entries except the `Status:` / `Confidence:` lines).
+
+So the same characters, in the same place, for the same reason, changed from a
+lint fix into a violation of the ledger's core property — and CodeRabbit
+correctly flagged its own earlier remedy. Reverted; the MD018 warning stands,
+because a cosmetic lint does not outrank append-only. (An append-only file's
+whole value is that a reader can trust an old entry reads as written; a
+"harmless" edit is exactly the kind that erodes that, since nobody objects to
+any single one.)
+
+**The generalizable bit: a remedy is scoped to the state of the tree when it
+was proposed.** Findings age well — the defect is either real or not — but
+remedies age badly, because they assume where the code sits. Between the
+finding and the fix, this entry crossed a boundary (unmerged → merged) that
+changed which rules governed it, and nothing in the finding text could have
+said so.
+
+**Consequence, cheap to apply:** before acting on a review comment from an
+EARLIER PR, re-check what the target is *now* — merged or not, moved, already
+fixed, or governed by a different rule than when the comment was written. Same
+family as this session's other silence-shaped errors: the check was right, the
+world moved, and only re-reading the world catches it.
+
+---
+
+## 2026-08-31 — E-THE-SUPERSESSION-GATE-WATCHED-TWO-OF-ITS-FOUR-INPUTS-1
+
+**Status:** FINDING — mechanical, fixed in the same PR that exposed it.
+**Confidence:** measured — `supersession_index.py` read against
+`.github/workflows/supersession-index.yml`, plus PR #1123's actual check list.
+
+`CLAUDE.md` says the generator reads *"`.claude/plans/`, `crates/`,
+`.claude/v3/COMPONENT-MAP.md`, **and the board itself**"*, and even warns that
+the workflow's error text names only the first three and "will mislead the same
+way". It does mislead — and so did the workflow's own `paths:` filter, which
+watched **two of the four inputs**:
+
+| generator input | source | watched by the gate |
+|---|---|---|
+| `.claude/v3/COMPONENT-MAP.md` | `:20` | yes |
+| `.claude/plans/*.md` | `:47` | yes |
+| `.claude/board/entries/*.md` + `EPIPHANIES.md` | `:48-49`, counted at `:85` | **no** |
+| `crates/**` | `:27`, per symbol | **no** |
+
+**Measured, not inferred:** PR #1123 prepends an `EPIPHANIES.md` entry citing
+D-ids — an input to the board-coverage column — and ran **no**
+`regenerate-and-diff` at all. The committed table could have gone stale with CI
+fully green, which is the single thing this workflow exists to prevent. It did
+not, only because the regeneration happened to be done by hand.
+
+**The shape worth keeping:** a gate whose trigger is narrower than its
+computation is silent exactly where it is needed. Nothing about it looks broken
+— it passes when it runs, and when it matters most it does not run. That is the
+same silence-reads-as-success failure as `E-A-MONITOR-KEYED-ON-THE-PR-HEAD-…-1`
+(a watch keyed on the wrong subject) and as a guard that cannot fire: three
+instances in one session, each in a different mechanism.
+
+**Rule:** when a gate regenerates an artifact, its `paths:` filter must list
+every input the generator actually READS — derived from the generator's source,
+never from its prose. Prose was accurate here and the filter still drifted,
+because nothing joins the two.
+
+Fixed by adding `.claude/board/entries/**`, `.claude/board/EPIPHANIES.md` and
+`crates/**`. The last is broad on purpose: the generator takes ~15 s (measured),
+which is cheap beside the Rust jobs it runs next to, and a symbol deleted from
+the tree genuinely moves the table.
+
+---
+
+## 2026-08-31 — E-I-PINNED-THE-DEFECT-AS-THE-GUARD-WHILE-FIXING-A-REVIEW-COMMENT-1
+
+**Status:** FINDING — self-inflicted, caught by both reviewers on PR #1122,
+one PR after writing the rule it violates.
+**Confidence:** measured — `next_base_seq`, `lance-graph-planner`, disable-run
+red-then-green.
+
+PR #1120's review said `base_seq + i` could overflow. The fix added
+`next_base_seq`, saturating, with a doc comment stating that saturation
+prevents a wrapped coordinate from aliasing the durable log — and a test:
+
+```rust
+// The saturating guard: a wrapped coordinate would alias the start of
+// the durable log, the one outcome this precondition exists to stop.
+assert_eq!(next_base_seq(u64::MAX, 4), u64::MAX);
+```
+
+**That assertion pins the defect as the intended behaviour.** Saturation does
+not produce a free coordinate; it hands back one the reservation just minted.
+Replaying 4 steps from `u64::MAX - 3` mints through `u64::MAX`, the helper
+returns `u64::MAX`, and a caller following the documented sequential pattern
+replays a one-step chain there — legal, since the reservation only needs
+`steps - 1` addable — and emits a **duplicate `cast_seq`**. Exactly the
+duplicate the comment claimed to prevent. Measured, not argued: the new test
+replays both halves and asserts the two rows carry the same coordinate.
+
+**A guard that cannot say "no" is not a guard.** Same shape as
+`E-A-DETERMINISM-GATE-IS-TRIVIALLY-SATISFIED-BY-A-KERNEL-THAT-DOES-NOTHING-1`,
+written one PR earlier, in this same module. Saturation is the arithmetic form
+of a check that always passes: it makes the failure *unrepresentable in the
+return type*, so no caller can handle it and no test can catch it — the test I
+wrote asserted the collapsed value and went green. Fixed by making exhaustion
+representable (`Option<u64>`), after which `checked_add` IS the boundary and no
+separate exhaustion test is needed.
+
+**Two things worth keeping beyond the bug:**
+
+1. **A fix written for a review comment gets no discount.** This defect was
+   introduced *by* the remedy for a finding about the same field, and shipped
+   with a confident doc comment plus a test. The review context made it feel
+   already-scrutinised; nothing about it was.
+2. **Writing a rule does not install it.** The determinism-gate entry was three
+   commits old, in the same file, and I still reached for the arithmetic that
+   makes a guard vacuous. The disable-run is what catches this class — and I
+   did not run one on `next_base_seq`, because it was "just a helper".
+
+**Second finding, same PR, same shape at doc level:** the `validate_chain`
+doctrine says replay must not refuse history, then listed *"loading a
+recording"* as an admission site — which validates an old recording against
+today's palette and rejects exactly the history the argument protects. The
+argument was right and the instruction beneath it contradicted it. Corrected:
+admission = FIRST acceptance; a chain re-read from the durable log is already
+admitted and is replayed, never re-judged.
+
+---
+
 ## 2026-08-31 — E-TWO-REVIEWERS-FOUND-THE-SAME-THREE-DEFECTS-AND-ONE-OF-THEM-WAS-MINE-ALONE-1
 
 **Status:** FINDING — #1120's full review surface, read after merge.

.claude/board/STATUS_BOARD.md

@@ -5,7 +5,7 @@
 | D-DCR-0 | W0 measurements: chain-step evals/ms, EvidenceMask branching shrink, palette round-trip; ALU BUY threshold stated | **Shipped (CORRECTED #1118)** — promised kernel (NarsTables::revise + CausalEdge64::forward) **34.7 ns/step**; alloc-free `[u64;64]` mask 61.5 ns ⇒ **MASK dominates 1.77x** (v1's 3.8x superseded: substitute kernel + allocating fixture); KILL does not fire at EITHER the pre-registered 10^5 (13.88 ms) or the real 2,449 arm (0.340 ms), crossover ~53 chains; BUY at >10x the **1.36 ms** oracle arm. Probe `lance-graph-planner/examples/dcr_w0_replay_budget` |
 | D-DCR-0b | "borrow masking from ndarray?" measured (§3d): `mask_and` is a DEAD HEAT (1.08x) because the AND is 11.1 ns of a 65.2 ns half — the scalar POPCOUNT is 5.1x it. R2IL's `CallMask` (`[u64;3]`) needs nothing; jitson is a kernel compiler, not masking. The primitive that would pay (fused `mask_and_popcount`) does not exist and belongs IN ndarray | **Shipped** (measured direction; no wave scheduled) |
 | D-DCR-0a | prior-art reconciliation: `contract::dismech_evidence` + `dismech-causality-v3-v1` §11 arms (2,449 / 4,076 / 361) are W1-W3's falsifier; plan §3a | **Shipped** (E-W0-MEASURED-THE-MASK-HALF-DOMINATES-...-1) |
-| D-DCR-1 | replay core: loco calls under the dismech vocabulary -> CausalEdge64/NarsTruth steps -> temporal.rs trace; determinism + perturbation falsifiers | **Shipped (#1120, merged `cc0046f8`)** + follow-up in PR — `lance-graph-planner/src/dismech_replay.rs` (`replay_step` / `replay_chain` / `first_divergence` / `ReplayTraceRow: LocalCausalRow`); 4 gates, 3 disable-verified red-then-green. Palette binds at the membrane (plain `u8` ordinal here); the caller supplies a durable `base_seq` and the planner DERIVES each row's `cast_seq` from it — nothing here mints a counter. (Wording corrected per CodeRabbit #1120: the earlier phrasing said `cast_seq` was caller-supplied, which reverses the API contract.) Membrane half CLOSED: contract `dismech_evidence::DISMECH_PREDICATES` (zero-dep 19-row mirror, floor 0x90, position lookup) + armed-tier fuse `lance_graph_ogar::parity::assert_dismech_palette_parity` against the real `ogar_dismech::RELATIONS`, both directions, 3 more disables verified. Codex #1120: 3 findings, all valid — `ReplayTraceRow.predicate` now carried as WITNESS (the P1 falsified the module's own doc claim), `first_divergence` contract narrowed to content `(predicate, edge)` (the review's literal whole-row remedy was measured and rejected), `next_base_seq` makes the per-STEP durable reservation explicit. 9 disables total. CodeRabbit #1120 (4 more, read after merge): board wording corrected; `validate_chain` + `UnmintedOrdinal` reject an out-of-band ordinal AT ADMISSION while replay stays total over history; `replay_chain -> Result` with `ReplayError::SequenceExhausted` checks the whole reservation up front (`base_seq + i` panicked in debug / wrapped in release at u64::MAX). 11 disables total; 10 module gates |
+| D-DCR-1 | replay core: loco calls under the dismech vocabulary -> CausalEdge64/NarsTruth steps -> temporal.rs trace; determinism + perturbation falsifiers | **Shipped (#1120, merged `cc0046f8`)** + follow-up in PR — `lance-graph-planner/src/dismech_replay.rs` (`replay_step` / `replay_chain` / `first_divergence` / `ReplayTraceRow: LocalCausalRow`); 4 gates, 3 disable-verified red-then-green. Palette binds at the membrane (plain `u8` ordinal here); the caller supplies a durable `base_seq` and the planner DERIVES each row's `cast_seq` from it — nothing here mints a counter. (Wording corrected per CodeRabbit #1120: the earlier phrasing said `cast_seq` was caller-supplied, which reverses the API contract.) Membrane half CLOSED: contract `dismech_evidence::DISMECH_PREDICATES` (zero-dep 19-row mirror, floor 0x90, position lookup) + armed-tier fuse `lance_graph_ogar::parity::assert_dismech_palette_parity` against the real `ogar_dismech::RELATIONS`, both directions, 3 more disables verified. Codex #1120: 3 findings, all valid — `ReplayTraceRow.predicate` now carried as WITNESS (the P1 falsified the module's own doc claim), `first_divergence` contract narrowed to content `(predicate, edge)` (the review's literal whole-row remedy was measured and rejected), `next_base_seq` makes the per-STEP durable reservation explicit. 9 disables total. CodeRabbit #1120 (4 more, read after merge): board wording corrected; `validate_chain` + `UnmintedOrdinal` reject an out-of-band ordinal AT ADMISSION while replay stays total over history; `replay_chain -> Result` with `ReplayError::SequenceExhausted` checks the whole reservation up front (`base_seq + i` panicked in debug / wrapped in release at u64::MAX). 11 disables total; 10 module gates. PR #1122 review (both reviewers, same bug): `next_base_seq` saturated and handed back an ALREADY-MINTED coordinate at the top of the range — a duplicate `cast_seq`, with the test pinning it as "the saturating guard". Now `Option<u64>`; exhaustion is representable. Also corrected: admission = FIRST acceptance, never re-reading the durable log (the old wording contradicted its own replay-must-not-refuse-history argument). 12 disables |
 | D-DCR-2 | Mengenlehre candidate evaluation via `contract::revision::EvidenceMask` (support ∩ / refute ∖ over `dismech_evidence::Supports`) | Queued — **spec corrected in preflight**: the refute class is the evidence STANCE (`Supports`, shipped + measured), NOT the graph-construction skip filter the plan first named. The skip filter decides whether an item becomes an edge at all, so a candidate set built from the graph has already excluded it — `∖` would subtract twice. Plan §W2 carries the full correction |
 | D-DCR-3 | counterfactual replay (edge cut through `contract::counterfactual`, Pearl rung 3), two-sided load-bearing/redundant gates | Queued |
 | D-DCR-4 | Σ transport via `jc::ewa_sandwich` + candidate-entropy readout; entropy-surface CONSOLIDATION decision recorded first | Queued |

.github/workflows/supersession-index.yml

@@ -14,6 +14,22 @@ on:
       - .claude/tools/supersession_index.py
       - .claude/board/SUPERSESSION-INDEX.md
       - .github/workflows/supersession-index.yml
+      # The BOARD is an input too, and was missing from this list. The
+      # generator's "board coverage" column counts each plan's D-ids cited in
+      # `board/entries/*.md` + `EPIPHANIES.md` (supersession_index.py:48-49,
+      # read at :85), so a PR that only PREPENDS an epiphany citing a D-id
+      # moves the table while the gate stayed silent -- CI green over a stale
+      # index, which is the one thing this workflow exists to prevent.
+      # Measured on #1123: an EPIPHANIES-only PR ran no `regenerate-and-diff`
+      # at all. `CLAUDE.md` already named the board among the inputs; the
+      # filter had not caught up.
+      - .claude/board/entries/**
+      - .claude/board/EPIPHANIES.md
+      # `crates/` decides the "live" column (:27 globs it per symbol). Broad,
+      # and deliberately so: a symbol deleted from the tree changes the table,
+      # and the generator takes ~15 s, so the gate is cheap next to the Rust
+      # jobs it runs beside.
+      - crates/**
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
@@ -33,8 +49,11 @@ jobs:
           if ! diff -u .claude/board/SUPERSESSION-INDEX.md /tmp/regen.md; then
             echo
             echo "::error::SUPERSESSION-INDEX.md is stale."
-            echo "It is GENERATED from .claude/plans/ + crates/ + COMPONENT-MAP.md,"
-            echo "so adding a plan that names a ruled symbol makes it stale."
+            echo "It is GENERATED from ALL of:"
+            echo "  .claude/plans/  +  crates/  +  .claude/v3/COMPONENT-MAP.md"
+            echo "  .claude/board/entries/  +  .claude/board/EPIPHANIES.md"
+            echo "so a plan naming a ruled symbol, a symbol added or deleted in"
+            echo "crates/, OR a board entry citing a D-id can make it stale."
             echo "Regenerate and commit:"
             echo "  python3 .claude/tools/supersession_index.py > .claude/board/SUPERSESSION-INDEX.md"
             exit 1