From b04f369d667e63a3096e186be5bed906a790142d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 27 Jun 2026 09:23:55 +0200 Subject: [PATCH] =?UTF-8?q?test(vcr-oracle):=20pin=20the=20#518=20cross-ba?= =?UTF-8?q?ckend=20contrast=20=E2=80=94=20RV32=20loud-skips,=20ARM=20silen?= =?UTF-8?q?tly=20miscompiles=20(#242,=20#518)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit No new external signal this issue-hunt pass (gates #418/#472/#396-emitter still await external triggers; no new issues/comments since watermark; deps unchanged). Bounded behavior-frozen #242 increment, cross-backend parity (VCR-SEL-005): measure how the #518 i64-param root cause manifests on RISC-V. Measured (objdump symtab + compile stderr): the SAME root cause (an i64 param is never classified i64, so it reaches an i64 op as an i32 operand) is SILENT on ARM (#518 miscompile) but LOUD-SKIPPED on RV32. The RV32 selector validates the operand-stack TYPE before lowering an i64 op, hits `stack type mismatch ... expected i64, found i32`, returns a typed Err → `warning: skipping function …` + absent symbol. That is the #378/#180/#185 never-guess Ok-or-Err contract acting as the honest-fail backstop ARM's select_with_stack LACKS for i64 params. So on this class RV32 is INCOMPLETE-but-SOUND; ARM is COMPLETE-but-UNSOUND until the gated fix. - scripts/repro/i64_param_518_riscv_loudskip.py: asserts all 7 i64-param fns are loud-skipped (warning + absent symbol) AND the i32 control (t_i32) is emitted (non-vacuity — the skip is #518-specific, not a blanket backend failure). A regression removing the RV32 stack-type guard would flip a loud-skip into a silent miscompile, which the oracle catches. - roadmap VCR-ORACLE-001 #518 entry: record the cross-backend contrast. FROZEN-SAFE — no codegen touched (frozen anchors 3/3 green); rivet clean. Co-Authored-By: Claude Opus 4.8 --- artifacts/verified-codegen-roadmap.yaml | 14 +++ scripts/repro/i64_param_518_riscv_loudskip.py | 111 ++++++++++++++++++ 2 files changed, 125 insertions(+) create mode 100644 scripts/repro/i64_param_518_riscv_loudskip.py diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 62bc304..3380b79 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -767,6 +767,20 @@ artifacts: with no i64 param are byte-identical by construction (the frozen anchors carry no i64 params), so the fix is frozen-safe on flip. Byte-changing, silicon- gated — its own gated session, never an idle tick. + CROSS-BACKEND CONTRAST (2026-06-27, measured): the SAME root cause is SILENT + on ARM but LOUD-SKIPPED on RISC-V. The RV32 selector validates the operand- + stack TYPE before lowering an i64 op, so an i64 param reaching `I64Add` as an + i32 operand trips `stack type mismatch ... expected i64, found i32` → typed + `Err` → `warning: skipping function …` + absent symbol (the #378/#180/#185 + never-guess Ok-or-Err contract as the honest-fail backstop ARM's + `select_with_stack` LACKS for i64 params). So on this class RV32 is INCOMPLETE + (cannot yet compile i64-param functions) but SOUND (no silent wrong-code), + while ARM is COMPLETE-but-UNSOUND until the gated fix — the precise + VCR-SEL-005 parity shape (ARM lowers X; RV32 loud-declines X). Pinned by + `scripts/repro/i64_param_518_riscv_loudskip.py` (all 7 i64-param fns + loud-skipped, i32 control emitted): a regression removing the RV32 stack-type + guard would flip a loud-skip into a silent miscompile, which the oracle + catches. status: approved tags: [oracle, differential, coverage, mcdc, validation, track-c, riscv] links: diff --git a/scripts/repro/i64_param_518_riscv_loudskip.py b/scripts/repro/i64_param_518_riscv_loudskip.py new file mode 100644 index 0000000..743a282 --- /dev/null +++ b/scripts/repro/i64_param_518_riscv_loudskip.py @@ -0,0 +1,111 @@ +#!/usr/bin/env python3 +"""#518 cross-backend contrast — RISC-V LOUD-SKIPS the i64-param class (#242, #518). + +Companion to `i64_param_518_differential.py` (which proves the ARM selectors +SILENTLY MISCOMPILE an i64 binop reading an i64 param). This oracle measures the +SAME fixture on the RISC-V backend and shows the SAME root cause (an i64 param is +never classified i64, so it reaches an i64 op as an i32 operand) manifests +DIFFERENTLY: the RV32 selector validates the operand-stack TYPE before lowering +the i64 op, hits `stack type mismatch ... expected i64, found i32`, and returns a +typed `Err` → the function is LOUD-SKIPPED (a `warning: skipping function …` plus +absence from the emitted symbol table), never emitted as wrong code. + +This is the #378 never-guess contract (the ARM encoder's Ok-or-Err discipline, +#180/#185) acting as the honest-fail backstop that ARM's `select_with_stack` +LACKS for i64 params. The consequence for the VCR-SEL-005 cross-backend parity +ledger: on this class RV32 is INCOMPLETE (cannot yet compile i64-param functions) +but SOUND (no silent wrong-code); ARM is COMPLETE-but-UNSOUND (#518) until its +gated fix lands. A future regression that removed the RV32 stack-type guard would +flip a loud-skip into a silent miscompile — this oracle catches that. + +What it asserts (analysis-only — compiles + inspects symtab/stderr, runs nothing): + - every i64-PARAM function (t_add/t_sub/t_or/t_mixed/t_ii_add/t_i64_i32/ + t_snd_i64) is LOUD-SKIPPED: a `skipping function ''` warning is emitted + AND the name is absent from the .o symbol table. + - the i32 control (t_i32) IS emitted (present in the symtab) — the i32 path is + unaffected, so the skip is specific to the i64-param defect, not a blanket + backend failure (non-vacuity). + +Run (needs the riscv backend built in; default features include it): + SYNTH=./target/debug/synth python scripts/repro/i64_param_518_riscv_loudskip.py +Exits 0 when the loud-skip contract holds exactly; 1 if any i64-param function was +silently emitted (a real RV32 regression) or the i32 control was skipped. +""" +import os +import subprocess +import sys +from pathlib import Path + +from elftools.elf.elffile import ELFFile + +WAT = Path(__file__).with_name("i64_param_518.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") +OUT = "/tmp/i518_rv_loudskip.o" + +I64_PARAM_FNS = [ + "t_add", "t_sub", "t_or", "t_mixed", "t_ii_add", "t_i64_i32", "t_snd_i64", +] +I32_CONTROL = "t_i32" + + +def compile_riscv(): + cmd = [SYNTH, "compile", str(WAT), "-o", OUT, "-b", "riscv", + "--target", "riscv32imac", "--all-exports", "--relocatable"] + r = subprocess.run(cmd, capture_output=True, text=True, + env={"PATH": "/usr/bin:/bin"}) + if r.returncode != 0: + sys.exit(f"riscv compile failed (expected success with skips): {r.stderr}") + return r.stderr + + +def emitted_funcs(): + e = ELFFile(open(OUT, "rb")) + return { + s.name + for sec in e.iter_sections() + if sec.header.sh_type == "SHT_SYMTAB" + for s in sec.iter_symbols() + if s.name and s["st_info"]["type"] == "STT_FUNC" + } + + +def main(): + stderr = compile_riscv() + emitted = emitted_funcs() + print("=== RV32 #518 loud-skip contract ===") + fails = 0 + + for fn in I64_PARAM_FNS: + warned = f"skipping function '{fn}'" in stderr + absent = fn not in emitted + ok = warned and absent + if not ok: + fails += 1 + why = [] + if not warned: + why.append("no skip warning") + if not absent: + why.append("SILENTLY EMITTED (regression!)") + print(f" [{'ok ' if ok else 'BUG'}] {fn}: loud-skipped" + + ("" if ok else f" [{', '.join(why)}]")) + + ctrl_ok = I32_CONTROL in emitted + if not ctrl_ok: + fails += 1 + print(f" [{'ok ' if ctrl_ok else 'BUG'}] {I32_CONTROL}: i32 control emitted" + + ("" if ctrl_ok else " [skipped — backend broken, not #518-specific]")) + + print("\n--- verdict ---") + if fails == 0: + print("RESULT: PASS — RV32 loud-skips the #518 i64-param class (honest-fail " + "backstop) while emitting the i32 control. Same root cause as ARM, " + "but SOUND (no silent wrong-code) vs ARM's silent miscompile.") + sys.exit(0) + print(f"RESULT: FAIL — {fails} issue(s): an i64-param function was silently " + "emitted (RV32 stack-type guard regressed → would miscompile), or the " + "i32 control was lost.") + sys.exit(1) + + +if __name__ == "__main__": + main()