aarch64: br_table + value-carrying block/loop/if (#851, VCR-A64-CF-001) #1639

Workflow file for this run

	name: CI

	on:
	push:
	branches: [main]
	pull_request:
	branches: [main]

	env:
	CARGO_TERM_COLOR: always

	jobs:
	test:
	name: Test
	# NOTE: stays on ubuntu-latest for now. It originally moved here from
	# [self-hosted, linux, x64, rust-cpu] because z3-sys's C++ build exhausted
	# the smithy runners' temp disk — that pressure is gone (#553: synth-verify
	# defaults to the pure-Rust ordeal engine, z3 is behind the off-by-default
	# `z3-solver` feature), so moving back is a possible follow-up.
	runs-on: ubuntu-latest
	# Outer wall-clock guard (#849). This job ran 4-6 h and timed out on the
	# GitHub default on EVERY run for three days because nothing anywhere
	# bounded a solver query. The per-query deadline in synth-verify
	# (`SYNTH_ORDEAL_DEADLINE_MS`, #848) is the inner floor; this is the outer
	# one, so a future cliff costs one red job in <1 h, not a burned day.
	timeout-minutes: 60
	env:
	RUSTFLAGS: -Dwarnings
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Install llvm-dwarfdump (independent DWARF parser gate, #394)
	# The `--debug-line` DWARF gate's Oracle I
	# (emitted_dwarf_verifies_with_llvm_dwarfdump_394) validates synth's
	# emitted `.debug_info`/`.debug_line` with the INDEPENDENT LLVM parser
	# (`llvm-dwarfdump --verify`), not gimli::read. That test FAILS (never
	# skips) when the tool is absent, so it must be present here. The `llvm`
	# package provides the unversioned `llvm-dwarfdump` on PATH.
	run: \|
	sudo apt-get update -qq
	sudo apt-get install -y --no-install-recommends llvm
	llvm-dwarfdump --version
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Run tests
	# Full workspace, synth-verify included (#553 steps 3/4): with ordeal as
	# the default solver there is no z3-sys / C++ build on the default
	# feature set, so the long-standing `--exclude synth-verify` (the #306
	# disk-exhaustion workaround) is gone. The z3-solver feature path is
	# covered by the dedicated `Z3 Verification` differential job below.
	run: cargo test --workspace
	- name: WCET bound gate (#778 — sound static WCET incl. phase-3/4/5)
	# The soundness gate for --emit-wcet: bound >= actual on loop-free +
	# const-loop fixtures, EXACT-literal composed bounds over the direct call
	# graph (leaf->mid->root; a callee in a proven loop counted trip×), and the
	# decline-honesty matrix — recursion (`recursion`), indirect
	# (`indirect-call`), external/import (`call`), and declined-callee
	# (`callee-unbounded`) still LOUD-DECLINE. Phase 4 (#49): a masked
	# single-self-call chain with a VERIFIED depth hint is BOUNDED (derived
	# depth 15, frame_count 16, 752 cyc); a too-low hint / tree (fib) / uncapped
	# countdown / mutual recursion STAY declined with the specific machine
	# reason (hint-below-derived-depth / hint-unverifiable-recursion). Phase 5
	# (#778): a DATA-DEPENDENT masked-ceiling loop bound (`i REL (x & K)`) with a
	# VERIFIED loop_bounds hint is BOUNDED (derived trip = both-endpoints max,
	# source `mask-ceiling`); the count-DOWN case's worst case is the rhs=0
	# endpoint (a single-endpoint seed would undercount); unhinted / too-low /
	# UNMASKED `i < param` STAY declined (`loop` + hint-below-derived-trip /
	# hint-unverifiable-induction). Covered by `cargo test --workspace` above;
	# run explicitly so a WCET-soundness regression is unmissable in the log.
	run: cargo test -p synth-cli --test wcet_bound_gate
	- name: Space-consistency invariant (#77 — execution+memory space)
	# The #77 checked property: an inconsistent execution/memory-space
	# pairing (bare-metal + OS-mapped, hosted + physical, FP-requiring space
	# on an FPU-less core) is REJECTED by synth_memory::space::validate().
	# Red-first unit tests (both directions of each invariant); covered by
	# `cargo test --workspace` above, run explicitly so a regression in the
	# space-consistency model is unmissable in the log.
	run: cargo test -p synth-memory --features std 'space::'
	- name: P3 async intrinsic honest-degradation gate (#80)
	# The #80 gate: the ONE lowered async op (error-context.drop) compiles
	# to a field-name BL call site; every declined intrinsic (error-context.new
	# /.debug-message, stream, future, waitable-set, task) LOUD-DECLINES the
	# compile by name. Runs the classifier unit tests + the CLI end-to-end
	# gate so an accidental silent-lower of a declined op is unmissable.
	run: \|
	cargo test -p synth-core --lib async_intrinsics
	cargo test -p synth-cli --features riscv --test async_intrinsics_gate

	clippy:
	name: Clippy
	# Same runner note as Test — the z3-sys disk pressure that forced
	# ubuntu-latest is gone (#553); moving back to smithy is a follow-up.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	with:
	components: clippy
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Run clippy
	run: cargo clippy --workspace --all-targets -- -D warnings

	fmt:
	name: Format
	runs-on: [self-hosted, linux, x64, light]
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	with:
	components: rustfmt
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Check formatting
	run: cargo fmt --all -- --check

	pin-sweep:
	name: Version Pin Sweep
	runs-on: [self-hosted, linux, x64, light]
	steps:
	- uses: actions/checkout@v7
	# Issue #145: fail at PR time if [workspace.package].version drifts from
	# any intra-workspace path-dep `version =` pin or MODULE.bazel — the
	# v0.7.0-class desync that breaks release.yml + publish at tag-push time.
	- name: Check intra-workspace version pins
	run: python3 scripts/check_version_pins.py

	claim-check:
	name: Claim Check
	# claim-verification gate: README/CLAUDE.md/coq/STATUS.md load-bearing
	# claims (proof counts, "verified" wording, DSL rule coverage, trusted-base
	# sizes) are pinned in claims.yaml and RE-DERIVED from source here — a
	# hand-maintained number that drifts from the tree fails the build.
	# When a proof/rule lands, update the docs AND claims.yaml together.
	#
	# Since the claim-surface extension, the same script run ALSO
	# * staleness-gates the machine-derived artifacts/status.json (the README
	# badges' data source) and the GENERATED docs/status/FEATURE_MATRIX.md —
	# regenerate with `python3 scripts/claim_check.py claims.yaml
	# --emit-status` and commit the result;
	# * closes the README linked-doc surface (every relative .md link must be
	# claim-covered, generated, or allowlisted with a rationale).
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- name: Ensure PyYAML
	run: python3 -c "import yaml" \|\| python3 -m pip install --user pyyaml
	- name: Re-derive documentation claims (+ generated-artifact staleness + link surface)
	run: python3 scripts/claim_check.py claims.yaml
	# #867: coverage OF the ISA semantics model. Re-derives
	# artifacts/model-coverage.json (static heuristic, documented in the
	# script) and fails if the committed artifact is stale or hand-edited;
	# prints the COMPLEMENT — modelled ISA behaviours no proof exercises —
	# loudly in the job log. The tier counts flow into status.json via
	# claims.yaml, so this step is what keeps those numbers honest.
	- name: Model-coverage artifact freshness + uncovered-complement report (867)
	run: python3 scripts/model_coverage_audit.py --check
	# #890: the ORACLE-WIRING gate. scripts/repro/*.py are the execution
	# oracles; 69 of 150 were referenced by no workflow at all and nothing
	# distinguished "manual by design" from "forgotten". Every script now
	# declares `# ci-status: wired\|manual\|unwired`, a `wired` declaration is
	# VERIFIED against this file (the "green board, inert gate" defect), and
	# an undeclared script is a hard failure so new oracles must CHOOSE.
	#
	# This gate lives in the already-REQUIRED claim-check job on purpose: a
	# brand-new job is not a required context on main, so it could be red for
	# weeks without blocking anything — which is the same failure mode the
	# gate exists to kill.
	#
	# ANTI-VACUITY: it must not become the thing it polices.
	# * `set -euo pipefail` EXPLICITLY. A bare `\| tee` reports tee's status
	# (always 0), and — found by mutating this very step — `pipefail`
	# WITHOUT `-e` is not enough either: the script's status is its LAST
	# command's, so the inert-gate mutation greened the step while the
	# gate itself printed FAIL and exited 1. Actions' default shell is
	# `bash -e`, but this step does not lean on that default.
	# * The verdict is re-derived from the summary the gate WROTE, not from
	# exit 0: a non-empty script set, a non-zero wired count, zero
	# undeclared, zero wired-but-unreferenced, and zero failures.
	- name: Oracle wiring gate — every repro script declares a CI status (890)
	run: \|
	set -euo pipefail
	python3 scripts/oracle_wiring_check.py --json /tmp/oracle-wiring.json --list \
	\| tee /tmp/oracle-wiring.log
	python3 - <<'PY'
	import json, sys
	s = json.load(open("/tmp/oracle-wiring.json"))["summary"]
	bad = [k for k, v in (("total<100", s["total"] < 100),
	("wired==0", s["wired"] < 1),
	("undeclared", s["undeclared"]),
	("wired_unreferenced", s["wired_unreferenced"]),
	("failures", s["failures"])) if v]
	if bad:
	sys.exit(f"oracle-wiring gate VACUOUS or DRIFTED {bad}: {s}")
	print(f"oracle-wiring gate is non-vacuous: it classified {s['total']} "
	f"scripts, {s['wired']} of them wired, {s['manual']} manual, "
	f"{s['unwired']} unwired-debt, 0 inert.")
	PY
	# The GitHub About surface (description + topics) is pinned verbatim in
	# claims.yaml's repo_metadata section. API/network failure = LOUD SKIP
	# (exit 0) so a flake can't block merges; a real mismatch = red.
	- name: Repo metadata check (description + topics)
	env:
	GITHUB_TOKEN: ${{ github.token }}
	run: python3 scripts/repo_metadata_check.py claims.yaml

	verify:
	name: Z3 Verification
	# #553 steps 3/4: this is now the ONLY job that pulls in z3 (feature
	# `z3-solver`) — the trusted-reference differential oracle, not the default
	# engine. SYNTH_SOLVER_DIFF=1 routes every query through BOTH engines
	# (ordeal + Z3); any decided-verdict disagreement is a hard error. Do not
	# delete this job: it is the standing cross-check that keeps the pure-Rust
	# default honest.
	# Links the SYSTEM libz3 (`sudo apt-get install -y libz3-dev`): the
	# `z3-solver` feature no longer enables `static-link-z3`, so z3-sys links
	# `-lz3` (via its `#[link(name="z3")]`) against the apt-installed shared
	# library instead of compiling z3 from source OR downloading a prebuilt —
	# this removes the flaky `z3-sys build.rs` GitHub download (HTTP 403/502)
	# that blocked releases. Stays on ubuntu-latest for `sudo` (smithy runners
	# have no sudo); move once libz3-dev is in the smithy toolchains role.
	runs-on: ubuntu-latest
	# Outer wall-clock guard (#849) — this job hung for 4-6 h alongside `test`
	# on the same unbounded 64-bit bvsrem/bvurem queries. Inner floor: the
	# per-query deadline (`SYNTH_ORDEAL_DEADLINE_MS`, #848), applied to the Z3
	# oracle too.
	timeout-minutes: 45
	env:
	SYNTH_SOLVER_DIFF: "1"
	# Point z3-sys bindgen at the apt header (libz3-dev installs it here);
	# without this it would fall back to the crate's wrapper.h + pkg-config
	# include path. Set explicitly so the system-link path is unambiguous.
	Z3_SYS_Z3_HEADER: /usr/include/z3.h
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Install system Z3 (shared lib + headers; no from-source/download)
	run: sudo apt-get update && sudo apt-get install -y libz3-dev
	- name: Run verification tests (differential ordeal vs Z3)
	run: cargo test -p synth-verify --features z3-solver,arm
	- name: Run comprehensive verification (differential ordeal vs Z3)
	run: cargo test -p synth-verify --test comprehensive_verification --features z3-solver,arm

	coverage:
	name: Code Coverage
	needs: [test]
	runs-on: [self-hosted, linux, x64, rust-cpu]
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@nightly
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-coverage-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-coverage-
	- name: Install cargo-llvm-cov
	uses: taiki-e/install-action@v2.85.5
	with:
	tool: cargo-llvm-cov
	- name: Generate coverage (LCOV)
	# synth-verify is no longer excluded (#553): the default feature set is
	# pure Rust (ordeal), so its tests run under llvm-cov like any crate.
	run: \|
	cargo llvm-cov --workspace --lcov --output-path lcov.info \
	--exclude synth-qemu \
	--exclude synth-backend-awsm --exclude synth-backend-wasker
	- name: Upload to Codecov
	uses: codecov/codecov-action@v7
	with:
	files: lcov.info
	fail_ci_if_error: false
	env:
	CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }}

	kani:
	name: Kani Verification
	# Stays on ubuntu-latest: Kani-CBMC bundle is not yet provisioned
	# in the smithy toolchains role (tracked in playbook out-of-scope
	# table). Move once smithy ships kani-verifier + CBMC.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- name: Install Kani
	run: cargo install --locked kani-verifier && cargo kani setup
	- name: Run Kani proofs
	run: cargo kani -p synth-backend --tests
	timeout-minutes: 30

	rivet:
	name: Rivet Validation
	runs-on: [self-hosted, linux, x64, rust-cpu]
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	# Cache the rivet-cli BINARY keyed on its pinned version, NOT on Cargo.lock.
	# The old key (hashFiles Cargo.lock) invalidated on every release version
	# bump, forcing a full rebuild of rivet-cli's HiGHS C++ dependency — which
	# filled a self-hosted runner's disk and red-failed the v0.14.0 release
	# (No space left on device). Version-keying means a Cargo.lock change no
	# longer triggers the rebuild; the cached binary is reused.
	- name: Cache rivet-cli binary
	uses: actions/cache@v6
	with:
	path: ~/.cargo/bin/rivet
	key: ${{ runner.os }}-rivet-cli-v0.23.0
	# PIN rivet to a release tag (was `--branch main`, unpinned). Unpinned, an
	# upstream schema/behaviour bump silently reddened the gate on unchanged
	# artifacts (rivet 0.15.0 promoted a WARN→ERROR, #229). v0.23.0 (adds configurable
	# release-readiness ready-when/coverage, check verification-evidence, trace-results) is validated clean on this repo's
	# artifacts before pinning — the exact CI gate below run locally under
	# v0.23.0 gives non-xref ERROR 0, same as v0.22.0. Skip
	# the (expensive) build entirely on a cache hit.
	- name: Install rivet (pinned v0.23.0)
	run: \|
	if ! rivet --version 2>/dev/null \| grep -q "0.23.0"; then
	cargo install --force --git https://github.com/pulseengine/rivet --tag v0.23.0 rivet-cli
	fi
	- name: Validate artifacts
	run: \|
	sed -i '/^externals:/,$d' rivet.yaml
	# Allow cross-repo link errors (kiln/gale/sigil haven't set up rivet yet)
	# but fail on any non-cross-repo errors (schema, missing fields, broken local refs)
	rivet validate 2>&1 \| tee /tmp/rivet-output.txt
	# Check if all errors are cross-repo links (contain ':' in target)
	if grep -q "^ ERROR:" /tmp/rivet-output.txt; then
	NON_XREF=$(grep "^ ERROR:" /tmp/rivet-output.txt \| grep -v "targets '.:.' which does not exist" \| grep -cv "missing '.*' link to" \|\| true)
	if [ "$NON_XREF" -gt 0 ]; then
	echo "::error::Found $NON_XREF non-cross-repo validation errors"
	exit 1
	fi
	echo "::warning::Cross-repo link errors present (expected — external projects need rivet init)"
	fi
	- name: Check coverage
	run: rivet coverage

	bazel:
	name: Bazel Build & Proofs
	# Stays on ubuntu-latest: needs Nix + Bazel + Rocq via Bazel
	# (none provisioned on smithy; tracked in playbook out-of-scope
	# table for both Bazel and Rocq).
	runs-on: ubuntu-latest
	timeout-minutes: 45
	steps:
	- uses: actions/checkout@v7
	- name: Install Nix
	uses: cachix/install-nix-action@v31
	with:
	nix_path: nixpkgs=channel:nixos-unstable
	- name: Setup Bazel
	uses: bazel-contrib/setup-bazel@0.19.0
	with:
	bazelisk-cache: true
	disk-cache: ${{ github.workflow }}
	repository-cache: true
	- name: Build Rust via Bazel
	run: bazel build //crates:synth
	- name: Verify Rocq proofs
	run: bazel test //coq:verify_proofs
	- name: Run Renode emulation tests
	run: bazel test //tests/renode/... --test_tag_filters=wast \|\| [ $? -eq 4 ]
	timeout-minutes: 10

	cmp-select-oracle:
	name: cmp-select two-move execution oracle
	# VCR-ORACLE-001 (#242, #428): EXECUTE the cmp->select two-move arm under
	# unicorn (faithful Thumb-2 IT-block predication) and diff flag-off vs flag-on
	# vs wasmtime. This is the runtime validation gale's #428 measurement showed no
	# real fixture provides (the two-move arm is reachable but runtime-dead on real
	# code). Isolated job: unicorn/wasmtime are pip-installed here ONLY, so the main
	# `cargo test --workspace` gate is NOT taxed with a C-library build graph.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run two-move execution oracle
	run: python scripts/repro/cmp_select_two_move_differential.py

	provenance-gate:
	name: synth-provenance-v1 reconciliation gate (#396)
	# VCR-DEC-003 (#396, witness#130): the source-to-object branch-transformation
	# map. Compiles a fixture that FOLDS (select->IT predication) and SPLITS
	# (br_table) branches, then reconciles every REAL object conditional branch
	# (from the BranchMap side-table) back to its source WASM condition. The gate
	# is the non-vacuous check that a folded/eliminated condition is recorded AS
	# folded with its object realization, never silently dropped. Runs in the
	# workspace test set too, but named here so a provenance regression is a
	# visible, self-describing red — witness's MC/DC object-certification depends
	# on this contract holding.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Run reconciliation gate + emitter unit tests
	run: \|
	cargo test -p synth-cli --test provenance_reconciliation_396
	cargo test -p synth-core --lib provenance

	aarch64-oracle:
	name: aarch64 backend execution + decline oracle (#538 m2–m4)
	# #538: the host-native A64 backend, oracle-gated per milestone. EXECUTE
	# every covered op's emitted A64 `.text` under unicorn (UC_ARCH_ARM64) and
	# diff vs wasmtime ground truth — the "third backend = third oracle"
	# property: m1 integer core, m2 full i32+i64 ALU, m3 scalar floats
	# (NaN-ordering compares, promote/demote, converts, reinterprets), m4 the
	# #709 boundary table (domain-guarded trapping trunc: every case where
	# WASM traps must TRAP under emulation, in-range must match bit-exactly)
	# + min/max NaN/±0 matrix + copysign. #851 added div/rem (SDIV/UDIV+MSUB
	# with WASM ÷0 + INT_MIN/-1 trap guards, execution-verified), popcnt (SIMD
	# CNT/ADDV), and f64<->i64 reinterpret. v0.54 L2 completes the SCALAR float
	# surface — rounding (FRINT), f32/f64 load/store (bounds-checked), i64->
	# float converts, and the DOMAIN-GUARDED trapping i64-target truncations —
	# so the decline-matrix probe now asserts the STRUCTURAL declines
	# (call_indirect, br_table, param writes, globals, bulk memory,
	# value-carrying blocks, SIMD) still LOUD-decline.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run m1 integer-core execution oracle
	run: SYNTH=./target/debug/synth python 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
	- name: Run m3 scalar-float execution oracle
	run: SYNTH=./target/debug/synth python 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
	- 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
	- name: Run #851 linear-memory load/store execution oracle
	run: SYNTH=./target/debug/synth python 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
	- name: Run #851 non-param locals execution oracle
	run: SYNTH=./target/debug/synth python 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
	- 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
	- 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
	- 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,
	# no precondition. The harness places `.text` and `.data` on DIFFERENT
	# pages and resolves the relocations itself, so a wrong page delta or
	# lo12 lands on the wrong bytes. NON-VACUITY: assert a non-zero check
	# count (a harness that compiled nothing would otherwise pass silently)
	# AND the summary verdict. `set -euo pipefail` (not bare `pipefail`,
	# which leaves the step's status as the LAST command's) makes the
	# script's own non-zero exit fail the step (#890).
	run: \|
	set -euo pipefail
	SYNTH=./target/debug/synth \
	python 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)
	# A64's `blr` is TOTAL; WASM §4.4.8 is not. All three traps must fire
	# exactly where wasmtime traps — and the structurally-DUPLICATE type
	# must NOT trap (the direction an "always trap" lowering would hide).
	# NON-VACUITY: assert non-zero counts in BOTH directions, so a run that
	# only trapped (or only returned values) fails, plus the summary
	# verdict. `set -euo pipefail` makes the script's own non-zero exit fail
	# the step (bare `pipefail` would leave the status as the last command's
	# — the #890 class).
	run: \|
	set -euo pipefail
	SYNTH=./target/debug/synth \
	python 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)
	# The four classes the VCR-SEL-005 third-backend parity gate listed as
	# Err(reason). The soundness-critical one is TRAP_TRUNC_I64: A64
	# FCVTZ{S,U} SATURATE where WASM §4.3.3 TRAPS, so the harness runs a
	# FULL boundary table (both sides of ±2^63 / 2^64, the nearest float
	# inside/outside each bound, ±0, ±inf, NaN) and requires every trap
	# case to ACTUALLY TRAP. Rounding is compared bit-exactly over a
	# halfway table, which is what makes the "FRINTN is ties-to-EVEN"
	# claim real rather than assumed.
	#
	# ANTI-VACUITY (#890). `set -euo pipefail`, NOT bare `pipefail`: with
	# pipefail ALONE the step's exit status is that of the LAST command, so
	# an oracle that printed FAIL and exited 1 still went GREEN. `-e` is
	# what makes the failing pipeline abort the step — and it is stated
	# explicitly here rather than left to the runner's default shell flags.
	#
	# The verdict is then taken from the script's OWN summary line, not
	# from exit 0 alone, and the counts are asserted non-collapsed: an
	# oracle that quietly stops exercising anything — or that loses the
	# out-of-range half of the #709 boundary table, which is this gate's
	# entire purpose — must go RED.
	run: \|
	set -euo pipefail
	SYNTH=./target/debug/synth python 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
	n=$(sed -n 's/^$[0-9]$ wasmtime cases./\1/p' /tmp/a64_floatdiff.log)
	t=$(sed -n 's/^[0-9]* wasmtime cases ($[0-9]$ trap cases)./\1/p' /tmp/a64_floatdiff.log)
	echo "float-completion oracle ran $n checks, $t of them trap cases"
	[ "$n" -ge 300 ]
	[ "$t" -ge 40 ]
	- name: Run v0.55 L6 br_table + VALUE-CARRYING block/loop/if oracle (VCR-A64-CF-001)
	# The two largest entries in the mechanically-derived aarch64 decline
	# complement, now lowered. `br_table` is a compare-and-branch CHAIN, so
	# a wrong destination is a wrong RESULT: the harness walks the index
	# lattice per table (every arm, the index AT the bound, one OVER it, and
	# 0xFFFFFFFF — which a SIGNED compare would mis-dispatch, since WASM
	# reads the index UNSIGNED), and puts a LOOP HEADER in the same table as
	# a forward block end so a wrong branch DIRECTION shows up as a wrong
	# trip count. The value-carrying frames are driven down BOTH edges of
	# every join, including a frame containing a `bl` — the one soundness
	# claim (a call cannot clobber a live reconciliation slot) that nothing
	# else executes.
	#
	# ANTI-VACUITY (#890). `set -euo pipefail`, NOT bare `pipefail`: with
	# pipefail ALONE the step's exit status is the LAST command's, so an
	# oracle that printed FAIL and exited 1 still went GREEN. The verdict is
	# then taken from the script's OWN summary line, and the counts are
	# asserted NON-ZERO in both outcome classes — an oracle that stopped
	# trapping (or stopped returning values) must go RED. The relocation
	# count is asserted too: the harness APPLIES the `R_AARCH64_CALL26`
	# relocations itself, and if they vanished the calls would become
	# self-branches and the clobber claim would go untested while the gate
	# stayed green.
	run: \|
	set -euo pipefail
	SYNTH=./target/debug/synth \
	python scripts/repro/aarch64_brtable_blockvals_851_differential.py \
	\| tee /tmp/a64_brtable.log
	grep -q '^RESULT: PASS' /tmp/a64_brtable.log
	grep -Eq '^[1-9][0-9]* checks $[1-9][0-9]* trap, [1-9][0-9]* value$ across [1-9][0-9]* exported' /tmp/a64_brtable.log
	grep -Eq '\[[1-9][0-9]* direct-call relocations applied\]' /tmp/a64_brtable.log
	n=$(sed -n 's/^$[0-9]$ checks ./\1/p' /tmp/a64_brtable.log)
	echo "br_table/value-carrying oracle ran $n checks"
	[ "$n" -ge 60 ]
	- name: Run decline-matrix honesty oracle
	run: SYNTH=./target/debug/synth python scripts/repro/aarch64_m2_decline_538.py

	aarch64-native-matrix:
	name: aarch64 native execution matrix (gale #851 acceptance gate)
	# gale's standing execution-differential (#851): compiles a broad op set with
	# `synth -b aarch64`, executes each ACCEPTED op NATIVELY on this arm64 runner
	# (MAP_JIT), and diffs bit-exact vs wasmtime. Exits non-zero ONLY on a
	# MISCOMPILE — a declined op is fine (the gate is "no accepted op is WRONG"),
	# so every op auto-flips declined→verified the day its lowering lands. macos
	# runners are arm64, so this is the real-silicon acceptance gate for the
	# host-native backend (the unicorn job above is the host-independent partner).
	runs-on: macos-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- name: Install wasm-tools + wasmtime + llvm (objcopy)
	run: brew install wasm-tools wasmtime llvm
	- name: Run gale's aarch64 execution matrix (miscompile → non-zero)
	# NON-VACUITY GUARD: the matrix DECLINES an op when `.text` extraction
	# fails (empty hex), and declined ops count as PASS — so a missing
	# objcopy/objdump would make the whole gate green having verified
	# NOTHING. Point OBJCOPY at brew's llvm (not on the default PATH) and
	# assert the accepted-op count is at least gale's 0.50.x baseline (32).
	run: \|
	out=$(SYNTH=./target/debug/synth \
	OBJCOPY="$(brew --prefix llvm)/bin/llvm-objcopy" \
	./scripts/repro/aarch64_matrix.sh); rc=$?
	echo "$out"
	# Primary purpose: a MISCOMPILE makes the matrix exit non-zero. Check
	# that explicitly (don't lean on set -e propagating through $(...)).
	if [ "$rc" -ne 0 ]; then
	echo "aarch64 matrix reported a miscompile/error (rc=$rc)"; exit "$rc"
	fi
	# Non-vacuity: extraction failure counts every op as declined (=PASS),
	# so a broken objcopy/objdump would green the gate having checked
	# nothing. Assert at least gale's 0.50.x accepted-op baseline.
	acc=$(echo "$out" \| sed -n 's/aarch64: $[0-9]$ ops accepted./\1/p')
	if [ "${acc:-0}" -lt 32 ]; then
	echo "VACUOUS GATE: only ${acc:-0} ops accepted (expected >= 32) — \
	objcopy/objdump/synth extraction likely broke"; exit 1
	fi
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install wasmtime python bindings
	run: pip install wasmtime
	- name: Run #851 direct-call execution differential
	# The matrix above is single-function (loads one function's .text) so it
	# cannot exercise CALLS. This harness compiles MULTI-function modules,
	# resolves the R_AARCH64_CALL26 relocations itself, JITs the linked blob
	# (MAP_JIT), and diffs bit-exact vs wasmtime. It asserts every expected
	# symbol is present, so a silently-declined caller fails LOUDLY.
	run: \|
	SYNTH=./target/debug/synth \
	WASMTOOLS=wasm-tools WASMTIME=wasmtime \
	python scripts/repro/aarch64_calls_851.py

	trap-semantics-oracle:
	name: trap-semantics oracle (#665 unreachable + #666 rem_s)
	# #665: wasm `unreachable` must TRAP (WASM §4.4.5) — it was decoder-dropped
	# to a no-op on EVERY backend, falling through panic/abort guards. #666:
	# rv32 rem_s wrongly carried div_s's INT_MIN/-1 ebreak guard —
	# irem_s(INT_MIN,-1) = 0, no trap (§4.3.2). Both EXECUTION-validated under
	# unicorn (thumb2 + rv32) against wasmtime ground truth, including the
	# non-vacuity direction (a guarded `unreachable` NOT taken runs normally;
	# rem_s zero-divisor + div_s overflow traps are KEPT). Isolated job:
	# emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	# capstone: the #846 gpio-thin oracle's mask census disassembles .text
	run: pip install wasmtime unicorn pyelftools capstone
	- name: Install arm-none-eabi-ld (#881 VFP spill oracle)
	# binutils only (NOT the full gcc-arm-none-eabi): the #881 oracle links
	# its ET_REL object with a REAL ld so the internal `bl` reloc is proven
	# to resolve. Skipping the link would make that half of the gate
	# 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
	- name: Run rem_s trap-table oracle (#666, rv32)
	run: SYNTH=./target/debug/synth python 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
	- name: Run ADDW static-offset oracle (#681, incl. software-bounds bypass)
	run: SYNTH=./target/debug/synth python 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
	# #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
	# masks strictly drop, (b) 75 mmio (addr,value) traces + returns are
	# bit-identical vs wasmtime across a pin sweep INCLUDING pin >= 32 (the
	# boundary an unsound elision would corrupt). #879: this gate existed
	# for two releases but was never CI-wired. The grep asserts the
	# NON-ZERO check count from the script's machine-readable summary —
	# exit 0 alone is not trusted (the "0 ops accepted PASS" lesson).
	- 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
	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
	# mod 2^32, so `addr >= 2^32 - (offset+size-1)` wrapped small, passed
	# the BLO, and the OOB access escaped below the linear-memory base.
	# 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
	- name: Run bulk-memory operand-clobber oracle (#677, thumb2)
	run: SYNTH=./target/debug/synth python 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
	# 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).
	# CI-gated now so the f32 path can't silently regress. The compare oracle
	# 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
	# #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
	# never wired it: the #879 shelfware class, recurring in the very release
	# whose audit fixed two other instances of it. The greps assert BOTH
	# halves of the claim from the script's own summary lines — every export
	# actually emitted (nm -> T, so a silent decline cannot read as success)
	# AND a non-zero count of execution rows bit-identical to wasmtime. Exit
	# 0 alone is not trusted (the "0 ops accepted PASS" lesson).
	- 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
	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
	# #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.
	# #719 phase 2 extension (same harness): f32 live ACROSS an integer call
	# (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
	# #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
	# #712-class f64 compare flag-clobber fix (MOVS after VMRS returned
	# stale-flag results), the m4f/m3 honest-reject (single-precision / no
	# 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
	# #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:
	# ARM32 m7dp+m4f (bare RZ VCVT — the guard-free dual of the #709 trapping
	# forms) and aarch64 (bare FCVTZS/FCVTZU, all 8 forms incl. i64 targets).
	# Also pins falcon's exact flags (-t cortex-m7dp --relocatable): the i32
	# 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
	# #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
	# forms EXECUTED on every NaN/±inf/2^63/-2^63/2^64 boundary row (a
	# wasmtime trap must be an ARM UDF stop — the #709-class silent-
	# miscompile gate), m4f loud-decline honesty, falcon-flags symbol
	# 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
	# #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
	# (the clamp idiom) and `return` of an f32 result. Bit-exact (selects
	# NaN-payload-STRICT — a select picks, never computes) vs wasmtime on
	# m7dp; m3/m4f capability gates pinned. Also pins the WIDE (i64) select
	# hi-half SILENT miscompile found adversarially (cond==0 returned val2's
	# lo paired with val1's hi — soft-float f64 select rode the same path)
	# and the hard-float SIGNATURE-only ABI hole (a float-signature function
	# 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
	# #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
	# the reloc-walking in-range oracle, which passed on the miscompile — a
	# vacuous gate, the #712-class lesson). Store/load through the above-SP
	# 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
	# #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
	# decline that skipped gale's gust:os log-emit function. i64 store/load
	# round-trips + narrow sign/zero-extend reads through an above-sp_init
	# static after the --shadow-stack-size shrink must match wasmtime
	# (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
	# #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.
	# the copy source/index LIVE ACROSS an internal `call` kept here — all
	# copy "gust:os up\n" correctly on 0.43.0. The oracle resolves the
	# R_ARM_THM_CALL relocation (the `bl` the copy loop is reached through)
	# and HARD-FAILS on any unhandled relocation type — an oracle that skips
	# 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
	# #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
	# faithful shapes ALL compile byte-correct vs wasmtime — the miscompile does
	# 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
	# #740: the Thumb-2 B<cond>.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
	# state write + spurious calls on the empty-budget round). Minimal
	# loop-inside-block shape with wide exits, direct path (non-tail return
	# declines the optimized path, #500); return AND a linear-memory window
	# 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<cond>.W branch-target oracle (#740, cortex-m4)
	run: SYNTH=./target/debug/synth python 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_<k> symbol at the base of the
	# object's .synth.wasm_mem_<k> reservation section. The oracle maps the
	# two memories at DISTINCT unicorn bases (far apart, so residual
	# aliasing faults or mismatches — never accidentally correct) and checks
	# store-both aliasing discriminators, memory-1 init-data peeks (pre-#406
	# those segments were silently DROPPED), sub-word round-trips, and
	# per-memory size/grow against wasmtime multi-memory. RED on v0.42.0
	# (the object has no per-memory region — every memory aliased R11);
	# GREEN with the per-memory lowering. The decline matrix (self-contained,
	# native-pointer-abi, shadow-stack, riscv/aarch64, cross-memory copy,
	# 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
	# #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,
	# so every load from an initialized region read 0 (silent miscompile of
	# any string/lookup/const table). The fix appends the segment bytes to
	# `.text` as a flash ROM image and copies ROM->RAM in Reset_Handler (crt0
	# `.data` init), copy dst = the same optimized_linmem_base() the functions
	# address. The oracle maps ZEROED RAM (inits must come from startup),
	# executes the REAL reset path, and checks two segments at distinct
	# 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
	# #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
	# 8*x+8 depends on the whole transitive `call` closure being compiled in
	# and every internal BL patched to the emitted callee. Runs the DEFAULT
	# image (its own Reset_Handler startup) on unicorn vs wasmtime for 7
	# vectors; an unreachable helper is confirmed absent (closure, not
	# 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
	# 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
	# reachable callees removed). `entry`'s BL then becomes an external
	# relocation and the builder degrades to a link-me ET_REL object with no
	# Reset_Handler — NOT self-contained. The gate MUST go RED, proving it
	# catches the historical #275 drop. `! ...` because RED = expected here.
	# The probe binary goes to a distinct target dir so it never shadows the
	# default binary the GREEN steps use.
	- name: Build #275 non-vacuity probe binary (non-default feature)
	run: cargo build -p synth-cli --features exports_only_275_probe --target-dir target-275probe
	- name: Reachable-callgraph oracle catches the pre-#235 drop (#275, RED)
	run: \|
	! EXPORTS_ONLY_275=1 SYNTH=./target-275probe/debug/synth \
	python scripts/repro/reachable_callgraph_275_selfcontained_differential.py
	# #406/#739-cluster coverage WIDENER: multi-chunk / multi-segment static
	# data across BOTH the self-contained (--cortex-m) and --relocatable
	# paths, segments at varied offsets — low, an UNALIGNED segment
	# straddling a 4 KiB internal page boundary (0x1000), an overlapping
	# later-wins pair, a HIGH segment near the top of a 2-page memory (0x1FF0,
	# approaching the globals boundary), and a long multi-word ROM->RAM copy.
	# Self-contained side runs the REAL reset path on ZEROED RAM (a dropped/
	# short/mis-based copy — the #758/#746/#739 family — reads 0 and goes
	# RED); relocatable side maps memory 0 at R11 with an embedder-populated
	# init image and .text far away (baked-absolute offsets fault). Ground
	# 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
	# #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
	# string source to the wrong (first, stale) overlapping segment. This oracle
	# reconstructs runtime linmem (segments applied in order, later-wins) and
	# asserts every static-data reloc reads the runtime-correct byte. RED on the
	# 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
	# 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
	# R11_base + memory_size, forgetting the #687 0x100 function-visible gap).
	# This boots the REAL self-contained image from reset under unicorn:
	# overlap_probe stores 0xDEADBEEF at mem[0xFF00] then reads global 0 (init
	# 0xABCD). RED pre-fix (0xDEADBEEF vs wasmtime 0xABCD); GREEN with the fix
	# (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
	- 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
	# 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
	# (the GOLDEN trick — the spike is byte-invisible when off), (2) flag-ON
	# APPLIES on ≥2 fixtures and the UNCONDITIONAL VCR-RA-003 validator returns
	# Consistent on every applied function (observed via SYNTH_RA003_VERBOSE —
	# the acceptance oracle validating the new allocator's REAL output), and
	# (3) NO SILENT DRIFT / NO GROWTH. v0.53 widened the spike to colour
	# ACROSS if/else joins (increment 2), so applied functions now genuinely
	# DIVERGE from the shipping bytes and the old "flag-ON ≡ flag-OFF
	# corpus-wide" claim — which made execution correctness TRANSITIVE — is
	# retired. What replaces it: a fixture the allocator did NOT apply to must
	# stay byte-identical (no drift through a decline path), an applied one
	# must not GROW its .text, and ≥2 fixtures must actually diverge or
	# 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
	# 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
	# transitively from byte identity, and increment 2 broke that.
	# `validate_cfg_rewrite` — the pass's own CFG-lifted trace-equality oracle
	# — SHARES the CFG shape with the pass it validates, and #872 is the
	# standing lesson that a validator can share its pass's blind spot, so the
	# new bytes get EXECUTED: unicorn runs the flag-ON image and compares
	# return value + linear-memory window against wasmtime, over every join
	# shape the allocator reaches (real if/else, if-without-else, desugared
	# block+br_if, early return, counted and data-dependent loops, two-level
	# br_if). PROVEN non-vacuous by MUTATION: emptying `cfg_exit_observable`
	# (the exit contract the pass and its validator SHARE) while removing the
	# churn bias that masks it emits code leaving the return value in the wrong
	# register — validate_cfg_rewrite AND VCR-RA-003 both ACCEPT it and only
	# this gate catches it (16 wrong results).
	#
	# Increment 3 (v0.54) adds the CALL shapes and the same argument applies
	# with MORE force: the AAPCS contract (`liveness::call_effect`) is SHARED
	# by the pass and the validator on purpose (two hand-maintained copies
	# would be the VCR-ORACLE mirror-pinning failure mode), so neither can
	# catch an error IN the contract. Both halves are executed — the CLOBBER
	# half (a value live across a `bl`, incl. self-recursion) and the ARGUMENT
	# half (5/6/7-argument callees that pack each argument into its own nibble,
	# register AND stack). Likewise proven non-vacuous by MUTATION: emptying
	# `call_effect`'s clobber set makes the colourer home a cross-call value in
	# R0-R3; `validate_cfg_rewrite` accepts it and only this gate fails it.
	#
	# The grep asserts the NON-ZERO check count, a non-zero engaged-function
	# count AND the ≥4 engaged CALL-shape floor from the machine-readable
	# summary: exit 0 alone is not trusted, and a run where the allocator
	# stopped reaching call-containing functions would pass every comparison
	# while leaving the whole increment-3 class ungated.
	- 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
	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
	# un-wired in the same #879 audit as the gpio gate. clang+lld build a
	# bare-metal riscv32 firmware from synth's object + generated startup/
	# linker script; unicorn boots it FROM _reset so the record-copy loop
	# (declaration order => later-wins) is what initializes linear memory;
	# result vs wasmtime. The script LOUD-fails on missing tools (never a
	# skip) and this wiring is pinned in claims.yaml
	# (SYNTH-MATRIX-RV32-DATA-SHIP).
	- 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

	instrument-independence-oracle:
	name: VCR-VER-004 instrument independence (#242, v0.53's mutation re-run)
	# THE LESSON THIS JOB PINS. v0.53 proved BY MUTATION that emptying
	# `cfg_exit_observable` — the exit contract the join-aware graph allocator
	# and its own CFG validator SHARE — emits code leaving the return value in
	# the WRONG REGISTER, and that BOTH per-compilation validators accept it
	# (`validate_cfg_rewrite` -> Ok, VCR-RA-003 -> Consistent). Only execution
	# caught it: two independent-LOOKING instruments, one shared blind spot,
	# and a counterexample to the claim that per-compilation validation is an
	# independent check on the code generator.
	#
	# This job re-applies that EXACT mutation (the committed patch, not a
	# reconstruction) and asserts on ONE compilation that the two dataflow
	# validators are still GREEN while VCR-VER-004 `validate_abi_contract`
	# REJECTS with a concrete violation naming the ABI result register — i.e.
	# that the class is now caught STATICALLY, and by an instrument that fails
	# DIFFERENTLY (forward value analysis, obligation = the AAPCS result
	# registers hard-named in its own source, CFG re-derived from both streams,
	# nothing taken from the pass).
	#
	# It asserts the BASELINE direction FIRST — the unmutated compiler must
	# still apply AND must not be rejected — so a false-rejection regression
	# (the v0.50 `JoinValueNotAvailable{R8}` class) fails this job before it
	# ever reaches the mutation. Isolated job: the script mutates the working
	# tree and rebuilds, then always restores it.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Build synth
	run: cargo build -p synth-cli
	# THE DEFAULT PATH, not the spike. The gate above guards the flag-OFF
	# graph-colouring allocator; this step asks the same ABI question of the
	# allocator every `synth compile` actually runs, and holds the answer to a
	# floor: ZERO violations (a violation is either a real shipping miscompile
	# or — far likelier, since the shipping bytes are frozen-pinned and
	# execution-differentialed — a FALSE REJECTION by the new instrument, and
	# neither may pass silently), plus a pinned `Holds` count so a change that
	# makes the checker SEE LESS of the shipping path is visible instead of
	# absorbed. Red-first in both directions (injected violation; stub binary
	# emitting no verdicts) — see the script docstring.
	- 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
	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):
	# exit 0 alone is not trusted, and a run that silently skipped every
	# assertion would otherwise pass while gating nothing.
	- 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
	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

	fact-spec-oracle:
	name: fact-spec elision oracle (#494 phases 2 + 2b + 3+ + bounds)
	# VCR-PERF-002 Phase 2 (#494): the proof-carrying-specialization lever
	# (SYNTH_FACT_SPEC, default off; per-elision ordeal obligation). Built
	# with the `verify` feature (the solver lives in synth-verify — pure-Rust
	# ordeal, no C++ toolchain): (1) the end-to-end flag/fact gating matrix +
	# certificate-evidence Rust gates; (2) the in-bounds execution
	# differential — specialized ≡ wasmtime ≡ unspecialized over the proven
	# bound ch ∈ [524,1524] under unicorn — plus the wrong-bound loud-decline
	# green path. Phase 2b (divisor-nonzero, kind 3): the div/rem trap-guard
	# elision byte gates + differential (incl. the two-guard distinction — the
	# i64 INT64_MIN/-1 overflow guard is RETAINED under a nonzero-only fact —
	# and the RED force-admit divergence demo, debug-build lever). Bounds
	# elision (#494 × #390 guard_bool): the software memory bounds guard falls
	# to a per-site certificate — byte gates, 1024-case sweep, retained-trap,
	# decline and RED legs (steps below). Isolated job: emulation deps
	# pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Run fact-spec end-to-end gates (flag matrix + certificates)
	run: cargo test -p synth-cli --features verify --test fact_spec_clamp_494
	- name: Run divisor-nonzero guard-elision gates (#494 phase 2b byte evidence)
	run: cargo test -p synth-cli --features verify --test fact_spec_div_494
	- name: Build synth (verify feature)
	run: cargo build -p synth-cli --features verify
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- 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
	- name: Run wrong-bound loud-decline path
	run: >
	python 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,
	# incl. the RETAINED-i64-overflow-guard trap assertion), the
	# Sat loud-decline byte-identity leg, and the RED force-admit divergence
	# 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
	- name: Run divisor-including-zero loud-decline path
	run: python 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
	# #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
	- name: Run select-collapse wrong-bound loud-decline path
	run: >
	python 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
	# representative gust_kernel lane-pack (`lo \| (hi<<11)`, both lanes proven
	# ∈ [0,2047], masks `& 0x7FF` that are NOT uxtb/uxth-foldable) this is an
	# unambiguous byte win LLVM cannot make (no range on the dissolved
	# params): in-bounds differential (specialized ≡ wasmtime ≡ unspecialized,
	# 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
	- name: Run mask-elision wrong-bound loud-decline path
	run: >
	python 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:
	# UNSAT(P ∧ trap_mem_oob(zext64(index) + offset, size, min_memory_bytes))
	# (ordeal 0.9.1 trap_mem_oob shape, wraparound-safe 64-bit extension).
	# Byte gates (poll 184 -> 104 B, all 8 guard UDFs gone, specialized
	# .text BYTE-IDENTICAL to the unguarded floor), the 1024-case in-bounds
	# sweep vs wasmtime + unspecialized (return value + full memory image),
	# the retained-trap leg (out-of-premise inputs still trap on the
	# UNSPECIALIZED path), the Sat loud-decline byte-identity leg, and the
	# RED force-admit sandbox-escape demonstration (debug-build lever).
	- 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
	- name: Run bounds-including-OOB loud-decline path
	run: python scripts/repro/fact_spec_bounds_494_differential.py --expect-decline
	- name: Run RED bounds force-admit divergence demonstration
	run: python scripts/repro/fact_spec_bounds_494_differential.py --force-admit
	# #890: the phase-3+ rem_u IDENTITY differential lived in scripts/repro/
	# unwired, so the headline "with the fact, synth deletes the whole rem_u
	# (2 B) where clang -Os needs a 24 B reciprocal multiply-subtract" claim
	# had no standing execution gate — the specialized build's equality with
	# BOTH wasmtime and the unspecialized build was hand-checked only.
	- name: Run constant-divisor rem_u identity differential (#494 phase 3+)
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/fact_spec_rem_494_differential.py

	rv32-shift-fold-oracle:
	name: rv32 immediate-shift-fold execution oracle
	# VCR-ORACLE-001 (#242, #472): EXECUTE the RV32 immediate-shift-fold lever
	# under unicorn (UC_ARCH_RISCV) in BOTH flag states and diff vs wasmtime. The
	# lever ships flag-off (SYNTH_RV_SHIFT_FOLD) awaiting the on-silicon flip, so
	# nothing else exercises the flag-on path; this continuously validates it
	# (slli/srli/srai folds incl. the &31 mask on >=32 and negative amounts, and
	# the variable-shift non-fold) against regression — the RV32 analogue of the
	# cmp-select oracle above. Isolated job: emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run RV32 shift-fold execution oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/shift_fold_riscv_differential.py

	rv32-const-addr-fold-oracle:
	name: rv32 const-address-fold execution oracle
	# VCR-ORACLE-001 (#242, #472 step 2): EXECUTE the RV32 const-address-fold lever
	# under unicorn (UC_ARCH_RISCV) in BOTH flag states and diff the resulting
	# linear MEMORY vs wasmtime. Ships flag-off (SYNTH_RV_ADDR_FOLD) awaiting the
	# on-silicon flip, so this continuously validates the flag-on path (folding a
	# constant address into the access immediate off s11) against regression.
	# Isolated job: emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run RV32 const-address-fold execution oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/const_addr_fold_riscv_differential.py

	rv32-br-table-oracle:
	name: rv32 br_table execution oracle (#882)
	# #882: RV32 lowers `br_table` as a compare-and-branch chain (entry 0 vs
	# x0, li+beq per further entry, jal to default) — the last op standing
	# between gale's wdg-thin driver and a complete RV32 lowering. The
	# differential EXECUTES gale's exact shape (targets [0,1,0] default 1) plus
	# 3-distinct-target and default-distinct dispatches under unicorn
	# (UC_ARCH_RISCV) vs wasmtime, with indices covering EVERY table entry AND
	# out-of-range/unsigned-edge (0x80000000, 0xFFFFFFFF must land on default —
	# a wrong default or a signed chain compare is loud). A missing export
	# (the pre-fix decline) fails the vacuity guard, so this can never pass
	# vacuously. Isolated job: emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run RV32 br_table execution oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/rv32_br_table_882_differential.py

	rv32-extern-call-reloc-oracle:
	name: rv32 external-call relocation oracle (#871)
	# #871: the gale thin-seam driver shape — exported functions calling an
	# imported 2-function mmio seam — must LOWER on `-b riscv --relocatable`
	# (pre-fix: every seam-using export was skipped, so no driver could
	# dissolve to RISC-V). The differential verifies (1) every export emits +
	# `nm -u` lists exactly the imports, (2) each `.rela.text` entry is a real
	# R_RISCV_CALL_PLT at a placeholder auipc/jalr pair with the right symbol
	# (a wrong offset/symbol is a silent link-time miscompile), (3) ARM-shape
	# parity on the same wasm, (4) a REAL link (ld.lld) against mmio stubs,
	# and (5) execution of the linked image under unicorn (UC_ARCH_RISCV) vs
	# wasmtime ground truth. Isolated job: emulation deps pip-installed here.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Install lld + clang (real-link stage)
	run: sudo apt-get update && sudo apt-get install -y lld clang
	- name: Run RV32 external-call relocation oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/riscv_extern_call_871_differential.py

	rv32-label-return-oracle:
	name: rv32 label/return dead-code oracle (#882)
	# #882: gale's i2c-thin driver — a `return` inside a block aborted the
	# lowering walk, so the frame-closing `end`s never defined their labels
	# ("undefined label `Lend0`" on i2c_step, loud skip) and reachable
	# else-arm/post-join code was never lowered. The 4-stage differential:
	# (1) the synthetic shapes (block-end br_if target past a return, then-arm
	# return with reachable else, the exact nested i2c_step shape) compile
	# with all exports, (2) they execute under unicorn (UC_ARCH_RISCV) bit-
	# identical to wasmtime on both the return path and every resumed join,
	# (3) gale's pinned REAL i2c_thin_882.wasm compiles 7/7 incl. i2c_step,
	# (4) a real ld.lld link against mmio stubs + i2c_step execution vs
	# wasmtime (return values AND the mmio register file) — stage 4 is also
	# the red gate for the #882 param-clobber-across-call fix (params spilled
	# to frame slots in call-containing bodies; pre-fix i2c_step compiled but
	# read the callee's leftover a0). Isolated job: emulation deps here only.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Install lld + clang (real-link stage)
	run: sudo apt-get update && sudo apt-get install -y lld clang
	- name: Run RV32 label/return dead-code oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/rv32_label_882_differential.py

	rv32-mem-size-grow-oracle:
	name: rv32 memory.size / memory.grow execution oracle
	# VCR-SEL-005 (#223/#242): EXECUTE the newly-lowered RV32 memory.size and
	# memory.grow under unicorn (UC_ARCH_RISCV) and diff vs wasmtime. Closes two
	# entries off the cross-backend op-parity allowlist — proves memory.size
	# reports the declared page count, the shared rewrite_memory_grow_zero fold
	# makes grow(0) return current size, and fixed-memory grow(>0) returns -1.
	# Isolated job: emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- 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

	callee-saved-490-oracle:
	name: optimized-path callee-saved preservation oracle
	# VCR-ORACLE-001 (#242, #490): EXECUTE optimized-path functions that use
	# r4-r8 under unicorn (UC_ARCH_ARM / Thumb) with r4-r8 set to sentinels, and
	# assert both the result matches wasmtime AND every callee-saved register is
	# restored at return. This is the runtime gate for the #490 fix (the
	# optimized path now emits the `push {r4-r8,lr}` / `pop {r4-r8,pc}` it was
	# missing); the frozen byte gate only covers the `--relocatable` direct path,
	# so nothing else exercises the optimized path's AAPCS compliance. Covers the
	# 16-bit push and the 32-bit PUSH.W (high-register) forms. Isolated job:
	# emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run callee-saved preservation oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/callee_saved_490_differential.py

	call-indirect-642-oracle:
	name: call_indirect bounds-guard oracle (Thumb-2 + A32)
	# VCR-ORACLE-001 (#242, #642): call_indirect emitted NO table bounds check
	# and NO type check — an out-of-bounds index read past the table and BLXed
	# whatever word lay there (uncontrolled indirect branch) where WASM Core
	# §4.4.8 mandates a trap. EXECUTE the fixture under unicorn on BOTH ISAs
	# (Thumb-2 cortex-m3 + A32 cortex-r5, table linked at r11) vs the wasmtime
	# oracle: in-bounds indices must match; OOB indices must stop AT A UDF.
	# Non-vacuous red: the words past the table are seeded with a valid decoy
	# function, so an unguarded build "succeeds" at the OOB call and the
	# harness fails loudly on the decoy's return value. The type check is
	# discharged at compile time (closed-world table verification in the
	# selector); its decline paths are unit-gated in synth-core/synth-synthesis.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run call_indirect bounds-guard oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/call_indirect_642_differential.py

	call-indirect-650-multitable-oracle:
	name: multi-table call_indirect oracle (Thumb-2 + A32)
	# VCR-ORACLE-001 (#242, #650): tables are ONE contiguous region of 4-byte
	# code pointers at R11 (table N at sum(size(0..N))*4, a compile-time
	# constant -- tables are provably fixed-size, #642). EXECUTE a TWO-table
	# fixture with OVERLAPPING indices and DISTINCT functions under unicorn on
	# BOTH ISAs vs the wasmtime oracle: dispatch through both tables must
	# match, OOB on EITHER table must stop at a UDF (bounds guard against THAT
	# table's own size), and the aliasing canary (table0[1] != table1[1])
	# catches a backend that drops the table index. On <= v0.33.1 this is red
	# at compile: table-1 call_indirect loud-declined (capability upgrade --
	# red = "declines today", green = correct dispatch). Single-table modules
	# stay byte-identical by construction (offset 0 = the pre-#650 expansion),
	# pinned by the frozen-fixture job and the #642/#594/#597 oracles.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run multi-table call_indirect oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/call_indirect_650_differential.py

	call-indirect-664-nullslot-oracle:
	name: null-funcref-slot call_indirect oracle (Thumb-2 + A32)
	# VCR-ORACLE-001 (#242, #664): a table with null (uninitialized funcref)
	# slots no longer poisons the closed world — the type check verifies the
	# INITIALIZED slots only, and the null-slot trap (WASM Core §4.4.8:
	# calling an uninitialized element traps) is discharged at RUNTIME: the
	# layout contract links null slots as ZERO words and the dispatch
	# null-checks the loaded pointer (`cmp ip,#0; bne ok; udf`) between the
	# #642 bounds guard and the BLX. EXECUTE the sparse-table fixture (4
	# slots, only 1 and 3 initialized — the falcon fused-component shape)
	# under unicorn on BOTH ISAs vs the wasmtime oracle: initialized slots
	# must match, null AND OOB indices must stop at a UDF. Non-vacuous red: a
	# build without the null check BLXes address 0 and faults (not a udf).
	# On <= v0.35.0 this is red at compile: the null slot rejected every type
	# and the function loud-declined (capability upgrade — red = "declines
	# today", green = sound sparse-table dispatch). Fully-initialized tables
	# stay byte-identical by construction (null_check=false emits the
	# pre-#664 bytes), pinned by the frozen-fixture job and the
	# #642/#650/#594/#597 oracles.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run null-funcref-slot call_indirect oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/call_indirect_664_differential.py

	call-indirect-676-heterogeneous-oracle:
	name: heterogeneous-table call_indirect oracle (Thumb-2 + A32)
	# VCR-ORACLE-001 (#242, #676): a HETEROGENEOUS funcref table (mixed
	# signatures — falcon's fused 41-slot dispatch table) can never satisfy
	# the closed-world type check, so WASM Core §4.4.8's type check is
	# discharged at RUNTIME: the object carries a type-id sidecar
	# (`.synth.table_type_ids`, one u32 structural class id per slot, id 0 =
	# null) which the layout contract places at R11 + sum(table sizes)*4,
	# and the dispatch compares the indexed slot's id against the expected
	# class id (compile-time immediate), UDF-trapping on mismatch — which
	# subsumes the #664 null trap. EXECUTE the mixed fixture (two signature
	# classes INTERLEAVED + a structural duplicate type + null slots) under
	# unicorn on BOTH ISAs vs the wasmtime oracle: matching-class calls must
	# return wasmtime's values; wrong-class ("indirect call type mismatch"),
	# null AND OOB indices must all stop at a UDF. Non-vacuous red: a build
	# without the type check CALLS the wrong-typed function and returns a
	# wrong value. On <= v0.37.1 this is red at compile: every dispatch
	# through the mixed table loud-declined (capability upgrade — red =
	# "declines today", green = sound heterogeneous dispatch). Homogeneous
	# tables stay byte-identical by construction (type_check=None emits the
	# pre-#676 bytes), pinned by the frozen-fixture job, the whole-object
	# no-sidecar test (heterogeneous_table_676.rs) and the
	# #642/#650/#664/#594/#597 oracles.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run heterogeneous-table call_indirect oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/call_indirect_676_differential.py

	call-indirect-275-selfcontained-oracle:
	name: self-contained call_indirect oracle (execution + residual declines)
	# #275 finale (v0.47): the SELF-CONTAINED Thumb-2 `--cortex-m` image now
	# lowers `call_indirect` through a flash-resident funcref table addressed
	# PC-relative (`__synth_func_table` literal, patched post-layout) — never
	# via R11, the linear-memory base the v0.42 #717 collision corrupted.
	# Two gates:
	# 1. EXECUTION differential (falcon shape): the default self-contained
	# image (its OWN Reset_Handler startup, nothing fabricated) runs a
	# heterogeneous 5-slot dispatch under unicorn vs the wasmtime oracle —
	# matching dispatches must return wasmtime's values (incl. a
	# linear-memory-reading target: the #717 non-collision proof), and
	# OOB / type-mismatch / null-slot cases must all stop AT A UDF
	# (§4.4.8). Red on <= v0.46: the dispatchers loud-declined (the #717
	# interim), so the harness fails at the symbol probe.
	# 2. Emission + RESIDUAL declines: cortex-m emits the table; the
	# A32/Cortex-R5 self-contained path (no flash-table builder) still
	# LOUD-declines with #275; `--relocatable` stays untouched on both
	# ISAs.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run self-contained call_indirect EXECUTION differential
	env:
	SYNTH: ./target/debug/synth
	run: python 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

	block-brif-483-oracle:
	name: optimized-path block/br_if lowering oracle
	# VCR-ORACLE-001 (#242, #483): EXECUTE optimized-path functions with forward
	# `block`/`br_if` and nested `block`+`br` under unicorn (UC_ARCH_ARM / Thumb)
	# and diff the resulting linear MEMORY vs wasmtime across both branch
	# directions. Guards the #483 fix (End labels with the closed block's id, and
	# the half/byte memory-op byte-size estimate) — before it, a forward br_if
	# resolved against an id no label held and landed mid-instruction, silently
	# miscompiling any non-relocatable function with that control flow. The frozen
	# byte gate only covers the `--relocatable` direct path, so nothing else
	# exercises the optimized path's branch resolution. Isolated job: emulation
	# deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run block/br_if lowering oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/block_brif_483_differential.py

	spill-frame-499-oracle:
	name: optimized-path spill-frame teardown oracle
	# #499: EXECUTE optimized-path functions whose register pressure fires the
	# flag-off Const-eviction spill (`sub sp,#N` frame) under unicorn
	# (UC_ARCH_ARM / Thumb) and diff linear MEMORY + SP balance vs wasmtime.
	# Guards the #499 fix: the bridge appended fall-off-the-end returns WITHOUT
	# the `add sp,#N` teardown, so post-#490 the `pop {…,pc}` epilogue read PC
	# from a spill slot — a shipped crash on straight-line AND control-flow
	# shapes. Compiles with SYNTH_BASE_CSE=0 (the #592 default relieves the
	# pressure on these fixtures; the teardown path must stay covered) and
	# trips loudly if a fixture stops spilling (vacuity guard). Isolated job:
	# emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run spill-frame teardown oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/spill_frame_499_differential.py

	r12-spill-496-oracle:
	name: optimized-path register-exhaustion oracle
	# VCR-ORACLE-001 (#242, #496): EXECUTE the two silicon fixtures
	# (control_step, flight_seam_flat) compiled via the DEFAULT optimized path
	# (no --relocatable) under unicorn (UC_ARCH_ARM / Thumb) and diff the result
	# vs wasmtime. Guards the #496 fix: the optimized path used to borrow R12/IP
	# as last-resort scratch when its R4-R8 pool was exhausted, but R12 is the
	# encoder's indexed-load base scratch (#212), so under real register pressure
	# the value collided — control_step execution-faulted (READ_UNMAPPED from
	# `add ip,ip,ip` = 2×base) and flight_seam_flat produced wrong values. The fix
	# flags exhaustion and DECLINES the function to the direct selector (which
	# spills). The frozen byte gate only covers the --relocatable direct path, so
	# nothing else exercises the default self-contained-image path's register
	# pressure. Isolated job: emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run register-exhaustion oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/r12_spill_496_differential.py

	flight-seam-570-oracle:
	name: flight-seam relocatable-path execution oracle
	# VCR-ORACLE-001 (#242, #212/#215, #570): EXECUTE the two flight_seam silicon
	# fixtures (inlined w/ internal `bl filter_step`, and flat fully-dissolved)
	# compiled via the SHIPPED direct path (--relocatable) under unicorn
	# (UC_ARCH_ARM / Thumb) and diff flight_algo's result vs wasmtime (anchor
	# 0x07FDF307). Guards the #212 R12-scratch reservation and #215 exposure on
	# the relocatable path. Previously a dev-only script: it drifted silently
	# when the #394 name work changed symbol naming (#570) — CI-gating it here
	# so harness drift reddens instead of rotting. Symbols come from the ELF
	# symtab, not `synth disasm` text (host-dependent, PR #489). Isolated job:
	# emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools capstone
	- name: Run flight-seam oracle (inlined #212 + flat #215)
	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
	./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 \
	scripts/repro/flight_seam_flat.wasm

	control-step-584-oracle:
	name: control-step relocatable-path execution oracle
	# VCR-ORACLE-001 (#242, #209, #584): EXECUTE the control_step silicon fixture
	# (4x unsigned constant div_u — the reciprocal-multiply cost-gate repro)
	# compiled via the SHIPPED direct path (--relocatable) under unicorn
	# (UC_ARCH_ARM / Thumb) and diff control_step_decide's result vs wasmtime
	# (anchor 0x00210A55, 13 vectors). Previously a dev-only script: its `synth
	# disasm` text parse drifted into a KeyError on current main (#584, same
	# class as #570/#489) — symbols now come from the ELF symtab, and CI-gating
	# it here (flight-seam-570-oracle pattern) so harness drift reddens instead
	# of rotting. The r12_spill_496 oracle covers control_step on the DEFAULT
	# optimized path; this covers the --relocatable direct path. Isolated job:
	# emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run control-step oracle
	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

	stack-args-503-oracle:
	name: AAPCS stack-argument path oracle
	# VCR-ORACLE-001 (#242, #503): EXECUTE functions that need the AAPCS
	# stack-argument path with >8 scalar i32 params/args under unicorn
	# (UC_ARCH_ARM / Thumb), via the SHIPPED direct path (--relocatable, what
	# falcon uses), and diff the result vs wasmtime. Guards the #503 fix: the arm
	# backend used to SKIP (emit no code for) any function with >8 scalar params
	# or a call passing >8 args — 3 reachable falcon helpers were dropped. The fix
	# lifts the conservative caps over the already-generic incoming_params /
	# emit_stack_args machinery, leaning on the existing 12-bit [sp,#imm] guards.
	# Covers a HIGH param count (sum25, reading param 24) and an outgoing 10-arg
	# call. The 64-bit stack-param case stays refused (a #503 follow-up). Isolated
	# job: emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools capstone
	- name: Run AAPCS stack-argument oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/stack_args_503_differential.py

	i64-completeness-503-587-oracle:
	name: i64 stack-param + spill-pool-grow oracle
	# VCR-ORACLE-001 (#242, #503-i64, #587): EXECUTE the two previously
	# loud-skipped direct-selector i64 classes under unicorn and diff vs
	# wasmtime, on BOTH paths (--relocatable = falcon's, and the default):
	# * #503-i64 — 64-bit params AAPCS-passed on the STACK (past R3 /
	# even-align-spilled), incl. the narrow-after-wide shape that was
	# silently MIScompiled (p3 of `(i64 i32 i32 i32)` read from R3 = p2),
	# a write-back shape, and a has-call shape. Falcon func_58/func_163.
	# * #587 — an i64-dense function whose ~16 concurrent pair spills
	# exhausted the fixed 8-slot pool; the pool-grow recovery retry (last
	# resort, after the #474 promotion-off fallback) sizes the pool from
	# the operand-stack-depth bound. Falcon func_60/func_73.
	# Isolated job: emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run i64 stack-param oracle (#503-i64)
	env:
	SYNTH: ./target/debug/synth
	run: python 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
	- 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
	- 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

	i64-rot-div-610-oracle:
	name: i64 rotl/rotr/div/rem expansion oracle
	# VCR-ORACLE-001 (#242, #610): EXECUTE the i64 rotl/rotr/div_u/rem_u (+
	# div_s/rem_s) encoder expansions under unicorn and diff vs wasmtime.
	# Pre-#610 these compiled without error and returned 0 for EVERY input:
	# the rot expansions restored saved scratch OVER the result (`POP {R4}`
	# with rd_lo == R4) and the div/rem expansions ignored their register
	# operands outright (hardcoded R0:R1/R2:R3). Now wrapped in the fixed-ABI
	# marshal/restore; divide-by-zero traps (UDF #0) like the i32 guard.
	# Vectors: rot-by-0 identity, rot 32/63/>=64, div by 1/self/0(trap),
	# high-bit patterns, _hi twins for the upper result half.
	# Isolated job: emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run i64 rot/div/rem expansion oracle (#610)
	run: python scripts/repro/i64_rot_div_610_differential.py target/debug/synth

	br-table-507-oracle:
	name: optimized-path br_table oracle
	# VCR-ORACLE-001 (#242, #507): EXECUTE br_table dispatch compiled via the
	# DEFAULT optimized path (no --relocatable) under unicorn (UC_ARCH_ARM /
	# Thumb) and diff the resulting linear memory vs wasmtime across every
	# selector (incl. out-of-range → default arm) and two table shapes. Guards
	# the #507 fix: the optimized path DROPPED the br_table dispatch during
	# wasm→IR, emitting the arm bodies in fall-through with no selector compare —
	# a silent miscompile (every input hit the last arm). The fix detects
	# br_table on the raw wasm op stream and forces the direct selector (which
	# lowers it as a cmp-chain). The frozen byte gate only covers the
	# --relocatable direct path, so nothing else exercises the default path's
	# br_table lowering. Isolated job: emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run br_table oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/br_table_507_differential.py

	const-cse-242-oracle:
	name: const-CSE flag-on execution oracle
	# VCR-RA const-CSE (#242): EXECUTE the optimized path compiled with
	# SYNTH_CONST_CSE=1 under unicorn (UC_ARCH_ARM / Thumb) and diff the returned
	# value vs wasmtime across redundant-const shapes (large/small/negative/mixed
	# consts, reuse ACROSS an if/else where the cache must reset, and a
	# 12-live-local function that forces real spills). The const cache aliases a
	# repeated const to the register already holding it; this proves the aliasing
	# is semantics-preserving on the flag-ON path. The flag ships DEFAULT-OFF
	# (off ⇒ byte-identical, pinned by const_cse_reduction_242.rs's golden), so
	# nothing else exercises the optimized-path const cache. Isolated job:
	# emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run const-CSE flag-on oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/const_cse_differential.py

	frame-slot-dce-242-oracle:
	name: frame-slot DCE default+optout execution oracle
	# VCR-RA frame-slot DCE (#242): EXECUTE flat_flight (stack-reload forwarding +
	# dead-frame-store elimination, DEFAULT-ON since the #242 feature-loop flip)
	# under unicorn (UC_ARCH_ARM / Thumb) and diff flight_algo's return value vs
	# wasmtime across several sensor inputs, in BOTH the shipped default AND the
	# SYNTH_NO_STACK_FWD=1 opt-out (a default flip is only safe if the shipped path
	# AND its rollback both match), with linear memory seeded exactly as wasmtime's.
	# Also asserts the two configs emit DIFFERENT bytes (the flip is engaged). The
	# paired passes turn frame reloads into register moves and remove the now-dead
	# stores (flight_algo sp-traffic 20→7, 139→135 insns). Isolated job: emulation
	# deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run frame-slot DCE flag-on oracle
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/frame_slot_dce_differential.py

	stack-layout-687-oracle:
	name: stack-layout=low overflow BusFault oracle
	# VCR-MEM-003 (#687): EXECUTE the REAL self-contained Cortex-M image (its
	# own vector-table SP + reset path) under unicorn, both stack layouts. RED:
	# today's stack-HIGH default silently corrupts linmem canary words on deep
	# recursion BEFORE any fault (the overflow hazard). GREEN: --stack-layout=low
	# BusFaults (UC_ERR_WRITE_UNMAPPED below the SRAM start) with every canary
	# intact — the fault PRECEDES any linmem damage. TRANSPARENT: in-budget
	# calls match wasmtime under BOTH layouts, and the existing #649 i64-global
	# -init differential passes unchanged under the low layout (the whole
	# RAM-anchored layout — R9/R10/R11 startup AND the optimized path's
	# absolute 0x2000_0100 base — shifts by stack_size as one). Flag-off
	# byte-identity is pinned by the frozen-fixture job + the startup unit
	# tests. Isolated job: emulation deps pip-installed here ONLY.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run stack-layout red/green/transparent oracle
	env:
	SYNTH: ./target/debug/synth
	run: python 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

	# #418: self-contained binding of the meld-dissolve embedder import
	# `env::__cabi_arena_realloc` — the compile must yield an ET_EXEC image
	# (not a "link me" ET_REL) whose synthesized arena allocator EXECUTES the
	# canonical-ABI realloc contract identically to a wasmtime host arena
	# (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.
	arena-bind-418-oracle:
	name: "#418 arena-bind self-contained execution oracle"
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools
	- name: Run the #418 arena-bind execution differential
	env:
	SYNTH: ./target/debug/synth
	run: python scripts/repro/cabi_arena_bind_418_differential.py

	vcr-ra-003-alloc-validator-gate:
	name: "VCR-RA-003 register-allocation validator (red-first + frozen)"
	# VCR-RA-003 (#242): the UNCONDITIONAL register-allocation validator
	# (synth_synthesis::liveness::validate_final_allocation) runs on every ARM
	# compile in the default build and hard-errors on a violation of FOUR
	# invariants: (1) callee-saved preservation (#490), (2) spill-slot
	# non-aliasing (#331), and — PHASE 2 (#49), whole-function past straight-line
	# — (3) caller-saved preservation across a call and (4) value availability
	# across a control-flow join. This job pins the gate's halves as an explicit,
	# self-describing red so a regression is visible on its own name:
	# (1) RED-FIRST non-vacuity: the ra003_red_* unit tests synthetically
	# revert / construct a known clobber and assert the validator CATCHES
	# it (revert #490 prologue -> CalleeSavedNotSaved; drop epilogue restore
	# -> CalleeSavedNotRestored; alias two live values on one slot ->
	# SpillSlotAliased; a caller-saved value live across a bl ->
	# CallerSavedLiveAcrossCall; a value in R4 on one join path but not the
	# other -> JoinValueNotAvailable; a BrTable -> NotAttempted loud
	# decline). The ra003_green_* tests assert it is SILENT on correct code.
	# (2) SILENT-ON-REAL-CODEGEN: the frozen suite compiles the whole ARM
	# fixture set THROUGH the unconditional validator; if it false-positived
	# on any real function that fixture would fail to compile, so 10/10 green
	# (control_step 0x00210A55, flight_algo 0x07FDF307 byte-identical) is the
	# validator's "Consistent on every real function" proof.
	# (3) PHASE-2 SILENT + FIRES ON REAL BRANCHY CODEGEN: the phase-2 repro
	# compiles branchy / memory-touching / call-bearing fixtures (real CF
	# joins the availability check reasons about) and asserts ZERO false
	# positives — the guard against the R11-linmem-base regression this lane
	# found (a join reading the reserved base register, defined nowhere in
	# the stream, must be seeded available not flagged).
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: RED-FIRST non-vacuity + silent-on-correct (validator unit tests)
	run: cargo test -p synth-synthesis --lib ra003_
	- name: Silent-on-real-codegen (frozen suite through the unconditional gate)
	run: cargo test -p synth-cli --test frozen_codegen_bytes
	- 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

	vcr-ra-003-rv32-alloc-validator-gate:
	name: "VCR-RA-003 RV32 register-allocation validator (red-first + frozen)"
	# VCR-RA-003 for RISC-V (#815, epic #242): the RV32 analogue of the ARM
	# register-allocation validator. A PARALLEL re-implementation
	# (synth_backend_riscv::alloc_validator::validate_final_allocation_rv32) keyed
	# on the RV32 calling convention — NOT a reuse of the ARM-coupled
	# validate_final_allocation. It runs UNCONDITIONALLY on every RV32 compile in
	# the default `--features riscv` build (wired in backend.rs
	# compile_function_with_opts, on the selector's `selection.ops`) and
	# hard-errors on a violation of the two STRAIGHT-LINE invariants #815 names:
	# (1) CALLEE-SAVED PRESERVATION — a body write of an s-register the pass
	# saves (s1, s2..s10, mirroring `preserve_callee_saved`; the reserved
	# s0/fp + s11/linmem-base excluded) must be saved by the prologue
	# `sw s_k, off(sp)` + restored by every epilogue `lw s_k, off(sp)` ->
	# CalleeSavedNotSaved / CalleeSavedNotRestored.
	# (2) SPILL-SLOT NON-ALIASING — a frame slot `off(sp)` overwritten by a
	# second `sw` while its value is still reloaded downstream, per
	# straight-line segment (an `addi sp` frame adjust resets the map) ->
	# SpillSlotAliased.
	# A `Call` (the ARM phase-2 across-call/across-join frontier, no RV CFG yet)
	# is a NON-FATAL NotAttempted (decline > guess). This job pins the gate:
	# (a) RED-FIRST non-vacuity: the ra003rv_red_* unit tests synthetically
	# revert a known-fixed clobber (drop the prologue save -> CalleeSavedNotSaved;
	# drop the epilogue restore -> CalleeSavedNotRestored; alias two live
	# values on one slot -> SpillSlotAliased) and assert the validator
	# CATCHES it. The ra003rv_green_* tests assert it is SILENT on correct
	# code + a Call -> NotAttempted.
	# (b) SILENT-ON-REAL-CODEGEN: the frozen RV32 oracle compiles the RV32
	# fixtures THROUGH the unconditional validator; if it false-positived on
	# a real function that fixture would fail to compile, so 10/10 green
	# (control_step 0x00210A55 byte-identical) is the "Consistent on every
	# real RV32 function" proof — PLUS a dedicated repro sweeping 9 fixtures
	# × {relocatable, default} = 18 pairs asserting ZERO false positives.
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: RED-FIRST non-vacuity + silent-on-correct (RV32 validator unit tests)
	run: cargo test -p synth-backend-riscv --lib ra003rv
	- name: Silent-on-real-codegen (frozen suite through the unconditional gate)
	run: cargo test -p synth-cli --test frozen_codegen_bytes
	- 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

	vcr-sel-005-cross-backend-op-parity-gate:
	name: "VCR-SEL-005 cross-backend op-parity (universe-complete + red-first)"
	# VCR-SEL-005 (#242, #223, #232): the "selector missed an op" class was never
	# a silent miscompile — it was a silent cross-backend DIVERGENCE: ARM lowered
	# an op RV32 loud-declined, so a function compiled on Cortex-M but was skipped
	# on RISC-V and nothing caught it until gale ran it on qemu. This gate makes
	# the divergence visible: for every WasmOp variant (a no-wildcard match — a
	# new op fails to compile until classified, so the universe is
	# compiler-enforced complete), the integer core is probed on BOTH the ARM
	# (select_with_stack) and RV32 selectors and must be at parity — both lower,
	# both decline, OR a ledgered one-sided divergence with a written reason. A
	# NEW un-ledgered one-sided gap FAILS the gate; a ledgered gap that has CLOSED
	# FAILS as stale. Float/f64/SIMD are StructurallyExcluded (their ARM lowering
	# is target-parameterized), tracked as separate parity gaps.
	# RED-FIRST non-vacuity: red_first_unledgered_one_sided_gap_is_caught drops
	# the real i32.rotl ledger entry and asserts the gate reports it as an
	# unexpected divergence on the REAL backends — proving it detects a genuine
	# one-sided op-gap, not a synthetic one, with no shipping-code change.
	# Test-only: emits nothing (.text byte-identical; frozen 10/10 unaffected).
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Universe-complete parity + red-first + ledger-liveness
	run: cargo test -p synth-backend-riscv --test cross_backend_op_parity

	repro-sweep-selector-oracle:
	name: repro sweep — selector / control-flow / call / i64 differentials
	# #890: these differentials existed in scripts/repro/ and NOTHING RAN THEM.
	# Each was written as the execution oracle for a specific miscompile (the
	# issue number is in the step name) and then left unwired, so every one of
	# those regressions was un-gated. They are batched here rather than given a
	# job each because they share one build and one pip install; the step name
	# identifies which oracle failed. The `# ci-status: wired` header in each
	# script is CHECKED against this file by scripts/oracle_wiring_check.py, so
	# deleting a step below turns the claim red instead of silently re-inerting
	# the gate.
	runs-on: ubuntu-latest
	env:
	SYNTH: ./target/debug/synth
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools capstone
	- name: Install wabt (wat2wasm — required by the newly-wired oracles)
	# #890: these oracles were never CI-run, so their host deps were never
	# discovered. wat2wasm is absent on the runner and several fixtures
	# build their .wasm from .wat at test time (the #850/#881 class).
	run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends wabt
	- name: a32 i64 execution differential (#615, cortex-r5)
	run: \|
	./target/debug/synth compile scripts/repro/a32_i64_615.wat --target cortex-r5 --all-exports --relocatable --no-optimize -o /tmp/a615.o
	python scripts/repro/a32_i64_615_differential.py /tmp/a615.o scripts/repro/a32_i64_615.wat
	- name: out-of-range ADD immediate differential (#350)
	run: \|
	./target/debug/synth compile scripts/repro/add_imm_large.wat -o /tmp/ail.elf --target cortex-m4f --all-exports --relocatable
	python scripts/repro/add_imm_large_differential.py /tmp/ail.elf
	- name: base-CSE execution differential (#468, default + opt-out)
	run: python scripts/repro/base_cse_differential.py
	- name: value-returning-branch differential (#509, both paths)
	run: python scripts/repro/br_table_value_509_differential.py
	- name: optimized-path forward-branch shapes (#500)
	run: python scripts/repro/cf_shapes_500_differential.py
	- name: const-only-body return differential (#791)
	run: python scripts/repro/const_body_791_differential.py
	- name: 5-argument call differential (#359)
	run: \|
	./target/debug/synth compile scripts/repro/call_5args.wat -o /tmp/c5.o --target cortex-m4f --native-pointer-abi --all-exports --relocatable
	python scripts/repro/call_5args_differential.py /tmp/c5.o
	- name: 6/7-argument stack-slot call differential (#359)
	run: \|
	./target/debug/synth compile scripts/repro/call_6_7args.wat -o /tmp/cm.o --target cortex-m4 --all-exports --relocatable
	python scripts/repro/call_6_7args_differential.py /tmp/cm.o
	- name: call_indirect A32 differential (#594, cortex-r5)
	run: \|
	./target/debug/synth compile scripts/repro/call_indirect_594.wat --target cortex-r5 --all-exports --relocatable --no-optimize -o /tmp/ci594.o
	python scripts/repro/call_indirect_594_differential.py /tmp/ci594.o
	- name: call_indirect thumb differential (#597, cortex-m3)
	run: \|
	./target/debug/synth compile scripts/repro/call_indirect_597.wat --target cortex-m3 --all-exports --relocatable --no-optimize -o /tmp/ci597.o
	python scripts/repro/call_indirect_597_differential.py /tmp/ci597.o
	- name: constant-divisor strength-reduction differential (#209)
	run: \|
	./target/debug/synth compile scripts/repro/div_const.wat -o /tmp/dc.elf --target cortex-m4 --relocatable
	python scripts/repro/div_const_differential.py /tmp/dc.elf
	- name: dynamic-table lookup differential (#359)
	run: \|
	./target/debug/synth compile scripts/repro/dyn_table_359.wat -o /tmp/dt.o --target cortex-m4 --native-pointer-abi --all-exports --relocatable
	python scripts/repro/dyn_table_359_differential.py /tmp/dt.o
	- name: branch-transparent reload forwarding on gust (#390)
	run: python scripts/repro/gust_spill_fwd_390_differential.py
	- name: i32 register-exhaustion spill differential (#242)
	run: \|
	./target/debug/synth compile scripts/repro/high_pressure_i32.wat -o /tmp/hp.elf --target cortex-m4 --relocatable
	python scripts/repro/high_pressure_i32_differential.py /tmp/hp.elf
	- name: i64 pair-spill differential (#242)
	run: \|
	./target/debug/synth compile scripts/repro/high_pressure_i64.wat -o /tmp/hp64.elf --target cortex-m4 --relocatable
	python scripts/repro/high_pressure_i64_differential.py /tmp/hp64.elf
	- name: i64.div_s(INT64_MIN,-1) overflow-trap differential (#633)
	run: python scripts/repro/i64_divs_overflow_633_differential.py
	- name: i64 global.get/set pair differential (#643, both selectors)
	run: python scripts/repro/i64_globals_643_differential.py
	- name: i64 pair-exhaustion spill differential (#587)
	run: \|
	SYNTH_SPILL_ON_EXHAUST=1 ./target/debug/synth compile scripts/repro/i64_pair_exhaust_587.wat -o /tmp/pe587.elf --target cortex-m4
	python scripts/repro/i64_pair_exhaust_587_differential.py /tmp/pe587.elf
	- name: i64.popcnt scratch-restore clobber differential (#632)
	run: python scripts/repro/i64_popcnt_632_differential.py
	- name: i64 shr_u/shr_s single-function path differential (#599)
	run: python scripts/repro/i64_shr_599_differential.py
	- name: dead-frame elision differential (#390, both flag states)
	run: python scripts/repro/leaf_dead_frame_differential.py
	- name: i32 local-promotion differential (#390, clean + dirty)
	run: \|
	./target/debug/synth compile scripts/repro/local_promote_i32.wat -o /tmp/lp.elf --target cortex-m4 --relocatable
	python scripts/repro/local_promote_i32_differential.py /tmp/lp.elf
	- name: param-bounded loop back-edge differential (#663)
	run: python scripts/repro/loop_param_bound_663_differential.py
	- name: arg-move-cycle-under-pressure differential (#326)
	run: \|
	./target/debug/synth compile scripts/repro/mutex_pressure.wat -o /tmp/mp.elf --target cortex-m4 --all-exports --relocatable
	python scripts/repro/mutex_pressure_differential.py /tmp/mp.elf
	- name: post-exhaustion cycle proxy, execution-matched (#242)
	run: python scripts/repro/postex_cycle_proxy.py
	- name: read-before-write local zero-init differential (#457)
	run: \|
	./target/debug/synth compile scripts/repro/read_before_write_local_zeroinit.wat -o /tmp/rbw.elf --target cortex-m4 --relocatable
	python scripts/repro/read_before_write_local_zeroinit_differential.py /tmp/rbw.elf
	- name: allocation-time Belady spill differential (#242)
	run: \|
	SYNTH_SPILL_ON_EXHAUST=1 ./target/debug/synth compile scripts/repro/spill_on_exhaust_242.wat -o /tmp/soe.elf --target cortex-m4
	python scripts/repro/spill_on_exhaust_242_differential.py /tmp/soe.elf
	- name: direct-selector spill-rung differential (#581)
	run: python scripts/repro/spill_rung_581_differential.py
	- name: sret shim differential (#359)
	run: \|
	./target/debug/synth compile scripts/repro/sret_decide.wasm -o /tmp/sret.o --target cortex-m4 --native-pointer-abi --all-exports --relocatable
	python scripts/repro/sret_decide_differential.py /tmp/sret.o
	- name: u64-unpack differential (#313)
	run: \|
	cp scripts/repro/u64_unpack.wat /tmp/u64repro.wat
	./target/debug/synth compile --target cortex-m4 --all-exports --relocatable scripts/repro/u64_unpack.wat -o /tmp/u64.elf
	python scripts/repro/u64_unpack_differential.py
	- name: u64-unpack if-with-result differential (#313)
	run: \|
	./target/debug/synth compile --target cortex-m4 --all-exports --relocatable scripts/repro/u64_unpack_if.wat -o /tmp/u64if.elf
	python scripts/repro/u64_unpack_if_differential.py
	- name: uxth/uxtb fold differential (#428, both flag states)
	run: python scripts/repro/uxth_fold_differential.py

	repro-sweep-memory-oracle:
	name: repro sweep — linear memory / static data / native-pointer differentials
	# #890 companion to the selector sweep: the memory-side oracles that were
	# written and never wired. The six mem757_* harnesses are the RED-FIRST
	# reconstructions of gale's wrong-segment miscompile — the class that
	# produced #757 — and none of them was running. postlink_359_oracle links a
	# REAL image with arm-none-eabi-ld (the #368 lesson: a unicorn-on-.o oracle
	# cannot see link-time retargeting), so binutils is installed for it here.
	runs-on: ubuntu-latest
	env:
	SYNTH: ./target/debug/synth
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools capstone
	- name: Install wabt (wat2wasm — required by the newly-wired oracles)
	# #890: these oracles were never CI-run, so their host deps were never
	# discovered. wat2wasm is absent on the runner and several fixtures
	# build their .wasm from .wat at test time (the #850/#881 class).
	run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends wabt
	- name: bulk-memory copy/fill numeric differential (#374)
	run: \|
	./target/debug/synth compile scripts/repro/bulk_memory_374_diff.wat -o /tmp/bmd.elf --target cortex-m7dp --all-exports --safety-bounds software
	python scripts/repro/bulk_memory_374_differential.py /tmp/bmd.elf
	- name: i64 large static offset differential (#382, direct path)
	run: python scripts/repro/i64_large_offset_382_differential.py
	- name: large static load/store offset differential (#382, optimized)
	run: python scripts/repro/load_store_big_offset_382_differential.py
	- name: memory.grow(0) differential (#539, both ARM paths)
	run: python scripts/repro/mem_grow_539_differential.py
	- name: static-src memmove differential (#757, inlined)
	run: python scripts/repro/mem757_inlined_memmove_differential.py
	- name: low-const-below-string chunked copy differential (#757)
	run: python scripts/repro/mem757_low_const_copy_differential.py
	- name: memory.copy from a static pointer differential (#757)
	run: python scripts/repro/mem757_memcopy_static_src_differential.py
	- name: memmove-with-param differential (#757)
	run: python scripts/repro/mem757_memmove_param_differential.py
	- name: chunked copy under register pressure differential (#757)
	run: python scripts/repro/mem757_pressure_chunks_differential.py
	- name: pointer-base copy differential (#757)
	run: python scripts/repro/mem757_ptr_base_copy_differential.py
	- name: multi-provider shared __stack_pointer co-rebase (#707)
	run: \|
	./target/debug/synth compile scripts/repro/mem707_multi_sp.wat -o /tmp/mem707.o --target cortex-m3 --native-pointer-abi --all-exports --relocatable --shadow-stack-size 512
	python scripts/repro/multi_sp_707_differential.py /tmp/mem707.o
	- name: native-pointer shadow-stack frame differential (#237)
	run: \|
	./target/debug/synth compile scripts/repro/native_pointer_shadow_stack.wat -o /tmp/np_ss.elf --target cortex-m4 --native-pointer-abi --all-exports --relocatable
	python scripts/repro/native_pointer_shadow_stack_differential.py /tmp/np_ss.elf
	- name: inline-statics down-shift differential (#678)
	run: \|
	./target/debug/synth compile scripts/repro/mem678_full.wat -o /tmp/mem678.o --target cortex-m3 --native-pointer-abi --all-exports --relocatable --shadow-stack-size 512
	python scripts/repro/native_pointer_static_downshift_678.py /tmp/mem678.o
	- name: volatile DMA-window back-off differential (#543, four builds)
	run: python scripts/repro/volatile_segment_543_differential.py
	- name: Install binutils-arm-none-eabi (#359 post-link oracle)
	run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends binutils-arm-none-eabi
	- name: post-link static-data placement oracle (#359)
	run: PATH=$PWD/target/debug:$PATH python scripts/repro/postlink_359_oracle.py

	repro-sweep-rv32-oracle:
	name: repro sweep — RISC-V RV32 execution differentials
	# #890: every RV32 oracle below pins a regression gale found on real
	# qemu_riscv32 silicon (#220 callee-saved, #226 live-range clobber, #232
	# overflow-guard clobber, #317 i64 sign, #343 if-join) — and none of them
	# was wired, so the backend those findings hardened had no standing
	# execution gate for them.
	runs-on: ubuntu-latest
	env:
	SYNTH: ./target/debug/synth
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools capstone
	- name: Install wabt (wat2wasm — required by the newly-wired oracles)
	# #890: these oracles were never CI-run, so their host deps were never
	# discovered. wat2wasm is absent on the runner and several fixtures
	# build their .wasm from .wat at test time (the #850/#881 class).
	run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends wabt
	- name: control_step RV32 correctness + ABI + shipped data (#223/#798)
	run: \|
	./target/debug/synth compile scripts/repro/control_step.wasm -b riscv -t rv32imac --all-exports --relocatable -o /tmp/cs_rv.o
	python scripts/repro/control_step_riscv_differential.py /tmp/cs_rv.o
	- name: controller_step RV32 live-range clobber differential (#226)
	run: \|
	./target/debug/synth compile scripts/repro/controller_step.wat -b riscv -t rv32imac --all-exports --relocatable -o /tmp/ctrl_rv.o
	python scripts/repro/controller_step_riscv_differential.py /tmp/ctrl_rv.o
	- name: RV32 callee-saved preservation differential (#220)
	run: \|
	./target/debug/synth compile scripts/repro/filter_axis.wasm -b riscv -t rv32imac --relocatable -o /tmp/fa.o
	python scripts/repro/filter_axis_riscv_differential.py /tmp/fa.o
	- name: RV32 i64 div_s/rem_s sign differential (#317)
	run: \|
	./target/debug/synth compile scripts/repro/i64_divs_317.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/i317.o
	python scripts/repro/i64_divs_317_riscv_differential.py /tmp/i317.o
	- name: RV32 i64-param LOUD-SKIP contrast oracle (#518)
	run: python scripts/repro/i64_param_518_riscv_loudskip.py
	- name: RV32 if-with-result join reconciliation (#343)
	run: \|
	./target/debug/synth compile scripts/repro/if_else_result_343.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/if343.o
	python scripts/repro/if_else_result_343_riscv_differential.py /tmp/if343.o
	- name: RV32 mask/software bounds effective-address oracle (#655)
	run: python scripts/repro/mask_bounds_655_riscv_differential.py
	- name: RV32 cmp->select fusion differential (#472)
	run: \|
	./target/debug/synth compile scripts/repro/rv32_cmp_select_472.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/cmpsel.o
	python scripts/repro/rv32_cmp_select_472_riscv_differential.py /tmp/cmpsel.o
	- name: RV32 i32 local-promotion differential (#472)
	run: \|
	./target/debug/synth compile scripts/repro/rv32_local_promotion_472.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/promo.o
	python scripts/repro/rv32_local_promotion_472_riscv_differential.py /tmp/promo.o
	- name: RV32 signed-div-const overflow-guard clobber (#232)
	run: \|
	./target/debug/synth compile scripts/repro/signed_div_const.wasm -b riscv -t rv32imac --all-exports --relocatable -o /tmp/sdiv.o
	python scripts/repro/signed_div_const_riscv_differential.py /tmp/sdiv.o
	- name: RV32 u64-unpack differential (#313)
	run: \|
	./target/debug/synth compile scripts/repro/u64_unpack_inlined.wat -b riscv -t rv32imac --all-exports --relocatable -o /tmp/u64_rv32.elf
	python scripts/repro/u64_unpack_riscv_differential.py

	repro-sweep-wcet-oracle:
	name: repro sweep — WCET bound soundness cross-checks (phases 2-5)
	# #890: the SOUNDNESS evidence for --emit-wcet. The cargo gate
	# (wcet_bound_gate.rs) pins the bounds analytically; these four harnesses
	# are the only thing that EXECUTES the fixtures under unicorn and checks
	# `bound_cycles >= executed_instructions`, i.e. that the bound synth
	# publishes is actually an upper bound. They were unwired — the soundness
	# claim in CLAUDE.md rested on a hand-run script.
	# SYNTH must be ABSOLUTE here: these harnesses chdir into a temp dir.
	runs-on: ubuntu-latest
	env:
	SYNTH: ${{ github.workspace }}/target/debug/synth
	steps:
	- uses: actions/checkout@v7
	- uses: dtolnay/rust-toolchain@stable
	- name: Cache Cargo dependencies
	uses: actions/cache@v6
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	target/
	key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
	restore-keys: \|
	${{ runner.os }}-cargo-
	- name: Build synth
	run: cargo build -p synth-cli
	- uses: actions/setup-python@v7
	with:
	python-version: "3.x"
	- name: Install emulation deps
	run: pip install wasmtime unicorn pyelftools capstone
	- name: Install wabt (wat2wasm — required by the newly-wired oracles)
	# #890: these oracles were never CI-run, so their host deps were never
	# discovered. wat2wasm is absent on the runner and several fixtures
	# build their .wasm from .wat at test time (the #850/#881 class).
	run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends wabt
	- name: WCET phase-2 const-loop bound soundness (#778)
	run: python scripts/repro/wcet_phase2_778_unicorn_soundness.py
	- name: WCET phase-3 inter-procedural composition soundness (#778)
	run: python scripts/repro/wcet_phase3_778_compose_soundness.py
	- name: WCET phase-4 bounded-recursion soundness (#49)
	run: python scripts/repro/wcet_phase4_49_recursion_soundness.py
	- name: WCET phase-5 masked-ceiling loop soundness (#778)
	run: python scripts/repro/wcet_phase5_778_masked_loop_soundness.py

Navigation Menu

Uh oh!

aarch64: br_table + value-carrying block/loop/if (#851, VCR-A64-CF-001) #1639

Workflow file

aarch64: br_table + value-carrying block/loop/if (#851, VCR-A64-CF-001) #1639

Uh oh!

Workflow file for this run