diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f2e22d7b..c61c6844 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -179,6 +179,47 @@ 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 -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 -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"] + 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, 0 inert.") + 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 +1058,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 +2216,343 @@ 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: 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 + 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: 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 + 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: 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 + 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: 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) + 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 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 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 new file mode 100644 index 00000000..81862fbf --- /dev/null +++ b/scripts/oracle_wiring_check.py @@ -0,0 +1,362 @@ +#!/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` 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 + 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 + +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 = { + "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 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, wf_raw = executable_surface(workflows) + + 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: + 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 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})") + 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 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/*")) + } + 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 " + 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())) + # 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 + + +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()) + ) + + summary["failures"] = len(fails) + + 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/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md new file mode 100644 index 00000000..8567875d --- /dev/null +++ b/scripts/repro/ORACLE_WIRING.md @@ -0,0 +1,214 @@ +# 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. + +"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 + 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 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 +no transcription drift between what was proved and what CI runs. + +``` +===== BASELINE ===== +STEP EXIT=0 +oracle-wiring gate is non-vacuous: it classified 152 scripts, 145 of them wired, +7 manual, 0 unwired-debt, 0 inert. + +===== 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 (wired | manual () — reason | unwired ... + +===== 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 +STEP runs it — the gate is INERT. Wire it in .github/workflows/, or dow... + +===== 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 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': ... + +===== M5: reference demoted to a COMMENT ===== +STEP EXIT=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 +``` + +**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 + +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`. 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/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/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/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/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/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/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/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/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/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_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_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_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/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/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/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_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/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/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/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_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/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/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/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/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/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_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_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_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_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_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_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_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/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/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_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_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/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/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_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/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/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/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/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/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_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_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_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_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/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/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_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/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("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/u64_unpack_differential.py b/scripts/repro/u64_unpack_differential.py index 259a4f89..95fb9d90 100644 --- a/scripts/repro/u64_unpack_differential.py +++ b/scripts/repro/u64_unpack_differential.py @@ -1,3 +1,4 @@ +# ci-status: wired import struct, sys import wasmtime from elftools.elf.elffile import ELFFile diff --git a/scripts/repro/u64_unpack_if_differential.py b/scripts/repro/u64_unpack_if_differential.py index dffcd8b7..def3ba1a 100755 --- a/scripts/repro/u64_unpack_if_differential.py +++ b/scripts/repro/u64_unpack_if_differential.py @@ -1,4 +1,5 @@ #!/usr/bin/env python3 +# ci-status: wired # #313 differential: wasmtime ground truth vs unicorn running synth's ARM for # the if-with-result variant of u64_unpack. The then-path must return its OWN # result (r>>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/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/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_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_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/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/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 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