RQ-61-MVORACLE (#1097): promote the #1093-class silent-miscompile differential into a CI-wired red-first oracle - #1122
Merged
Merged
Conversation
avrabe
added a commit
that referenced
this pull request
Sep 1, 2026
The PR number (#1122), not the issue number — the RQ-61-VCLOSURE confusion (#1118) applied preemptively. Refs #1097 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
… decline, promoted into a CI-wired red-first oracle The #1096 guard survived; its justification lived in a lane scratchpad. This commits the demonstration: the PRE-#1096 compiler's own emitted objects (fixture rev b2abf95 = c4b463f^, regenerable via --capture) are re-executed under unicorn against wasmtime-first values on every CI run. Demonstrated SILENT-WRONG (exit 0, wrong value), pinned exactly: if/ARM ipe(0) -> 0xC0DE0003 (uninitialized-R3 canary), want 7 if/RV32 ipe(0) -> uninitialized-T2 canary, want 7 block/RV32 bpb(1) -> uninitialized-T2 canary (dropped br_if param), want 7 loop/RV32 lpb(3) -> 2 (mis-reconciled back-edge join), want 10 Negative results pinned as such, not manufactured: block/ARM was CORRECT pre-#1096 on all 7 probed vectors (that leg's decline is conservative); loop/ARM was already refused by the #509 back-edge decline (the fixture records that refusal, needle-checked). Green half: all six shape x backend legs decline cleanly on main (exit 1, not 101, no "panicked at", no object written, the shared #1093 needle), and a guard module of supported neighbours (plain `if (result)`, value-carrying forward br_if) still compiles and matches wasmtime on both backends — the decline covers the class, not everything. Floors: `# ci-checks: emulations >= 19` (11 fixture + 8 guard unicorn entries). That floor CANNOT see the decline half (#1113 — a refused compile emulates nothing), so the script carries refusals == 6 in-script (non-zero exit otherwise) and ci.yml greps `refusals:` plus the `silent-wrong vectors: 4 (of 4 pinned)` partition line (#1112 pattern). Red-first: pointing SYNTH at the pre-#1096 binary fails the oracle — all six legs accepted + refusals=0 VACUOUS, exit 1. Refs #1097 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
The PR number (#1122), not the issue number — the RQ-61-VCLOSURE confusion (#1118) applied preemptively. Refs #1097 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…D declines in the ARM corpus sweep The #973 sweep's EXPECTED_DECLINES is exact both ways, so the new declining fixtures reddened it on their own PR — correctly. Measured at the sweep's own flags (cortex-m4f --relocatable --all-exports): if/block/loop decline (rc=1, no object; the #1096 class, by design), guard COMPILES (rc=0) and is deliberately absent from the list — the sweep now also executes its 2 exports x 12 vectors (0 mismatches). Sweep re-run locally: 155/171 compiled, 2526 vectors, PASS, exit 0. Refs #1097 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
force-pushed
the
feat/mvoracle-1097
branch
from
September 1, 2026 22:12
09f76ad to
9dc073d
Compare
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
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.
RQ-61-MVORACLE — the evidence for the #1096 decline, made permanent and executable
Refs #1097. The inverse of this release's other findings: the #1096 guard is right, but the demonstration of why it is mandatory lived in a lane scratchpad. This PR promotes it into
scripts/repro/, CI-wired, red-first.What the oracle does on every CI run
Red half — the pre-#1096 compiler's own bytes, re-executed. The committed fixture
param_block_silent_1097_red_pre1096.jsonholds the objects emitted at revb2abf951(c4b463f3^, one commit before the #1096 merge; regenerable via--capture, recipe in the docstring). They run under unicorn against wasmtime-first expected values, with every ABI-unassigned register seeded with a canary that names it (0xC0DE0000 | index). The four demonstrated silent miscompiles must reproduce exactly as pinned:if (param i32)no else, ARMipe(0)0xC0DE0003— the uninitialized R3 canary (the issue's exact shape)7if (param i32)no else, RV32ipe(0)0xC0DE0012— uninitialized T2 canary7block (param i32)+br_if, RV32bpb(1)0xC0DE0012— the taken edge drops the carried param7loop (param i32)+back-edge, RV32lpb(3)2— mis-reconciled join once the back-edge is taken10Negative results, pinned as such (not manufactured):
block/ARM was correct pre-#1096 on all 7 probed vectors — that leg's decline is conservative, and the oracle pins it as MATCH so the honest matrix survives.loop/ARM never compiled pre-#1096 (the #509 back-edge decline predates #1096); the fixture records that refusal and the oracle needle-checks it.Green half — current main. All six shape x backend legs decline cleanly: exit 1 (not the panic 101), no
panicked at, no object written, the shared #1093 needle present. A guard module of supported neighbours (plainif (result), value-carrying forwardbr_if— the #483/#509 shapes) must still compile and match wasmtime on both backends, so the guard cannot silently grow past its class.Floors, and what each cannot see
# ci-checks: emulations >= 19(11 fixture + 8 guard unicorn entries). Per An oracle's ci-checks floor cannot see its decline half — 4 oracles could lose that half and stay green #1113 this floor cannot see the decline half — a refused compile emulates nothing — nor whether the wrong vectors stayed wrong.refusals == 6(non-zero exit at less),refusals:line grepped in ci.yml (the fix(oracle): #1104 shadowed the aarch64 builder guard and left its oracle pinned to the superseded wording #1112 pattern).silent-wrong vectors == 4, plus the ci.yml grep of the exact partition line — a red half that stops demonstrating the miscompile cannot stay green.Red-first demonstrated
Pointing
SYNTHat the pre-#1096 binary fails the oracle: all six legs reportexit 0 (accepted); object written; missing needle, thenVACUOUS: refusals=0, exit 1.Gates run locally
cargo fmt --check0 ·cargo clippy --workspace --all-targets -- -D warnings0 ·oracle_wiring_check.py0 (182 scripts, 0 undeclared) ·claim_check.py0 ·status_evidence_check.py0 (45 delivery commits matched) · oracle underoracle_run.py:measured=19,RESULT: PASS, exit 0.Artifact
RQ-61-MVORACLEflipped toimplemented; itsdone-whenis now the machine signature of the CI wiring (the load-bearing half of the filed manual predicate).🤖 Generated with Claude Code
https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L