From 035af26dd91ff3141e5fef30e136f7365c1032de Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 18 Aug 2026 12:38:57 +0000 Subject: [PATCH 1/4] r2il: council SPEC v1 for the round-trip reconstruction oracle Phase-0 artifact of the 5+3 council convened on the PR2 gate deliverable (R2IL -> routes -> semantic-equivalent R2IL; SPO explicitly NOT the oracle). Frozen decisions with citations, verified input inventory, the committed resolution (facet::unproject, OpSkeleton equivalence, reconstruct/judge, permissive measurement convention, artifact-mediated arm), non-goals, pre-registered gates, and per-savant question sets. Draft v2 (post-savant consolidation) and the ratified v3 will amend this file in later commits on this branch. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01AGVLyRZNEKKBSfBDJfbY3V --- .../plans/r2il-roundtrip-oracle-spec-v1.md | 295 ++++++++++++++++++ 1 file changed, 295 insertions(+) create mode 100644 .claude/plans/r2il-roundtrip-oracle-spec-v1.md diff --git a/.claude/plans/r2il-roundtrip-oracle-spec-v1.md b/.claude/plans/r2il-roundtrip-oracle-spec-v1.md new file mode 100644 index 00000000000000..08b4a5355ff5b0 --- /dev/null +++ b/.claude/plans/r2il-roundtrip-oracle-spec-v1.md @@ -0,0 +1,295 @@ +# SPEC v1 — PR2 slice: the round-trip reconstruction oracle (`oracle.rs`) + +> 5+3 council spec (Phase 0). Orchestrator-authored. Savants verify/harden; +> they never design. Panel: default 5 lenses; reviewers: overclaim-auditor / +> dilution-collapse-sentinel / firewall-warden charters. +> +> Scope: the PR2 gate deliverable from `.claude/plans/r2il-behavioral-ir-v1.md` +> — "round-trip reconstruction oracle (R2IL → routes → semantic-equivalent +> R2IL; SPO explicitly NOT the oracle)". This slice follows PR #101 (sink +> trait + OfflineSink + O1) and PR #102 (v2 facts/residuals schemas + readers). + +## 1. FROZEN DECISIONS + +1. **SPO is NOT the oracle.** The comparison happens on typed r2il values, + never on a triple projection. (`r2il-behavioral-ir-v1.md:282-285`, and the + PR2 wave text `:377-380`.) +2. **Success = semantic/behavioral parity on TYPED values** — never textual, + never binary-artifact equality. (C4, `r2il-behavioral-ir-v1.md:277-285`.) +3. **Conservation is load-bearing.** `harvested == classified + residual`, + `dropped == 0` (`furnace.rs` `HarvestReport::is_conserved`). The oracle + extends the same reading: every source op is either reconstructed-equal or + ledger-accounted; a site that is neither is a FAILURE, not a footnote. + (C3, `r2il-behavioral-ir-v1.md:270-276`.) +4. **No persistence assumption enters `furnace`/`ore`/`slag`.** (SUBSTRATE + RULING, "PR-1 consequence" block.) +5. **`FlatFact` stays flat, `Copy`, exact 88-byte pin.** This slice adds NO + field to it. (`furnace.rs:163-207`, const assert.) +6. **Widening classification is a `R2ilConvention` DATA change, never a new + `smelt` match arm.** (`furnace.rs` module docs; `convention.rs:86-88`.) +7. **`ResidualReason` has no catch-all** and consumers render unknown reasons + as raw strings. (`slag.rs:80-119` + guide §4 rule 3.) +8. **`format!("{:?}")` is FORBIDDEN as a data path.** (plan, forbidden list.) +9. **Artifact discipline is additive; readers key off `#schema` names.** + This slice changes NO TSV schema — v2 (`sink.rs:173-177`) already carries + facet coords + `a`/`b` + full provenance, which is sufficient for + artifact-mediated reconstruction. (guide §4.) +10. **Falsifiability rule** (lance-graph CLAUDE.md, adopted by this crate's + practice): every new check gets a can-fire AND a can-stay-silent test, + plus manual disable-run verification recorded in the commit message. +11. **No model identifier in any committed artifact.** + +## 2. INPUT INVENTORY (verified this session unless marked VERIFY) + +- `crates/ruff_r2il/src/behavior.rs:57-70` `from_blocks_raw` (lossless + ingest; `from_blocks` runs SCCP and must NOT be used by the oracle); + `:188-218` provenance helpers `op_site`/`inst_at`/`value_var`. +- `crates/ruff_r2il/src/ore.rs` — `OreFact` emission (`enumerate`), operand + coordinates taken from typed source varnodes via `R2ILOp::inputs()` / + `output()` (`ore.rs:882-894`); `OpTag` ~85 variants with + `as_str`/`parse` (PR #102) and `from_r2il`/`from_op`; `FactProvenance + {inst, block, op_site, value}`. +- `crates/ruff_r2il/src/furnace.rs:112-140` `Concern`/`FactKind`; + `:167-179` `FlatFact{id, at, concern, kind, opcode, a, b, prov}`; payload + table (module docs `:62-77`): Op row `a`=ordinal, `b`=arity bits 0..32 | + has_output bit 32; OperandIn `a`=input index, `b`=ValueId+1; OperandOut + `a`=0; `smelt` `:262`; `VARIADIC_ARITY_THRESHOLD=3` `:95`; the pass-1 + ladder (module docs `:12-58`): operands melt iff facet-projects AND parent + melted AND `conv.resolve(&facet).is_some()`. +- `crates/ruff_r2il/src/slag.rs:80-119` `ResidualReason` (11 variants, + typed payloads); `ResidualFact{shape_id, reason, at, at_prefix, + provenance}`; `ResidualLedger`. +- `crates/ruff_r2il/src/facet.rs:49` `VarnodeFacet([u8;16])`; + `:222-244` `project` — discriminant map: Ram/Register/Unique/Const fixed + + `Custom(raw)` interned via `CustomSpaceTable` from + `CUSTOM_ORDINAL_BASE`; `FacetPrefix` `:94`. NO inverse exists today + (VERIFY: grep). `sink.rs` `facet_from_raw` (PR #102) rebuilds facet BYTES, + not a `Varnode`. +- `crates/ruff_r2il/src/convention.rs:80-110` `R2ilConvention` (radix rows + + `classified_opcodes` as data); `minimal_pass_one` = exactly + `[Copy, IntAdd, Load, Store, CBranch, Call, Return]`, ZERO rows — so under + it `conv.resolve` is `None` everywhere and NO operand row melts + (VERIFY consequence in smelt); `classifies` `:231`; `resolve` / + `resolved_prefix` `:215-229`. +- `crates/ruff_r2il/src/sink.rs:173-177` FACTS v2 / RESIDUALS v2 schemas; + `read_facts` / `read_residuals` (PR #102, round-trip tested). +- Upstream `r2sleigh/crates/r2il/src/opcode.rs:26` `R2ILOp` (~85 variants, + `PartialEq`); `:534` `output()`, `:691` `inputs()` — varnode-only + projections. **Non-varnode semantic state NOT covered by + inputs()/output()**: `Load`/`Store` `space: SpaceId`; `MemoryOrdering` on + `Fence`/`LoadLinked`/`StoreConditional`/`LoadGuarded`/`StoreGuarded`/ + `AtomicCAS` (VERIFY exact list); `CallOther` userop index (VERIFY whether + index reaches any fact row); possibly others (S3 enumerates). +- Upstream `r2il/src/varnode.rs:18-19` `Varnode{space, offset, size}` — + derive line shows `Debug, Clone, Serialize, Deserialize` and NOT + `PartialEq` (VERIFY: manual impl? `R2ILOp: PartialEq` requires it). + +## 3. THE PROPOSED RESOLUTION (committed) + +New module `crates/ruff_r2il/src/oracle.rs` + additions below. No other +source file changes semantics. + +### 3.1 `facet::unproject` (in `facet.rs`, beside `project`) + +`pub fn unproject(f: &VarnodeFacet, spaces: &CustomSpaceTable) -> +Option` — exact inverse of `project`: discriminant → `SpaceId` +(four fixed; custom via ordinal→raw reverse lookup — add a read-only +accessor on `CustomSpaceTable` if none exists). `None` only for an unknown +discriminant (typed refusal, mirroring `project`'s refusal posture; never a +guess). Property test: `unproject(project(vn)) == vn` over all four fixed +spaces + custom + 64-bit offsets; unknown-discriminant can-fire test. + +### 3.2 `OpSkeleton` — THE equivalence target + +```rust +pub struct OpSkeleton { pub opcode: OpTag, pub output: Option, + pub inputs: Vec } +impl OpSkeleton { pub fn of(op: &R2ILOp) -> Self /* from_r2il + output() + inputs() */ } +``` + +Semantic equivalence for this slice = skeleton equality at each source op +site. This is exactly the projection the routes carry (frozen 2: typed +parity, not binary equality). Non-varnode attributes are OUT of the skeleton +and INTO the measured gap channel (3.4) — never silently passed. + +### 3.3 `reconstruct` + +`pub fn reconstruct(rows: &[FlatFact], spaces: &CustomSpaceTable) -> +Reconstruction`: + +- Group `FactKind::Op` rows by `prov.op_site`; attach `OperandIn` rows (same + `prov.inst`, ordered by `a`) + the `OperandOut` row. +- Completeness per op (from the op row's OWN payload): OperandIn count == + arity (`b` bits 0..32) AND OperandOut presence == has_output (`b` bit 32). + Incomplete → `ReconstructionMiss::MissingOperands{site, have, need}` — + reported, never skipped. +- Operand facets → `facet::unproject`; failure → + `ReconstructionMiss::UnknownDiscriminant{site, index}`. +- Output: `Reconstruction{ ops: Vec, misses: Vec }`. + +### 3.4 `judge` — the verdict + +`pub fn judge(source: &[R2ILBlock], recon: &Reconstruction, +ledger: &ResidualLedger) -> OracleVerdict`: + +For every source op site `(block_addr, op_idx)` exactly one of: +(a) reconstructed AND `OpSkeleton::of(source_op) == reconstructed.skeleton` +→ `matched`; (b) named by ≥1 ledger residual anchored at that site (via +`provenance.op_site`, or block-anchored for reasons that carry only +`block`) → `ledger_accounted`; (c) neither → `orphans` entry. Skeleton +inequality → `mismatches` entry carrying both skeletons. + +`OracleVerdict{ matched, ledger_accounted, orphans, mismatches, +attribute_gaps }`, `fn holds() = orphans.is_empty() && +mismatches.is_empty()`. + +**Attribute-gap channel:** for each matched op whose source variant carries +non-varnode semantic state (the S3-verified list), emit +`AttributeGap{site, opcode, attribute: GapAttribute}` where `GapAttribute` +is a small typed enum (`MemorySpace`, `MemoryOrdering`, `UserOpIndex`, …). +This is deliberately NOT a `ResidualReason` — the furnace did not fail; the +schema deliberately projects. The gap census is the measured input for a +FUTURE additive widening decision (probe-first). Can-fire fixture: +Load/Fence; can-stay-silent fixture: Copy/IntAdd-only. + +### 3.5 Oracle convention (measurement config, not a shipped default) + +`pub fn permissive_convention(blocks: &[R2ILBlock]) -> R2ilConvention` in +`oracle.rs`: classify every `OpTag` present in `blocks` + insert +`FacetPrefix::Space` root rows for every discriminant the blocks' varnodes +project to. Pure config widening (frozen 6). Documented as the oracle's +measurement convention; `minimal_pass_one` remains the shipped default and +its stressor-slag acceptance tests are untouched. + +### 3.6 Artifact-mediated arm + +One test: smelt → `OfflineSink::write_harvest` → `read_facts` + +`read_residuals` → `reconstruct` + `judge` → verdict EQUAL to the in-memory +verdict. This is the load-bearing proof that the v2 schemas (PR #102) are +reconstruction-sufficient. Zero schema change (frozen 9). + +### 3.7 `lift`-gated example + harvest doc + +`examples/r2il_roundtrip_oracle.rs` (feature `lift`): run the oracle over +the same corpus as the §12 profile (r2sleigh e2e stress binaries; stripped +ELFs op-level), print matched / accounted / orphans / mismatches / +gap-census. Result recorded in `.claude/harvest/r2il/ORACLE-RESULT.md` +(cite-never-rederive, same footing as CORPUS-PROFILE-RESULT.md), and the +guide §1 stability table gains a row for it. Run in-session if build cost +permits; otherwise the doc records "example shipped, corpus run pending" +honestly. + +## 4. NON-GOALS + +- **Codebook wiring** (read `ogar_codebook`) — its own PR2 slice; different + blast radius (cross-repo read). +- **SPO projection of semantic facts** (calls/objects) — optional per plan, + sequenced after the oracle. +- **Closing the attribute gaps by widening FACTS/FlatFact now** — gated ON + this oracle's measured gap census (probe-first; frozen 5 protects the pin). +- **Changing `smelt`/ladder semantics** — the oracle measures the furnace. +- **lance-graph SoA sink (backend 2)** — downstream repo, per SUBSTRATE + RULING. +- **S3 signed PUT** — credential plumbing only remains, unchanged. + +## 5. PRE-REGISTERED GATES + +1. `cargo test` (crate dir) all green; total strictly above the current + 52 (40 lib + 12 integration). +2. `cargo clippy --all-targets -- -D warnings` clean; `cargo fmt --check` + clean; `uv run --only-group dev prek run --files ` clean. +3. Oracle fixture gates (each an automated test): + - full-melt fixture under `permissive_convention`: `holds()` AND + `matched == source op count` AND `ledger_accounted ==` exact phi + + CallDefine count — exact numbers, not `>=`. + - `minimal_pass_one` fixture: stressors land in ledger; still `holds()` + (accounted, not orphaned); anti-vacuity `matched >= 1 && + ledger_accounted >= 1`. + - mismatch can-fire (negative test IN the suite): corrupt one operand + row's facet offset → exactly one mismatch reported. + - orphan can-fire: drop one op's rows AND residuals → orphan reported. + - gap can-fire (Load or Fence) + can-stay-silent (Copy/IntAdd only). + - artifact-mediated verdict == in-memory verdict. + - `unproject∘project == id` (4 fixed spaces + custom + 64-bit offsets); + unknown discriminant → `None`. +4. Manual disable-run on ≥2 new tests (mutate → red → restore → green), + named in the commit message. +5. Diff confinement: `oracle.rs` (new), `facet.rs` (+`unproject` + + accessor only), `lib.rs` (module wiring), `tests/`, `examples/`, + `.claude/harvest/r2il/ORACLE-RESULT.md`, guide §1 row, this spec's + ratification note. NO diff in `furnace.rs`/`ore.rs`/`slag.rs`/`sink.rs` + semantics (doc-comment cross-refs allowed). + +## 6. PER-SAVANT QUESTION SETS + +Output contract (every savant): ≤10 findings, each = `(question #, verdict +∈ {CONFIRMS, VIOLATES, GAP, PRIOR-ART-AT, RISK}, file:line evidence, ≤2 +sentences)`. No prose essays. No redesigns — a redesign urge files one RISK +and stops. Read-only. + +### S1 — prior art +1. Does any existing code in ruff_r2il or r2sleigh already implement + facet→Varnode inversion or op-from-parts reconstruction (grep: + `unproject`, `reconstruct`, `from_facet`, `from_parts`, `build_op`)? +2. Does r2sleigh ship an R2ILOp constructor from (tag, output, inputs) the + skeleton could reuse instead of comparing projections? +3. Is there an existing permissive/test convention helper anywhere in + tests/examples that 3.5 would duplicate? +4. Do the plan/guide name an artifact filename convention that + `ORACLE-RESULT.md` should follow or that already exists? + +### S2 — iron rules / repo doctrine +1. Does the design keep SPO out of the oracle path end-to-end? (frozen 1) +2. Does anything in 3.x introduce a persistence assumption into + furnace/ore/slag? (frozen 4) +3. Any `Debug`-as-data path in skeleton compare, gap enum, or verdict + rendering? (frozen 8) +4. Is the artifact discipline strictly additive (no schema bump, new doc + + guide row only)? (frozen 9) +5. Does `permissive_convention` stay pure-config (frozen 6), or does any + part of the design require a new `smelt` arm? +6. RISK check: does the AttributeGap channel (a second accounting channel + beside the ledger) dilute the conservation ledger's authority (frozen + 3/7), or is it cleanly orthogonal (furnace-didn't-fail vs + furnace-failed)? + +### S3 — code truth (verify the spec against source) +1. Verify every file:line claim in §2, especially the payload-table + semantics used by 3.3 (Op `b` = arity|has_output<<32; OperandIn `a` = + index; op row and its operand rows share `prov.inst`). +2. Does `Varnode` implement `PartialEq` (derive or manual)? Cite the line. +3. Enumerate EXACTLY the R2ILOp variants whose semantic state exceeds + `inputs()`/`output()` — variant → lost attribute(s). This list becomes + `GapAttribute`. +4. Does `CustomSpaceTable` expose an ordinal→raw inverse today? If not, what + is the minimal read-only accessor? +5. Under `minimal_pass_one` (zero rows), confirm from `smelt`'s operand arm + that NO operand row melts (`conv.resolve` gate) — i.e. the oracle's + full-melt gate REQUIRES root rows. +6. For each `ResidualReason`, which provenance anchor does its + `ResidualFact` carry (`op_site` vs `block` vs none) — can `judge` + re-anchor every residual to a source op site, and what is the honest + rule for `Edge` (no prov at all)? + +### S4 — cascade impact +1. Complete the mandatory-same-commit file list (§5 gate 5) — anything + missed (plan Open-items update? STAGED-CODEGEN-GUIDE §1 table? lib.rs + docs? README?)? +2. Which existing tests could the new module break (name any test coupling + to facet.rs internals or convention defaults)? +3. Does adding `unproject` weaken the guide §1 caveat that the 16-byte + facet is "provisional — treat as opaque key, do not persist as durable + address"? What wording must the doc row carry? +4. Follow-up (not this slice) rows to file: gap-census → widening decision; + corpus oracle run if deferred; PR3 mint implications. + +### S5 — different views (no redesigns; strongest alternative + consequence) +1. Alternative: widen the schema NOW for full R2ILOp equality instead of + skeleton + gap census. Second-order consequence of deferring vs taking? +2. Alternative: judge by FORWARD comparison (re-smelt the reconstructed + blocks and diff row sets) instead of skeleton equality. Name each + approach's blind spot. +3. Does an oracle that holds under `permissive_convention` prove anything + about the shipped `minimal_pass_one`? Is the gate framing honest? +4. What does the gap census imply for PR3's classid-mint scope (one line)? From 7bb1f583bb1b2cad3038ad22e17b84f5baca16ef Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 18 Aug 2026 12:44:47 +0000 Subject: [PATCH 2/4] =?UTF-8?q?r2il:=20council=20draft=20v2=20=E2=80=94=20?= =?UTF-8?q?consolidate=20the=205=20savants'=20findings?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Phase-2 consolidation (before any reviewer): facet::unproject and CustomSpaceTable::raw_of already ship with the exact property tests v1 proposed, so 3.1 collapses to consuming them; the attribute-gap enumeration is corrected to the verified 12 variants / 5 kinds (adds Subpiece offset, PtrAdd/PtrSub element_size, Fence's empty skeleton); GapAttribute gains ResidualReason-style ALL/as_str/totality discipline; judge's universe is pinned to source op sites with an ssa_only_residuals channel for block-anchored residuals; the permissive-vs-shipped framing becomes normative; gate 5's file list gains Cargo.toml, README, and plan item O6. Full change ledger in section 7, losing findings recorded. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01AGVLyRZNEKKBSfBDJfbY3V --- .../plans/r2il-roundtrip-oracle-spec-v1.md | 468 +++++++++--------- 1 file changed, 225 insertions(+), 243 deletions(-) diff --git a/.claude/plans/r2il-roundtrip-oracle-spec-v1.md b/.claude/plans/r2il-roundtrip-oracle-spec-v1.md index 08b4a5355ff5b0..f3ec4d20ef08a9 100644 --- a/.claude/plans/r2il-roundtrip-oracle-spec-v1.md +++ b/.claude/plans/r2il-roundtrip-oracle-spec-v1.md @@ -1,295 +1,277 @@ -# SPEC v1 — PR2 slice: the round-trip reconstruction oracle (`oracle.rs`) +# SPEC — PR2 slice: the round-trip reconstruction oracle (`oracle.rs`) -> 5+3 council spec (Phase 0). Orchestrator-authored. Savants verify/harden; -> they never design. Panel: default 5 lenses; reviewers: overclaim-auditor / -> dilution-collapse-sentinel / firewall-warden charters. +> 5+3 council spec. **This file is DRAFT v2** (post-Phase-1 consolidation); +> v1 is the previous git revision of this file. Phase-3 reviewers see THIS +> document only. The change ledger (§7) records every savant finding and its +> disposition, including losing findings (anti-collapse). > > Scope: the PR2 gate deliverable from `.claude/plans/r2il-behavioral-ir-v1.md` > — "round-trip reconstruction oracle (R2IL → routes → semantic-equivalent -> R2IL; SPO explicitly NOT the oracle)". This slice follows PR #101 (sink -> trait + OfflineSink + O1) and PR #102 (v2 facts/residuals schemas + readers). +> R2IL; SPO explicitly NOT the oracle)". Follows PR #101 (sink trait + +> OfflineSink + O1) and PR #102 (v2 facts/residuals schemas + readers). ## 1. FROZEN DECISIONS 1. **SPO is NOT the oracle.** The comparison happens on typed r2il values, - never on a triple projection. (`r2il-behavioral-ir-v1.md:282-285`, and the - PR2 wave text `:377-380`.) + never on a triple projection. (`r2il-behavioral-ir-v1.md:282-285`, + `:377-380`.) [S2 Q1: CONFIRMS] 2. **Success = semantic/behavioral parity on TYPED values** — never textual, never binary-artifact equality. (C4, `r2il-behavioral-ir-v1.md:277-285`.) 3. **Conservation is load-bearing.** `harvested == classified + residual`, `dropped == 0` (`furnace.rs` `HarvestReport::is_conserved`). The oracle - extends the same reading: every source op is either reconstructed-equal or - ledger-accounted; a site that is neither is a FAILURE, not a footnote. - (C3, `r2il-behavioral-ir-v1.md:270-276`.) + extends the same reading over its own universe (§3.4): every SOURCE OP + SITE is reconstructed-equal or ledger-accounted; neither is a FAILURE. + (C3.) 4. **No persistence assumption enters `furnace`/`ore`/`slag`.** (SUBSTRATE - RULING, "PR-1 consequence" block.) + RULING.) [S2 Q2: CONFIRMS] 5. **`FlatFact` stays flat, `Copy`, exact 88-byte pin.** This slice adds NO - field to it. (`furnace.rs:163-207`, const assert.) -6. **Widening classification is a `R2ilConvention` DATA change, never a new - `smelt` match arm.** (`furnace.rs` module docs; `convention.rs:86-88`.) -7. **`ResidualReason` has no catch-all** and consumers render unknown reasons - as raw strings. (`slag.rs:80-119` + guide §4 rule 3.) -8. **`format!("{:?}")` is FORBIDDEN as a data path.** (plan, forbidden list.) -9. **Artifact discipline is additive; readers key off `#schema` names.** - This slice changes NO TSV schema — v2 (`sink.rs:173-177`) already carries - facet coords + `a`/`b` + full provenance, which is sufficient for - artifact-mediated reconstruction. (guide §4.) -10. **Falsifiability rule** (lance-graph CLAUDE.md, adopted by this crate's - practice): every new check gets a can-fire AND a can-stay-silent test, - plus manual disable-run verification recorded in the commit message. + field. (`furnace.rs:206-207` const assert.) +6. **Widening classification is `R2ilConvention` DATA, never a new `smelt` + arm.** (`furnace.rs` module docs; `convention.rs:88/205`.) + [S2 Q5: CONFIRMS — 3.5 uses only data-driven constructors] +7. **No catch-all discipline** extends to the NEW `GapAttribute` enum: it + gets `ALL`, `as_str`, and an exhaustiveness test mirroring + `ResidualReason` (`slag.rs:124+`). [S2 Q6 RISK, absorbed as a gate] +8. **`format!("{:?}")` is FORBIDDEN as a data path** — and this now + explicitly covers verdict/skeleton RENDERING: the example's printed + report and `ORACLE-RESULT.md` numbers are produced from typed fields and + `as_str()` only. `Debug` remains legal solely inside test-assertion + failure messages (a diagnostic on a failing test is not a data path). + [S2 Q3 VIOLATES, fixed here] +9. **Artifact discipline additive; no TSV schema change.** v2 schemas + (`sink.rs:173-177`) are sufficient (proven by §3.6's arm). [S2 Q4] +10. **Falsifiability rule**: can-fire + can-stay-silent per guard; manual + disable-runs recorded in the commit message. 11. **No model identifier in any committed artifact.** -## 2. INPUT INVENTORY (verified this session unless marked VERIFY) - -- `crates/ruff_r2il/src/behavior.rs:57-70` `from_blocks_raw` (lossless - ingest; `from_blocks` runs SCCP and must NOT be used by the oracle); - `:188-218` provenance helpers `op_site`/`inst_at`/`value_var`. -- `crates/ruff_r2il/src/ore.rs` — `OreFact` emission (`enumerate`), operand - coordinates taken from typed source varnodes via `R2ILOp::inputs()` / - `output()` (`ore.rs:882-894`); `OpTag` ~85 variants with - `as_str`/`parse` (PR #102) and `from_r2il`/`from_op`; `FactProvenance - {inst, block, op_site, value}`. -- `crates/ruff_r2il/src/furnace.rs:112-140` `Concern`/`FactKind`; - `:167-179` `FlatFact{id, at, concern, kind, opcode, a, b, prov}`; payload - table (module docs `:62-77`): Op row `a`=ordinal, `b`=arity bits 0..32 | - has_output bit 32; OperandIn `a`=input index, `b`=ValueId+1; OperandOut - `a`=0; `smelt` `:262`; `VARIADIC_ARITY_THRESHOLD=3` `:95`; the pass-1 - ladder (module docs `:12-58`): operands melt iff facet-projects AND parent - melted AND `conv.resolve(&facet).is_some()`. -- `crates/ruff_r2il/src/slag.rs:80-119` `ResidualReason` (11 variants, - typed payloads); `ResidualFact{shape_id, reason, at, at_prefix, - provenance}`; `ResidualLedger`. -- `crates/ruff_r2il/src/facet.rs:49` `VarnodeFacet([u8;16])`; - `:222-244` `project` — discriminant map: Ram/Register/Unique/Const fixed - + `Custom(raw)` interned via `CustomSpaceTable` from - `CUSTOM_ORDINAL_BASE`; `FacetPrefix` `:94`. NO inverse exists today - (VERIFY: grep). `sink.rs` `facet_from_raw` (PR #102) rebuilds facet BYTES, - not a `Varnode`. -- `crates/ruff_r2il/src/convention.rs:80-110` `R2ilConvention` (radix rows + - `classified_opcodes` as data); `minimal_pass_one` = exactly - `[Copy, IntAdd, Load, Store, CBranch, Call, Return]`, ZERO rows — so under - it `conv.resolve` is `None` everywhere and NO operand row melts - (VERIFY consequence in smelt); `classifies` `:231`; `resolve` / - `resolved_prefix` `:215-229`. -- `crates/ruff_r2il/src/sink.rs:173-177` FACTS v2 / RESIDUALS v2 schemas; - `read_facts` / `read_residuals` (PR #102, round-trip tested). -- Upstream `r2sleigh/crates/r2il/src/opcode.rs:26` `R2ILOp` (~85 variants, - `PartialEq`); `:534` `output()`, `:691` `inputs()` — varnode-only - projections. **Non-varnode semantic state NOT covered by - inputs()/output()**: `Load`/`Store` `space: SpaceId`; `MemoryOrdering` on - `Fence`/`LoadLinked`/`StoreConditional`/`LoadGuarded`/`StoreGuarded`/ - `AtomicCAS` (VERIFY exact list); `CallOther` userop index (VERIFY whether - index reaches any fact row); possibly others (S3 enumerates). -- Upstream `r2il/src/varnode.rs:18-19` `Varnode{space, offset, size}` — - derive line shows `Debug, Clone, Serialize, Deserialize` and NOT - `PartialEq` (VERIFY: manual impl? `R2ILOp: PartialEq` requires it). - -## 3. THE PROPOSED RESOLUTION (committed) - -New module `crates/ruff_r2il/src/oracle.rs` + additions below. No other -source file changes semantics. - -### 3.1 `facet::unproject` (in `facet.rs`, beside `project`) - -`pub fn unproject(f: &VarnodeFacet, spaces: &CustomSpaceTable) -> -Option` — exact inverse of `project`: discriminant → `SpaceId` -(four fixed; custom via ordinal→raw reverse lookup — add a read-only -accessor on `CustomSpaceTable` if none exists). `None` only for an unknown -discriminant (typed refusal, mirroring `project`'s refusal posture; never a -guess). Property test: `unproject(project(vn)) == vn` over all four fixed -spaces + custom + 64-bit offsets; unknown-discriminant can-fire test. +## 2. INPUT INVENTORY (savant-verified; corrections from v1 marked ✎) + +- `behavior.rs:57-70` `from_blocks_raw` (lossless; `from_blocks` runs SCCP — + forbidden for the oracle); `:188-218` provenance helpers. +- `ore.rs:841-899` — Op row and its Operand rows share the identical + `base_prov` (`inst: Some(inst_id)`) [S3 Q1 CONFIRMS]; phi facts hardcode + `op_site: None` (`ore.rs:824-829, 941-949`) [S3 Q6]. +- `furnace.rs:280-408, 791-793` — payload semantics CONFIRMED: Op `a` = + ordinal, `b` = `input_arity | (has_output << 32)` via `pack_op_metadata`; + OperandIn `a` = index, `b` = `ValueId.0+1`. Operand melt gate + `conv.resolve(&facet).is_some()` at `:350`; unresolved → + `NoConventionRowAtAddress` (`:371-377`). +- `slag.rs:80-118` `ResidualReason` (11 variants). ✎ Provenance anchors per + reason [S3 Q6]: all op-derived reasons carry the parent op's full `prov` + (with `op_site: Some`); `PhiFanInExceedsPredecessors` and phi/CallDefine + `NoFacetCoordinate` are block-anchored only (`op_site: None`); the Edge + no-facet case carries a furnace-SYNTHESIZED `prov{block: Some(from)}` + (`furnace.rs:421-426`). ✎ `UserOpNotInConvention` is NEVER constructed by + the current ladder (dead variant) — recorded, out of scope to fix. +- ✎ `facet.rs:246-261` — **`unproject(f, spaces) -> Result` ALREADY EXISTS**, with the exact property tests v1 + proposed (`fixed_spaces_round_trip_byte_for_byte`, + `custom_space_within_budget_round_trips`, + `custom_space_outside_the_table_errors_and_never_truncates`, + `offsets_above_u32_max_survive_the_lo_hi_split`). `CustomSpaceTable:: + raw_of` (`facet.rs:196-206`) is the ordinal→raw inverse. v1's "no inverse + exists" was WRONG. [S1/S3/S4 unanimous] +- `convention.rs:98-114` `minimal_pass_one` = 7 opcodes, ZERO rows ⇒ + `resolve` always `None` ⇒ NO operand row ever melts under it [S3 Q5 + CONFIRMS]. No existing test couples to its row contents [S4 CONFIRMS]. +- `sink.rs:173-177` FACTS/RESIDUALS v2 + `read_facts`/`read_residuals`. +- `r2il/src/opcode.rs:26-495` `R2ILOp` (`PartialEq`); `:534 output()`, + `:691 inputs()`. ✎ `varnode.rs:149-155`: `Varnode` has a MANUAL + `PartialEq` over `space`/`offset`/`size` only (excludes `meta`) — so + `unproject`'s output compares correctly. [S1/S3] +- ✎ **The verified attribute-gap enumeration — 12 variants, 5 attribute + kinds** [S3 Q3, replaces v1's 7-variant guess]: + + | variant(s) | lost attribute(s) | + |---|---| + | `Load`, `Store` | `space: SpaceId` | + | `Fence` | `ordering: MemoryOrdering` — AND zero varnode fields: its skeleton is `(Fence, None, [])`, trivially equal; the gap channel carries ALL its semantics | + | `LoadLinked`, `StoreConditional`, `AtomicCAS`, `LoadGuarded`, `StoreGuarded` | `space` AND `ordering` | + | `CallOther` | `userop: u32` (`opcode.rs:425`) | + | `Subpiece` | `offset: u32` (`opcode.rs:301`) | + | `PtrAdd`, `PtrSub` | `element_size: u32` (`opcode.rs:457/465`) | + +- No op-builder `(tag, output, inputs) -> R2ILOp` exists anywhere + [S1 Q2 GAP] — projection comparison is the only viable equivalence path, + which independently validates §3.2's design. +- `*-RESULT.md` naming convention confirmed (`CORPUS-PROFILE-RESULT.md:5`) + [S1 Q4]. + +## 3. THE RESOLUTION (committed; v1 deltas marked ✎) + +New module `crates/ruff_r2il/src/oracle.rs`. `facet.rs` gets **no code +change** (✎ — at most a doc-comment cross-reference). + +### 3.1 ✎ Facet inversion: CONSUME `facet::unproject`, build nothing + +The oracle uses the shipped `facet::unproject` and `CustomSpaceTable:: +raw_of` as-is. `FacetOverflow` from `unproject` maps to +`ReconstructionMiss::FacetInversion{site, index, raw}` (carrying the +overflow's own payload) — no bespoke `Option` shape, no duplicate inverse, +no new accessor. The already-shipped round-trip property tests stand as the +inversion gates; the oracle adds none. ### 3.2 `OpSkeleton` — THE equivalence target ```rust pub struct OpSkeleton { pub opcode: OpTag, pub output: Option, pub inputs: Vec } -impl OpSkeleton { pub fn of(op: &R2ILOp) -> Self /* from_r2il + output() + inputs() */ } +impl OpSkeleton { pub fn of(op: &R2ILOp) -> Self /* from_r2il + output().cloned() + inputs() cloned */ } ``` Semantic equivalence for this slice = skeleton equality at each source op -site. This is exactly the projection the routes carry (frozen 2: typed -parity, not binary equality). Non-varnode attributes are OUT of the skeleton -and INTO the measured gap channel (3.4) — never silently passed. +site (Varnode's own `PartialEq`: space/offset/size). Non-varnode attributes +are OUT of the skeleton and INTO the measured gap channel (3.4). ### 3.3 `reconstruct` `pub fn reconstruct(rows: &[FlatFact], spaces: &CustomSpaceTable) -> Reconstruction`: -- Group `FactKind::Op` rows by `prov.op_site`; attach `OperandIn` rows (same - `prov.inst`, ordered by `a`) + the `OperandOut` row. -- Completeness per op (from the op row's OWN payload): OperandIn count == - arity (`b` bits 0..32) AND OperandOut presence == has_output (`b` bit 32). - Incomplete → `ReconstructionMiss::MissingOperands{site, have, need}` — - reported, never skipped. -- Operand facets → `facet::unproject`; failure → - `ReconstructionMiss::UnknownDiscriminant{site, index}`. +- Group `FactKind::Op` rows by `prov.op_site`; attach `OperandIn` rows + (same `prov.inst`, ordered by `a`) + the `OperandOut` row. +- Completeness per op (from the op row's own payload, `b` = arity | + has_output<<32): OperandIn count == arity AND OperandOut presence == + has_output; incomplete → `ReconstructionMiss::MissingOperands{site, + have, need}` — reported, never skipped. +- Operand facets → `facet::unproject`; `Err(FacetOverflow)` → + `ReconstructionMiss::FacetInversion` (✎ per 3.1). - Output: `Reconstruction{ ops: Vec, misses: Vec }`. -### 3.4 `judge` — the verdict +### 3.4 `judge` — the verdict, with a PINNED universe ✎ -`pub fn judge(source: &[R2ILBlock], recon: &Reconstruction, -ledger: &ResidualLedger) -> OracleVerdict`: +**Universe = source op sites** `(block_addr, op_idx)` enumerated from the +input `&[R2ILBlock]`. For each site exactly one of: (a) reconstructed AND +`OpSkeleton::of(source_op) == skeleton` → `matched`; (b) ≥1 ledger residual +whose `provenance.op_site` equals the site → `ledger_accounted`; (c) +neither → `orphans`. Skeleton inequality → `mismatches` (both skeletons +carried as typed values). -For every source op site `(block_addr, op_idx)` exactly one of: -(a) reconstructed AND `OpSkeleton::of(source_op) == reconstructed.skeleton` -→ `matched`; (b) named by ≥1 ledger residual anchored at that site (via -`provenance.op_site`, or block-anchored for reasons that carry only -`block`) → `ledger_accounted`; (c) neither → `orphans` entry. Skeleton -inequality → `mismatches` entry carrying both skeletons. +✎ **Ledger rows OUTSIDE the universe** — residuals with `op_site: None` +(phi inputs, CallDefine, the Edge no-facet case; S3 Q6's anchor table) — +account for SSA-level facts that have no source op site. They are counted +as `ssa_only_residuals: usize` in the verdict, never errors and never +silently dropped. `holds()` = `orphans.is_empty() && mismatches.is_empty()`. -`OracleVerdict{ matched, ledger_accounted, orphans, mismatches, -attribute_gaps }`, `fn holds() = orphans.is_empty() && -mismatches.is_empty()`. +**Attribute-gap channel:** for each matched op whose variant appears in +§2's 12-variant table, emit `AttributeGap{site, opcode, attribute}` with -**Attribute-gap channel:** for each matched op whose source variant carries -non-varnode semantic state (the S3-verified list), emit -`AttributeGap{site, opcode, attribute: GapAttribute}` where `GapAttribute` -is a small typed enum (`MemorySpace`, `MemoryOrdering`, `UserOpIndex`, …). -This is deliberately NOT a `ResidualReason` — the furnace did not fail; the -schema deliberately projects. The gap census is the measured input for a -FUTURE additive widening decision (probe-first). Can-fire fixture: -Load/Fence; can-stay-silent fixture: Copy/IntAdd-only. +```rust +pub enum GapAttribute { MemorySpace, MemoryOrdering, UserOpIndex, + SubpieceOffset, PtrElementSize } +``` + +✎ Discipline mirrors `ResidualReason` (frozen 7): `GapAttribute::ALL`, +`as_str`, a no-catch-all test, AND the variant→gap mapping lives as ONE +total `fn gaps_of(tag: OpTag) -> &'static [GapAttribute]` match whose +completeness over the 12 variants is asserted by test (each of the 12 +returns non-empty; a spot-check set of non-gap tags returns empty). Not a +`ResidualReason` — the furnace did not fail; the schema deliberately +projects. The census is the measured input for a FUTURE additive widening +decision, tracked as plan item O6 (§5 gate 5). ### 3.5 Oracle convention (measurement config, not a shipped default) `pub fn permissive_convention(blocks: &[R2ILBlock]) -> R2ilConvention` in -`oracle.rs`: classify every `OpTag` present in `blocks` + insert -`FacetPrefix::Space` root rows for every discriminant the blocks' varnodes -project to. Pure config widening (frozen 6). Documented as the oracle's -measurement convention; `minimal_pass_one` remains the shipped default and -its stressor-slag acceptance tests are untouched. +`oracle.rs`: classify every `OpTag` present + insert `FacetPrefix::Space` +root rows for every discriminant the blocks' varnodes project to. Pure +config (frozen 6; S2 Q5 CONFIRMS). No prior art duplicated (S1 Q3). + +✎ **Honest framing (normative, from S5 Q3):** a verdict that holds under +`permissive_convention` proves the reconstruction MECHANISM (facet +inversion + grouping + skeleton compare) — it says nothing about the +shipped `minimal_pass_one`'s coverage, under which no operand melts and +accounting dominates. `oracle.rs` module docs and `ORACLE-RESULT.md` MUST +state this, and the corpus example reports BOTH conventions' numbers so the +census shows what the shipped default actually covers. ### 3.6 Artifact-mediated arm -One test: smelt → `OfflineSink::write_harvest` → `read_facts` + -`read_residuals` → `reconstruct` + `judge` → verdict EQUAL to the in-memory -verdict. This is the load-bearing proof that the v2 schemas (PR #102) are -reconstruction-sufficient. Zero schema change (frozen 9). +smelt → `OfflineSink::write_harvest` → `read_facts` + `read_residuals` → +`reconstruct` + `judge` → verdict EQUAL to the in-memory verdict. Proves +the v2 schemas are reconstruction-sufficient. Zero schema change. ### 3.7 `lift`-gated example + harvest doc -`examples/r2il_roundtrip_oracle.rs` (feature `lift`): run the oracle over -the same corpus as the §12 profile (r2sleigh e2e stress binaries; stripped -ELFs op-level), print matched / accounted / orphans / mismatches / -gap-census. Result recorded in `.claude/harvest/r2il/ORACLE-RESULT.md` -(cite-never-rederive, same footing as CORPUS-PROFILE-RESULT.md), and the -guide §1 stability table gains a row for it. Run in-session if build cost -permits; otherwise the doc records "example shipped, corpus run pending" -honestly. - -## 4. NON-GOALS - -- **Codebook wiring** (read `ogar_codebook`) — its own PR2 slice; different - blast radius (cross-repo read). -- **SPO projection of semantic facts** (calls/objects) — optional per plan, - sequenced after the oracle. -- **Closing the attribute gaps by widening FACTS/FlatFact now** — gated ON - this oracle's measured gap census (probe-first; frozen 5 protects the pin). -- **Changing `smelt`/ladder semantics** — the oracle measures the furnace. -- **lance-graph SoA sink (backend 2)** — downstream repo, per SUBSTRATE - RULING. -- **S3 signed PUT** — credential plumbing only remains, unchanged. +`examples/r2il_roundtrip_oracle.rs` (feature `lift`; ✎ requires its own +`[[example]] required-features` stanza in `Cargo.toml` — S4): corpus run +per §3.5's dual-convention rule; results → +`.claude/harvest/r2il/ORACLE-RESULT.md`; run in-session if build cost +permits, else the doc records "example shipped, corpus run pending" and +plan item O6 tracks it (✎ S4 Q4). + +## 4. NON-GOALS (unchanged from v1) + +- Codebook wiring (`ogar_codebook`) — own PR2 slice. +- SPO projection of semantic facts — after the oracle. +- Closing attribute gaps by widening FACTS/FlatFact now — gated on O6's + census (S5 Q1: the census MUST be tracked or the loss goes permanent; + hence O6 is mandatory-same-commit). +- Changing `smelt`/ladder semantics; fixing the dead `UserOpNotInConvention` + variant (recorded, untouched). +- lance-graph SoA sink; S3 signed PUT. ## 5. PRE-REGISTERED GATES -1. `cargo test` (crate dir) all green; total strictly above the current - 52 (40 lib + 12 integration). -2. `cargo clippy --all-targets -- -D warnings` clean; `cargo fmt --check` - clean; `uv run --only-group dev prek run --files ` clean. -3. Oracle fixture gates (each an automated test): - - full-melt fixture under `permissive_convention`: `holds()` AND - `matched == source op count` AND `ledger_accounted ==` exact phi + - CallDefine count — exact numbers, not `>=`. - - `minimal_pass_one` fixture: stressors land in ledger; still `holds()` - (accounted, not orphaned); anti-vacuity `matched >= 1 && - ledger_accounted >= 1`. - - mismatch can-fire (negative test IN the suite): corrupt one operand - row's facet offset → exactly one mismatch reported. - - orphan can-fire: drop one op's rows AND residuals → orphan reported. - - gap can-fire (Load or Fence) + can-stay-silent (Copy/IntAdd only). +1. `cargo test` (crate dir) all green; total strictly above 52. +2. `cargo clippy --all-targets -- -D warnings`, `cargo fmt --check`, + `uv run --only-group dev prek run --files ` — all clean. +3. Oracle test gates (automated): + - full-melt fixture under `permissive_convention`: `holds()`, `matched + == source op count` (exact), `ledger_accounted == 0` (exact), + `ssa_only_residuals ==` exact phi+CallDefine count. + - `minimal_pass_one` fixture: still `holds()` (accounted, not + orphaned); anti-vacuity `matched >= 1 && ledger_accounted >= 1`; PLUS + the framing assertion that `matched` under minimal < `matched` under + permissive on the same blocks (proves the two conventions measure + different things — S5 Q3). + - mismatch can-fire: corrupt one operand row's facet → exactly one + mismatch. ✎ swap can-fire (S5 Q2): swap two operand rows' facets + ACROSS two ops → BOTH sites report mismatches (cross-row corruption + is visible, not cancelled). + - orphan can-fire: drop one op's rows AND its residuals → orphan. + - gap can-fire: Load (MemorySpace) and Fence (MemoryOrdering, empty + skeleton); can-stay-silent: Copy/IntAdd-only → zero gaps. + - `gaps_of` completeness: all 12 table variants non-empty; non-gap tags + empty; `GapAttribute::ALL` no-catch-all test (frozen 7). - artifact-mediated verdict == in-memory verdict. - - `unproject∘project == id` (4 fixed spaces + custom + 64-bit offsets); - unknown discriminant → `None`. -4. Manual disable-run on ≥2 new tests (mutate → red → restore → green), - named in the commit message. -5. Diff confinement: `oracle.rs` (new), `facet.rs` (+`unproject` + - accessor only), `lib.rs` (module wiring), `tests/`, `examples/`, - `.claude/harvest/r2il/ORACLE-RESULT.md`, guide §1 row, this spec's - ratification note. NO diff in `furnace.rs`/`ore.rs`/`slag.rs`/`sink.rs` - semantics (doc-comment cross-refs allowed). - -## 6. PER-SAVANT QUESTION SETS - -Output contract (every savant): ≤10 findings, each = `(question #, verdict -∈ {CONFIRMS, VIOLATES, GAP, PRIOR-ART-AT, RISK}, file:line evidence, ≤2 -sentences)`. No prose essays. No redesigns — a redesign urge files one RISK -and stops. Read-only. - -### S1 — prior art -1. Does any existing code in ruff_r2il or r2sleigh already implement - facet→Varnode inversion or op-from-parts reconstruction (grep: - `unproject`, `reconstruct`, `from_facet`, `from_parts`, `build_op`)? -2. Does r2sleigh ship an R2ILOp constructor from (tag, output, inputs) the - skeleton could reuse instead of comparing projections? -3. Is there an existing permissive/test convention helper anywhere in - tests/examples that 3.5 would duplicate? -4. Do the plan/guide name an artifact filename convention that - `ORACLE-RESULT.md` should follow or that already exists? - -### S2 — iron rules / repo doctrine -1. Does the design keep SPO out of the oracle path end-to-end? (frozen 1) -2. Does anything in 3.x introduce a persistence assumption into - furnace/ore/slag? (frozen 4) -3. Any `Debug`-as-data path in skeleton compare, gap enum, or verdict - rendering? (frozen 8) -4. Is the artifact discipline strictly additive (no schema bump, new doc + - guide row only)? (frozen 9) -5. Does `permissive_convention` stay pure-config (frozen 6), or does any - part of the design require a new `smelt` arm? -6. RISK check: does the AttributeGap channel (a second accounting channel - beside the ledger) dilute the conservation ledger's authority (frozen - 3/7), or is it cleanly orthogonal (furnace-didn't-fail vs - furnace-failed)? - -### S3 — code truth (verify the spec against source) -1. Verify every file:line claim in §2, especially the payload-table - semantics used by 3.3 (Op `b` = arity|has_output<<32; OperandIn `a` = - index; op row and its operand rows share `prov.inst`). -2. Does `Varnode` implement `PartialEq` (derive or manual)? Cite the line. -3. Enumerate EXACTLY the R2ILOp variants whose semantic state exceeds - `inputs()`/`output()` — variant → lost attribute(s). This list becomes - `GapAttribute`. -4. Does `CustomSpaceTable` expose an ordinal→raw inverse today? If not, what - is the minimal read-only accessor? -5. Under `minimal_pass_one` (zero rows), confirm from `smelt`'s operand arm - that NO operand row melts (`conv.resolve` gate) — i.e. the oracle's - full-melt gate REQUIRES root rows. -6. For each `ResidualReason`, which provenance anchor does its - `ResidualFact` carry (`op_site` vs `block` vs none) — can `judge` - re-anchor every residual to a source op site, and what is the honest - rule for `Edge` (no prov at all)? - -### S4 — cascade impact -1. Complete the mandatory-same-commit file list (§5 gate 5) — anything - missed (plan Open-items update? STAGED-CODEGEN-GUIDE §1 table? lib.rs - docs? README?)? -2. Which existing tests could the new module break (name any test coupling - to facet.rs internals or convention defaults)? -3. Does adding `unproject` weaken the guide §1 caveat that the 16-byte - facet is "provisional — treat as opaque key, do not persist as durable - address"? What wording must the doc row carry? -4. Follow-up (not this slice) rows to file: gap-census → widening decision; - corpus oracle run if deferred; PR3 mint implications. - -### S5 — different views (no redesigns; strongest alternative + consequence) -1. Alternative: widen the schema NOW for full R2ILOp equality instead of - skeleton + gap census. Second-order consequence of deferring vs taking? -2. Alternative: judge by FORWARD comparison (re-smelt the reconstructed - blocks and diff row sets) instead of skeleton equality. Name each - approach's blind spot. -3. Does an oracle that holds under `permissive_convention` prove anything - about the shipped `minimal_pass_one`? Is the gate framing honest? -4. What does the gap census imply for PR3's classid-mint scope (one line)? + - ✎ NO new facet round-trip tests (they exist; re-running them is the + gate). +4. Manual disable-run on ≥2 new tests, named in the commit message. +5. ✎ Diff confinement (corrected + completed per S4): `oracle.rs` (new), + `lib.rs` (module wiring + module-table row), `Cargo.toml` + (`[[example]]` stanza), `tests/` (new oracle fixture file), `examples/ + r2il_roundtrip_oracle.rs`, `.claude/harvest/r2il/ORACLE-RESULT.md` + (new), `.claude/harvest/r2il/STAGED-CODEGEN-GUIDE.md` (§1: ONE new row + for ORACLE-RESULT; the `VarnodeFacet ⚠ provisional` row is NOT edited — + S4 Q3: unproject recovers a typed Varnode, not a durable address, so + the persistence caveat is orthogonal), `.claude/harvest/r2il/README.md` + (entry for the new example/artifact pair), `.claude/plans/ + r2il-behavioral-ir-v1.md` (new Open item **O6**: gap-census → widening + decision; corpus-run-pending state; PR3 mint-scope note per S5 Q4), + this spec (ratification note). `facet.rs`: doc-comment cross-ref at + most. NO semantic diff in `furnace.rs`/`ore.rs`/`slag.rs`/`sink.rs`. + +## 6. PER-SAVANT QUESTION SETS — retired (Phase 1 complete) + +Question sets from v1 were answered; findings and dispositions in §7. + +## 7. CHANGE LEDGER v1 → v2 (every finding, its disposition) + +| # | savant, verdict | finding | disposition | +|---|---|---|---| +| 1 | S1/S3/S4 VIOLATES | `unproject` + `raw_of` already shipped with the exact tests v1 proposed | §3.1 rewritten to CONSUME; facet.rs code diff = zero; gates drop the duplicate tests | +| 2 | S1 RISK | real signature is `Result<_, FacetOverflow>`, not `Option` | §3.1/§3.3: `FacetInversion` miss maps the real error | +| 3 | S1 GAP/CONFIRMS | no op-builder exists; skeleton comparison is the only path | design validated; noted in §2 | +| 4 | S2 VIOLATES | no-Debug rule not stated for verdict rendering | frozen 8 extended; rendering rule normative | +| 5 | S2 RISK | `GapAttribute` lacked ResidualReason-style exhaustiveness | §3.4: `ALL` + `as_str` + `gaps_of` totality test; gate 3 | +| 6 | S3 GAP | gap enumeration is 12 variants/5 kinds, incl. `Subpiece`/`PtrAdd`/`PtrSub`/`Fence`-empty-skeleton | §2 table replaces v1 guess; `GapAttribute` gains `SubpieceOffset`, `PtrElementSize` | +| 7 | S3 CONFIRMS | payload semantics, shared `prov.inst`, Varnode manual `PartialEq`, minimal-pass-one no-operand-melt | inventory marked verified | +| 8 | S3 RISK | provenance anchors: phi/Edge block-only; `UserOpNotInConvention` dead | §3.4 universe pinned; `ssa_only_residuals` channel; dead variant recorded in §4 | +| 9 | S4 GAP ×4 | Cargo.toml stanza, README entry, plan O6, guide row missing from file list | gate 5 completed | +| 10 | S4 Q1 (partial) vs S4 Q3 | Q1 said the provisional facet row needs in-place edit; Q3 (deeper) says orthogonal | **Q3 wins** — no edit; losing finding recorded here per anti-collapse | +| 11 | S5 RISK | deferring widening is safe only if census is tracked | O6 mandatory-same-commit (§5) | +| 12 | S5 RISK | forward re-smelt oracle tests furnace against itself; skeleton misses cross-row swaps | direction confirmed; swap can-fire added to gate 3 | +| 13 | S5 RISK | permissive pass ≠ shipped-coverage proof | §3.5 honest-framing normative + dual-convention reporting + minimal Date: Tue, 18 Aug 2026 12:47:32 +0000 Subject: [PATCH 3/4] =?UTF-8?q?r2il:=20ratify=20council=20spec=20v3=20?= =?UTF-8?q?=E2=80=94=20apply=20the=203=20reviewers'=20five=20FIX=20finding?= =?UTF-8?q?s?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Zero BLOCK across the three reviews. Applied: the judge partition is now a true 4-way (matched / mismatched / ledger_accounted / orphan) with precedence, and ReconstructionMiss routing is explicit; the minimal- convention gate's matched>=1 conjunct was proven unsatisfiable (all 7 classified opcodes carry >=1 operand, none melts under zero rows) and is restated as matched==0 exact; gate-5's facet.rs line now matches 3.1's zero-code-diff commitment; ledger row 10 is self-contained. Rows 15-18 record the review round. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01AGVLyRZNEKKBSfBDJfbY3V --- .../plans/r2il-roundtrip-oracle-spec-v1.md | 57 +++++++++++++------ 1 file changed, 41 insertions(+), 16 deletions(-) diff --git a/.claude/plans/r2il-roundtrip-oracle-spec-v1.md b/.claude/plans/r2il-roundtrip-oracle-spec-v1.md index f3ec4d20ef08a9..6edb6c10f223df 100644 --- a/.claude/plans/r2il-roundtrip-oracle-spec-v1.md +++ b/.claude/plans/r2il-roundtrip-oracle-spec-v1.md @@ -1,9 +1,15 @@ # SPEC — PR2 slice: the round-trip reconstruction oracle (`oracle.rs`) -> 5+3 council spec. **This file is DRAFT v2** (post-Phase-1 consolidation); -> v1 is the previous git revision of this file. Phase-3 reviewers see THIS -> document only. The change ledger (§7) records every savant finding and its -> disposition, including losing findings (anti-collapse). +> 5+3 council spec. **RATIFIED v3** (v1 and v2 are the prior git revisions +> of this file). Council run: 5 savants (prior-art / iron-rules / +> code-truth / cascade / views, all Sonnet) → consolidation → 3 reviewers +> (overclaim / dilution-collapse / firewall charters, Sonnet) → fix. +> Reviewer verdicts on v2: R3 all-PASS 0 findings; R2 five-PASS + +> FIX(P2)×2; R1 four-PASS + FIX(P1)×1 + FIX(P2)×2; ZERO BLOCK. All five +> FIX findings applied — §7 rows 15-18. This document is the executable +> spec; implementation follows it without further design. +> The change ledger (§7) records every finding and its disposition, +> including losing findings (anti-collapse). > > Scope: the PR2 gate deliverable from `.claude/plans/r2il-behavioral-ir-v1.md` > — "round-trip reconstruction oracle (R2IL → routes → semantic-equivalent @@ -142,11 +148,22 @@ Reconstruction`: ### 3.4 `judge` — the verdict, with a PINNED universe ✎ **Universe = source op sites** `(block_addr, op_idx)` enumerated from the -input `&[R2ILBlock]`. For each site exactly one of: (a) reconstructed AND -`OpSkeleton::of(source_op) == skeleton` → `matched`; (b) ≥1 ledger residual -whose `provenance.op_site` equals the site → `ledger_accounted`; (c) -neither → `orphans`. Skeleton inequality → `mismatches` (both skeletons -carried as typed values). +input `&[R2ILBlock]`. For each site, a TRUE 4-way partition, evaluated in +this precedence order [R2 F1 / R1 F2]: + +1. reconstructed (complete) AND `OpSkeleton::of(source_op) == skeleton` → + `matched`; +2. reconstructed (complete) AND unequal → `mismatches` (both skeletons + carried as typed values) — checked BEFORE the ledger criterion: a + mismatch is never excused by a coincident residual at the same site; +3. not reconstructed — including every site whose op appears only via a + `ReconstructionMiss` (`MissingOperands` / `FacetInversion` mean the site + is NOT reconstructed) — AND ≥1 ledger residual whose + `provenance.op_site` equals the site → `ledger_accounted`. This is the + expected home of incomplete ops: the very operands that failed to melt + produced op_site-anchored residuals; +4. else → `orphans`. An incomplete op with NO residual at its site orphans + — that is the correct failure signal, not a gap to paper over. ✎ **Ledger rows OUTSIDE the universe** — residuals with `op_site: None` (phi inputs, CallDefine, the Edge no-facet case; S3 Q6's anchor table) — @@ -222,10 +239,12 @@ plan item O6 tracks it (✎ S4 Q4). == source op count` (exact), `ledger_accounted == 0` (exact), `ssa_only_residuals ==` exact phi+CallDefine count. - `minimal_pass_one` fixture: still `holds()` (accounted, not - orphaned); anti-vacuity `matched >= 1 && ledger_accounted >= 1`; PLUS - the framing assertion that `matched` under minimal < `matched` under - permissive on the same blocks (proves the two conventions measure - different things — S5 Q3). + orphaned); `matched == 0` EXACT — satisfiable and pinned, because all + 7 classified opcodes carry ≥1 operand and no operand melts under zero + rows, so no op can fully reconstruct (the v2 draft's `matched >= 1` + conjunct was UNSATISFIABLE — R1 F1, P1); `ledger_accounted >= 1` + anti-vacuity; PLUS `matched(minimal) < matched(permissive)` on the + same blocks (the two conventions measure different things — S5 Q3). - mismatch can-fire: corrupt one operand row's facet → exactly one mismatch. ✎ swap can-fire (S5 Q2): swap two operand rows' facets ACROSS two ops → BOTH sites report mismatches (cross-row corruption @@ -250,8 +269,10 @@ plan item O6 tracks it (✎ S4 Q4). (entry for the new example/artifact pair), `.claude/plans/ r2il-behavioral-ir-v1.md` (new Open item **O6**: gap-census → widening decision; corpus-run-pending state; PR3 mint-scope note per S5 Q4), - this spec (ratification note). `facet.rs`: doc-comment cross-ref at - most. NO semantic diff in `furnace.rs`/`ore.rs`/`slag.rs`/`sink.rs`. + this spec (ratification note). `facet.rs`: **ZERO code diff** (same + commitment as §3.1's "no code change"); at most a doc-comment + cross-reference [R1 F5]. NO semantic diff in + `furnace.rs`/`ore.rs`/`slag.rs`/`sink.rs`. ## 6. PER-SAVANT QUESTION SETS — retired (Phase 1 complete) @@ -270,8 +291,12 @@ Question sets from v1 were answered; findings and dispositions in §7. | 7 | S3 CONFIRMS | payload semantics, shared `prov.inst`, Varnode manual `PartialEq`, minimal-pass-one no-operand-melt | inventory marked verified | | 8 | S3 RISK | provenance anchors: phi/Edge block-only; `UserOpNotInConvention` dead | §3.4 universe pinned; `ssa_only_residuals` channel; dead variant recorded in §4 | | 9 | S4 GAP ×4 | Cargo.toml stanza, README entry, plan O6, guide row missing from file list | gate 5 completed | -| 10 | S4 Q1 (partial) vs S4 Q3 | Q1 said the provisional facet row needs in-place edit; Q3 (deeper) says orthogonal | **Q3 wins** — no edit; losing finding recorded here per anti-collapse | +| 10 | S4 Q1 (partial) vs S4 Q3 | Q1 said the provisional facet row needs in-place edit; Q3 (deeper) says orthogonal | **Q3 wins** — `unproject` recovers a typed `Varnode`, not a durable address, so the row's persistence caveat is untouched by this slice. Q1's ONE salvageable facet — a discoverability pointer toward the oracle's use of `unproject` — is granted as the `facet.rs` doc-comment cross-reference (§3.1, §5 gate 5); no other facet of Q1 survives unaddressed [R2 F2] | | 11 | S5 RISK | deferring widening is safe only if census is tracked | O6 mandatory-same-commit (§5) | | 12 | S5 RISK | forward re-smelt oracle tests furnace against itself; skeleton misses cross-row swaps | direction confirmed; swap can-fire added to gate 3 | | 13 | S5 RISK | permissive pass ≠ shipped-coverage proof | §3.5 honest-framing normative + dual-convention reporting + minimal= 1` under `minimal_pass_one` was unsatisfiable (all 7 classified opcodes carry ≥1 operand; none melts under zero rows) | gate restated: `matched == 0` exact + `ledger_accounted >= 1` + the comparative inequality carries the signal | +| 16 | R1 F2 / R2 F1 FIX(P2) | §3.4's "(a)/(b)/(c)" partition omitted the mismatch bucket and the `ReconstructionMiss` routing | true 4-way partition with precedence; misses route to rule 3 or orphan | +| 17 | R1 F5 FIX(P2) | gate-5 facet.rs phrasing weaker than §3.1's "no code change" | aligned: ZERO code diff both places | +| 18 | R2 F2 FIX(P2) | ledger row 10 not self-contained | row 10 now names Q1's one salvageable facet and where it is granted | From 65f84f6fb6caf4babf871cb1d5148886b2f479ea Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 18 Aug 2026 13:10:02 +0000 Subject: [PATCH 4/4] r2il: the round-trip reconstruction oracle (PR2 gate deliverable) Implements the plan's section-14 deliverable per the 5+3 council-ratified spec: R2IL -> routes -> semantic-equivalent R2IL, compared on TYPED r2il values (OpSkeleton over Varnode), never a triple projection -- SPO is explicitly not the oracle, and success is semantic parity, never textual or binary equality. src/oracle.rs: - OpSkeleton: opcode + output + inputs, the projection the fact rows actually carry. Varnode's own manual PartialEq (space/offset/size) is the comparison; facet::unproject is CONSUMED, not rebuilt (it already ships with the exact property tests, including the custom-space and 64-bit-offset cases). - reconstruct: groups Op rows by prov.op_site, attaches operand rows by shared prov.inst ordered by their own payload index, and judges completeness against the op row's OWN payload; every miss is reported, never skipped. - judge: a true 4-way partition over source op sites with defined precedence -- matched / mismatched (checked BEFORE the ledger, so a mismatch is never excused by a coincident residual) / ledger_accounted / orphan. Residuals with no op site (phi inputs, CallDefine, the Edge no-facet case) are counted as ssa_only_residuals rather than dropped. - GapAttribute + gaps_of: the twelve R2ILOp variants carrying semantic state beyond the varnode projection are MEASURED, not silently passed. Carries ResidualReason's no-catch-all discipline (ALL, as_str, and a totality test over all twelve). - permissive_convention: the oracle's measurement config, pure data through existing constructors -- never a new smelt arm. Measured on the real corpus (.claude/harvest/r2il/ORACLE-RESULT.md): ZERO reconstruction mismatches across 35,946 matched op sites in four binaries. Two caveats the doc and the example both carry rather than bury: that result is under the permissive convention and proves the MECHANISM (the shipped minimal_pass_one measures matched = 0 -- it round-trips through accounting, not matching, and both columns are always printed); and the large orphan count is a linear-sweep chunking artifact, measured as only ~50% of a chunk's blocks reaching the CFG, not a reconstruction defect. The gap census opens plan item O6: memory_space dominates at 3586, subpiece_offset is 113, and three gap kinds are unmeasured on this corpus (no atomics) -- absence of evidence, recorded as such. No schema change, no FlatFact field, no furnace/ore/slag semantics touched; the artifact-mediated test proves the existing v2 TSV schemas are reconstruction-sufficient by requiring the from-disk verdict to EQUAL the in-memory one. Three disable-runs verified load-bearing: removing the skeleton comparison drives both mismatch tests red; removing the operand completeness check drives the minimal-convention test red; silencing the gap channel drives the Load/Fence test red. --- .claude/harvest/r2il/ORACLE-RESULT.md | 127 +++++ .claude/harvest/r2il/README.md | 20 + .claude/harvest/r2il/STAGED-CODEGEN-GUIDE.md | 1 + .claude/plans/r2il-behavioral-ir-v1.md | 21 +- crates/ruff_r2il/Cargo.toml | 4 + .../examples/r2il_roundtrip_oracle.rs | 371 +++++++++++++ crates/ruff_r2il/src/lib.rs | 2 + crates/ruff_r2il/src/oracle.rs | 503 ++++++++++++++++++ crates/ruff_r2il/tests/oracle_roundtrip.rs | 355 ++++++++++++ 9 files changed, 1403 insertions(+), 1 deletion(-) create mode 100644 .claude/harvest/r2il/ORACLE-RESULT.md create mode 100644 crates/ruff_r2il/examples/r2il_roundtrip_oracle.rs create mode 100644 crates/ruff_r2il/src/oracle.rs create mode 100644 crates/ruff_r2il/tests/oracle_roundtrip.rs diff --git a/.claude/harvest/r2il/ORACLE-RESULT.md b/.claude/harvest/r2il/ORACLE-RESULT.md new file mode 100644 index 00000000000000..ba6a533abf8732 --- /dev/null +++ b/.claude/harvest/r2il/ORACLE-RESULT.md @@ -0,0 +1,127 @@ +# R2IL round-trip reconstruction oracle — measured + +Resolves the PR-2 gate deliverable from `.claude/plans/r2il-behavioral-ir-v1.md` +§14 ("R2IL → routes → semantic-equivalent R2IL; SPO explicitly NOT the oracle") +and opens **O6a**'s census. Cite this, never re-derive it — same discipline as +`TRIAGE-RESULT.md` and `CORPUS-PROFILE-RESULT.md`. + +Command: `cargo run --release --example r2il_roundtrip_oracle --features lift` +(from `crates/ruff_r2il/`). Caps: `R2IL_ORACLE_MAX_SECTION_BYTES=262144`, +`R2IL_ORACLE_CHUNK_BLOCKS=24`, `R2IL_ORACLE_MAX_CHUNKS=200` (all defaults). +Module: `src/oracle.rs`; spec: `.claude/plans/r2il-roundtrip-oracle-spec-v1.md` +(council-ratified v3). + +Corpus: identical to the §12 profile — `r2sleigh/tests/e2e/{stress_test, +stress_test_opt}` plus `/bin/ls`, `/usr/bin/env` (all ELF64 x86-64). + +## Headline finding — ZERO mismatches on every binary + +| binary | chunks | matched | ledger_accounted | ssa_only | orphans | **mismatches** | +|---|---|---|---|---|---|---| +| stress_test | 143 | 8053 | 0 | 2253 | 6105 | **0** | +| stress_test_opt | 125 | 7761 | 0 | 3058 | 5167 | **0** | +| /bin/ls | 200 | 9743 | 0 | 3703 | 7224 | **0** | +| /usr/bin/env | 200 | 10389 | 0 | 2321 | 7230 | **0** | + +(permissive convention; `minimal_pass_one` produces the identical orphan and +`ssa_only` counts with `matched = 0` and the same totals moved wholesale into +`ledger_accounted` — see "Both conventions" below.) + +**Across 35,946 matched op sites in four binaries, the reconstruction never +produced a skeleton that differed from its source op.** Reconstruction is +`facet::unproject` + row grouping + `OpSkeleton` comparison; a mismatch would +mean the routes carried an op that decodes back to something else. None did. + +This is the mechanism claim and nothing more. It does NOT claim the routes +carry every op (they do not — see the gap census), nor that the shipped default +convention achieves this coverage (it does not — see below). + +## The orphan count is a CHUNKING artifact — measured, not assumed + +`orphans` is large (5167–7230) and that number is explained entirely by how the +corpus is fed in, not by the oracle: + +| binary | blocks reaching the CFG | source blocks in chunks | +|---|---|---| +| stress_test | 1835 | 3427 | +| stress_test_opt | 1579 | 2978 | +| /bin/ls | 2377 | 4800 | +| /usr/bin/env | 2607 | 4800 | + +A chunk is a window of 24 consecutive linear-sweep blocks, so many of its +blocks branch to targets OUTSIDE the window and are unreachable from the +chunk's entry. `CFG::from_blocks` drops them; their ops therefore never reach +`ore::enumerate`, produce neither a fact row nor a residual, and land in +`orphans` by construction. Roughly 46–50 % of blocks are dropped this way, +and the op-level arithmetic matches exactly: for `stress_test`, +`8053 matched + 6105 orphans = 14158`, which is precisely that binary's +`ops_total` in `CORPUS-PROFILE-RESULT.md`. + +**Two things this is and is not.** It is NOT evidence of a reconstruction +defect — the in-repo fixtures (`tests/oracle_roundtrip.rs`), which use coherent +CFGs, report zero orphans. It IS evidence that the oracle refuses to hide a +gap: an implementation that quietly skipped unreachable blocks would have +reported `holds()` on every chunk and looked perfect. Getting a loud, countable +orphan population from a deliberately lossy input is the behaviour the +conservation reading (plan C3) exists to produce. + +A symtab-driven function decomposition (the §12 profiler's Pass 2 shape) would +shrink this dramatically; that is O6a's natural next refinement, not a defect +to fix here. + +## Both conventions, never conflated (spec §3.5) + +`minimal_pass_one` — the SHIPPED default — has zero convention rows, so +`R2ilConvention::resolve` returns `None` for every facet and no operand row +melts. Measured consequence on all four binaries: `matched = 0`, with every one +of those op sites moving into `ledger_accounted` (8053 / 7761 / 9743 / 10389 +respectively) and `holds` unchanged. + +So the honest reading is: +- **permissive** proves the reconstruction MECHANISM is faithful; +- **minimal_pass_one** shows the shipped default currently round-trips nothing + through matching — it round-trips through ACCOUNTING, which is a real but + different property. + +Anyone quoting the mismatch-free result must quote which convention produced +it. The example prints both columns for exactly this reason. + +## O6 — the attribute-gap census (the schema-widening input) + +Twelve `R2ILOp` variants carry semantic state beyond the `inputs()`/`output()` +varnode projection the fact rows represent. Matched ops of those variants emit a +typed `AttributeGap` rather than passing silently. Measured: + +| binary | memory_space | subpiece_offset | memory_ordering | userop_index | ptr_element_size | +|---|---|---|---|---|---| +| stress_test | 1273 | 20 | 0 | 0 | 0 | +| stress_test_opt | 536 | 56 | 0 | 0 | 0 | +| /bin/ls | 741 | 25 | 0 | 0 | 0 | +| /usr/bin/env | 1036 | 12 | 0 | 0 | 0 | + +**`MemorySpace` is the dominant gap by an order of magnitude** (3586 total +against 113 `SubpieceOffset`). Every `Load`/`Store` that round-trips today +round-trips WITHOUT which address space it touched — the fact rows carry the +address varnode but not the `space: SpaceId` field. That is the single +highest-value candidate for an additive widening, and it is now measured rather +than assumed. + +**Three gap kinds recorded ZERO on this corpus** — `MemoryOrdering`, +`UserOpIndex`, `PtrElementSize`. That is absence of evidence, not evidence of +absence: this corpus exercises no atomics/fences (consistent with +`CORPUS-PROFILE-RESULT.md`'s own `call_other_arity: (no samples)` finding), so +those three remain unmeasured here. A corpus with atomics is what would move +them, and the `gaps_of` totality test (`tests/oracle_roundtrip.rs`) pins that +all twelve variants CAN fire regardless of whether this corpus makes them. + +## What this resolves and what it does not + +- **Resolved:** the §14 round-trip oracle exists, runs on the real corpus, and + reports zero reconstruction mismatches over 35,946 matched op sites. +- **Resolved (O6, first census):** `MemorySpace` dominates the attribute gap; + `SubpieceOffset` is real but small; three kinds are unmeasured on this corpus. +- **NOT resolved:** whether to widen the schema for `MemorySpace` (that is the + O6 decision this census feeds, and it must stay additive — the `FlatFact` + 88-byte pin holds); the symtab-driven decomposition that would collapse the + chunking orphans (O6a refinement); and the shipped `minimal_pass_one` + convention's own coverage, which this run measures as accounting-only. diff --git a/.claude/harvest/r2il/README.md b/.claude/harvest/r2il/README.md index dd202decbd6ba5..a9202ab14427eb 100644 --- a/.claude/harvest/r2il/README.md +++ b/.claude/harvest/r2il/README.md @@ -45,10 +45,30 @@ Both are gitignored, so a regenerate run leaves the tree clean. | `r2il-pass1-slag.tsv` | the addressed residual ledger; the artifact a reviewer actually reads | | `r2il-pass1-census.md` | per-fact-kind and per-opcode counts | | `PROVENANCE.md` | corpus manifest (FNV-1a 64 per input), r2sleigh commit pin, caps, exact invocation | +| `CORPUS-PROFILE-RESULT.md` | the §12 corpus profile (resolves O1: 100.00 % of 130193 ops fit `dst+src0+src1` inline) | +| `ORACLE-RESULT.md` | the §14 round-trip verdict + the O6 attribute-gap census (see below) | Together under 32 KB. The Release assets are reproducible from these plus the pinned corpus; these are not reproducible from the Release. +## The second example / artifact pair — the round-trip oracle + +`examples/r2il_roundtrip_oracle.rs` (feature `lift`) is a SEPARATE deliverable +from `harvest_r2il.rs` above: it writes no files and prints its verdict to +stdout, and the numbers are transcribed into `ORACLE-RESULT.md` by hand, the +same way `CORPUS-PROFILE-RESULT.md` records the profiler. + +```sh +cargo run --manifest-path crates/ruff_r2il/Cargo.toml --features lift --release \ + --example r2il_roundtrip_oracle +``` + +Reads the same corpus as the profiler (`$R2IL_CORPUS`, CLI args, or the same +four-binary fallback). Caps: `R2IL_ORACLE_MAX_SECTION_BYTES`, +`R2IL_ORACLE_CHUNK_BLOCKS`, `R2IL_ORACLE_MAX_CHUNKS`. It prints BOTH +conventions (permissive = mechanism proof, `minimal_pass_one` = shipped-default +coverage) and never conflates them — cite whichever one a number came from. + ## Regenerate ```sh diff --git a/.claude/harvest/r2il/STAGED-CODEGEN-GUIDE.md b/.claude/harvest/r2il/STAGED-CODEGEN-GUIDE.md index 34d5ff9e947d92..50267033f7c500 100644 --- a/.claude/harvest/r2il/STAGED-CODEGEN-GUIDE.md +++ b/.claude/harvest/r2il/STAGED-CODEGEN-GUIDE.md @@ -29,6 +29,7 @@ migration story you will then have to run. | `r2il-pass1.ore.tsv.gz` | **shape stable, columns additive** | the melted rows. Read by the `#schema` header, never by column position. | | `r2il-convention.toml.gz` | **stable** | the drill tree. Every row is `unmeasured` until something measures it. | | `FlatFact`'s two payload slots (`a`, `b`) | **shape confirmed, meaning still per-kind** | `.claude/harvest/r2il/CORPUS-PROFILE-RESULT.md` (O1, resolved 2026-08-18): 100.00% of 130193 sampled ops across 4 corpus binaries fit `dst+src0+src1` inline, 0.00% needed `Vec` routing — the existing 2-slot `a`/`b` shape needs no re-carving for PR 2's §11 layout choice. What is STILL not pinned is the PER-KIND MEANING of `a`/`b` (documented in `furnace.rs`'s payload table) and the byte-level persistence encoding, both real PR 2 scope. Do not hardcode the bit layout; go through the accessor or re-read the module table. Caveat carried forward: `CallOther` arity was unmeasured (no samples in this corpus) and phi/`Multiequal` fan-in reaches 7 at the CFG level though it never appears as a sampled `Op` row here — neither contradicts the inline finding but neither is covered by it either. | +| `ORACLE-RESULT.md` + `examples/r2il_roundtrip_oracle.rs` | **stable finding, corpus-dependent numbers** | the §14 round-trip verdict: `R2IL → routes → semantic-equivalent R2IL` on typed values (SPO is NOT the oracle). **Zero reconstruction mismatches over 35,946 matched op sites across 4 binaries.** Two caveats you MUST carry when citing it: (a) that result is under the oracle's `permissive_convention` and proves the reconstruction MECHANISM — the SHIPPED `minimal_pass_one` measures `matched = 0` (accounting, not matching), and the example prints both columns so they are never conflated; (b) the large `orphans` count is a linear-sweep CHUNKING artifact (only ~50 % of a chunk's blocks are reachable from its entry, so the rest produce no ore facts at all), not a reconstruction defect. The `attribute_gap_census` is the O6 input: `memory_space` dominates (3586), `subpiece_offset` is small (113), and `memory_ordering`/`userop_index`/`ptr_element_size` are UNMEASURED on this corpus (no atomics) — absence of evidence, not evidence of absence. | | `OpTag::as_str()` opcode tags | **stable, with one correction** | one tag shipped briefly as `int_scary` — a spellchecker rewrite of `int_scarry` (P-code `INT_SCARRY`, signed carry) that reached the enum's `as_str`. Corrected; the pass-1 artifacts never carried it (no SCARRY op classified in the corpus). If you pinned the misspelling, repin. | | the 16-byte `VarnodeFacet` **as an address** | ⚠ **provisional** | `PROVISIONAL_R2IL_VARNODE = 0x0000` is a local placeholder. The real classid is minted in `ogar_codebook` (PR 3). Treat the facet as an opaque key today; do not persist it as a durable address. | diff --git a/.claude/plans/r2il-behavioral-ir-v1.md b/.claude/plans/r2il-behavioral-ir-v1.md index 5c0c562f7e9024..27c22c679164c5 100644 --- a/.claude/plans/r2il-behavioral-ir-v1.md +++ b/.claude/plans/r2il-behavioral-ir-v1.md @@ -404,4 +404,23 @@ direct consumption already succeeds without it. - O3: `SpaceId::Custom(u32)` fit in the 16-byte varnode projection (fixture). - O4: function discovery for whole-ELF lifting (linear sweep vs CLI vs r2) — profiler may start at instruction/op-level stats + e2e binaries. -- O5: classid mint request shape for lance-graph (PR 3 gate). +- O5: classid mint request shape for lance-graph (PR 3 gate). **Input added + 2026-08-18:** the oracle's attribute-gap census (O6) is a scope input here — + if `MemorySpace`/`MemoryOrdering` fire broadly on the corpus, the mint may + need more than the single `NETWORK_LAYER`-analog container concept this + plan currently expects (a second facet dimension for ordering/space + semantics). Anticipate it rather than discover it mid-flight. +- O6: **attribute-gap census → schema-widening decision** (opened 2026-08-18 by + the round-trip oracle, `.claude/plans/r2il-roundtrip-oracle-spec-v1.md` + ratified v3; module `crates/ruff_r2il/src/oracle.rs`). Twelve `R2ILOp` + variants carry semantic state beyond the `inputs()`/`output()` varnode + projection the fact rows represent — `Load`/`Store` (space), `Fence` (+ + zero varnodes at all), `LoadLinked`/`StoreConditional`/`AtomicCAS`/ + `LoadGuarded`/`StoreGuarded` (space + ordering), `CallOther` (userop), + `Subpiece` (offset), `PtrAdd`/`PtrSub` (element_size). The oracle MEASURES + them as typed `AttributeGap` rows rather than silently passing them; the + census is the probe-first input for a future ADDITIVE widening (never a + `FlatFact` field — the 88-byte pin holds). **Sub-item O6a:** run + `examples/r2il_roundtrip_oracle.rs` over the §12 corpus and record the + census in `.claude/harvest/r2il/ORACLE-RESULT.md` — until then that doc + carries only the in-repo fixture numbers and says so. diff --git a/crates/ruff_r2il/Cargo.toml b/crates/ruff_r2il/Cargo.toml index 61743f6da23a03..03bbb349da8c0f 100644 --- a/crates/ruff_r2il/Cargo.toml +++ b/crates/ruff_r2il/Cargo.toml @@ -37,6 +37,10 @@ required-features = ["lift"] name = "r2il_corpus_profile" required-features = ["lift"] +[[example]] +name = "r2il_roundtrip_oracle" +required-features = ["lift"] + [lints.rust] unsafe_code = "forbid" unreachable_pub = "warn" diff --git a/crates/ruff_r2il/examples/r2il_roundtrip_oracle.rs b/crates/ruff_r2il/examples/r2il_roundtrip_oracle.rs new file mode 100644 index 00000000000000..3e22d67f1d8f4d --- /dev/null +++ b/crates/ruff_r2il/examples/r2il_roundtrip_oracle.rs @@ -0,0 +1,371 @@ +//! The round-trip reconstruction oracle over a real corpus — plain text to stdout, no file +//! writes (`.claude/plans/r2il-roundtrip-oracle-spec-v1.md` §3.7, ratified v3). +//! +//! For each binary: a linear byte sweep of every executable section lifts native instructions +//! into `R2ILBlock`s (the same `Disassembler::lift`-per-instruction pass `r2il_corpus_profile` +//! calls "MEASURED EXACT (op level)"), the sweep's blocks are chunked into +//! `R2IL_ORACLE_CHUNK_BLOCKS`-sized groups, and each chunk is run through +//! `FunctionBehavior::from_blocks_raw` → `furnace::smelt` → `oracle::reconstruct` → +//! `oracle::judge` under BOTH conventions. +//! +//! **Both conventions are reported, never conflated** (spec §3.5, normative): a verdict holding +//! under `permissive_convention` proves the reconstruction MECHANISM; the `minimal_pass_one` +//! column shows what the SHIPPED default actually covers, which on a zero-row convention is +//! accounting rather than matching. +//! +//! **Labelling rule, inherited from the profiler:** the chunking is a linear-sweep +//! APPROXIMATION of function boundaries, not a symtab-exact one — a chunk is a window of +//! consecutive lifted blocks, so its CFG is whatever those blocks' own branch targets imply. +//! That is sound for the oracle (it measures round-trip fidelity of whatever CFG it is given) +//! and is NOT a claim about function decomposition. Every printed row says `chunked`. +//! +//! Nothing here is copied into ruff: the corpus lives outside the repository, and this example +//! only ever reads it. No `unwrap`/`panic` on corpus input. + +// See `r2il_corpus_profile.rs`'s identical note: ruff's `clippy.toml` disallowed-methods list is +// directory-scoped and reaches this workspace-EXCLUDED crate even though its reasons say "in ty +// crates"; `ruff_r2il` has no `ty::System` to route through, and these are the documented +// `R2IL_ORACLE_*` / `R2IL_CORPUS` overrides. +#![expect( + clippy::disallowed_methods, + reason = "not a ty crate: `System` is unavailable to this workspace-excluded crate; these are the example's documented env overrides" +)] + +use std::collections::BTreeMap; +use std::env; +use std::fs; +use std::path::{Path, PathBuf}; + +use r2il::R2ILBlock; +use r2sleigh_lift::{Disassembler, userop_map_for_arch}; + +use ruff_r2il::behavior::FunctionBehavior; +use ruff_r2il::convention::R2ilConvention; +use ruff_r2il::furnace; +use ruff_r2il::oracle::{self, OracleVerdict}; + +/// Minimum bytes libsla needs per lift call — mirrors the profiler's own constant. +const MIN_LIFT_BYTES: usize = 16; +const DEFAULT_MAX_SECTION_BYTES: usize = 262_144; +const DEFAULT_CHUNK_BLOCKS: usize = 24; +const DEFAULT_MAX_CHUNKS: usize = 200; + +const ELF_EXEC_FLAG: u64 = 0x4; +const ELF_SHT_NOBITS: u32 = 8; + +/// Minimal ELF64 LE executable-section reader. Every read is bounds-checked; anything malformed +/// yields an empty list and the caller skips the binary with a printed note. Deliberately much +/// smaller than `r2il_corpus_profile`'s `mod elf` — the oracle needs no symtab. +fn exec_sections(bytes: &[u8]) -> Vec<(String, u64, u64, u64)> { + let read_u16 = |off: usize| -> Option { + bytes + .get(off..off + 2) + .map(|b| u16::from_le_bytes([b[0], b[1]])) + }; + let read_u32 = |off: usize| -> Option { + bytes + .get(off..off + 4) + .map(|b| u32::from_le_bytes([b[0], b[1], b[2], b[3]])) + }; + let read_u64 = |off: usize| -> Option { + bytes + .get(off..off + 8) + .map(|b| u64::from_le_bytes([b[0], b[1], b[2], b[3], b[4], b[5], b[6], b[7]])) + }; + + if bytes.get(0..4) != Some(&[0x7f, b'E', b'L', b'F']) || bytes.get(4) != Some(&2) { + return Vec::new(); + } + let (Some(shoff), Some(shentsize), Some(shnum), Some(shstrndx)) = ( + read_u64(0x28), + read_u16(0x3a), + read_u16(0x3c), + read_u16(0x3e), + ) else { + return Vec::new(); + }; + let (shoff, shentsize, shnum, shstrndx) = ( + shoff as usize, + shentsize as usize, + shnum as usize, + shstrndx as usize, + ); + if shentsize < 64 || shnum == 0 || shstrndx >= shnum { + return Vec::new(); + } + + let strtab_hdr = shoff + shstrndx * shentsize; + let Some(strtab_off) = read_u64(strtab_hdr + 0x18).map(|v| v as usize) else { + return Vec::new(); + }; + + let mut out = Vec::new(); + for index in 0..shnum { + let hdr = shoff + index * shentsize; + let (Some(name_off), Some(sh_type), Some(flags), Some(addr), Some(offset), Some(size)) = ( + read_u32(hdr), + read_u32(hdr + 0x04), + read_u64(hdr + 0x08), + read_u64(hdr + 0x10), + read_u64(hdr + 0x18), + read_u64(hdr + 0x20), + ) else { + continue; + }; + if flags & ELF_EXEC_FLAG == 0 || sh_type == ELF_SHT_NOBITS || size == 0 { + continue; + } + let name_start = strtab_off.saturating_add(name_off as usize); + let name = bytes + .get(name_start..) + .and_then(|tail| tail.iter().position(|&c| c == 0).map(|end| &tail[..end])) + .map(|raw| String::from_utf8_lossy(raw).into_owned()) + .unwrap_or_else(|| format!("sh{index}")); + out.push((name, addr, offset, size)); + } + out +} + +fn env_usize(name: &str, default: usize) -> usize { + env::var(name) + .ok() + .and_then(|v| v.parse::().ok()) + .unwrap_or(default) +} + +/// `$R2IL_CORPUS` (colon-separated) or CLI args, else the same fallback list the §12 profiler +/// uses, so the two examples measure the same corpus. +fn corpus_paths() -> Vec { + let args: Vec = env::args().skip(1).collect(); + if !args.is_empty() { + return args.into_iter().map(PathBuf::from).collect(); + } + if let Ok(value) = env::var("R2IL_CORPUS") { + let paths: Vec = value + .split(':') + .filter(|s| !s.is_empty()) + .map(PathBuf::from) + .collect(); + if !paths.is_empty() { + return paths; + } + } + vec![ + PathBuf::from(concat!( + env!("CARGO_MANIFEST_DIR"), + "/../../../r2sleigh/tests/e2e/stress_test" + )), + PathBuf::from(concat!( + env!("CARGO_MANIFEST_DIR"), + "/../../../r2sleigh/tests/e2e/stress_test_opt" + )), + PathBuf::from("/bin/ls"), + PathBuf::from("/usr/bin/env"), + ] +} + +fn lift_window(bytes: &[u8], offset: usize) -> Vec { + let avail = &bytes[offset..]; + if avail.len() >= MIN_LIFT_BYTES { + avail[..MIN_LIFT_BYTES].to_vec() + } else { + let mut window = avail.to_vec(); + window.resize(MIN_LIFT_BYTES, 0); + window + } +} + +/// Accumulated verdict counters across every chunk, per convention. +#[derive(Default)] +struct Totals { + chunks: usize, + holds: usize, + matched: usize, + ledger_accounted: usize, + ssa_only_residuals: usize, + orphans: usize, + mismatches: usize, + gaps: BTreeMap<&'static str, usize>, +} + +impl Totals { + fn absorb(&mut self, verdict: &OracleVerdict) { + self.chunks += 1; + if verdict.holds() { + self.holds += 1; + } + self.matched += verdict.matched; + self.ledger_accounted += verdict.ledger_accounted; + self.ssa_only_residuals += verdict.ssa_only_residuals; + self.orphans += verdict.orphans.len(); + self.mismatches += verdict.mismatches.len(); + for gap in &verdict.attribute_gaps { + *self.gaps.entry(gap.attribute.as_str()).or_insert(0) += 1; + } + } + + fn print(&self, label: &str) { + println!( + " {label}: chunks={} holds={}/{} matched={} ledger_accounted={} \ + ssa_only_residuals={} orphans={} mismatches={}", + self.chunks, + self.holds, + self.chunks, + self.matched, + self.ledger_accounted, + self.ssa_only_residuals, + self.orphans, + self.mismatches, + ); + print!(" attribute_gap_census:"); + if self.gaps.is_empty() { + println!(" (none)"); + } else { + println!(); + for (name, count) in &self.gaps { + println!(" {name}={count}"); + } + } + } +} + +fn run_chunk(blocks: &[R2ILBlock], conv: &R2ilConvention, totals: &mut Totals) { + let Some(behavior) = FunctionBehavior::from_blocks_raw(blocks, None) else { + return; + }; + let (rows, ledger, report) = furnace::smelt(&behavior, blocks, conv); + if !report.is_conserved() { + // Conservation is the furnace's own invariant (plan C3); a violation makes every + // downstream number meaningless, so it is reported rather than absorbed. + println!(" WARNING: conservation failed on a chunk — verdict omitted"); + return; + } + let recon = oracle::reconstruct(&rows, conv.spaces()); + totals.absorb(&oracle::judge(blocks, &recon, &ledger)); +} + +fn process_binary( + disasm: &Disassembler, + path: &Path, + max_section_bytes: usize, + chunk: usize, + max_chunks: usize, +) { + println!("== binary: {} ==", path.display()); + + let Ok(bytes) = fs::read(path) else { + println!(" skipped: cannot read file"); + println!(); + return; + }; + let sections = exec_sections(&bytes); + if sections.is_empty() { + println!(" skipped: no executable sections in a recognized ELF64 LE image"); + println!(); + return; + } + + let mut lifted: Vec = Vec::new(); + let mut undecodable = 0usize; + for (_, addr, offset, size) in §ions { + let (Ok(start), Ok(len)) = (usize::try_from(*offset), usize::try_from(*size)) else { + continue; + }; + let Some(section_bytes) = bytes.get(start..start.saturating_add(len)) else { + continue; + }; + let limit = section_bytes.len().min(max_section_bytes); + let mut cursor = 0usize; + while cursor < limit { + let at = addr.saturating_add(cursor as u64); + match disasm.lift(&lift_window(section_bytes, cursor), at) { + Ok(block) => { + cursor += (block.size as usize).max(1); + lifted.push(block); + } + Err(_) => { + undecodable += 1; + cursor += 1; + } + } + } + } + + let chunks: Vec<&[R2ILBlock]> = lifted.chunks(chunk.max(1)).take(max_chunks).collect(); + // Always measured and printed, because it is what EXPLAINS the orphan count below. A + // linear-sweep window's blocks branch to targets outside the window, so `CFG::from_blocks` + // drops every block unreachable from the chunk's entry; those blocks' ops never reach + // `ore::enumerate` at all and therefore have neither a fact row nor a residual — they land + // in `orphans` by construction. Reporting the ratio here keeps that visible instead of + // letting a reader mistake a chunking artifact for a reconstruction defect. + let mut chunk_source_blocks = 0usize; + let mut chunk_cfg_blocks = 0usize; + for window in &chunks { + chunk_source_blocks += window.len(); + if let Some(behavior) = FunctionBehavior::from_blocks_raw(window, None) { + chunk_cfg_blocks += behavior.control().num_blocks(); + } + } + println!( + " lifted_blocks={} undecodable={} chunked_windows={} (chunk={} blocks, linear sweep — \ + an APPROXIMATION of function boundaries, never a symtab-exact claim)", + lifted.len(), + undecodable, + chunks.len(), + chunk, + ); + println!( + " chunk_blocks_reaching_the_cfg={chunk_cfg_blocks}/{chunk_source_blocks} — the rest are \ + unreachable from their chunk's entry, produce NO ore facts, and are therefore counted \ + as orphans below (a chunking artifact, not a reconstruction defect)" + ); + + let mut permissive_totals = Totals::default(); + let mut minimal_totals = Totals::default(); + let minimal = R2ilConvention::minimal_pass_one(); + + for window in chunks { + if let Ok(conv) = oracle::permissive_convention(window) { + run_chunk(window, &conv, &mut permissive_totals); + } + run_chunk(window, &minimal, &mut minimal_totals); + } + + permissive_totals.print("permissive (MECHANISM proof)"); + minimal_totals.print("minimal_pass_one (SHIPPED default coverage)"); + println!(); +} + +fn main() { + let max_section_bytes = env_usize("R2IL_ORACLE_MAX_SECTION_BYTES", DEFAULT_MAX_SECTION_BYTES); + let chunk = env_usize("R2IL_ORACLE_CHUNK_BLOCKS", DEFAULT_CHUNK_BLOCKS); + let max_chunks = env_usize("R2IL_ORACLE_MAX_CHUNKS", DEFAULT_MAX_CHUNKS); + + println!("r2il round-trip reconstruction oracle"); + println!( + "caps: R2IL_ORACLE_MAX_SECTION_BYTES={max_section_bytes} \ + R2IL_ORACLE_CHUNK_BLOCKS={chunk} R2IL_ORACLE_MAX_CHUNKS={max_chunks}" + ); + println!( + "BOTH conventions are reported and never conflated: permissive proves the reconstruction \ + MECHANISM; minimal_pass_one shows the SHIPPED default's coverage." + ); + println!(); + + let mut disasm = match Disassembler::from_sla( + sleigh_config::processor_x86::SLA_X86_64, + sleigh_config::processor_x86::PSPEC_X86_64, + "x86-64", + ) { + Ok(disasm) => disasm, + Err(err) => { + println!("FATAL: Disassembler::from_sla(x86-64) failed: {err}"); + return; + } + }; + disasm.set_userop_map(userop_map_for_arch("x86-64")); + + for path in corpus_paths() { + process_binary(&disasm, &path, max_section_bytes, chunk, max_chunks); + } +} diff --git a/crates/ruff_r2il/src/lib.rs b/crates/ruff_r2il/src/lib.rs index ac39d0b5ac80c7..f30427f219f496 100644 --- a/crates/ruff_r2il/src/lib.rs +++ b/crates/ruff_r2il/src/lib.rs @@ -27,6 +27,7 @@ //! | — · drill key + config tree | [`facet`], [`convention`] | the 16-byte address, and longest-prefix-wins config over it | //! | 4 · DTO / codebook factoring | [`vocab`] | feeds lance-graph `ogar_codebook` **read-only** | //! | 5 · sink | [`sink`] | where refined truth lands — trait + offline backend; lance-graph SoA is implemented downstream, not here | +//! | 6 · **oracle** | [`oracle`] | round-trip reconstruction: routes → [`oracle::OpSkeleton`] equality per source op site; SPO is NOT the oracle | //! | — · artifact set | `examples/harvest_r2il.rs` | the deliverable, per MedCare-rs / openproject-nexgen-rs | //! //! Refined concern *contracts* are a later, measured furnace output. This crate does not invent @@ -66,6 +67,7 @@ pub mod behavior; pub mod convention; pub mod facet; pub mod furnace; +pub mod oracle; pub mod ore; pub mod sink; pub mod slag; diff --git a/crates/ruff_r2il/src/oracle.rs b/crates/ruff_r2il/src/oracle.rs new file mode 100644 index 00000000000000..1320f9ac81021e --- /dev/null +++ b/crates/ruff_r2il/src/oracle.rs @@ -0,0 +1,503 @@ +//! Stage 6 — the round-trip reconstruction ORACLE: `R2IL → routes → semantic-equivalent R2IL`. +//! +//! The PR-2 gate deliverable from `.claude/plans/r2il-behavioral-ir-v1.md` §14, executed per the +//! council-ratified spec `.claude/plans/r2il-roundtrip-oracle-spec-v1.md` (v3). Three committed +//! properties: +//! +//! - **SPO is NOT the oracle.** The comparison happens on typed r2il values — [`OpSkeleton`] +//! equality over [`r2il::Varnode`]s — never on a triple projection and never on +//! textual/binary artifact equality (plan C4). +//! - **Conservation is the verdict's shape** (plan C3): every SOURCE OP SITE is either +//! reconstructed-equal, mismatched, ledger-accounted, or an ORPHAN — a true 4-way partition +//! with defined precedence, and orphans/mismatches are failures, never footnotes. +//! - **What the skeleton cannot carry is MEASURED, never silently passed.** Twelve `R2ILOp` +//! variants hold semantic state beyond their `inputs()`/`output()` varnode projection (the +//! spec §2 table); each matched op of those variants emits a typed [`AttributeGap`]. The gap +//! census is the probe-first input for a FUTURE additive schema widening (plan open item O6) +//! — this module changes no schema and no furnace semantics. +//! +//! # What a passing verdict does and does not prove +//! +//! A verdict that [`OracleVerdict::holds`] under [`permissive_convention`] proves the +//! reconstruction MECHANISM — facet inversion ([`facet::unproject`]) + row grouping + skeleton +//! comparison — is faithful. It says NOTHING about the shipped +//! [`R2ilConvention::minimal_pass_one`] default's coverage: under that convention no operand +//! row melts at all (zero rows ⇒ `resolve` is `None` everywhere), so its verdict holds through +//! ledger ACCOUNTING, with `matched == 0`. The two conventions measure different things; report +//! both, never conflate them (spec §3.5, normative). +//! +//! Rendering rule (spec frozen 8): every printed or persisted representation of a verdict is +//! produced from typed fields and `as_str()` — `format!("{:?}")` is FORBIDDEN as a data path. +//! `Debug` derives below exist solely for test-assertion diagnostics. + +use std::collections::{BTreeMap, BTreeSet}; + +use r2il::{AddressSpace, ArchSpec, R2ILBlock, R2ILOp, SpaceId, Varnode}; + +use crate::convention::R2ilConvention; +use crate::facet::{self, CustomSpaceTable, FacetOverflow}; +use crate::furnace::FactKind; +use crate::furnace::FlatFact; +use crate::ore::OpTag; +use crate::slag::ResidualLedger; + +// ================================================================================================ +// OpSkeleton — THE equivalence target +// ================================================================================================ + +/// The typed projection an op's fact rows carry: opcode + output varnode + input varnodes in +/// position order. Exactly what [`R2ILOp::output`]/[`R2ILOp::inputs`] project — which is exactly +/// what `ore::enumerate` fed the furnace, so skeleton equality at a site is the honest +/// definition of "the routes carried this op" (spec §3.2). +/// +/// `Varnode`'s own manual `PartialEq` (space/offset/size, `meta` excluded — `varnode.rs:149`) +/// is the comparison; [`facet::unproject`] never reconstructs `meta`, and `meta` never entered +/// the projection, so the exclusion is load-bearing, not incidental. +#[derive(Debug, Clone, PartialEq)] +pub struct OpSkeleton { + pub opcode: OpTag, + pub output: Option, + pub inputs: Vec, +} + +impl OpSkeleton { + /// Project one source op. This is the SOURCE side of the comparison; the reconstructed side + /// is assembled from fact rows by [`reconstruct`]. + #[must_use] + pub fn of(op: &R2ILOp) -> Self { + Self { + opcode: OpTag::from_r2il(op), + output: op.output().cloned(), + inputs: op.inputs().into_iter().cloned().collect(), + } + } +} + +// ================================================================================================ +// GapAttribute — the measured, typed "what the skeleton cannot carry" channel +// ================================================================================================ + +/// One kind of non-varnode semantic state a matched op's variant carries that neither the +/// skeleton nor any current fact row represents. Deliberately NOT a +/// [`crate::slag::ResidualReason`]: the furnace did not fail — the schema deliberately projects +/// (spec §3.4). Mirrors `ResidualReason`'s no-catch-all discipline: [`Self::ALL`] + +/// [`Self::as_str`] + the totality of [`gaps_of`] are all pinned by tests. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum GapAttribute { + /// `Load`/`Store` (and the atomic/guarded family): the `space: SpaceId` field. + MemorySpace, + /// `Fence` and the atomic/guarded family: the `ordering: MemoryOrdering` field. Note + /// `Fence` carries ZERO varnodes — its skeleton is `(Fence, None, [])`, trivially equal, so + /// this gap carries ALL of its semantics. + MemoryOrdering, + /// `CallOther`: the `userop: u32` index. + UserOpIndex, + /// `Subpiece`: the `offset: u32` field (r2il models it as a field, not a const operand). + SubpieceOffset, + /// `PtrAdd`/`PtrSub`: the `element_size: u32` field. + PtrElementSize, +} + +impl GapAttribute { + /// Every variant's stable name — the no-catch-all pin, exactly like + /// [`crate::slag::ResidualReason::ALL`]. + pub const ALL: &'static [&'static str] = &[ + "memory_space", + "memory_ordering", + "userop_index", + "subpiece_offset", + "ptr_element_size", + ]; + + /// Stable `snake_case` name. Never derived from `Debug`. + #[must_use] + pub fn as_str(self) -> &'static str { + match self { + GapAttribute::MemorySpace => "memory_space", + GapAttribute::MemoryOrdering => "memory_ordering", + GapAttribute::UserOpIndex => "userop_index", + GapAttribute::SubpieceOffset => "subpiece_offset", + GapAttribute::PtrElementSize => "ptr_element_size", + } + } +} + +/// The verified spec-§2 table: which non-varnode attributes each opcode's variant carries. +/// TWELVE variants return non-empty; everything else returns `&[]`. The +/// `gaps_of_covers_exactly_the_twelve_table_variants` test pins both halves (can-fire AND +/// can-stay-silent), so coverage drift is caught the way `there_is_no_catch_all_reason` catches +/// a new `ResidualReason`. +#[must_use] +pub fn gaps_of(tag: OpTag) -> &'static [GapAttribute] { + match tag { + OpTag::Load | OpTag::Store => &[GapAttribute::MemorySpace], + OpTag::Fence => &[GapAttribute::MemoryOrdering], + OpTag::LoadLinked + | OpTag::StoreConditional + | OpTag::AtomicCAS + | OpTag::LoadGuarded + | OpTag::StoreGuarded => &[GapAttribute::MemorySpace, GapAttribute::MemoryOrdering], + OpTag::CallOther => &[GapAttribute::UserOpIndex], + OpTag::Subpiece => &[GapAttribute::SubpieceOffset], + OpTag::PtrAdd | OpTag::PtrSub => &[GapAttribute::PtrElementSize], + _ => &[], + } +} + +// ================================================================================================ +// Reconstruction +// ================================================================================================ + +/// One op rebuilt from its fact rows: the [`FactKind::Op`] row's site and ordinal, plus the +/// skeleton assembled from its [`FactKind::OperandIn`]/[`FactKind::OperandOut`] rows. +#[derive(Debug, Clone, PartialEq)] +pub struct ReconstructedOp { + pub site: (u64, usize), + pub ordinal: u64, + pub skeleton: OpSkeleton, +} + +/// Why one op row could NOT be rebuilt. A missed site is "not reconstructed" for +/// [`judge`]'s partition — it falls to the ledger criterion or orphans (spec §3.4 rules 3-4). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum ReconstructionMiss { + /// The operand rows present do not satisfy the op row's OWN payload + /// (`b` = `input_arity | has_output << 32`). `have`/`need` count inputs AND the output + /// slot together: `have = ins.len() + out_present`, `need = arity + has_output`. + MissingOperands { + site: (u64, usize), + have: usize, + need: usize, + }, + /// [`facet::unproject`] refused an operand row's facet. `input_index` is `Some(i)` for the + /// `i`-th input, `None` for the output operand. Carries the inversion's own typed error — + /// never a bespoke shape (spec §3.1, council ledger row 2). + FacetInversion { + site: (u64, usize), + input_index: Option, + overflow: FacetOverflow, + }, +} + +impl ReconstructionMiss { + #[must_use] + pub fn site(&self) -> (u64, usize) { + match self { + ReconstructionMiss::MissingOperands { site, .. } + | ReconstructionMiss::FacetInversion { site, .. } => *site, + } + } +} + +/// [`reconstruct`]'s output: rebuilt ops plus every miss, reported — never skipped. +#[derive(Debug, Clone, PartialEq, Default)] +pub struct Reconstruction { + pub ops: Vec, + pub misses: Vec, +} + +/// Rebuild op skeletons from flat rows (spec §3.3). +/// +/// Grouping keys are the rows' OWN provenance: [`FactKind::Op`] rows are sited by +/// `prov.op_site` (a melted Op row always has one — the furnace ladder derives its block +/// anchor from it); operand rows attach by shared `prov.inst` (`ore.rs` emits the Op row and +/// its operand rows with the identical `base_prov`). `OperandIn` rows order by their own `a` +/// payload (the input index); completeness is judged against the op row's own `b` payload, +/// never against the source. +#[must_use] +pub fn reconstruct(rows: &[FlatFact], spaces: &CustomSpaceTable) -> Reconstruction { + // inst.0 -> (ordered input facets by index, output facet) + struct Operands { + ins: BTreeMap, + out: Option, + } + let mut operands: BTreeMap = BTreeMap::new(); + let mut op_rows: Vec<&FlatFact> = Vec::new(); + + for row in rows { + match row.kind { + FactKind::Op => op_rows.push(row), + FactKind::OperandIn => { + if let Some(inst) = row.prov.inst { + operands + .entry(inst.0) + .or_insert_with(|| Operands { + ins: BTreeMap::new(), + out: None, + }) + .ins + .insert(row.a, row.at); + } + } + FactKind::OperandOut => { + if let Some(inst) = row.prov.inst { + operands + .entry(inst.0) + .or_insert_with(|| Operands { + ins: BTreeMap::new(), + out: None, + }) + .out = Some(row.at); + } + } + // Edge / memory / predicate / call rows carry no operand varnodes of their own + // (block-anchored facets) — nothing to rebuild from them here. + _ => {} + } + } + + let mut out = Reconstruction::default(); + + for op_row in op_rows { + // A melted Op row always carries an op site (the ladder's block anchor is derived from + // it); a row without one cannot be sited and cannot participate in the source-site + // universe, so it is skipped rather than guessed at. + let Some(site) = op_row.prov.op_site else { + continue; + }; + let arity = (op_row.b & 0xFFFF_FFFF) as usize; + let has_output = (op_row.b >> 32) & 1 == 1; + + let empty = Operands { + ins: BTreeMap::new(), + out: None, + }; + let ops = op_row + .prov + .inst + .and_then(|inst| operands.get(&inst.0)) + .unwrap_or(&empty); + + let have = ops.ins.len() + usize::from(ops.out.is_some()); + let need = arity + usize::from(has_output); + if ops.ins.len() != arity || ops.out.is_some() != has_output { + out.misses + .push(ReconstructionMiss::MissingOperands { site, have, need }); + continue; + } + + let mut inputs = Vec::with_capacity(arity); + let mut inversion_miss = None; + for (index, (_, at)) in ops.ins.iter().enumerate() { + match facet::unproject(at, spaces) { + Ok(vn) => inputs.push(vn), + Err(overflow) => { + inversion_miss = Some(ReconstructionMiss::FacetInversion { + site, + input_index: Some(index), + overflow, + }); + break; + } + } + } + if let Some(miss) = inversion_miss { + out.misses.push(miss); + continue; + } + + let output = match &ops.out { + None => None, + Some(at) => match facet::unproject(at, spaces) { + Ok(vn) => Some(vn), + Err(overflow) => { + out.misses.push(ReconstructionMiss::FacetInversion { + site, + input_index: None, + overflow, + }); + continue; + } + }, + }; + + out.ops.push(ReconstructedOp { + site, + ordinal: op_row.a, + skeleton: OpSkeleton { + opcode: op_row.opcode, + output, + inputs, + }, + }); + } + + out +} + +// ================================================================================================ +// judge — the verdict +// ================================================================================================ + +/// One site where the reconstructed skeleton differs from the source's — both carried as typed +/// values so a report renders fields, never `Debug`. +#[derive(Debug, Clone, PartialEq)] +pub struct SkeletonMismatch { + pub site: (u64, usize), + pub source: OpSkeleton, + pub reconstructed: OpSkeleton, +} + +/// One matched op whose variant carries semantic state the skeleton cannot (see [`gaps_of`]). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct AttributeGap { + pub site: (u64, usize), + pub opcode: OpTag, + pub attribute: GapAttribute, +} + +/// The oracle's conservation reading over the source-op-site universe (spec §3.4). +#[derive(Debug, Clone, PartialEq, Default)] +pub struct OracleVerdict { + /// Rule 1: reconstructed complete AND skeleton-equal. + pub matched: usize, + /// Rule 3: not reconstructed, but ≥1 ledger residual anchored at the site. + pub ledger_accounted: usize, + /// Ledger rows with `provenance.op_site == None` — SSA-level facts (phi inputs, + /// `CallDefine`, the Edge no-facet case) OUTSIDE the source-site universe. Counted, never + /// errors, never silently dropped. + pub ssa_only_residuals: usize, + /// Rule 4: neither reconstructed nor accounted — the failure signal. + pub orphans: Vec<(u64, usize)>, + /// Rule 2: reconstructed but unequal — checked BEFORE the ledger criterion; a mismatch is + /// never excused by a coincident residual at the same site. + pub mismatches: Vec, + /// The measured "what the skeleton cannot carry" census over MATCHED ops. + pub attribute_gaps: Vec, +} + +impl OracleVerdict { + /// The oracle passes iff every source op site is matched or ledger-accounted. + /// Attribute gaps and SSA-only residuals do not fail the verdict — they are measurements. + #[must_use] + pub fn holds(&self) -> bool { + self.orphans.is_empty() && self.mismatches.is_empty() + } +} + +/// Partition every source op site per spec §3.4's 4-way precedence. +#[must_use] +pub fn judge( + source: &[R2ILBlock], + recon: &Reconstruction, + ledger: &ResidualLedger, +) -> OracleVerdict { + let by_site: BTreeMap<(u64, usize), &ReconstructedOp> = + recon.ops.iter().map(|op| (op.site, op)).collect(); + + let mut ledger_sites: BTreeSet<(u64, usize)> = BTreeSet::new(); + let mut ssa_only_residuals = 0usize; + for row in ledger.rows() { + match row.provenance.op_site { + Some(site) => { + ledger_sites.insert(site); + } + None => ssa_only_residuals += 1, + } + } + + let mut verdict = OracleVerdict { + ssa_only_residuals, + ..OracleVerdict::default() + }; + + for block in source { + for (op_idx, op) in block.ops.iter().enumerate() { + let site = (block.addr, op_idx); + let source_skeleton = OpSkeleton::of(op); + if let Some(rebuilt) = by_site.get(&site) { + if rebuilt.skeleton == source_skeleton { + verdict.matched += 1; + for &attribute in gaps_of(source_skeleton.opcode) { + verdict.attribute_gaps.push(AttributeGap { + site, + opcode: source_skeleton.opcode, + attribute, + }); + } + } else { + verdict.mismatches.push(SkeletonMismatch { + site, + source: source_skeleton, + reconstructed: rebuilt.skeleton.clone(), + }); + } + } else if ledger_sites.contains(&site) { + verdict.ledger_accounted += 1; + } else { + verdict.orphans.push(site); + } + } + } + + verdict +} + +// ================================================================================================ +// permissive_convention — the oracle's measurement config +// ================================================================================================ + +/// Build the oracle's MEASUREMENT convention for `blocks`: classify every opcode present, and +/// give every space that appears (the four fixed spaces via [`R2ilConvention::from_arch`]'s own +/// fall-through rows, plus a deliberate fall-through row per CUSTOM space) a resolvable root. +/// +/// This is pure config — data through the existing constructors, never a new `smelt` arm +/// (spec frozen 6). It is NOT a shipped default and deliberately inverts `from_arch`'s +/// no-custom-fall-through doctrine: the oracle WANTS everything resolvable so that what fails +/// to round-trip is the machinery's fault, not the config's. Production conventions keep the +/// doctrine; this one is for measuring. +/// +/// # Errors +/// [`FacetOverflow`] if the blocks' custom-space raw ids exceed the interned-ordinal budget — +/// a config-key must be lossless, same rule as everywhere else in `facet.rs`. +pub fn permissive_convention(blocks: &[R2ILBlock]) -> Result { + let mut tags: BTreeSet = BTreeSet::new(); + let mut custom_raws: BTreeSet = BTreeSet::new(); + + for block in blocks { + for op in &block.ops { + tags.insert(OpTag::from_r2il(op)); + for vn in op.inputs().into_iter().chain(op.output()) { + if let SpaceId::Custom(raw) = vn.space { + custom_raws.insert(raw); + } + } + } + } + + let mut arch = ArchSpec::new("oracle-permissive"); + for &raw in &custom_raws { + arch.spaces.push(AddressSpace { + id: SpaceId::Custom(raw), + name: format!("custom{raw}"), + addr_size: 8, + word_size: 1, + is_default: false, + endianness: None, + memory_class: None, + permissions: None, + valid_ranges: Vec::new(), + bank_id: None, + segment_id: None, + }); + } + + let mut conv = R2ilConvention::from_arch(&arch, tags)?; + + for &raw in &custom_raws { + // `from_arch` interned the raw id into the table above, so the ordinal exists; a raw + // the table does not know is exactly the lossless-config-key refusal `from_arch` + // already returned Err for. + if let Some(discriminant) = conv.spaces().ordinal_of(raw) { + let at = crate::facet::FacetPrefix::Space { discriminant }; + conv.insert(crate::convention::ConventionRow { + at, + name: Some(format!("custom{raw}")), + note: Some("oracle permissive fall-through".to_string()), + state: crate::convention::ValidationState::Unmeasured, + }); + } + } + + Ok(conv) +} diff --git a/crates/ruff_r2il/tests/oracle_roundtrip.rs b/crates/ruff_r2il/tests/oracle_roundtrip.rs new file mode 100644 index 00000000000000..b5ce9f73f67f50 --- /dev/null +++ b/crates/ruff_r2il/tests/oracle_roundtrip.rs @@ -0,0 +1,355 @@ +//! Gate-3 fixtures for the round-trip reconstruction oracle +//! (`.claude/plans/r2il-roundtrip-oracle-spec-v1.md` §5, ratified v3). +//! +//! Every guard here has a can-fire AND a can-stay-silent half, and the two negative tests +//! (mismatch, orphan) corrupt REAL smelted rows rather than hand-built ones, so they exercise +//! the same partition path the positive tests do. + +use r2il::memory::MemoryOrdering; +use r2il::{R2ILBlock, R2ILOp, SpaceId, Varnode}; +use ruff_r2il::behavior::FunctionBehavior; +use ruff_r2il::convention::R2ilConvention; +use ruff_r2il::furnace::{self, FactKind, FlatFact}; +use ruff_r2il::oracle::{self, GapAttribute, OracleVerdict, Reconstruction}; +use ruff_r2il::sink::{self, OfflineSink, RefinedTruthSink}; +use ruff_r2il::slag::ResidualLedger; + +fn reg(offset: u64, size: u32) -> Varnode { + Varnode::register(offset, size) +} + +fn con(value: u64, size: u32) -> Varnode { + Varnode::constant(value, size) +} + +/// A diamond CFG that forces one 2-input phi at the merge block: `0x1000` conditionally +/// branches to `0x1008`; `0x1004` and `0x1008` write DIFFERENT values into the same register +/// and both branch to `0x100c`, which returns that register. Six source ops total, four +/// opcodes (`CBranch`, `Copy`, `Branch`, `Return`), operands only in the register/const +/// spaces so every operand resolves under a rooted convention. +fn diamond_with_phi() -> Vec { + let mut b0 = R2ILBlock::new(0x1000, 4); + b0.push(R2ILOp::CBranch { + target: con(0x1008, 8), + cond: reg(0x8, 1), + }); + + let mut b1 = R2ILBlock::new(0x1004, 4); + b1.push(R2ILOp::Copy { + dst: reg(0x0, 8), + src: con(1, 8), + }); + b1.push(R2ILOp::Branch { + target: con(0x100c, 8), + }); + + let mut b2 = R2ILBlock::new(0x1008, 4); + b2.push(R2ILOp::Copy { + dst: reg(0x0, 8), + src: con(2, 8), + }); + b2.push(R2ILOp::Branch { + target: con(0x100c, 8), + }); + + let mut b3 = R2ILBlock::new(0x100c, 4); + b3.push(R2ILOp::Return { + target: reg(0x0, 8), + }); + + vec![b0, b1, b2, b3] +} + +/// smelt + reconstruct + judge under one convention — the whole pipeline the oracle measures. +fn run_oracle( + blocks: &[R2ILBlock], + conv: &R2ilConvention, +) -> (Vec, ResidualLedger, OracleVerdict) { + let behavior = FunctionBehavior::from_blocks_raw(blocks, None).expect("fixture ingests"); + let (rows, ledger, report) = furnace::smelt(&behavior, blocks, conv); + assert!(report.is_conserved(), "furnace conservation must hold"); + let recon = oracle::reconstruct(&rows, conv.spaces()); + let verdict = oracle::judge(blocks, &recon, &ledger); + (rows, ledger, verdict) +} + +#[test] +fn full_melt_under_the_permissive_convention_matches_every_source_op_exactly() { + let blocks = diamond_with_phi(); + let conv = oracle::permissive_convention(&blocks).expect("fixed spaces cannot overflow"); + let (_, _, verdict) = run_oracle(&blocks, &conv); + + assert!(verdict.holds(), "orphans/mismatches must be empty"); + assert_eq!(verdict.matched, 6, "every source op site skeleton-matches"); + assert_eq!( + verdict.ledger_accounted, 0, + "nothing needs accounting under full melt" + ); + // Four SSA-level constructs carry no source op site (`prov.op_site: None`) and land + // exclusively in `ssa_only_residuals`, never against a matched op: the one phi's Op fact + // (`ore.rs`'s `base_prov.op_site: None` for `InstPayload::Phi`) plus its two `PhiInput` + // facts, and the CBranch's `Predicate` fact — `OreFact::Predicate` always carries + // `prov.inst: None` (`ore.rs:997`), so `furnace.rs`'s parent-melted lookup keyed by `inst` + // always misses for it and it residualizes regardless of convention; a pre-existing + // furnace behaviour this oracle measures rather than changes. + assert_eq!(verdict.ssa_only_residuals, 4); + // Silence half of the gap channel: none of CBranch/Copy/Branch/Return carries + // non-varnode semantic state. + assert!(verdict.attribute_gaps.is_empty()); +} + +#[test] +fn minimal_pass_one_accounts_everything_and_matches_nothing() { + let blocks = diamond_with_phi(); + let minimal = R2ilConvention::minimal_pass_one(); + let (_, _, verdict) = run_oracle(&blocks, &minimal); + + assert!(verdict.holds(), "accounted, not orphaned"); + // Pinned EXACT per the ratified spec (council ledger row 15): all 7 classified opcodes + // carry >= 1 operand and no operand melts under a zero-row convention, so no op can fully + // reconstruct. A `matched >= 1` assertion here would be unsatisfiable. + assert_eq!(verdict.matched, 0); + assert_eq!( + verdict.ledger_accounted, 6, + "every source op site is ledger-accounted" + ); + + let conv = oracle::permissive_convention(&blocks).expect("fixed spaces cannot overflow"); + let (_, _, permissive) = run_oracle(&blocks, &conv); + assert!( + verdict.matched < permissive.matched, + "the two conventions must measure different things: minimal {} vs permissive {}", + verdict.matched, + permissive.matched + ); +} + +/// Locate the OperandIn row of `site` with input index `index` among smelted rows. +fn operand_in_row_index(rows: &[FlatFact], site: (u64, usize), index: u64) -> usize { + rows.iter() + .position(|row| { + row.kind == FactKind::OperandIn && row.prov.op_site == Some(site) && row.a == index + }) + .expect("fixture must contain the operand row") +} + +#[test] +fn a_corrupted_operand_facet_fires_exactly_one_mismatch() { + let blocks = diamond_with_phi(); + let conv = oracle::permissive_convention(&blocks).expect("fixed spaces cannot overflow"); + let behavior = FunctionBehavior::from_blocks_raw(&blocks, None).expect("fixture ingests"); + let (mut rows, ledger, _) = furnace::smelt(&behavior, &blocks, &conv); + + let target = operand_in_row_index(&rows, (0x1004, 0), 0); + rows[target].at = + ruff_r2il::facet::project(&con(99, 8), conv.spaces()).expect("const projects in any table"); + + let recon = oracle::reconstruct(&rows, conv.spaces()); + let verdict = oracle::judge(&blocks, &recon, &ledger); + + assert!(!verdict.holds()); + assert_eq!(verdict.mismatches.len(), 1, "exactly the corrupted site"); + assert_eq!(verdict.mismatches[0].site, (0x1004, 0)); + assert_eq!(verdict.matched, 5, "the other five sites still match"); +} + +#[test] +fn swapped_operand_facets_across_two_ops_fire_both_mismatches() { + // Cross-row corruption must be visible at BOTH sites, not cancel out (spec gate 3 / S5's + // forward-comparison blind-spot finding). The two Copy ops' source constants (1 vs 2) + // guarantee the swapped facets differ. + let blocks = diamond_with_phi(); + let conv = oracle::permissive_convention(&blocks).expect("fixed spaces cannot overflow"); + let behavior = FunctionBehavior::from_blocks_raw(&blocks, None).expect("fixture ingests"); + let (mut rows, ledger, _) = furnace::smelt(&behavior, &blocks, &conv); + + let first = operand_in_row_index(&rows, (0x1004, 0), 0); + let second = operand_in_row_index(&rows, (0x1008, 0), 0); + assert_ne!( + rows[first].at, rows[second].at, + "anti-vacuity: the two source constants must project to different facets" + ); + let tmp = rows[first].at; + rows[first].at = rows[second].at; + rows[second].at = tmp; + + let recon = oracle::reconstruct(&rows, conv.spaces()); + let verdict = oracle::judge(&blocks, &recon, &ledger); + + assert!(!verdict.holds()); + let mut sites: Vec<(u64, usize)> = verdict.mismatches.iter().map(|m| m.site).collect(); + sites.sort_unstable(); + assert_eq!(sites, vec![(0x1004, 0), (0x1008, 0)]); +} + +#[test] +fn a_site_with_neither_rows_nor_residuals_is_an_orphan() { + let blocks = diamond_with_phi(); + let conv = oracle::permissive_convention(&blocks).expect("fixed spaces cannot overflow"); + let behavior = FunctionBehavior::from_blocks_raw(&blocks, None).expect("fixture ingests"); + let (rows, ledger, _) = furnace::smelt(&behavior, &blocks, &conv); + + let victim = (0x100c_u64, 0_usize); + let filtered: Vec = rows + .iter() + .copied() + .filter(|row| row.prov.op_site != Some(victim)) + .collect(); + assert!( + filtered.len() < rows.len(), + "anti-vacuity: the filter must actually remove the victim's rows" + ); + + let recon = oracle::reconstruct(&filtered, conv.spaces()); + let verdict = oracle::judge(&blocks, &recon, &ledger); + + assert!(!verdict.holds()); + assert_eq!(verdict.orphans, vec![victim]); + assert_eq!(verdict.matched, 5); +} + +#[test] +fn load_and_fence_fire_their_typed_attribute_gaps() { + let mut b0 = R2ILBlock::new(0x2000, 4); + b0.push(R2ILOp::Load { + dst: reg(0x0, 8), + space: SpaceId::Ram, + addr: con(0x8000, 8), + }); + b0.push(R2ILOp::Fence { + ordering: MemoryOrdering::SeqCst, + }); + b0.push(R2ILOp::Branch { + target: con(0x2004, 8), + }); + let mut b1 = R2ILBlock::new(0x2004, 4); + b1.push(R2ILOp::Return { + target: reg(0x0, 8), + }); + let blocks = vec![b0, b1]; + + let conv = oracle::permissive_convention(&blocks).expect("fixed spaces cannot overflow"); + let (_, _, verdict) = run_oracle(&blocks, &conv); + + assert!(verdict.holds()); + // Fence's skeleton is (Fence, None, []) — trivially equal — so its ONLY semantic content + // travels through the gap channel; a silent pass here would be the exact defect the + // channel exists to prevent. + let mut gaps: Vec<(&str, (u64, usize))> = verdict + .attribute_gaps + .iter() + .map(|gap| (gap.attribute.as_str(), gap.site)) + .collect(); + gaps.sort_unstable(); + assert_eq!( + gaps, + vec![ + ("memory_ordering", (0x2000, 1)), + ("memory_space", (0x2000, 0)), + ] + ); +} + +#[test] +fn gaps_of_covers_exactly_the_twelve_table_variants() { + use ruff_r2il::ore::OpTag; + + let twelve = [ + OpTag::Load, + OpTag::Store, + OpTag::Fence, + OpTag::LoadLinked, + OpTag::StoreConditional, + OpTag::AtomicCAS, + OpTag::LoadGuarded, + OpTag::StoreGuarded, + OpTag::CallOther, + OpTag::Subpiece, + OpTag::PtrAdd, + OpTag::PtrSub, + ]; + for tag in twelve { + assert!( + !oracle::gaps_of(tag).is_empty(), + "{} must carry at least one gap attribute", + tag.as_str() + ); + } + for tag in [ + OpTag::Copy, + OpTag::IntAdd, + OpTag::Branch, + OpTag::Return, + OpTag::BoolAnd, + OpTag::Phi, + ] { + assert!( + oracle::gaps_of(tag).is_empty(), + "{} must carry no gap attribute", + tag.as_str() + ); + } +} + +#[test] +fn gap_attribute_has_no_catch_all_and_stable_names() { + // Mirrors slag.rs's `there_is_no_catch_all_reason`: every variant's name is in ALL, ALL + // has no duplicates, and none of the names is a catch-all. + let all = GapAttribute::ALL; + let variants = [ + GapAttribute::MemorySpace, + GapAttribute::MemoryOrdering, + GapAttribute::UserOpIndex, + GapAttribute::SubpieceOffset, + GapAttribute::PtrElementSize, + ]; + assert_eq!(all.len(), variants.len()); + for v in variants { + assert!(all.contains(&v.as_str())); + assert!(!matches!(v.as_str(), "other" | "unknown" | "misc")); + } + let mut sorted: Vec<&str> = all.to_vec(); + sorted.sort_unstable(); + sorted.dedup(); + assert_eq!(sorted.len(), all.len(), "no duplicate names"); +} + +// Unlike `src/`, ruff's directory-scoped `clippy.toml` disallowed-methods list does NOT reach +// this integration-test target, so `std::env::temp_dir`/`std::fs` need no suppression here (an +// `#[expect]` would itself fail as an unfulfilled expectation under `-D warnings`). +#[test] +fn the_artifact_mediated_verdict_equals_the_in_memory_verdict() { + let blocks = diamond_with_phi(); + let conv = oracle::permissive_convention(&blocks).expect("fixed spaces cannot overflow"); + let behavior = FunctionBehavior::from_blocks_raw(&blocks, None).expect("fixture ingests"); + let (rows, ledger, report) = furnace::smelt(&behavior, &blocks, &conv); + + let in_memory = oracle::judge(&blocks, &oracle::reconstruct(&rows, conv.spaces()), &ledger); + + let dir = std::env::temp_dir().join(format!("ruff_r2il_oracle_arm_{}", std::process::id())); + let mut sink_backend = OfflineSink::new(&dir); + sink_backend + .write_harvest("oracle_arm", &rows, &ledger, &report) + .expect("offline write succeeds"); + + let facts_path = dir.join("oracle_arm.facts.tsv"); + let residuals_path = dir.join("oracle_arm.residuals.tsv"); + let read_rows = sink::read_facts(&facts_path).expect("v2 facts read back"); + let read_residuals = sink::read_residuals(&residuals_path).expect("v2 residuals read back"); + std::fs::remove_dir_all(&dir).ok(); + + let mut read_ledger = ResidualLedger::new(); + for row in read_residuals { + read_ledger.push(row); + } + + let recon: Reconstruction = oracle::reconstruct(&read_rows, conv.spaces()); + let from_artifacts = oracle::judge(&blocks, &recon, &read_ledger); + + // The load-bearing claim of the v2 schemas: everything the oracle needs survives the + // write→read round trip, so the two verdicts are EQUAL — same counts, same gap census, + // same (empty) orphan/mismatch lists. + assert_eq!(from_artifacts, in_memory); + assert!(from_artifacts.holds()); + assert_eq!(from_artifacts.matched, 6); +}