From b623ac732e81cf0695c516dc1b98da4a9134998d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:31:37 +0200 Subject: [PATCH 1/9] =?UTF-8?q?feat(#890):=20oracle-wiring=20gate=20?= =?UTF-8?q?=E2=80=94=20declared=20ci-status=20per=20repro=20script=20(step?= =?UTF-8?q?=201/5)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds scripts/oracle_wiring_check.py: every scripts/repro/*.py|*.sh must carry exactly one `# ci-status:` declaration (wired | manual () — reason | unwired — reason), and a `wired` declaration is VERIFIED against .github/workflows/*.yml so a green board can never sit on top of an inert gate. Step 1 declares the 82 scripts a workflow already references. The remaining 70 are UNDECLARED and the gate is red on them by construction — classified next. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- scripts/oracle_wiring_check.py | 303 ++++++++++++++++++ scripts/repro/aarch64_add_538_differential.py | 1 + .../repro/aarch64_bounds_865_differential.py | 1 + scripts/repro/aarch64_calls_851.py | 1 + scripts/repro/aarch64_cf_538_differential.py | 1 + .../aarch64_ctrlflow_851_differential.py | 1 + .../repro/aarch64_divrem_851_differential.py | 1 + .../repro/aarch64_locals_851_differential.py | 1 + scripts/repro/aarch64_m2_538_differential.py | 1 + scripts/repro/aarch64_m2_decline_538.py | 1 + .../aarch64_m3_floats_538_differential.py | 1 + ...arch64_m4_trunc_minmax_538_differential.py | 1 + scripts/repro/aarch64_matrix.sh | 1 + scripts/repro/aarch64_mem_851_differential.py | 1 + .../repro/aarch64_surface_851_differential.py | 1 + scripts/repro/addw_offset_681_differential.py | 1 + scripts/repro/block_brif_483_differential.py | 1 + scripts/repro/br_table_507_differential.py | 1 + scripts/repro/brif_outer_740_differential.py | 1 + .../bulk_local_clobber_677_differential.py | 1 + scripts/repro/bulk_mask_679_differential.py | 1 + .../repro/cabi_arena_bind_418_differential.py | 1 + ...indirect_275_selfcontained_differential.py | 1 + ...75_selfcontained_execution_differential.py | 1 + .../repro/call_indirect_642_differential.py | 1 + .../repro/call_indirect_650_differential.py | 1 + .../repro/call_indirect_664_differential.py | 1 + .../repro/call_indirect_676_differential.py | 1 + .../repro/callee_saved_490_differential.py | 1 + .../repro/cmp_select_two_move_differential.py | 1 + .../const_addr_fold_riscv_differential.py | 1 + scripts/repro/const_cse_differential.py | 1 + scripts/repro/control_step_differential.py | 1 + .../f32_mem_trunc_708_709_differential.py | 1 + scripts/repro/f32_ops_719_differential.py | 1 + scripts/repro/f32_vfp_619_differential.py | 1 + scripts/repro/f64_369_differential.py | 1 + .../fact_spec_bounds_494_differential.py | 1 + .../repro/fact_spec_clamp_494_differential.py | 1 + .../repro/fact_spec_div_494_differential.py | 1 + .../repro/fact_spec_mask_494_differential.py | 1 + .../fact_spec_select_494_differential.py | 1 + scripts/repro/flight_seam_differential.py | 1 + .../float_select_return_782_differential.py | 1 + scripts/repro/frame_slot_dce_differential.py | 1 + .../framebacking_i64param_837_differential.py | 1 + scripts/repro/gpio_thin_846_differential.py | 1 + .../repro/i32_shift_mask_682_differential.py | 1 + .../repro/i64_float_conv_869_differential.py | 1 + .../repro/i64_global_init_649_differential.py | 1 + scripts/repro/i64_param_518_differential.py | 1 + scripts/repro/i64_rot_div_610_differential.py | 1 + .../repro/i64_spill_pool_587_differential.py | 1 + .../repro/i64_stack_param_503_differential.py | 1 + scripts/repro/mem757_gale_differential.py | 1 + .../mem757_rawvec_memcopy_differential.py | 1 + .../mem761_linmem_r9_overlap_differential.py | 1 + .../repro/multi_memory_406_differential.py | 1 + .../multi_segment_static_data_differential.py | 1 + scripts/repro/r12_spill_496_differential.py | 1 + ...allgraph_275_selfcontained_differential.py | 1 + scripts/repro/rem_s_666_differential.py | 1 + .../riscv_extern_call_871_differential.py | 1 + .../repro/rv32_br_table_882_differential.py | 1 + .../repro/rv32_data_798_boot_differential.py | 1 + scripts/repro/rv32_label_882_differential.py | 1 + .../rv32_mem_size_grow_242_differential.py | 1 + .../repro/safety_bounds_377_differential.py | 1 + .../self_contained_data_758_differential.py | 1 + .../repro/shift_fold_riscv_differential.py | 1 + scripts/repro/spill_frame_499_differential.py | 1 + scripts/repro/stack_args_503_differential.py | 1 + .../repro/stack_layout_687_differential.py | 1 + .../repro/static_above_sp_739_differential.py | 1 + scripts/repro/trunc_sat_782_differential.py | 1 + scripts/repro/unreachable_665_differential.py | 1 + .../vcr_dec_001_graph_alloc_differential.py | 1 + ...c_001_join_alloc_execution_differential.py | 1 + scripts/repro/vcr_ra_003_phase2_join_call.py | 1 + .../repro/vcr_ra_003_rv32_alloc_validator.py | 1 + scripts/repro/vfp_spill_881_differential.py | 1 + scripts/repro/wide_static_746_differential.py | 1 + .../wide_static_copy_757_differential.py | 1 + 83 files changed, 385 insertions(+) create mode 100644 scripts/oracle_wiring_check.py diff --git a/scripts/oracle_wiring_check.py b/scripts/oracle_wiring_check.py new file mode 100644 index 00000000..07fb59b5 --- /dev/null +++ b/scripts/oracle_wiring_check.py @@ -0,0 +1,303 @@ +#!/usr/bin/env python3 +"""oracle_wiring_check — gate the EXECUTION-ORACLE surface against CI wiring. + +The problem this exists to kill (#890): `scripts/repro/*.py` are synth's +execution oracles — the differentials that catch silent miscompiles. Writing an +oracle and WIRING an oracle are two steps, and the second is the one that gets +dropped under release pressure. Before this gate, 69 of 150 repro scripts were +referenced by no workflow at all, and nothing in the tree distinguished + + "manual by design — needs gale's pinned drop / real silicon / a toolchain + CI does not install" + +from + + "somebody forgot". + +A forgotten gate is indistinguishable from an intentional one, so the only way +to tell was to read all 150 and reason about each — an audit that kept +rediscovering the same defect one instance at a time. v0.53 hand-wired three +and the unwired count still went UP: instances were fixed, the factory was not. + +THE MECHANISM — a declared status per script, in a header comment +-------------------------------------------------------------------------- +Each `scripts/repro/*.py` (and `*.sh`) carries EXACTLY ONE declaration line: + + # ci-status: wired + # ci-status: manual (hardware) — needs a real STM32H743; no emulator path + # ci-status: unwired — needs a compile line + ELF arg; no blocker + +Chosen over a central manifest deliberately: + + * LOCALITY. The declaration lives in the file it describes, so it shows up in + the diff of the PR that adds the script — the author cannot add an oracle + without meeting the convention. A manifest is edited far from the script and + goes stale on rename/delete. + * NO SECOND SOURCE OF TRUTH. A manifest entry can disagree with reality + (script deleted, entry left behind); a header cannot outlive its file. + * The repo already reserves the central-ledger shape (`claims.yaml`) for + claims that have NO natural home (prose spread across many docs). A script's + CI status has a natural home: the script. + +THREE STATUSES, on purpose +-------------------------------------------------------------------------- + wired — at least one `.github/workflows/*.yml` references the file by name. + VERIFIED here: declaring `wired` without a workflow reference is a + hard failure. This is the exact "green board, inert gate" defect. + manual — legitimately NOT CI-runnable. Requires a CATEGORY from the fixed + list below plus a reason. Categories are a closed set so the manual + surface stays groupable and arguable, not a free-text dumping + ground. + unwired — KNOWN DEBT: no blocker, simply not wired yet. Separated from + `manual` so honest blockers and backlog cannot hide in each other. + This is the count that must ratchet DOWN (pinned in claims.yaml). + +Undeclared = failure. New scripts are FORCED to choose. + +Exit: 0 = every script declared and consistent · 1 = drift +""" + +import argparse +import glob +import json +import os +import pathlib +import re +import sys + +# The closed set of `manual` categories. Adding one is a deliberate code change +# (and a review conversation), not a free-text escape hatch. +MANUAL_CATEGORIES = { + "hardware": "needs real silicon / a board CI does not have", + "toolchain": "needs a toolchain CI does not install (cross binutils, qemu, ...)", + "external-input": "needs an input that is not in-tree (a pinned vendor drop, a gist)", + "network": "fetches over the network at run time", + "measurement": "produces a REPORT, not a pass/fail verdict — nothing to gate on", + "superseded": "the behaviour is gated elsewhere; kept as historical repro only", + "red-first": "asserts a defect that is still OPEN — expected to fail today", + "scratch": "ad-hoc probe kept for provenance; carries no assertions", + "slow": "runtime is prohibitive for per-PR CI", +} + +DECL_RE = re.compile( + r"^#\s*ci-status:\s*(?P[A-Za-z-]+)" + r"(?:\s*\((?P[a-z-]+)\))?" + r"\s*(?:[-—:]+\s*(?P.*))?$", + re.MULTILINE, +) + +PLACEHOLDER_RE = re.compile(r"^\s*(todo|tbd|t\.b\.d\.?|n/?a|xxx|fixme|-+)\s*$", re.I) + +MIN_REASON_CHARS = 20 + + +def repo_root(): + return pathlib.Path(__file__).resolve().parent.parent + + +def collect(root): + scripts = sorted( + glob.glob(str(root / "scripts/repro/*.py")) + + glob.glob(str(root / "scripts/repro/*.sh")) + ) + workflows = sorted( + glob.glob(str(root / ".github/workflows/*.yml")) + + glob.glob(str(root / ".github/workflows/*.yaml")) + ) + return scripts, workflows + + +def classify(root, scripts, workflows): + """Return (records, failures). One record per script; failures are strings.""" + wf_text = { + os.path.basename(w): pathlib.Path(w).read_text(errors="ignore") + for w in workflows + } + blob = "\n".join(wf_text.values()) + + records, fails = [], [] + for path in scripts: + rel = os.path.relpath(path, root) + name = os.path.basename(path) + text = pathlib.Path(path).read_text(errors="ignore") + refs = sorted(w for w, t in wf_text.items() if name in t) + + decls = list(DECL_RE.finditer(text)) + if not decls: + fails.append( + f"{rel}: UNDECLARED — add a `# ci-status:` header line " + f"(wired | manual () — reason | unwired — reason). " + f"An oracle nothing runs must SAY so." + ) + records.append({"script": rel, "status": "undeclared", "workflows": refs}) + continue + if len(decls) > 1: + fails.append( + f"{rel}: {len(decls)} `# ci-status:` lines — exactly one is allowed" + ) + m = decls[0] + status = m.group("status").lower() + category = (m.group("category") or "").lower() or None + reason = (m.group("reason") or "").strip() + + rec = { + "script": rel, + "status": status, + "category": category, + "reason": reason, + "workflows": refs, + } + records.append(rec) + + if status == "wired": + if not refs: + fails.append( + f"{rel}: declares `wired` but NO workflow references it — " + f"the gate is INERT. Wire it in .github/workflows/, or " + f"downgrade the declaration to `unwired`/`manual`." + ) + if category: + fails.append(f"{rel}: `wired` takes no category (got {category!r})") + elif status in ("manual", "unwired"): + if refs: + fails.append( + f"{rel}: declares `{status}` but IS referenced by " + f"{', '.join(refs)} — flip the declaration to `wired`." + ) + if not reason or PLACEHOLDER_RE.match(reason) or len(reason) < MIN_REASON_CHARS: + fails.append( + f"{rel}: `{status}` needs a REAL reason (>= {MIN_REASON_CHARS} " + f"chars, not a placeholder); got {reason!r}" + ) + if status == "manual": + if not category: + fails.append( + f"{rel}: `manual` needs a category: " + f"{', '.join(sorted(MANUAL_CATEGORIES))}" + ) + elif category not in MANUAL_CATEGORIES: + fails.append( + f"{rel}: unknown manual category {category!r} — " + f"allowed: {', '.join(sorted(MANUAL_CATEGORIES))}" + ) + elif category: + fails.append(f"{rel}: `unwired` takes no category (got {category!r})") + else: + fails.append( + f"{rel}: unknown ci-status {status!r} — " + f"expected wired | manual | unwired" + ) + + # Reverse direction: a workflow may not reference a repro script that is + # gone (a rename that half-landed leaves a step that can never run). + on_disk = {os.path.basename(p) for p in scripts} | { + os.path.basename(p) for p in glob.glob(str(root / "scripts/repro/*")) + } + for ref in sorted(set(re.findall(r"scripts/repro/([\w.\-]+)", blob))): + if ref not in on_disk: + fails.append( + f".github/workflows: references scripts/repro/{ref}, which does " + f"NOT exist — dangling CI step" + ) + + return records, fails + + +def summarize(records): + out = {"total": len(records), "wired": 0, "manual": 0, "unwired": 0, "undeclared": 0} + by_cat = {} + for r in records: + s = r["status"] + out[s] = out.get(s, 0) + 1 + if s == "manual" and r.get("category"): + by_cat[r["category"]] = by_cat.get(r["category"], 0) + 1 + out["manual_by_category"] = dict(sorted(by_cat.items())) + return out + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("--json", metavar="PATH", help="write the summary as JSON") + ap.add_argument("--list", action="store_true", help="print every script + status") + args = ap.parse_args() + + root = repo_root() + scripts, workflows = collect(root) + + # ------------------------------------------------------------------ + # ANTI-VACUITY. This gate must not become the thing it polices: a check + # that measures nothing and exits 0. If the globs come up empty (moved + # directory, renamed workflows, run from the wrong root) that is a HARD + # failure, never a silent pass. + # ------------------------------------------------------------------ + if not scripts: + sys.exit("oracle_wiring_check: VACUOUS — scripts/repro/*.py matched NO files") + if not workflows: + sys.exit("oracle_wiring_check: VACUOUS — .github/workflows/*.yml matched NO files") + + records, fails = classify(root, scripts, workflows) + summary = summarize(records) + + if summary["wired"] == 0: + fails.append( + "VACUOUS — zero scripts classify as `wired`; the reference " + "derivation is broken (did the workflow layout move?)" + ) + + if args.list: + for r in sorted(records, key=lambda r: (r["status"], r["script"])): + tag = r["status"] + (f"({r['category']})" if r.get("category") else "") + where = ",".join(r["workflows"]) or "-" + print(f" {tag:<22} {os.path.basename(r['script']):<52} {where}") + print() + + print( + f"oracle wiring: {summary['total']} repro scripts — " + f"{summary['wired']} wired, {summary['manual']} manual, " + f"{summary['unwired']} unwired(debt), {summary['undeclared']} UNDECLARED" + ) + if summary["manual_by_category"]: + print( + " manual by category: " + + ", ".join(f"{k}={v}" for k, v in summary["manual_by_category"].items()) + ) + + if args.json: + pathlib.Path(args.json).write_text( + json.dumps( + {"summary": summary, "scripts": records}, indent=2, sort_keys=True + ) + + "\n" + ) + + # A GitHub step summary keeps the manual/unwired backlog visible on every + # run instead of only in a log nobody opens. + step_summary = os.environ.get("GITHUB_STEP_SUMMARY") + if step_summary: + with open(step_summary, "a") as fh: + fh.write("### Oracle wiring (#890)\n\n") + fh.write( + f"| total | wired | manual | unwired (debt) | undeclared |\n" + f"|---|---|---|---|---|\n" + f"| {summary['total']} | {summary['wired']} | {summary['manual']} " + f"| {summary['unwired']} | {summary['undeclared']} |\n\n" + ) + debt = [r for r in records if r["status"] == "unwired"] + if debt: + fh.write("**Unwired debt** (wire these; the count must ratchet down):\n\n") + for r in sorted(debt, key=lambda r: r["script"]): + fh.write(f"- `{os.path.basename(r['script'])}` — {r['reason']}\n") + fh.write("\n") + + if fails: + print() + for f in fails: + print(f"FAIL {f}") + print(f"\n{len(fails)} oracle-wiring failure(s).") + return 1 + print("all repro scripts declare a CI status, and every `wired` one is wired.") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/repro/aarch64_add_538_differential.py b/scripts/repro/aarch64_add_538_differential.py index ef4c2110..f48e31bb 100644 --- a/scripts/repro/aarch64_add_538_differential.py +++ b/scripts/repro/aarch64_add_538_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#538 milestone-1b — validate the aarch64 backend's codegen end-to-end. Compiles a small integer module with `synth compile -b aarch64`, then executes diff --git a/scripts/repro/aarch64_bounds_865_differential.py b/scripts/repro/aarch64_bounds_865_differential.py index 88724c9a..f7b55205 100644 --- a/scripts/repro/aarch64_bounds_865_differential.py +++ b/scripts/repro/aarch64_bounds_865_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#865 — aarch64 linear-memory BOUNDS differential (gale's OOB table). gale (#865): the v0.51.0 aarch64 lowering emitted NO bounds check and diff --git a/scripts/repro/aarch64_calls_851.py b/scripts/repro/aarch64_calls_851.py index 8cbb6140..127d4ed5 100644 --- a/scripts/repro/aarch64_calls_851.py +++ b/scripts/repro/aarch64_calls_851.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """synth aarch64 direct-`call` execution differential (#851, lane L3). The standing gate `aarch64_matrix.sh` is single-function (it loads only the diff --git a/scripts/repro/aarch64_cf_538_differential.py b/scripts/repro/aarch64_cf_538_differential.py index 557b9acd..5c752f85 100644 --- a/scripts/repro/aarch64_cf_538_differential.py +++ b/scripts/repro/aarch64_cf_538_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#538 control-flow increment — the void-block br/br_if EXECUTION differential. The #538 aarch64 backend gains its first control-flow construct: forward diff --git a/scripts/repro/aarch64_ctrlflow_851_differential.py b/scripts/repro/aarch64_ctrlflow_851_differential.py index 37fa9e54..dfa76b96 100644 --- a/scripts/repro/aarch64_ctrlflow_851_differential.py +++ b/scripts/repro/aarch64_ctrlflow_851_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#851 aarch64 FULL control-flow — if/else, loop back-edge, return EXECUTION diff. The #851 increment extends the void-block-only #538 control flow with: diff --git a/scripts/repro/aarch64_divrem_851_differential.py b/scripts/repro/aarch64_divrem_851_differential.py index 0754c473..78b8378c 100644 --- a/scripts/repro/aarch64_divrem_851_differential.py +++ b/scripts/repro/aarch64_divrem_851_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#851 — aarch64 integer div/rem trap-and-value EXECUTION differential. A64 SDIV/UDIV are TOTAL where WASM `idiv`/`irem` (Core §4.3.2) are PARTIAL, so diff --git a/scripts/repro/aarch64_locals_851_differential.py b/scripts/repro/aarch64_locals_851_differential.py index dfe6843a..999aede1 100644 --- a/scripts/repro/aarch64_locals_851_differential.py +++ b/scripts/repro/aarch64_locals_851_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#851 — aarch64 NON-PARAM LOCALS execution differential (RED-first). Compiles `aarch64_locals_851.wat` with `synth compile -b aarch64`, then executes diff --git a/scripts/repro/aarch64_m2_538_differential.py b/scripts/repro/aarch64_m2_538_differential.py index 69940faa..61b62a4e 100755 --- a/scripts/repro/aarch64_m2_538_differential.py +++ b/scripts/repro/aarch64_m2_538_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#538 milestone-2 — validate the BROADENED aarch64 backend codegen end-to-end. Compiles the m2 acceptance module with `synth compile -b aarch64`, then executes diff --git a/scripts/repro/aarch64_m2_decline_538.py b/scripts/repro/aarch64_m2_decline_538.py index bcd5f469..a243769d 100755 --- a/scripts/repro/aarch64_m2_decline_538.py +++ b/scripts/repro/aarch64_m2_decline_538.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#538 milestone-2 — assert the aarch64 decline matrix stays HONEST. The broadening in m2 covers the full i32/i64 integer ALU, but four classes are diff --git a/scripts/repro/aarch64_m3_floats_538_differential.py b/scripts/repro/aarch64_m3_floats_538_differential.py index 707e8e4e..934b2aff 100755 --- a/scripts/repro/aarch64_m3_floats_538_differential.py +++ b/scripts/repro/aarch64_m3_floats_538_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#538 milestone-3 — validate the aarch64 SCALAR-FLOAT backend codegen. Compiles the m3 float acceptance module with `synth compile -b aarch64`, then diff --git a/scripts/repro/aarch64_m4_trunc_minmax_538_differential.py b/scripts/repro/aarch64_m4_trunc_minmax_538_differential.py index 9976c765..eeeb48a3 100644 --- a/scripts/repro/aarch64_m4_trunc_minmax_538_differential.py +++ b/scripts/repro/aarch64_m4_trunc_minmax_538_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#538 milestone-4 — the #709 boundary-table EXECUTION differential. m4 converts the aarch64 backend's #709-class declines into capabilities: diff --git a/scripts/repro/aarch64_matrix.sh b/scripts/repro/aarch64_matrix.sh index b5a95890..ad655a2b 100755 --- a/scripts/repro/aarch64_matrix.sh +++ b/scripts/repro/aarch64_matrix.sh @@ -1,4 +1,5 @@ #!/usr/bin/env bash +# ci-status: wired # synth aarch64 execution-differential acceptance gate. # Compiles a broad WASM op set with `synth -b aarch64`, executes each accepted op NATIVELY on an # arm64 host (MAP_JIT), and diffs bit-exact vs wasmtime. Exits non-zero on any MISCOMPILE (a declined diff --git a/scripts/repro/aarch64_mem_851_differential.py b/scripts/repro/aarch64_mem_851_differential.py index 8ff5f06d..7e8eb28a 100644 --- a/scripts/repro/aarch64_mem_851_differential.py +++ b/scripts/repro/aarch64_mem_851_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#851 — execution-differential for aarch64 linear-memory load/store. Compiles a `(memory 1)` module of store/load round-trips with diff --git a/scripts/repro/aarch64_surface_851_differential.py b/scripts/repro/aarch64_surface_851_differential.py index 647af007..7ff12998 100644 --- a/scripts/repro/aarch64_surface_851_differential.py +++ b/scripts/repro/aarch64_surface_851_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#851 v0.53 — execution-differential for the aarch64 op-surface closes. The VCR-SEL-005 third-backend enumeration (cross_backend_op_parity.rs, aarch64 diff --git a/scripts/repro/addw_offset_681_differential.py b/scripts/repro/addw_offset_681_differential.py index de7f392e..028e8bad 100644 --- a/scripts/repro/addw_offset_681_differential.py +++ b/scripts/repro/addw_offset_681_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#681 — T3 ADD.W raw-immediate packing: dynamic base + static offset 0x100..0xFFF. `encode_thumb32_add_imm` packed the raw offset into the T3 ADD.W ThumbExpandImm diff --git a/scripts/repro/block_brif_483_differential.py b/scripts/repro/block_brif_483_differential.py index 5ef39cd7..87828caa 100644 --- a/scripts/repro/block_brif_483_differential.py +++ b/scripts/repro/block_brif_483_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#483 (epic #242) — EXECUTION-validate optimized-path block/br_if lowering. On the OPTIMIZED (non-`--relocatable`) ARM path, a forward `block` + `br_if` diff --git a/scripts/repro/br_table_507_differential.py b/scripts/repro/br_table_507_differential.py index 2b37a4f3..5b56dcd2 100644 --- a/scripts/repro/br_table_507_differential.py +++ b/scripts/repro/br_table_507_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#507 (epic #242) — EXECUTION-validate the optimized-path br_table fix. On the optimized (non-`--relocatable`) path, `synth compile` silently diff --git a/scripts/repro/brif_outer_740_differential.py b/scripts/repro/brif_outer_740_differential.py index 4f56f58c..e1caff9a 100644 --- a/scripts/repro/brif_outer_740_differential.py +++ b/scripts/repro/brif_outer_740_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#740 — EXECUTION-validate the direct path's wide conditional branches on the loop-inside-block shape: a `br_if` at a loop head exiting an OUTER block. diff --git a/scripts/repro/bulk_local_clobber_677_differential.py b/scripts/repro/bulk_local_clobber_677_differential.py index 15af0b76..5f47867f 100644 --- a/scripts/repro/bulk_local_clobber_677_differential.py +++ b/scripts/repro/bulk_local_clobber_677_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#677 — bulk-memory operand-register clobber differential (thumb-2). The #374 memory.copy/memory.fill lowering mutated its popped operand registers diff --git a/scripts/repro/bulk_mask_679_differential.py b/scripts/repro/bulk_mask_679_differential.py index ea2aaeae..b409db9f 100644 --- a/scripts/repro/bulk_mask_679_differential.py +++ b/scripts/repro/bulk_mask_679_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#679 — `--safety-bounds mask` bulk-memory coverage oracle (thumb-2). Pre-fix, `memory.copy`/`memory.fill` under `--safety-bounds mask` were emitted diff --git a/scripts/repro/cabi_arena_bind_418_differential.py b/scripts/repro/cabi_arena_bind_418_differential.py index 18368dc7..83fda5d4 100644 --- a/scripts/repro/cabi_arena_bind_418_differential.py +++ b/scripts/repro/cabi_arena_bind_418_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#418 — self-contained binding of `env::__cabi_arena_realloc` (the meld dissolve gap): EXECUTION differential vs wasmtime. diff --git a/scripts/repro/call_indirect_275_selfcontained_differential.py b/scripts/repro/call_indirect_275_selfcontained_differential.py index e1d9571d..bf1222dd 100755 --- a/scripts/repro/call_indirect_275_selfcontained_differential.py +++ b/scripts/repro/call_indirect_275_selfcontained_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#275 — self-contained call_indirect: emission + residual-decline oracle. The v0.42 #717 interim (loud-decline on the whole self-contained path) was diff --git a/scripts/repro/call_indirect_275_selfcontained_execution_differential.py b/scripts/repro/call_indirect_275_selfcontained_execution_differential.py index ff7ba472..23cf0de3 100644 --- a/scripts/repro/call_indirect_275_selfcontained_execution_differential.py +++ b/scripts/repro/call_indirect_275_selfcontained_execution_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#275 — self-contained `--cortex-m` call_indirect EXECUTION differential. The finale of #275: the falcon shape — a SELF-CONTAINED Cortex-M image whose diff --git a/scripts/repro/call_indirect_642_differential.py b/scripts/repro/call_indirect_642_differential.py index 60fd1c41..d311727a 100644 --- a/scripts/repro/call_indirect_642_differential.py +++ b/scripts/repro/call_indirect_642_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#642 — call_indirect bounds-guard oracle: OOB index must TRAP, not branch. The Thumb-2 `call_indirect` expansion (`lsl.w ip, idx, #2; ldr.w ip, [r11, diff --git a/scripts/repro/call_indirect_650_differential.py b/scripts/repro/call_indirect_650_differential.py index c06705d7..49bb2d13 100644 --- a/scripts/repro/call_indirect_650_differential.py +++ b/scripts/repro/call_indirect_650_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#650 — multi-table call_indirect oracle: the contiguous R11 region. Layout contract (#650): the runtime/harness links every funcref table as ONE diff --git a/scripts/repro/call_indirect_664_differential.py b/scripts/repro/call_indirect_664_differential.py index 2eb12995..901ee2bc 100644 --- a/scripts/repro/call_indirect_664_differential.py +++ b/scripts/repro/call_indirect_664_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#664 — null-funcref-slot call_indirect oracle: sparse tables trap, not decline. The fixture's 4-slot table has only slots 1 and 3 initialized; 0 and 2 are diff --git a/scripts/repro/call_indirect_676_differential.py b/scripts/repro/call_indirect_676_differential.py index 2e657f77..e1006da2 100644 --- a/scripts/repro/call_indirect_676_differential.py +++ b/scripts/repro/call_indirect_676_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#676 — heterogeneous-table call_indirect oracle: runtime type check. The fixture's 5-slot table interleaves TWO structural signature classes diff --git a/scripts/repro/callee_saved_490_differential.py b/scripts/repro/callee_saved_490_differential.py index 5afefbc3..940fb711 100644 --- a/scripts/repro/callee_saved_490_differential.py +++ b/scripts/repro/callee_saved_490_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#490 (epic #242) — EXECUTION-validate optimized-path callee-saved preservation. The optimized ARM path (the default, non-`--relocatable` self-contained image) diff --git a/scripts/repro/cmp_select_two_move_differential.py b/scripts/repro/cmp_select_two_move_differential.py index cfaac016..afb957df 100755 --- a/scripts/repro/cmp_select_two_move_differential.py +++ b/scripts/repro/cmp_select_two_move_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-SEL-004 / VCR-ORACLE-001 (#428, #242) — EXECUTION-validate the two-move arm. gale's gust_codegen_bench follow-up (#428) proved that no real fixture — gust_mix diff --git a/scripts/repro/const_addr_fold_riscv_differential.py b/scripts/repro/const_addr_fold_riscv_differential.py index 8957bc91..07e6193f 100644 --- a/scripts/repro/const_addr_fold_riscv_differential.py +++ b/scripts/repro/const_addr_fold_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA RV32 lever (#472 step 2, epic #242) — EXECUTION-validate const-addr-fold. `SYNTH_RV_ADDR_FOLD=1` folds a constant memory address into the access immediate diff --git a/scripts/repro/const_cse_differential.py b/scripts/repro/const_cse_differential.py index 5dcc8801..8787bfc5 100755 --- a/scripts/repro/const_cse_differential.py +++ b/scripts/repro/const_cse_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA const-CSE (#242) — EXECUTION-validate the optimized-path const cache. The ARM path re-materializes a constant at every use: the same `i32.const N` diff --git a/scripts/repro/control_step_differential.py b/scripts/repro/control_step_differential.py index 5d6378e4..bd19a0e2 100644 --- a/scripts/repro/control_step_differential.py +++ b/scripts/repro/control_step_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#209 — control_step_decide reciprocal-multiply register-pressure regression. gale's `control_step_decide` (loom-lowered, 4× unsigned constant `div_u`: diff --git a/scripts/repro/f32_mem_trunc_708_709_differential.py b/scripts/repro/f32_mem_trunc_708_709_differential.py index ee98c8ea..ffd2a54f 100644 --- a/scripts/repro/f32_mem_trunc_708_709_differential.py +++ b/scripts/repro/f32_mem_trunc_708_709_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#708/#709 — EXECUTION-validate the phase-1b thumb-2 f32 increment. Two capabilities land on the v0.39.0 hard-float path: diff --git a/scripts/repro/f32_ops_719_differential.py b/scripts/repro/f32_ops_719_differential.py index 32dc54bf..2c535f74 100755 --- a/scripts/repro/f32_ops_719_differential.py +++ b/scripts/repro/f32_ops_719_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#719 — EXECUTION-validate the phase-1b thumb-2 f32 residual increment. After #708 (f32.load + reinterpret) landed, falcon's float functions skip on the diff --git a/scripts/repro/f32_vfp_619_differential.py b/scripts/repro/f32_vfp_619_differential.py index fda90291..d502c2ff 100755 --- a/scripts/repro/f32_vfp_619_differential.py +++ b/scripts/repro/f32_vfp_619_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """GI-FPU-002 (#619/#369) — EXECUTION-validate scalar f32 hard-float codegen. synth has a working VFP encoder + selector VFP lowering, but the decoder dropped diff --git a/scripts/repro/f64_369_differential.py b/scripts/repro/f64_369_differential.py index 1b73ffb9..25aa1629 100644 --- a/scripts/repro/f64_369_differential.py +++ b/scripts/repro/f64_369_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#369 (GI-FPU-002 phases 2+3) — EXECUTION-validate scalar f64 on cortex-m7dp (double-precision VFP). diff --git a/scripts/repro/fact_spec_bounds_494_differential.py b/scripts/repro/fact_spec_bounds_494_differential.py index bbcd7431..59b3c1c4 100644 --- a/scripts/repro/fact_spec_bounds_494_differential.py +++ b/scripts/repro/fact_spec_bounds_494_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#494 bounds-elision × #390 guard_bool — four-way execution differential for the ordeal-certified memory bounds-guard elision. diff --git a/scripts/repro/fact_spec_clamp_494_differential.py b/scripts/repro/fact_spec_clamp_494_differential.py index 0f0ddedf..48ff3faf 100644 --- a/scripts/repro/fact_spec_clamp_494_differential.py +++ b/scripts/repro/fact_spec_clamp_494_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-PERF-002 Phase 2 (#494) — in-bounds differential for the fact-spec clamp elision (oracle 2 of the design doc's three). diff --git a/scripts/repro/fact_spec_div_494_differential.py b/scripts/repro/fact_spec_div_494_differential.py index 33dd9633..0e6e4b6d 100644 --- a/scripts/repro/fact_spec_div_494_differential.py +++ b/scripts/repro/fact_spec_div_494_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-PERF-002 Phase 2b (#494) — in-bounds differential for the divisor-nonzero trap-guard elision (oracle 3), plus the red force-admit divergence demonstration (oracle 4). diff --git a/scripts/repro/fact_spec_mask_494_differential.py b/scripts/repro/fact_spec_mask_494_differential.py index f9de0be4..170fc73e 100755 --- a/scripts/repro/fact_spec_mask_494_differential.py +++ b/scripts/repro/fact_spec_mask_494_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-PERF-002 Phase 3+ (#494) — redundant-mask (narrowing) elision oracle. Builds the `gust_kernel` lane-pack fixture WITH schema-v1 `wsc.facts` diff --git a/scripts/repro/fact_spec_select_494_differential.py b/scripts/repro/fact_spec_select_494_differential.py index 815279cd..a5d409cf 100755 --- a/scripts/repro/fact_spec_select_494_differential.py +++ b/scripts/repro/fact_spec_select_494_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-PERF-002 Phase 3 (#494) — in-bounds differential for the fact-spec branchless SELECT-collapse elision (the Phase-2 clamp oracle's sibling). diff --git a/scripts/repro/flight_seam_differential.py b/scripts/repro/flight_seam_differential.py index 09dc8e9b..77c07c2a 100644 --- a/scripts/repro/flight_seam_differential.py +++ b/scripts/repro/flight_seam_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#212 — inlined-callee-after-opaque-call differential oracle. gale's loom-inlined `flight_algo` calls the opaque `filter_step` (which writes diff --git a/scripts/repro/float_select_return_782_differential.py b/scripts/repro/float_select_return_782_differential.py index f1f55343..17f3b220 100644 --- a/scripts/repro/float_select_return_782_differential.py +++ b/scripts/repro/float_select_return_782_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#782(b) — EXECUTION-validate float `select` + explicit float `return`. The dominant decline class on the real falcon-flight-v1.123 fused core diff --git a/scripts/repro/frame_slot_dce_differential.py b/scripts/repro/frame_slot_dce_differential.py index 3afd7c4f..cbc32631 100755 --- a/scripts/repro/frame_slot_dce_differential.py +++ b/scripts/repro/frame_slot_dce_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA frame-slot DCE (#242) — EXECUTION-validate stack-reload forwarding + dead-frame-store elimination on the optimized path. diff --git a/scripts/repro/framebacking_i64param_837_differential.py b/scripts/repro/framebacking_i64param_837_differential.py index 17a99f40..b14814b9 100644 --- a/scripts/repro/framebacking_i64param_837_differential.py +++ b/scripts/repro/framebacking_i64param_837_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#837 — frame-backing i64/f64-param lowering (the last #518 i64-param sub-case). gale's `gust:os/timer` provider hit a LOUD DECLINE (not a miscompile — the object diff --git a/scripts/repro/gpio_thin_846_differential.py b/scripts/repro/gpio_thin_846_differential.py index acbdcf98..1d09b08f 100644 --- a/scripts/repro/gpio_thin_846_differential.py +++ b/scripts/repro/gpio_thin_846_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#846 gpio-thin size-regression gate — SIZE drop + execution-UNCHANGED. gale's `gpio-thin` gust driver regressed +44 B / +9% (490→534 `.text`) on synth diff --git a/scripts/repro/i32_shift_mask_682_differential.py b/scripts/repro/i32_shift_mask_682_differential.py index 65e7df32..c5b38fa3 100644 --- a/scripts/repro/i32_shift_mask_682_differential.py +++ b/scripts/repro/i32_shift_mask_682_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#682 — thumb-2 i32 shifts must reduce the amount mod 32 (WASM §4.3.2). ARMv7-M register-controlled shifts consume Rm[7:0] and yield 0 (LSL/LSR) or diff --git a/scripts/repro/i64_float_conv_869_differential.py b/scripts/repro/i64_float_conv_869_differential.py index 88ca680f..48d59bf9 100644 --- a/scripts/repro/i64_float_conv_869_differential.py +++ b/scripts/repro/i64_float_conv_869_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#869 — the ARM 64-bit integer<->float conversion family EXECUTION differential (cortex-m7dp, Thumb-2, unicorn) vs wasmtime. diff --git a/scripts/repro/i64_global_init_649_differential.py b/scripts/repro/i64_global_init_649_differential.py index 1560e94f..48582af7 100644 --- a/scripts/repro/i64_global_init_649_differential.py +++ b/scripts/repro/i64_global_init_649_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#649 — nonzero i64.const GLOBAL INITIALIZERS silently zeroed. The decoder's `init_i32` captured only a leading `i32.const`; an i64 global's diff --git a/scripts/repro/i64_param_518_differential.py b/scripts/repro/i64_param_518_differential.py index bba07aad..ae10aea5 100644 --- a/scripts/repro/i64_param_518_differential.py +++ b/scripts/repro/i64_param_518_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#518 — CHARACTERIZE the i64-param binop miscompile on BOTH selectors. This is the *oracle-first* artifact for issue #518 (epic #242, VCR-RA/VCR-SEL): diff --git a/scripts/repro/i64_rot_div_610_differential.py b/scripts/repro/i64_rot_div_610_differential.py index 5d966b87..01e1523f 100644 --- a/scripts/repro/i64_rot_div_610_differential.py +++ b/scripts/repro/i64_rot_div_610_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired # #610: i64.rotl / i64.rotr / i64.div_u / i64.rem_u compiled to code returning # 0 for every input on the ARM Cortex-M path. The encoder expansions either # used colliding hardcoded scratch and restored it OVER the result (rot: `POP diff --git a/scripts/repro/i64_spill_pool_587_differential.py b/scripts/repro/i64_spill_pool_587_differential.py index e26a9b28..e48dcd4f 100644 --- a/scripts/repro/i64_spill_pool_587_differential.py +++ b/scripts/repro/i64_spill_pool_587_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#587 — DIRECT-PATH i64 spill-slot pool-grow differential oracle (epic #242). `i64_spill_pool_587.wat` keeps twenty i64 constants simultaneously live — diff --git a/scripts/repro/i64_stack_param_503_differential.py b/scripts/repro/i64_stack_param_503_differential.py index 2dc74266..2f696af1 100644 --- a/scripts/repro/i64_stack_param_503_differential.py +++ b/scripts/repro/i64_stack_param_503_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#503-i64 — AAPCS 64-bit STACK-param differential oracle (epic #242). Compiles `i64_stack_param_503.wat` — every shape of the previously-declined diff --git a/scripts/repro/mem757_gale_differential.py b/scripts/repro/mem757_gale_differential.py index 8861a703..0eece475 100644 --- a/scripts/repro/mem757_gale_differential.py +++ b/scripts/repro/mem757_gale_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#757 — gale's exact fused os-tl node (the real miscompile, not a reconstruction). `mem757_gale/loom.wasm` (md5 18da000d9142dfa0885f57578d3af150) is the meld-fused + diff --git a/scripts/repro/mem757_rawvec_memcopy_differential.py b/scripts/repro/mem757_rawvec_memcopy_differential.py index bca4ac48..2311ebfd 100644 --- a/scripts/repro/mem757_rawvec_memcopy_differential.py +++ b/scripts/repro/mem757_rawvec_memcopy_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#757 RED-FIRST differential — memmove (`memory.copy`) from a STATIC pointer. gale's real mechanism: a RawVec-grow `call` followed by a `memory.copy` whose diff --git a/scripts/repro/mem761_linmem_r9_overlap_differential.py b/scripts/repro/mem761_linmem_r9_overlap_differential.py index db0babc5..ab0f1f24 100644 --- a/scripts/repro/mem761_linmem_r9_overlap_differential.py +++ b/scripts/repro/mem761_linmem_r9_overlap_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#761 — self-contained --cortex-m full-page linmem view OVERLAPS the R9 globals table at the top of SRAM (a silent global<->linmem ALIAS: the worst class). diff --git a/scripts/repro/multi_memory_406_differential.py b/scripts/repro/multi_memory_406_differential.py index bd7eec5f..e387d2a0 100644 --- a/scripts/repro/multi_memory_406_differential.py +++ b/scripts/repro/multi_memory_406_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#406 (VCR-MEM-002 phase 1) execution differential: two wasm linear memories must be two DISTINCT native regions. diff --git a/scripts/repro/multi_segment_static_data_differential.py b/scripts/repro/multi_segment_static_data_differential.py index 03e73a0f..7e09ed68 100644 --- a/scripts/repro/multi_segment_static_data_differential.py +++ b/scripts/repro/multi_segment_static_data_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#406 / #739-cluster COVERAGE WIDENER — multi-chunk / multi-segment static data across BOTH the self-contained (`--cortex-m`, no --relocatable) and the `--relocatable` object paths, with segments at varied offsets: a low segment, an diff --git a/scripts/repro/r12_spill_496_differential.py b/scripts/repro/r12_spill_496_differential.py index eaefe8e1..cbadce69 100644 --- a/scripts/repro/r12_spill_496_differential.py +++ b/scripts/repro/r12_spill_496_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#496 (epic #242) — EXECUTION-validate the DEFAULT optimized-path register- exhaustion fix. diff --git a/scripts/repro/reachable_callgraph_275_selfcontained_differential.py b/scripts/repro/reachable_callgraph_275_selfcontained_differential.py index 2e711b46..56e19397 100644 --- a/scripts/repro/reachable_callgraph_275_selfcontained_differential.py +++ b/scripts/repro/reachable_callgraph_275_selfcontained_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#275 — the DIRECT reachable call graph must EXECUTE on the self-contained `--cortex-m` image (no --relocatable, no loader). diff --git a/scripts/repro/rem_s_666_differential.py b/scripts/repro/rem_s_666_differential.py index 5ba61d2e..fdfed7a8 100644 --- a/scripts/repro/rem_s_666_differential.py +++ b/scripts/repro/rem_s_666_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#666 — rv32 i32.rem_s(INT_MIN,-1) must return 0, not trap (WASM §4.3.2). The rv32 selector shared div_s's INT_MIN/-1 overflow `ebreak` guard with diff --git a/scripts/repro/riscv_extern_call_871_differential.py b/scripts/repro/riscv_extern_call_871_differential.py index be1b2d23..c1ef151a 100644 --- a/scripts/repro/riscv_extern_call_871_differential.py +++ b/scripts/repro/riscv_extern_call_871_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#871 — RV32 external-call relocations: read-back + link + execution oracle. gale's thin-seam drivers import a two-function mmio seam (env::mmio_read32 / diff --git a/scripts/repro/rv32_br_table_882_differential.py b/scripts/repro/rv32_br_table_882_differential.py index 2ebeacda..62496dbc 100644 --- a/scripts/repro/rv32_br_table_882_differential.py +++ b/scripts/repro/rv32_br_table_882_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#882 — RV32 br_table compare-chain execution oracle. RV32 lowers `br_table` as a compare-and-branch chain (`beq idx, x0` for entry diff --git a/scripts/repro/rv32_data_798_boot_differential.py b/scripts/repro/rv32_data_798_boot_differential.py index c530daf1..1a0b7b03 100644 --- a/scripts/repro/rv32_data_798_boot_differential.py +++ b/scripts/repro/rv32_data_798_boot_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#798 — RV32 active-data-segment shipping: FULL-BOOT differential. End-to-end over the REAL artifacts, not a model of them: synth compiles a diff --git a/scripts/repro/rv32_label_882_differential.py b/scripts/repro/rv32_label_882_differential.py index 29bdcdea..90d2c4d2 100644 --- a/scripts/repro/rv32_label_882_differential.py +++ b/scripts/repro/rv32_label_882_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#882 — RV32 `return`-inside-a-frame: label definition + reachable-join oracle. gale's i2c-thin driver (v0.52.0, `-b riscv --target esp32c3 --all-exports diff --git a/scripts/repro/rv32_mem_size_grow_242_differential.py b/scripts/repro/rv32_mem_size_grow_242_differential.py index f846e06e..20caa0fc 100644 --- a/scripts/repro/rv32_mem_size_grow_242_differential.py +++ b/scripts/repro/rv32_mem_size_grow_242_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#223 / #242 (VCR-SEL-005) — RV32 memory.size / memory.grow execution oracle. The v0.49 cross-backend op-parity gate ledgered `memory.size` and `memory.grow` diff --git a/scripts/repro/safety_bounds_377_differential.py b/scripts/repro/safety_bounds_377_differential.py index 0e7dfc56..b7551a17 100644 --- a/scripts/repro/safety_bounds_377_differential.py +++ b/scripts/repro/safety_bounds_377_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#377 — `--safety-bounds software` optimized-path enforcement differential. Pre-fix, `--safety-bounds software` emitted NO bounds check on the optimized diff --git a/scripts/repro/self_contained_data_758_differential.py b/scripts/repro/self_contained_data_758_differential.py index a83ff77a..ba2784f5 100755 --- a/scripts/repro/self_contained_data_758_differential.py +++ b/scripts/repro/self_contained_data_758_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#758 — the DEFAULT self-contained `--cortex-m` image silently DROPS active `(data …)` segments. diff --git a/scripts/repro/shift_fold_riscv_differential.py b/scripts/repro/shift_fold_riscv_differential.py index 0482ec7e..4394303e 100644 --- a/scripts/repro/shift_fold_riscv_differential.py +++ b/scripts/repro/shift_fold_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA RV32 lever (#472, epic #242) — EXECUTION-validate the imm-shift-fold. The immediate-shift-fold (SYNTH_RV_SHIFT_FOLD=1) rewrites a constant shift diff --git a/scripts/repro/spill_frame_499_differential.py b/scripts/repro/spill_frame_499_differential.py index 3234795e..d79fd5ab 100644 --- a/scripts/repro/spill_frame_499_differential.py +++ b/scripts/repro/spill_frame_499_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#499 — EXECUTION-validate optimized-path spill-frame teardown on return. The optimized (non-`--relocatable`) ARM path allocates a spill frame diff --git a/scripts/repro/stack_args_503_differential.py b/scripts/repro/stack_args_503_differential.py index 23aa2ecb..4b707d25 100644 --- a/scripts/repro/stack_args_503_differential.py +++ b/scripts/repro/stack_args_503_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#503 (epic #242) — EXECUTION-validate the AAPCS stack-argument path for functions with >8 scalar i32 params/args. diff --git a/scripts/repro/stack_layout_687_differential.py b/scripts/repro/stack_layout_687_differential.py index fe2d9766..782f4aaa 100644 --- a/scripts/repro/stack_layout_687_differential.py +++ b/scripts/repro/stack_layout_687_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#687 — `--stack-layout=low`: stack at the SRAM bottom, overflow BusFaults. Today's self-contained Cortex-M image puts the initial SP at the TOP of SRAM, diff --git a/scripts/repro/static_above_sp_739_differential.py b/scripts/repro/static_above_sp_739_differential.py index 17197aba..73607096 100644 --- a/scripts/repro/static_above_sp_739_differential.py +++ b/scripts/repro/static_above_sp_739_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#739 execution differential: static ABOVE sp_init under --shadow-stack-size. A meld `--memory shared` fused node places component statics ABOVE the shared diff --git a/scripts/repro/trunc_sat_782_differential.py b/scripts/repro/trunc_sat_782_differential.py index a9ef7003..50c54e0b 100644 --- a/scripts/repro/trunc_sat_782_differential.py +++ b/scripts/repro/trunc_sat_782_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#782a — the trunc_sat (nontrapping saturating float->int) boundary EXECUTION differential. diff --git a/scripts/repro/unreachable_665_differential.py b/scripts/repro/unreachable_665_differential.py index fc515b75..f6729036 100644 --- a/scripts/repro/unreachable_665_differential.py +++ b/scripts/repro/unreachable_665_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#665 — `unreachable` must TRAP (WASM Core §4.4.5), on BOTH ISAs. synth compiled wasm `unreachable` to a NO-OP: the decoder dropped it as diff --git a/scripts/repro/vcr_dec_001_graph_alloc_differential.py b/scripts/repro/vcr_dec_001_graph_alloc_differential.py index b8837178..45a5babe 100644 --- a/scripts/repro/vcr_dec_001_graph_alloc_differential.py +++ b/scripts/repro/vcr_dec_001_graph_alloc_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-DEC-001 graph-colouring allocator SPIKE differential (SYNTH_GRAPH_ALLOC). The North Star's first foothold: a whole-function Chaitin/Briggs graph-colouring diff --git a/scripts/repro/vcr_dec_001_join_alloc_execution_differential.py b/scripts/repro/vcr_dec_001_join_alloc_execution_differential.py index 8bc1ab6a..80aef49e 100644 --- a/scripts/repro/vcr_dec_001_join_alloc_execution_differential.py +++ b/scripts/repro/vcr_dec_001_join_alloc_execution_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-DEC-001 increments 2+3 — EXECUTION differential for the join- and call-aware graph-colouring allocator (`SYNTH_GRAPH_ALLOC=1`, epic #242). diff --git a/scripts/repro/vcr_ra_003_phase2_join_call.py b/scripts/repro/vcr_ra_003_phase2_join_call.py index 1956073d..b0bfbc54 100644 --- a/scripts/repro/vcr_ra_003_phase2_join_call.py +++ b/scripts/repro/vcr_ra_003_phase2_join_call.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA-003 phase 2 (#242) repro — across-CALL + across-JOIN allocation validation. The v0.48 validator (`validate_final_allocation`) was BOUNDED to straight-line diff --git a/scripts/repro/vcr_ra_003_rv32_alloc_validator.py b/scripts/repro/vcr_ra_003_rv32_alloc_validator.py index c7a2bf10..bbe2c7ba 100644 --- a/scripts/repro/vcr_ra_003_rv32_alloc_validator.py +++ b/scripts/repro/vcr_ra_003_rv32_alloc_validator.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA-003 for RISC-V (#815, epic #242) — RV32 register-allocation validator. The RV32 analogue of the ARM `validate_final_allocation` gate. The RV32 checker diff --git a/scripts/repro/vfp_spill_881_differential.py b/scripts/repro/vfp_spill_881_differential.py index f9988c7a..53bd60ad 100644 --- a/scripts/repro/vfp_spill_881_differential.py +++ b/scripts/repro/vfp_spill_881_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#881 (GI-FPU-002 + RA tail / VCR-RA-004) — EXECUTION-validate VFP register-file spilling on cortex-m7dp under falcon's exact flags (`-t cortex-m7dp --relocatable`). diff --git a/scripts/repro/wide_static_746_differential.py b/scripts/repro/wide_static_746_differential.py index 0a84534d..0ab0d8f2 100644 --- a/scripts/repro/wide_static_746_differential.py +++ b/scripts/repro/wide_static_746_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#746 execution differential: i64/wide static ABOVE sp_init under --shadow-stack-size (the #739 residual — sub-word arms were fixed in #744). diff --git a/scripts/repro/wide_static_copy_757_differential.py b/scripts/repro/wide_static_copy_757_differential.py index 677596a1..f14b27dd 100644 --- a/scripts/repro/wide_static_copy_757_differential.py +++ b/scripts/repro/wide_static_copy_757_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#757 investigation harness — the multi-chunk static-copy differential. #757 reported a SILENT MISCOMPILE regression from the #746 fix: a chunked copy From 2c01e1cfa72cd5714c2f97fe9c5dc65ca9f1be51 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:38:55 +0200 Subject: [PATCH 2/9] =?UTF-8?q?feat(#890):=20classify=20all=20152=20repro?= =?UTF-8?q?=20scripts=20=E2=80=94=207=20manual=20with=20real=20reasons=20(?= =?UTF-8?q?step=202/5)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Read and classified the 70 scripts no workflow referenced. 63 of them run green against a freshly built synth right now (verified locally, one at a time) and are wired in the next step; 7 are genuinely manual and say WHY, in a closed category vocabulary (measurement / scratch / external-input) rather than free text. Three enabling fixes fall out of the audit: * base_cse / leaf_dead_frame / load_store_big_offset_382 / uxth_fold hardcoded ./target/{debug,release}/synth; they now honour $SYNTH (same literal default) so CI can point them at its own build. * sret_decide_differential printed "MISMATCH <-- BUG" and still exited 0 — wiring it as-is would have added a gate that CANNOT fail. The verdict is now the exit status (proved: mutating the -35 expectation to -34 gives rc=1). The gate is deliberately still red: 63 files declare `wired` while no workflow references them. That is the exact defect being fixed, and it is now MACHINE VISIBLE instead of requiring a 150-file read. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- scripts/repro/a32_i64_615_differential.py | 1 + scripts/repro/add_imm_large_differential.py | 1 + scripts/repro/base_cse_differential.py | 6 +++++- scripts/repro/br_table_value_509_differential.py | 1 + scripts/repro/bulk_memory_374_differential.py | 1 + scripts/repro/call_5args_differential.py | 1 + scripts/repro/call_6_7args_differential.py | 1 + scripts/repro/call_indirect_594_differential.py | 1 + scripts/repro/call_indirect_597_differential.py | 1 + scripts/repro/cf_shapes_500_differential.py | 1 + scripts/repro/const_body_791_differential.py | 1 + scripts/repro/control_step_riscv_differential.py | 1 + scripts/repro/controller_step_riscv_differential.py | 1 + scripts/repro/div_const_differential.py | 1 + scripts/repro/dyn_table_359_differential.py | 1 + scripts/repro/fact_spec_rem_494_differential.py | 1 + scripts/repro/filter_axis_riscv_differential.py | 1 + scripts/repro/gust_spill_fwd_390_differential.py | 1 + scripts/repro/high_pressure_i32_differential.py | 1 + scripts/repro/high_pressure_i64_differential.py | 1 + scripts/repro/i64_divs_317_riscv_differential.py | 1 + scripts/repro/i64_divs_overflow_633_differential.py | 1 + scripts/repro/i64_globals_643_differential.py | 1 + scripts/repro/i64_large_offset_382_differential.py | 1 + scripts/repro/i64_load_store_372_differential.py | 1 + scripts/repro/i64_pair_exhaust_587_differential.py | 1 + scripts/repro/i64_param_518_riscv_loudskip.py | 1 + scripts/repro/i64_popcnt_632_differential.py | 1 + scripts/repro/i64_shr_599_differential.py | 1 + scripts/repro/if_else_result_343_riscv_differential.py | 1 + scripts/repro/leaf_dead_frame_differential.py | 6 +++++- scripts/repro/load_store_big_offset_382_differential.py | 6 +++++- scripts/repro/local_promote_i32_differential.py | 1 + scripts/repro/local_promotion_headroom.py | 1 + scripts/repro/loop_param_bound_663_differential.py | 1 + scripts/repro/mask_bounds_655_riscv_differential.py | 1 + scripts/repro/mem757_inlined_memmove_differential.py | 1 + scripts/repro/mem757_low_const_copy_differential.py | 1 + scripts/repro/mem757_memcopy_static_src_differential.py | 1 + scripts/repro/mem757_memmove_param_differential.py | 1 + scripts/repro/mem757_pressure_chunks_differential.py | 1 + scripts/repro/mem757_ptr_base_copy_differential.py | 1 + scripts/repro/mem_grow_539_differential.py | 1 + scripts/repro/multi_sp_707_differential.py | 1 + scripts/repro/mutex_pressure_differential.py | 1 + .../repro/native_pointer_shadow_stack_differential.py | 1 + scripts/repro/native_pointer_static_downshift_678.py | 1 + scripts/repro/postex_cycle_proxy.py | 1 + scripts/repro/postlink_359_oracle.py | 1 + .../read_before_write_local_zeroinit_differential.py | 1 + scripts/repro/run204_unicorn.py | 1 + scripts/repro/rv32_cmp_select_472_riscv_differential.py | 1 + .../repro/rv32_local_promotion_472_riscv_differential.py | 1 + scripts/repro/signed_div_const_riscv_differential.py | 1 + scripts/repro/size_attribution_390.py | 1 + scripts/repro/spill_baseline_measure.sh | 1 + scripts/repro/spill_on_exhaust_242_differential.py | 1 + scripts/repro/spill_rung_581_differential.py | 1 + scripts/repro/sret_decide_differential.py | 9 ++++++++- scripts/repro/u64_unpack_differential.py | 1 + scripts/repro/u64_unpack_if_differential.py | 1 + scripts/repro/u64_unpack_riscv_differential.py | 1 + scripts/repro/uxth_fold_differential.py | 6 +++++- scripts/repro/vcr_dec_001_join_alloc_measure.py | 1 + scripts/repro/volatile_segment_543_differential.py | 1 + scripts/repro/wake_path_differential.py | 1 + scripts/repro/wcet_phase2_778_unicorn_soundness.py | 1 + scripts/repro/wcet_phase3_778_compose_soundness.py | 1 + scripts/repro/wcet_phase4_49_recursion_soundness.py | 1 + scripts/repro/wcet_phase5_778_masked_loop_soundness.py | 1 + 70 files changed, 93 insertions(+), 5 deletions(-) diff --git a/scripts/repro/a32_i64_615_differential.py b/scripts/repro/a32_i64_615_differential.py index 99c094dd..9e0b982c 100644 --- a/scripts/repro/a32_i64_615_differential.py +++ b/scripts/repro/a32_i64_615_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired # #615: A32/ARM-mode encoder silently NOP'd every i64 op (--target cortex-r5) # — mul/shift/rotate/compare/eqz/clz/ctz/popcnt/div/rem/const/extend/wrap all # encoded as 0xE1A00000, so the operation vanished and functions returned diff --git a/scripts/repro/add_imm_large_differential.py b/scripts/repro/add_imm_large_differential.py index 4d403d1b..6c1dc183 100644 --- a/scripts/repro/add_imm_large_differential.py +++ b/scripts/repro/add_imm_large_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#350 — out-of-range `ADD #imm` lowering (MOVW/MOVT + ADD instead of erroring). A static store with `offset=70000` (> 0xFFF) forces the indexed-address path diff --git a/scripts/repro/base_cse_differential.py b/scripts/repro/base_cse_differential.py index b830f896..52f2d3c8 100644 --- a/scripts/repro/base_cse_differential.py +++ b/scripts/repro/base_cse_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA lever 3 / VCR-ORACLE-001 (#468, #242) — EXECUTION-validate base-CSE. base-CSE (DEFAULT-ON since the #468 lever flip; opt-out SYNTH_BASE_CSE=0) @@ -26,6 +27,7 @@ python scripts/repro/base_cse_differential.py Exits nonzero on any mismatch or vacuity failure. """ +import os import subprocess import sys @@ -34,7 +36,9 @@ from unicorn import UC_ARCH_ARM, UC_MODE_THUMB, Uc, UcError from unicorn.arm_const import UC_ARM_REG_LR, UC_ARM_REG_R0, UC_ARM_REG_SP -SYNTH = "./target/release/synth" +# CI wires this via the SYNTH env var (#890); the literal stays the +# local-dev default. +SYNTH = os.environ.get("SYNTH", "./target/release/synth") # The optimized path materializes this absolute linear-memory base. LINMEM = 0x20000100 CODE, STK, RET = 0x200000, 0x90000, 0x300000 diff --git a/scripts/repro/br_table_value_509_differential.py b/scripts/repro/br_table_value_509_differential.py index 8c7710b7..6592eabf 100644 --- a/scripts/repro/br_table_value_509_differential.py +++ b/scripts/repro/br_table_value_509_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#509 (epic #242) — CHARACTERIZE the value-returning-branch miscompile. The oracle-first artifact for #509: the DIRECT selector (so the SHIPPED diff --git a/scripts/repro/bulk_memory_374_differential.py b/scripts/repro/bulk_memory_374_differential.py index f870555d..a4dad906 100644 --- a/scripts/repro/bulk_memory_374_differential.py +++ b/scripts/repro/bulk_memory_374_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#374 — memory.copy / memory.fill (bulk-memory) numeric differential. synth had no bulk-memory lowering: `memory.copy`/`memory.fill` fell through the diff --git a/scripts/repro/call_5args_differential.py b/scripts/repro/call_5args_differential.py index 804a66f1..140cfe6a 100644 --- a/scripts/repro/call_5args_differential.py +++ b/scripts/repro/call_5args_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#359 differential: a 5-argument call must pass ALL five args (caller/callee agree). The callee packs each arg into a distinct nibble (a | b<<4 | c<<8 | d<<12 | e<<16), diff --git a/scripts/repro/call_6_7args_differential.py b/scripts/repro/call_6_7args_differential.py index df496313..df24ddd7 100644 --- a/scripts/repro/call_6_7args_differential.py +++ b/scripts/repro/call_6_7args_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired import struct, sys from elftools.elf.elffile import ELFFile from unicorn import Uc, UC_ARCH_ARM, UC_MODE_THUMB diff --git a/scripts/repro/call_indirect_594_differential.py b/scripts/repro/call_indirect_594_differential.py index ec31aed8..f460dc05 100644 --- a/scripts/repro/call_indirect_594_differential.py +++ b/scripts/repro/call_indirect_594_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired # #594: call_indirect on the A32 path (--target cortex-r5) compiled to a NOP — # no call, wrong result (leftover table index instead of the callee's return). # diff --git a/scripts/repro/call_indirect_597_differential.py b/scripts/repro/call_indirect_597_differential.py index 1fd699e9..effcff13 100644 --- a/scripts/repro/call_indirect_597_differential.py +++ b/scripts/repro/call_indirect_597_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired # #597: the Thumb-2 CallIndirect expansion put its `LSL #2` shift amount in # the mov.w TYPE field (bits 5:4 → ASR #32) instead of imm2 (bits 7:6), so the # table index was destroyed and EVERY call_indirect dispatched entry 0. A probe diff --git a/scripts/repro/cf_shapes_500_differential.py b/scripts/repro/cf_shapes_500_differential.py index 02368ee0..bda394ea 100644 --- a/scripts/repro/cf_shapes_500_differential.py +++ b/scripts/repro/cf_shapes_500_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#500 (epic #242) — EXECUTION-validate optimized-path forward-branch shapes. #483 fixed the single `block`+`br_if` forward-exit; #500 shows the class is diff --git a/scripts/repro/const_body_791_differential.py b/scripts/repro/const_body_791_differential.py index 9c074ae5..43041d6d 100644 --- a/scripts/repro/const_body_791_differential.py +++ b/scripts/repro/const_body_791_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#791 — EXECUTION-validate const-only-body returns on the optimized path. On the OPTIMIZED (default self-contained) ARM path, a function whose result is diff --git a/scripts/repro/control_step_riscv_differential.py b/scripts/repro/control_step_riscv_differential.py index 0ef8711e..dd0fbb25 100644 --- a/scripts/repro/control_step_riscv_differential.py +++ b/scripts/repro/control_step_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#223 / #798 — control_step on RISC-V: correctness + ABI + shipped-data differential. After #218 (reachable) + #220 (callee-saved ABI) + #223 (Select, non-param diff --git a/scripts/repro/controller_step_riscv_differential.py b/scripts/repro/controller_step_riscv_differential.py index bef78490..6dc7bd90 100644 --- a/scripts/repro/controller_step_riscv_differential.py +++ b/scripts/repro/controller_step_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#226 — controller_step on RISC-V: the regalloc live-range clobber. In v0.11.23 the RV32 temp allocator was round-robin and blind to the operand diff --git a/scripts/repro/div_const_differential.py b/scripts/repro/div_const_differential.py index 57b9c14c..3b053bda 100644 --- a/scripts/repro/div_const_differential.py +++ b/scripts/repro/div_const_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#209 Opt 1 — constant-divisor strength-reduction differential oracle. wasmtime runs div_const.wat as ground truth; unicorn runs synth's ARM (the diff --git a/scripts/repro/dyn_table_359_differential.py b/scripts/repro/dyn_table_359_differential.py index 8cf9c4bb..daed6ba9 100644 --- a/scripts/repro/dyn_table_359_differential.py +++ b/scripts/repro/dyn_table_359_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired import struct,sys from elftools.elf.elffile import ELFFile from unicorn import Uc,UC_ARCH_ARM,UC_MODE_THUMB diff --git a/scripts/repro/fact_spec_rem_494_differential.py b/scripts/repro/fact_spec_rem_494_differential.py index b3f55456..410ce3ab 100644 --- a/scripts/repro/fact_spec_rem_494_differential.py +++ b/scripts/repro/fact_spec_rem_494_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-PERF-002 Phase 3+ (#494) — constant-divisor rem_u IDENTITY differential. Builds the `gust_scale` fixture (`x rem_u 1000`, a LITERAL divisor) WITH a diff --git a/scripts/repro/filter_axis_riscv_differential.py b/scripts/repro/filter_axis_riscv_differential.py index f0d69767..9a81acba 100644 --- a/scripts/repro/filter_axis_riscv_differential.py +++ b/scripts/repro/filter_axis_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#220 — RISC-V callee-saved register preservation differential. gale's first on-target RISC-V finding: the backend used callee-saved s-registers diff --git a/scripts/repro/gust_spill_fwd_390_differential.py b/scripts/repro/gust_spill_fwd_390_differential.py index 026edbc6..b422c134 100644 --- a/scripts/repro/gust_spill_fwd_390_differential.py +++ b/scripts/repro/gust_spill_fwd_390_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#390 (VCR-RA) — EXECUTION-validate conditional-branch-transparent stack-reload forwarding on the gust hot path, and own the SYNTH_NO_STACK_FWD flip-engagement check. diff --git a/scripts/repro/high_pressure_i32_differential.py b/scripts/repro/high_pressure_i32_differential.py index b6db04b0..869c2cd5 100644 --- a/scripts/repro/high_pressure_i32_differential.py +++ b/scripts/repro/high_pressure_i32_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA-001 step 3b-lite (#242) — spill-on-exhaustion differential oracle. `high_pressure_i32.wat` keeps 10 i32 constants simultaneously live (plus both diff --git a/scripts/repro/high_pressure_i64_differential.py b/scripts/repro/high_pressure_i64_differential.py index b30f7a9a..d005b1d7 100644 --- a/scripts/repro/high_pressure_i64_differential.py +++ b/scripts/repro/high_pressure_i64_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA-001 acceptance increment (#242) — i64 pair-spill differential oracle. `high_pressure_i64.wat` keeps 4 i64 constants simultaneously live (4 register diff --git a/scripts/repro/i64_divs_317_riscv_differential.py b/scripts/repro/i64_divs_317_riscv_differential.py index d3d9efc7..7f0e73b2 100644 --- a/scripts/repro/i64_divs_317_riscv_differential.py +++ b/scripts/repro/i64_divs_317_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#317 — RV32 i64.div_s / i64.rem_s sign clobbered by the udiv core. The signed 64-bit div/rem lowering allocated its `nsign`/`dsign` sign masks diff --git a/scripts/repro/i64_divs_overflow_633_differential.py b/scripts/repro/i64_divs_overflow_633_differential.py index 5cf3c1c5..788d25d3 100644 --- a/scripts/repro/i64_divs_overflow_633_differential.py +++ b/scripts/repro/i64_divs_overflow_633_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired # #633: i64.div_s(INT64_MIN, -1) must trap (WASM Core 4.3.2 idiv_s — the # quotient +2^63 is unrepresentable). The Thumb-2 I64DivS expansion emitted # only the divide-by-zero guard: it negated the dividend (INT64_MIN wraps to diff --git a/scripts/repro/i64_globals_643_differential.py b/scripts/repro/i64_globals_643_differential.py index 30223b8d..63b5b4cc 100644 --- a/scripts/repro/i64_globals_643_differential.py +++ b/scripts/repro/i64_globals_643_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#643 — i64 global.set/global.get pair correctness on BOTH ARM selectors. Differential oracle for issue #643: on Thumb-2, an i64 global was stored/loaded diff --git a/scripts/repro/i64_large_offset_382_differential.py b/scripts/repro/i64_large_offset_382_differential.py index 4c825ee6..161a5ba5 100755 --- a/scripts/repro/i64_large_offset_382_differential.py +++ b/scripts/repro/i64_large_offset_382_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#382 (direct/relocatable path) — i64 large static load/store offset oracle. The direct selector (`--relocatable`, R11/fp = linear-memory base) lowers a diff --git a/scripts/repro/i64_load_store_372_differential.py b/scripts/repro/i64_load_store_372_differential.py index 73f86620..11cca831 100644 --- a/scripts/repro/i64_load_store_372_differential.py +++ b/scripts/repro/i64_load_store_372_differential.py @@ -1,3 +1,4 @@ +# ci-status: manual (scratch) — a 25-line print-only probe (does ld64 read mem[addr] or mem[0]?), hardcoded to /tmp/i64/i64_d.elf, no assertion and no exit code; superseded as a GATE by i64_large_offset_382 + load_store_big_offset_382, both wired. Kept for the #372 provenance trail. # Does ld64(addr) read mem[addr] (correct) or mem[0] (address dropped)? import subprocess from unicorn import Uc, UC_ARCH_ARM, UC_MODE_THUMB diff --git a/scripts/repro/i64_pair_exhaust_587_differential.py b/scripts/repro/i64_pair_exhaust_587_differential.py index 5ede7da1..c6bebd27 100644 --- a/scripts/repro/i64_pair_exhaust_587_differential.py +++ b/scripts/repro/i64_pair_exhaust_587_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#587 (VCR-RA, #242) — i64 pair-exhaustion spill differential oracle. `i64_pair_exhaust_587.wat` keeps five i64 values simultaneously live, one more diff --git a/scripts/repro/i64_param_518_riscv_loudskip.py b/scripts/repro/i64_param_518_riscv_loudskip.py index 743a2829..16db6905 100644 --- a/scripts/repro/i64_param_518_riscv_loudskip.py +++ b/scripts/repro/i64_param_518_riscv_loudskip.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#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 diff --git a/scripts/repro/i64_popcnt_632_differential.py b/scripts/repro/i64_popcnt_632_differential.py index a841e4bd..703e017b 100644 --- a/scripts/repro/i64_popcnt_632_differential.py +++ b/scripts/repro/i64_popcnt_632_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired # #632: i64.popcnt result clobbered by the expansion's own scratch-restore pop. # # The Thumb-2 I64Popcnt expansion saves scratch with `PUSH {R3,R4,R5}`, diff --git a/scripts/repro/i64_shr_599_differential.py b/scripts/repro/i64_shr_599_differential.py index 60b039cf..a459f6d7 100644 --- a/scripts/repro/i64_shr_599_differential.py +++ b/scripts/repro/i64_shr_599_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired # #599: i64.shr_u / i64.shr_s register-pair right shift miscompiled on the # single-function CLI path (`-n `): the path built its CompileConfig with # `..default()` and never plumbed the module's declared param widths diff --git a/scripts/repro/if_else_result_343_riscv_differential.py b/scripts/repro/if_else_result_343_riscv_differential.py index ab9a099d..2e0cb936 100755 --- a/scripts/repro/if_else_result_343_riscv_differential.py +++ b/scripts/repro/if_else_result_343_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#343 — RV32 `if (result i32)` result-register reconciliation. The RV32 selector lowered a value-returning `if/else` without merging the two diff --git a/scripts/repro/leaf_dead_frame_differential.py b/scripts/repro/leaf_dead_frame_differential.py index 77804a5f..27ac04db 100644 --- a/scripts/repro/leaf_dead_frame_differential.py +++ b/scripts/repro/leaf_dead_frame_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA-002 / VCR-ORACLE-001 (#390, #242) — EXECUTION-validate dead-frame elision. `compute_local_layout` reserves a frame slot (`sub sp,#N` / `add sp,#N`) for every @@ -25,6 +26,7 @@ Exits nonzero on any mismatch or vacuity failure. """ +import os import subprocess import sys @@ -39,7 +41,9 @@ ) WASM = "scripts/repro/leaf_caller_saved.wat" -SYNTH = "./target/debug/synth" +# CI wires this via the SYNTH env var (#890); the literal stays the +# local-dev default. +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") ELF_OFF, ELF_ON = "/tmp/leaf_frame_off.elf", "/tmp/leaf_frame_on.elf" CODE, LIN, STK, RET = 0x200000, 0x40000, 0x90000, 0x300000 diff --git a/scripts/repro/load_store_big_offset_382_differential.py b/scripts/repro/load_store_big_offset_382_differential.py index 1f40f883..24d0da6c 100644 --- a/scripts/repro/load_store_big_offset_382_differential.py +++ b/scripts/repro/load_store_big_offset_382_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#382 — large static load/store offset (> imm12) differential oracle. The optimized (non-relocatable) ARM path materializes the linear-memory base as @@ -21,6 +22,7 @@ Exits nonzero on mismatch so it can gate a release. """ +import os import subprocess import sys @@ -37,7 +39,9 @@ WAT = "scripts/repro/load_store_big_offset_382.wat" WASM = "/tmp/ls382.wasm" ELF = "/tmp/ls382_diff.elf" -SYNTH = "./target/debug/synth" +# CI wires this via the SYNTH env var (#890); the literal stays the +# local-dev default. +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") # Absolute linear-memory base the optimized path materializes (optimizer_bridge). LIN_BASE = 0x20000100 diff --git a/scripts/repro/local_promote_i32_differential.py b/scripts/repro/local_promote_i32_differential.py index c3177f29..5ce03645 100644 --- a/scripts/repro/local_promote_i32_differential.py +++ b/scripts/repro/local_promote_i32_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA local-promotion validation oracle (#390, epic #242). `local_promote_i32.wat` is built to defeat the #193 non-vacuity trap: 7 diff --git a/scripts/repro/local_promotion_headroom.py b/scripts/repro/local_promotion_headroom.py index a7155d66..12c09d2d 100755 --- a/scripts/repro/local_promotion_headroom.py +++ b/scripts/repro/local_promotion_headroom.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: manual (measurement) — a #390 scoping SPIKE that prints a per-function sp-traffic/pressure table to cost the local-promotion lever. It has no expected values and no verdict, so there is nothing for CI to fail on; the lever it sized is gated by local_promote_i32_differential.py (wired). """VCR-RA local-promotion scoping spike (#390, #209, epic #242). The structural gap to native parity is that synth's instruction selector lowers diff --git a/scripts/repro/loop_param_bound_663_differential.py b/scripts/repro/loop_param_bound_663_differential.py index 45c68cf0..91b87ede 100644 --- a/scripts/repro/loop_param_bound_663_differential.py +++ b/scripts/repro/loop_param_bound_663_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#663 — thumb-2 parameter-bounded loop: live param bound clobbered by the induction increment (loop exits after 1 iteration). diff --git a/scripts/repro/mask_bounds_655_riscv_differential.py b/scripts/repro/mask_bounds_655_riscv_differential.py index 3f625a6c..3f71d9a2 100644 --- a/scripts/repro/mask_bounds_655_riscv_differential.py +++ b/scripts/repro/mask_bounds_655_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#655 — RV32 mask/software bounds: EXECUTION-validate the effective-address fix. The #651 class, RISC-V twin of ARM PR #654: `emit_bounds_check`'s Mask arm diff --git a/scripts/repro/mem757_inlined_memmove_differential.py b/scripts/repro/mem757_inlined_memmove_differential.py index 4e5956c1..910422c2 100644 --- a/scripts/repro/mem757_inlined_memmove_differential.py +++ b/scripts/repro/mem757_inlined_memmove_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#757 RED-FIRST differential — memmove (`memory.copy`) from a STATIC pointer. gale's real mechanism: a RawVec-grow `call` followed by a `memory.copy` whose diff --git a/scripts/repro/mem757_low_const_copy_differential.py b/scripts/repro/mem757_low_const_copy_differential.py index c72f9274..1bfe5772 100644 --- a/scripts/repro/mem757_low_const_copy_differential.py +++ b/scripts/repro/mem757_low_const_copy_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#757 RED-FIRST differential — the low-const-below-string chunked static copy. The six 0.43.0 reconstructions all found the wide-head source addend CORRECT, diff --git a/scripts/repro/mem757_memcopy_static_src_differential.py b/scripts/repro/mem757_memcopy_static_src_differential.py index 48dd4987..415c12df 100644 --- a/scripts/repro/mem757_memcopy_static_src_differential.py +++ b/scripts/repro/mem757_memcopy_static_src_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#757 RED-FIRST differential — memmove (`memory.copy`) from a STATIC pointer. gale's real mechanism: a RawVec-grow `call` followed by a `memory.copy` whose diff --git a/scripts/repro/mem757_memmove_param_differential.py b/scripts/repro/mem757_memmove_param_differential.py index 92689439..9282a0f5 100644 --- a/scripts/repro/mem757_memmove_param_differential.py +++ b/scripts/repro/mem757_memmove_param_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#757 RED-FIRST differential — memmove (`memory.copy`) from a STATIC pointer. gale's real mechanism: a RawVec-grow `call` followed by a `memory.copy` whose diff --git a/scripts/repro/mem757_pressure_chunks_differential.py b/scripts/repro/mem757_pressure_chunks_differential.py index d2f60873..a704c4eb 100644 --- a/scripts/repro/mem757_pressure_chunks_differential.py +++ b/scripts/repro/mem757_pressure_chunks_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#757 RED-FIRST differential — memmove (`memory.copy`) from a STATIC pointer. gale's real mechanism: a RawVec-grow `call` followed by a `memory.copy` whose diff --git a/scripts/repro/mem757_ptr_base_copy_differential.py b/scripts/repro/mem757_ptr_base_copy_differential.py index 1d7915aa..34d8cc8a 100644 --- a/scripts/repro/mem757_ptr_base_copy_differential.py +++ b/scripts/repro/mem757_ptr_base_copy_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#757 RED-FIRST differential — memmove (`memory.copy`) from a STATIC pointer. gale's real mechanism: a RawVec-grow `call` followed by a `memory.copy` whose diff --git a/scripts/repro/mem_grow_539_differential.py b/scripts/repro/mem_grow_539_differential.py index f3053317..4c735b2b 100644 --- a/scripts/repro/mem_grow_539_differential.py +++ b/scripts/repro/mem_grow_539_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#539 — EXECUTION-validate the memory.grow(0) fix on both ARM lowering paths. Before the fix, every `memory.grow` lowered to a constant `-1`, so the legal diff --git a/scripts/repro/multi_sp_707_differential.py b/scripts/repro/multi_sp_707_differential.py index 7f925911..cef9827b 100644 --- a/scripts/repro/multi_sp_707_differential.py +++ b/scripts/repro/multi_sp_707_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#707 multi-provider shared-memory fused node: N `__stack_pointer` globals all init == sp_init, co-rebased by `--shadow-stack-size`. diff --git a/scripts/repro/mutex_pressure_differential.py b/scripts/repro/mutex_pressure_differential.py index 907794df..64bc9588 100644 --- a/scripts/repro/mutex_pressure_differential.py +++ b/scripts/repro/mutex_pressure_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#326 — arg-move-cycle-under-pressure differential oracle. `mutex_pressure.wat` reproduces the shape that stopped gale's dissolved diff --git a/scripts/repro/native_pointer_shadow_stack_differential.py b/scripts/repro/native_pointer_shadow_stack_differential.py index 2932e760..568f9b08 100644 --- a/scripts/repro/native_pointer_shadow_stack_differential.py +++ b/scripts/repro/native_pointer_shadow_stack_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#237 shadow-stack differential: the gmutex frame shape under --native-pointer-abi. Compile: diff --git a/scripts/repro/native_pointer_static_downshift_678.py b/scripts/repro/native_pointer_static_downshift_678.py index 4b10f786..a6df148e 100644 --- a/scripts/repro/native_pointer_static_downshift_678.py +++ b/scripts/repro/native_pointer_static_downshift_678.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-MEM-001 layer-2 (#678) execution differential: inline linmem statics down-shifted into `.data`/`.bss` under `--native-pointer-abi --shadow-stack-size`. diff --git a/scripts/repro/postex_cycle_proxy.py b/scripts/repro/postex_cycle_proxy.py index 9c44b1fa..68d25bb0 100644 --- a/scripts/repro/postex_cycle_proxy.py +++ b/scripts/repro/postex_cycle_proxy.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-VER-001 post-exhaustion cycle proxy (#242) — the PR #659 gate table, reproducible. diff --git a/scripts/repro/postlink_359_oracle.py b/scripts/repro/postlink_359_oracle.py index 845e0146..64b0b563 100755 --- a/scripts/repro/postlink_359_oracle.py +++ b/scripts/repro/postlink_359_oracle.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """ #359 POST-LINK ORACLE — the structural fix to the #368 mistake (a unicorn-on-.o oracle could not see the #354 link-time retargeting, so #368 passed locally and diff --git a/scripts/repro/read_before_write_local_zeroinit_differential.py b/scripts/repro/read_before_write_local_zeroinit_differential.py index 9f1d17b7..ebade40b 100644 --- a/scripts/repro/read_before_write_local_zeroinit_differential.py +++ b/scripts/repro/read_before_write_local_zeroinit_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#457 read-before-write local zero-init oracle (ARM direct + optimized, RV32). `read_before_write_local_zeroinit.wat` declares ONE i32 param and ONE never- diff --git a/scripts/repro/run204_unicorn.py b/scripts/repro/run204_unicorn.py index fa634b47..66d62cab 100644 --- a/scripts/repro/run204_unicorn.py +++ b/scripts/repro/run204_unicorn.py @@ -1,3 +1,4 @@ +# ci-status: manual (scratch) — a #204 bring-up probe hardcoded to /tmp/gz.bin with hand-transcribed import-stub offsets from one historical `synth disasm` run; it prints stores and asserts nothing. Both inputs are stale by construction, so it can only be re-run by hand against a fresh disassembly. from unicorn import * from unicorn.arm_const import * code=open('/tmp/gz.bin','rb').read() diff --git a/scripts/repro/rv32_cmp_select_472_riscv_differential.py b/scripts/repro/rv32_cmp_select_472_riscv_differential.py index 5da721d6..4612a2fa 100755 --- a/scripts/repro/rv32_cmp_select_472_riscv_differential.py +++ b/scripts/repro/rv32_cmp_select_472_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#472 — RV32 cmp→select fusion (VCR-SEL-004 port) differential oracle. Ports the ARM cmp→select lever to RV32: an i32 comparison that DIRECTLY feeds diff --git a/scripts/repro/rv32_local_promotion_472_riscv_differential.py b/scripts/repro/rv32_local_promotion_472_riscv_differential.py index f26d3fce..b9ab74ea 100644 --- a/scripts/repro/rv32_local_promotion_472_riscv_differential.py +++ b/scripts/repro/rv32_local_promotion_472_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#472 — RV32 i32 local-promotion lever (VCR-RA) differential oracle. Ports the ARM local-promotion lever (#390/#457/#458) to RV32: non-parameter i32 diff --git a/scripts/repro/signed_div_const_riscv_differential.py b/scripts/repro/signed_div_const_riscv_differential.py index 310a53b7..45d81599 100644 --- a/scripts/repro/signed_div_const_riscv_differential.py +++ b/scripts/repro/signed_div_const_riscv_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#232 — RV32 signed-division-by-constant overflow-guard clobber. v0.11.26's lowest-free allocator (#231) materialized the `INT_MIN`/`-1` overflow diff --git a/scripts/repro/size_attribution_390.py b/scripts/repro/size_attribution_390.py index a836f852..3c246406 100755 --- a/scripts/repro/size_attribution_390.py +++ b/scripts/repro/size_attribution_390.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: manual (measurement) — prints the #390 .text size-attribution table (named causal buckets) for the beat-LLVM lanes; it is a REPORT with no pass/fail. The numbers it produces are pinned by crates/synth-cli/tests/size_attribution_390.rs, which cargo test runs — that is the gate. """size_attribution_390.py — quantify and attribute synth's .text size on the gust hot path (issue #390, rivet VCR-PERF-001). diff --git a/scripts/repro/spill_baseline_measure.sh b/scripts/repro/spill_baseline_measure.sh index 8a4b5b16..f0a27a8f 100755 --- a/scripts/repro/spill_baseline_measure.sh +++ b/scripts/repro/spill_baseline_measure.sh @@ -1,4 +1,5 @@ #!/usr/bin/env bash +# ci-status: manual (measurement) — the VCR-PERF-001 Pass-1 spill-waste BASELINE census (#390): it compiles the frozen fixtures and reports spill-slot counts to size the allocator work. Changes zero codegen bytes and has no expected values, so there is no verdict to gate on. # VCR-PERF-001 Pass-1 / VCR-RA-010 — in-tree spill-elimination baseline (#390, #242). # # gale #390 measured the headline size gap on the gust scheduler hot path diff --git a/scripts/repro/spill_on_exhaust_242_differential.py b/scripts/repro/spill_on_exhaust_242_differential.py index af250c7c..5b091f09 100644 --- a/scripts/repro/spill_on_exhaust_242_differential.py +++ b/scripts/repro/spill_on_exhaust_242_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA-001 (#242) — allocation-time spill-on-exhaustion differential oracle. `spill_on_exhaust_242.wat` keeps 10 param-derived i32 values simultaneously diff --git a/scripts/repro/spill_rung_581_differential.py b/scripts/repro/spill_rung_581_differential.py index b70a2052..69e4aebf 100644 --- a/scripts/repro/spill_rung_581_differential.py +++ b/scripts/repro/spill_rung_581_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#581 — DIRECT-selector spill-rung differential: unicorn vs wasmtime. The direct selector's spill rung (the backend's exhaustion retry, diff --git a/scripts/repro/sret_decide_differential.py b/scripts/repro/sret_decide_differential.py index f8a8c0c0..382b31d2 100644 --- a/scripts/repro/sret_decide_differential.py +++ b/scripts/repro/sret_decide_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired import struct, sys from elftools.elf.elffile import ELFFile from unicorn import Uc, UC_ARCH_ARM, UC_MODE_THUMB @@ -27,5 +28,11 @@ def run(w,u,m): mu.reg_write(UC_ARM_REG_R11,DATA); mu.reg_write(UC_ARM_REG_SP,STK+0x80000); mu.reg_write(UC_ARM_REG_LR,RET|1) mu.emu_start((CODE+(syms["shim"]&~1))|1,RET,timeout=5_000_000,count=20000) return struct.unpack(">32), not the else-arm's register. check_call(3,4) must be 8. diff --git a/scripts/repro/u64_unpack_riscv_differential.py b/scripts/repro/u64_unpack_riscv_differential.py index 5a0b3fdf..234ea375 100644 --- a/scripts/repro/u64_unpack_riscv_differential.py +++ b/scripts/repro/u64_unpack_riscv_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired import sys import wasmtime from elftools.elf.elffile import ELFFile diff --git a/scripts/repro/uxth_fold_differential.py b/scripts/repro/uxth_fold_differential.py index b4f33de3..5e706f30 100644 --- a/scripts/repro/uxth_fold_differential.py +++ b/scripts/repro/uxth_fold_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """VCR-RA uxth/uxtb fold validation oracle (#428, epic #242). The fold rewrites `movw rM,#0xffff; and rD,rN,rM` -> `uxth rD,rN` (and the 0xff / @@ -15,6 +16,7 @@ /tmp/armv/bin/python scripts/repro/uxth_fold_differential.py """ +import os import re import subprocess import sys @@ -32,7 +34,9 @@ ) WAT = "scripts/repro/uxth_fold.wat" -SYNTH = "./target/debug/synth" +# CI wires this via the SYNTH env var (#890); the literal stays the +# local-dev default. +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") CODE, LIN, STK, RET = 0x200000, 0x40000, 0x180000, 0x300000 diff --git a/scripts/repro/vcr_dec_001_join_alloc_measure.py b/scripts/repro/vcr_dec_001_join_alloc_measure.py index 3c5589ff..5a776b7c 100644 --- a/scripts/repro/vcr_dec_001_join_alloc_measure.py +++ b/scripts/repro/vcr_dec_001_join_alloc_measure.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: manual (measurement) — the #242 join-allocator COMPARISON deliverable (bytes and --emit-wcet bounds, graph-alloc ON vs OFF) whose whole point is a number to judge a flip by; it deliberately has no verdict. The allocator's correctness is gated by the wired VCR-DEC-001 differential jobs. """VCR-DEC-001 increments 2+3 — MEASURE the join- and call-aware graph-colouring allocator against the shipping greedy/segment allocator (epic #242, the North Star). diff --git a/scripts/repro/volatile_segment_543_differential.py b/scripts/repro/volatile_segment_543_differential.py index 3b347963..988f7dbc 100644 --- a/scripts/repro/volatile_segment_543_differential.py +++ b/scripts/repro/volatile_segment_543_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#543 Phase 2 / VCR-DMA-001 — EXECUTION-validate the volatile DMA-window back-off. `--volatile-segment :` must change ACCESS PATTERNS, never RESULTS: diff --git a/scripts/repro/wake_path_differential.py b/scripts/repro/wake_path_differential.py index 9a05c127..3eee6e00 100644 --- a/scripts/repro/wake_path_differential.py +++ b/scripts/repro/wake_path_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: manual (external-input) — needs gale's merged.both.loom.wat, fetched at run time from a GitHub gist that is not in-tree and not vendored; the WAKE path it exercises cannot be reproduced from any in-repo fixture (that is why the harness exists — the debugger perturbs the give/take race on silicon). """ #204 WAKE-path differential harness (gale's binary semaphore). diff --git a/scripts/repro/wcet_phase2_778_unicorn_soundness.py b/scripts/repro/wcet_phase2_778_unicorn_soundness.py index 0c658f0b..2c4bbf0b 100644 --- a/scripts/repro/wcet_phase2_778_unicorn_soundness.py +++ b/scripts/repro/wcet_phase2_778_unicorn_soundness.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#778 phase 2 soundness cross-check: execute compiled loop fixtures under unicorn (Thumb-2), count machine instructions, and check: diff --git a/scripts/repro/wcet_phase3_778_compose_soundness.py b/scripts/repro/wcet_phase3_778_compose_soundness.py index 8f78d526..f9d62f3c 100755 --- a/scripts/repro/wcet_phase3_778_compose_soundness.py +++ b/scripts/repro/wcet_phase3_778_compose_soundness.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#778 phase 3 soundness cross-check: execute compiled DIRECT-CALL fixtures under unicorn (Thumb-2) and confirm the COMPOSED inter-procedural bound is a sound upper bound on the ACTUAL executed cost. diff --git a/scripts/repro/wcet_phase4_49_recursion_soundness.py b/scripts/repro/wcet_phase4_49_recursion_soundness.py index 4d6b02b0..0e30ab3a 100644 --- a/scripts/repro/wcet_phase4_49_recursion_soundness.py +++ b/scripts/repro/wcet_phase4_49_recursion_soundness.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#778 phase 4 (#49) recursion-bound soundness cross-check: execute a compiled BOUNDED self-recursion under unicorn (Thumb-2) and confirm the composed recursion bound is a sound upper bound on the ACTUAL total executed cost across diff --git a/scripts/repro/wcet_phase5_778_masked_loop_soundness.py b/scripts/repro/wcet_phase5_778_masked_loop_soundness.py index e4d22ac0..c9b1d57b 100755 --- a/scripts/repro/wcet_phase5_778_masked_loop_soundness.py +++ b/scripts/repro/wcet_phase5_778_masked_loop_soundness.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired """#778 phase 5 masked-ceiling loop-bound soundness cross-check: execute a compiled BOUNDED data-dependent loop under unicorn (Thumb-2) and confirm the derived masked-ceiling bound is a sound upper bound on the ACTUAL executed cost From d539737f6328723403c57b36f52a55c2be419d38 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:42:49 +0200 Subject: [PATCH 3/9] feat(#890): wire 63 forgotten oracles + CI-wire the gate itself (step 3/5) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Four new sweep jobs (selector / memory / rv32 / wcet) plus one step in the existing fact-spec job run the 63 differentials that were sitting in scripts/repro/ with nothing executing them. Every one was verified green locally against a freshly built synth before being wired — the compile line comes from each harness's own documented Run: block. Highlights of what was NOT being gated: the six mem757_* red-first reconstructions of gale's wrong-segment miscompile (#757); every RV32 oracle for a regression gale found on real silicon (#220/#226/#232/#317/#343); all four WCET soundness cross-checks — the only thing that EXECUTES the fixtures and checks bound_cycles >= executed_instructions, i.e. the evidence behind the "sound WCET bound" claim; and the #494 rem_u identity differential behind the beat-clang headline. The gate itself is wired IN THE SAME COMMIT, as a step in claim-check — an ALREADY-REQUIRED context on main. A brand-new job would not be required, so it could sit red for weeks without blocking anything: the exact failure mode. It uses `set -o pipefail` and re-reads its own JSON summary to assert a non-zero wired count over a non-empty script set, so a run that measured nothing fails instead of greening on exit 0. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 360 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 360 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f2e22d7b..af058887 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -179,6 +179,37 @@ jobs: # claims.yaml, so this step is what keeps those numbers honest. - name: Model-coverage artifact freshness + uncovered-complement report (867) run: python3 scripts/model_coverage_audit.py --check + # #890: the ORACLE-WIRING gate. scripts/repro/*.py are the execution + # oracles; 69 of 150 were referenced by no workflow at all and nothing + # distinguished "manual by design" from "forgotten". Every script now + # declares `# ci-status: wired|manual|unwired`, a `wired` declaration is + # VERIFIED against this file (the "green board, inert gate" defect), and + # an undeclared script is a hard failure so new oracles must CHOOSE. + # + # This gate lives in the already-REQUIRED claim-check job on purpose: a + # brand-new job is not a required context on main, so it could be red for + # weeks without blocking anything — which is the same failure mode the + # gate exists to kill. + # + # ANTI-VACUITY: it must not become the thing it polices. `set -o pipefail` + # (a bare `| tee` reports tee's status, always 0), and the verdict is NOT + # taken from exit 0 alone — the summary the gate wrote is re-read and a + # NON-ZERO wired count over a NON-EMPTY script set is asserted, so a run + # that silently measured nothing fails instead of greening. + - name: Oracle wiring gate — every repro script declares a CI status (890) + run: | + set -o pipefail + python3 scripts/oracle_wiring_check.py --json /tmp/oracle-wiring.json --list \ + | tee /tmp/oracle-wiring.log + python3 - <<'PY' + import json, sys + s = json.load(open("/tmp/oracle-wiring.json"))["summary"] + if s["total"] < 100 or s["wired"] < 1 or s["undeclared"] != 0: + sys.exit(f"VACUOUS/DRIFTED oracle-wiring summary: {s}") + print(f"oracle-wiring gate is non-vacuous: it classified {s['total']} " + f"scripts, {s['wired']} of them wired, {s['manual']} manual, " + f"{s['unwired']} unwired-debt.") + PY # The GitHub About surface (description + topics) is pinned verbatim in # claims.yaml's repo_metadata section. API/network failure = LOUD SKIP # (exit 0) so a flake can't block merges; a real mismatch = red. @@ -1017,6 +1048,15 @@ jobs: run: python scripts/repro/fact_spec_bounds_494_differential.py --expect-decline - name: Run RED bounds force-admit divergence demonstration run: python scripts/repro/fact_spec_bounds_494_differential.py --force-admit + # #890: the phase-3+ rem_u IDENTITY differential lived in scripts/repro/ + # unwired, so the headline "with the fact, synth deletes the whole rem_u + # (2 B) where clang -Os needs a 24 B reciprocal multiply-subtract" claim + # had no standing execution gate — the specialized build's equality with + # BOTH wasmtime and the unspecialized build was hand-checked only. + - name: Run constant-divisor rem_u identity differential (#494 phase 3+) + env: + SYNTH: ./target/debug/synth + run: python scripts/repro/fact_spec_rem_494_differential.py rv32-shift-fold-oracle: name: rv32 immediate-shift-fold execution oracle @@ -2166,3 +2206,323 @@ jobs: ${{ runner.os }}-cargo- - name: Universe-complete parity + red-first + ledger-liveness run: cargo test -p synth-backend-riscv --test cross_backend_op_parity + + repro-sweep-selector-oracle: + name: repro sweep — selector / control-flow / call / i64 differentials + # #890: these differentials existed in scripts/repro/ and NOTHING RAN THEM. + # Each was written as the execution oracle for a specific miscompile (the + # issue number is in the step name) and then left unwired, so every one of + # those regressions was un-gated. They are batched here rather than given a + # job each because they share one build and one pip install; the step name + # identifies which oracle failed. The `# ci-status: wired` header in each + # script is CHECKED against this file by scripts/oracle_wiring_check.py, so + # deleting a step below turns the claim red instead of silently re-inerting + # the gate. + runs-on: ubuntu-latest + env: + SYNTH: ./target/debug/synth + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache Cargo dependencies + uses: actions/cache@v6 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo- + - name: Build synth + run: cargo build -p synth-cli + - uses: actions/setup-python@v7 + with: + python-version: "3.x" + - name: Install emulation deps + run: pip install wasmtime unicorn pyelftools capstone + - name: a32 i64 execution differential (#615, cortex-r5) + run: | + ./target/debug/synth compile scripts/repro/a32_i64_615.wat --target cortex-r5 --all-exports --relocatable --no-optimize -o /tmp/a615.o + python scripts/repro/a32_i64_615_differential.py /tmp/a615.o scripts/repro/a32_i64_615.wat + - name: out-of-range ADD immediate differential (#350) + run: | + ./target/debug/synth compile scripts/repro/add_imm_large.wat -o /tmp/ail.elf --target cortex-m4f --all-exports --relocatable + python scripts/repro/add_imm_large_differential.py /tmp/ail.elf + - name: base-CSE execution differential (#468, default + opt-out) + run: python scripts/repro/base_cse_differential.py + - name: value-returning-branch differential (#509, both paths) + run: python scripts/repro/br_table_value_509_differential.py + - name: optimized-path forward-branch shapes (#500) + run: python scripts/repro/cf_shapes_500_differential.py + - name: const-only-body return differential (#791) + run: python scripts/repro/const_body_791_differential.py + - name: 5-argument call differential (#359) + run: | + ./target/debug/synth compile scripts/repro/call_5args.wat -o /tmp/c5.o --target cortex-m4f --native-pointer-abi --all-exports --relocatable + python scripts/repro/call_5args_differential.py /tmp/c5.o + - name: 6/7-argument stack-slot call differential (#359) + run: | + ./target/debug/synth compile scripts/repro/call_6_7args.wat -o /tmp/cm.o --target cortex-m4 --all-exports --relocatable + python scripts/repro/call_6_7args_differential.py /tmp/cm.o + - name: call_indirect A32 differential (#594, cortex-r5) + run: | + ./target/debug/synth compile scripts/repro/call_indirect_594.wat --target cortex-r5 --all-exports --relocatable --no-optimize -o /tmp/ci594.o + python scripts/repro/call_indirect_594_differential.py /tmp/ci594.o + - name: call_indirect thumb differential (#597, cortex-m3) + run: | + ./target/debug/synth compile scripts/repro/call_indirect_597.wat --target cortex-m3 --all-exports --relocatable --no-optimize -o /tmp/ci597.o + python scripts/repro/call_indirect_597_differential.py /tmp/ci597.o + - name: constant-divisor strength-reduction differential (#209) + run: | + ./target/debug/synth compile scripts/repro/div_const.wat -o /tmp/dc.elf --target cortex-m4 --relocatable + python scripts/repro/div_const_differential.py /tmp/dc.elf + - name: dynamic-table lookup differential (#359) + run: | + ./target/debug/synth compile scripts/repro/dyn_table_359.wat -o /tmp/dt.o --target cortex-m4 --native-pointer-abi --all-exports --relocatable + python scripts/repro/dyn_table_359_differential.py /tmp/dt.o + - name: branch-transparent reload forwarding on gust (#390) + run: python scripts/repro/gust_spill_fwd_390_differential.py + - name: i32 register-exhaustion spill differential (#242) + run: | + ./target/debug/synth compile scripts/repro/high_pressure_i32.wat -o /tmp/hp.elf --target cortex-m4 --relocatable + python scripts/repro/high_pressure_i32_differential.py /tmp/hp.elf + - name: i64 pair-spill differential (#242) + run: | + ./target/debug/synth compile scripts/repro/high_pressure_i64.wat -o /tmp/hp64.elf --target cortex-m4 --relocatable + python scripts/repro/high_pressure_i64_differential.py /tmp/hp64.elf + - name: i64.div_s(INT64_MIN,-1) overflow-trap differential (#633) + run: python scripts/repro/i64_divs_overflow_633_differential.py + - name: i64 global.get/set pair differential (#643, both selectors) + run: python scripts/repro/i64_globals_643_differential.py + - name: i64 pair-exhaustion spill differential (#587) + run: | + SYNTH_SPILL_ON_EXHAUST=1 ./target/debug/synth compile scripts/repro/i64_pair_exhaust_587.wat -o /tmp/pe587.elf --target cortex-m4 + python scripts/repro/i64_pair_exhaust_587_differential.py /tmp/pe587.elf + - name: i64.popcnt scratch-restore clobber differential (#632) + run: python scripts/repro/i64_popcnt_632_differential.py + - name: i64 shr_u/shr_s single-function path differential (#599) + run: python scripts/repro/i64_shr_599_differential.py + - name: dead-frame elision differential (#390, both flag states) + run: python scripts/repro/leaf_dead_frame_differential.py + - name: i32 local-promotion differential (#390, clean + dirty) + run: | + ./target/debug/synth compile scripts/repro/local_promote_i32.wat -o /tmp/lp.elf --target cortex-m4 --relocatable + python scripts/repro/local_promote_i32_differential.py /tmp/lp.elf + - name: param-bounded loop back-edge differential (#663) + run: python scripts/repro/loop_param_bound_663_differential.py + - name: arg-move-cycle-under-pressure differential (#326) + run: | + ./target/debug/synth compile scripts/repro/mutex_pressure.wat -o /tmp/mp.elf --target cortex-m4 --all-exports --relocatable + python scripts/repro/mutex_pressure_differential.py /tmp/mp.elf + - name: post-exhaustion cycle proxy, execution-matched (#242) + run: python scripts/repro/postex_cycle_proxy.py + - name: read-before-write local zero-init differential (#457) + run: | + ./target/debug/synth compile scripts/repro/read_before_write_local_zeroinit.wat -o /tmp/rbw.elf --target cortex-m4 --relocatable + python scripts/repro/read_before_write_local_zeroinit_differential.py /tmp/rbw.elf + - name: allocation-time Belady spill differential (#242) + run: | + SYNTH_SPILL_ON_EXHAUST=1 ./target/debug/synth compile scripts/repro/spill_on_exhaust_242.wat -o /tmp/soe.elf --target cortex-m4 + python scripts/repro/spill_on_exhaust_242_differential.py /tmp/soe.elf + - name: direct-selector spill-rung differential (#581) + run: python scripts/repro/spill_rung_581_differential.py + - name: sret shim differential (#359) + run: | + ./target/debug/synth compile scripts/repro/sret_decide.wasm -o /tmp/sret.o --target cortex-m4 --native-pointer-abi --all-exports --relocatable + python scripts/repro/sret_decide_differential.py /tmp/sret.o + - name: u64-unpack differential (#313) + run: | + cp scripts/repro/u64_unpack.wat /tmp/u64repro.wat + ./target/debug/synth compile --target cortex-m4 --all-exports --relocatable scripts/repro/u64_unpack.wat -o /tmp/u64.elf + python scripts/repro/u64_unpack_differential.py + - name: u64-unpack if-with-result differential (#313) + run: | + ./target/debug/synth compile --target cortex-m4 --all-exports --relocatable scripts/repro/u64_unpack_if.wat -o /tmp/u64if.elf + python scripts/repro/u64_unpack_if_differential.py + - name: uxth/uxtb fold differential (#428, both flag states) + run: python scripts/repro/uxth_fold_differential.py + + repro-sweep-memory-oracle: + name: repro sweep — linear memory / static data / native-pointer differentials + # #890 companion to the selector sweep: the memory-side oracles that were + # written and never wired. The six mem757_* harnesses are the RED-FIRST + # reconstructions of gale's wrong-segment miscompile — the class that + # produced #757 — and none of them was running. postlink_359_oracle links a + # REAL image with arm-none-eabi-ld (the #368 lesson: a unicorn-on-.o oracle + # cannot see link-time retargeting), so binutils is installed for it here. + runs-on: ubuntu-latest + env: + SYNTH: ./target/debug/synth + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache Cargo dependencies + uses: actions/cache@v6 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo- + - name: Build synth + run: cargo build -p synth-cli + - uses: actions/setup-python@v7 + with: + python-version: "3.x" + - name: Install emulation deps + run: pip install wasmtime unicorn pyelftools capstone + - name: bulk-memory copy/fill numeric differential (#374) + run: | + ./target/debug/synth compile scripts/repro/bulk_memory_374_diff.wat -o /tmp/bmd.elf --target cortex-m7dp --all-exports --safety-bounds software + python scripts/repro/bulk_memory_374_differential.py /tmp/bmd.elf + - name: i64 large static offset differential (#382, direct path) + run: python scripts/repro/i64_large_offset_382_differential.py + - name: large static load/store offset differential (#382, optimized) + run: python scripts/repro/load_store_big_offset_382_differential.py + - name: memory.grow(0) differential (#539, both ARM paths) + run: python scripts/repro/mem_grow_539_differential.py + - name: static-src memmove differential (#757, inlined) + run: python scripts/repro/mem757_inlined_memmove_differential.py + - name: low-const-below-string chunked copy differential (#757) + run: python scripts/repro/mem757_low_const_copy_differential.py + - name: memory.copy from a static pointer differential (#757) + run: python scripts/repro/mem757_memcopy_static_src_differential.py + - name: memmove-with-param differential (#757) + run: python scripts/repro/mem757_memmove_param_differential.py + - name: chunked copy under register pressure differential (#757) + run: python scripts/repro/mem757_pressure_chunks_differential.py + - name: pointer-base copy differential (#757) + run: python scripts/repro/mem757_ptr_base_copy_differential.py + - name: multi-provider shared __stack_pointer co-rebase (#707) + run: | + ./target/debug/synth compile scripts/repro/mem707_multi_sp.wat -o /tmp/mem707.o --target cortex-m3 --native-pointer-abi --all-exports --relocatable --shadow-stack-size 512 + python scripts/repro/multi_sp_707_differential.py /tmp/mem707.o + - name: native-pointer shadow-stack frame differential (#237) + run: | + ./target/debug/synth compile scripts/repro/native_pointer_shadow_stack.wat -o /tmp/np_ss.elf --target cortex-m4 --native-pointer-abi --all-exports --relocatable + python scripts/repro/native_pointer_shadow_stack_differential.py /tmp/np_ss.elf + - name: inline-statics down-shift differential (#678) + run: | + ./target/debug/synth compile scripts/repro/mem678_full.wat -o /tmp/mem678.o --target cortex-m3 --native-pointer-abi --all-exports --relocatable --shadow-stack-size 512 + python scripts/repro/native_pointer_static_downshift_678.py /tmp/mem678.o + - name: volatile DMA-window back-off differential (#543, four builds) + run: python scripts/repro/volatile_segment_543_differential.py + - name: Install binutils-arm-none-eabi (#359 post-link oracle) + run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends binutils-arm-none-eabi + - name: post-link static-data placement oracle (#359) + run: PATH=$PWD/target/debug:$PATH python scripts/repro/postlink_359_oracle.py + + repro-sweep-rv32-oracle: + name: repro sweep — RISC-V RV32 execution differentials + # #890: every RV32 oracle below pins a regression gale found on real + # qemu_riscv32 silicon (#220 callee-saved, #226 live-range clobber, #232 + # overflow-guard clobber, #317 i64 sign, #343 if-join) — and none of them + # was wired, so the backend those findings hardened had no standing + # execution gate for them. + runs-on: ubuntu-latest + env: + SYNTH: ./target/debug/synth + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache Cargo dependencies + uses: actions/cache@v6 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo- + - name: Build synth + run: cargo build -p synth-cli + - uses: actions/setup-python@v7 + with: + python-version: "3.x" + - name: Install emulation deps + run: pip install wasmtime unicorn pyelftools capstone + - name: control_step RV32 correctness + ABI + shipped data (#223/#798) + run: | + ./target/debug/synth compile scripts/repro/control_step.wasm -b riscv -t rv32imac --all-exports --relocatable -o /tmp/cs_rv.o + python scripts/repro/control_step_riscv_differential.py /tmp/cs_rv.o + - name: controller_step RV32 live-range clobber differential (#226) + run: | + ./target/debug/synth compile scripts/repro/controller_step.wat -b riscv -t rv32imac --all-exports --relocatable -o /tmp/ctrl_rv.o + python scripts/repro/controller_step_riscv_differential.py /tmp/ctrl_rv.o + - name: RV32 callee-saved preservation differential (#220) + run: | + ./target/debug/synth compile scripts/repro/filter_axis.wasm -b riscv -t rv32imac --relocatable -o /tmp/fa.o + python scripts/repro/filter_axis_riscv_differential.py /tmp/fa.o + - name: RV32 i64 div_s/rem_s sign differential (#317) + run: | + ./target/debug/synth compile scripts/repro/i64_divs_317.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/i317.o + python scripts/repro/i64_divs_317_riscv_differential.py /tmp/i317.o + - name: RV32 i64-param LOUD-SKIP contrast oracle (#518) + run: python scripts/repro/i64_param_518_riscv_loudskip.py + - name: RV32 if-with-result join reconciliation (#343) + run: | + ./target/debug/synth compile scripts/repro/if_else_result_343.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/if343.o + python scripts/repro/if_else_result_343_riscv_differential.py /tmp/if343.o + - name: RV32 mask/software bounds effective-address oracle (#655) + run: python scripts/repro/mask_bounds_655_riscv_differential.py + - name: RV32 cmp->select fusion differential (#472) + run: | + ./target/debug/synth compile scripts/repro/rv32_cmp_select_472.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/cmpsel.o + python scripts/repro/rv32_cmp_select_472_riscv_differential.py /tmp/cmpsel.o + - name: RV32 i32 local-promotion differential (#472) + run: | + ./target/debug/synth compile scripts/repro/rv32_local_promotion_472.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/promo.o + python scripts/repro/rv32_local_promotion_472_riscv_differential.py /tmp/promo.o + - name: RV32 signed-div-const overflow-guard clobber (#232) + run: | + ./target/debug/synth compile scripts/repro/signed_div_const.wasm -b riscv -t rv32imac --all-exports --relocatable -o /tmp/sdiv.o + python scripts/repro/signed_div_const_riscv_differential.py /tmp/sdiv.o + - name: RV32 u64-unpack differential (#313) + run: | + ./target/debug/synth compile scripts/repro/u64_unpack_inlined.wat -b riscv -t rv32imac --all-exports --relocatable -o /tmp/u64_rv32.elf + python scripts/repro/u64_unpack_riscv_differential.py + + repro-sweep-wcet-oracle: + name: repro sweep — WCET bound soundness cross-checks (phases 2-5) + # #890: the SOUNDNESS evidence for --emit-wcet. The cargo gate + # (wcet_bound_gate.rs) pins the bounds analytically; these four harnesses + # are the only thing that EXECUTES the fixtures under unicorn and checks + # `bound_cycles >= executed_instructions`, i.e. that the bound synth + # publishes is actually an upper bound. They were unwired — the soundness + # claim in CLAUDE.md rested on a hand-run script. + # SYNTH must be ABSOLUTE here: these harnesses chdir into a temp dir. + runs-on: ubuntu-latest + env: + SYNTH: ${{ github.workspace }}/target/debug/synth + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache Cargo dependencies + uses: actions/cache@v6 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo- + - name: Build synth + run: cargo build -p synth-cli + - uses: actions/setup-python@v7 + with: + python-version: "3.x" + - name: Install emulation deps + run: pip install wasmtime unicorn pyelftools capstone + - name: WCET phase-2 const-loop bound soundness (#778) + run: python scripts/repro/wcet_phase2_778_unicorn_soundness.py + - name: WCET phase-3 inter-procedural composition soundness (#778) + run: python scripts/repro/wcet_phase3_778_compose_soundness.py + - name: WCET phase-4 bounded-recursion soundness (#49) + run: python scripts/repro/wcet_phase4_49_recursion_soundness.py + - name: WCET phase-5 masked-ceiling loop soundness (#778) + run: python scripts/repro/wcet_phase5_778_masked_loop_soundness.py From 638153cd791b2d52442a58a4e672339596e6300c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 14:52:12 +0200 Subject: [PATCH 4/9] feat(#890): ratchet the manual/unwired budgets + policy doc (step 4/5) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit claims.yaml SYNTH-ORACLE-WIRING-890 pins the totals the header comments cannot express: wired >= 145 (a FLOOR — the oracle surface must not be emptied by deleting harnesses instead of fixing them), manual <= 7 (a ceiling on the legitimate escape hatch), unwired <= 0 (a ceiling of ZERO — a new un-wired oracle is a red build, not a backlog entry). Proved by mutation: flipping one wired script to manual fails BOTH the floor and the ceiling legs. This generalizes SYNTH-GPIO-846-ORACLE-CI-WIRED, which hand-pins exactly one script's CI wiring — the instance-at-a-time shape #890 exists to replace. Also hardens the gate after a mutation found a real defect in it: `pipefail` without `-e` let the INERT-GATE mutation green the CI step, because the shell's status is its last command's. The step now sets `-euo pipefail` explicitly and the summary carries `wired_unreferenced` + `failures` so the verdict is reachable from the summary alone, never from exit 0. scripts/repro/ORACLE_WIRING.md documents the mechanism, argues header-over- manifest, itemizes the manual seven, and carries the four-mutation transcript (each run executes the step extracted VERBATIM from ci.yml, so there is no drift between what was proved and what CI runs). Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 28 ++++-- claims.yaml | 44 +++++++++ scripts/oracle_wiring_check.py | 9 ++ scripts/repro/ORACLE_WIRING.md | 172 +++++++++++++++++++++++++++++++++ 4 files changed, 244 insertions(+), 9 deletions(-) create mode 100644 scripts/repro/ORACLE_WIRING.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index af058887..78eb5a7c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -191,24 +191,34 @@ jobs: # weeks without blocking anything — which is the same failure mode the # gate exists to kill. # - # ANTI-VACUITY: it must not become the thing it polices. `set -o pipefail` - # (a bare `| tee` reports tee's status, always 0), and the verdict is NOT - # taken from exit 0 alone — the summary the gate wrote is re-read and a - # NON-ZERO wired count over a NON-EMPTY script set is asserted, so a run - # that silently measured nothing fails instead of greening. + # ANTI-VACUITY: it must not become the thing it polices. + # * `set -euo pipefail` EXPLICITLY. A bare `| tee` reports tee's status + # (always 0), and — found by mutating this very step — `pipefail` + # WITHOUT `-e` is not enough either: the script's status is its LAST + # command's, so the inert-gate mutation greened the step while the + # gate itself printed FAIL and exited 1. Actions' default shell is + # `bash -e`, but this step does not lean on that default. + # * The verdict is re-derived from the summary the gate WROTE, not from + # exit 0: a non-empty script set, a non-zero wired count, zero + # undeclared, zero wired-but-unreferenced, and zero failures. - name: Oracle wiring gate — every repro script declares a CI status (890) run: | - set -o pipefail + set -euo pipefail python3 scripts/oracle_wiring_check.py --json /tmp/oracle-wiring.json --list \ | tee /tmp/oracle-wiring.log python3 - <<'PY' import json, sys s = json.load(open("/tmp/oracle-wiring.json"))["summary"] - if s["total"] < 100 or s["wired"] < 1 or s["undeclared"] != 0: - sys.exit(f"VACUOUS/DRIFTED oracle-wiring summary: {s}") + bad = [k for k, v in (("total<100", s["total"] < 100), + ("wired==0", s["wired"] < 1), + ("undeclared", s["undeclared"]), + ("wired_unreferenced", s["wired_unreferenced"]), + ("failures", s["failures"])) if v] + if bad: + sys.exit(f"oracle-wiring gate VACUOUS or DRIFTED {bad}: {s}") print(f"oracle-wiring gate is non-vacuous: it classified {s['total']} " f"scripts, {s['wired']} of them wired, {s['manual']} manual, " - f"{s['unwired']} unwired-debt.") + f"{s['unwired']} unwired-debt, 0 inert.") PY # The GitHub About surface (description + topics) is pinned verbatim in # claims.yaml's repo_metadata section. API/network failure = LOUD SKIP diff --git a/claims.yaml b/claims.yaml index 7602948b..3a71ca87 100644 --- a/claims.yaml +++ b/claims.yaml @@ -922,3 +922,47 @@ claims: text: "pip install wasmtime unicorn pyelftools capstone" - kind: verbatim text: 'grep -q "^#846 CHECKS=75/75" gpio846.out' + + # --------------------------------------------------------------------------- + # #890 — the ORACLE-WIRING surface, generalized. SYNTH-GPIO-846-ORACLE-CI-WIRED + # above pins ONE script's CI wiring by hand; that is the instance-at-a-time + # shape this entry replaces. `scripts/repro/*.py` are synth's execution + # oracles, and 69 of 150 were referenced by NO workflow while nothing in the + # tree told a forgotten gate from an intentionally-manual one. Every script now + # carries a `# ci-status:` declaration and `scripts/oracle_wiring_check.py` + # (claim-check CI job) PROVES every `wired` one is actually wired — that check + # is mechanical and needs no ledger. What a header CANNOT express is the + # ratchet on the totals, which is what this entry is: + # + # * wired >= 145 — a FLOOR. The oracle surface must not be emptied by + # deleting harnesses instead of fixing them. + # * manual <= 7 — a CEILING on the legitimate escape hatch (4 measurement, + # 2 scratch, 1 external-input; itemized in the doc). An + # eighth needs a conversation, not a commit. + # * unwired <= 0 — a CEILING OF ZERO on known debt. A new oracle that is + # not wired is a RED BUILD, not a backlog entry. + # + # Lower the manual ceiling when one is wired; never raise it to green a build. + # --------------------------------------------------------------------------- + - id: SYNTH-ORACLE-WIRING-890 + doc: scripts/repro/ORACLE_WIRING.md + text: "**145 wired**" + evidence: + - kind: file-exists + path: scripts/oracle_wiring_check.py + - kind: count-min # the surface must not be emptied + pattern: '^# ci-status: wired' + glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] + min: 145 + - kind: count-max # the legitimate escape hatch + pattern: '^# ci-status: manual' + glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] + max: 7 + - kind: count-max # known debt: zero, and it stays zero + pattern: '^# ci-status: unwired' + glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] + max: 0 + - kind: verbatim # the doc must carry the manual budget + text: "**7 manual**" + - kind: verbatim + text: "**0 unwired**" diff --git a/scripts/oracle_wiring_check.py b/scripts/oracle_wiring_check.py index 07fb59b5..ef3504b0 100644 --- a/scripts/oracle_wiring_check.py +++ b/scripts/oracle_wiring_check.py @@ -212,6 +212,13 @@ def summarize(records): if s == "manual" and r.get("category"): by_cat[r["category"]] = by_cat.get(r["category"], 0) + 1 out["manual_by_category"] = dict(sorted(by_cat.items())) + # The INERT-GATE count, carried in the summary on purpose: a consumer must + # be able to reach the verdict from the summary ALONE, without trusting an + # exit status. (Found by mutation: with only `pipefail` and no `-e`, a shell + # wrapper whose last command was the summary check greened this very case.) + out["wired_unreferenced"] = sum( + 1 for r in records if r["status"] == "wired" and not r["workflows"] + ) return out @@ -262,6 +269,8 @@ def main(): + ", ".join(f"{k}={v}" for k, v in summary["manual_by_category"].items()) ) + summary["failures"] = len(fails) + if args.json: pathlib.Path(args.json).write_text( json.dumps( diff --git a/scripts/repro/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md new file mode 100644 index 00000000..1c1e6c3b --- /dev/null +++ b/scripts/repro/ORACLE_WIRING.md @@ -0,0 +1,172 @@ +# Oracle wiring — every repro script declares its CI status (#890) + +`scripts/repro/*.py` are synth's **execution oracles**: the differentials that +run compiled output under unicorn/wasmtime and catch silent miscompiles. They +are the reason several whole classes of defect (#757 wrong-segment static data, +#220 RV32 callee-saved, #518 i64 params) were found at all. + +Writing an oracle and **wiring** an oracle are two separate steps, and the second +is the one that gets dropped under release pressure. Before this gate, **69 of +150** repro scripts were referenced by no workflow at all — and nothing in the +tree distinguished + +> *manual by design* — needs gale's pinned vendor drop, real silicon, a licensed +> input, or a toolchain CI does not install + +from + +> *somebody forgot*. + +A forgotten gate is indistinguishable from an intentional one, so the only way to +tell was to read all 150 scripts and reason about each — an audit that kept +rediscovering the same defect one instance at a time. v0.53 hand-wired three of +them and **the unwired count still went up**: the instances were fixed, the +factory that produces them was not. One of the three had a green PR board while +its central gate was inert, so the claim it backed was hand-checked only. + +## The mechanism + +Every `scripts/repro/*.py` and `*.sh` carries **exactly one** declaration line, +conventionally on the line after the shebang: + +```python +#!/usr/bin/env python3 +# ci-status: wired +``` +```python +# ci-status: manual (external-input) — needs gale's merged.both.loom.wat, fetched +# at run time from a gist that is not in-tree and not vendored; ... +``` +```python +# ci-status: unwired — no blocker, just not wired yet: +``` + +`scripts/oracle_wiring_check.py` enforces it, and runs as a step of the +**`claim-check`** CI job. + +### Why a header comment, not a manifest file + +* **Locality.** The declaration lives in the file it describes, so it appears in + the diff of the PR that adds the script. An author cannot add an oracle + without meeting the convention. +* **No second source of truth.** A manifest entry can outlive its script (rename, + delete) and is edited far from the thing it describes. A header cannot drift + from its own file. +* The repo already reserves the central-ledger shape (`claims.yaml`) for claims + that have *no natural home* — prose spread across many docs. A script's CI + status has a natural home: the script. `claims.yaml` is still used here, but + only for the one thing a header cannot express: the **ratchet** on the totals. + +### Three statuses, on purpose + +| status | meaning | checked | +|---|---|---| +| `wired` | at least one `.github/workflows/*.yml` references the file by name | **verified** — declaring `wired` with no workflow reference is a hard failure | +| `manual` | legitimately not CI-runnable | needs a category from a closed set **and** a real reason; must NOT be referenced by a workflow | +| `unwired` | known debt: no blocker, simply not wired yet | needs a reason saying what it would take | + +`manual` and `unwired` are separate so that **honest blockers and backlog cannot +hide inside each other**. Undeclared is a failure: a new oracle is forced to +choose. + +The `manual` categories are a closed set (`hardware`, `toolchain`, +`external-input`, `network`, `measurement`, `superseded`, `red-first`, `scratch`, +`slow`) declared in the gate script, so the manual surface stays groupable and +arguable instead of becoming a free-text dumping ground. Adding a category is a +deliberate code change. + +## The ratchet + +The totals are pinned in `claims.yaml` (`SYNTH-ORACLE-WIRING-890`) so they can be +argued **down** over time and cannot grow silently: + +- **145 wired** — a floor (`count-min`). The surface cannot be emptied by + deleting oracles instead of fixing them. +- **7 manual** — a ceiling (`count-max`). An eighth needs a conversation, not a + commit. +- **0 unwired** — a ceiling of zero. Any new un-wired oracle is a **red build**, + not a silent backlog entry. + +The gate also writes a table (and the unwired-debt list) to +`$GITHUB_STEP_SUMMARY`, so the backlog is visible on every run rather than only +in a log nobody opens. + +## The manual seven + +| script | category | why | +|---|---|---| +| `wake_path_differential.py` | external-input | needs gale's `merged.both.loom.wat`, fetched from a gist; the WAKE path cannot be reproduced from any in-repo fixture (the debugger perturbs the race on silicon) | +| `size_attribution_390.py` | measurement | prints the #390 size-attribution table; the numbers are pinned by `crates/synth-cli/tests/size_attribution_390.rs`, which *is* the gate | +| `local_promotion_headroom.py` | measurement | #390 scoping spike; no expected values, no verdict. The lever it sized is gated by the wired `local_promote_i32_differential.py` | +| `vcr_dec_001_join_alloc_measure.py` | measurement | the #242 join-allocator ON-vs-OFF comparison deliverable; deliberately has no verdict | +| `spill_baseline_measure.sh` | measurement | VCR-PERF-001 Pass-1 spill-waste census; changes zero codegen bytes, no expected values | +| `run204_unicorn.py` | scratch | #204 bring-up probe, hardcoded `/tmp/gz.bin` + hand-transcribed stub offsets from one historical disassembly; asserts nothing | +| `i64_load_store_372_differential.py` | scratch | 25-line print-only probe; superseded as a gate by the wired `i64_large_offset_382` / `load_store_big_offset_382` differentials | + +## Anti-vacuity — the gate must not become the thing it polices + +The gate is CI-wired in the same commit that introduced it, as a step of the +**already-required** `claim-check` job. A brand-new job is not a required context +on `main`, so it could sit red for weeks without blocking anything — the same +failure mode the gate exists to kill. + +The step uses `set -euo pipefail` **explicitly** and does not take its verdict +from exit 0: it re-reads the JSON summary the gate wrote and asserts a non-empty +script set, a non-zero `wired` count, and zero `undeclared` / +`wired_unreferenced` / `failures`. + +`-e` is not decoration. It was added *because a mutation caught its absence*: +with `pipefail` alone, the shell's status is its **last** command's, so the +inert-gate mutation greened the step while the gate itself printed `FAIL` and +exited 1. `wired_unreferenced` was added to the summary in the same fix, so the +verdict is reachable from the summary alone. + +### Red-first mutation evidence + +Each run below executes the Oracle-wiring step **extracted verbatim from +`ci.yml`** (`yaml.safe_load` → the step's `run:` block → `bash -e`), so there is +no transcription drift between what was proved and what CI runs. + +``` +===== BASELINE ===== +STEP EXIT=0 +all repro scripts declare a CI status, and every `wired` one is wired. +oracle-wiring gate is non-vacuous: it classified 152 scripts, 145 of them wired, +7 manual, 0 unwired-debt, 0 inert. + +===== MUTATION 1: un-declare mem757_ptr_base_copy_differential.py ===== +STEP EXIT=1 +FAIL scripts/repro/mem757_ptr_base_copy_differential.py: UNDECLARED — add a +`# ci-status:` header line ... An oracle nothing runs must SAY so. + +===== MUTATION 2: declare `wired` on wake_path (no workflow reference) ===== +STEP EXIT=1 +FAIL scripts/repro/wake_path_differential.py: declares `wired` but NO workflow +references it — the gate is INERT. + +===== MUTATION 3: delete a wired oracle's CI step (re-inert it) ===== +STEP EXIT=1 +FAIL scripts/repro/mem757_low_const_copy_differential.py: declares `wired` but NO +workflow references it — the gate is INERT. + +===== MUTATION 4: gate measures nothing (glob matches no scripts) ===== +STEP EXIT=1 +oracle-wiring gate VACUOUS or DRIFTED ['total<100']: {'total': 2, 'wired': 1, ...} + +===== RESTORED ===== +STEP EXIT=0 +``` + +Mutation 3 is the one that closes the loop the other way: deleting a CI step +without touching the script no longer silently re-inerts the oracle. + +## Adding a repro script + +1. Write the harness. Give it **exit-code discipline** — `sys.exit(0 if ok else 1)`. + A harness that prints `MISMATCH` and exits 0 is a gate that cannot fail + (`sret_decide_differential.py` was exactly that until #890). +2. Read the binary under test from `$SYNTH` (`os.environ.get("SYNTH", ...)`), so + CI can point it at its own build. +3. Add a CI step and declare `# ci-status: wired`; or declare `manual ()` + / `unwired` with a real reason and bump `SYNTH-ORACLE-WIRING-890` in + `claims.yaml`. From 229df75d5c612c31d4a98459ca6ac6110d9bd11c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:03:52 +0200 Subject: [PATCH 5/9] fix(#890): a COMMENT mention must not count as wired (step 5/5) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The gate derived "referenced by a workflow" from a raw grep of the .yml, so a mention in a COMMENT satisfied it — a gate satisfiable by prose, which is the exact failure shape #890 exists to reject. References now come from the PARSED workflow: each step's `run:` body plus its `with:`/`env:` values. A workflow that will not parse is a hard error, never a silent pass. No script changed status (verified before the change: zero of the 145 wired were wired by a comment alone), so this is pure future-proofing — but the diagnostic now says WHY: "It IS mentioned in ci.yml, but only in a COMMENT — prose does not run an oracle." Mutation matrix against the final gate, each run executing the step extracted VERBATIM from ci.yml (no drift between what was proved and what CI runs): baseline EXIT 0 M1 un-declare a script EXIT 1 UNDECLARED M2 declare wired, no reference at all EXIT 1 the gate is INERT M3 delete a wired oracle's CI step EXIT 1 the gate is INERT M4 gate's glob matches nothing EXIT 1 VACUOUS ['total<100'] M5 reference demoted to a comment EXIT 1 only in a COMMENT M6 manual reason replaced with "TODO" EXIT 1 needs a REAL reason restored EXIT 0 Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- scripts/oracle_wiring_check.py | 60 +++++++++++++++++++++++++++++----- scripts/repro/ORACLE_WIRING.md | 44 ++++++++++++++++++------- 2 files changed, 85 insertions(+), 19 deletions(-) diff --git a/scripts/oracle_wiring_check.py b/scripts/oracle_wiring_check.py index ef3504b0..23b1dc3e 100644 --- a/scripts/oracle_wiring_check.py +++ b/scripts/oracle_wiring_check.py @@ -65,6 +65,11 @@ import re import sys +try: + import yaml +except ImportError: # pragma: no cover - the claim-check job installs PyYAML + sys.exit("oracle_wiring_check: needs PyYAML (pip install pyyaml)") + # The closed set of `manual` categories. Adding one is a deliberate code change # (and a review conversation), not a free-text escape hatch. MANUAL_CATEGORIES = { @@ -107,13 +112,45 @@ def collect(root): return scripts, workflows +def executable_surface(workflows): + """Map workflow filename -> the text a runner would actually EXECUTE. + + A raw grep of the .yml would count a mention in a COMMENT as "wired" — a + gate satisfied by prose, which is the failure shape this whole check exists + to reject. So references are derived from the PARSED workflow: each step's + `run:` body plus its `with:`/`env:` values. A workflow that will not parse + is a hard error, never a silent pass. + """ + surface, raw = {}, {} + for w in workflows: + name = os.path.basename(w) + raw[name] = pathlib.Path(w).read_text(errors="ignore") + try: + doc = yaml.safe_load(raw[name]) or {} + except yaml.YAMLError as exc: + raise RuntimeError(f"workflow {name} does not parse: {exc}") from exc + chunks = [] + for job in (doc.get("jobs") or {}).values(): + if not isinstance(job, dict): + continue + for st in job.get("steps") or []: + if not isinstance(st, dict): + continue + if isinstance(st.get("run"), str): + chunks.append(st["run"]) + for block in ("with", "env"): + for v in (st.get(block) or {}).values(): + chunks.append(str(v)) + for v in (job.get("env") or {}).values(): + chunks.append(str(v)) + surface[name] = "\n".join(chunks) + return surface, raw + + def classify(root, scripts, workflows): """Return (records, failures). One record per script; failures are strings.""" - wf_text = { - os.path.basename(w): pathlib.Path(w).read_text(errors="ignore") - for w in workflows - } - blob = "\n".join(wf_text.values()) + wf_text, wf_raw = executable_surface(workflows) + blob = "\n".join(wf_raw.values()) records, fails = [], [] for path in scripts: @@ -151,10 +188,17 @@ def classify(root, scripts, workflows): if status == "wired": if not refs: + mentioned = [w for w, t in wf_raw.items() if name in t] + where = ( + f" It IS mentioned in {', '.join(mentioned)}, but only in a " + f"COMMENT — prose does not run an oracle." + if mentioned + else "" + ) fails.append( - f"{rel}: declares `wired` but NO workflow references it — " - f"the gate is INERT. Wire it in .github/workflows/, or " - f"downgrade the declaration to `unwired`/`manual`." + f"{rel}: declares `wired` but NO workflow STEP runs it — " + f"the gate is INERT.{where} Wire it in .github/workflows/, " + f"or downgrade the declaration to `unwired`/`manual`." ) if category: fails.append(f"{rel}: `wired` takes no category (got {category!r})") diff --git a/scripts/repro/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md index 1c1e6c3b..114925cd 100644 --- a/scripts/repro/ORACLE_WIRING.md +++ b/scripts/repro/ORACLE_WIRING.md @@ -44,6 +44,12 @@ conventionally on the line after the shebang: `scripts/oracle_wiring_check.py` enforces it, and runs as a step of the **`claim-check`** CI job. +"Referenced by a workflow" means referenced by something a runner would +**execute** — a step's `run:` body, or a `with:`/`env:` value — derived from the +*parsed* workflow, not from a raw grep. A mention in a comment does not count: a +gate satisfiable by prose is the failure shape this check exists to reject. (A +workflow that will not parse is a hard error, never a silent pass.) + ### Why a header comment, not a manifest file * **Locality.** The declaration lives in the file it describes, so it appears in @@ -130,35 +136,51 @@ no transcription drift between what was proved and what CI runs. ``` ===== BASELINE ===== STEP EXIT=0 -all repro scripts declare a CI status, and every `wired` one is wired. oracle-wiring gate is non-vacuous: it classified 152 scripts, 145 of them wired, 7 manual, 0 unwired-debt, 0 inert. -===== MUTATION 1: un-declare mem757_ptr_base_copy_differential.py ===== +===== M1: un-declare mem757_ptr_base_copy_differential.py ===== STEP EXIT=1 FAIL scripts/repro/mem757_ptr_base_copy_differential.py: UNDECLARED — add a -`# ci-status:` header line ... An oracle nothing runs must SAY so. +`# ci-status:` header line (wired | manual () — reason | unwired ... -===== MUTATION 2: declare `wired` on wake_path (no workflow reference) ===== +===== M2: declare `wired` on wake_path (no reference at all) ===== STEP EXIT=1 FAIL scripts/repro/wake_path_differential.py: declares `wired` but NO workflow -references it — the gate is INERT. +STEP runs it — the gate is INERT. Wire it in .github/workflows/, or dow... -===== MUTATION 3: delete a wired oracle's CI step (re-inert it) ===== +===== M3: delete a wired oracle's CI step ===== STEP EXIT=1 FAIL scripts/repro/mem757_low_const_copy_differential.py: declares `wired` but NO -workflow references it — the gate is INERT. +workflow STEP runs it — the gate is INERT. Wire it in .github/workfl... + +===== M4: gate glob matches nothing ===== +STEP EXIT=1 +oracle-wiring gate VACUOUS or DRIFTED ['total<100']: {'failures': 0, 'manual': 1, +'manual_by_category': {'measurement': 1}, 'total': 2, 'undeclared': ... -===== MUTATION 4: gate measures nothing (glob matches no scripts) ===== +===== M5: reference demoted to a COMMENT ===== STEP EXIT=1 -oracle-wiring gate VACUOUS or DRIFTED ['total<100']: {'total': 2, 'wired': 1, ...} +FAIL scripts/repro/mem757_memmove_param_differential.py: declares `wired` but NO +workflow STEP runs it — the gate is INERT. It IS mentioned in ci.yml, ... + +===== M6: manual reason replaced with a placeholder ===== +STEP EXIT=1 +FAIL scripts/repro/run204_unicorn.py: `manual` needs a REAL reason (>= 20 chars, +not a placeholder); got 'TODO' ===== RESTORED ===== STEP EXIT=0 ``` -Mutation 3 is the one that closes the loop the other way: deleting a CI step -without touching the script no longer silently re-inerts the oracle. +**M3** closes the loop the other way: deleting a CI step without touching the +script no longer silently re-inerts the oracle. **M5** closes it a third way: a +step demoted to a comment still *mentions* the script, and a raw grep would call +that wired — prose does not run an oracle. + +`SYNTH-ORACLE-WIRING-890`'s ratchet legs are proved the same way: flipping one +wired script to `manual` fails **both** `count-min 145` (the floor) and +`count-max 7` (the ceiling). ## Adding a repro script From 64f4f052d9db0840066b11a488a30501bce6c2ed Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:05:17 +0200 Subject: [PATCH 6/9] docs(#890): record the REAL CI-red evidence for the oracle-wiring gate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A gate that has never been seen to fire is indistinguishable from one that cannot — which is the #890 thesis applied to #890 itself. So both required mutations were run through GitHub, not just locally: a throwaway branch carrying only the two mutations turned the real `Claim Check` job red at the Oracle wiring gate step (PR #895, closed unmerged, branch deleted). oracle wiring: 152 repro scripts — 145 wired, 6 manual, 0 unwired(debt), 1 UNDECLARED FAIL ... mem757_ptr_base_copy_differential.py: UNDECLARED ... FAIL ... wake_path_differential.py: declares `wired` but NO workflow references it — the gate is INERT ... ##[error]Process completed with exit code 1. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- scripts/repro/ORACLE_WIRING.md | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) diff --git a/scripts/repro/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md index 114925cd..8567875d 100644 --- a/scripts/repro/ORACLE_WIRING.md +++ b/scripts/repro/ORACLE_WIRING.md @@ -127,7 +127,27 @@ inert-gate mutation greened the step while the gate itself printed `FAIL` and exited 1. `wired_unreferenced` was added to the summary in the same fix, so the verdict is reachable from the summary alone. -### Red-first mutation evidence +### Red-first evidence — in real CI + +M1 and M2 were also proved on a throwaway branch whose only content was the two +mutations, so the failure is a genuine **`Claim Check` job** result on GitHub — +not a local reproduction. That branch was closed unmerged +([PR #895](https://github.com/pulseengine/synth/pull/895), +[run](https://github.com/pulseengine/synth/actions/runs/30545009045/job/90878830002)): + +``` +oracle wiring: 152 repro scripts — 145 wired, 6 manual, 0 unwired(debt), 1 UNDECLARED +FAIL scripts/repro/mem757_ptr_base_copy_differential.py: UNDECLARED — add a + `# ci-status:` header line ... An oracle nothing runs must SAY so. +FAIL scripts/repro/wake_path_differential.py: declares `wired` but NO workflow + references it — the gate is INERT ... +##[error]Process completed with exit code 1. +``` + +This matters for exactly the reason #890 exists: a gate that has never been seen +to fire is indistinguishable from one that cannot. + +### Red-first mutation evidence — the full matrix Each run below executes the Oracle-wiring step **extracted verbatim from `ci.yml`** (`yaml.safe_load` → the step's `run:` block → `bash -e`), so there is From a12dad5269de72d2f4500e3b7c27bfbca9048141 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:06:22 +0200 Subject: [PATCH 7/9] docs(#890): the gate docstring says PARSED-workflow, matching the implementation Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- scripts/oracle_wiring_check.py | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/scripts/oracle_wiring_check.py b/scripts/oracle_wiring_check.py index 23b1dc3e..8e14bb78 100644 --- a/scripts/oracle_wiring_check.py +++ b/scripts/oracle_wiring_check.py @@ -41,9 +41,13 @@ THREE STATUSES, on purpose -------------------------------------------------------------------------- - wired — at least one `.github/workflows/*.yml` references the file by name. - VERIFIED here: declaring `wired` without a workflow reference is a - hard failure. This is the exact "green board, inert gate" defect. + wired — at least one `.github/workflows/*.yml` STEP runs the file. + VERIFIED here: declaring `wired` without one is a hard failure — + the exact "green board, inert gate" defect. "References" is derived + from the PARSED workflow (a step's `run:` body plus its + `with:`/`env:` values), never a raw grep: a mention in a COMMENT + would otherwise satisfy the gate, and a gate satisfiable by prose + is the very shape this check exists to reject. manual — legitimately NOT CI-runnable. Requires a CATEGORY from the fixed list below plus a reason. Categories are a closed set so the manual surface stays groupable and arguable, not a free-text dumping From 46845202eabf1e6b1a9ae6ab8614f740662aef66 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 15:07:52 +0200 Subject: [PATCH 8/9] fix(#890): scope the dangling-reference check to the executable surface MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The reverse check (a workflow step running a repro script that no longer exists) scanned the RAW .yml, so a stale mention in a COMMENT would have been reported as a "dangling CI step" — a false red, and the wrong diagnosis: untidy prose is not a broken gate. It now scans the same executable surface the forward check uses. Proved still live by mutation: adding a step that runs a nonexistent script fails with the dangling-step message (EXIT 1). Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- scripts/oracle_wiring_check.py | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/scripts/oracle_wiring_check.py b/scripts/oracle_wiring_check.py index 8e14bb78..81862fbf 100644 --- a/scripts/oracle_wiring_check.py +++ b/scripts/oracle_wiring_check.py @@ -154,7 +154,6 @@ def executable_surface(workflows): def classify(root, scripts, workflows): """Return (records, failures). One record per script; failures are strings.""" wf_text, wf_raw = executable_surface(workflows) - blob = "\n".join(wf_raw.values()) records, fails = [], [] for path in scripts: @@ -236,12 +235,15 @@ def classify(root, scripts, workflows): f"expected wired | manual | unwired" ) - # Reverse direction: a workflow may not reference a repro script that is - # gone (a rename that half-landed leaves a step that can never run). + # Reverse direction: a workflow STEP may not run a repro script that is gone + # (a rename that half-landed leaves a step that can never run). Scoped to the + # executable surface on purpose — a stale mention in a comment is untidy + # prose, not a broken gate, and calling it one would be a false red. on_disk = {os.path.basename(p) for p in scripts} | { os.path.basename(p) for p in glob.glob(str(root / "scripts/repro/*")) } - for ref in sorted(set(re.findall(r"scripts/repro/([\w.\-]+)", blob))): + exec_blob = "\n".join(wf_text.values()) + for ref in sorted(set(re.findall(r"scripts/repro/([\w.\-]+)", exec_blob))): if ref not in on_disk: fails.append( f".github/workflows: references scripts/repro/{ref}, which does " From cdca03178246b631d0a5310dabb2e9c2b29e0238 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 30 Jul 2026 16:48:30 +0200 Subject: [PATCH 9/9] ci(#890): install wabt in the four repro sweeps; restore the lane CHANGELOG after rebase MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two fixes on top of the rebase onto main (which now carries L4 #896 and the bare-pipefail hardening #900). 1. **wat2wasm was missing.** Both failing sweeps died with `FileNotFoundError: 'wat2wasm'`. That is the gate DOING ITS JOB: these 63 oracles had never run in CI, so their host dependencies had never been discovered — exactly the class that made the #881 VFP oracle fail on the runner while passing locally (#850). Several fixtures build their .wasm from .wat at test time. wabt installed in all four sweep jobs. 2. **Restored this lane's CHANGELOG entries.** My conflict resolution kept the `# ci-status:` header lines plus main's side, which is correct for the repro scripts and WRONG for an additive CHANGELOG — it silently dropped all four of the lane's bullets. Recovered verbatim from the pre-rebase branch and merged with the existing entry. Caught by counting bullets after the rebase rather than trusting that a clean `rebase --continue` meant a clean result. Rebase conflict in vcr_dec_001_join_alloc_execution_differential.py resolved keeping BOTH sides: L4's updated "increments 2+3" docstring and this lane's ci-status header. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 20 ++++++++++++++ CHANGELOG.md | 57 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 77 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 78eb5a7c..c61c6844 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2251,6 +2251,11 @@ jobs: python-version: "3.x" - name: Install emulation deps run: pip install wasmtime unicorn pyelftools capstone + - name: Install wabt (wat2wasm — required by the newly-wired oracles) + # #890: these oracles were never CI-run, so their host deps were never + # discovered. wat2wasm is absent on the runner and several fixtures + # build their .wasm from .wat at test time (the #850/#881 class). + run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends wabt - name: a32 i64 execution differential (#615, cortex-r5) run: | ./target/debug/synth compile scripts/repro/a32_i64_615.wat --target cortex-r5 --all-exports --relocatable --no-optimize -o /tmp/a615.o @@ -2384,6 +2389,11 @@ jobs: python-version: "3.x" - name: Install emulation deps run: pip install wasmtime unicorn pyelftools capstone + - name: Install wabt (wat2wasm — required by the newly-wired oracles) + # #890: these oracles were never CI-run, so their host deps were never + # discovered. wat2wasm is absent on the runner and several fixtures + # build their .wasm from .wat at test time (the #850/#881 class). + run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends wabt - name: bulk-memory copy/fill numeric differential (#374) run: | ./target/debug/synth compile scripts/repro/bulk_memory_374_diff.wat -o /tmp/bmd.elf --target cortex-m7dp --all-exports --safety-bounds software @@ -2455,6 +2465,11 @@ jobs: python-version: "3.x" - name: Install emulation deps run: pip install wasmtime unicorn pyelftools capstone + - name: Install wabt (wat2wasm — required by the newly-wired oracles) + # #890: these oracles were never CI-run, so their host deps were never + # discovered. wat2wasm is absent on the runner and several fixtures + # build their .wasm from .wat at test time (the #850/#881 class). + run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends wabt - name: control_step RV32 correctness + ABI + shipped data (#223/#798) run: | ./target/debug/synth compile scripts/repro/control_step.wasm -b riscv -t rv32imac --all-exports --relocatable -o /tmp/cs_rv.o @@ -2528,6 +2543,11 @@ jobs: python-version: "3.x" - name: Install emulation deps run: pip install wasmtime unicorn pyelftools capstone + - name: Install wabt (wat2wasm — required by the newly-wired oracles) + # #890: these oracles were never CI-run, so their host deps were never + # discovered. wat2wasm is absent on the runner and several fixtures + # build their .wasm from .wat at test time (the #850/#881 class). + run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends wabt - name: WCET phase-2 const-loop bound soundness (#778) run: python scripts/repro/wcet_phase2_778_unicorn_soundness.py - name: WCET phase-3 inter-procedural composition soundness (#778) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7198a91b..68f5cdd3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -9,6 +9,63 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Added +- **#890 — the oracle-wiring gate: fix the factory, not the bugs.** + `scripts/repro/*.py` are synth's execution oracles, and **69 of 150 were + referenced by no workflow** — nothing ran them. v0.53 hand-wired three and the + unwired count still went *up*, because instances were fixed while the mechanism + that produces them was untouched. The defect was never "69 broken gates": many + are legitimately manual (a pinned vendor drop, real silicon, a toolchain CI + does not install). The defect is that **nothing distinguished "manual by + design" from "forgotten"**, so telling them apart meant reading all 150 — the + audit that kept rediscovering this one instance at a time. + + Every repro script now carries exactly one `# ci-status:` declaration — + `wired`, `manual () — reason`, or `unwired — reason` — and + `scripts/oracle_wiring_check.py` (a step of the already-**required** + `claim-check` job) fails the build when a script declares `wired` but no + workflow **step** runs it, when a `manual`/`unwired` declaration has no real + reason or an out-of-vocabulary category, or when a script declares nothing at + all. New oracles are forced to choose. "Runs it" is derived from the *parsed* + workflow (a step's `run:` body and its `with:`/`env:` values), not a raw grep — + a mention in a comment does not wire an oracle, and a gate satisfiable by prose + is the failure shape this one exists to reject. Rationale, the categorized + manual set, and the six-mutation red-first transcript (plus the real + `Claim Check` CI red): `scripts/repro/ORACLE_WIRING.md`. + +- **#890 — 63 forgotten oracles wired.** Each was verified green locally against + a freshly built synth before wiring, using the compile line from its own + documented `Run:` block; they run in four new sweep jobs (selector / memory / + rv32 / wcet) plus one step in the existing fact-spec job. Among what was *not* + being gated: the six `mem757_*` red-first reconstructions of gale's + wrong-segment miscompile (#757); every RV32 oracle for a regression gale found + on real silicon (#220, #226, #232, #317, #343); all four WCET soundness + cross-checks — the only thing that *executes* the fixtures and checks + `bound_cycles >= executed_instructions`, i.e. the evidence behind the + sound-WCET claim; and the #494 `rem_u` identity differential behind the + beat-clang headline. Final surface: **145 wired / 7 manual / 0 unwired**, + ratcheted in `claims.yaml` (`SYNTH-ORACLE-WIRING-890`) — the wired count is a + floor, manual a ceiling, and *unwired a ceiling of zero*, so new debt is a red + build rather than a silent backlog entry. + +### Fixed + +- **#890 — `sret_decide_differential.py` was a gate that could not fail.** It + printed `MISMATCH <-- BUG` and still exited 0. The verdict is now the exit + status (proved by mutation: flipping the `-35` expectation gives `rc=1`). + `base_cse`, `leaf_dead_frame`, `load_store_big_offset_382` and `uxth_fold` + hardcoded `./target/{debug,release}/synth`; all four now honour `$SYNTH` with + the same literal default. + +- **#890 — the gate's own CI step was vacuous, and a mutation caught it.** + `set -o pipefail` without `-e` means the shell's status is its *last* + command's: the inert-gate mutation greened the step while the gate printed + `FAIL` and exited 1. The step now sets `-euo pipefail` explicitly (rather than + leaning on Actions' default `bash -e`) and re-derives its verdict from the JSON + summary the gate wrote — non-empty script set, non-zero wired count, zero + `undeclared` / `wired_unreferenced` / `failures` — instead of trusting exit 0. + +### Added + - **VCR-DEC-001 increment 3 (#242): the graph-colouring allocator colours ACROSS CALLS.** Increment 2's second-largest decline bucket was `call` / `call-indirect` — 68 of the measured corpus — because a `bl` had no modeled