From a80d9ac007951d9430f38a3bf90bc99bc603e19a Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 3 Sep 2026 11:18:02 +0000 Subject: [PATCH 1/2] board: mint D-PRLR-1..5 for probe-r2il-live-regfile-v1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The second instance of the defect #1155 fixed for the parent plan, and one of the 53 counted in #1156's census: a GREEN probe with 18/18 and seven red-then-green disable runs, invisible to every discovery path because it carried no D-ids and no board rows. Ids are minted against sections that already exist; no scope added. Two of the five are worth reaching from an index rather than by reading 286 lines. D-PRLR-4: the §7.8 facet binding is a PROJECTION of the register file, never a byte-identity with SLEIGH's layout, because SLEIGH spans 55 bytes modelling each status flag as its own byte register while the semantic register file is 7 — pinned two-sided, so it fails if SLEIGH ever packs the 6502 into 12 bytes. D-PRLR-5: r2sleigh's CI has never run at all (total_count 0 workflow runs, ever; the workflow targets an unregistered self-hosted runner), so every green in the probe is a local run, as is the r2conc crate merged in r2sleigh PR #5. That row stays OPEN — moving to a hosted runner is an operator infra call, not a drive-by. Supersession index regenerated last, after the board writes; no diff. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01DCfrD5y19cvFc4AoyydXYv --- .claude/board/INTEGRATION_PLANS.md | 20 ++++++++++++++++++++ .claude/board/STATUS_BOARD.md | 17 +++++++++++++++++ 2 files changed, 37 insertions(+) diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 30adc2d59..7be26e2ee 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,23 @@ +## 2026-09-03 — `probe-r2il-live-regfile-v1` (PROBE, GREEN 2026-08-26) — BACKFILLED INDEX ENTRY + +`.claude/plans/probe-r2il-live-regfile-v1.md`. The executable falsifier for +`r2il-machine-semantic-contract-v1` §7.8: a real 6502 routine, lifted to R2IL by +Ghidra's own SLEIGH spec and executed through `r2conc::SlabState` with machine +state bound to borrowed slabs, must produce byte-identical architectural state to +an independently-written reference. GREEN, 18/18, seven disable runs +red-then-green. `D-PRLR-1..5` minted in the same commit. + +Two results worth finding from the index rather than by reading 286 lines. **The +facet binding is a projection, not a byte-identity** — SLEIGH lays the 6502 out +across 55 bytes because each status flag is its own byte register, while the +semantic register file is 7; §7.8's V4 binding survives, restated correctly. +And **r2sleigh's CI has never run** (`total_count: 0`, ever), so every green here +is local — the same "a gate that never runs is not a gate" lesson tesseract-rs +recorded, found by checking rather than by being bitten. + +Its parent plan was indexed 2026-09-03 (#1155); this probe was the second +instance of the same untracked-plan defect, counted in #1156's census. + ## 2026-09-03 — `r2il-machine-semantic-contract-v1` (PLAN, 2026-08-25) — BACKFILLED INDEX ENTRY `.claude/plans/r2il-machine-semantic-contract-v1.md`. Answers *"wie soll die diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index ce8e994fd..6c55512cd 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,3 +1,20 @@ +## probe-r2il-live-regfile-v1 (D-ids minted 2026-09-03; the plan shipped 2026-08-26) + +`.claude/plans/probe-r2il-live-regfile-v1.md`. The executable falsifier for +`r2il-machine-semantic-contract-v1` §7.8's V4 space binding. Untracked since it +landed and carrying no D-ids — one of the 53 counted in +`ISS-PLAN-TRACKING-IS-UNENFORCED` (#1156), and the second instance of the same +defect as its parent plan (#1155). Ids are minted against sections that already +exist; no scope is added. + +| D-id | deliverable | status | +|---|---|---| +| D-PRLR-1 | §2 the three-leg validity answer: side A's semantics are Ghidra's own SLEIGH spec (not ours), side B written in enforced isolation, side C arithmetic ground truth external to both | **Shipped 2026-08-26** — the design that makes the differential meaningful rather than self-confirming | +| D-PRLR-2 | §3/§7 the probe itself: a real 6502 routine lifted to R2IL and executed through `r2conc::SlabState` against an independent reference | **GREEN 2026-08-26** — 18/18, **seven disable runs red-then-green**. Code: r2sleigh `crates/r2conc/tests/{live_regfile,mos6502_oracle}.rs`, feature `probe-6502` | +| D-PRLR-3 | §6 the measured facts (each row naming what produced it, none predicted) | **Measured** — 6502 memory is `SpaceId::Ram` not `Custom(n)`; SLEIGH's register space spans **55 bytes** because each status flag is its own byte register, while the semantic register file is **7 bytes** | +| D-PRLR-4 | §6's consequence for §7.8: the facet binding is a **PROJECTION** of the register file, never a byte-identity with SLEIGH's layout | **Ruled + pinned two-sided** — `the_sleigh_register_space_is_sparse_so_the_facet_binding_is_a_projection` fails if SLEIGH ever packs the 6502 into 12 bytes, forcing a re-measure instead of letting a stale note stand | +| D-PRLR-5 | §9 the gate finding: **r2sleigh's CI has never run** — `--all-features` would execute this probe, but the repo reports `total_count: 0` workflow runs, ever (the workflow targets an unregistered self-hosted runner) | **OPEN, not fixed** — every green in §6/§7 is a LOCAL run, and the same holds for the `r2conc` crate merged in r2sleigh PR #5. Switching to a hosted runner is an operator infra call (the job compiles SLEIGH specs for every architecture), deliberately not a drive-by | + ## r2il-machine-semantic-contract-v1 (BACKFILLED 2026-09-03 — the plan shipped 2026-08-25 with NO board tracking) `.claude/plans/r2il-machine-semantic-contract-v1.md` (1427 lines). Untracked From abc5c8d8494c800f6b2ce6c3b6b717534bba2a22 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 3 Sep 2026 11:25:13 +0000 Subject: [PATCH 2/2] board: address Codex P2s on #1158 and record the board-only-mint gap MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two external P2s, both correct, and both my index entry over-claiming relative to the plan it indexes. P2-1: "byte-identical architectural state" drops the V exclusion. The plan's own §6a records that Ghidra's 6502 ADC assigns the unsigned carry to the signed-overflow flag, so on 255x255 both sides compute 0xFE01 and agree on every other field while Ghidra leaves V=1 and a real 6502 leaves V=0. V is excluded from the headline comparison and the exclusion is itself two-sided (falsifier D7). The entry now says "every field except V" and carries the finding rather than the summary. P2-2: labelling the probe "the executable falsifier for the V4 space binding" makes unfinished projection work look covered. The probe validates the lift-and-execute path against borrowed slabs; it never exercises a projection from SLEIGH's 55-byte layout into a 12-byte facet register. It measures the two layouts and concludes one is needed. Re-worded to "the EXECUTABLE HALF", with the misreading it is worded to prevent stated explicitly, and D-PRLR-4 regraded from "ruled" to "constraint measured, projection not built and not validated". Also recorded, found while verifying: the mint is board-only. D-PRLR-* and D-R2IL-* appear in STATUS_BOARD but not in the plans themselves, and supersession_index.py counts D-ids by scanning .claude/plans/, so the coverage column cannot see them. #1156's root cause is masked at the board layer, not closed. Writing ids into plan bodies is the real close and is out of scope for a board PR that said so. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01DCfrD5y19cvFc4AoyydXYv --- .claude/board/INTEGRATION_PLANS.md | 15 ++++++++++++--- .claude/board/STATUS_BOARD.md | 25 ++++++++++++++++++++----- 2 files changed, 32 insertions(+), 8 deletions(-) diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 7be26e2ee..35d5fd21d 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -3,9 +3,18 @@ `.claude/plans/probe-r2il-live-regfile-v1.md`. The executable falsifier for `r2il-machine-semantic-contract-v1` §7.8: a real 6502 routine, lifted to R2IL by Ghidra's own SLEIGH spec and executed through `r2conc::SlabState` with machine -state bound to borrowed slabs, must produce byte-identical architectural state to -an independently-written reference. GREEN, 18/18, seven disable runs -red-then-green. `D-PRLR-1..5` minted in the same commit. +state bound to borrowed slabs, must produce architectural state identical to an +independently-written reference **on every field except `V`**. GREEN, 18/18, +seven disable runs red-then-green. `D-PRLR-1..5` minted in the same commit. + +The `V` exclusion is the probe's own FINDING, not a weakening (§6a): Ghidra's +6502 `ADC` assigns the unsigned carry to the signed-overflow flag, so on +`255 × 255` both sides compute `0xFE01` and agree on every other field while +Ghidra leaves `V=1` and a real 6502 leaves `V=0`. The exclusion is itself tested +two-sided (falsifier D7 — it must diverge on some pairs and agree on others), and +the product is compared in full on every pair. Calling the result plain +"byte-identical" — as the first version of this entry did — overstates what the +18 checks establish. Two results worth finding from the index rather than by reading 286 lines. **The facet binding is a projection, not a byte-identity** — SLEIGH lays the 6502 out diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 6c55512cd..40dc39b1e 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,18 +1,33 @@ ## probe-r2il-live-regfile-v1 (D-ids minted 2026-09-03; the plan shipped 2026-08-26) -`.claude/plans/probe-r2il-live-regfile-v1.md`. The executable falsifier for -`r2il-machine-semantic-contract-v1` §7.8's V4 space binding. Untracked since it -landed and carrying no D-ids — one of the 53 counted in +`.claude/plans/probe-r2il-live-regfile-v1.md`. The falsifier for the EXECUTABLE +HALF of `r2il-machine-semantic-contract-v1` §7.8's V4 space binding: it validates +the lift-and-execute path against borrowed slabs. It does **NOT** exercise a +projection from SLEIGH's layout into a 12-byte V3 facet register — it measures +the two layouts and concludes one is needed. **The projection is unbuilt and +unvalidated**; reading this row as "the V4 binding is covered" is the misreading +it is worded to prevent. Untracked since it landed and carrying no D-ids — one of +the 53 counted in `ISS-PLAN-TRACKING-IS-UNENFORCED` (#1156), and the second instance of the same defect as its parent plan (#1155). Ids are minted against sections that already exist; no scope is added. | D-id | deliverable | status | |---|---|---| +> **⚠ The mint is BOARD-ONLY, and that does not close #1156's root cause.** +> `D-PRLR-1..5` exist in this file; `grep -c "D-PRLR" .claude/plans/probe-r2il-live-regfile-v1.md` +> → **0**. `supersession_index.py` counts D-ids by scanning `.claude/plans/*.md`, +> so a board-only mint is invisible to its coverage column. #1156 named the root +> cause as *"a plan without a D-id is unaddressable"* — this PR makes the plan +> addressable FROM the board, it does not put ids in the plan. Same for +> `D-R2IL-1..5` (#1155). Writing the ids into the two plans is the real close and +> is deliberately not done here: it edits plan bodies, which both of those PRs +> declared out of scope. + | D-PRLR-1 | §2 the three-leg validity answer: side A's semantics are Ghidra's own SLEIGH spec (not ours), side B written in enforced isolation, side C arithmetic ground truth external to both | **Shipped 2026-08-26** — the design that makes the differential meaningful rather than self-confirming | -| D-PRLR-2 | §3/§7 the probe itself: a real 6502 routine lifted to R2IL and executed through `r2conc::SlabState` against an independent reference | **GREEN 2026-08-26** — 18/18, **seven disable runs red-then-green**. Code: r2sleigh `crates/r2conc/tests/{live_regfile,mos6502_oracle}.rs`, feature `probe-6502` | +| D-PRLR-2 | §3/§7 the probe itself: a real 6502 routine lifted to R2IL and executed through `r2conc::SlabState` against an independent reference, all fields except `V` (see §6a — the `V` divergence is the probe's own finding, and the exclusion is falsifier-D7 two-sided) | **GREEN 2026-08-26** — 18/18, **seven disable runs red-then-green**. Code: r2sleigh `crates/r2conc/tests/{live_regfile,mos6502_oracle}.rs`, feature `probe-6502` | | D-PRLR-3 | §6 the measured facts (each row naming what produced it, none predicted) | **Measured** — 6502 memory is `SpaceId::Ram` not `Custom(n)`; SLEIGH's register space spans **55 bytes** because each status flag is its own byte register, while the semantic register file is **7 bytes** | -| D-PRLR-4 | §6's consequence for §7.8: the facet binding is a **PROJECTION** of the register file, never a byte-identity with SLEIGH's layout | **Ruled + pinned two-sided** — `the_sleigh_register_space_is_sparse_so_the_facet_binding_is_a_projection` fails if SLEIGH ever packs the 6502 into 12 bytes, forcing a re-measure instead of letting a stale note stand | +| D-PRLR-4 | §6's consequence for §7.8: the facet binding MUST be a **PROJECTION** of the register file, never a byte-identity with SLEIGH's layout | **Constraint measured + pinned two-sided; the projection itself is NOT built and NOT validated** — `the_sleigh_register_space_is_sparse_so_the_facet_binding_is_a_projection` fails if SLEIGH ever packs the 6502 into 12 bytes, forcing a re-measure instead of letting a stale note stand | | D-PRLR-5 | §9 the gate finding: **r2sleigh's CI has never run** — `--all-features` would execute this probe, but the repo reports `total_count: 0` workflow runs, ever (the workflow targets an unregistered self-hosted runner) | **OPEN, not fixed** — every green in §6/§7 is a LOCAL run, and the same holds for the `r2conc` crate merged in r2sleigh PR #5. Switching to a hosted runner is an operator infra call (the job compiles SLEIGH specs for every architecture), deliberately not a drive-by | ## r2il-machine-semantic-contract-v1 (BACKFILLED 2026-09-03 — the plan shipped 2026-08-25 with NO board tracking)