r2il: the round-trip reconstruction oracle (PR2 gate deliverable) - #103
Merged
Conversation
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AGVLyRZNEKKBSfBDJfbY3V
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AGVLyRZNEKKBSfBDJfbY3V
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AGVLyRZNEKKBSfBDJfbY3V
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.
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_9fa8a30f-0b1f-4c81-88b6-b4272ecbc672) |
AdaWorldAPI
marked this pull request as ready for review
August 18, 2026 13:20
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
The PR2 gate deliverable from
.claude/plans/r2il-behavioral-ir-v1.md§14:R2IL → routes → semantic-equivalent R2IL, with SPO explicitly NOT the
oracle. Follows #101 (sink trait) and #102 (v2 schemas + readers).
Designed through a 5+3 council (5 research savants → consolidate → 3 brutal
reviewers → fix → ratify), whose spec is committed alongside the code at
.claude/plans/r2il-roundtrip-oracle-spec-v1.md— v1, draft v2 and ratified v3are three separate commits on this branch, and §7 is the full change ledger
including the losing findings.
The headline result
Zero reconstruction mismatches across 35,946 matched op sites in four
binaries. Full numbers:
.claude/harvest/r2il/ORACLE-RESULT.md.Two caveats that the doc, the module docs, and the example's own output all
carry rather than bury:
permissive_conventionand proves thereconstruction MECHANISM. The shipped
minimal_pass_onemeasuresmatched = 0— it has zero convention rows, so no operand melts and itround-trips through accounting, not matching. The example always prints
both columns so the two claims can never be conflated.
assumed. Only ~50% of a chunk's blocks are reachable from its entry
(1835/3427 on
stress_test), soCFG::from_blocksdrops the rest and theirops produce no facts at all. The arithmetic confirms it exactly:
8053 matched + 6105 orphans = 14158 = that binary's
ops_totalfrom the §12profile. The in-repo fixtures, which use coherent CFGs, report zero orphans.
What landed
src/oracle.rs—OpSkeleton(the typed equivalence target),reconstruct(groups Op rows byprov.op_site, operands by sharedprov.inst, completeness judged against the op row's own payload),judge(a true 4-way partition with defined precedence: matched /mismatched / ledger_accounted / orphan, plus an
ssa_only_residualschannelfor residuals with no op site),
GapAttribute+gaps_of, andpermissive_convention.facet::unprojectis CONSUMED, not rebuilt — the council's code-truthsavant found it already ships with the exact property tests the first draft
proposed adding, so §3.1 collapsed from "build it" to "use it".
R2ILOpvariants carry semantic statebeyond their varnode projection; matched ops of those variants emit a typed
AttributeGapinstead of passing silently. Opens plan item O6:memory_spacedominates (3586),subpiece_offsetis small (113), and threekinds are unmeasured on this corpus (no atomics) — recorded as absence of
evidence, not evidence of absence.
examples/r2il_roundtrip_oracle.rs(featurelift) + docs: the resultartifact, a guide §1 row, a README entry, and plan items O6/O6a.
Not in this slice
No schema change, no
FlatFactfield (the 88-byte pin holds), nofurnace/ore/slagsemantics touched. Still open for PR2: codebook wiring(
ogar_codebook), and the optional SPO projection of semantic facts.Test plan
cargo test— 61 tests (40 lib + 12 fixtures + 9 new oracle), all greencargo clippy --all-targets -- -D warningsand--features lift— cleancargo fmt --check— cleanuv run --only-group dev prek run --files <changed>— cleancomparison 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
in-memory one, proving r2il: fix lossy v1 sink artifacts, add facts/residuals reader #102's v2 schemas are reconstruction-sufficient
🤖 Generated with Claude Code
Generated by Claude Code