diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cf1cc6d0..d3e38d54 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 295333 \ | 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 @@ -276,7 +295,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 +341,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: @@ -458,7 +519,18 @@ 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 + # #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) @@ -529,31 +601,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, @@ -567,7 +639,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) @@ -582,7 +654,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) @@ -608,7 +680,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 @@ -618,7 +690,18 @@ 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 + # #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) @@ -685,7 +768,18 @@ 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 + # #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) @@ -726,19 +820,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 @@ -751,7 +845,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 @@ -760,11 +854,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). @@ -772,7 +866,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 @@ -785,12 +879,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. @@ -798,7 +892,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 @@ -807,7 +901,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: @@ -817,7 +911,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 @@ -827,7 +921,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 @@ -840,7 +934,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 @@ -849,7 +943,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 @@ -859,7 +953,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. @@ -870,7 +964,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 @@ -878,7 +972,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 @@ -888,7 +982,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 @@ -904,7 +998,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, @@ -917,7 +1011,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 @@ -928,7 +1022,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 @@ -957,7 +1051,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 @@ -967,7 +1061,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 @@ -978,9 +1072,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 @@ -998,7 +1092,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 @@ -1035,7 +1129,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 @@ -1049,7 +1143,18 @@ 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 + # #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) @@ -1108,7 +1213,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): @@ -1117,11 +1222,22 @@ 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) 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) @@ -1166,10 +1282,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, @@ -1178,21 +1294,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 @@ -1203,10 +1319,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: @@ -1221,11 +1337,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 @@ -1234,7 +1350,18 @@ 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 + # #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 proven-safe-oracle: name: proven-safe bounds-elision oracle (VCR-MEM-004, #901) @@ -1290,7 +1417,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. @@ -1331,7 +1459,18 @@ 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 + # #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 @@ -1365,7 +1504,18 @@ 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 + # #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) @@ -1403,7 +1553,18 @@ 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 + # #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) @@ -1443,7 +1604,18 @@ 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 + # #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) @@ -1487,7 +1659,18 @@ 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 + # #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 @@ -1521,7 +1704,18 @@ 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 + # #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 @@ -1558,7 +1752,18 @@ 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 + # #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) @@ -1597,7 +1802,18 @@ 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 + # #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) @@ -1637,7 +1853,18 @@ 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 + # #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) @@ -1682,7 +1909,18 @@ 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 + # #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) @@ -1731,7 +1969,18 @@ 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 + # #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) @@ -1776,11 +2025,22 @@ 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 + # #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 @@ -1818,7 +2078,18 @@ 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 + # #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 @@ -1856,7 +2127,18 @@ 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 + # #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 @@ -1896,7 +2178,18 @@ 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 + # #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 @@ -1935,11 +2228,22 @@ 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 + # #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 @@ -1979,7 +2283,18 @@ 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 + # #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 @@ -2018,7 +2333,18 @@ 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 + # #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 @@ -2058,19 +2384,30 @@ 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 + # #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 @@ -2106,7 +2443,18 @@ 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 + # #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 @@ -2145,7 +2493,18 @@ 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 + # #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 @@ -2183,7 +2542,18 @@ 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 + # #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 @@ -2221,7 +2591,18 @@ 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 + # #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 @@ -2261,12 +2642,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 @@ -2275,6 +2656,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 @@ -2301,7 +2694,18 @@ 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 + # #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)" @@ -2353,7 +2757,18 @@ 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 + # #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)" @@ -2409,7 +2824,18 @@ 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 + # #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)" @@ -2489,110 +2915,122 @@ 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: 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/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 + # #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 @@ -2633,43 +3071,54 @@ 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 + # #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 @@ -2709,43 +3158,54 @@ 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 + # #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) @@ -2785,10 +3245,21 @@ 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 + # #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..e645f2e8 100644 --- a/.gitignore +++ b/.gitignore @@ -73,3 +73,10 @@ result-* /*.elf 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/CHANGELOG.md b/CHANGELOG.md index 626e0b48..b81cedef 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,92 @@ 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.** **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 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. + `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. + +- **`VCR-VER-004` now exists in the roadmap.** It shipped in v0.54 and appeared + in the CHANGELOG, the feature matrix and CI — but not in the file README calls + "the single source of truth for roadmap status". The entry records the four + axes on which it fails *differently* from the two validators that shared a + blind spot, and all three of its limits, including the one that bounds the + whole claim: **the op model is still shared.** Def/use extraction for all three + instruments runs through `liveness::reg_effect`, so a mismodeled op remains a + common blind spot; `VCR-VER-004` closes the shared-*contract* hole, not the + shared-*op-model* hole, and until `synth-verify`'s `ArmSemantics::encode_op` is + pinned against it, "three independent validators" would be an overclaim. + ### Fixed - **The traceability graph disagreed with itself in four places, and the gate @@ -69,19 +155,6 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 against both trees: exit 1 naming both errors on the pre-fix artifacts, exit 0 after. -### Added - -- **`VCR-VER-004` now exists in the roadmap.** It shipped in v0.54 and appeared - in the CHANGELOG, the feature matrix and CI — but not in the file README calls - "the single source of truth for roadmap status". The entry records the four - axes on which it fails *differently* from the two validators that shared a - blind spot, and all three of its limits, including the one that bounds the - whole claim: **the op model is still shared.** Def/use extraction for all three - instruments runs through `liveness::reg_effect`, so a mismodeled op remains a - common blind spot; `VCR-VER-004` closes the shared-*contract* hole, not the - shared-*op-model* hole, and until `synth-verify`'s `ArmSemantics::encode_op` is - pinned against it, "three independent validators" would be an overclaim. - - **`--proven-safe`: bounds-check elision on scry's proof, fail-closed and attested (VCR-MEM-004, #901).** `synth compile --proven-safe safe-accesses.json` consumes scry's `scry/safe-accesses/v1` verdict list diff --git a/README.md b/README.md index a267f472..4045cb57 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). +  
diff --git a/artifacts/verification-gaps.yaml b/artifacts/verification-gaps.yaml index 74aac21d..a6678da0 100644 --- a/artifacts/verification-gaps.yaml +++ b/artifacts/verification-gaps.yaml @@ -203,3 +203,92 @@ 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 + # `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`, + 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: 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 + 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 + scripts/repro/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)" 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/claims.yaml b/claims.yaml index 40ca4f0a..a2adfd54 100644 --- a/claims.yaml +++ b/claims.yaml @@ -1049,3 +1049,125 @@ 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: "**295,333 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: 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: "**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 + # 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 295333" + 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 19c3531f..4c19b56d 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -137,11 +137,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: **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` + 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/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/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_run.py b/scripts/oracle_run.py new file mode 100644 index 00000000..0d31fca0 --- /dev/null +++ b/scripts/oracle_run.py @@ -0,0 +1,449 @@ +#!/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 + +# 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.""" + + 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, 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 + # 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 + # 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() + + +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 = _LEDGER_PATH + 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/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: diff --git a/scripts/repro/ORACLE_WIRING.md b/scripts/repro/ORACLE_WIRING.md index 8567875d..6ba6ddc2 100644 --- a/scripts/repro/ORACLE_WIRING.md +++ b/scripts/repro/ORACLE_WIRING.md @@ -202,6 +202,246 @@ 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` | **135 oracles** | **295,333 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 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 +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. + +## 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 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 (295333 emulator entries asserted across 135 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 295333. 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)`. @@ -212,3 +452,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/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_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/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/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/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/scripts/templates/feature_matrix.md.tmpl b/scripts/templates/feature_matrix.md.tmpl index 5c9192be..a410ca1e 100644 --- a/scripts/templates/feature_matrix.md.tmpl +++ b/scripts/templates/feature_matrix.md.tmpl @@ -137,11 +137,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: **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` + 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