diff --git a/.claude/board/EPIPHANIES.md b/.claude/board/EPIPHANIES.md index 537161da9..a71721983 100644 --- a/.claude/board/EPIPHANIES.md +++ b/.claude/board/EPIPHANIES.md @@ -1,3 +1,60 @@ +## 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. +**Confidence:** measured — 7 findings across two independent reviewers on the +same diff; each adjudicated against the code, two remedies rejected with +evidence. + +#1120 drew **7 findings from two reviewers that never see each other's +output** — codex (3) and CodeRabbit (4). Their overlap is the interesting +part, and so is the one place they diverge. + +| line | codex | CodeRabbit | verdict | +|---|---|---|---| +| 179 | predicate dropped from the trace | reject an out-of-band ordinal | **same defect, two different remedies** | +| 183 | overlapping durable coordinates | `cast_seq` overflow at `u64::MAX` | **same field, two distinct bugs — both real** | +| 199/200 | compare only edges vs the doc's promise | identical finding | **agreed, and both remedies wrong** | +| board | — | `cast_seq` described as caller-supplied | **CodeRabbit alone; correct** | + +**Independent agreement is evidence; identical remedies are not.** Both +reviewers proposed comparing whole `ReplayTraceRow` values in +`first_divergence`. Running it: the same chain replayed from durable base 100 +vs 900 is declared divergent at step 0 — the same witness at two addresses. +Two reviewers converging on a fix does not make the fix right, and the cost of +checking was one test run. + +**The 179 pair is the sharper lesson.** Both saw that the ordinal was +mishandled; they disagreed about *which* mishandling. Codex: it is dropped +from the witness (so a recorded program cannot be reconstructed). CodeRabbit: +it is not validated (so a chain carrying `0xA3`, the SEARCH band, replays as +if causal). **Both are true and the fixes go in opposite directions** — carry +it *more* faithfully, and judge it *before* it is carried. Taking either alone +would have looked complete. + +The split that resolves it: **replay must not refuse history.** A recorded +chain is a fact; the engine reproduces it, it does not judge it. If the palette +later drops or renumbers an ordinal, a validating replay starts returning `Err` +for chains that were valid when recorded — destroying the very property the +wave exists to hold. So validation is an ADMISSION check (`validate_chain`, +constant per chain, checked once) and replay stays total over admitted chains, +while the witness carries the ordinal faithfully. Both findings satisfied, +neither remedy taken literally. + +**The board finding is the one only a doc-reader caught.** The status row said +*"`cast_seq` is caller-supplied and durable, never minted"* — reversing the +contract, since the caller supplies `base_seq` and the planner DERIVES +`cast_seq`. No code reviewer would flag it; no test could fail on it. It is +exactly the class of error that survives forever because it lives where nothing +executes. + +**Consequence for the review posture:** a second reviewer is not redundancy — +measured here, it contributed one finding neither the first reviewer nor any +gate could reach, and it disagreed usefully about a defect the first had +already found. And a finding's *remedy* is a proposal, never a verdict: 3 of 7 +remedies here were wrong or too literal, while 7 of 7 findings were real. + +--- + ## 2026-08-31 — E-Q8-THE-SIX-DOES-NO-WORK-A-DEGREE-ABLATION-COLLAPSES-THE-HEX-OVERLAYS-ENTIRE-ADVANTAGE-1 — B passes every pre-registered gate and the pass is unattributable: at degree 1 it scores identically with 5.5x less memory **Status:** FINDING [MEASURED] — full entry in @@ -21,6 +78,156 @@ nothing; B is a bigram successor table. Converges with `E-PALETTE256-IS-A-NEEDLE-THE-COLON-IS-THE-DISTRIBUTION-1` by a different road: the information is in the PAIR, not the neighbourhood's shape. One relation carried everything; five more neighbours added bytes. +## 2026-08-31 — E-A-MONITOR-KEYED-ON-THE-PR-HEAD-CAN-CERTIFY-THE-WRONG-COMMIT-1 + +**Status:** FINDING — the RULE stands; the CAUSE first recorded here was +**wrong and is corrected below**, same day, before this entry ever merged. +**Confidence:** measured — GitHub's `pulls/1120` reported head `233ce3f1` for +>45 minutes while `git/ref/heads/…` (same API, same token, same request) already +had `216d8f2` and then `81820cc`; `mergeable` stayed `null` throughout. + +> **⊘ CAUSE CORRECTED (same day, on discovering the merge).** This entry first +> blamed *"GitHub delivered no push event"* — an exotic infrastructure story. +> The real cause was mundane and one field away: **#1120 had already MERGED**, +> at 19:45:46, with head `233ce3f1`. A merged PR stops tracking its branch and +> stops running PR-triggered workflows, so the frozen head, the null +> `mergeable`, and the silent Actions were all *correct behaviour* for a closed +> PR — not a delivery stall. +> +> **How the wrong cause survived four checks:** an early query printed +> `pr["state"]` (`open`); every later query printed head, mergeable and +> check-runs and **dropped `state`**. Each subsequent read was consistent with +> both hypotheses — "GitHub is stalling" and "the PR is closed" — and I never +> re-read the one field that separates them. I then wrote an increasingly +> specific infrastructure diagnosis (webhooks, proxy ref-updates) on top of a +> premise I had stopped checking. +> +> **The transferable rule is the sharper one:** when a subject stops behaving, +> **re-read its STATE before theorising about its plumbing.** A field you +> printed once and dropped is not a field you know. The exotic explanation felt +> earned because each new observation fit it — but they fit the boring one +> equally, and only the dropped field discriminated. +> +> **What survives unchanged:** the rule this entry exists for. Keying a watch +> on the PR head certified the wrong commit, and it would have done so for a +> *merged* PR just as surely as for a stalled one — arguably more so, since a +> merged PR's head is frozen permanently. Pin the SHA; compare it. If anything, +> a merged-PR head is the commoner way to hit this. + +A CI monitor was armed to poll the PR, emit each check as it landed, and stop +at "all complete". It reported **ALL GREEN**. The verdict was true — and it was +a verdict on the **wrong commit**: 7/7 covered the head GitHub still believed +in, while the two commits carrying that PR's review fixes had **zero** checks. + +``` +PR head: 233ce3f1 → 7/7 complete, red=none +branch ref: 216d8f29 → 0/0 complete +``` + +**The failure is in the KEY, not the polling.** A monitor that resolves its +subject through the PR object inherits whatever the PR object believes, and a +PR head pointer is *derived state* that can lag the ref it points at. Every +line the monitor printed was accurate; none of them was about the code under +review. Silence would have been safer than that green. + +**Rules, both cheap:** + +1. **Pin the SHA before arming, and assert it.** A watch should be keyed on the + commit you pushed — read it from `git rev-parse HEAD` — not on whatever the + PR resolves to at poll time. If the PR's head and your SHA disagree, that + disagreement is itself the event worth reporting. +2. **A green run is a verdict on a SHA, never on a PR.** Before acting on one, + check `pr.head.sha == `. Two API calls. + +**Why it was caught:** not by the monitor and not by any gate — by noticing +that a routine status read showed a head two commits behind a push whose +output had scrolled past. (The *cause* took longer and was got wrong first — +see the correction at the top.) The generalization is uncomfortable and worth +keeping: **an automated check can be simultaneously correct and irrelevant**, +and nothing inside it can tell the difference, because relevance is a property +of what it was pointed at. + +Cf. `E-EVERY-DEFECT-IN-A-MEASUREMENT-WAS-IN-ITS-FIXTURE-NOT-ITS-CODE-1` — same +shape one layer up: there the fixture was wrong and the timing loop was fine; +here the subject was wrong and the polling was fine. In both, the instrument +reported faithfully on something that was not the question. + +--- + +## 2026-08-31 — E-A-WITNESS-THAT-DROPS-THE-RELATION-IS-NOT-A-WITNESS-1 — and the review's own remedy was measurably wrong + +**Status:** FINDING — three codex P1/P2 findings on #1120, all valid; the P1 +falsified a claim in the module's own doc comment. The P2 remedy was tried +literally, measured, and rejected in favour of a narrowing. +**Confidence:** measured — `lance-graph-planner/src/dismech_replay.rs`, +D-DCR-1 (W1), three disable-runs. + +### The P1: the trace dropped the predicate, and the doc said otherwise + +`replay_chain` destructured `&(_predicate, weight)` and never carried the +ordinal into `ReplayTraceRow`. Two chains with identical weights and different +relations — `causes` vs `protects_against`, near-opposite meanings — replay to +**byte-identical traces**, and `first_divergence` reports no change. + +For a plan whose keystone is *causality replay*, that is not a gap in a +convenience field: the witness cannot reconstruct the recorded program. And +the module doc claimed the opposite — *"carried into the trace's step index so +a consumer can join a diff back to the palette at the membrane"* — where the +step index is `i` and the ordinal was carried nowhere. A doc claim with no +behaviour behind it, in the same PR that added a mirror so the ordinal would +have a checkable domain. + +**Why every W1 gate passed anyway, and this is the transferable part:** W1's +arithmetic deliberately does not read the ordinal. A property that does not +touch a field cannot notice that the field is gone. Determinism, perturbation +position, sibling isolation, deinterlace — four gates, none of which could +ever fail on this. **A value carried as WITNESS needs a gate that reads it as +witness; the gates on the computation will not cover it, by construction.** + +### The P2 remedy was wrong, and running it is how that was established + +The review's `first_divergence` finding was right about the defect (the name +promised a whole-row comparison the body did not perform) and its suggested +fix — *"compare the full `ReplayTraceRow` values"* — was tried verbatim: + +``` +addressing_is_not_content_but_the_predicate_is ... FAILED + left: Some(0) right: None +``` + +The same chain, same owner, replayed from durable base 100 vs 900, is declared +**divergent at step 0**. That is the same causal witness at two addresses, and +an instrument that calls it divergent is useless for every comparison the plan +needs. So the fix is the review's *alternative* clause — "narrow the API +contract explicitly": content is `(predicate, edge)`; `owner`/`cast_seq` are +addressing and deliberately excluded; `step` is positional and is what the +return value NAMES. + +**A correct finding does not make its proposed remedy correct.** Both halves +were verifiable in about a minute each; taking the remedy on trust would have +shipped a diff instrument that fires on every address change. + +### The third: a precondition stated as prose is not a precondition + +`base_seq` reserves `[base_seq, base_seq + chain.len())` — one coordinate per +STEP. A caller advancing by 1 per CHAIN overlaps (bases 10 and 11 over 4 steps +share 3 of 4 coordinates), which violates `LocalCausalRow::cast_seq`'s +uniqueness requirement and silently degrades `local_trajectory_of` to scan +order. The old doc said two chains "never collide" — true only for a caller +already following a rule the doc did not state. + +The overlap is a property ACROSS calls and cannot be checked inside one, so it +stays a precondition — but now it is stated, and shipped as code +(`next_base_seq`) so the correct advance is the easy one. The gate measures +the collision (`shared == 3`) rather than asserting the rule. + +### Disable table (all three red-then-green) + +| assertion | disable | observed | +|---|---|---| +| predicate is in the witness | `predicate: 0` in the row | RED ×2 | +| addressing is not content | compare whole rows (the review's literal remedy) | RED — `Some(0)` vs `None` | +| the reservation is per step | `next_base_seq` → `base + 1` | RED — `left: 11, right: 14` | --- diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 42fb15ef4..693b21f7f 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -5,8 +5,8 @@ | 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 | **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); `cast_seq` is caller-supplied and durable, never minted. 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 | -| D-DCR-2 | Mengenlehre candidate evaluation via `contract::revision::EvidenceMask` (support ∩ / refute ∖, skip-words as ordinals) | Queued | +| 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-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 | | D-DCR-5 | frontier scheduling (info-gain / rung-cost via `EpistemicMode::for_rung`) | **HELD** — operator rung 5-9 table ruling + W0 KILL check | diff --git a/.claude/plans/dismech-causal-replay-v1.md b/.claude/plans/dismech-causal-replay-v1.md index 8b4d552ef..76de8b7a3 100644 --- a/.claude/plans/dismech-causal-replay-v1.md +++ b/.claude/plans/dismech-causal-replay-v1.md @@ -125,8 +125,43 @@ nothing. Disable-verified per the falsifiability rule. ### W2 — Mengenlehre candidate evaluation — `D-DCR-2` Candidate sets as masks; support evidence intersects, refuting evidence -subtracts (the skip-word semantics — `biomarker/disputed/modifier/ -protective/refuted/unknown` — as refute-class ordinals, never strings). +subtracts — as ordinals, never strings. + +> **⊘ CORRECTION (2026-08-31, preflight before the wave was spawned).** The +> line above originally named the refute class as *"the skip-word semantics — +> `biomarker/disputed/modifier/protective/refuted/unknown`"*. That set is +> real, but it is **the wrong axis for this wave**, and building W2 on it +> would have been a category error: +> +> | axis | what it decides | where it belongs | +> |---|---|---| +> | evidence **stance** — `dismech_evidence::Supports` (`Support` / `Partial` / `Refute` / `NoEvidence`), already shipped, measured ~89,800 occurrences | does this evidence item support or refute a candidate | **W2's ∩ / ∖** | +> | the **graph-construction skip filter** — a predicate over the source's own `relationship_type` / free-text `association` fields | does a source item infer a mechanism edge AT ALL | upstream of any candidate set; it runs while the graph is built, not while candidates are evaluated | +> +> The skip filter is not a refutation. An item it skips never becomes an edge, +> so there is nothing for `∖` to subtract — a candidate set built from the +> graph has already had them excluded. Wiring it as the refute class would +> subtract a second time, against a set that never contained them. +> +> Two further facts make the original line worse than merely mis-axised, and +> both are reasons to leave that vocabulary where it is: +> +> 1. **It is two lists, not one, and the asymmetry is load-bearing.** The +> enum-valued arm and the free-text-token arm do not carry the same +> members — `refuted` appears in one and not the other. That asymmetry is +> upstream's, preserved deliberately by its transcode as *not a bug to +> fix*. A single 6-ordinal enum in this crate would flatten it, and the +> flattening would be invisible. +> 2. **Its authority is consumer-side**, in the crate that transcodes the +> source graph builder. This crate would be holding a second copy of a +> filter it does not own and cannot check — the exact mirror-without-a-fuse +> shape `ogar_codebook` and (this PR) `DISMECH_PREDICATES` both avoid by +> pairing every mirror with a drift gate. There is no gate available here. +> +> **So W2 uses `Supports`**, which is already in the contract, already +> measured, already exhaustively round-tripped, and is the axis the ∩/∖ +> algebra is actually about. If a wave ever genuinely needs the skip filter, +> it belongs where the graph is built, with its two arms intact. **Gates:** anti-vacuity (`kept * 3 < total` on the synthetic corpus); two-sided discrimination (a discriminating evidence item must split the diff --git a/crates/lance-graph-planner/src/dismech_replay.rs b/crates/lance-graph-planner/src/dismech_replay.rs index 1721fe223..9d7df8a8d 100644 --- a/crates/lance-graph-planner/src/dismech_replay.rs +++ b/crates/lance-graph-planner/src/dismech_replay.rs @@ -39,6 +39,8 @@ use causal_edge::tables::{unpack_c, unpack_f, NarsTables}; use causal_edge::CausalEdge64; +use core::fmt; + use lance_graph_contract::collapse_gate::MailboxId; use crate::temporal::LocalCausalRow; @@ -68,6 +70,20 @@ pub struct ReplayTraceRow { /// Index of the step within its chain — the address a perturbation is /// reported AT, so a diff names a position rather than a row. pub step: u32, + /// The DisMech predicate ordinal this step travelled under. + /// + /// **Carried as witness, not as an operand.** W1's arithmetic never reads + /// it — but a trace that dropped it would not be a witness of the recorded + /// program: two chains with identical weights and different relations + /// (`causes` vs `protects_against`) would replay to byte-identical traces, + /// and no consumer could reconstruct or validate what was actually + /// recorded. Resolve it through [`chain_step_predicate`] (or, at the + /// membrane, the real palette). + /// + /// Added after review on #1120: the module previously claimed the ordinal + /// was "carried into the trace's step index" — it was not carried at all, + /// and the step index is `i`. That was a doc claim no behaviour backed. + pub predicate: u8, /// The packed edge this step produced. pub edge: CausalEdge64, } @@ -126,6 +142,88 @@ pub fn chain_step_predicate(step: ChainStep) -> Option<&'static (u8, &'static st lance_graph_contract::dismech_evidence::dismech_predicate(step.0) } +/// A replay could not be performed as asked. +/// +/// Deliberately small: replay has exactly one way to fail, and it is a +/// property of the ADDRESS SPACE the caller offered, never of the recorded +/// chain (see [`validate_chain`] for why a chain's content is not judged here). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +#[non_exhaustive] +pub enum ReplayError { + /// `[base_seq, base_seq + chain.len())` does not fit in `u64`. + /// + /// Not a theoretical guard: the alternative is wrapping, and wrapped + /// coordinates alias the START of the durable log — duplicate `cast_seq` + /// values that violate [`LocalCausalRow`]'s uniqueness requirement and + /// silently degrade `local_trajectory_of` to scan order. Refused loudly + /// rather than emitted quietly. (Raised by review on #1120: the previous + /// `base_seq + i as u64` panicked in debug builds and wrapped in release.) + SequenceExhausted { + /// The base the caller offered. + base_seq: u64, + /// How many steps the chain needed. + steps: usize, + }, +} + +impl fmt::Display for ReplayError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::SequenceExhausted { base_seq, steps } => write!( + f, + "durable sequence exhausted: base {base_seq} cannot reserve {steps} steps" + ), + } + } +} + +impl std::error::Error for ReplayError {} + +/// A step whose predicate ordinal names no minted DisMech predicate. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct UnmintedOrdinal { + /// Index of the offending step within the chain. + pub step: usize, + /// The ordinal that resolved to nothing. + pub ordinal: u8, +} + +/// Check that every step of a chain travels under a minted DisMech predicate. +/// +/// # Why this is an ADMISSION check and NOT part of [`replay_chain`] +/// +/// Review on #1120 proposed validating inside the replay loop and returning an +/// error before emitting a trace row. The defect it names is real — a chain +/// carrying `0xA3` (the palette's SEARCH band) is not a causal chain, and +/// replaying it produces a byte-identical, meaningless trace. But the remedy +/// belongs one step earlier, for a reason that goes to the plan's keystone: +/// +/// **Replay must not refuse history.** A recorded chain is a fact about what +/// was evaluated; the engine's job is to reproduce it, not to judge it. If the +/// palette ever drops or renumbers an ordinal, a replay that validated would +/// start returning `Err` for chains that were perfectly valid when recorded — +/// and "yesterday's evaluation replays today byte-for-byte" is precisely the +/// property the whole wave exists to hold. +/// +/// So the judgement happens where a chain ENTERS the system (loading a +/// recording, accepting one over a boundary) and is a constant property of the +/// chain, checked once; replay stays total over admitted chains. Call this at +/// admission, and at the membrane where the real palette is reachable. +/// +/// Fails closed and reports WHICH step, so a rejection is actionable rather +/// than a boolean. +pub fn validate_chain(chain: &[ChainStep]) -> Result<(), UnmintedOrdinal> { + for (step, &entry) in chain.iter().enumerate() { + if chain_step_predicate(entry).is_none() { + return Err(UnmintedOrdinal { + step, + ordinal: entry.0, + }); + } + } + Ok(()) +} + /// The single step, isolated so the replay and any future accelerator agree on /// what a step IS. Composes the two halves W0 measured, in that order: /// the table lookup (evidence fusion) then the packed forward (palette @@ -156,16 +254,35 @@ pub fn replay_step( /// Replay a recorded chain against `seed`, emitting one trace row per step. /// -/// `base_seq` is the caller's DURABLE ordering position (see the module doc): -/// row *i* is stamped `base_seq + i`, so a chain replayed from the same log -/// position is byte-identical, and two chains from different positions never -/// collide. Nothing here mints a counter. +/// # `base_seq` RESERVES a half-open range, it is not a chain counter /// -/// The predicate ordinal rides each step but does not alter the arithmetic in -/// W1 — it is the ADDRESS the step travels under, carried into the trace's -/// step index so a consumer can join a diff back to the palette at the -/// membrane. W3's counterfactual arm is what makes it selective. -#[must_use] +/// This call stamps `[base_seq, base_seq + chain.len())` — one durable +/// coordinate per STEP, not per chain. A caller that advances by 1 per chain +/// therefore overlaps: bases 10 and 11 over 4-step chains produce +/// `[10,11,12,13]` and `[11,12,13,14]`, and the shared coordinates violate +/// [`LocalCausalRow::cast_seq`]'s uniqueness requirement — after which +/// `local_trajectory_of` preserves SCAN order rather than durable causal +/// order, so a crash replay varies with how rows happened to interleave. +/// +/// Advance with [`next_base_seq`], which is the reservation stated as code. +/// The overlap cannot be detected inside one call (it is a property ACROSS +/// calls), so this is a precondition, not a check — said plainly rather than +/// implied. `overlapping_bases_collide_which_is_why_next_base_seq_exists` +/// pins both directions. (Raised in review on #1120; the prior doc said two +/// chains "never collide", which was true only for a caller already +/// following the rule it did not state.) +/// +/// The predicate ordinal rides each step into [`ReplayTraceRow::predicate`]. +/// It does not alter W1's arithmetic — it is the ADDRESS the step travels +/// under — but it IS part of the witness, so a consumer can join a diff back +/// to the palette at the membrane. W3's counterfactual arm makes it selective. +/// +/// # Errors +/// +/// [`ReplayError::SequenceExhausted`] when `[base_seq, base_seq + chain.len())` +/// does not fit in `u64`. The reservation is checked ONCE, up front, so the +/// loop cannot emit a partial trace and then discover it has no coordinate +/// left — a half-written trace is worse than a refusal. pub fn replay_chain( chain: &[ChainStep], seed: CausalEdge64, @@ -173,30 +290,71 @@ pub fn replay_chain( compose: ComposeTables<'_>, owner: MailboxId, base_seq: u64, -) -> Vec { +) -> Result, ReplayError> { + // Check the whole reservation before writing anything. + let steps = chain.len(); + if steps > 0 { + u64::try_from(steps - 1) + .ok() + .and_then(|last| base_seq.checked_add(last)) + .ok_or(ReplayError::SequenceExhausted { base_seq, steps })?; + } + let mut running = seed; - let mut trace = Vec::with_capacity(chain.len()); - for (i, &(_predicate, weight)) in chain.iter().enumerate() { + let mut trace = Vec::with_capacity(steps); + for (i, &(predicate, weight)) in chain.iter().enumerate() { running = replay_step(running, weight, tables, compose); trace.push(ReplayTraceRow { owner, cast_seq: base_seq + i as u64, step: u32::try_from(i).unwrap_or(u32::MAX), + predicate, edge: running, }); } - trace + Ok(trace) } -/// The first step index at which two traces differ, or `None` when they are -/// byte-identical. This is the determinism gate's instrument AND the -/// perturbation gate's: a perturbation must be reported at the step it was -/// applied to, never earlier. +/// The next free durable coordinate after replaying a `chain_len`-step chain +/// from `base_seq` — the half-open reservation `[base_seq, base_seq + len)` +/// stated as code, so a caller replaying several chains in sequence cannot +/// reach for a naive `+ 1`. +/// +/// Saturating rather than wrapping: a wrapped coordinate would silently alias +/// the beginning of the durable log, which is the one failure this whole +/// precondition exists to prevent. +#[must_use] +pub const fn next_base_seq(base_seq: u64, chain_len: usize) -> u64 { + base_seq.saturating_add(chain_len as u64) +} + +/// The first step whose replayed CONTENT differs, or `None` when the two +/// traces carry the same content throughout. +/// +/// # What "content" means here, and why it is not the whole row +/// +/// Content is `(predicate, edge)` — the relation the step travelled under and +/// the edge it produced. **Addressing (`owner`, `cast_seq`) is deliberately +/// NOT compared**, and the narrowing is the point rather than a shortcut: the +/// same chain replayed by the same owner from two different durable positions +/// is the SAME causal witness at two addresses, and an instrument that called +/// those "divergent" would report a difference at step 0 for every comparison +/// the plan actually needs. `step` is excluded for the same reason — it is +/// positional, and position is what the return value NAMES. +/// +/// This is the determinism gate's instrument AND the perturbation gate's: a +/// perturbation must be reported at the step it was applied to, never earlier. +/// +/// (Contract narrowed explicitly after review on #1120, which correctly +/// observed that the previous wording — "where the traces differ" — promised +/// a whole-row comparison the body did not perform. Fixed by naming the +/// contract, not by widening the comparison: see +/// `addressing_is_not_content_but_the_predicate_is`.) #[must_use] pub fn first_divergence(a: &[ReplayTraceRow], b: &[ReplayTraceRow]) -> Option { a.iter() .zip(b.iter()) - .find(|(x, y)| x.edge != y.edge) + .find(|(x, y)| (x.predicate, x.edge) != (y.predicate, y.edge)) .map(|(x, _)| x.step) .or_else(|| { if a.len() == b.len() { @@ -277,8 +435,8 @@ mod tests { let ch = chain(&mut rng, 12); let seed = edge(&mut rng); - let a = replay_chain(&ch, seed, &t, tabs, 7, 1_000); - let b = replay_chain(&ch, seed, &t, tabs, 7, 1_000); + let a = replay_chain(&ch, seed, &t, tabs, 7, 1_000).expect("reservation fits"); + let b = replay_chain(&ch, seed, &t, tabs, 7, 1_000).expect("reservation fits"); assert_eq!(a, b, "replay is not deterministic"); assert_eq!(first_divergence(&a, &b), None); // Anti-vacuity, and it must cover BOTH halves of the kernel — a @@ -314,7 +472,7 @@ mod tests { let mut rng = Lcg(0x0BAD_5EED_1234_5678); let ch = chain(&mut rng, 12); let seed = edge(&mut rng); - let base = replay_chain(&ch, seed, &t, tabs, 7, 1_000); + let base = replay_chain(&ch, seed, &t, tabs, 7, 1_000).expect("reservation fits"); for k in [0usize, 5, 11] { let mut perturbed = ch.clone(); @@ -323,7 +481,8 @@ mod tests { w.set_s_idx(w.s_idx().wrapping_add(1)); perturbed[k].1 = w; - let other = replay_chain(&perturbed, seed, &t, tabs, 7, 1_000); + let other = + replay_chain(&perturbed, seed, &t, tabs, 7, 1_000).expect("reservation fits"); assert_eq!( first_divergence(&base, &other), Some(k as u32), @@ -351,16 +510,16 @@ mod tests { let mut sibling = chain(&mut rng, 12); let seed = edge(&mut rng); - let base = replay_chain(&ch, seed, &t, tabs, 7, 1_000); + let base = replay_chain(&ch, seed, &t, tabs, 7, 1_000).expect("reservation fits"); let mut w = sibling[3].1; w.set_s_idx(w.s_idx().wrapping_add(17)); sibling[3].1 = w; - let after = replay_chain(&ch, seed, &t, tabs, 7, 1_000); + let after = replay_chain(&ch, seed, &t, tabs, 7, 1_000).expect("reservation fits"); assert_eq!(base, after, "a sibling chain must not reach this replay"); // anti-vacuity: the sibling really is a different chain, and replaying // IT really does differ — otherwise "unchanged" is trivially true. - let sib_trace = replay_chain(&sibling, seed, &t, tabs, 7, 1_000); + let sib_trace = replay_chain(&sibling, seed, &t, tabs, 7, 1_000).expect("reservation fits"); assert_ne!(base, sib_trace); } @@ -380,8 +539,8 @@ mod tests { let (ch_a, ch_b) = (chain(&mut rng, 4), chain(&mut rng, 4)); let seed = edge(&mut rng); - let a = replay_chain(&ch_a, seed, &t, tabs, 1, 10); - let b = replay_chain(&ch_b, seed, &t, tabs, 2, 500); + let a = replay_chain(&ch_a, seed, &t, tabs, 1, 10).expect("reservation fits"); + let b = replay_chain(&ch_b, seed, &t, tabs, 2, 500).expect("reservation fits"); // interleave them the way a shared durable log would let mut global = Vec::new(); for i in 0..4 { @@ -417,4 +576,222 @@ mod tests { assert!(chain_step_predicate((0xA3, w)).is_none()); assert!(chain_step_predicate((0x8F, w)).is_none()); } + #[test] + fn two_chains_differing_only_in_predicate_do_not_replay_identically() { + // The P1 finding from #1120, pinned. Identical weights, one relation + // swapped: `causes` (0x90) vs `protects_against` (0x95) — two + // predicates whose real-world meanings are near opposites, so a trace + // that cannot tell them apart is not a witness of anything. + let tables = NarsTables::build(1); + let c_tabs = compose_tables(); + let tabs = ComposeTables { + s: &c_tabs[0], + p: &c_tabs[1], + o: &c_tabs[2], + }; + let mut rng = Lcg(0x0C0D_E4A1_7B39_5E62); + let seed = edge(&mut rng); + let steps: Vec = (0..6).map(|_| edge(&mut rng)).collect(); + + let a: Vec = steps.iter().map(|&w| (0x90u8, w)).collect(); + let mut b = a.clone(); + b[3].0 = 0x95; + + // Anti-vacuity: the two chains must be identical in EVERY other + // respect, or this test would pass for the wrong reason. + assert_eq!(a.len(), b.len()); + for (x, y) in a.iter().zip(b.iter()) { + assert_eq!( + x.1, y.1, + "weights must match — only the predicate may differ" + ); + } + assert_ne!(a[3].0, b[3].0); + + let ta = replay_chain(&a, seed, &tables, tabs, 7, 100).expect("reservation fits"); + let tb = replay_chain(&b, seed, &tables, tabs, 7, 100).expect("reservation fits"); + + // The packed arithmetic is genuinely identical — W1 does not read the + // ordinal — so the ONLY thing that can distinguish these traces is the + // predicate being carried as witness. + for (x, y) in ta.iter().zip(tb.iter()) { + assert_eq!( + x.edge, y.edge, + "W1 arithmetic must not depend on the ordinal" + ); + } + assert_eq!( + first_divergence(&ta, &tb), + Some(3), + "the swapped relation must be visible in the witness, at its own step", + ); + } + + #[test] + fn addressing_is_not_content_but_the_predicate_is() { + // The P2 `first_divergence` finding, pinned two-sided. + let tables = NarsTables::build(1); + let c_tabs = compose_tables(); + let tabs = ComposeTables { + s: &c_tabs[0], + p: &c_tabs[1], + o: &c_tabs[2], + }; + let mut rng = Lcg(0x51CE_2D07_A4B8_1193); + let seed = edge(&mut rng); + let c = chain(&mut rng, 5); + + // (a) SILENT on pure addressing: same chain, same owner, different + // durable base — the same causal witness at another address. + let at_100 = replay_chain(&c, seed, &tables, tabs, 1, 100).expect("reservation fits"); + let at_900 = replay_chain(&c, seed, &tables, tabs, 1, 900).expect("reservation fits"); + assert_ne!( + at_100[0].cast_seq, at_900[0].cast_seq, + "the addresses must actually differ, or this proves nothing", + ); + assert_eq!(first_divergence(&at_100, &at_900), None); + + // (b) ...and a different OWNER is addressing too. + let other = replay_chain(&c, seed, &tables, tabs, 2, 100).expect("reservation fits"); + assert_ne!(at_100[0].owner(), other[0].owner()); + assert_eq!(first_divergence(&at_100, &other), None); + + // (c) FIRES on content: one predicate swapped, addressing untouched. + let mut c2 = c.clone(); + c2[2].0 = if c2[2].0 == 0x90 { 0x91 } else { 0x90 }; + let swapped = replay_chain(&c2, seed, &tables, tabs, 1, 100).expect("reservation fits"); + assert_eq!(first_divergence(&at_100, &swapped), Some(2)); + } + + #[test] + fn overlapping_bases_collide_which_is_why_next_base_seq_exists() { + // The P2 durable-coordinate finding, pinned as the precondition it is. + let tables = NarsTables::build(1); + let c_tabs = compose_tables(); + let tabs = ComposeTables { + s: &c_tabs[0], + p: &c_tabs[1], + o: &c_tabs[2], + }; + let mut rng = Lcg(0xD0A7_31FC_5E28_44B9); + let seed = edge(&mut rng); + let c = chain(&mut rng, 4); + let owner = 3; + + let coords = + |t: &[ReplayTraceRow]| -> Vec { t.iter().map(|r| r.cast_seq()).collect() }; + + // WRONG: advance by one per chain. The reservation is per STEP, so the + // ranges overlap on 3 of 4 coordinates. + let naive_a = replay_chain(&c, seed, &tables, tabs, owner, 10).expect("reservation fits"); + let naive_b = replay_chain(&c, seed, &tables, tabs, owner, 11).expect("reservation fits"); + let (ca, cb) = (coords(&naive_a), coords(&naive_b)); + let shared = ca.iter().filter(|x| cb.contains(x)).count(); + assert_eq!( + shared, 3, + "a naive +1 advance must demonstrably collide, or the precondition is decoration", + ); + + // RIGHT: advance by the reservation. + let ok_a = replay_chain(&c, seed, &tables, tabs, owner, 10).expect("reservation fits"); + let next = next_base_seq(10, c.len()); + assert_eq!(next, 14); + let ok_b = replay_chain(&c, seed, &tables, tabs, owner, next).expect("reservation fits"); + let (oa, ob) = (coords(&ok_a), coords(&ok_b)); + assert!( + oa.iter().all(|x| !ob.contains(x)), + "correctly advanced ranges must be disjoint", + ); + // ...and contiguous, so the log has no unexplained holes. + assert_eq!(*oa.last().unwrap() + 1, ob[0]); + + // 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); + } + #[test] + fn a_chain_carrying_a_search_op_is_refused_at_admission_and_still_replays() { + // CodeRabbit #1120 asked that `replay_chain` itself reject an ordinal + // outside the predicate band. Both halves are pinned here, because the + // SPLIT is the decision, not either half alone. + let mut rng = Lcg(0x5EA2_C401_9D3B_77E6); + let mut c = chain(&mut rng, 5); + c[2].0 = 0xA3; // CANDIDATES — a real slot, in the SEARCH band + + // (a) admission REFUSES it, and names the step so the rejection is + // actionable rather than a boolean. + assert_eq!( + validate_chain(&c), + Err(UnmintedOrdinal { + step: 2, + ordinal: 0xA3 + }), + ); + // Anti-vacuity: the same chain without that step must PASS, or the + // check could be rejecting everything. + let mut clean = c.clone(); + clean[2].0 = 0x90; + assert_eq!(validate_chain(&clean), Ok(())); + + // (b) replay stays TOTAL over it. Replay must not refuse history: a + // recorded chain is a fact, and a replay that judged content would + // start returning Err for chains that were valid when recorded — + // against the keystone this whole wave exists to hold. + let tables = NarsTables::build(1); + let c_tabs = compose_tables(); + let tabs = ComposeTables { + s: &c_tabs[0], + p: &c_tabs[1], + o: &c_tabs[2], + }; + let seed = edge(&mut rng); + let t = replay_chain(&c, seed, &tables, tabs, 1, 10).expect("reservation fits"); + assert_eq!(t.len(), 5); + assert_eq!( + t[2].predicate, 0xA3, + "the witness records what was replayed" + ); + } + + #[test] + fn a_reservation_that_cannot_fit_is_refused_before_a_partial_trace_exists() { + // CodeRabbit #1120: `base_seq + i` panicked in debug and wrapped in + // release. Wrapped coordinates alias the start of the durable log. + let tables = NarsTables::build(1); + let c_tabs = compose_tables(); + let tabs = ComposeTables { + s: &c_tabs[0], + p: &c_tabs[1], + o: &c_tabs[2], + }; + let mut rng = Lcg(0x77C1_0E5B_2A94_3D18); + let c = chain(&mut rng, 4); + let seed = edge(&mut rng); + + assert_eq!( + replay_chain(&c, seed, &tables, tabs, 1, u64::MAX).unwrap_err(), + ReplayError::SequenceExhausted { + base_seq: u64::MAX, + steps: 4 + }, + ); + + // Can-stay-silent, and NOT on a trivially small base: the last base + // that exactly fits a 4-step chain must still succeed, so the check + // rejects only what genuinely overflows rather than anything large. + let exact = u64::MAX - 3; + let t = + replay_chain(&c, seed, &tables, tabs, 1, exact).expect("the exact fit must be allowed"); + assert_eq!(t.last().unwrap().cast_seq(), u64::MAX); + + // A one-step chain at the very top fits: the reservation is half-open, + // so `steps - 1` is what has to be addable, not `steps`. + let one = &c[..1]; + assert!(replay_chain(one, seed, &tables, tabs, 1, u64::MAX).is_ok()); + + // An empty chain reserves nothing and cannot exhaust anything. + assert!(replay_chain(&[], seed, &tables, tabs, 1, u64::MAX) + .expect("empty reserves nothing") + .is_empty()); + } }