From 473d7521bce5993365f2a5143356e33dde09a03e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:02:13 +0200 Subject: [PATCH 1/9] =?UTF-8?q?docs(#910):=20rivet=20=E2=80=94=20VG-009/VG?= =?UTF-8?q?-010,=20the=20two=20evidence-INSTRUMENT=20gaps?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Traceability leads the lane. VG-001..VG-008 all say "a property is not yet proven"; these two say something different in kind — an instrument REPORTS something other than what its name implies, and the measurement itself is the defect. VG-009 (#910): `Code Coverage` runs `cargo llvm-cov --workspace`, i.e. the Rust test suite. The execution differentials spawn the compiler as a separate, UNINSTRUMENTED process from different CI jobs, so every one of those executions is invisible to the percentage — it understates real testing AND cannot be read as completeness. Records the v0.54.0 measurement and the decline of #910 option 1 with its reason (instrumenting the binary changes the artifact under test; the differentials exist to execute the SHIPPED bytes). VG-010 (#910 F10): measured — 152 of the 160 workflow steps that run a scripts/repro/ oracle assert nothing beyond the process exit code. Not only the 63 wired by #890; the pre-existing hand-wired steps too. Exactly 8 assert a printed verdict or count. Both carry the RESOLUTION TAKEN so the artifact states the shipped decision, not just the complaint. --- artifacts/verification-gaps.yaml | 84 ++++++++++++++++++++++++++++++++ 1 file changed, 84 insertions(+) diff --git a/artifacts/verification-gaps.yaml b/artifacts/verification-gaps.yaml index 74aac21d..025cd2b9 100644 --- a/artifacts/verification-gaps.yaml +++ b/artifacts/verification-gaps.yaml @@ -203,3 +203,87 @@ artifacts: req-type: non-functional priority: should verification-track: kani + + # ========================================================================= + # VG-009 / VG-010 — the EVIDENCE-INSTRUMENT gaps (#910, #890 F10). + # + # These two are a different species from VG-001..VG-008. Those say "a + # property is not yet proven". These say "an instrument REPORTS something + # other than what its name implies" — the measurement itself is the defect. + # A green-but-meaningless number is worse than a red one, because it gets + # quoted; that is the #890 lesson wearing new clothes. + # ========================================================================= + - id: VG-009 + type: sys-verification + title: "Line coverage is blind to the execution differentials (scope mislabel)" + description: > + The `Code Coverage` CI job runs `cargo llvm-cov --workspace --lcov`, + which instruments and executes the RUST TEST SUITE only. This project's + strongest evidence is the execution differentials: Python harnesses in + scripts/repro/ that spawn the compiler as a SEPARATE, UNINSTRUMENTED + process (resolved from $SYNTH), in DIFFERENT CI jobs (the repro sweeps, + the trap-semantics oracle, the per-issue oracles). An uninstrumented + subprocess emits no profile data, so every one of those executions is + invisible to the percentage. + Consequence, measured at v0.54.0: synth-backend-aarch64/src/backend.rs + 41.6 %, synth-backend-riscv/src/backend.rs 43.7 %, + instruction_selector.rs 42.7 % (92 of 260 functions "never executed") — + while aarch64/selector.rs reads 89.4 %. backend.rs is largely ELF + emission, exercised end-to-end constantly through the invisible path. + The number therefore UNDERSTATES real testing, and for the same reason + cannot be read as a completeness measure: it cannot say what the + differentials do not reach. + RESOLUTION TAKEN (v0.55, #910 options 2+3): the job is renamed to state + its scope, the instrument's blindness is documented at the job and at + every place the percentage is quoted, and the differential population is + reported SEPARATELY as an executed-check count rather than folded into + one percentage. Option 1 (point the differentials at an instrumented + binary) was DECLINED: it changes the artifact under test — the + differentials exist to execute the SHIPPED bytes — and it would buy + precision on an axis that is still the wrong completeness instrument. + status: implemented + tags: [verification-gap, evidence-instrument, coverage, honesty] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + fields: + req-type: non-functional + priority: must + verification-track: measurement + issue: "#910" + + - id: VG-010 + type: sys-verification + title: "Oracle CI steps asserted exit status, not that any check ran" + description: > + #890 wired 63 forgotten execution oracles into CI. Measured on that + result: 152 of the 160 workflow steps that run a scripts/repro/ oracle + assert NOTHING BEYOND THE PROCESS EXIT CODE — not only the 63 newly + wired ones, the pre-existing hand-wired steps too; exactly 8 steps + asserted a printed verdict or count. An oracle that exits 0 having + executed zero comparisons is indistinguishable from one that executed + hundreds, which is the inert-gate failure #890 exists to reject, + one level down: the gate is wired, but what it attests is unstated. + RESOLUTION TAKEN (v0.55): oracle steps run through scripts/oracle_run.py, + an in-process driver that counts REAL emulator entries and wasmtime + invocations, asserts a declared per-script floor (`# ci-checks:` header, + the same locality argument as `# ci-status:`), and records the count. + Scripts that execute nothing emulatable declare a stdout-pattern floor + instead; the residue that can bind to neither is enumerated in + docs/development/ORACLE_WIRING.md rather than covered by a uniform claim. + status: implemented + tags: [verification-gap, evidence-instrument, oracle, honesty] + links: + - type: derives-from + target: BR-001 + - type: refines + target: NFR-002 + - type: traces-to + target: H-CODE-1 + fields: + req-type: non-functional + priority: must + verification-track: measurement + issue: "#910 (F10)" From 5e58cb1861b488be49a1afc5c098d39866cfdbb1 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:03:50 +0200 Subject: [PATCH 2/9] docs(#910): the coverage number now says what it measures (option 2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Code Coverage` -> `Rust-test Line Coverage (unit + integration only)`. The old name implied whole-system coverage; the job runs `cargo llvm-cov --workspace`, i.e. one population — the Rust test suite, in-process. The scope note travels WITH the number in three places, because a caveat that lives somewhere else does not survive being quoted: * the job body, for whoever edits it; * `$GITHUB_STEP_SUMMARY`, so reading the percentage and reading the caveat are the same act; * the README, under the badge. All three say the same two things: the number UNDERSTATES the testing that exists (the differentials run an uninstrumented subprocess from other jobs, so `backend.rs` reads ~42 % while being exercised end-to-end by nearly every differential), and it is NOT a completeness measure. Verified before renaming that `Code Coverage` is NOT among main's 9 required status checks — renaming a required context deadlocks every merge until branch protection is updated, which is a coordinator decision, not a lane one. gh api repos/pulseengine/synth/branches/main/protection/required_status_checks --jq '.contexts' ["Format","Clippy","Test","Z3 Verification","Claim Check", "Version Pin Sweep","Bazel Build & Proofs","Kani Verification", "Rivet Validation"] No emitted byte moves; 37/37 claims still hold. --- .github/workflows/ci.yml | 44 +++++++++++++++++++++++++++++++++++++++- README.md | 4 +++- 2 files changed, 46 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b6069e16..039c39aa 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -276,7 +276,26 @@ jobs: run: cargo test -p synth-verify --test comprehensive_verification --features z3-solver,arm coverage: - name: Code Coverage + # RENAMED from "Code Coverage" (#910). The old name implied whole-system + # coverage; the job measures ONE population — the Rust test suite, in-process, + # under llvm-cov instrumentation. + # + # What it CANNOT see, structurally: the execution differentials. Those spawn + # `$SYNTH` as a SEPARATE, UNINSTRUMENTED process, from OTHER jobs entirely + # (`repro sweep-*`, `trap-semantics oracle`, the per-issue oracles). An + # uninstrumented subprocess emits no profile data, so none of that execution + # reaches this percentage. That is why backend.rs — almost pure ELF emission, + # exercised end-to-end on every differential — reads ~42 % here. + # + # Consequence, stated so nobody has to rediscover it: this number UNDERSTATES + # the testing that exists, and it is NOT a completeness measure. The + # differential population is reported separately and in its own unit — + # asserted executed checks, see scripts/oracle_run.py and the + # `oracle-evidence-ledger` job. Do not add them together. + # + # Not a required status check on `main` (verified before renaming: renaming a + # required context deadlocks every merge until protection is updated). + name: Rust-test Line Coverage (unit + integration only) needs: [test] runs-on: [self-hosted, linux, x64, rust-cpu] steps: @@ -303,6 +322,29 @@ jobs: cargo llvm-cov --workspace --lcov --output-path lcov.info \ --exclude synth-qemu \ --exclude synth-backend-awsm --exclude synth-backend-wasker + - name: Say what this number does and does not measure (#910) + # The scope note travels WITH the number. Reading the percentage off the + # job summary and reading this are the same act, which is the only way a + # caveat survives being quoted. + run: | + set -euo pipefail + test -s lcov.info + { + echo "### Rust-test line coverage — SCOPE (#910)" + echo + echo "Measures: \`cargo llvm-cov --workspace\` — the **Rust test suite**, in-process." + echo + echo "Does **not** measure: the execution differentials" + echo "(\`scripts/repro/*.py\`). They spawn \`\$SYNTH\` as a separate," + echo "UNINSTRUMENTED process, from other jobs — no profile data reaches" + echo "this figure. \`backend.rs\` reads ~42 % here while being exercised" + echo "end-to-end by nearly every differential." + echo + echo "So this number **understates** the testing that exists, and is" + echo "**not** a completeness measure. The differential population is" + echo "reported separately, in executed checks, by the" + echo "\`oracle evidence ledger\` job. **Do not add them together.**" + } >> "$GITHUB_STEP_SUMMARY" - name: Upload to Codecov uses: codecov/codecov-action@v7 with: diff --git a/README.md b/README.md index 695b46a3..84a5325c 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@   [![CI](https://github.com/pulseengine/synth/actions/workflows/ci.yml/badge.svg)](https://github.com/pulseengine/synth/actions/workflows/ci.yml) -[![codecov](https://codecov.io/gh/pulseengine/synth/graph/badge.svg)](https://codecov.io/gh/pulseengine/synth) +[![Rust-test line coverage](https://codecov.io/gh/pulseengine/synth/graph/badge.svg)](https://codecov.io/gh/pulseengine/synth) ![Rust](https://img.shields.io/badge/Rust-CE422B?style=flat-square&logo=rust&logoColor=white&labelColor=1a1b27) ![WebAssembly](https://img.shields.io/badge/WebAssembly-654FF0?style=flat-square&logo=webassembly&logoColor=white&labelColor=1a1b27) ![License: Apache-2.0](https://img.shields.io/badge/License-Apache--2.0-blue?style=flat-square&labelColor=1a1b27) @@ -18,6 +18,8 @@ Badge numbers are machine-derived into [`artifacts/status.json`](artifacts/status.json) and CI-staleness-gated — never hand-typed. +The coverage badge is Rust-test line coverage only — it cannot see the execution differentials, which run the compiler as a separate uninstrumented process from other CI jobs. It understates the testing that exists and is not a completeness measure; the differential population is counted separately in executed checks (#910). +  
From b2d274b21b2b91570a4255ca9aef60933b5f2181 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:33:26 +0200 Subject: [PATCH 3/9] feat(#910 F10): oracle steps assert EXECUTION, not exit status MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Measured first, because the premise was understated: not 63 but **152 of the 160 workflow steps** that run a `scripts/repro/` oracle asserted nothing beyond the process exit code. Exactly 8 asserted a printed verdict or count — and the pre-#890 hand-wired steps are mostly in the bare 152 too. Exit 0 does not distinguish "emulated 240 vectors, all bit-identical" from "the fixture list came back empty, printed PASS". That is #890's inert gate one level down: wired, but what it attests is unstated. MECHANISM — `scripts/oracle_run.py`, an in-process driver (runpy) that wraps three entry points and counts them: unicorn.Uc.emu_start -> emulations wasmtime.Func.__call__ -> wasmtime_calls subprocess `synth … compile …` -> compiles The count comes from the emulator, not from the harness's own bookkeeping, so a comparison loop that never runs cannot fake it. Chosen over 152 bespoke greps because it is uniform and needs no edit to any harness; chosen over #910 option 1 (instrumenting the binary) because that changes the artifact under test. DECLARATION — one `# ci-checks:` header per oracle, same locality argument as `# ci-status:`: the floor lives in the file it describes and cannot outlive it. Floors are `>=`, never equality, so adding a fixture cannot redden a step. CALIBRATION, not assumption — every floor below is a MEASURED value, obtained by executing each CI oracle step VERBATIM (parsed out of ci.yml, so there is no transcription drift) with the invocation routed through the driver. Four oracles that self-report a check count agree with the driver 1:1: gpio_thin_846 prints `#846 CHECKS=75/75` driver 75 aarch64_call_indirect_851 prints `35 checks (23 trap, 12 value)` driver 35 aarch64_globals_851 prints `17 checks` driver 17 aarch64_float_completion_851 (the "662 float-boundary checks") driver 662 150 wired oracles now declare: emulations 133 scripts 294,914 emulator entries asserted stdout 7 scripts 458 printed counts asserted compiles 9 scripts 43 compilations asserted none 1 script aarch64_matrix.sh — a POSIX shell oracle the in-process driver cannot instrument; its step already carries its own >= 32 accepted-ops assertion The mode is the STRONGEST that holds on EVERY invocation: several oracles run twice, once executing and once on a decline / byte-identity leg that executes nothing by design, and a floor that only holds for the good leg is not a floor. The weaker floor loses nothing — every counter is still measured and recorded. 159 CI step lines routed. The one deliberately NOT routed is the #275 RED non-vacuity step (`! python …`), which inverts its verdict: routing it would file a below-floor record for a run that is SUPPOSED to fail. No emitted byte moves; no existing assertion removed. --- .github/workflows/ci.yml | 318 ++++++------- ci851.txt | 4 + ga_join.out | 72 +++ globals851.txt | 4 + gpio846.out | 10 + scripts/oracle_run.py | 432 ++++++++++++++++++ scripts/repro/a32_i64_615_differential.py | 1 + scripts/repro/aarch64_add_538_differential.py | 1 + .../repro/aarch64_bounds_865_differential.py | 1 + .../aarch64_call_indirect_851_differential.py | 1 + scripts/repro/aarch64_calls_851.py | 1 + scripts/repro/aarch64_cf_538_differential.py | 1 + .../aarch64_ctrlflow_851_differential.py | 1 + .../repro/aarch64_divrem_851_differential.py | 1 + ...rch64_float_completion_851_differential.py | 1 + .../repro/aarch64_globals_851_differential.py | 1 + .../repro/aarch64_locals_851_differential.py | 1 + scripts/repro/aarch64_m2_538_differential.py | 1 + scripts/repro/aarch64_m2_decline_538.py | 1 + .../aarch64_m3_floats_538_differential.py | 1 + ...arch64_m4_trunc_minmax_538_differential.py | 1 + scripts/repro/aarch64_matrix.sh | 1 + scripts/repro/aarch64_mem_851_differential.py | 1 + .../repro/aarch64_surface_851_differential.py | 1 + scripts/repro/add_imm_large_differential.py | 1 + scripts/repro/addw_offset_681_differential.py | 1 + scripts/repro/base_cse_differential.py | 1 + scripts/repro/block_brif_483_differential.py | 1 + scripts/repro/br_table_507_differential.py | 1 + .../repro/br_table_value_509_differential.py | 1 + scripts/repro/brif_outer_740_differential.py | 1 + .../bulk_local_clobber_677_differential.py | 1 + scripts/repro/bulk_mask_679_differential.py | 1 + scripts/repro/bulk_memory_374_differential.py | 1 + .../repro/cabi_arena_bind_418_differential.py | 1 + scripts/repro/call_5args_differential.py | 1 + scripts/repro/call_6_7args_differential.py | 1 + ...indirect_275_selfcontained_differential.py | 1 + ...75_selfcontained_execution_differential.py | 1 + .../repro/call_indirect_594_differential.py | 1 + .../repro/call_indirect_597_differential.py | 1 + .../repro/call_indirect_642_differential.py | 1 + .../repro/call_indirect_650_differential.py | 1 + .../repro/call_indirect_664_differential.py | 1 + .../repro/call_indirect_676_differential.py | 1 + .../repro/callee_saved_490_differential.py | 1 + scripts/repro/cf_shapes_500_differential.py | 1 + .../repro/cmp_select_two_move_differential.py | 1 + .../const_addr_fold_riscv_differential.py | 1 + scripts/repro/const_body_791_differential.py | 1 + scripts/repro/const_cse_differential.py | 1 + scripts/repro/control_step_differential.py | 1 + .../repro/control_step_riscv_differential.py | 1 + .../controller_step_riscv_differential.py | 1 + scripts/repro/div_const_differential.py | 1 + scripts/repro/dyn_table_359_differential.py | 1 + .../f32_mem_trunc_708_709_differential.py | 1 + scripts/repro/f32_ops_719_differential.py | 1 + scripts/repro/f32_vfp_619_differential.py | 1 + scripts/repro/f64_369_differential.py | 1 + .../fact_spec_bounds_494_differential.py | 1 + .../repro/fact_spec_clamp_494_differential.py | 1 + .../repro/fact_spec_div_494_differential.py | 1 + .../repro/fact_spec_mask_494_differential.py | 1 + .../repro/fact_spec_rem_494_differential.py | 1 + .../fact_spec_select_494_differential.py | 1 + .../repro/filter_axis_riscv_differential.py | 1 + scripts/repro/flight_seam_differential.py | 1 + .../float_select_return_782_differential.py | 1 + scripts/repro/frame_slot_dce_differential.py | 1 + .../framebacking_i64param_837_differential.py | 1 + scripts/repro/gpio_thin_846_differential.py | 1 + .../repro/gust_spill_fwd_390_differential.py | 1 + .../repro/high_pressure_i32_differential.py | 1 + .../repro/high_pressure_i64_differential.py | 1 + .../repro/i32_shift_mask_682_differential.py | 1 + .../repro/i64_divs_317_riscv_differential.py | 1 + .../i64_divs_overflow_633_differential.py | 1 + .../repro/i64_float_conv_869_differential.py | 1 + .../repro/i64_global_init_649_differential.py | 1 + scripts/repro/i64_globals_643_differential.py | 1 + .../i64_large_offset_382_differential.py | 1 + .../i64_pair_exhaust_587_differential.py | 1 + scripts/repro/i64_param_518_differential.py | 1 + scripts/repro/i64_param_518_riscv_loudskip.py | 1 + scripts/repro/i64_popcnt_632_differential.py | 1 + scripts/repro/i64_rot_div_610_differential.py | 1 + scripts/repro/i64_shr_599_differential.py | 1 + .../repro/i64_spill_pool_587_differential.py | 1 + .../repro/i64_stack_param_503_differential.py | 1 + .../if_else_result_343_riscv_differential.py | 1 + scripts/repro/leaf_dead_frame_differential.py | 1 + .../load_store_big_offset_382_differential.py | 1 + .../repro/local_promote_i32_differential.py | 1 + .../loop_param_bound_663_differential.py | 1 + .../mask_bounds_655_riscv_differential.py | 1 + scripts/repro/mem757_gale_differential.py | 1 + .../mem757_inlined_memmove_differential.py | 1 + .../mem757_low_const_copy_differential.py | 1 + .../mem757_memcopy_static_src_differential.py | 1 + .../mem757_memmove_param_differential.py | 1 + .../mem757_pressure_chunks_differential.py | 1 + .../mem757_ptr_base_copy_differential.py | 1 + .../mem757_rawvec_memcopy_differential.py | 1 + .../mem761_linmem_r9_overlap_differential.py | 1 + scripts/repro/mem_grow_539_differential.py | 1 + .../repro/multi_memory_406_differential.py | 1 + .../multi_segment_static_data_differential.py | 1 + scripts/repro/multi_sp_707_differential.py | 1 + scripts/repro/mutex_pressure_differential.py | 1 + ...ative_pointer_shadow_stack_differential.py | 1 + .../native_pointer_static_downshift_678.py | 1 + scripts/repro/postex_cycle_proxy.py | 1 + scripts/repro/postlink_359_oracle.py | 1 + scripts/repro/r12_spill_496_differential.py | 1 + ...allgraph_275_selfcontained_differential.py | 1 + ...efore_write_local_zeroinit_differential.py | 1 + scripts/repro/rem_s_666_differential.py | 1 + .../riscv_extern_call_871_differential.py | 1 + .../repro/rv32_br_table_882_differential.py | 1 + .../rv32_cmp_select_472_riscv_differential.py | 1 + .../repro/rv32_data_798_boot_differential.py | 1 + scripts/repro/rv32_label_882_differential.py | 1 + ..._local_promotion_472_riscv_differential.py | 1 + .../rv32_mem_size_grow_242_differential.py | 1 + .../repro/safety_bounds_377_differential.py | 1 + .../self_contained_data_758_differential.py | 1 + .../repro/shift_fold_riscv_differential.py | 1 + .../signed_div_const_riscv_differential.py | 1 + scripts/repro/spill_frame_499_differential.py | 1 + .../spill_on_exhaust_242_differential.py | 1 + scripts/repro/spill_rung_581_differential.py | 1 + scripts/repro/sret_decide_differential.py | 1 + scripts/repro/stack_args_503_differential.py | 1 + .../repro/stack_layout_687_differential.py | 1 + .../repro/static_above_sp_739_differential.py | 1 + scripts/repro/trunc_sat_782_differential.py | 1 + scripts/repro/u64_unpack_differential.py | 1 + scripts/repro/u64_unpack_if_differential.py | 1 + .../repro/u64_unpack_riscv_differential.py | 1 + scripts/repro/unreachable_665_differential.py | 1 + scripts/repro/uxth_fold_differential.py | 1 + .../vcr_dec_001_graph_alloc_differential.py | 1 + ...c_001_join_alloc_execution_differential.py | 1 + scripts/repro/vcr_ra_003_phase2_join_call.py | 1 + .../repro/vcr_ra_003_rv32_alloc_validator.py | 1 + .../vcr_ver_004_instrument_independence.py | 1 + .../repro/vcr_ver_004_shipping_path_audit.py | 1 + scripts/repro/vfp_spill_881_differential.py | 1 + .../volatile_segment_543_differential.py | 1 + .../wcet_phase2_778_unicorn_soundness.py | 1 + .../wcet_phase3_778_compose_soundness.py | 1 + .../wcet_phase4_49_recursion_soundness.py | 1 + .../wcet_phase5_778_masked_loop_soundness.py | 1 + scripts/repro/wide_static_746_differential.py | 1 + .../wide_static_copy_757_differential.py | 1 + vcr_ver_004.out | 1 + vcr_ver_004_ship.out | 12 + vfp881.out | 3 + 159 files changed, 847 insertions(+), 159 deletions(-) create mode 100644 ci851.txt create mode 100644 ga_join.out create mode 100644 globals851.txt create mode 100644 gpio846.out create mode 100644 scripts/oracle_run.py create mode 100644 vcr_ver_004.out create mode 100644 vcr_ver_004_ship.out create mode 100644 vfp881.out diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 039c39aa..e941bb50 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -471,7 +471,7 @@ jobs: - name: Install emulation deps run: pip install wasmtime unicorn pyelftools - name: Run two-move execution oracle - run: python scripts/repro/cmp_select_two_move_differential.py + run: python scripts/oracle_run.py scripts/repro/cmp_select_two_move_differential.py provenance-gate: name: synth-provenance-v1 reconciliation gate (#396) @@ -542,31 +542,31 @@ jobs: - name: Install emulation deps run: pip install wasmtime unicorn pyelftools - name: Run m1 integer-core execution oracle - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_add_538_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_add_538_differential.py - name: Run m2 broadened i32+i64 ALU execution oracle - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m2_538_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_m2_538_differential.py - name: Run m3 scalar-float execution oracle - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m3_floats_538_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_m3_floats_538_differential.py - name: Run m4 trunc boundary-table + min/max NaN/±0 execution oracle - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m4_trunc_minmax_538_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_m4_trunc_minmax_538_differential.py - name: Run cf void-block br/br_if execution oracle (both branch edges) - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_cf_538_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_cf_538_differential.py - name: Run #851 linear-memory load/store execution oracle - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_mem_851_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_mem_851_differential.py - name: Run #851 div/rem trap + popcnt + reinterpret execution oracle (÷0 + INT_MIN/-1) - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_divrem_851_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_divrem_851_differential.py - name: Run #851 non-param locals execution oracle - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_locals_851_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_locals_851_differential.py - name: Run #851 control-flow (if/else + loop back-edge + return) execution oracle - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_ctrlflow_851_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_ctrlflow_851_differential.py - name: Run #865 linear-memory BOUNDS oracle (OOB traps + modes differ + mask/mpu hard-error) - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_bounds_865_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_bounds_865_differential.py - name: Run #851 v0.53 op-surface oracle (select x4 types + wrap/extends + drop/nop + memory.size/grow) # The VCR-SEL-005 third-backend closes: select (CSEL/FCSEL) incl. # NaN/-0 carry, wrap/extends with POISONED upper argument bits (the # AAPCS64 x-view hazard), drop/nop, fixed-memory size/grow parity # against a min=max module (growth failure is spec-forced there). - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_surface_851_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_surface_851_differential.py - name: Run #851 lane L3 GLOBALS execution oracle (emitted .data region + persistence) # synth EMITS the globals region (a `.data` image carrying the decoded # initializers) and reaches it `adrp`+`add :lo12:` — no base register, @@ -580,7 +580,7 @@ jobs: run: | set -euo pipefail SYNTH=./target/debug/synth \ - python scripts/repro/aarch64_globals_851_differential.py | tee globals851.txt + python scripts/oracle_run.py scripts/repro/aarch64_globals_851_differential.py | tee globals851.txt grep -Eq '^[1-9][0-9]* checks across [1-9][0-9]* exported' globals851.txt grep -q '^RESULT: PASS' globals851.txt - name: Run #851 lane L3 CALL_INDIRECT execution oracle (§4.4.8 OOB + null + type traps) @@ -595,7 +595,7 @@ jobs: run: | set -euo pipefail SYNTH=./target/debug/synth \ - python scripts/repro/aarch64_call_indirect_851_differential.py | tee ci851.txt + python scripts/oracle_run.py scripts/repro/aarch64_call_indirect_851_differential.py | tee ci851.txt grep -Eq '^[1-9][0-9]* checks \([1-9][0-9]* trap, [1-9][0-9]* value\)' ci851.txt grep -q '^RESULT: PASS' ci851.txt - name: Run v0.54 L2 float-completion oracle (#851 rounding / i64 converts / GUARDED i64 trunc / FP mem) @@ -621,7 +621,7 @@ jobs: # entire purpose — must go RED. run: | set -euo pipefail - SYNTH=./target/debug/synth python scripts/repro/aarch64_float_completion_851_differential.py \ + SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_float_completion_851_differential.py \ | tee /tmp/a64_floatdiff.log grep -q '^RESULT: PASS' /tmp/a64_floatdiff.log grep -Eq '^[0-9]+ wasmtime cases \([0-9]+ trap cases\)' /tmp/a64_floatdiff.log @@ -631,7 +631,7 @@ jobs: [ "$n" -ge 300 ] [ "$t" -ge 40 ] - name: Run decline-matrix honesty oracle - run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m2_decline_538.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_m2_decline_538.py aarch64-native-matrix: name: aarch64 native execution matrix (gale #851 acceptance gate) @@ -698,7 +698,7 @@ jobs: run: | SYNTH=./target/debug/synth \ WASMTOOLS=wasm-tools WASMTIME=wasmtime \ - python scripts/repro/aarch64_calls_851.py + python scripts/oracle_run.py scripts/repro/aarch64_calls_851.py trap-semantics-oracle: name: trap-semantics oracle (#665 unreachable + #666 rem_s) @@ -739,19 +739,19 @@ jobs: # vacuous, so install the linker rather than weaken the check. run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends binutils-arm-none-eabi - name: Run unreachable trap oracle (#665, thumb2 + rv32) - run: SYNTH=./target/debug/synth python scripts/repro/unreachable_665_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/unreachable_665_differential.py - name: Run rem_s trap-table oracle (#666, rv32) - run: SYNTH=./target/debug/synth python scripts/repro/rem_s_666_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/rem_s_666_differential.py - name: Run i32 shift-mask oracle (#682) - run: SYNTH=./target/debug/synth python scripts/repro/i32_shift_mask_682_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/i32_shift_mask_682_differential.py - name: Run ADDW static-offset oracle (#681, incl. software-bounds bypass) - run: SYNTH=./target/debug/synth python scripts/repro/addw_offset_681_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/addw_offset_681_differential.py # #686: the same oracle under the mask-elision lever (opt-in, # SYNTH_SHIFT_MASK_ELIDE=1) — const amounts fold to the immediate form # mod 32, unproven amounts keep the mask; the >= 32 rows pin that the # elision never fires unsoundly (red-tested at land time). - name: Run i32 shift-mask oracle with mask elision ON (#686) - run: SYNTH_SHIFT_MASK_ELIDE=1 SYNTH=./target/debug/synth python scripts/repro/i32_shift_mask_682_differential.py + run: SYNTH_SHIFT_MASK_ELIDE=1 SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/i32_shift_mask_682_differential.py # #846/#879: gale's REAL gpio-thin driver (pinned loom.wasm, never a # synthetic) under the default-ON mask elision — BOTH halves of the # v0.50.1 headline claim: (a) .text shrinks and the redundant mod-32 @@ -764,7 +764,7 @@ jobs: - name: Run gpio-thin size + mmio execution oracle (#846/#879, cortex-m3) run: | set -euo pipefail - SYNTH=./target/debug/synth python scripts/repro/gpio_thin_846_differential.py | tee gpio846.out + SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/gpio_thin_846_differential.py | tee gpio846.out grep -q "^#846 CHECKS=75/75" gpio846.out # #752: the software bounds guard must trap the top-of-address-space # wraparound class — the retired shape ADD-computed the end address @@ -773,11 +773,11 @@ jobs: # 19 vectors (in-bounds, exact-boundary, first-OOB, far-OOB, and six # #752 top-of-space rows) x BOTH codegen paths, wasmtime ground truth. - name: Run software-bounds wraparound oracle (#752/#377, thumb2 both paths) - run: SYNTH=./target/debug/synth python scripts/repro/safety_bounds_377_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/safety_bounds_377_differential.py - name: Run bulk-memory operand-clobber oracle (#677, thumb2) - run: SYNTH=./target/debug/synth python scripts/repro/bulk_local_clobber_677_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/bulk_local_clobber_677_differential.py - name: Run bulk-memory mask-coverage oracle (#679, thumb2) - run: SYNTH=./target/debug/synth python scripts/repro/bulk_mask_679_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/bulk_mask_679_differential.py # f32 hard-float SOUNDNESS oracles (GI-FPU-002). Dev-only before v0.40.0 — # the exact gap that let TWO silent miscompiles ship in v0.39.0 (trunc # saturation #709, and every compare returning 0 via a flag-clobber #712). @@ -785,7 +785,7 @@ jobs: # covers ALL SIX comparisons (#712: eq/ne/lt/gt/le/ge — the old harness # exercised only lt/gt, which is how eq/ne/le/ge stayed ungated). - name: Run f32 arith/compare execution oracle (#619/#712, cortex-m4f) - run: SYNTH=./target/debug/synth python scripts/repro/f32_vfp_619_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/f32_vfp_619_differential.py # #881: the VFP register-file spilling gate (GI-FPU-002 phase 1 S0..S15 + # phase 2 D0..D7) — the oracle behind the "falcon reaches the M7" claim, # so it must RUN, not merely exist. The lane wrote this differential and @@ -798,12 +798,12 @@ jobs: - name: Run VFP spill execution oracle (#881, cortex-m7dp) run: | set -euo pipefail - SYNTH=./target/debug/synth python scripts/repro/vfp_spill_881_differential.py | tee vfp881.out + SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/vfp_spill_881_differential.py | tee vfp881.out grep -q "^PASS: all 7 exports emitted (nm -> T)" vfp881.out grep -qE "^PASS: [1-9][0-9]+ execution rows bit-identical to wasmtime" vfp881.out # #708/#709: f32.load/reinterpret bit-casts + i32.trunc_f32 trap table. - name: Run f32 load/reinterpret + trunc-trap oracle (#708/#709, m4f) - run: SYNTH=./target/debug/synth python scripts/repro/f32_mem_trunc_708_709_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/f32_mem_trunc_708_709_differential.py # #719: the falcon f32 residual — f32.store, abs/neg/copysign, local.set/ # tee, and mixed f32/int AAPCS-VFP params — bit-exact vs wasmtime on m4f, # including the copysign ±0/NaN-sign/±inf sign edges. m3 honest-reject. @@ -811,7 +811,7 @@ jobs: # (spill/reload around the bl, non-vacuous — the callee clobbers S0/S1) # + float-signature-callee loud-decline pinned via symtab absence. - name: Run f32 store/abs/neg/copysign/local + mixed-param oracle (#719, m4f) - run: SYNTH=./target/debug/synth python scripts/repro/f32_ops_719_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/f32_ops_719_differential.py # #369 (GI-FPU-002 phase 2): the scalar f64 subset on cortex-m7dp — # const/promote_f32/arith/compare/load/store + f64-across-call, bit-exact # (NaN==NaN per Core §4.3.3) vs wasmtime under unicorn. Pins the @@ -820,7 +820,7 @@ jobs: # FPU), and the f64-ABI-boundary loud-declines (f64 params, f64-returning # calls). - name: Run f64 const/promote/arith/compare/mem + across-call oracle (#369, m7dp) - run: SYNTH=./target/debug/synth python scripts/repro/f64_369_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/f64_369_differential.py # #782a: the NONTRAPPING trunc_sat family (§4.3.2 — NaN→0, out-of-range # saturates, NEVER traps). Full boundary table (NaN/±inf/exact # INT_MIN-INT_MAX bounds/±0.5) vs wasmtime on BOTH prioritized backends: @@ -830,7 +830,7 @@ jobs: # forms must NOT skip, the ARM32 i64 forms MUST decline loudly by name. # This gate caught the optimized-path silent-NOP drop at land time. - name: Run trunc_sat boundary oracle (#782a, m7dp+m4f+aarch64) - run: SYNTH=./target/debug/synth python scripts/repro/trunc_sat_782_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/trunc_sat_782_differential.py # #869: the 64-bit integer<->float conversion family (gale's six + # the #756 i64.trunc_f64 pair) on cortex-m7dp — converts bit-exact # (incl. the round-to-odd double-rounding killers), the TRAPPING trunc @@ -840,7 +840,7 @@ jobs: # presence, and >=10k fixed-seed fuzz per direction. This gate caught # the range-realloc cross-barrier live-in miscompile at land time. - name: Run i64<->float conversion family oracle (#869, m7dp+m4f) - run: SYNTH=./target/debug/synth python scripts/repro/i64_float_conv_869_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/i64_float_conv_869_differential.py # #782(b): float `select` + explicit float `return` — the dominant class # on the real falcon fused core (12/26 skips incl. run-stabilization was # "an integer operation popped an f32"): select over two f32/f64 values @@ -853,7 +853,7 @@ jobs: # with no float op stayed on the float-naive optimized path: callers # marshal S0/S1, the body read R0/R1). - name: Run float select + explicit float return oracle (#782b, m7dp+m3) - run: SYNTH=./target/debug/synth python scripts/repro/float_select_return_782_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/float_select_return_782_differential.py # #739: static ABOVE sp_init under --shadow-stack-size — the sub-word # load/store arms previously BAKED the linmem offset as an un-relocated # MOVW/MOVT immediate (invisible to the #678 reloc-walking rebase AND to @@ -862,7 +862,7 @@ jobs: # static after the shrink must match wasmtime, with .bss/.data mapped at # SEPARATE bases so a baked absolute offset cannot accidentally resolve. - name: Run above-SP static shadow-stack-shrink oracle (#739, cortex-m3) - run: SYNTH=./target/debug/synth python scripts/repro/static_above_sp_739_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/static_above_sp_739_differential.py # #746 (the #739 residual): the i64/WIDE static-region arms — i64.load/ # i64.store pair accesses plus the i64 narrow loads/stores (load8/16/32, # store8/16/32) — get the #744 relocation treatment instead of the loud @@ -872,7 +872,7 @@ jobs: # (unicorn, .bss/.data at SEPARATE bases). RED on v0.42.0 (compile # declines, nothing to emit) -> GREEN with the relocated arms. - name: Run i64/wide above-SP static shrink oracle (#746, cortex-m3) - run: SYNTH=./target/debug/synth python scripts/repro/wide_static_746_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/wide_static_746_differential.py # #757: the multi-chunk static-copy CONTROL (gale's gust:os v0.4.0 # static-string copy shape). The triage claimed the #746 fix miscompiles # the head chunk's source ADDRESS relocation; six faithful shapes — incl. @@ -883,7 +883,7 @@ jobs: # the call relocation is a vacuous gate (the self-call masqueraded as a # miscompile). Guards that the call-crossing static copy stays correct. - name: Run multi-chunk static-copy control oracle (#757, cortex-m3) - run: SYNTH=./target/debug/synth python scripts/repro/wide_static_copy_757_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/wide_static_copy_757_differential.py # #757 v0.45 investigation: a RawVec-grow + memmove reconstruction of gale's # exact characterization (a >=9-byte static above wasm_data_base copied via a # bump-allocator memmove reached through a grow-call spill/reload). Seven such @@ -891,7 +891,7 @@ jobs: # NOT reproduce from the issue text; it needs gale's exact loom.wasm/os-tl-cm3.o. # Kept as a regression guard that the RawVec-grow copy path stays correct. - name: Run #757 RawVec-grow memmove reconstruction (cortex-m3) - run: SYNTH=./target/debug/synth python scripts/repro/mem757_rawvec_memcopy_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/mem757_rawvec_memcopy_differential.py # #740: the Thumb-2 B.W (T3) arm packed `halfword_offset >> 1`, # HALVING every conditional branch spanning > 254 bytes — gust_poll's # loop-head `br_if` to an outer block end landed mid-shape (spurious @@ -901,7 +901,7 @@ jobs: # must match wasmtime. Anti-vacuous: FAILS if `poll` stops containing a # 32-bit T3 conditional branch. RED on v0.42.0 (5/6 cases) -> GREEN. - name: Run wide-B.W branch-target oracle (#740, cortex-m4) - run: SYNTH=./target/debug/synth python scripts/repro/brif_outer_740_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/brif_outer_740_differential.py # #406 (VCR-MEM-002 phase 1): N wasm memories = N DISTINCT native base # regions. Memory 0 keeps the runtime R11 base; memory k > 0 is # addressed via its own __synth_wasm_data_ symbol at the base of the @@ -917,7 +917,7 @@ jobs: # wide accesses, non-const segment offsets) is the cargo test # crates/synth-cli/tests/multi_memory_406.rs. - name: Run multi-memory distinct-regions oracle (#406, cortex-m3) - run: SYNTH=./target/debug/synth python scripts/repro/multi_memory_406_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/multi_memory_406_differential.py # #758: the DEFAULT self-contained `--cortex-m` image (no --relocatable, # no native-pointer ABI) must SHIP active memory-0 data segments. Before # the fix `.linear_memory` was NoBits and the reset path had no copy loop, @@ -930,7 +930,7 @@ jobs: # offsets, a byte load mid-segment, an unaligned segment, and a zero-init # region (must stay 0). RED on v0.43.0 (4/5 read 0) -> GREEN. - name: Run self-contained data-segment oracle (#758, cortex-m3) - run: SYNTH=./target/debug/synth python scripts/repro/self_contained_data_758_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/self_contained_data_758_differential.py # #275: the DIRECT reachable call graph must EXECUTE on the self-contained # --cortex-m image (no --relocatable, no loader). Only `entry` is exported; # it calls two non-exported helpers, one of which calls a third — result @@ -941,7 +941,7 @@ jobs: # emit-all). The reachability walk is #235 (v0.11.28) — this is the missing # EXECUTION gate. - name: Run self-contained reachable-callgraph oracle (#275, cortex-m3, GREEN) - run: SYNTH=./target/debug/synth python scripts/repro/reachable_callgraph_275_selfcontained_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/reachable_callgraph_275_selfcontained_differential.py # Non-vacuity: a SEPARATE probe binary (feature `exports_only_275_probe`, # NEVER in the default/release build) exposes an `EXPORTS_ONLY_275=1` env # hatch that reverts to the pre-#235 exports-only drop (non-exported @@ -970,7 +970,7 @@ jobs: # truth is wasmtime. WIDENS coverage only — #757 stays OPEN (blocked on # the reporter's reduced module); a divergence here is a real find. - name: Run multi-segment static-data oracle (#406, self-contained + relocatable) - run: SYNTH=./target/debug/synth python scripts/repro/multi_segment_static_data_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/multi_segment_static_data_differential.py # #757: gale's EXACT fused os-tl node (loom.wasm) — the real miscompile that # 7 synthetic reconstructions could not reproduce (PR #772). Three active data # segments overlap at linmem 0x100000; the #354 reloc retargeting bound the @@ -980,7 +980,7 @@ jobs: # pre-fix binary (seg_0+8 reads 0x02, runtime owns 'g'); the permanent # regression fixture the synthetic shapes provably don't cover. - name: Run #757 gale fused-node static-data oracle (cortex-m3) - run: SYNTH=./target/debug/synth python scripts/repro/mem757_gale_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/mem757_gale_differential.py # VCR-VER-761: the self-contained --cortex-m full-page linmem view could # OVERLAP the R9 globals table at the top of SRAM — a store to the top of # the first page silently ALIASED a global slot (the R9 base was placed at @@ -991,9 +991,9 @@ jobs: # (R9 based at func_visible + memory_size, above the page ceiling). Runs # BOTH stack layouts (--stack-layout=low does NOT sidestep the overlap). - name: Run #761 linmem<->globals overlap oracle (cortex-m4, high layout) - run: SYNTH=./target/debug/synth python scripts/repro/mem761_linmem_r9_overlap_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/mem761_linmem_r9_overlap_differential.py - name: Run #761 linmem<->globals overlap oracle (cortex-m4, low layout) - run: EXTRA_SYNTH_FLAGS="--stack-layout low" SYNTH=./target/debug/synth python scripts/repro/mem761_linmem_r9_overlap_differential.py + run: EXTRA_SYNTH_FLAGS="--stack-layout low" SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/mem761_linmem_r9_overlap_differential.py # VCR-DEC-001 (epic #242, the North Star's first foothold): the # SYNTH_GRAPH_ALLOC whole-function graph-colouring allocator SPIKE. Gates # three properties on the ARM corpus: (1) flag-OFF ≡ the frozen goldens @@ -1011,7 +1011,7 @@ jobs: # increment 2's reach has regressed. Byte-only compare — needs pyelftools # ONLY (no unicorn/wasmtime). - name: Run VCR-DEC-001 graph-alloc spike differential (#242, thumb2) - run: python scripts/repro/vcr_dec_001_graph_alloc_differential.py ./target/debug/synth + run: python scripts/oracle_run.py scripts/repro/vcr_dec_001_graph_alloc_differential.py ./target/debug/synth # VCR-DEC-001 increments 2+3 (#242): EXECUTION-gate the DIVERGENT bytes the # join- and call-aware colouring now produces. This is NOT redundant with # the byte differential above: increment 1's correctness followed @@ -1048,7 +1048,7 @@ jobs: - name: Run VCR-DEC-001 join+call allocator execution differential (#242, thumb2) run: | set -euo pipefail - SYNTH=./target/debug/synth python scripts/repro/vcr_dec_001_join_alloc_execution_differential.py | tee ga_join.out + SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/vcr_dec_001_join_alloc_execution_differential.py | tee ga_join.out grep -q "^VCR-DEC-001-JOIN CHECKS=" ga_join.out awk -F'[=/ ]' '/^VCR-DEC-001-JOIN/ { if ($3+0 > 0 && $3 == $4 && $6+0 > 0 && $8+0 >= 4) ok = 1 } END { exit ok ? 0 : 1 }' ga_join.out # #798/#879: the RV32 active-data-segment FULL-BOOT oracle — found @@ -1062,7 +1062,7 @@ jobs: - name: Install clang + lld (riscv32 bare-metal, #798 boot oracle) run: sudo apt-get update && sudo apt-get install -y clang lld - name: Run RV32 data-segment full-boot oracle (#798, rv32imac) - run: SYNTH=./target/debug/synth python scripts/repro/rv32_data_798_boot_differential.py + run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/rv32_data_798_boot_differential.py instrument-independence-oracle: name: VCR-VER-004 instrument independence (#242, v0.53's mutation re-run) @@ -1121,7 +1121,7 @@ jobs: - name: Audit the SHIPPING allocator against the ABI contract (#242) run: | set -euo pipefail - SYNTH=./target/debug/synth python scripts/repro/vcr_ver_004_shipping_path_audit.py | tee vcr_ver_004_ship.out + SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/vcr_ver_004_shipping_path_audit.py | tee vcr_ver_004_ship.out grep -q "^VCR-VER-004-SHIPPING .* VIOLATED=0 " vcr_ver_004_ship.out test "$(grep -c '^ Holds ' vcr_ver_004_ship.out)" -eq 1 # The grep asserts the machine-readable 4/4 AND a non-zero OK count (#890): @@ -1130,7 +1130,7 @@ jobs: - name: Re-run the v0.53 mutation against all three instruments (#242) run: | set -euo pipefail - python scripts/repro/vcr_ver_004_instrument_independence.py | tee vcr_ver_004.out + python scripts/oracle_run.py scripts/repro/vcr_ver_004_instrument_independence.py | tee vcr_ver_004.out grep -q "^VCR-VER-004-INDEPENDENCE ASSERTIONS=4/4$" vcr_ver_004.out test "$(grep -c '^OK ' vcr_ver_004.out)" -eq 5 - name: Assert the tree was restored (the mutation must never persist) @@ -1179,10 +1179,10 @@ jobs: - name: Install emulation deps run: pip install wasmtime unicorn pyelftools - name: Run in-bounds differential (proven bound) - run: python scripts/repro/fact_spec_clamp_494_differential.py + run: python scripts/oracle_run.py scripts/repro/fact_spec_clamp_494_differential.py - name: Run wrong-bound loud-decline path run: > - python scripts/repro/fact_spec_clamp_494_differential.py + python scripts/oracle_run.py scripts/repro/fact_spec_clamp_494_differential.py --fact-lo 0 --fact-hi 4000 --expect-decline # #494 phase 2b — divisor-nonzero: in-bounds div/rem differential # (specialized ≡ wasmtime ≡ unspecialized over the proven divisor bound, @@ -1191,21 +1191,21 @@ jobs: # demonstration (the lever exists in debug builds only — CI's synth is # a debug build). - name: Run divisor-nonzero in-bounds differential (green) - run: python scripts/repro/fact_spec_div_494_differential.py + run: python scripts/oracle_run.py scripts/repro/fact_spec_div_494_differential.py - name: Run divisor-including-zero loud-decline path - run: python scripts/repro/fact_spec_div_494_differential.py --expect-decline + run: python scripts/oracle_run.py scripts/repro/fact_spec_div_494_differential.py --expect-decline - name: Run RED force-admit divergence demonstration - run: python scripts/repro/fact_spec_div_494_differential.py --force-admit + run: python scripts/oracle_run.py scripts/repro/fact_spec_div_494_differential.py --force-admit # #494 phase 3 — branchless select-collapse: the sibling of the Phase-2 # if-elision on the shape LLVM actually emits (min/max clamp via select). # In-bounds differential (specialized ≡ wasmtime ≡ unspecialized over the # proven bound; 2 collapses + gust_mix 50 B -> 14 B shrink required) and # the wrong-bound loud-decline byte-identity leg. - name: Run select-collapse in-bounds differential (proven bound) - run: python scripts/repro/fact_spec_select_494_differential.py + run: python scripts/oracle_run.py scripts/repro/fact_spec_select_494_differential.py - name: Run select-collapse wrong-bound loud-decline path run: > - python scripts/repro/fact_spec_select_494_differential.py + python scripts/oracle_run.py scripts/repro/fact_spec_select_494_differential.py --fact-lo 0 --fact-hi 4000 --expect-decline # #494 phase 3+ — redundant-mask (narrowing) elision: a proven-narrow # value makes an `i32.and` mask the identity, so it is deleted. On the @@ -1216,10 +1216,10 @@ jobs: # 2 elisions + a required shrink) and the wrong-bound loud-decline # byte-identity leg (bound [0,4095] makes `x & 0x7FF != x` Sat). - name: Run mask-elision in-bounds differential (proven bound) - run: python scripts/repro/fact_spec_mask_494_differential.py + run: python scripts/oracle_run.py scripts/repro/fact_spec_mask_494_differential.py - name: Run mask-elision wrong-bound loud-decline path run: > - python scripts/repro/fact_spec_mask_494_differential.py + python scripts/oracle_run.py scripts/repro/fact_spec_mask_494_differential.py --fact-lo 0 --fact-hi 4095 --expect-decline # #494 bounds-elision × #390 guard_bool — the `--safety-bounds software` # memory bounds guard falls to a per-site certificate: @@ -1234,11 +1234,11 @@ jobs: - name: Run bounds-elision gates (#494 bounds byte evidence) run: cargo test -p synth-cli --features verify --test fact_spec_bounds_494 - name: Run bounds-elision in-bounds differential (green) - run: python scripts/repro/fact_spec_bounds_494_differential.py + run: python scripts/oracle_run.py scripts/repro/fact_spec_bounds_494_differential.py - name: Run bounds-including-OOB loud-decline path - run: python scripts/repro/fact_spec_bounds_494_differential.py --expect-decline + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 @@ -1247,7 +1247,7 @@ jobs: - 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 + run: python scripts/oracle_run.py scripts/repro/fact_spec_rem_494_differential.py rv32-shift-fold-oracle: name: rv32 immediate-shift-fold execution oracle @@ -1282,7 +1282,7 @@ jobs: - name: Run RV32 shift-fold execution oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/shift_fold_riscv_differential.py + run: python scripts/oracle_run.py scripts/repro/shift_fold_riscv_differential.py rv32-const-addr-fold-oracle: name: rv32 const-address-fold execution oracle @@ -1316,7 +1316,7 @@ jobs: - name: Run RV32 const-address-fold execution oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/const_addr_fold_riscv_differential.py + run: python scripts/oracle_run.py scripts/repro/const_addr_fold_riscv_differential.py rv32-br-table-oracle: name: rv32 br_table execution oracle (#882) @@ -1354,7 +1354,7 @@ jobs: - name: Run RV32 br_table execution oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/rv32_br_table_882_differential.py + run: python scripts/oracle_run.py scripts/repro/rv32_br_table_882_differential.py rv32-extern-call-reloc-oracle: name: rv32 external-call relocation oracle (#871) @@ -1394,7 +1394,7 @@ jobs: - name: Run RV32 external-call relocation oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/riscv_extern_call_871_differential.py + run: python scripts/oracle_run.py scripts/repro/riscv_extern_call_871_differential.py rv32-label-return-oracle: name: rv32 label/return dead-code oracle (#882) @@ -1438,7 +1438,7 @@ jobs: - name: Run RV32 label/return dead-code oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/rv32_label_882_differential.py + run: python scripts/oracle_run.py scripts/repro/rv32_label_882_differential.py rv32-mem-size-grow-oracle: name: rv32 memory.size / memory.grow execution oracle @@ -1472,7 +1472,7 @@ jobs: - name: Run RV32 memory.size / memory.grow execution oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/rv32_mem_size_grow_242_differential.py + run: python scripts/oracle_run.py scripts/repro/rv32_mem_size_grow_242_differential.py callee-saved-490-oracle: name: optimized-path callee-saved preservation oracle @@ -1509,7 +1509,7 @@ jobs: - name: Run callee-saved preservation oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/callee_saved_490_differential.py + run: python scripts/oracle_run.py scripts/repro/callee_saved_490_differential.py call-indirect-642-oracle: name: call_indirect bounds-guard oracle (Thumb-2 + A32) @@ -1548,7 +1548,7 @@ jobs: - name: Run call_indirect bounds-guard oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/call_indirect_642_differential.py + run: python scripts/oracle_run.py scripts/repro/call_indirect_642_differential.py call-indirect-650-multitable-oracle: name: multi-table call_indirect oracle (Thumb-2 + A32) @@ -1588,7 +1588,7 @@ jobs: - name: Run multi-table call_indirect oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/call_indirect_650_differential.py + run: python scripts/oracle_run.py scripts/repro/call_indirect_650_differential.py call-indirect-664-nullslot-oracle: name: null-funcref-slot call_indirect oracle (Thumb-2 + A32) @@ -1633,7 +1633,7 @@ jobs: - name: Run null-funcref-slot call_indirect oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/call_indirect_664_differential.py + run: python scripts/oracle_run.py scripts/repro/call_indirect_664_differential.py call-indirect-676-heterogeneous-oracle: name: heterogeneous-table call_indirect oracle (Thumb-2 + A32) @@ -1682,7 +1682,7 @@ jobs: - name: Run heterogeneous-table call_indirect oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/call_indirect_676_differential.py + run: python scripts/oracle_run.py scripts/repro/call_indirect_676_differential.py call-indirect-275-selfcontained-oracle: name: self-contained call_indirect oracle (execution + residual declines) @@ -1727,11 +1727,11 @@ jobs: - name: Run self-contained call_indirect EXECUTION differential env: SYNTH: ./target/debug/synth - run: python scripts/repro/call_indirect_275_selfcontained_execution_differential.py + run: python scripts/oracle_run.py scripts/repro/call_indirect_275_selfcontained_execution_differential.py - name: Run emission + residual-decline oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/call_indirect_275_selfcontained_differential.py + run: python scripts/oracle_run.py scripts/repro/call_indirect_275_selfcontained_differential.py block-brif-483-oracle: name: optimized-path block/br_if lowering oracle @@ -1769,7 +1769,7 @@ jobs: - name: Run block/br_if lowering oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/block_brif_483_differential.py + run: python scripts/oracle_run.py scripts/repro/block_brif_483_differential.py spill-frame-499-oracle: name: optimized-path spill-frame teardown oracle @@ -1807,7 +1807,7 @@ jobs: - name: Run spill-frame teardown oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/spill_frame_499_differential.py + run: python scripts/oracle_run.py scripts/repro/spill_frame_499_differential.py r12-spill-496-oracle: name: optimized-path register-exhaustion oracle @@ -1847,7 +1847,7 @@ jobs: - name: Run register-exhaustion oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/r12_spill_496_differential.py + run: python scripts/oracle_run.py scripts/repro/r12_spill_496_differential.py flight-seam-570-oracle: name: flight-seam relocatable-path execution oracle @@ -1886,10 +1886,10 @@ jobs: run: | ./target/debug/synth compile scripts/repro/flight_seam.wasm \ -o /tmp/fs.elf --target cortex-m4 --all-exports --relocatable - python scripts/repro/flight_seam_differential.py /tmp/fs.elf + python scripts/oracle_run.py scripts/repro/flight_seam_differential.py /tmp/fs.elf ./target/debug/synth compile scripts/repro/flight_seam_flat.wasm \ -o /tmp/fsf.elf --target cortex-m4 --all-exports --relocatable - python scripts/repro/flight_seam_differential.py /tmp/fsf.elf \ + python scripts/oracle_run.py scripts/repro/flight_seam_differential.py /tmp/fsf.elf \ scripts/repro/flight_seam_flat.wasm control-step-584-oracle: @@ -1930,7 +1930,7 @@ jobs: run: | ./target/debug/synth compile scripts/repro/control_step.wasm \ -o /tmp/cs.elf --target cortex-m4 --all-exports --relocatable - python scripts/repro/control_step_differential.py /tmp/cs.elf + python scripts/oracle_run.py scripts/repro/control_step_differential.py /tmp/cs.elf stack-args-503-oracle: name: AAPCS stack-argument path oracle @@ -1969,7 +1969,7 @@ jobs: - name: Run AAPCS stack-argument oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/stack_args_503_differential.py + run: python scripts/oracle_run.py scripts/repro/stack_args_503_differential.py i64-completeness-503-587-oracle: name: i64 stack-param + spill-pool-grow oracle @@ -2009,19 +2009,19 @@ jobs: - name: Run i64 stack-param oracle (#503-i64) env: SYNTH: ./target/debug/synth - run: python scripts/repro/i64_stack_param_503_differential.py + run: python scripts/oracle_run.py scripts/repro/i64_stack_param_503_differential.py - name: Run i64 spill-pool-grow oracle (#587) env: SYNTH: ./target/debug/synth - run: python scripts/repro/i64_spill_pool_587_differential.py + run: python scripts/oracle_run.py scripts/repro/i64_spill_pool_587_differential.py - name: Run i64-param correctness + decline oracle (#518, d_call now emits #837) env: SYNTH: ./target/debug/synth - run: python scripts/repro/i64_param_518_differential.py + run: python scripts/oracle_run.py scripts/repro/i64_param_518_differential.py - name: Run frame-backing i64-param-with-call oracle (#837 gale gust:os/timer) env: SYNTH: ./target/debug/synth - run: python scripts/repro/framebacking_i64param_837_differential.py + run: python scripts/oracle_run.py scripts/repro/framebacking_i64param_837_differential.py i64-rot-div-610-oracle: name: i64 rotl/rotr/div/rem expansion oracle @@ -2057,7 +2057,7 @@ jobs: - name: Install emulation deps run: pip install wasmtime unicorn pyelftools - name: Run i64 rot/div/rem expansion oracle (#610) - run: python scripts/repro/i64_rot_div_610_differential.py target/debug/synth + run: python scripts/oracle_run.py scripts/repro/i64_rot_div_610_differential.py target/debug/synth br-table-507-oracle: name: optimized-path br_table oracle @@ -2096,7 +2096,7 @@ jobs: - name: Run br_table oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/br_table_507_differential.py + run: python scripts/oracle_run.py scripts/repro/br_table_507_differential.py const-cse-242-oracle: name: const-CSE flag-on execution oracle @@ -2134,7 +2134,7 @@ jobs: - name: Run const-CSE flag-on oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/const_cse_differential.py + run: python scripts/oracle_run.py scripts/repro/const_cse_differential.py frame-slot-dce-242-oracle: name: frame-slot DCE default+optout execution oracle @@ -2172,7 +2172,7 @@ jobs: - name: Run frame-slot DCE flag-on oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/frame_slot_dce_differential.py + run: python scripts/oracle_run.py scripts/repro/frame_slot_dce_differential.py stack-layout-687-oracle: name: stack-layout=low overflow BusFault oracle @@ -2212,12 +2212,12 @@ jobs: - name: Run stack-layout red/green/transparent oracle env: SYNTH: ./target/debug/synth - run: python scripts/repro/stack_layout_687_differential.py + run: python scripts/oracle_run.py scripts/repro/stack_layout_687_differential.py - name: Run the #649 global-init differential under --stack-layout=low env: SYNTH: ./target/debug/synth EXTRA_SYNTH_FLAGS: "--stack-layout low" - run: python scripts/repro/i64_global_init_649_differential.py + run: python scripts/oracle_run.py scripts/repro/i64_global_init_649_differential.py # #418: self-contained binding of the meld-dissolve embedder import # `env::__cabi_arena_realloc` — the compile must yield an ET_EXEC image @@ -2252,7 +2252,7 @@ jobs: - name: Run the #418 arena-bind execution differential env: SYNTH: ./target/debug/synth - run: python scripts/repro/cabi_arena_bind_418_differential.py + run: python scripts/oracle_run.py scripts/repro/cabi_arena_bind_418_differential.py vcr-ra-003-alloc-validator-gate: name: "VCR-RA-003 register-allocation validator (red-first + frozen)" @@ -2304,7 +2304,7 @@ jobs: - name: PHASE-2 silent-on-real-branchy-codegen (across-CALL + across-JOIN) run: | cargo build -p synth-cli - python3 scripts/repro/vcr_ra_003_phase2_join_call.py ./target/debug/synth + python3 scripts/oracle_run.py scripts/repro/vcr_ra_003_phase2_join_call.py ./target/debug/synth vcr-ra-003-rv32-alloc-validator-gate: name: "VCR-RA-003 RV32 register-allocation validator (red-first + frozen)" @@ -2360,7 +2360,7 @@ jobs: - name: Silent-on-real-codegen (RV32 fixture sweep, both paths) run: | cargo build -p synth-cli - python3 scripts/repro/vcr_ra_003_rv32_alloc_validator.py ./target/debug/synth + python3 scripts/oracle_run.py scripts/repro/vcr_ra_003_rv32_alloc_validator.py ./target/debug/synth vcr-sel-005-cross-backend-op-parity-gate: name: "VCR-SEL-005 cross-backend op-parity (universe-complete + red-first)" @@ -2440,104 +2440,104 @@ jobs: - 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py scripts/repro/base_cse_differential.py - name: value-returning-branch differential (#509, both paths) - run: python scripts/repro/br_table_value_509_differential.py + run: python scripts/oracle_run.py scripts/repro/br_table_value_509_differential.py - name: optimized-path forward-branch shapes (#500) - run: python scripts/repro/cf_shapes_500_differential.py + run: python scripts/oracle_run.py scripts/repro/cf_shapes_500_differential.py - name: const-only-body return differential (#791) - run: python scripts/repro/const_body_791_differential.py + run: python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py scripts/repro/u64_unpack_if_differential.py - name: uxth/uxtb fold differential (#428, both flag states) - run: python scripts/repro/uxth_fold_differential.py + run: python scripts/oracle_run.py scripts/repro/uxth_fold_differential.py repro-sweep-memory-oracle: name: repro sweep — linear memory / static data / native-pointer differentials @@ -2578,43 +2578,43 @@ jobs: - 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py scripts/repro/mem_grow_539_differential.py - name: static-src memmove differential (#757, inlined) - run: python scripts/repro/mem757_inlined_memmove_differential.py + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py scripts/repro/mem757_memcopy_static_src_differential.py - name: memmove-with-param differential (#757) - run: python scripts/repro/mem757_memmove_param_differential.py + run: python scripts/oracle_run.py scripts/repro/mem757_memmove_param_differential.py - name: chunked copy under register pressure differential (#757) - run: python scripts/repro/mem757_pressure_chunks_differential.py + run: python scripts/oracle_run.py scripts/repro/mem757_pressure_chunks_differential.py - name: pointer-base copy differential (#757) - run: python scripts/repro/mem757_ptr_base_copy_differential.py + run: python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + run: PATH=$PWD/target/debug:$PATH python scripts/oracle_run.py scripts/repro/postlink_359_oracle.py repro-sweep-rv32-oracle: name: repro sweep — RISC-V RV32 execution differentials @@ -2654,43 +2654,43 @@ jobs: - 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py 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 + python scripts/oracle_run.py scripts/repro/u64_unpack_riscv_differential.py repro-sweep-wcet-oracle: name: repro sweep — WCET bound soundness cross-checks (phases 2-5) @@ -2730,10 +2730,10 @@ jobs: # 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 + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py 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 + run: python scripts/oracle_run.py scripts/repro/wcet_phase5_778_masked_loop_soundness.py diff --git a/ci851.txt b/ci851.txt new file mode 100644 index 00000000..783dc78f --- /dev/null +++ b/ci851.txt @@ -0,0 +1,4 @@ + +35 checks (23 trap, 12 value) across 6 exported functions; 5 table trampolines relocated +RESULT: PASS — aarch64 call_indirect matches wasmtime, including the three §4.4.8 traps (out-of-range, null slot, signature mismatch) and the structurally-duplicate type that must NOT trap +ORACLE-CALIBRATION script=aarch64_call_indirect_851_differential.py emulations=35 wasmtime_calls=35 compiles=1 exit=0 secs=0.1 diff --git a/ga_join.out b/ga_join.out new file mode 100644 index 00000000..e321284f --- /dev/null +++ b/ga_join.out @@ -0,0 +1,72 @@ +== cf_shapes_500.wat: applied=4 RA003-consistent=6 == +OK real_ifelse(0) = 0x00000000 (wasmtime void) mem== +OK real_ifelse(1) = 0x00000001 (wasmtime void) mem== +OK real_ifelse(7) = 0x00000007 (wasmtime void) mem== +OK real_if(0) = 0x00000000 (wasmtime void) mem== +OK real_if(1) = 0x00000001 (wasmtime void) mem== +OK br_func(0) = 0x00000000 (wasmtime void) mem== +OK br_func(1) = 0x00000001 (wasmtime void) mem== +OK early_ret(0) = 0x00000000 (wasmtime void) mem== +OK early_ret(1) = 0x00000001 (wasmtime void) mem== +== provenance_branches_396.wat: applied=1 RA003-consistent=1 == +OK decide(0,0) = 0x0000006D (wasmtime 0x0000006D) mem== +OK decide(5,3) = 0x00000009 (wasmtime 0x00000009) mem== +OK decide(3,5) = 0x00000009 (wasmtime 0x00000009) mem== +OK decide(100,1) = 0x00000009 (wasmtime 0x00000009) mem== +== aarch64_ctrlflow_851.wat: applied=3 RA003-consistent=8 == +OK count_sum(0) = 0x00000000 (wasmtime 0x00000000) mem== +OK count_sum(1) = 0x00000000 (wasmtime 0x00000000) mem== +OK count_sum(5) = 0x0000000A (wasmtime 0x0000000A) mem== +OK count_sum(17) = 0x00000088 (wasmtime 0x00000088) mem== +OK countdown(0) = 0x00000000 (wasmtime 0x00000000) mem== +OK countdown(1) = 0x00000001 (wasmtime 0x00000001) mem== +OK countdown(9) = 0x00000009 (wasmtime 0x00000009) mem== +OK do_while_count(1) = 0x00000001 (wasmtime 0x00000001) mem== +OK do_while_count(6) = 0x00000006 (wasmtime 0x00000006) mem== +OK do_while_count(23) = 0x00000017 (wasmtime 0x00000017) mem== +== loop_param_bound_663.wat: applied=4 RA003-consistent=4 == +OK sum_const(0,0) = 0x0000002D (wasmtime 0x0000002D) mem== +OK sum_const(3,4) = 0x0000002D (wasmtime 0x0000002D) mem== +OK sum_below(0,0) = 0x00000000 (wasmtime 0x00000000) mem== +OK sum_below(1,5) = 0x00000000 (wasmtime 0x00000000) mem== +OK sum_below(4,4) = 0x00000006 (wasmtime 0x00000006) mem== +OK sum_below(2,9) = 0x00000001 (wasmtime 0x00000001) mem== +== if_else_result_343.wat: applied=2 RA003-consistent=3 == +OK pick(0) = 0x00000014 (wasmtime 0x00000014) mem== +OK pick(1) = 0x00000003 (wasmtime 0x00000003) mem== +OK pick(4294967295) = 0x00000003 (wasmtime 0x00000003) mem== +OK pick2(0) = 0x0000012C (wasmtime 0x0000012C) mem== +OK pick2(1) = 0x00000007 (wasmtime 0x00000007) mem== +== brif_outer_740.wat: applied=1 RA003-consistent=1 == +OK poll(7,0) = 0x00000007 (wasmtime 0x00000007) mem== +OK poll(200,0) = 0x000000C8 (wasmtime 0x000000C8) mem== +OK poll(200,1) = 0x000000C9 (wasmtime 0x000000C9) mem== +OK poll(5,3) = 0x00000005 (wasmtime 0x00000005) mem== +== local_promote_cross_call.wat: applied=1 RA003-consistent=2 == +OK cross_call(0) = 0x00000064 (wasmtime 0x00000064) mem== +OK cross_call(5) = 0x00000076 (wasmtime 0x00000076) mem== +OK cross_call(100) = 0x000001F4 (wasmtime 0x000001F4) mem== +OK cross_call(65535) = 0x0003FF9E (wasmtime 0x0003FF9E) mem== +== intra_module_callee_saved.wat: applied=1 RA003-consistent=2 == +OK a(0) = 0x0000006B (wasmtime 0x0000006B) mem== +OK a(7) = 0x00000087 (wasmtime 0x00000087) mem== +OK a(100) = 0x000001FB (wasmtime 0x000001FB) mem== +== stack_canary_687.wat: applied=1 RA003-consistent=4 == +OK recurse(0) = 0x00000000 (wasmtime 0x00000000) mem== +OK recurse(1) = 0x00000001 (wasmtime 0x00000001) mem== +OK recurse(5) = 0x00000005 (wasmtime 0x00000005) mem== +OK recurse(12) = 0x0000000C (wasmtime 0x0000000C) mem== +== call_5args.wat: applied=1 RA003-consistent=2 == +OK caller(1,2,3,4,5) = 0x00054321 (wasmtime 0x00054321) mem== +OK caller(0,0,0,0,9) = 0x00090000 (wasmtime 0x00090000) mem== +OK caller(15,1,2,4,8) = 0x0008421F (wasmtime 0x0008421F) mem== +== call_6_7args.wat: applied=4 RA003-consistent=4 == +OK call6(1,2,3,4,5,6) = 0x00654321 (wasmtime 0x00654321) mem== +OK call6(0,0,0,0,0,7) = 0x00700000 (wasmtime 0x00700000) mem== +OK call7(1,2,3,4,5,6,7) = 0x07654321 (wasmtime 0x07654321) mem== +OK call7(0,0,0,0,0,0,9) = 0x09000000 (wasmtime 0x09000000) mem== + +engaged functions (flag-on bytes differ): 19 (of which CALL shapes: 6) +VCR-DEC-001-JOIN CHECKS=56/56 ENGAGED=19 CALLSHAPES=6 +RESULT: PASS +ORACLE-CALIBRATION script=vcr_dec_001_join_alloc_execution_differential.py emulations=56 wasmtime_calls=56 compiles=22 exit=0 secs=0.5 diff --git a/globals851.txt b/globals851.txt new file mode 100644 index 00000000..c256938b --- /dev/null +++ b/globals851.txt @@ -0,0 +1,4 @@ + +17 checks across 6 exported functions (11 ADRP + 11 ADD lo12 relocations applied) +RESULT: PASS — aarch64 global.get/global.set match wasmtime (initial values, i32+i64 slots, stores persisting across calls) +ORACLE-CALIBRATION script=aarch64_globals_851_differential.py emulations=17 wasmtime_calls=17 compiles=1 exit=0 secs=0.1 diff --git a/gpio846.out b/gpio846.out new file mode 100644 index 00000000..d4943e26 --- /dev/null +++ b/gpio846.out @@ -0,0 +1,10 @@ +=== #846 SIZE === + flag-OFF (SYNTH_SHIFT_MASK_ELIDE=0): .text=534 B redundant `and r12,#0x1f` masks=10 + flag-ON (default v0.50.0) : .text=502 B redundant `and r12,#0x1f` masks=3 + recovered: 32 B (7 masks elided) +=== #846 EXECUTION UNCHANGED (flag-ON bytes vs wasmtime) === + 75/75 match — mmio (addr,value) sequences + returns bit-identical across pins [0, 1, 5, 7, 8, 15, 16, 31, 32, 33, 47, 63, 100, 255, 2147483647] (incl. >=32 mod-32 boundary) +=== RESULT === +#846 CHECKS=75/75 trace_events=105 +gpio-thin #846: PASS +ORACLE-CALIBRATION script=gpio_thin_846_differential.py emulations=75 wasmtime_calls=75 compiles=2 exit=0 secs=0.3 diff --git a/scripts/oracle_run.py b/scripts/oracle_run.py new file mode 100644 index 00000000..b9cea0c0 --- /dev/null +++ b/scripts/oracle_run.py @@ -0,0 +1,432 @@ +#!/usr/bin/env python3 +r"""oracle_run — run an execution oracle and assert that it EXECUTED something. + +The problem this exists to kill (#910 F10, on top of #890) +-------------------------------------------------------------------------- +#890 wired 63 forgotten oracles into CI. Measured on the result: **152 of the +160 workflow steps that run a `scripts/repro/` oracle asserted nothing beyond +the process exit code** — not only the newly wired ones, the pre-existing +hand-wired steps too. Exactly 8 asserted a printed verdict or a count. + +Exit 0 does not distinguish + + "compiled 40 fixtures, emulated 240 vectors, all bit-identical to wasmtime" + +from + + "the fixture list came back empty, the loop body never ran, printed PASS". + +That is #890's inert gate one level down: the oracle is wired, but *what it +attests* is unstated. A differential that executes zero comparisons and exits 0 +is the exact shape of a green-but-meaningless number. + +WHAT IS COUNTED, and why that word +-------------------------------------------------------------------------- +This driver runs the oracle IN-PROCESS (`runpy`) with three entry points +wrapped: + + unicorn.Uc.emu_start -> `emulations` (a real emulator entry) + wasmtime.Func.__call__ -> `wasmtime_calls` (a real reference execution) + subprocess `synth … compile …` -> `compiles` (a real compilation) + +The first two are the ends of a differential: run the compiled bytes, run the +reference, compare. Counting them counts EXECUTION — a comparison loop that +never runs cannot fake it, because the count comes from the emulator, not from +the harness's own bookkeeping. + +`compiles` exists for the oracles whose work is not emulation: decline +matrices, byte-identity legs, symtab/relocation validators, and the native +(non-unicorn) aarch64 matrix. Those still drive the compiler, and "the harness +compiled nothing" is exactly the vacuity that needs catching there. It is the +WEAKEST of the three and is only declared where the stronger two cannot hold on +every invocation of that script. + +The unit is named `emulations`, NOT "checks", and that is deliberate. The +calibration (docs in scripts/repro/ORACLE_WIRING.md) found the ratio to a +harness's self-reported check count is NOT 1:1 — some harnesses emulate once +per vector, some enter the emulator several times per vector, some compare +several values out of one run. This lane exists because an instrument was +reporting something other than what its name implied; shipping a number +labelled "checks" that actually counts emulator entries would repeat the defect +being fixed. `emulations` is what is measured, so `emulations` is what it is +called. + +THE DECLARATION — one `# ci-checks:` header per oracle +-------------------------------------------------------------------------- +Same locality argument as `# ci-status:` (see ORACLE_WIRING.md): the floor +lives in the file it describes, so it shows up in the diff of the PR that adds +the oracle, and it cannot outlive its file the way a manifest entry can. + + # ci-checks: emulations >= 24 + # ci-checks: wasmtime >= 8 + # ci-checks: compiles >= 2 + # ci-checks: stdout /^#846 CHECKS=(\d+)\/75$/ >= 75 + # ci-checks: none — <>= 20 chars saying why nothing can be bound> + +Declare the STRONGEST mode that holds on EVERY invocation of that script in +CI — several oracles are run twice, once executing and once on a decline / +byte-identity leg that executes nothing by design, and a floor that only holds +for the good leg is not a floor. What the weaker floor gives up is not lost: +every counter is still MEASURED and recorded, so the ledger reports what ran +while the gate asserts what is guaranteed. + +`stdout` mode is for the oracles that execute nothing emulatable (structural +validators, decline matrices, symtab differentials). Its regex must carry +exactly one capture group holding an integer, so it asserts a COUNT and not +merely the presence of a happy-path string. + +FLOORS, NEVER EQUALITY. `>=` so that adding a fixture cannot redden a step; the +ratchet direction is up. `scripts/oracle_wiring_check.py` sums the declared +floors, and `claims.yaml` pins the total. + +Exit: the oracle's own exit code, unless a floor is unmet (then 1). An oracle +that exits 0 having emulated nothing FAILS here. +""" + +import argparse +import io +import os +import pathlib +import re +import runpy +import sys +import time + +DECL_RE = re.compile( + r"^#\s*ci-checks:\s*" + r"(?Pemulations|wasmtime|compiles|stdout|none)\b" + r"\s*(?P.*)$", + re.MULTILINE, +) + +# `stdout // >= N` +STDOUT_RE = re.compile(r"^/(?P.+)/\s*>=\s*(?P\d+)\s*$") +# `emulations >= N` / `wasmtime >= N` +NUM_RE = re.compile(r"^>=\s*(?P\d+)\s*$") + +MIN_REASON_CHARS = 20 + + +class Decl: + """A parsed `# ci-checks:` declaration.""" + + def __init__(self, mode, minimum=0, regex=None, reason=""): + self.mode = mode + self.minimum = minimum + self.regex = regex + self.reason = reason + + def __repr__(self): # pragma: no cover - diagnostics only + return f"Decl({self.mode}, min={self.minimum}, rx={self.regex})" + + +def parse_decl(text, rel): + """Parse the single `# ci-checks:` header. Returns (Decl, error-or-None).""" + decls = list(DECL_RE.finditer(text)) + if not decls: + return None, ( + f"{rel}: no `# ci-checks:` header. Every oracle must declare what it " + f"attests: `emulations >= N` | `wasmtime >= N` | " + f"`stdout // >= N` | `none — `." + ) + if len(decls) > 1: + return None, f"{rel}: {len(decls)} `# ci-checks:` lines — exactly one is allowed" + + m = decls[0] + mode = m.group("mode") + rest = (m.group("rest") or "").strip() + + if mode == "none": + reason = rest.lstrip("-—: ").strip() + if len(reason) < MIN_REASON_CHARS: + return None, ( + f"{rel}: `ci-checks: none` needs a REAL reason " + f"(>= {MIN_REASON_CHARS} chars) saying what cannot be bound; " + f"got {reason!r}" + ) + return Decl("none", reason=reason), None + + if mode == "stdout": + sm = STDOUT_RE.match(rest) + if not sm: + return None, ( + f"{rel}: `ci-checks: stdout` wants `// >= N`; got {rest!r}" + ) + try: + rx = re.compile(sm.group("rx"), re.MULTILINE) + except re.error as exc: + return None, f"{rel}: `ci-checks: stdout` regex does not compile: {exc}" + if rx.groups != 1: + return None, ( + f"{rel}: `ci-checks: stdout` regex must have EXACTLY ONE capture " + f"group holding the count (got {rx.groups}) — a pattern with no " + f"group asserts a happy-path STRING, not that anything ran." + ) + return Decl("stdout", int(sm.group("min")), regex=rx), None + + nm = NUM_RE.match(rest) + if not nm: + return None, f"{rel}: `ci-checks: {mode}` wants `>= N`; got {rest!r}" + return Decl(mode, int(nm.group("min"))), None + + +class Counters: + def __init__(self): + self.emulations = 0 + self.wasmtime_calls = 0 + self.compiles = 0 + + +def _is_synth_compile(argv): + """True for a subprocess that is `<...>/synth … compile …`. + + Deliberately narrow: `nm`, `objdump` and `wat2wasm` runs are not evidence + that the thing under test did anything. + """ + try: + if isinstance(argv, (str, bytes, os.PathLike)): + return False + parts = [os.fsdecode(a) for a in argv] + except (TypeError, ValueError): + return False + if not parts: + return False + exe = os.path.basename(parts[0]).lower() + if not (exe == "synth" or exe.startswith("synth")): + return False + return "compile" in parts[1:] + + +def install_probes(counters): + """Wrap the two library entry points. Returns the list of names wrapped. + + Deliberately NOT an import hook or a `sitecustomize` shim: the wrap happens + here, before the oracle runs, and `sys.modules` caching means a later + `import unicorn` / `from unicorn import Uc` inside the oracle gets the same + already-patched class object. + """ + wrapped = [] + + try: + import unicorn + except ImportError: + unicorn = None + if unicorn is not None and hasattr(unicorn, "Uc"): + orig_emu = unicorn.Uc.emu_start + + def emu_start(self, *a, **kw): + counters.emulations += 1 + return orig_emu(self, *a, **kw) + + unicorn.Uc.emu_start = emu_start + wrapped.append("unicorn.Uc.emu_start") + + try: + import wasmtime + except ImportError: + wasmtime = None + if wasmtime is not None and hasattr(wasmtime, "Func"): + orig_call = wasmtime.Func.__call__ + + def func_call(self, *a, **kw): + counters.wasmtime_calls += 1 + return orig_call(self, *a, **kw) + + wasmtime.Func.__call__ = func_call + wrapped.append("wasmtime.Func.__call__") + + # Every harness reaches the compiler through subprocess.Popen — `run`, + # `check_output`, `call` and `check_call` are all thin wrappers over it, so + # patching the class catches all of them, including a harness that imported + # `run` by name before this ran. + import subprocess + + orig_popen_init = subprocess.Popen.__init__ + + def popen_init(self, args, *a, **kw): + if _is_synth_compile(args): + counters.compiles += 1 + return orig_popen_init(self, args, *a, **kw) + + subprocess.Popen.__init__ = popen_init + wrapped.append("subprocess.Popen") + + return wrapped + + +class Tee(io.TextIOBase): + """Mirror the oracle's stdout to the real stdout AND to a buffer. + + The CI log must keep showing exactly what the oracle printed — a driver that + swallowed the harness output would make every failure harder to read than + before, which is not a trade worth making for a count. + """ + + def __init__(self, real): + self.real = real + self.buf = io.StringIO() + + def write(self, s): + self.buf.write(s) + return self.real.write(s) + + def flush(self): + self.real.flush() + + @property + def encoding(self): # some harnesses inspect it + return getattr(self.real, "encoding", "utf-8") + + def isatty(self): + return False + + def writable(self): + return True + + +def run_oracle(script, argv): + """Execute `script` in-process. Returns (exit_code, counters, stdout_text).""" + counters = Counters() + install_probes(counters) + + real_out = sys.stdout + tee = Tee(real_out) + saved_argv, saved_path = sys.argv[:], sys.path[:] + + # `python script.py` puts the script's OWN directory at sys.path[0]; + # runpy.run_path does not, and several repro harnesses import sibling + # helpers. Reproduce the plain-interpreter behaviour so the driver is not + # observably different from the invocation it replaces. + sys.path.insert(0, os.path.dirname(os.path.abspath(script))) + sys.argv = [script] + list(argv) + sys.stdout = tee + code = 0 + try: + runpy.run_path(script, run_name="__main__") + except SystemExit as exc: # the normal exit path of every repro harness + c = exc.code + code = 0 if c is None else (c if isinstance(c, int) else 1) + finally: + sys.stdout = real_out + sys.argv, sys.path = saved_argv, saved_path + return code, counters, tee.buf.getvalue() + + +def evaluate(decl, code, counters, out, rel): + """Apply the declared floor. Returns (ok, measured, failures).""" + fails = [] + if decl.mode == "emulations": + measured = counters.emulations + elif decl.mode == "wasmtime": + measured = counters.wasmtime_calls + elif decl.mode == "compiles": + measured = counters.compiles + elif decl.mode == "stdout": + hits = decl.regex.findall(out) + try: + measured = max(int(h) for h in hits) if hits else 0 + except (TypeError, ValueError): + measured = 0 + fails.append( + f"{rel}: `ci-checks: stdout` regex matched, but its capture group " + f"is not an integer: {hits[:3]!r}" + ) + if not hits: + fails.append( + f"{rel}: `ci-checks: stdout` pattern {decl.regex.pattern!r} did NOT " + f"match the oracle's output — the declared evidence line is gone " + f"or renamed." + ) + else: # none + measured = None + + if measured is not None and measured < decl.minimum: + fails.append( + f"{rel}: VACUOUS — declared floor {decl.mode} >= {decl.minimum}, " + f"measured {measured}. The oracle exited {code} having executed " + f"{'nothing' if measured == 0 else 'less than it claims'}; that is a " + f"gate that cannot fail, not a passing gate." + ) + return not fails, measured, fails + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("script", help="path to the scripts/repro/ oracle") + ap.add_argument("args", nargs=argparse.REMAINDER, help="arguments for it") + ap.add_argument( + "--report-only", + action="store_true", + help="print the measurement, do not enforce the floor (calibration only)", + ) + args = ap.parse_args() + + script = args.script + rel = os.path.relpath(script) + if not os.path.isfile(script): + sys.exit(f"oracle_run: no such oracle: {script}") + + decl, err = parse_decl(pathlib.Path(script).read_text(errors="ignore"), rel) + if err and not args.report_only: + sys.exit(f"oracle_run: {err}") + + t0 = time.time() + code, counters, out = run_oracle(script, args.args) + dt = time.time() - t0 + + if args.report_only: + print( + f"ORACLE-CALIBRATION script={os.path.basename(script)} " + f"emulations={counters.emulations} " + f"wasmtime_calls={counters.wasmtime_calls} " + f"compiles={counters.compiles} " + f"exit={code} secs={dt:.1f}" + ) + return 0 + + ok, measured, fails = evaluate(decl, code, counters, out, rel) + + print( + f"ORACLE-EVIDENCE script={os.path.basename(script)} " + f"mode={decl.mode} floor={decl.minimum} measured={measured} " + f"emulations={counters.emulations} wasmtime_calls={counters.wasmtime_calls} " + f"compiles={counters.compiles} exit={code}" + ) + + # Append to the per-job ledger, if the job asked for one. Written even on + # failure: a run that fell BELOW its floor is exactly the datum worth having. + ledger = os.environ.get("ORACLE_EVIDENCE_JSONL") + if ledger: + import json + + with open(ledger, "a") as fh: + fh.write( + json.dumps( + { + "script": rel, + "mode": decl.mode, + "floor": decl.minimum, + "measured": measured, + "emulations": counters.emulations, + "wasmtime_calls": counters.wasmtime_calls, + "compiles": counters.compiles, + "exit": code, + "ok": bool(ok and code == 0), + }, + sort_keys=True, + ) + + "\n" + ) + + for f in fails: + print(f"FAIL {f}", file=sys.stderr) + + # The oracle's own verdict still rules: a differential that found a + # miscompile must stay red even if it emulated plenty. + if code != 0: + return code + return 0 if ok else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/repro/a32_i64_615_differential.py b/scripts/repro/a32_i64_615_differential.py index 9e0b982c..3110e3e6 100644 --- a/scripts/repro/a32_i64_615_differential.py +++ b/scripts/repro/a32_i64_615_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 352 # #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 f48e31bb..6f7c12a0 100644 --- a/scripts/repro/aarch64_add_538_differential.py +++ b/scripts/repro/aarch64_add_538_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 f7b55205..f926a671 100644 --- a/scripts/repro/aarch64_bounds_865_differential.py +++ b/scripts/repro/aarch64_bounds_865_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 21 """#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_call_indirect_851_differential.py b/scripts/repro/aarch64_call_indirect_851_differential.py index e51f4c5e..376b1dda 100644 --- a/scripts/repro/aarch64_call_indirect_851_differential.py +++ b/scripts/repro/aarch64_call_indirect_851_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 35 """#851 lane L3 — aarch64 `call_indirect` execution differential vs wasmtime. A64's `blr` is TOTAL: it branches wherever the register points. WASM §4.4.8 is diff --git a/scripts/repro/aarch64_calls_851.py b/scripts/repro/aarch64_calls_851.py index 127d4ed5..8da5f07c 100644 --- a/scripts/repro/aarch64_calls_851.py +++ b/scripts/repro/aarch64_calls_851.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: stdout /^PASS: (\d+) call runs bit-identical/ >= 5 """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 5c752f85..2665bf23 100644 --- a/scripts/repro/aarch64_cf_538_differential.py +++ b/scripts/repro/aarch64_cf_538_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 14 """#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 dfa76b96..141be6b8 100644 --- a/scripts/repro/aarch64_ctrlflow_851_differential.py +++ b/scripts/repro/aarch64_ctrlflow_851_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 28 """#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 78b8378c..ce9e80ef 100644 --- a/scripts/repro/aarch64_divrem_851_differential.py +++ b/scripts/repro/aarch64_divrem_851_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 179 """#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_float_completion_851_differential.py b/scripts/repro/aarch64_float_completion_851_differential.py index be7308df..6a3ee78e 100644 --- a/scripts/repro/aarch64_float_completion_851_differential.py +++ b/scripts/repro/aarch64_float_completion_851_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 662 """v0.54 L2 (#851) — the aarch64 float-completion EXECUTION differential. Closes the four classes the VCR-SEL-005 third-backend op-parity oracle listed as diff --git a/scripts/repro/aarch64_globals_851_differential.py b/scripts/repro/aarch64_globals_851_differential.py index 0c5edf40..af95be38 100644 --- a/scripts/repro/aarch64_globals_851_differential.py +++ b/scripts/repro/aarch64_globals_851_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 17 """#851 lane L3 — aarch64 WASM GLOBALS execution differential vs wasmtime. synth emits the globals region ITSELF: a `.data` section carrying each global's diff --git a/scripts/repro/aarch64_locals_851_differential.py b/scripts/repro/aarch64_locals_851_differential.py index 999aede1..5ba85f04 100644 --- a/scripts/repro/aarch64_locals_851_differential.py +++ b/scripts/repro/aarch64_locals_851_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 17 """#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 61b62a4e..da2bdcc3 100755 --- a/scripts/repro/aarch64_m2_538_differential.py +++ b/scripts/repro/aarch64_m2_538_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 182 """#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 c8d8e671..bfdde92d 100755 --- a/scripts/repro/aarch64_m2_decline_538.py +++ b/scripts/repro/aarch64_m2_decline_538.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: stdout /^(\d+)/\d+ declined ops loud-declined/ >= 12 """#538 milestone-2 — assert the aarch64 decline matrix stays HONEST. Some WASM constructs are DELIBERATELY not lowered on aarch64, and the contract diff --git a/scripts/repro/aarch64_m3_floats_538_differential.py b/scripts/repro/aarch64_m3_floats_538_differential.py index 934b2aff..0e05b6fc 100755 --- a/scripts/repro/aarch64_m3_floats_538_differential.py +++ b/scripts/repro/aarch64_m3_floats_538_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 513 """#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 eeeb48a3..9e103120 100644 --- a/scripts/repro/aarch64_m4_trunc_minmax_538_differential.py +++ b/scripts/repro/aarch64_m4_trunc_minmax_538_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 167 """#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 c73623ab..0087e909 100755 --- a/scripts/repro/aarch64_matrix.sh +++ b/scripts/repro/aarch64_matrix.sh @@ -1,5 +1,6 @@ #!/usr/bin/env bash # ci-status: wired +# ci-checks: none — a POSIX shell oracle — oracle_run.py drives Python in-process and cannot instrument it. Its step carries its own count assertion (>= 32 accepted ops), written before this mechanism existed. # 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 7e8eb28a..10a1c63f 100644 --- a/scripts/repro/aarch64_mem_851_differential.py +++ b/scripts/repro/aarch64_mem_851_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 41 """#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 7ff12998..16ca3e7c 100644 --- a/scripts/repro/aarch64_surface_851_differential.py +++ b/scripts/repro/aarch64_surface_851_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 58 """#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 6c1dc183..5e0f345a 100644 --- a/scripts/repro/add_imm_large_differential.py +++ b/scripts/repro/add_imm_large_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 028e8bad..1bbe0a01 100644 --- a/scripts/repro/addw_offset_681_differential.py +++ b/scripts/repro/addw_offset_681_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 49 """#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 52f2d3c8..ecfcafbb 100644 --- a/scripts/repro/base_cse_differential.py +++ b/scripts/repro/base_cse_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 2 """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) diff --git a/scripts/repro/block_brif_483_differential.py b/scripts/repro/block_brif_483_differential.py index 87828caa..1cfa3eab 100644 --- a/scripts/repro/block_brif_483_differential.py +++ b/scripts/repro/block_brif_483_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 4 """#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 5b56dcd2..b75fad03 100644 --- a/scripts/repro/br_table_507_differential.py +++ b/scripts/repro/br_table_507_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 12 """#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 6592eabf..76d38293 100644 --- a/scripts/repro/br_table_value_509_differential.py +++ b/scripts/repro/br_table_value_509_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 32 """#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 e1caff9a..55c48a08 100644 --- a/scripts/repro/brif_outer_740_differential.py +++ b/scripts/repro/brif_outer_740_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 6 """#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 5f47867f..bbbe7aaa 100644 --- a/scripts/repro/bulk_local_clobber_677_differential.py +++ b/scripts/repro/bulk_local_clobber_677_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 b409db9f..f3e78221 100644 --- a/scripts/repro/bulk_mask_679_differential.py +++ b/scripts/repro/bulk_mask_679_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 a4dad906..4c16a332 100644 --- a/scripts/repro/bulk_memory_374_differential.py +++ b/scripts/repro/bulk_memory_374_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 16 """#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 83fda5d4..a4b73cdd 100644 --- a/scripts/repro/cabi_arena_bind_418_differential.py +++ b/scripts/repro/cabi_arena_bind_418_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 12 """#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 140cfe6a..a2069b44 100644 --- a/scripts/repro/call_5args_differential.py +++ b/scripts/repro/call_5args_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 5 """#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 df24ddd7..7d1ed584 100644 --- a/scripts/repro/call_6_7args_differential.py +++ b/scripts/repro/call_6_7args_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 4 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 bf1222dd..c72e4c2c 100755 --- a/scripts/repro/call_indirect_275_selfcontained_differential.py +++ b/scripts/repro/call_indirect_275_selfcontained_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: compiles >= 4 """#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 23cf0de3..d11a6dd0 100644 --- a/scripts/repro/call_indirect_275_selfcontained_execution_differential.py +++ b/scripts/repro/call_indirect_275_selfcontained_execution_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 15 """#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 f460dc05..5a23bef8 100644 --- a/scripts/repro/call_indirect_594_differential.py +++ b/scripts/repro/call_indirect_594_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 1 # #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 effcff13..78ede526 100644 --- a/scripts/repro/call_indirect_597_differential.py +++ b/scripts/repro/call_indirect_597_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 3 # #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 d311727a..631d2a1c 100644 --- a/scripts/repro/call_indirect_642_differential.py +++ b/scripts/repro/call_indirect_642_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 12 """#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 49bb2d13..8e4adf9a 100644 --- a/scripts/repro/call_indirect_650_differential.py +++ b/scripts/repro/call_indirect_650_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 28 """#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 901ee2bc..942f87c0 100644 --- a/scripts/repro/call_indirect_664_differential.py +++ b/scripts/repro/call_indirect_664_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 12 """#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 e1006da2..fdb58b6b 100644 --- a/scripts/repro/call_indirect_676_differential.py +++ b/scripts/repro/call_indirect_676_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 28 """#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 940fb711..9a525242 100644 --- a/scripts/repro/callee_saved_490_differential.py +++ b/scripts/repro/callee_saved_490_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 15 """#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 bda394ea..db94efd5 100644 --- a/scripts/repro/cf_shapes_500_differential.py +++ b/scripts/repro/cf_shapes_500_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 14 """#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 afb957df..f929bc05 100755 --- a/scripts/repro/cmp_select_two_move_differential.py +++ b/scripts/repro/cmp_select_two_move_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 22 """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 07e6193f..ecfee5f6 100644 --- a/scripts/repro/const_addr_fold_riscv_differential.py +++ b/scripts/repro/const_addr_fold_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 2 """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 43041d6d..316f6a66 100644 --- a/scripts/repro/const_body_791_differential.py +++ b/scripts/repro/const_body_791_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 6 """#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 8787bfc5..ac98dcad 100755 --- a/scripts/repro/const_cse_differential.py +++ b/scripts/repro/const_cse_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 54 """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 bd19a0e2..cd35d71a 100644 --- a/scripts/repro/control_step_differential.py +++ b/scripts/repro/control_step_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 13 """#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 dd0fbb25..4be00a72 100644 --- a/scripts/repro/control_step_riscv_differential.py +++ b/scripts/repro/control_step_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 5 """#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 6dc7bd90..177bee58 100644 --- a/scripts/repro/controller_step_riscv_differential.py +++ b/scripts/repro/controller_step_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 5 """#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 3b053bda..5ae801d2 100644 --- a/scripts/repro/div_const_differential.py +++ b/scripts/repro/div_const_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 338 """#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 daed6ba9..72315900 100644 --- a/scripts/repro/dyn_table_359_differential.py +++ b/scripts/repro/dyn_table_359_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 4 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 ffd2a54f..abe1898f 100644 --- a/scripts/repro/f32_mem_trunc_708_709_differential.py +++ b/scripts/repro/f32_mem_trunc_708_709_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 48 """#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 2c535f74..bda20a13 100755 --- a/scripts/repro/f32_ops_719_differential.py +++ b/scripts/repro/f32_ops_719_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 238 """#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 d502c2ff..60105ce2 100755 --- a/scripts/repro/f32_vfp_619_differential.py +++ b/scripts/repro/f32_vfp_619_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 84 """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 25aa1629..e0573ab2 100644 --- a/scripts/repro/f64_369_differential.py +++ b/scripts/repro/f64_369_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 339 """#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 59b3c1c4..425c0ad5 100644 --- a/scripts/repro/fact_spec_bounds_494_differential.py +++ b/scripts/repro/fact_spec_bounds_494_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: compiles >= 2 """#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 48ff3faf..bc2cd7e6 100644 --- a/scripts/repro/fact_spec_clamp_494_differential.py +++ b/scripts/repro/fact_spec_clamp_494_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: compiles >= 2 """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 0e6e4b6d..0e211f89 100644 --- a/scripts/repro/fact_spec_div_494_differential.py +++ b/scripts/repro/fact_spec_div_494_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: compiles >= 2 """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 170fc73e..108dcb4c 100755 --- a/scripts/repro/fact_spec_mask_494_differential.py +++ b/scripts/repro/fact_spec_mask_494_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: compiles >= 2 """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 410ce3ab..5847cb6d 100644 --- a/scripts/repro/fact_spec_rem_494_differential.py +++ b/scripts/repro/fact_spec_rem_494_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 26 """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 a5d409cf..bff19ed0 100755 --- a/scripts/repro/fact_spec_select_494_differential.py +++ b/scripts/repro/fact_spec_select_494_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: compiles >= 2 """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 9a81acba..4b15983a 100644 --- a/scripts/repro/filter_axis_riscv_differential.py +++ b/scripts/repro/filter_axis_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 5 """#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 77c07c2a..0b87363e 100644 --- a/scripts/repro/flight_seam_differential.py +++ b/scripts/repro/flight_seam_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 1 """#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 17f3b220..4b7cecc9 100644 --- a/scripts/repro/float_select_return_782_differential.py +++ b/scripts/repro/float_select_return_782_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 702 """#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 cbc32631..e4d2b9b3 100755 --- a/scripts/repro/frame_slot_dce_differential.py +++ b/scripts/repro/frame_slot_dce_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """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 b14814b9..3df18dc9 100644 --- a/scripts/repro/framebacking_i64param_837_differential.py +++ b/scripts/repro/framebacking_i64param_837_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 10 """#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 1d09b08f..478c9670 100644 --- a/scripts/repro/gpio_thin_846_differential.py +++ b/scripts/repro/gpio_thin_846_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 75 """#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 b422c134..6e854f05 100644 --- a/scripts/repro/gust_spill_fwd_390_differential.py +++ b/scripts/repro/gust_spill_fwd_390_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 30 """#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 869c2cd5..efc57167 100644 --- a/scripts/repro/high_pressure_i32_differential.py +++ b/scripts/repro/high_pressure_i32_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 6 """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 d005b1d7..2c4aa2d6 100644 --- a/scripts/repro/high_pressure_i64_differential.py +++ b/scripts/repro/high_pressure_i64_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 6 """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 c5b38fa3..b40ab04c 100644 --- a/scripts/repro/i32_shift_mask_682_differential.py +++ b/scripts/repro/i32_shift_mask_682_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 28 """#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 7f0e73b2..911edb3e 100644 --- a/scripts/repro/i64_divs_317_riscv_differential.py +++ b/scripts/repro/i64_divs_317_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 10 """#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 788d25d3..69a07be7 100644 --- a/scripts/repro/i64_divs_overflow_633_differential.py +++ b/scripts/repro/i64_divs_overflow_633_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 16 # #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 48d59bf9..83eb620d 100644 --- a/scripts/repro/i64_float_conv_869_differential.py +++ b/scripts/repro/i64_float_conv_869_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 96276 """#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 48582af7..6d829daa 100644 --- a/scripts/repro/i64_global_init_649_differential.py +++ b/scripts/repro/i64_global_init_649_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 11 """#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 63b5b4cc..9f29a2ba 100644 --- a/scripts/repro/i64_globals_643_differential.py +++ b/scripts/repro/i64_globals_643_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 28 """#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 161a5ba5..76316564 100755 --- a/scripts/repro/i64_large_offset_382_differential.py +++ b/scripts/repro/i64_large_offset_382_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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_pair_exhaust_587_differential.py b/scripts/repro/i64_pair_exhaust_587_differential.py index c6bebd27..0adc186e 100644 --- a/scripts/repro/i64_pair_exhaust_587_differential.py +++ b/scripts/repro/i64_pair_exhaust_587_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 ae10aea5..3ac016e0 100644 --- a/scripts/repro/i64_param_518_differential.py +++ b/scripts/repro/i64_param_518_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 25 """#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 16db6905..f1824d20 100644 --- a/scripts/repro/i64_param_518_riscv_loudskip.py +++ b/scripts/repro/i64_param_518_riscv_loudskip.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: compiles >= 1 """#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 703e017b..54208246 100644 --- a/scripts/repro/i64_popcnt_632_differential.py +++ b/scripts/repro/i64_popcnt_632_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 11 # #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 01e1523f..d73398bf 100644 --- a/scripts/repro/i64_rot_div_610_differential.py +++ b/scripts/repro/i64_rot_div_610_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 54 # #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 a459f6d7..609e4d1a 100644 --- a/scripts/repro/i64_shr_599_differential.py +++ b/scripts/repro/i64_shr_599_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 9 # #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 e48dcd4f..6e3634df 100644 --- a/scripts/repro/i64_spill_pool_587_differential.py +++ b/scripts/repro/i64_spill_pool_587_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 2f696af1..a8106c3e 100644 --- a/scripts/repro/i64_stack_param_503_differential.py +++ b/scripts/repro/i64_stack_param_503_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 16 """#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 2e0cb936..c2d44ecd 100755 --- a/scripts/repro/if_else_result_343_riscv_differential.py +++ b/scripts/repro/if_else_result_343_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 12 """#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 27ac04db..a9eb1fbd 100644 --- a/scripts/repro/leaf_dead_frame_differential.py +++ b/scripts/repro/leaf_dead_frame_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 20 """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 diff --git a/scripts/repro/load_store_big_offset_382_differential.py b/scripts/repro/load_store_big_offset_382_differential.py index 24d0da6c..3d36932a 100644 --- a/scripts/repro/load_store_big_offset_382_differential.py +++ b/scripts/repro/load_store_big_offset_382_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#382 — large static load/store offset (> imm12) differential oracle. The optimized (non-relocatable) ARM path materializes the linear-memory base as diff --git a/scripts/repro/local_promote_i32_differential.py b/scripts/repro/local_promote_i32_differential.py index 5ce03645..e543ff1a 100644 --- a/scripts/repro/local_promote_i32_differential.py +++ b/scripts/repro/local_promote_i32_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 14 """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/loop_param_bound_663_differential.py b/scripts/repro/loop_param_bound_663_differential.py index 91b87ede..ff5be829 100644 --- a/scripts/repro/loop_param_bound_663_differential.py +++ b/scripts/repro/loop_param_bound_663_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 16 """#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 3f71d9a2..3abf5d3f 100644 --- a/scripts/repro/mask_bounds_655_riscv_differential.py +++ b/scripts/repro/mask_bounds_655_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 25 """#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 0eece475..389857de 100644 --- a/scripts/repro/mem757_gale_differential.py +++ b/scripts/repro/mem757_gale_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: stdout /^loom\.wasm: (\d+) data segments/ >= 3 """#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 910422c2..5082d3d0 100644 --- a/scripts/repro/mem757_inlined_memmove_differential.py +++ b/scripts/repro/mem757_inlined_memmove_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 11 """#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 1bfe5772..a3cd9d19 100644 --- a/scripts/repro/mem757_low_const_copy_differential.py +++ b/scripts/repro/mem757_low_const_copy_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 11 """#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 415c12df..0aa487e1 100644 --- a/scripts/repro/mem757_memcopy_static_src_differential.py +++ b/scripts/repro/mem757_memcopy_static_src_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 11 """#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 9282a0f5..f8221a99 100644 --- a/scripts/repro/mem757_memmove_param_differential.py +++ b/scripts/repro/mem757_memmove_param_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 11 """#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 a704c4eb..322dd43e 100644 --- a/scripts/repro/mem757_pressure_chunks_differential.py +++ b/scripts/repro/mem757_pressure_chunks_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 11 """#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 34d8cc8a..59cc6520 100644 --- a/scripts/repro/mem757_ptr_base_copy_differential.py +++ b/scripts/repro/mem757_ptr_base_copy_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 11 """#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 2311ebfd..a5638029 100644 --- a/scripts/repro/mem757_rawvec_memcopy_differential.py +++ b/scripts/repro/mem757_rawvec_memcopy_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 11 """#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 ab0f1f24..4221b565 100644 --- a/scripts/repro/mem761_linmem_r9_overlap_differential.py +++ b/scripts/repro/mem761_linmem_r9_overlap_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 4 """#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 4c735b2b..881159e6 100644 --- a/scripts/repro/mem_grow_539_differential.py +++ b/scripts/repro/mem_grow_539_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 6 """#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 e387d2a0..90a1aefc 100644 --- a/scripts/repro/multi_memory_406_differential.py +++ b/scripts/repro/multi_memory_406_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 29 """#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 7e09ed68..0c318f42 100644 --- a/scripts/repro/multi_segment_static_data_differential.py +++ b/scripts/repro/multi_segment_static_data_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 27 """#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 cef9827b..669dec1d 100644 --- a/scripts/repro/multi_sp_707_differential.py +++ b/scripts/repro/multi_sp_707_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 13 """#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 64bc9588..81059881 100644 --- a/scripts/repro/mutex_pressure_differential.py +++ b/scripts/repro/mutex_pressure_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 7 """#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 568f9b08..cc240515 100644 --- a/scripts/repro/native_pointer_shadow_stack_differential.py +++ b/scripts/repro/native_pointer_shadow_stack_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 3 """#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 a6df148e..b045949b 100644 --- a/scripts/repro/native_pointer_static_downshift_678.py +++ b/scripts/repro/native_pointer_static_downshift_678.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 4 """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 68d25bb0..ed433cad 100644 --- a/scripts/repro/postex_cycle_proxy.py +++ b/scripts/repro/postex_cycle_proxy.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 78 """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 64b0b563..a1001057 100755 --- a/scripts/repro/postlink_359_oracle.py +++ b/scripts/repro/postlink_359_oracle.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: compiles >= 1 """ #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 cbadce69..185f676f 100644 --- a/scripts/repro/r12_spill_496_differential.py +++ b/scripts/repro/r12_spill_496_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 14 """#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 56e19397..ad47d349 100644 --- a/scripts/repro/reachable_callgraph_275_selfcontained_differential.py +++ b/scripts/repro/reachable_callgraph_275_selfcontained_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 ebade40b..442e7e57 100644 --- a/scripts/repro/read_before_write_local_zeroinit_differential.py +++ b/scripts/repro/read_before_write_local_zeroinit_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 14 """#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 fdfed7a8..00a57a5f 100644 --- a/scripts/repro/rem_s_666_differential.py +++ b/scripts/repro/rem_s_666_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 c1ef151a..3a7a0d00 100644 --- a/scripts/repro/riscv_extern_call_871_differential.py +++ b/scripts/repro/riscv_extern_call_871_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 20 """#871 — RV32 external-call relocations: read-back + link + execution oracle. gale's thin-seam drivers import a two-function mmio seam (env::mmio_read32 / diff --git a/scripts/repro/rv32_br_table_882_differential.py b/scripts/repro/rv32_br_table_882_differential.py index 62496dbc..d007703a 100644 --- a/scripts/repro/rv32_br_table_882_differential.py +++ b/scripts/repro/rv32_br_table_882_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 27 """#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 4612a2fa..008b7b2f 100755 --- a/scripts/repro/rv32_cmp_select_472_riscv_differential.py +++ b/scripts/repro/rv32_cmp_select_472_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 182 """#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 1a0b7b03..bc26b112 100644 --- a/scripts/repro/rv32_data_798_boot_differential.py +++ b/scripts/repro/rv32_data_798_boot_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 1 """#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 90d2c4d2..8760c78d 100644 --- a/scripts/repro/rv32_label_882_differential.py +++ b/scripts/repro/rv32_label_882_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 15 """#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 b9ab74ea..96ecd2ae 100644 --- a/scripts/repro/rv32_local_promotion_472_riscv_differential.py +++ b/scripts/repro/rv32_local_promotion_472_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 12 """#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 20caa0fc..8ddca3ab 100644 --- a/scripts/repro/rv32_mem_size_grow_242_differential.py +++ b/scripts/repro/rv32_mem_size_grow_242_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 3 """#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 b7551a17..1f8aeb74 100644 --- a/scripts/repro/safety_bounds_377_differential.py +++ b/scripts/repro/safety_bounds_377_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 38 """#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 ba2784f5..52172010 100755 --- a/scripts/repro/self_contained_data_758_differential.py +++ b/scripts/repro/self_contained_data_758_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 7 """#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 4394303e..c5f55b69 100644 --- a/scripts/repro/shift_fold_riscv_differential.py +++ b/scripts/repro/shift_fold_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 44 """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 45d81599..e9543ff3 100644 --- a/scripts/repro/signed_div_const_riscv_differential.py +++ b/scripts/repro/signed_div_const_riscv_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 5 """#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/spill_frame_499_differential.py b/scripts/repro/spill_frame_499_differential.py index d79fd5ab..ddc23a33 100644 --- a/scripts/repro/spill_frame_499_differential.py +++ b/scripts/repro/spill_frame_499_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 4 """#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 5b091f09..223b013e 100644 --- a/scripts/repro/spill_on_exhaust_242_differential.py +++ b/scripts/repro/spill_on_exhaust_242_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """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 69e4aebf..c577c08d 100644 --- a/scripts/repro/spill_rung_581_differential.py +++ b/scripts/repro/spill_rung_581_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 12 """#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 382b31d2..f74401f7 100644 --- a/scripts/repro/sret_decide_differential.py +++ b/scripts/repro/sret_decide_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 3 import struct, sys from elftools.elf.elffile import ELFFile from unicorn import Uc, UC_ARCH_ARM, UC_MODE_THUMB diff --git a/scripts/repro/stack_args_503_differential.py b/scripts/repro/stack_args_503_differential.py index 4b707d25..cf0c83ea 100644 --- a/scripts/repro/stack_args_503_differential.py +++ b/scripts/repro/stack_args_503_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 13 """#503 (epic #242) — EXECUTION-validate the AAPCS stack-argument path for functions with >8 scalar i32 params/args. diff --git a/scripts/repro/stack_layout_687_differential.py b/scripts/repro/stack_layout_687_differential.py index 782f4aaa..fdffac86 100644 --- a/scripts/repro/stack_layout_687_differential.py +++ b/scripts/repro/stack_layout_687_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 26 """#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 73607096..7010ed70 100644 --- a/scripts/repro/static_above_sp_739_differential.py +++ b/scripts/repro/static_above_sp_739_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 50c54e0b..62411570 100644 --- a/scripts/repro/trunc_sat_782_differential.py +++ b/scripts/repro/trunc_sat_782_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 192672 """#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 95fb9d90..5d63fb17 100644 --- a/scripts/repro/u64_unpack_differential.py +++ b/scripts/repro/u64_unpack_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 12 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 def3ba1a..caa6deb7 100755 --- a/scripts/repro/u64_unpack_if_differential.py +++ b/scripts/repro/u64_unpack_if_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 16 # #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 234ea375..27efe9ce 100644 --- a/scripts/repro/u64_unpack_riscv_differential.py +++ b/scripts/repro/u64_unpack_riscv_differential.py @@ -1,4 +1,5 @@ # ci-status: wired +# ci-checks: emulations >= 4 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 f6729036..fba9fa3d 100644 --- a/scripts/repro/unreachable_665_differential.py +++ b/scripts/repro/unreachable_665_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 5e706f30..f4eb82f4 100644 --- a/scripts/repro/uxth_fold_differential.py +++ b/scripts/repro/uxth_fold_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 14 """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 / diff --git a/scripts/repro/vcr_dec_001_graph_alloc_differential.py b/scripts/repro/vcr_dec_001_graph_alloc_differential.py index 45a5babe..db8355f1 100644 --- a/scripts/repro/vcr_dec_001_graph_alloc_differential.py +++ b/scripts/repro/vcr_dec_001_graph_alloc_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: compiles >= 27 """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 80aef49e..22b8421d 100644 --- a/scripts/repro/vcr_dec_001_join_alloc_execution_differential.py +++ b/scripts/repro/vcr_dec_001_join_alloc_execution_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 56 """VCR-DEC-001 increments 2+3 — EXECUTION differential for the join- and call-aware graph-colouring allocator (`SYNTH_GRAPH_ALLOC=1`, epic #242). diff --git a/scripts/repro/vcr_ra_003_phase2_join_call.py b/scripts/repro/vcr_ra_003_phase2_join_call.py index b0bfbc54..9648fe8f 100644 --- a/scripts/repro/vcr_ra_003_phase2_join_call.py +++ b/scripts/repro/vcr_ra_003_phase2_join_call.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: stdout /^checked (\d+) \(fixture, path\) pairs/ >= 16 """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 bbe2c7ba..2bd5125f 100644 --- a/scripts/repro/vcr_ra_003_rv32_alloc_validator.py +++ b/scripts/repro/vcr_ra_003_rv32_alloc_validator.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: stdout /^checked (\d+) \(fixture, path\) pairs/ >= 18 """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/vcr_ver_004_instrument_independence.py b/scripts/repro/vcr_ver_004_instrument_independence.py index 73659a05..589fefc6 100644 --- a/scripts/repro/vcr_ver_004_instrument_independence.py +++ b/scripts/repro/vcr_ver_004_instrument_independence.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: stdout /^VCR-VER-004-INDEPENDENCE ASSERTIONS=(\d+)/4$/ >= 4 """VCR-VER-004 — INSTRUMENT INDEPENDENCE, proven by re-running v0.53's mutation. **The finding this responds to.** v0.53's VCR-DEC-001 lane proved BY MUTATION diff --git a/scripts/repro/vcr_ver_004_shipping_path_audit.py b/scripts/repro/vcr_ver_004_shipping_path_audit.py index 53ffbf74..c63d16fd 100644 --- a/scripts/repro/vcr_ver_004_shipping_path_audit.py +++ b/scripts/repro/vcr_ver_004_shipping_path_audit.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: stdout /^VCR-VER-004-SHIPPING HOLDS=(\d+) / >= 400 """VCR-VER-004 — the ABI observable contract on the SHIPPING allocator (#242). The sibling script `vcr_ver_004_instrument_independence.py` proves the new diff --git a/scripts/repro/vfp_spill_881_differential.py b/scripts/repro/vfp_spill_881_differential.py index 53bd60ad..018905ce 100644 --- a/scripts/repro/vfp_spill_881_differential.py +++ b/scripts/repro/vfp_spill_881_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 109 """#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 988f7dbc..876ab42a 100644 --- a/scripts/repro/volatile_segment_543_differential.py +++ b/scripts/repro/volatile_segment_543_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 24 """#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/wcet_phase2_778_unicorn_soundness.py b/scripts/repro/wcet_phase2_778_unicorn_soundness.py index 2c4bbf0b..d4598b05 100644 --- a/scripts/repro/wcet_phase2_778_unicorn_soundness.py +++ b/scripts/repro/wcet_phase2_778_unicorn_soundness.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 8 """#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 f9d62f3c..40f0c106 100755 --- a/scripts/repro/wcet_phase3_778_compose_soundness.py +++ b/scripts/repro/wcet_phase3_778_compose_soundness.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 2 """#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 0e30ab3a..91e77593 100644 --- a/scripts/repro/wcet_phase4_49_recursion_soundness.py +++ b/scripts/repro/wcet_phase4_49_recursion_soundness.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 3 """#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 c9b1d57b..09299946 100755 --- a/scripts/repro/wcet_phase5_778_masked_loop_soundness.py +++ b/scripts/repro/wcet_phase5_778_masked_loop_soundness.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 12 """#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 0ab0d8f2..fd493c8f 100644 --- a/scripts/repro/wide_static_746_differential.py +++ b/scripts/repro/wide_static_746_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 25 """#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 f14b27dd..a71651c8 100644 --- a/scripts/repro/wide_static_copy_757_differential.py +++ b/scripts/repro/wide_static_copy_757_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 11 """#757 investigation harness — the multi-chunk static-copy differential. #757 reported a SILENT MISCOMPILE regression from the #746 fix: a chunked copy diff --git a/vcr_ver_004.out b/vcr_ver_004.out new file mode 100644 index 00000000..ddc915e0 --- /dev/null +++ b/vcr_ver_004.out @@ -0,0 +1 @@ +ORACLE-CALIBRATION script=vcr_ver_004_instrument_independence.py emulations=0 wasmtime_calls=0 compiles=0 exit=1 secs=0.3 diff --git a/vcr_ver_004_ship.out b/vcr_ver_004_ship.out new file mode 100644 index 00000000..aa01eb99 --- /dev/null +++ b/vcr_ver_004_ship.out @@ -0,0 +1,12 @@ +functions audited (--relocatable) : 633 + Holds : 431 + NotAttempted : 202 + Violated : 0 +decline reasons: + unmodeled-op 175 + indirect-call-pseudo-op 17 + numeric-offset-branch 10 + +VCR-VER-004-SHIPPING HOLDS=431 VIOLATED=0 TOTAL=633 FLOOR=400 +RESULT: PASS +ORACLE-CALIBRATION script=vcr_ver_004_shipping_path_audit.py emulations=0 wasmtime_calls=0 compiles=161 exit=0 secs=1.6 diff --git a/vfp881.out b/vfp881.out new file mode 100644 index 00000000..9b06c883 --- /dev/null +++ b/vfp881.out @@ -0,0 +1,3 @@ +PASS: all 7 exports emitted (nm -> T) under -t cortex-m7dp --relocatable +PASS: 109 execution rows bit-identical to wasmtime (unicorn, cortex-m7dp, spilled VFP paths) +ORACLE-CALIBRATION script=vfp_spill_881_differential.py emulations=109 wasmtime_calls=109 compiles=1 exit=0 secs=0.2 From 72a7797824d0a277d163591d2f7282a5d99583f5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:37:46 +0200 Subject: [PATCH 4/9] =?UTF-8?q?feat(#910):=20the=20check-floor=20ledger=20?= =?UTF-8?q?=E2=80=94=20report=20the=20population,=20ratchet=20the=20floor?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two gates on top of the per-step floors: 1. `oracle_wiring_check.py` now also requires a `# ci-checks:` declaration on every `wired` oracle, and sums the floors PER MODE. It shares the driver's parser by importing it (`_load_oracle_run`) rather than re-implementing the grammar — two hand-maintained copies of one declaration format is the mirror-drift shape this repo keeps paying for. `--min-emulation-floor 294914` is the RATCHET, wired into the existing (required) `Claim Check` job rather than a new job — a brand-new job is not a required context on main and could sit red for weeks, which is the exact failure #890 exists to kill. Anti-vacuity in the gate itself: zero declared emulation floor is a hard failure, not a clean sheet. 2. `scripts/oracle_evidence.py` closes every oracle job with what it MEASURED, from the JSONL the driver appends to ($ORACLE_EVIDENCE_JSONL, set at workflow level so no oracle job can forget it). It asserts every record met its floor AND that the expected number of oracles reported at all — a step deleted, commented out or skipped by an early exit leaves the ledger short, and a short ledger is a red job rather than a quietly smaller number. Wired into 37 oracle jobs with their own `--min-oracles` count. REPORTED PER UNIT, NEVER SUMMED ACROSS UNITS. Emulator entries, wasmtime reference executions and compilations are three different things; one impressive combined figure is precisely the defect #910 is about. Both step summaries say so, and say that none of it is visible to `Rust-test Line Coverage` — the two populations are reported side by side and never added. Both directions exercised locally: --min-oracles 2 green on a 2-record ledger, --min-oracles 3 red on the same ledger with the reason printed. --- .github/workflows/ci.yml | 429 ++++++++++++++++++++++++++++++++- .gitignore | 1 + scripts/oracle_evidence.py | 106 ++++++++ scripts/oracle_wiring_check.py | 112 +++++++++ 4 files changed, 647 insertions(+), 1 deletion(-) create mode 100644 scripts/oracle_evidence.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e941bb50..9bf4cab6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -8,6 +8,10 @@ on: env: CARGO_TERM_COLOR: always + # #910: where scripts/oracle_run.py appends one JSON record per oracle it + # drives. Workflow-level so no oracle job can forget it; jobs that run no + # oracle simply never create the file. + ORACLE_EVIDENCE_JSONL: oracle-evidence.jsonl jobs: test: @@ -201,10 +205,19 @@ jobs: # * 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. + # #910 adds `--min-emulation-floor`: the summed `# ci-checks: emulations` + # floors, i.e. the emulator entries the wired oracle surface ASSERTS on + # every CI run. It is a RATCHET (direction: up) and a separate population + # from the `Rust-test Line Coverage` percentage — which cannot see any of + # it, because the oracles run the compiler as an uninstrumented + # subprocess from other jobs. The literal below is pinned in claims.yaml + # against the same number in scripts/repro/ORACLE_WIRING.md, so the gate + # and the doc cannot drift apart. - 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 \ + --min-emulation-floor 294914 \ | tee /tmp/oracle-wiring.log python3 - <<'PY' import json, sys @@ -213,12 +226,18 @@ jobs: ("wired==0", s["wired"] < 1), ("undeclared", s["undeclared"]), ("wired_unreferenced", s["wired_unreferenced"]), + ("checks_undeclared", s["checks_undeclared"]), + ("emulation_floor<100000", + s["emulation_floor"] < 100000), ("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.") + f"{s['unwired']} unwired-debt, 0 inert, and every wired oracle " + f"declares a check floor ({s['emulation_floor']} emulator " + f"entries asserted across " + f"{s['checks_by_mode']['emulations']['scripts']} of them).") PY # The GitHub About surface (description + topics) is pinned verbatim in # claims.yaml's repo_metadata section. API/network failure = LOUD SKIP @@ -472,6 +491,17 @@ jobs: run: pip install wasmtime unicorn pyelftools - name: Run two-move execution oracle run: python scripts/oracle_run.py scripts/repro/cmp_select_two_move_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 provenance-gate: name: synth-provenance-v1 reconciliation gate (#396) @@ -632,6 +662,17 @@ jobs: [ "$t" -ge 40 ] - name: Run decline-matrix honesty oracle run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_m2_decline_538.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 15 aarch64-native-matrix: name: aarch64 native execution matrix (gale #851 acceptance gate) @@ -699,6 +740,17 @@ jobs: SYNTH=./target/debug/synth \ WASMTOOLS=wasm-tools WASMTIME=wasmtime \ python scripts/oracle_run.py scripts/repro/aarch64_calls_851.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 trap-semantics-oracle: name: trap-semantics oracle (#665 unreachable + #666 rem_s) @@ -1063,6 +1115,17 @@ jobs: run: sudo apt-get update && sudo apt-get install -y clang lld - name: Run RV32 data-segment full-boot oracle (#798, rv32imac) run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/rv32_data_798_boot_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 30 instrument-independence-oracle: name: VCR-VER-004 instrument independence (#242, v0.53's mutation re-run) @@ -1135,6 +1198,17 @@ jobs: test "$(grep -c '^OK ' vcr_ver_004.out)" -eq 5 - name: Assert the tree was restored (the mutation must never persist) run: git diff --exit-code + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 2 fact-spec-oracle: name: fact-spec elision oracle (#494 phases 2 + 2b + 3+ + bounds) @@ -1248,6 +1322,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/fact_spec_rem_494_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 6 rv32-shift-fold-oracle: name: rv32 immediate-shift-fold execution oracle @@ -1283,6 +1368,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/shift_fold_riscv_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 rv32-const-addr-fold-oracle: name: rv32 const-address-fold execution oracle @@ -1317,6 +1413,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/const_addr_fold_riscv_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 rv32-br-table-oracle: name: rv32 br_table execution oracle (#882) @@ -1355,6 +1462,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/rv32_br_table_882_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 rv32-extern-call-reloc-oracle: name: rv32 external-call relocation oracle (#871) @@ -1395,6 +1513,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/riscv_extern_call_871_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 rv32-label-return-oracle: name: rv32 label/return dead-code oracle (#882) @@ -1439,6 +1568,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/rv32_label_882_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 rv32-mem-size-grow-oracle: name: rv32 memory.size / memory.grow execution oracle @@ -1473,6 +1613,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/rv32_mem_size_grow_242_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 callee-saved-490-oracle: name: optimized-path callee-saved preservation oracle @@ -1510,6 +1661,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/callee_saved_490_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 call-indirect-642-oracle: name: call_indirect bounds-guard oracle (Thumb-2 + A32) @@ -1549,6 +1711,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/call_indirect_642_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 call-indirect-650-multitable-oracle: name: multi-table call_indirect oracle (Thumb-2 + A32) @@ -1589,6 +1762,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/call_indirect_650_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 call-indirect-664-nullslot-oracle: name: null-funcref-slot call_indirect oracle (Thumb-2 + A32) @@ -1634,6 +1818,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/call_indirect_664_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 call-indirect-676-heterogeneous-oracle: name: heterogeneous-table call_indirect oracle (Thumb-2 + A32) @@ -1683,6 +1878,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/call_indirect_676_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 call-indirect-275-selfcontained-oracle: name: self-contained call_indirect oracle (execution + residual declines) @@ -1732,6 +1938,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/call_indirect_275_selfcontained_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 2 block-brif-483-oracle: name: optimized-path block/br_if lowering oracle @@ -1770,6 +1987,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/block_brif_483_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 spill-frame-499-oracle: name: optimized-path spill-frame teardown oracle @@ -1808,6 +2036,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/spill_frame_499_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 r12-spill-496-oracle: name: optimized-path register-exhaustion oracle @@ -1848,6 +2087,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/r12_spill_496_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 flight-seam-570-oracle: name: flight-seam relocatable-path execution oracle @@ -1891,6 +2141,17 @@ jobs: -o /tmp/fsf.elf --target cortex-m4 --all-exports --relocatable python scripts/oracle_run.py scripts/repro/flight_seam_differential.py /tmp/fsf.elf \ scripts/repro/flight_seam_flat.wasm + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 control-step-584-oracle: name: control-step relocatable-path execution oracle @@ -1931,6 +2192,17 @@ jobs: ./target/debug/synth compile scripts/repro/control_step.wasm \ -o /tmp/cs.elf --target cortex-m4 --all-exports --relocatable python scripts/oracle_run.py scripts/repro/control_step_differential.py /tmp/cs.elf + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 stack-args-503-oracle: name: AAPCS stack-argument path oracle @@ -1970,6 +2242,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/stack_args_503_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 i64-completeness-503-587-oracle: name: i64 stack-param + spill-pool-grow oracle @@ -2022,6 +2305,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/framebacking_i64param_837_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 4 i64-rot-div-610-oracle: name: i64 rotl/rotr/div/rem expansion oracle @@ -2058,6 +2352,17 @@ jobs: run: pip install wasmtime unicorn pyelftools - name: Run i64 rot/div/rem expansion oracle (#610) run: python scripts/oracle_run.py scripts/repro/i64_rot_div_610_differential.py target/debug/synth + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 br-table-507-oracle: name: optimized-path br_table oracle @@ -2097,6 +2402,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/br_table_507_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 const-cse-242-oracle: name: const-CSE flag-on execution oracle @@ -2135,6 +2451,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/const_cse_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 frame-slot-dce-242-oracle: name: frame-slot DCE default+optout execution oracle @@ -2173,6 +2500,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/frame_slot_dce_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 stack-layout-687-oracle: name: stack-layout=low overflow BusFault oracle @@ -2226,6 +2564,18 @@ jobs: # (pointer-independent observables; exhaustion traps on both sides). The # `--relocatable` undefined-symbol seam (#420) is asserted untouched by # cabi_arena_realloc_linkability_418.rs in the `test` job. + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 2 + arena-bind-418-oracle: name: "#418 arena-bind self-contained execution oracle" runs-on: ubuntu-latest @@ -2253,6 +2603,17 @@ jobs: env: SYNTH: ./target/debug/synth run: python scripts/oracle_run.py scripts/repro/cabi_arena_bind_418_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 vcr-ra-003-alloc-validator-gate: name: "VCR-RA-003 register-allocation validator (red-first + frozen)" @@ -2305,6 +2666,17 @@ jobs: run: | cargo build -p synth-cli python3 scripts/oracle_run.py scripts/repro/vcr_ra_003_phase2_join_call.py ./target/debug/synth + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 vcr-ra-003-rv32-alloc-validator-gate: name: "VCR-RA-003 RV32 register-allocation validator (red-first + frozen)" @@ -2361,6 +2733,17 @@ jobs: run: | cargo build -p synth-cli python3 scripts/oracle_run.py scripts/repro/vcr_ra_003_rv32_alloc_validator.py ./target/debug/synth + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1 vcr-sel-005-cross-backend-op-parity-gate: name: "VCR-SEL-005 cross-backend op-parity (universe-complete + red-first)" @@ -2538,6 +2921,17 @@ jobs: python scripts/oracle_run.py scripts/repro/u64_unpack_if_differential.py - name: uxth/uxtb fold differential (#428, both flag states) run: python scripts/oracle_run.py scripts/repro/uxth_fold_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 32 repro-sweep-memory-oracle: name: repro sweep — linear memory / static data / native-pointer differentials @@ -2615,6 +3009,17 @@ jobs: 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/oracle_run.py scripts/repro/postlink_359_oracle.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 15 repro-sweep-rv32-oracle: name: repro sweep — RISC-V RV32 execution differentials @@ -2691,6 +3096,17 @@ jobs: 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/oracle_run.py scripts/repro/u64_unpack_riscv_differential.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 11 repro-sweep-wcet-oracle: name: repro sweep — WCET bound soundness cross-checks (phases 2-5) @@ -2737,3 +3153,14 @@ jobs: run: python scripts/oracle_run.py scripts/repro/wcet_phase4_49_recursion_soundness.py - name: WCET phase-5 masked-ceiling loop soundness (#778) run: python scripts/oracle_run.py scripts/repro/wcet_phase5_778_masked_loop_soundness.py + # #910: close the job with what it EXECUTED. Asserts every oracle + # met its declared floor AND that the expected number of them + # reported at all — a step deleted, commented out, or skipped by an + # early exit leaves the ledger short, which is a red job rather than + # a quietly smaller number. Also writes the measured totals to the + # step summary, per unit, never summed. + - name: Differential evidence ledger (#910) + if: always() + run: | + set -euo pipefail + python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 4 diff --git a/.gitignore b/.gitignore index d886e0eb..0d82973f 100644 --- a/.gitignore +++ b/.gitignore @@ -73,3 +73,4 @@ result-* /*.elf output.elf __pycache__/ +oracle-evidence.jsonl diff --git a/scripts/oracle_evidence.py b/scripts/oracle_evidence.py new file mode 100644 index 00000000..7c2d490f --- /dev/null +++ b/scripts/oracle_evidence.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""oracle_evidence — close out an oracle job with what it actually EXECUTED. + +Per-step floors (scripts/oracle_run.py) answer "did this oracle run?". This +answers the job-level question #910 asks: **report the differential population +in its own unit instead of folding it into a coverage percentage.** + +It reads the JSONL ledger the driver appended to during the job and + + * asserts every record passed AND the expected number of oracles reported — + a step that vanished (deleted, commented out, short-circuited by an earlier + `exit`) leaves the ledger short, and a short ledger is a red job, not a + quietly smaller number; + * writes the job's measured totals to `$GITHUB_STEP_SUMMARY`. + +Reported PER UNIT, never as one figure: emulator entries, wasmtime reference +executions and compilations are three different things. Summing them would +manufacture exactly the kind of impressive-but-meaningless total this lane +exists to remove. + +Exit: 0 = ledger complete and every oracle met its floor · 1 = otherwise. +""" + +import argparse +import json +import os +import pathlib +import sys + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + ap.add_argument("ledger", help="the JSONL written via $ORACLE_EVIDENCE_JSONL") + ap.add_argument( + "--min-oracles", + type=int, + required=True, + metavar="N", + help="how many oracle records this job must have filed", + ) + ap.add_argument("--job", default=os.environ.get("GITHUB_JOB", "oracle job")) + args = ap.parse_args() + + p = pathlib.Path(args.ledger) + if not p.exists(): + sys.exit( + f"oracle_evidence: no ledger at {args.ledger} — the job ran NO " + f"instrumented oracle. Either the steps are not routed through " + f"scripts/oracle_run.py, or $ORACLE_EVIDENCE_JSONL is unset." + ) + + records = [json.loads(line) for line in p.read_text().splitlines() if line.strip()] + if not records: + sys.exit(f"oracle_evidence: ledger {args.ledger} is EMPTY — nothing ran.") + + fails = [r for r in records if not r.get("ok")] + scripts = {r["script"] for r in records} + tot_emu = sum(r.get("emulations", 0) for r in records) + tot_wasm = sum(r.get("wasmtime_calls", 0) for r in records) + tot_comp = sum(r.get("compiles", 0) for r in records) + + print( + f"ORACLE-LEDGER job={args.job} oracles={len(scripts)} runs={len(records)} " + f"emulations={tot_emu} wasmtime_calls={tot_wasm} compiles={tot_comp} " + f"below_floor={len(fails)}" + ) + + step_summary = os.environ.get("GITHUB_STEP_SUMMARY") + if step_summary: + with open(step_summary, "a") as fh: + fh.write(f"### Differential evidence — `{args.job}` (#910)\n\n") + fh.write("| unit | measured |\n|---|---|\n") + fh.write(f"| oracles run | {len(scripts)} |\n") + fh.write(f"| emulator entries | {tot_emu} |\n") + fh.write(f"| wasmtime reference executions | {tot_wasm} |\n") + fh.write(f"| compilations | {tot_comp} |\n\n") + fh.write( + "Three units, reported separately on purpose. None of this is " + "visible to `Rust-test Line Coverage`: these oracles run the " + "compiler as an uninstrumented subprocess, in this job, not " + "under `cargo llvm-cov`.\n\n" + ) + + problems = [] + if len(scripts) < args.min_oracles: + problems.append( + f"ledger SHORT: {len(scripts)} distinct oracles reported, expected " + f">= {args.min_oracles}. A step is missing, commented out, or the " + f"job exited early — its gate is inert (#890)." + ) + for r in fails: + problems.append( + f"{r['script']}: below floor — mode={r.get('mode')} " + f"floor={r.get('floor')} measured={r.get('measured')} " + f"exit={r.get('exit')}" + ) + if problems: + print() + for f in problems: + print(f"FAIL {f}", file=sys.stderr) + return 1 + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/oracle_wiring_check.py b/scripts/oracle_wiring_check.py index 6ce07fd6..5e329344 100644 --- a/scripts/oracle_wiring_check.py +++ b/scripts/oracle_wiring_check.py @@ -88,6 +88,27 @@ "slow": "runtime is prohibitive for per-PR CI", } +def _load_oracle_run(): + """Import the `# ci-checks:` parser from its owner, by path. + + Deliberately NOT a re-implementation: two hand-maintained copies of a + declaration grammar are the mirror-drift shape this repo keeps paying for. + The driver that ENFORCES the floor and the gate that SUMS the floors must + read the header the same way, so they share one parser. + """ + import importlib.util + + p = pathlib.Path(__file__).resolve().parent / "oracle_run.py" + spec = importlib.util.spec_from_file_location("oracle_run", p) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +_ORACLE_RUN = _load_oracle_run() +parse_checks_decl = _ORACLE_RUN.parse_decl + + DECL_RE = re.compile( r"^#\s*ci-status:\s*(?P[A-Za-z-]+)" r"(?:\s*\((?P[a-z-]+)\))?" @@ -205,6 +226,23 @@ def classify(root, scripts, workflows): } records.append(rec) + # ------------------------------------------------------------------ + # #910 F10 — the SECOND declaration. `ci-status` says a step runs the + # oracle; it says NOTHING about what that step attests. 152 of 160 + # oracle steps asserted only the process exit code, and exit 0 does not + # distinguish "emulated 240 vectors" from "the loop never ran". So a + # `wired` oracle must also declare a FLOOR that scripts/oracle_run.py + # enforces at run time. Only `wired` scripts: a manual/unwired oracle + # has no run to measure. + # ------------------------------------------------------------------ + if status == "wired": + decl, err = parse_checks_decl(text, rel) + if err: + fails.append(err) + else: + rec["checks_mode"] = decl.mode + rec["checks_floor"] = decl.minimum + if status == "wired": if not refs: mentioned = [w for w, t in wf_raw.items() if name in t] @@ -285,6 +323,30 @@ def summarize(records): out["wired_unreferenced"] = sum( 1 for r in records if r["status"] == "wired" and not r["workflows"] ) + + # ------------------------------------------------------------------ + # #910 — the CHECK-FLOOR ledger, reported PER MODE and never summed + # across modes. Emulator entries, compilations and printed counts are + # three different units; adding them would produce one impressive number + # that means nothing, which is the defect this lane exists to fix (the + # coverage percentage that silently spanned two populations). The + # emulations floor is the one that ratchets. + # ------------------------------------------------------------------ + modes = {} + for r in records: + if r["status"] != "wired": + continue + m = r.get("checks_mode") + if not m: + continue + e = modes.setdefault(m, {"scripts": 0, "floor": 0}) + e["scripts"] += 1 + e["floor"] += r.get("checks_floor", 0) + out["checks_by_mode"] = dict(sorted(modes.items())) + out["checks_undeclared"] = sum( + 1 for r in records if r["status"] == "wired" and not r.get("checks_mode") + ) + out["emulation_floor"] = modes.get("emulations", {}).get("floor", 0) return out @@ -292,6 +354,13 @@ 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") + ap.add_argument( + "--min-emulation-floor", + type=int, + metavar="N", + help="fail if the summed `ci-checks: emulations` floors drop below N " + "(the #910 ratchet; direction is UP)", + ) args = ap.parse_args() root = repo_root() @@ -317,6 +386,24 @@ def main(): "derivation is broken (did the workflow layout move?)" ) + # #910: the check-floor ledger, and its own anti-vacuity. A run in which + # NOTHING declares an emulation floor has not measured the population it + # claims to; that is a broken derivation, not a clean sheet. + if summary["emulation_floor"] == 0: + fails.append( + "VACUOUS — no `wired` oracle declares `ci-checks: emulations`; the " + "execution population is unmeasured." + ) + if args.min_emulation_floor is not None: + if summary["emulation_floor"] < args.min_emulation_floor: + fails.append( + f"check-floor RATCHET BROKEN: summed `ci-checks: emulations` " + f"floors {summary['emulation_floor']} < recorded minimum " + f"{args.min_emulation_floor}. An oracle lost execution, or a " + f"floor was lowered. Lower the ledger only when the evidence " + f"genuinely weakened — never to green a build." + ) + 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 "") @@ -334,6 +421,14 @@ def main(): " manual by category: " + ", ".join(f"{k}={v}" for k, v in summary["manual_by_category"].items()) ) + # Per mode, never summed across modes — three different units. + for mode, e in summary["checks_by_mode"].items(): + print( + f" ci-checks {mode:<11} {e['scripts']:>4} scripts, " + f"floor total {e['floor']}" + ) + if summary["checks_undeclared"]: + print(f" ci-checks UNDECLARED: {summary['checks_undeclared']}") summary["failures"] = len(fails) @@ -364,6 +459,23 @@ def main(): fh.write(f"- `{os.path.basename(r['script'])}` — {r['reason']}\n") fh.write("\n") + fh.write("### Oracle check floors (#910)\n\n") + fh.write( + "What each wired oracle ASSERTS beyond exit 0, enforced per run " + "by `scripts/oracle_run.py`. Reported per mode and **not summed " + "across modes** — emulator entries, compilations and printed " + "counts are three different units.\n\n" + ) + fh.write("| mode | oracles | floor total |\n|---|---|---|\n") + for mode, e in summary["checks_by_mode"].items(): + fh.write(f"| `{mode}` | {e['scripts']} | {e['floor']} |\n") + fh.write( + "\nThis is a separate population from the " + "`Rust-test Line Coverage` percentage, which cannot see any of " + "it (the oracles run the compiler as an uninstrumented " + "subprocess, from other jobs). Do not add them together.\n\n" + ) + if fails: print() for f in fails: From a6c9de17b68a5c3dbf81533d2b843adf931ef1e6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:40:43 +0200 Subject: [PATCH 5/9] =?UTF-8?q?docs(#910):=20pin=20the=20two=20populations?= =?UTF-8?q?=20=E2=80=94=20ledger,=20policy=20doc,=20CHANGELOG?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit claims.yaml gains four entries, all pinned to CAPABILITY GAPS rather than issue numbers (the v0.53 burn: a ledger pinned to a CLOSED issue green-confirms a false residual, and correcting the prose then turns it RED): SYNTH-ORACLE-CHECK-FLOORS-910 — every wired oracle carries a floor (count-min 150), the execution population does not shrink (count-min 133), and the "nothing can be bound" hatch stays at ONE (count-max 1) SYNTH-ORACLE-CHECK-FLOORS-910-CI — the doc's number and the number the gate ENFORCES cannot drift, and the routing cannot be quietly undone (count-min 159 routed steps, 37 job ledgers) SYNTH-COVERAGE-SCOPE-910 — the scope caveat cannot be dropped while SYNTH-COVERAGE-SCOPE-910-README the percentage stays quotable ORACLE_WIRING.md gains the whole #910 half: the mechanism, why a driver instead of 152 greps, why #910 option 1 was declined, the declaration grammar, the CALIBRATION table (four self-reporting oracles agreeing 1:1), the per-mode floor table, the "this is not the coverage percentage and must never be added to it" section, and the itemized weak-floor list. The FEATURE_MATRIX template (a source file) drops the now-closed "the sweeps assert exit status rather than a per-script check count" residual and states both #910 outcomes; docs/status/FEATURE_MATRIX.md regenerated via --emit-status, never hand-edited. 41/41 claims hold. --- CHANGELOG.md | 75 +++++++++++ claims.yaml | 98 ++++++++++++++ docs/status/FEATURE_MATRIX.md | 24 +++- scripts/repro/ORACLE_WIRING.md | 157 +++++++++++++++++++++++ scripts/templates/feature_matrix.md.tmpl | 24 +++- 5 files changed, 374 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c77dba86..b2010a82 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,81 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Changed + +- **The evidence now says what it measures (#910).** `Code Coverage` was red + repo-wide until v0.54 fixed a test binary-path bug. Green and quotable, it was + structurally misleading: it runs `cargo llvm-cov --workspace`, i.e. the Rust + test suite in process, while this project's strongest evidence — the execution + differentials — spawns the compiler as a separate, **uninstrumented** process + from **other CI jobs**, emitting no profile data at all. So + `synth-backend-aarch64/src/backend.rs` reads 41.6 % and + `instruction_selector.rs` 42.7 % while both are exercised end-to-end + constantly. The number understates real testing *and* cannot be read as + completeness. Renamed to **`Rust-test Line Coverage (unit + integration + only)`**, with the scope caveat carried in three places that travel with the + number (the job body, `$GITHUB_STEP_SUMMARY`, the README badge) and pinned in + `claims.yaml` so it cannot be dropped while the percentage stays quotable. + #910 option 1 — instrumenting the binary the differentials run — was + **declined**: it changes the artifact under test (these oracles exist to + execute the *shipped* bytes) and buys precision on an axis that is still the + wrong completeness instrument. + +### Added + +- **Oracle steps assert EXECUTION, not exit status (#910 F10).** Measured first, + and the premise was understated: not the 63 oracles #890 wired, but **152 of + the 160** workflow steps that run a `scripts/repro/` oracle asserted nothing + beyond the process exit code — the pre-#890 hand-wired steps included; exactly + 8 asserted a printed verdict or count. Exit 0 cannot tell *"emulated 240 + vectors, all bit-identical to wasmtime"* from *"the fixture list came back + empty, printed PASS"* — #890's inert gate one level down. + + `scripts/oracle_run.py` is an in-process driver (`runpy`) that wraps + `unicorn.Uc.emu_start`, `wasmtime.Func.__call__` and `subprocess` `synth … + compile …`, so the count comes from the emulator rather than the harness's own + bookkeeping — a comparison loop that never runs cannot fake it. 159 CI step + lines now route through it, and **no harness was edited**. Chosen over 152 + bespoke greps (152 patterns to keep in sync with 150 harnesses' output strings + is the mirror-drift shape this repo keeps paying for). + + Each `wired` oracle declares a `# ci-checks:` floor next to its `# ci-status:` + line — same locality argument, enforced per run, `>=` never equality so + adding a fixture cannot redden a step. **Every floor is measured**, obtained + by executing each CI step *verbatim* out of `ci.yml`. The four oracles that + self-report a check count agree with the driver **1:1** (`#846 CHECKS=75/75` + → 75; `35 checks (23 trap, 12 value)` → 35; `17 checks` → 17; the 662 + float-boundary checks → 662) — and the counter is still called `emulations`, + not "checks", because naming a measurement after something it does not measure + is the defect this lane exists to remove. + +- **The differential population is reported, and ratcheted.** **133 oracles + assert 294,914 emulator entries per CI run**; 7 assert a printed count, 9 + assert compilations, 1 can bind to nothing. Reported **per mode and never + summed across modes** — three different units, and one impressive combined + figure is exactly the instrument defect being fixed. + `oracle_wiring_check.py --min-emulation-floor 294914` enforces the total in + the already-required `Claim Check` job (a brand-new job is not a required + context on `main` and could sit red for weeks — the #890 failure), sharing the + driver's header parser by import rather than re-implementing the grammar. + `scripts/oracle_evidence.py` closes each of 37 oracle jobs with what it + *measured*, asserting every record met its floor and that the expected number + of oracles reported at all — a step deleted, commented out or skipped by an + early exit leaves the ledger short and reddens the job instead of quietly + shrinking the number. + +- **The weak floors are itemized, not averaged away** + (`scripts/repro/ORACLE_WIRING.md`): `aarch64_matrix.sh` (a POSIX shell oracle + the in-process driver cannot instrument — its step already carries its own + `>= 32 accepted ops` assertion), `i64_param_518_riscv_loudskip.py` and + `postlink_359_oracle.py` (`compiles >= 1`; a loud-skip contract and a + link-layout assertion, neither of which executes by design), the five + `fact_spec_*` differentials (`compiles >= 2`; each has a `--expect-decline` + leg that emulates nothing, and a floor that only holds for the good leg is not + a floor), `call_indirect_275_selfcontained_differential.py` (`compiles >= 4`), + and the #275 RED non-vacuity step, deliberately not routed because it inverts + its verdict. + ## [0.54.0] - 2026-08-05 **"Close what we measured."** v0.53 built the instruments; this release acts on diff --git a/claims.yaml b/claims.yaml index 094a94ca..48ea15fd 100644 --- a/claims.yaml +++ b/claims.yaml @@ -1008,3 +1008,101 @@ claims: text: "**7 manual**" - kind: verbatim text: "**0 unwired**" + + # --------------------------------------------------------------------------- + # #910 — what a wired oracle ATTESTS. SYNTH-ORACLE-WIRING-890 above pins that + # a step RUNS each oracle; it says nothing about what that step checks, and + # measured on the #890 result, 152 of 160 oracle steps asserted only the + # process exit code. Exit 0 cannot tell "emulated 240 vectors" from "the loop + # never ran", so every `wired` oracle now declares a `# ci-checks:` floor that + # scripts/oracle_run.py enforces per run. + # + # The CAPABILITY pinned here (deliberately not an issue number — a ledger + # pinned to a closed issue green-confirms a false residual, the v0.53 burn): + # + # * every wired oracle carries a floor — count-min 150 declarations + # * the execution population does not shrink — count-min 133 `emulations` + # declarations, and the summed + # floor is ratcheted in CI by + # --min-emulation-floor + # * the `none` escape hatch stays at ONE — count-max 1. A second oracle + # that can bind to nothing needs + # a conversation, not a commit. + # + # Floors are `>=`, so adding a fixture cannot redden a step; the ratchet + # direction is UP. Lower the recorded minimum only when the evidence genuinely + # weakened — never to green a build. + # --------------------------------------------------------------------------- + - id: SYNTH-ORACLE-CHECK-FLOORS-910 + doc: scripts/repro/ORACLE_WIRING.md + text: "**294,914 emulator entries**" + evidence: + - kind: file-exists + path: scripts/oracle_run.py + - kind: file-exists + path: scripts/oracle_evidence.py + - kind: count-min # every wired oracle declares a floor + pattern: '^# ci-checks: ' + glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] + min: 150 + - kind: count-min # the EXECUTION population, per script + pattern: '^# ci-checks: emulations >= ' + glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] + min: 133 + - kind: count-max # the "nothing can be bound" hatch + pattern: '^# ci-checks: none' + glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] + max: 1 + - kind: verbatim # the doc carries the per-mode split + text: "**133 oracles**" + - kind: verbatim + text: "Reported per mode and never summed across modes." + - kind: verbatim # the itemized weak-floor list stays + text: "## The oracles whose floor is weak, itemized" + + # --------------------------------------------------------------------------- + # #910 — the CI side of the same claim, pinned so the doc's number and the + # number the gate actually enforces cannot drift apart, and so the routing + # cannot be quietly undone (unrouting a step would restore exit-status-only + # assertion while every other surface still claimed a floor). + # --------------------------------------------------------------------------- + - id: SYNTH-ORACLE-CHECK-FLOORS-910-CI + doc: .github/workflows/ci.yml + text: "--min-emulation-floor 294914" + evidence: + - kind: count-min # oracle steps routed through the driver + pattern: 'oracle_run\.py scripts/repro/' + glob: ['.github/workflows/*.yml'] + min: 159 + - kind: count-min # per-job measured-evidence ledgers + pattern: 'oracle_evidence\.py' + glob: ['.github/workflows/*.yml'] + min: 37 + - kind: verbatim + text: "ORACLE_EVIDENCE_JSONL: oracle-evidence.jsonl" + + # --------------------------------------------------------------------------- + # #910 — the coverage instrument says its SCOPE. The job was `Code Coverage`, + # a name implying whole-system coverage for a measurement of the Rust test + # suite alone; the differentials spawn an UNINSTRUMENTED subprocess from other + # jobs and are structurally invisible to it. Pinned so the scope caveat cannot + # be dropped while the number stays quotable — a green-but-meaningless number + # is worse than a red one. + # --------------------------------------------------------------------------- + - id: SYNTH-COVERAGE-SCOPE-910 + doc: .github/workflows/ci.yml + text: "name: Rust-test Line Coverage (unit + integration only)" + evidence: + - kind: verbatim # the caveat travels WITH the number + text: "**Do not add them together.**" + - kind: verbatim + text: "UNINSTRUMENTED process" + + - id: SYNTH-COVERAGE-SCOPE-910-README + doc: README.md + text: "Rust-test line coverage only" + evidence: + - kind: verbatim # the badge alt-text matches the scope + text: "[![Rust-test line coverage]" + - kind: verbatim + text: "It understates the testing that exists and is not a completeness measure" diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index dd21747c..29a1c829 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -136,11 +136,31 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. oracle-wiring gate now leaves 0 undeclared and 0 unwired scripts, so a forgotten gate is no longer indistinguishable from a deliberately manual one — what remains open is the 7 `manual` scripts (external fixture, measurement - and scratch categories) and the fact that the newly-wired sweeps assert exit - status rather than a per-script non-zero check count; #851: the aarch64 + and scratch categories); #851: the aarch64 op-surface gaps the VCR-SEL-005 third-backend oracle now enumerates mechanically; #846: two `gpio-thin` CRL/CRH sites still need relational ranges). +- **What the oracle steps ATTEST is now stated (#910).** The exit-status-only + residual noted above was measured and was larger than described: **152 of the + 160** workflow steps that run a `scripts/repro/` oracle asserted nothing + beyond the process exit code — the pre-#890 hand-wired steps too, not only + the newly wired ones; exactly 8 asserted a printed verdict or count. Every + `wired` oracle now declares a `# ci-checks:` floor that + `scripts/oracle_run.py` enforces per run by counting real emulator entries, + wasmtime executions and compilations: **133 oracles assert 294,914 emulator + entries**, 7 assert a printed count, 9 assert compilations, and 1 + (`aarch64_matrix.sh`, a POSIX shell oracle the in-process driver cannot + instrument) is itemized as unbindable in `scripts/repro/ORACLE_WIRING.md` + alongside the five other weak floors. +- **The `Code Coverage` percentage was renamed for what it measures (#910).** + It is `Rust-test Line Coverage (unit + integration only)`: `cargo llvm-cov + --workspace`, the Rust test suite, in process. It is structurally blind to + the execution differentials, which spawn the compiler as a separate + UNINSTRUMENTED process from other jobs — which is why + `synth-backend-*/src/backend.rs` reads ~42 % while being exercised + end-to-end by nearly every differential. The number understates the testing + that exists and is not a completeness measure. The two populations are + reported separately, in their own units, and are never added together. - Two residuals live in code comments rather than issues, and are restated here so they are not implied away: `validate_segment_rewrite` does NOT catch a recoloured `Pop {…, PC}` in the MIDDLE of a segment (pinned at the pass via diff --git a/scripts/repro/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md index 8567875d..06304083 100644 --- a/scripts/repro/ORACLE_WIRING.md +++ b/scripts/repro/ORACLE_WIRING.md @@ -202,6 +202,159 @@ that wired — prose does not run an oracle. wired script to `manual` fails **both** `count-min 145` (the floor) and `count-max 7` (the ceiling). +--- + +# What a wired oracle ATTESTS — the check floors (#910) + +`ci-status: wired` says a CI step runs the oracle. It says nothing about what +that step *attests*. Measured on the #890 result: + +> **152 of the 160** workflow steps that run a `scripts/repro/` oracle asserted +> nothing beyond the process exit code. Exactly **8** asserted a printed verdict +> or count. + +That is not a #890 leftover — the pre-#890 hand-wired steps are mostly in the +152 as well. And exit 0 does not distinguish + +> compiled 40 fixtures, emulated 240 vectors, all bit-identical to wasmtime + +from + +> the fixture list came back empty, the loop body never ran, printed `PASS` + +which is #890's inert gate one level down: wired, but silent about its own +content. + +## The mechanism — `scripts/oracle_run.py` + +Oracle steps run `python scripts/oracle_run.py scripts/repro/.py …` +instead of invoking the harness directly. The driver executes it **in process** +(`runpy`) with three entry points wrapped: + +| wrapped | counter | what it means | +|---|---|---| +| `unicorn.Uc.emu_start` | `emulations` | a real emulator entry | +| `wasmtime.Func.__call__` | `wasmtime_calls` | a real reference execution | +| `subprocess` `synth … compile …` | `compiles` | a real compilation | + +The count comes from the emulator, not from the harness's own bookkeeping, so a +comparison loop that never runs cannot fake it. No harness was edited to get +this. + +**Why a driver and not 152 greps.** A bespoke `grep` per step is 152 hand-written +patterns to keep in sync with 150 harnesses' output strings — the mirror-drift +shape this repo keeps paying for. One driver is one thing to maintain, and it +measures the *behaviour* rather than the prose describing it. + +**Why not instrument the compiler instead** (#910 option 1: point the +differentials at an `llvm-cov` build and merge profiles). Two reasons. It +changes the artifact under test — these oracles exist to execute the *shipped* +bytes, and an instrumented binary is not those bytes. And it would buy precision +on an axis that is still the wrong instrument: a line percentage cannot answer +"what do the differentials not reach", which is the question worth asking. + +## The declaration + +One `# ci-checks:` header per oracle, next to its `# ci-status:` line — same +locality argument: it lives in the file it describes, appears in the diff of the +PR that adds the oracle, and cannot outlive its file. + +```python +# ci-status: wired +# ci-checks: emulations >= 75 +``` + +| form | use | +|---|---| +| `emulations >= N` | the normal case — a unicorn differential | +| `wasmtime >= N` | reference executions, where those are the countable work | +| `compiles >= N` | oracles whose work is not emulation: decline matrices, byte-identity legs, structural validators | +| `stdout // >= N` | the harness already prints a better count than any of the above; the regex must carry **exactly one** capture group holding an integer, so it asserts a *count* and not the presence of a happy-path string | +| `none — ` | nothing can be bound; needs a real reason (>= 20 chars) | + +Declare the **strongest mode that holds on every invocation** of that script. +Several oracles are run twice — once executing, once on a decline or +byte-identity leg that executes nothing by design — and a floor that only holds +for the good leg is not a floor. The weaker floor loses nothing: every counter +is still measured and recorded, so the ledger reports what ran while the gate +asserts what is guaranteed. + +Floors are **`>=`, never equality**: adding a fixture must never redden a step. +The ratchet direction is up. + +### Calibration — the floors are measured, not guessed + +Every floor was obtained by executing each CI oracle step **verbatim** (parsed +out of `ci.yml`, so there is no transcription drift between what was measured +and what CI runs) with the invocation routed through the driver. + +The unit is called `emulations`, not "checks", on purpose — but the four oracles +that self-report a check count agree with the driver **1:1**: + +| oracle | its own report | driver | +|---|---|---| +| `gpio_thin_846_differential.py` | `#846 CHECKS=75/75` | 75 | +| `aarch64_call_indirect_851_differential.py` | `35 checks (23 trap, 12 value)` | 35 | +| `aarch64_globals_851_differential.py` | `17 checks across 6 exported functions` | 17 | +| `aarch64_float_completion_851_differential.py` | the 662 float-boundary checks | 662 | + +Calling the aggregate "checks" on the strength of four agreements would still be +naming a measurement after something it does not measure — the exact defect this +whole lane is about. So the counter keeps the name of the thing it counts. + +## The floors, and the ratchet + +| mode | oracles | floor total | +|---|---|---| +| `emulations` | **133 oracles** | **294,914 emulator entries** | +| `stdout` | 7 oracles | 458 printed counts | +| `compiles` | 9 oracles | 43 compilations | +| `none` | **1 oracle** | — | + +**Reported per mode and never summed across modes.** Emulator entries, +compilations and printed counts are three different units; one impressive +combined figure is precisely the instrument defect #910 is about. + +`scripts/oracle_wiring_check.py --min-emulation-floor 294914` enforces the +emulations total, in the **already-required** `Claim Check` job. It shares the +driver's header parser by import rather than re-implementing the grammar. Pinned +in `claims.yaml` (`SYNTH-ORACLE-CHECK-FLOORS-910`) so the number here, the +number in `ci.yml`, and the declared headers move together. + +Per job, `scripts/oracle_evidence.py` closes out with what that job **measured** +— asserting every record met its floor *and* that the expected number of oracles +reported at all, so a step deleted, commented out, or skipped by an early exit +leaves the ledger short and reddens the job instead of quietly shrinking the +number. + +## This is not the coverage percentage, and must never be added to it + +`Rust-test Line Coverage` (was: `Code Coverage`) measures `cargo llvm-cov +--workspace` — the Rust test suite, in process. It **cannot see any of the +above**: the oracles spawn `$SYNTH` as a separate, uninstrumented process, from +other jobs entirely, and an uninstrumented subprocess emits no profile data. + +That is why `synth-backend-*/src/backend.rs` reads ~42 % line coverage while +being exercised end-to-end by nearly every differential in this table. The +percentage **understates** the testing that exists and is **not** a completeness +measure. Two populations, two units, reported side by side — never one number. + +## The oracles whose floor is weak, itemized + +An honest short list beats a uniform claim: + +| oracle | floor | why not stronger | +|---|---|---| +| `aarch64_matrix.sh` | `none` | a POSIX shell oracle; the driver runs Python in process and cannot instrument it. Its step already carries its own count assertion (>= 32 accepted ops), written before this mechanism existed | +| `i64_param_518_riscv_loudskip.py` | `compiles >= 1` | asserts a LOUD SKIP — by construction nothing executes, and it compiles the whole fixture once. Its eight `[ok ]` rows carry no printed total to bind to | +| `postlink_359_oracle.py` | `compiles >= 1` | a symbol-address/link-layout assertion over one compile; it prints addresses, not a check count | +| `fact_spec_*_494_differential.py` (5) | `compiles >= 2` | each runs twice — once executing thousands of vectors, once on a `--expect-decline` byte-identity leg that emulates nothing. The floor is the weaker leg's guarantee; the executing leg's real counts (2 002 / 2 052 / 3 167 / 288) still reach the ledger | +| `call_indirect_275_selfcontained_differential.py` | `compiles >= 4` | a decline/emission-shape oracle across four target configurations; no execution by design | +| `reachable_callgraph_275_selfcontained_differential.py` (RED step only) | not routed | that step inverts its verdict (`! python …`) because RED is the expected result. Routing it would file a below-floor record for a run that is *supposed* to fail. Its GREEN step is routed and carries `emulations >= 8` | + +Everything else — 133 of 150 wired oracles — asserts a real emulator-entry +floor. + ## Adding a repro script 1. Write the harness. Give it **exit-code discipline** — `sys.exit(0 if ok else 1)`. @@ -212,3 +365,7 @@ wired script to `manual` fails **both** `count-min 145` (the floor) and 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`. +4. If `wired`: run it through the driver (`python scripts/oracle_run.py + scripts/repro/.py …`), declare a `# ci-checks:` floor, and bump the job's + `--min-oracles`. Measure the floor — run it once with + `scripts/oracle_run.py --report-only` and use what comes back. diff --git a/scripts/templates/feature_matrix.md.tmpl b/scripts/templates/feature_matrix.md.tmpl index a7d99938..d0779491 100644 --- a/scripts/templates/feature_matrix.md.tmpl +++ b/scripts/templates/feature_matrix.md.tmpl @@ -136,11 +136,31 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. oracle-wiring gate now leaves 0 undeclared and 0 unwired scripts, so a forgotten gate is no longer indistinguishable from a deliberately manual one — what remains open is the 7 `manual` scripts (external fixture, measurement - and scratch categories) and the fact that the newly-wired sweeps assert exit - status rather than a per-script non-zero check count; #851: the aarch64 + and scratch categories); #851: the aarch64 op-surface gaps the VCR-SEL-005 third-backend oracle now enumerates mechanically; #846: two `gpio-thin` CRL/CRH sites still need relational ranges). +- **What the oracle steps ATTEST is now stated (#910).** The exit-status-only + residual noted above was measured and was larger than described: **152 of the + 160** workflow steps that run a `scripts/repro/` oracle asserted nothing + beyond the process exit code — the pre-#890 hand-wired steps too, not only + the newly wired ones; exactly 8 asserted a printed verdict or count. Every + `wired` oracle now declares a `# ci-checks:` floor that + `scripts/oracle_run.py` enforces per run by counting real emulator entries, + wasmtime executions and compilations: **133 oracles assert 294,914 emulator + entries**, 7 assert a printed count, 9 assert compilations, and 1 + (`aarch64_matrix.sh`, a POSIX shell oracle the in-process driver cannot + instrument) is itemized as unbindable in `scripts/repro/ORACLE_WIRING.md` + alongside the five other weak floors. +- **The `Code Coverage` percentage was renamed for what it measures (#910).** + It is `Rust-test Line Coverage (unit + integration only)`: `cargo llvm-cov + --workspace`, the Rust test suite, in process. It is structurally blind to + the execution differentials, which spawn the compiler as a separate + UNINSTRUMENTED process from other jobs — which is why + `synth-backend-*/src/backend.rs` reads ~42 % while being exercised + end-to-end by nearly every differential. The number understates the testing + that exists and is not a completeness measure. The two populations are + reported separately, in their own units, and are never added together. - Two residuals live in code comments rather than issues, and are restated here so they are not implied away: `validate_segment_rewrite` does NOT catch a recoloured `Pop {…, PC}` in the MIDDLE of a segment (pinned at the pass via From 89eee86bd3dfede86658053189e9cabd95e10e9a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:42:20 +0200 Subject: [PATCH 6/9] =?UTF-8?q?test(#910):=20prove=20the=20check-floor=20g?= =?UTF-8?q?ates=20by=20MUTATION=20=E2=80=94=207=20legs,=20all=20red?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The mechanism must not become the thing it polices. Each leg runs the step EXTRACTED VERBATIM from ci.yml (yaml.safe_load -> the step's `run:` block -> bash -e), so nothing here is a transcription of what CI does. M1 harness returns before its comparison loop -> driver measured 0, step RED M2 one floor lowered to 0 -> ratchet 294912 < 294914 RED M3 `# ci-checks:` header deleted -> wiring gate RED M4 stdout regex with no capture group -> driver rejects, RED M5 a routed step demoted to a COMMENT -> wiring gate RED M6 oracle steps un-routed -> claims count-min RED M7 job ledger short (1 of 15 oracles) -> ledger RED BASELINE and RESTORED both green; `git status --porcelain` empty afterwards. M1 is the load-bearing leg: the mutated harness STILL prints `ORACLE: PASS` and STILL exits 0. A `grep -q '^ORACLE: PASS'` would have greened it, and so would every one of the 152 exit-status-only steps this replaces. Only the emulator count catches it — because that count does not come from the harness. M5 re-proves the v0.54 comment-stripping fix under this lane's edits rather than assuming it: 159 `run:` bodies were rewritten here, and that is precisely the surface the fix covers. M6's nuance is written down rather than rounded off — the substitution hit both the `python3` and `python` spellings, so it un-routed two lines (159 -> 157), not one. The leg proves the direction. --- scripts/repro/ORACLE_WIRING.md | 87 ++++++++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/scripts/repro/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md index 06304083..249957a8 100644 --- a/scripts/repro/ORACLE_WIRING.md +++ b/scripts/repro/ORACLE_WIRING.md @@ -355,6 +355,93 @@ An honest short list beats a uniform claim: Everything else — 133 of 150 wired oracles — asserts a real emulator-entry floor. +## Red-first mutation evidence — the check floors + +Same discipline as the #890 matrix above: each leg runs the 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: wiring gate + floor ratchet ===== +STEP EXIT=0 + ci-checks compiles 9 scripts, floor total 43 + ci-checks emulations 133 scripts, floor total 294914 + ci-checks none 1 scripts, floor total 0 + ci-checks stdout 7 scripts, floor total 458 +oracle-wiring gate is non-vacuous: ... 150 of them wired ... and every wired +oracle declares a check floor (294914 emulator entries asserted across 133 of them). + +===== BASELINE: one oracle step through the driver ===== +STEP EXIT=0 +ORACLE-EVIDENCE script=base_cse_differential.py mode=emulations floor=2 +measured=2 emulations=2 wasmtime_calls=1 compiles=4 exit=0 + +===== M1: harness returns BEFORE its comparison loop (still prints PASS, exits 0) ===== +STEP EXIT=1 +ORACLE: PASS +ORACLE-EVIDENCE script=base_cse_differential.py mode=emulations floor=2 +measured=0 emulations=0 wasmtime_calls=0 compiles=0 exit=0 +FAIL scripts/repro/base_cse_differential.py: VACUOUS — declared floor +emulations >= 2, measured 0. The oracle exited 0 having executed nothing; that +is a gate that cannot fail, not a passing gate. + +===== M2: one floor lowered to 0 -> --min-emulation-floor ratchet ===== +STEP EXIT=1 +FAIL check-floor RATCHET BROKEN: summed `ci-checks: emulations` floors 294912 < +recorded minimum 294914. An oracle lost execution, or a floor was lowered. + +===== M3: `# ci-checks:` header deleted -> wiring gate ===== +STEP EXIT=1 + ci-checks UNDECLARED: 1 +FAIL scripts/repro/base_cse_differential.py: no `# ci-checks:` header. Every +oracle must declare what it attests ... + +===== M4: a happy-path STRING instead of a count (no capture group) ===== +STEP EXIT=1 +oracle_run: ... `ci-checks: stdout` regex must have EXACTLY ONE capture group +holding the count (got 0) — a pattern with no group asserts a happy-path +STRING, not that anything ran. + +===== M5: a routed oracle step demoted to a COMMENT -> wiring gate ===== +STEP EXIT=1 +FAIL scripts/repro/bulk_memory_374_differential.py: declares `wired` but NO +workflow STEP runs it — the gate is INERT. It IS mentioned in ci.yml, but only +in a COMMENT — prose does not run an oracle. + +===== M6: oracle steps un-routed (exit-status-only again) -> claims ledger ===== +STEP EXIT=1 +track shrank below floor: 157 < recorded min 159 +[/oracle_run\.py scripts/repro//] — update the claim, not just the number + +===== M7: job ledger short (1 of 15 oracles reported, --min-oracles 15) ===== +STEP EXIT=1 +ORACLE-LEDGER job=... oracles=1 runs=1 emulations=16 ... below_floor=0 +FAIL ledger SHORT: 1 distinct oracles reported, expected >= 15. A step is +missing, commented out, or the job exited early — its gate is inert (#890). + +===== RESTORED ===== +STEP EXIT=0 +``` + +**M1 is the load-bearing one.** The mutated harness still prints its `ORACLE: +PASS` banner and still exits 0 — a `grep -q '^ORACLE: PASS'` assertion would +have greened it, and so would every one of the 152 exit-status-only steps this +mechanism replaces. Only the emulator count catches it, because that count does +not come from the harness. + +**M5 re-proves the v0.54 fix under this lane's edits.** YAML eats `#` only in a +single-line plain scalar; in a `run: |` block the `#` survives into the script +body, so commenting a step out used to leave the script "referenced" and the +gate GREEN. 159 step bodies were rewritten here, which is exactly the surface +that fix covers, so it is re-run rather than assumed. + +**M6 nuance, stated rather than rounded off:** the mutation substituted both the +`python3` and the `python` spelling, so it un-routed two step lines, not one +(159 → 157). The direction is what the leg proves — un-routing reddens. + +**M7** is the runtime counterpart of M5: even if the static gate were bypassed, +a job whose oracle steps stopped running files a short ledger and goes red. + ## Adding a repro script 1. Write the harness. Give it **exit-code discipline** — `sys.exit(0 if ok else 1)`. From bc662b0b0a840e742d3dc44330f7664da0bc35aa Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 6 Aug 2026 06:29:20 +0200 Subject: [PATCH 7/9] fix(#918): three red gates, three defects in the instruments (#910) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit All three failures were this lane's own, and none was the CI-floor calibration the lane predicted. Reading the logs beat predicting them. 1. WCET sweep — "ledger SHORT: 3 oracles, expected >= 4". A TRUE POSITIVE with its root cause in the ledger's own harness. `ORACLE_EVIDENCE_JSONL` is a RELATIVE path and oracles run in-process (runpy), so a harness that chdir's redirects the append into its own scratch directory, which is then deleted. Exactly one of the four WCET phase scripts chdir's (phase2, line 213) and exactly that one's record went missing — 17 emulations recorded of 25 executed. Fixed twice over, because they are different failure modes: - resolve the ledger to an ABSOLUTE path at import, before any oracle can move the cwd; - restore `os.getcwd()` in run_oracle's finally block. It already restored sys.argv and sys.path; the third piece of interpreter state an in-process oracle can move was the one that bit. Red-first: a chdir'ing fixture records 0 ledger lines before, 1 after. No new gate — the --min-oracles assert IS the regression test for this class; it is what caught it. 2. Instrument independence — the failing step is `git diff --exit-code`, the assert that the v0.53 mutation never persists. The oracle steps `tee` into *.out AND those files were COMMITTED, so every fresh run dirties the tree and trips a soundness assert that has nothing to do with the mutation. Untracked all five and ignored them; the steps that produce and consume them at runtime are unchanged. 3. Rivet Validation — VG-009/VG-010 were typed `sys-verification`, a verification MEASURE, which rivet requires to `verifies` a system requirement. They are recorded GAPS and verify nothing. Typed `system-req` as VG-001..VG-008; their links already matched that shape. The species distinction the file draws is real, but it belongs in the prose, not the schema type. Refs #910, #918 --- .gitignore | 6 +++ artifacts/verification-gaps.yaml | 9 +++- ga_join.out | 72 -------------------------------- gpio846.out | 10 ----- scripts/oracle_run.py | 21 +++++++++- vcr_ver_004.out | 1 - vcr_ver_004_ship.out | 12 ------ vfp881.out | 3 -- 8 files changed, 32 insertions(+), 102 deletions(-) delete mode 100644 ga_join.out delete mode 100644 gpio846.out delete mode 100644 vcr_ver_004.out delete mode 100644 vcr_ver_004_ship.out delete mode 100644 vfp881.out diff --git a/.gitignore b/.gitignore index 0d82973f..e645f2e8 100644 --- a/.gitignore +++ b/.gitignore @@ -74,3 +74,9 @@ result-* output.elf __pycache__/ oracle-evidence.jsonl + +# Oracle run outputs — PRODUCED by CI steps and CONSUMED by the assert +# steps that follow them. Never tracked: the mutation-restoration gate is +# `git diff --exit-code`, so a committed copy makes every fresh run dirty the +# tree and fail a soundness assert that has nothing to do with the mutation. +*.out diff --git a/artifacts/verification-gaps.yaml b/artifacts/verification-gaps.yaml index 025cd2b9..3b995639 100644 --- a/artifacts/verification-gaps.yaml +++ b/artifacts/verification-gaps.yaml @@ -214,7 +214,12 @@ artifacts: # quoted; that is the #890 lesson wearing new clothes. # ========================================================================= - id: VG-009 - type: sys-verification + # `system-req`, as VG-001..VG-008 — NOT `sys-verification`. A + # sys-verification artifact is a verification MEASURE, which rivet requires + # to `verifies` a system requirement; these two are recorded GAPS, which + # verify nothing. The species distinction noted above is real but it lives + # in the prose, not in the schema type. + type: system-req title: "Line coverage is blind to the execution differentials (scope mislabel)" description: > The `Code Coverage` CI job runs `cargo llvm-cov --workspace --lcov`, @@ -255,7 +260,7 @@ artifacts: issue: "#910" - id: VG-010 - type: sys-verification + type: system-req # see VG-009 — a gap, not a measure title: "Oracle CI steps asserted exit status, not that any check ran" description: > #890 wired 63 forgotten execution oracles into CI. Measured on that diff --git a/ga_join.out b/ga_join.out deleted file mode 100644 index e321284f..00000000 --- a/ga_join.out +++ /dev/null @@ -1,72 +0,0 @@ -== cf_shapes_500.wat: applied=4 RA003-consistent=6 == -OK real_ifelse(0) = 0x00000000 (wasmtime void) mem== -OK real_ifelse(1) = 0x00000001 (wasmtime void) mem== -OK real_ifelse(7) = 0x00000007 (wasmtime void) mem== -OK real_if(0) = 0x00000000 (wasmtime void) mem== -OK real_if(1) = 0x00000001 (wasmtime void) mem== -OK br_func(0) = 0x00000000 (wasmtime void) mem== -OK br_func(1) = 0x00000001 (wasmtime void) mem== -OK early_ret(0) = 0x00000000 (wasmtime void) mem== -OK early_ret(1) = 0x00000001 (wasmtime void) mem== -== provenance_branches_396.wat: applied=1 RA003-consistent=1 == -OK decide(0,0) = 0x0000006D (wasmtime 0x0000006D) mem== -OK decide(5,3) = 0x00000009 (wasmtime 0x00000009) mem== -OK decide(3,5) = 0x00000009 (wasmtime 0x00000009) mem== -OK decide(100,1) = 0x00000009 (wasmtime 0x00000009) mem== -== aarch64_ctrlflow_851.wat: applied=3 RA003-consistent=8 == -OK count_sum(0) = 0x00000000 (wasmtime 0x00000000) mem== -OK count_sum(1) = 0x00000000 (wasmtime 0x00000000) mem== -OK count_sum(5) = 0x0000000A (wasmtime 0x0000000A) mem== -OK count_sum(17) = 0x00000088 (wasmtime 0x00000088) mem== -OK countdown(0) = 0x00000000 (wasmtime 0x00000000) mem== -OK countdown(1) = 0x00000001 (wasmtime 0x00000001) mem== -OK countdown(9) = 0x00000009 (wasmtime 0x00000009) mem== -OK do_while_count(1) = 0x00000001 (wasmtime 0x00000001) mem== -OK do_while_count(6) = 0x00000006 (wasmtime 0x00000006) mem== -OK do_while_count(23) = 0x00000017 (wasmtime 0x00000017) mem== -== loop_param_bound_663.wat: applied=4 RA003-consistent=4 == -OK sum_const(0,0) = 0x0000002D (wasmtime 0x0000002D) mem== -OK sum_const(3,4) = 0x0000002D (wasmtime 0x0000002D) mem== -OK sum_below(0,0) = 0x00000000 (wasmtime 0x00000000) mem== -OK sum_below(1,5) = 0x00000000 (wasmtime 0x00000000) mem== -OK sum_below(4,4) = 0x00000006 (wasmtime 0x00000006) mem== -OK sum_below(2,9) = 0x00000001 (wasmtime 0x00000001) mem== -== if_else_result_343.wat: applied=2 RA003-consistent=3 == -OK pick(0) = 0x00000014 (wasmtime 0x00000014) mem== -OK pick(1) = 0x00000003 (wasmtime 0x00000003) mem== -OK pick(4294967295) = 0x00000003 (wasmtime 0x00000003) mem== -OK pick2(0) = 0x0000012C (wasmtime 0x0000012C) mem== -OK pick2(1) = 0x00000007 (wasmtime 0x00000007) mem== -== brif_outer_740.wat: applied=1 RA003-consistent=1 == -OK poll(7,0) = 0x00000007 (wasmtime 0x00000007) mem== -OK poll(200,0) = 0x000000C8 (wasmtime 0x000000C8) mem== -OK poll(200,1) = 0x000000C9 (wasmtime 0x000000C9) mem== -OK poll(5,3) = 0x00000005 (wasmtime 0x00000005) mem== -== local_promote_cross_call.wat: applied=1 RA003-consistent=2 == -OK cross_call(0) = 0x00000064 (wasmtime 0x00000064) mem== -OK cross_call(5) = 0x00000076 (wasmtime 0x00000076) mem== -OK cross_call(100) = 0x000001F4 (wasmtime 0x000001F4) mem== -OK cross_call(65535) = 0x0003FF9E (wasmtime 0x0003FF9E) mem== -== intra_module_callee_saved.wat: applied=1 RA003-consistent=2 == -OK a(0) = 0x0000006B (wasmtime 0x0000006B) mem== -OK a(7) = 0x00000087 (wasmtime 0x00000087) mem== -OK a(100) = 0x000001FB (wasmtime 0x000001FB) mem== -== stack_canary_687.wat: applied=1 RA003-consistent=4 == -OK recurse(0) = 0x00000000 (wasmtime 0x00000000) mem== -OK recurse(1) = 0x00000001 (wasmtime 0x00000001) mem== -OK recurse(5) = 0x00000005 (wasmtime 0x00000005) mem== -OK recurse(12) = 0x0000000C (wasmtime 0x0000000C) mem== -== call_5args.wat: applied=1 RA003-consistent=2 == -OK caller(1,2,3,4,5) = 0x00054321 (wasmtime 0x00054321) mem== -OK caller(0,0,0,0,9) = 0x00090000 (wasmtime 0x00090000) mem== -OK caller(15,1,2,4,8) = 0x0008421F (wasmtime 0x0008421F) mem== -== call_6_7args.wat: applied=4 RA003-consistent=4 == -OK call6(1,2,3,4,5,6) = 0x00654321 (wasmtime 0x00654321) mem== -OK call6(0,0,0,0,0,7) = 0x00700000 (wasmtime 0x00700000) mem== -OK call7(1,2,3,4,5,6,7) = 0x07654321 (wasmtime 0x07654321) mem== -OK call7(0,0,0,0,0,0,9) = 0x09000000 (wasmtime 0x09000000) mem== - -engaged functions (flag-on bytes differ): 19 (of which CALL shapes: 6) -VCR-DEC-001-JOIN CHECKS=56/56 ENGAGED=19 CALLSHAPES=6 -RESULT: PASS -ORACLE-CALIBRATION script=vcr_dec_001_join_alloc_execution_differential.py emulations=56 wasmtime_calls=56 compiles=22 exit=0 secs=0.5 diff --git a/gpio846.out b/gpio846.out deleted file mode 100644 index d4943e26..00000000 --- a/gpio846.out +++ /dev/null @@ -1,10 +0,0 @@ -=== #846 SIZE === - flag-OFF (SYNTH_SHIFT_MASK_ELIDE=0): .text=534 B redundant `and r12,#0x1f` masks=10 - flag-ON (default v0.50.0) : .text=502 B redundant `and r12,#0x1f` masks=3 - recovered: 32 B (7 masks elided) -=== #846 EXECUTION UNCHANGED (flag-ON bytes vs wasmtime) === - 75/75 match — mmio (addr,value) sequences + returns bit-identical across pins [0, 1, 5, 7, 8, 15, 16, 31, 32, 33, 47, 63, 100, 255, 2147483647] (incl. >=32 mod-32 boundary) -=== RESULT === -#846 CHECKS=75/75 trace_events=105 -gpio-thin #846: PASS -ORACLE-CALIBRATION script=gpio_thin_846_differential.py emulations=75 wasmtime_calls=75 compiles=2 exit=0 secs=0.3 diff --git a/scripts/oracle_run.py b/scripts/oracle_run.py index b9cea0c0..0d31fca0 100644 --- a/scripts/oracle_run.py +++ b/scripts/oracle_run.py @@ -106,6 +106,19 @@ MIN_REASON_CHARS = 20 +# Resolved at IMPORT, before any oracle has had the chance to chdir. +# `ORACLE_EVIDENCE_JSONL` is set to a *relative* path by the workflow, and +# oracles run in-process (`runpy`), so a harness that chdir's into a scratch +# directory silently redirects the append into that directory — which is then +# deleted. The record vanishes, the ledger comes up short, and the job reads as +# "an oracle is missing" when in fact it ran and passed. Exactly one of the four +# WCET phase scripts chdir's, and exactly that one went missing. +_LEDGER_PATH = ( + os.path.abspath(os.environ["ORACLE_EVIDENCE_JSONL"]) + if os.environ.get("ORACLE_EVIDENCE_JSONL") + else None +) + class Decl: """A parsed `# ci-checks:` declaration.""" @@ -291,7 +304,7 @@ def run_oracle(script, argv): real_out = sys.stdout tee = Tee(real_out) - saved_argv, saved_path = sys.argv[:], sys.path[:] + saved_argv, saved_path, saved_cwd = sys.argv[:], sys.path[:], os.getcwd() # `python script.py` puts the script's OWN directory at sys.path[0]; # runpy.run_path does not, and several repro harnesses import sibling @@ -309,6 +322,10 @@ def run_oracle(script, argv): finally: sys.stdout = real_out sys.argv, sys.path = saved_argv, saved_path + # The third piece of interpreter state an in-process oracle can move. + # Restoring argv and sys.path but not cwd is what let a chdir'ing + # harness redirect everything written afterwards on a relative path. + os.chdir(saved_cwd) return code, counters, tee.buf.getvalue() @@ -395,7 +412,7 @@ def main(): # Append to the per-job ledger, if the job asked for one. Written even on # failure: a run that fell BELOW its floor is exactly the datum worth having. - ledger = os.environ.get("ORACLE_EVIDENCE_JSONL") + ledger = _LEDGER_PATH if ledger: import json diff --git a/vcr_ver_004.out b/vcr_ver_004.out deleted file mode 100644 index ddc915e0..00000000 --- a/vcr_ver_004.out +++ /dev/null @@ -1 +0,0 @@ -ORACLE-CALIBRATION script=vcr_ver_004_instrument_independence.py emulations=0 wasmtime_calls=0 compiles=0 exit=1 secs=0.3 diff --git a/vcr_ver_004_ship.out b/vcr_ver_004_ship.out deleted file mode 100644 index aa01eb99..00000000 --- a/vcr_ver_004_ship.out +++ /dev/null @@ -1,12 +0,0 @@ -functions audited (--relocatable) : 633 - Holds : 431 - NotAttempted : 202 - Violated : 0 -decline reasons: - unmodeled-op 175 - indirect-call-pseudo-op 17 - numeric-offset-branch 10 - -VCR-VER-004-SHIPPING HOLDS=431 VIOLATED=0 TOTAL=633 FLOOR=400 -RESULT: PASS -ORACLE-CALIBRATION script=vcr_ver_004_shipping_path_audit.py emulations=0 wasmtime_calls=0 compiles=161 exit=0 secs=1.6 diff --git a/vfp881.out b/vfp881.out deleted file mode 100644 index 9b06c883..00000000 --- a/vfp881.out +++ /dev/null @@ -1,3 +0,0 @@ -PASS: all 7 exports emitted (nm -> T) under -t cortex-m7dp --relocatable -PASS: 109 execution rows bit-identical to wasmtime (unicorn, cortex-m7dp, spilled VFP paths) -ORACLE-CALIBRATION script=vfp_spill_881_differential.py emulations=109 wasmtime_calls=109 compiles=1 exit=0 secs=0.2 From 808ed2dafad4c13a1cebc2556d1839b6902bc27c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 6 Aug 2026 06:38:27 +0200 Subject: [PATCH 8/9] =?UTF-8?q?fix:=20the=20merge=20left=20conflict=20mark?= =?UTF-8?q?ers=20in=20ci.yml=20=E2=80=94=20the=20workflow=20could=20not=20?= =?UTF-8?q?parse?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A merge-created defect, present in NEITHER parent. The merge conflicted in TWO files; I read the output through `tail -5` and saw only the CHANGELOG one, then `git add -A` staged ci.yml with its markers intact and the commit succeeded. GitHub reported it as `.github/workflows/ci.yml: failure` with ZERO checks — not a red gate, an ABSENT one, which is the harder failure to notice. Resolved keeping both sides: #599 keeps this lane's oracle_run.py routing, and main's new #916 zero-fill differential is kept verbatim as raw `python` — it carries no `# ci-checks:` header and the driver hard-errors on a script it cannot bind a floor to. Listed in the weak-floor table so the residue stays counted rather than silently unrouted. Also corrects the ORACLE_WIRING.md path in VG-010 and in the new comment: the file is at scripts/repro/, never docs/development/. Post-merge asserts, since resolving one conflict is not resolving the merge: zero conflict markers tree-wide, and both edited YAML files parse. --- .github/workflows/ci.yml | 9 +++++---- artifacts/verification-gaps.yaml | 2 +- scripts/repro/ORACLE_WIRING.md | 1 + 3 files changed, 7 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3b077ea4..a6dbe919 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2943,17 +2943,18 @@ jobs: - name: i64.popcnt scratch-restore clobber differential (#632) run: python scripts/oracle_run.py scripts/repro/i64_popcnt_632_differential.py - name: i64 shr_u/shr_s single-function path differential (#599) -<<<<<<< HEAD run: python scripts/oracle_run.py scripts/repro/i64_shr_599_differential.py -======= - run: python scripts/repro/i64_shr_599_differential.py + # Kept as main wrote it — raw `python`, NOT routed through oracle_run.py. + # The #916 harness carries no `# ci-checks:` declaration, and the driver + # hard-errors on a script it cannot bind a floor to. Wiring it is a + # follow-up on the harness, not a rename here; it is listed with the rest + # of the unbound residue in scripts/repro/ORACLE_WIRING.md. - name: i64 high-register zero-fill differential (#916) run: | set -euo pipefail ./target/debug/synth compile scripts/repro/i64_high_reg_zero_fill_916.wat \ -o /tmp/zf916.elf --target cortex-m4 --relocatable --all-exports python scripts/repro/i64_high_reg_zero_fill_916_differential.py /tmp/zf916.elf ->>>>>>> origin/main - name: dead-frame elision differential (#390, both flag states) run: python scripts/oracle_run.py scripts/repro/leaf_dead_frame_differential.py - name: i32 local-promotion differential (#390, clean + dirty) diff --git a/artifacts/verification-gaps.yaml b/artifacts/verification-gaps.yaml index 3b995639..a6678da0 100644 --- a/artifacts/verification-gaps.yaml +++ b/artifacts/verification-gaps.yaml @@ -277,7 +277,7 @@ artifacts: the same locality argument as `# ci-status:`), and records the count. Scripts that execute nothing emulatable declare a stdout-pattern floor instead; the residue that can bind to neither is enumerated in - docs/development/ORACLE_WIRING.md rather than covered by a uniform claim. + scripts/repro/ORACLE_WIRING.md rather than covered by a uniform claim. status: implemented tags: [verification-gap, evidence-instrument, oracle, honesty] links: diff --git a/scripts/repro/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md index 249957a8..23bf1084 100644 --- a/scripts/repro/ORACLE_WIRING.md +++ b/scripts/repro/ORACLE_WIRING.md @@ -351,6 +351,7 @@ An honest short list beats a uniform claim: | `fact_spec_*_494_differential.py` (5) | `compiles >= 2` | each runs twice — once executing thousands of vectors, once on a `--expect-decline` byte-identity leg that emulates nothing. The floor is the weaker leg's guarantee; the executing leg's real counts (2 002 / 2 052 / 3 167 / 288) still reach the ledger | | `call_indirect_275_selfcontained_differential.py` | `compiles >= 4` | a decline/emission-shape oracle across four target configurations; no execution by design | | `reachable_callgraph_275_selfcontained_differential.py` (RED step only) | not routed | that step inverts its verdict (`! python …`) because RED is the expected result. Routing it would file a below-floor record for a run that is *supposed* to fail. Its GREEN step is routed and carries `emulations >= 8` | +| `i64_high_reg_zero_fill_916_differential.py` | not routed | arrived from main (#919, the five-site zero-fill fix) after this table was measured, and carries no `# ci-checks:` header — the driver hard-errors rather than bind a floor it cannot derive. Its step asserts `set -euo pipefail` and the harness's own exit only. Declaring a floor on it is a follow-up on the harness, not a rename at the call site | Everything else — 133 of 150 wired oracles — asserts a real emulator-entry floor. From 82ec4d93285fe171eeec91ec3b8e1307e993418a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 6 Aug 2026 11:36:35 +0200 Subject: [PATCH 9/9] =?UTF-8?q?fix(#918):=20declare=20the=20two=20undeclar?= =?UTF-8?q?ed=20oracles=20=E2=80=94=20and=20pin=20the=20third=20surface=20?= =?UTF-8?q?(#910)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Claim Check` went red on the lane's OWN gate, correctly. Two oracles reached main AFTER the floors were measured and declare nothing: scripts/repro/i64_high_reg_zero_fill_916_differential.py (via #919) scripts/repro/proven_safe_bounds_901_differential.py (via #915) Both are real unicorn+wasmtime execution differentials, so both get `emulations >= N`. Floors MEASURED through the driver, never guessed — a guessed floor is the vacuous number this lane exists to remove: #916 measured=48 emulations=48 wasmtime_calls=48 #901 measured=371 emulations=371 wasmtime_calls=188 compiles=5 Both steps now route through `scripts/oracle_run.py`, so they report to the per-job ledger like every other wired oracle. This RETRACTS the comment I added in the previous commit claiming the #916 harness could not be bound and that declaring a floor was a follow-up: the gate disagreed, and the gate was right. Its weak-floor table row is dropped for the same reason. Totals move 133 -> 135 oracles, 294,914 -> 295,333 emulator entries. THE FIND: that number lives on THREE surfaces, and only two were pinned. ORACLE_WIRING.md and ci.yml are in `claims.yaml`; the FEATURE_MATRIX template was not — so with the matrix still reading "133 oracles assert 294,914" the ledger reported 42/42 HOLD. A number quotable in a shipped doc and bound to no gate is #880 exactly: the gate checked the matrix against its RENDER, never its CONTENT. Added SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX, pinned on the TEMPLATE rather than the generated file — pinning the render is satisfiable by faithfully regenerating wrong prose. Negative-controlled, not assumed: reverting the template to 133/294,914 yields `FAIL SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX`; restoring gives 43/43. Local: oracle wiring 159 scripts, 0 UNDECLARED, emulations 135 / floor 295333. Refs #910, #918 --- .github/workflows/ci.yml | 13 +++----- CHANGELOG.md | 6 ++-- claims.yaml | 32 ++++++++++++++++--- docs/status/FEATURE_MATRIX.md | 2 +- scripts/repro/ORACLE_WIRING.md | 11 +++---- ...i64_high_reg_zero_fill_916_differential.py | 1 + .../proven_safe_bounds_901_differential.py | 1 + scripts/templates/feature_matrix.md.tmpl | 2 +- 8 files changed, 45 insertions(+), 23 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a6dbe919..f844b815 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -217,7 +217,7 @@ jobs: run: | set -euo pipefail python3 scripts/oracle_wiring_check.py --json /tmp/oracle-wiring.json --list \ - --min-emulation-floor 294914 \ + --min-emulation-floor 295333 \ | tee /tmp/oracle-wiring.log python3 - <<'PY' import json, sys @@ -1388,7 +1388,8 @@ jobs: SYNTH: ./target/debug/synth run: | set -euo pipefail - python scripts/repro/proven_safe_bounds_901_differential.py \ + python scripts/oracle_run.py \ + scripts/repro/proven_safe_bounds_901_differential.py \ | tee /tmp/proven_safe_901.log grep -q '^RESULT: PASS' /tmp/proven_safe_901.log # Non-vacuity: a differential that checked nothing must not pass. @@ -2944,17 +2945,13 @@ jobs: run: python scripts/oracle_run.py scripts/repro/i64_popcnt_632_differential.py - name: i64 shr_u/shr_s single-function path differential (#599) run: python scripts/oracle_run.py scripts/repro/i64_shr_599_differential.py - # Kept as main wrote it — raw `python`, NOT routed through oracle_run.py. - # The #916 harness carries no `# ci-checks:` declaration, and the driver - # hard-errors on a script it cannot bind a floor to. Wiring it is a - # follow-up on the harness, not a rename here; it is listed with the rest - # of the unbound residue in scripts/repro/ORACLE_WIRING.md. - name: i64 high-register zero-fill differential (#916) run: | set -euo pipefail ./target/debug/synth compile scripts/repro/i64_high_reg_zero_fill_916.wat \ -o /tmp/zf916.elf --target cortex-m4 --relocatable --all-exports - python scripts/repro/i64_high_reg_zero_fill_916_differential.py /tmp/zf916.elf + python scripts/oracle_run.py \ + scripts/repro/i64_high_reg_zero_fill_916_differential.py /tmp/zf916.elf - name: dead-frame elision differential (#390, both flag states) run: python scripts/oracle_run.py scripts/repro/leaf_dead_frame_differential.py - name: i32 local-promotion differential (#390, clean + dirty) diff --git a/CHANGELOG.md b/CHANGELOG.md index f6327aab..d136f321 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -55,12 +55,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 not "checks", because naming a measurement after something it does not measure is the defect this lane exists to remove. -- **The differential population is reported, and ratcheted.** **133 oracles - assert 294,914 emulator entries per CI run**; 7 assert a printed count, 9 +- **The differential population is reported, and ratcheted.** **135 oracles + assert 295,333 emulator entries per CI run**; 7 assert a printed count, 9 assert compilations, 1 can bind to nothing. Reported **per mode and never summed across modes** — three different units, and one impressive combined figure is exactly the instrument defect being fixed. - `oracle_wiring_check.py --min-emulation-floor 294914` enforces the total in + `oracle_wiring_check.py --min-emulation-floor 295333` enforces the total in the already-required `Claim Check` job (a brand-new job is not a required context on `main` and could sit red for weeks — the #890 failure), sharing the driver's header parser by import rather than re-implementing the grammar. diff --git a/claims.yaml b/claims.yaml index 0c340e54..a2adfd54 100644 --- a/claims.yaml +++ b/claims.yaml @@ -1076,7 +1076,7 @@ claims: # --------------------------------------------------------------------------- - id: SYNTH-ORACLE-CHECK-FLOORS-910 doc: scripts/repro/ORACLE_WIRING.md - text: "**294,914 emulator entries**" + text: "**295,333 emulator entries**" evidence: - kind: file-exists path: scripts/oracle_run.py @@ -1089,18 +1089,42 @@ claims: - kind: count-min # the EXECUTION population, per script pattern: '^# ci-checks: emulations >= ' glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] - min: 133 + min: 135 - kind: count-max # the "nothing can be bound" hatch pattern: '^# ci-checks: none' glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] max: 1 - kind: verbatim # the doc carries the per-mode split - text: "**133 oracles**" + text: "**135 oracles**" - kind: verbatim text: "Reported per mode and never summed across modes." - kind: verbatim # the itemized weak-floor list stays text: "## The oracles whose floor is weak, itemized" + # --------------------------------------------------------------------------- + # #910 — the THIRD surface carrying this number: the FEATURE_MATRIX template. + # + # Found while adding the #916 and #901 oracles: ORACLE_WIRING.md and ci.yml + # were pinned, the generated matrix was NOT, so the ledger reported 42/42 HOLD + # while the matrix still read "133 oracles assert 294,914". A number quotable + # in a shipped doc and bound to no gate is the #880 defect exactly — the gate + # checked the matrix against its RENDER, never its CONTENT. + # + # Pinned on the TEMPLATE, not the rendered file: the render is generated + # (`--emit-status`), so pinning the output would be satisfiable by a + # regeneration that faithfully reproduces wrong prose. + # --------------------------------------------------------------------------- + - id: SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX + doc: scripts/templates/feature_matrix.md.tmpl + text: "**135 oracles assert 295,333 emulator" + evidence: + - kind: file-exists + path: scripts/oracle_run.py + - kind: count-min # same population the other two pin + pattern: '^# ci-checks: emulations >= ' + glob: ['scripts/repro/*.py', 'scripts/repro/*.sh'] + min: 135 + # --------------------------------------------------------------------------- # #910 — the CI side of the same claim, pinned so the doc's number and the # number the gate actually enforces cannot drift apart, and so the routing @@ -1109,7 +1133,7 @@ claims: # --------------------------------------------------------------------------- - id: SYNTH-ORACLE-CHECK-FLOORS-910-CI doc: .github/workflows/ci.yml - text: "--min-emulation-floor 294914" + text: "--min-emulation-floor 295333" evidence: - kind: count-min # oracle steps routed through the driver pattern: 'oracle_run\.py scripts/repro/' diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index e6ea9a33..4c19b56d 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -148,7 +148,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. the newly wired ones; exactly 8 asserted a printed verdict or count. Every `wired` oracle now declares a `# ci-checks:` floor that `scripts/oracle_run.py` enforces per run by counting real emulator entries, - wasmtime executions and compilations: **133 oracles assert 294,914 emulator + wasmtime executions and compilations: **135 oracles assert 295,333 emulator entries**, 7 assert a printed count, 9 assert compilations, and 1 (`aarch64_matrix.sh`, a POSIX shell oracle the in-process driver cannot instrument) is itemized as unbindable in `scripts/repro/ORACLE_WIRING.md` diff --git a/scripts/repro/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md index 23bf1084..6ba6ddc2 100644 --- a/scripts/repro/ORACLE_WIRING.md +++ b/scripts/repro/ORACLE_WIRING.md @@ -306,7 +306,7 @@ whole lane is about. So the counter keeps the name of the thing it counts. | mode | oracles | floor total | |---|---|---| -| `emulations` | **133 oracles** | **294,914 emulator entries** | +| `emulations` | **135 oracles** | **295,333 emulator entries** | | `stdout` | 7 oracles | 458 printed counts | | `compiles` | 9 oracles | 43 compilations | | `none` | **1 oracle** | — | @@ -315,7 +315,7 @@ whole lane is about. So the counter keeps the name of the thing it counts. compilations and printed counts are three different units; one impressive combined figure is precisely the instrument defect #910 is about. -`scripts/oracle_wiring_check.py --min-emulation-floor 294914` enforces the +`scripts/oracle_wiring_check.py --min-emulation-floor 295333` enforces the emulations total, in the **already-required** `Claim Check` job. It shares the driver's header parser by import rather than re-implementing the grammar. Pinned in `claims.yaml` (`SYNTH-ORACLE-CHECK-FLOORS-910`) so the number here, the @@ -351,7 +351,6 @@ An honest short list beats a uniform claim: | `fact_spec_*_494_differential.py` (5) | `compiles >= 2` | each runs twice — once executing thousands of vectors, once on a `--expect-decline` byte-identity leg that emulates nothing. The floor is the weaker leg's guarantee; the executing leg's real counts (2 002 / 2 052 / 3 167 / 288) still reach the ledger | | `call_indirect_275_selfcontained_differential.py` | `compiles >= 4` | a decline/emission-shape oracle across four target configurations; no execution by design | | `reachable_callgraph_275_selfcontained_differential.py` (RED step only) | not routed | that step inverts its verdict (`! python …`) because RED is the expected result. Routing it would file a below-floor record for a run that is *supposed* to fail. Its GREEN step is routed and carries `emulations >= 8` | -| `i64_high_reg_zero_fill_916_differential.py` | not routed | arrived from main (#919, the five-site zero-fill fix) after this table was measured, and carries no `# ci-checks:` header — the driver hard-errors rather than bind a floor it cannot derive. Its step asserts `set -euo pipefail` and the harness's own exit only. Declaring a floor on it is a follow-up on the harness, not a rename at the call site | Everything else — 133 of 150 wired oracles — asserts a real emulator-entry floor. @@ -366,11 +365,11 @@ so there is no transcription drift between what was proved and what CI runs. ===== BASELINE: wiring gate + floor ratchet ===== STEP EXIT=0 ci-checks compiles 9 scripts, floor total 43 - ci-checks emulations 133 scripts, floor total 294914 + ci-checks emulations 135 scripts, floor total 295333 ci-checks none 1 scripts, floor total 0 ci-checks stdout 7 scripts, floor total 458 oracle-wiring gate is non-vacuous: ... 150 of them wired ... and every wired -oracle declares a check floor (294914 emulator entries asserted across 133 of them). +oracle declares a check floor (295333 emulator entries asserted across 135 of them). ===== BASELINE: one oracle step through the driver ===== STEP EXIT=0 @@ -389,7 +388,7 @@ is a gate that cannot fail, not a passing gate. ===== M2: one floor lowered to 0 -> --min-emulation-floor ratchet ===== STEP EXIT=1 FAIL check-floor RATCHET BROKEN: summed `ci-checks: emulations` floors 294912 < -recorded minimum 294914. An oracle lost execution, or a floor was lowered. +recorded minimum 295333. An oracle lost execution, or a floor was lowered. ===== M3: `# ci-checks:` header deleted -> wiring gate ===== STEP EXIT=1 diff --git a/scripts/repro/i64_high_reg_zero_fill_916_differential.py b/scripts/repro/i64_high_reg_zero_fill_916_differential.py index 84272b01..fad77dca 100644 --- a/scripts/repro/i64_high_reg_zero_fill_916_differential.py +++ b/scripts/repro/i64_high_reg_zero_fill_916_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 48 """#916 — i64 zero-fill mis-encodes for a HIGH destination (R8-R12). The 16-bit `MOVS Rd,#imm8` (T1) has a **three-bit** Rd field. `reg_to_bits(R8)` diff --git a/scripts/repro/proven_safe_bounds_901_differential.py b/scripts/repro/proven_safe_bounds_901_differential.py index bae3581b..bf0a14a4 100644 --- a/scripts/repro/proven_safe_bounds_901_differential.py +++ b/scripts/repro/proven_safe_bounds_901_differential.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 # ci-status: wired +# ci-checks: emulations >= 371 """VCR-MEM-004 / #901 — execution differential for `--proven-safe`. Compiles `scripts/repro/proven_safe_bounds_901.wat` (one function, EIGHT diff --git a/scripts/templates/feature_matrix.md.tmpl b/scripts/templates/feature_matrix.md.tmpl index a6b29dd2..a410ca1e 100644 --- a/scripts/templates/feature_matrix.md.tmpl +++ b/scripts/templates/feature_matrix.md.tmpl @@ -148,7 +148,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. the newly wired ones; exactly 8 asserted a printed verdict or count. Every `wired` oracle now declares a `# ci-checks:` floor that `scripts/oracle_run.py` enforces per run by counting real emulator entries, - wasmtime executions and compilations: **133 oracles assert 294,914 emulator + wasmtime executions and compilations: **135 oracles assert 295,333 emulator entries**, 7 assert a printed count, 9 assert compilations, and 1 (`aarch64_matrix.sh`, a POSIX shell oracle the in-process driver cannot instrument) is itemized as unbindable in `scripts/repro/ORACLE_WIRING.md`