ci.yml

name: CI

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

env:
  CARGO_TERM_COLOR: always
  # #910: where scripts/oracle_run.py appends one JSON record per oracle it
  # drives. Workflow-level so no oracle job can forget it; jobs that run no
  # oracle simply never create the file.
  ORACLE_EVIDENCE_JSONL: oracle-evidence.jsonl

jobs:
  test:
    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.
      # #910 adds `--min-emulation-floor`: the summed `# ci-checks: emulations`
      # floors, i.e. the emulator entries the wired oracle surface ASSERTS on
      # every CI run. It is a RATCHET (direction: up) and a separate population
      # from the `Rust-test Line Coverage` percentage — which cannot see any of
      # it, because the oracles run the compiler as an uninstrumented
      # subprocess from other jobs. The literal below is pinned in claims.yaml
      # against the same number in scripts/repro/ORACLE_WIRING.md, so the gate
      # and the doc cannot drift apart.
      # RQ-56-CITE / #911 — the SAME shape as the oracle-wiring gate below, on
      # the artifacts surface, which never had one. `cargo test -- <filter>`
      # exits 0 when the filter matches NOTHING, so a rivet artifact could claim
      # verification by a test that does not exist. v0.55.0 shipped two such
      # citations; a post-release sweep found them, no gate did.
      #
      # Scoped to CLAIMING statuses (implemented/verified/accepted): under
      # draft/proposed a forward-looking citation is a plan, and flagging it
      # would make this gate noisy. A noisy gate gets ignored — that is how
      # codecov/patch stopped being read (#923).
      - name: Artifact citation gate — no artifact claims a test that does not exist (911)
        run: |
          set -euo pipefail
          python3 scripts/artifact_citation_check.py | tee /tmp/artifact-cites.log
          # Non-vacuity: assert it examined a NON-EMPTY population rather than
          # merely exiting 0 over nothing.
          grep -qE '^artifact citations: [1-9][0-9]* cited filters over [1-9][0-9]* test names' \
            /tmp/artifact-cites.log

      - name: Oracle wiring gate — every repro script declares a CI status (890)
        run: |
          set -euo pipefail
          python3 scripts/oracle_wiring_check.py --json /tmp/oracle-wiring.json --list \
            --min-emulation-floor 295421 \
            | 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"]),
                                ("checks_undeclared", s["checks_undeclared"]),
                                ("emulation_floor<100000",
                                 s["emulation_floor"] < 100000),
                                ("failures", s["failures"])) if v]
          if bad:
              sys.exit(f"oracle-wiring gate VACUOUS or DRIFTED {bad}: {s}")
          print(f"oracle-wiring gate is non-vacuous: it classified {s['total']} "
                f"scripts, {s['wired']} of them wired, {s['manual']} manual, "
                f"{s['unwired']} unwired-debt, 0 inert, and every wired oracle "
                f"declares a check floor ({s['emulation_floor']} emulator "
                f"entries asserted across "
                f"{s['checks_by_mode']['emulations']['scripts']} of them).")
          PY
      # The GitHub About surface (description + topics) is pinned verbatim in
      # claims.yaml's repo_metadata section. API/network failure = LOUD SKIP
      # (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:
    # RENAMED from "Code Coverage" (#910). The old name implied whole-system
    # coverage; the job measures ONE population — the Rust test suite, in-process,
    # under llvm-cov instrumentation.
    #
    # What it CANNOT see, structurally: the execution differentials. Those spawn
    # `$SYNTH` as a SEPARATE, UNINSTRUMENTED process, from OTHER jobs entirely
    # (`repro sweep-*`, `trap-semantics oracle`, the per-issue oracles). An
    # uninstrumented subprocess emits no profile data, so none of that execution
    # reaches this percentage. That is why backend.rs — almost pure ELF emission,
    # exercised end-to-end on every differential — reads ~42 % here.
    #
    # Consequence, stated so nobody has to rediscover it: this number UNDERSTATES
    # the testing that exists, and it is NOT a completeness measure. The
    # differential population is reported separately and in its own unit —
    # asserted executed checks, see scripts/oracle_run.py and the
    # `oracle-evidence-ledger` job. Do not add them together.
    #
    # Not a required status check on `main` (verified before renaming: renaming a
    # required context deadlocks every merge until protection is updated).
    name: Rust-test Line Coverage (unit + integration only)
    needs: [test]
    runs-on: [self-hosted, linux, x64, rust-cpu]
    steps:
      - 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.10
        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: Say what this number does and does not measure (#910)
        # The scope note travels WITH the number. Reading the percentage off the
        # job summary and reading this are the same act, which is the only way a
        # caveat survives being quoted.
        run: |
          set -euo pipefail
          test -s lcov.info
          {
            echo "### Rust-test line coverage — SCOPE (#910)"
            echo
            echo "Measures: \`cargo llvm-cov --workspace\` — the **Rust test suite**, in-process."
            echo
            echo "Does **not** measure: the execution differentials"
            echo "(\`scripts/repro/*.py\`). They spawn \`\$SYNTH\` as a separate,"
            echo "UNINSTRUMENTED process, from other jobs — no profile data reaches"
            echo "this figure. \`backend.rs\` reads ~42 % here while being exercised"
            echo "end-to-end by nearly every differential."
            echo
            echo "So this number **understates** the testing that exists, and is"
            echo "**not** a completeness measure. The differential population is"
            echo "reported separately, in executed checks, by the"
            echo "\`oracle evidence ledger\` job. **Do not add them together.**"
          } >> "$GITHUB_STEP_SUMMARY"
      - name: Upload to Codecov
        uses: codecov/codecov-action@v7
        with:
          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
        # THIS GATE HAD TWO HOLES, and v0.55 (#893) found them by finding two
        # OURS-not-theirs errors sitting in a green tree. Both are fixed below;
        # both fixes are red-first — replay this step's logic against the
        # pre-fix artifacts and it reports 2, against the fixed ones 0.
        #
        #  (1) `^  ERROR:` anchored on two-space-indented lines. rivet prefixes
        #      SOME diagnostics with the source file instead
        #      (`gale-integration.yaml: ERROR: …`), so that whole class was
        #      invisible here — including "artifact id X is declared more than
        #      once … the second definition silently overwrites the first",
        #      which is how GI-FPU-002 could be `implemented` in one file and
        #      `proposed` in another with this job green. Now every line
        #      containing `ERROR:` is considered.
        #  (2) The exemption `targets '.*:.*' which does not exist` exempted ANY
        #      target containing a colon — including `synth:396`, i.e. OUR OWN
        #      repo prefix. A `synth:`-prefixed target that does not resolve is
        #      not a cross-repo link into an un-rivet'd sibling; it is a broken
        #      link in our own graph (there, an issue NUMBER written where an
        #      artifact id belongs). Exemption is now "any prefix EXCEPT ours".
        #
        # Deliberately still exempt: kiln/gale/sigil/scry/jess/witness/loom/meld
        # targets, because those repos have no rivet project at the configured
        # path and the errors are unresolvable from this repo. Not an allowlist —
        # the rule is structural ("a foreign prefix"), so a new sibling repo does
        # not need this file edited, and our own prefix can never slip back in.
        run: |
          sed -i '/^externals:/,$d' rivet.yaml
          rivet validate 2>&1 | tee /tmp/rivet-output.txt
          grep -E "ERROR:" /tmp/rivet-output.txt > /tmp/rivet-errors.txt || true
          # Everything that is NOT a foreign-prefix broken link, ...
          grep -vE "targets '[A-Za-z0-9_.-]+:[^']*' which does not exist" /tmp/rivet-errors.txt \
            | grep -v "missing '.*' link to" > /tmp/rivet-ours.txt || true
          # ... plus foreign-looking links that actually carry OUR prefix.
          grep -E "targets 'synth:[^']*' which does not exist" /tmp/rivet-errors.txt >> /tmp/rivet-ours.txt || true
          NON_XREF=$(grep -c . /tmp/rivet-ours.txt || true)
          if [ "${NON_XREF:-0}" -gt 0 ]; then
            echo "::error::Found $NON_XREF rivet validation errors that are OURS (not cross-repo):"
            cat /tmp/rivet-ours.txt
            exit 1
          fi
          if [ -s /tmp/rivet-errors.txt ]; then
            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/oracle_run.py scripts/repro/cmp_select_two_move_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  provenance-gate:
    name: synth-provenance-v1 reconciliation gate (#396)
    # 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 moved on to the STRUCTURAL declines. v0.54 L3
    # then landed call_indirect + globals and v0.55 L6 (VCR-A64-CF-001)
    # `br_table` + value-carrying block/loop/if, so what the probe asserts today
    # is the NARROWER residue: param writes in a LEAF function, bulk memory,
    # SIMD, a `br_table` past 16 targets or with value-carrying targets, a block
    # type with params / multi-value results, and a non-leaf FLOAT param. Each
    # entry LEAVES this list the day its lowering lands — asserting a decline
    # for a capability that now ships is the same doc-honesty defect as claiming
    # one that does not.
    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/oracle_run.py scripts/repro/aarch64_add_538_differential.py
      - name: Run m2 broadened i32+i64 ALU execution oracle
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_m2_538_differential.py
      - name: Run m3 scalar-float execution oracle
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_m3_floats_538_differential.py
      - name: Run m4 trunc boundary-table + min/max NaN/±0 execution oracle
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_m4_trunc_minmax_538_differential.py
      - name: Run cf void-block br/br_if execution oracle (both branch edges)
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_cf_538_differential.py
      - name: Run #851 linear-memory load/store execution oracle
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_mem_851_differential.py
      - name: Run #851 div/rem trap + popcnt + reinterpret execution oracle (÷0 + INT_MIN/-1)
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_divrem_851_differential.py
      - name: Run #851 non-param locals execution oracle
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_locals_851_differential.py
      - name: Run #851 control-flow (if/else + loop back-edge + return) execution oracle
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_ctrlflow_851_differential.py
      - name: Run #865 linear-memory BOUNDS oracle (OOB traps + modes differ + mask/mpu hard-error)
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_bounds_865_differential.py
      - name: Run #851 v0.53 op-surface oracle (select x4 types + wrap/extends + drop/nop + memory.size/grow)
        # The VCR-SEL-005 third-backend closes: select (CSEL/FCSEL) incl.
        # NaN/-0 carry, wrap/extends with POISONED upper argument bits (the
        # AAPCS64 x-view hazard), drop/nop, fixed-memory size/grow parity
        # against a min=max module (growth failure is spec-forced there).
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_surface_851_differential.py
      - name: Run #851 lane L3 GLOBALS execution oracle (emitted .data region + persistence)
        # synth EMITS the globals region (a `.data` image carrying the decoded
        # initializers) and reaches it `adrp`+`add :lo12:` — no base register,
        # 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/oracle_run.py scripts/repro/aarch64_globals_851_differential.py | tee globals851.txt
          grep -Eq '^[1-9][0-9]* checks across [1-9][0-9]* exported' globals851.txt
          grep -q '^RESULT: PASS' globals851.txt
      - name: Run #851 lane L3 CALL_INDIRECT execution oracle (§4.4.8 OOB + null + type traps)
        # 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/oracle_run.py scripts/repro/aarch64_call_indirect_851_differential.py | tee ci851.txt
          grep -Eq '^[1-9][0-9]* checks \([1-9][0-9]* trap, [1-9][0-9]* value\)' ci851.txt
          grep -q '^RESULT: PASS' ci851.txt
      - name: Run v0.54 L2 float-completion oracle (#851 rounding / i64 converts / GUARDED i64 trunc / FP mem)
        # 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/oracle_run.py scripts/repro/aarch64_float_completion_851_differential.py \
            | tee /tmp/a64_floatdiff.log
          grep -q '^RESULT: PASS' /tmp/a64_floatdiff.log
          grep -Eq '^[0-9]+ wasmtime cases \([0-9]+ trap cases\)' /tmp/a64_floatdiff.log
          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/oracle_run.py \
              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/oracle_run.py scripts/repro/aarch64_m2_decline_538.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 15

  aarch64-native-matrix:
    name: aarch64 native execution matrix (gale #851 acceptance gate)
    # 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/oracle_run.py scripts/repro/aarch64_calls_851.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  trap-semantics-oracle:
    name: trap-semantics oracle (#665 unreachable + #666 rem_s)
    # #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/oracle_run.py scripts/repro/unreachable_665_differential.py
      - name: Run rem_s trap-table oracle (#666, rv32)
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/rem_s_666_differential.py
      - name: Run i32 shift-mask oracle (#682)
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/i32_shift_mask_682_differential.py
      - name: Run ADDW static-offset oracle (#681, incl. software-bounds bypass)
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/addw_offset_681_differential.py
      # #686: the same oracle under the mask-elision lever (opt-in,
      # SYNTH_SHIFT_MASK_ELIDE=1) — const amounts fold to the immediate form
      # mod 32, unproven amounts keep the mask; the >= 32 rows pin that the
      # elision never fires unsoundly (red-tested at land time).
      - name: Run i32 shift-mask oracle with mask elision ON (#686)
        run: SYNTH_SHIFT_MASK_ELIDE=1 SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/i32_shift_mask_682_differential.py
      # #846/#879: gale's REAL gpio-thin driver (pinned loom.wasm, never a
      # synthetic) under the default-ON mask elision — BOTH halves of the
      # v0.50.1 headline claim: (a) .text shrinks and the redundant mod-32
      # 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/oracle_run.py scripts/repro/gpio_thin_846_differential.py | tee gpio846.out
          grep -q "^#846 CHECKS=75/75" gpio846.out
      # #752: the software bounds guard must trap the top-of-address-space
      # wraparound class — the retired shape ADD-computed the end address
      # 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/oracle_run.py scripts/repro/safety_bounds_377_differential.py
      - name: Run bulk-memory operand-clobber oracle (#677, thumb2)
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/bulk_local_clobber_677_differential.py
      - name: Run bulk-memory mask-coverage oracle (#679, thumb2)
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/bulk_mask_679_differential.py
      # f32 hard-float SOUNDNESS oracles (GI-FPU-002). Dev-only before v0.40.0 —
      # the exact gap that let TWO silent miscompiles ship in v0.39.0 (trunc
      # saturation #709, and every compare returning 0 via a flag-clobber #712).
      # 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/oracle_run.py scripts/repro/f32_vfp_619_differential.py
      # #881: the VFP register-file spilling gate (GI-FPU-002 phase 1 S0..S15 +
      # phase 2 D0..D7) — the oracle behind the "falcon reaches the M7" claim,
      # so it must RUN, not merely exist. The lane wrote this differential and
      # 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/oracle_run.py scripts/repro/vfp_spill_881_differential.py | tee vfp881.out
          grep -q "^PASS: all 7 exports emitted (nm -> T)" vfp881.out
          grep -qE "^PASS: [1-9][0-9]+ execution rows bit-identical to wasmtime" vfp881.out
      # #708/#709: f32.load/reinterpret bit-casts + i32.trunc_f32 trap table.
      - name: Run f32 load/reinterpret + trunc-trap oracle (#708/#709, m4f)
        run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/f32_mem_trunc_708_709_differential.py
      # #719: the falcon f32 residual — f32.store, abs/neg/copysign, local.set/
      # tee, and mixed f32/int AAPCS-VFP params — bit-exact vs wasmtime on m4f,
      # including the copysign ±0/NaN-sign/±inf sign edges. m3 honest-reject.
      # #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/oracle_run.py scripts/repro/f32_ops_719_differential.py
      # #369 (GI-FPU-002 phase 2): the scalar f64 subset on cortex-m7dp —
      # const/promote_f32/arith/compare/load/store + f64-across-call, bit-exact
      # (NaN==NaN per Core §4.3.3) vs wasmtime under unicorn. Pins the
      # #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/oracle_run.py scripts/repro/f64_369_differential.py
      # #782a: the NONTRAPPING trunc_sat family (§4.3.2 — NaN→0, out-of-range
      # saturates, NEVER traps). Full boundary table (NaN/±inf/exact
      # INT_MIN-INT_MAX bounds/±0.5) vs wasmtime on BOTH prioritized backends:
      # 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/oracle_run.py scripts/repro/trunc_sat_782_differential.py
      # #869: the 64-bit integer<->float conversion family (gale's six +
      # the #756 i64.trunc_f64 pair) on cortex-m7dp — converts bit-exact
      # (incl. the round-to-odd double-rounding killers), the TRAPPING trunc
      # 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/oracle_run.py scripts/repro/i64_float_conv_869_differential.py
      # #782(b): float `select` + explicit float `return` — the dominant class
      # on the real falcon fused core (12/26 skips incl. run-stabilization was
      # "an integer operation popped an f32"): select over two f32/f64 values
      # (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/oracle_run.py scripts/repro/float_select_return_782_differential.py
      # #739: static ABOVE sp_init under --shadow-stack-size — the sub-word
      # load/store arms previously BAKED the linmem offset as an un-relocated
      # MOVW/MOVT immediate (invisible to the #678 reloc-walking rebase AND to
      # 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/oracle_run.py scripts/repro/static_above_sp_739_differential.py
      # #746 (the #739 residual): the i64/WIDE static-region arms — i64.load/
      # i64.store pair accesses plus the i64 narrow loads/stores (load8/16/32,
      # store8/16/32) — get the #744 relocation treatment instead of the loud
      # 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/oracle_run.py scripts/repro/wide_static_746_differential.py
      # #757: the multi-chunk static-copy CONTROL (gale's gust:os v0.4.0
      # static-string copy shape). The triage claimed the #746 fix miscompiles
      # the head chunk's source ADDRESS relocation; six faithful shapes — incl.
      # 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/oracle_run.py scripts/repro/wide_static_copy_757_differential.py
      # #757 v0.45 investigation: a RawVec-grow + memmove reconstruction of gale's
      # exact characterization (a >=9-byte static above wasm_data_base copied via a
      # bump-allocator memmove reached through a grow-call spill/reload). Seven such
      # 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/oracle_run.py 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/oracle_run.py scripts/repro/brif_outer_740_differential.py
      # #406 (VCR-MEM-002 phase 1): N wasm memories = N DISTINCT native base
      # regions. Memory 0 keeps the runtime R11 base; memory k > 0 is
      # addressed via its own __synth_wasm_data_<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/oracle_run.py scripts/repro/multi_memory_406_differential.py
      # #758: the DEFAULT self-contained `--cortex-m` image (no --relocatable,
      # no native-pointer ABI) must SHIP active memory-0 data segments. Before
      # the fix `.linear_memory` was NoBits and the reset path had no copy loop,
      # 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/oracle_run.py scripts/repro/self_contained_data_758_differential.py
      # #275: the DIRECT reachable call graph must EXECUTE on the self-contained
      # --cortex-m image (no --relocatable, no loader). Only `entry` is exported;
      # it calls two non-exported helpers, one of which calls a third — result
      # 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/oracle_run.py scripts/repro/reachable_callgraph_275_selfcontained_differential.py
      # Non-vacuity: a SEPARATE probe binary (feature `exports_only_275_probe`,
      # NEVER in the default/release build) exposes an `EXPORTS_ONLY_275=1` env
      # hatch that reverts to the pre-#235 exports-only drop (non-exported
      # 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/oracle_run.py scripts/repro/multi_segment_static_data_differential.py
      # #757: gale's EXACT fused os-tl node (loom.wasm) — the real miscompile that
      # 7 synthetic reconstructions could not reproduce (PR #772). Three active data
      # segments overlap at linmem 0x100000; the #354 reloc retargeting bound the
      # 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/oracle_run.py scripts/repro/mem757_gale_differential.py
      # VCR-VER-761: the self-contained --cortex-m full-page linmem view could
      # OVERLAP the R9 globals table at the top of SRAM — a store to the top of
      # the first page silently ALIASED a global slot (the R9 base was placed at
      # 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/oracle_run.py scripts/repro/mem761_linmem_r9_overlap_differential.py
      - name: Run #761 linmem<->globals overlap oracle (cortex-m4, low layout)
        run: EXTRA_SYNTH_FLAGS="--stack-layout low" SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/mem761_linmem_r9_overlap_differential.py
      # VCR-DEC-001 (epic #242, the North Star's first foothold): the
      # SYNTH_GRAPH_ALLOC whole-function graph-colouring allocator SPIKE. Gates
      # three properties on the ARM corpus: (1) flag-OFF ≡ the frozen goldens
      # (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/oracle_run.py scripts/repro/vcr_dec_001_graph_alloc_differential.py ./target/debug/synth
      # VCR-DEC-001 increments 2+3 (#242): EXECUTION-gate the DIVERGENT bytes the
      # join- and call-aware colouring now produces. This is NOT redundant with
      # the byte differential above: increment 1's correctness followed
      # 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.
      #
      # Increment 4 (VCR-REACH-001, v0.55) adds the i64 register-PAIR shapes and
      # the argument is the same a third time: `liveness::pair_effect` is SHARED
      # by the pass, `validate_cfg_rewrite` and the ABI observable contract, so
      # none of them can catch an error IN the model. Proven non-vacuous by
      # MUTATION, and this one is the sharpest of the three: deleting the
      # EARLY-CLOBBER interference edges (`pair_early_clobber`, the obligation a
      # defs/uses pair structurally cannot express) lets the colourer coalesce
      # `I64Ldr`'s `rdlo` onto a `base` the second `LDR` still re-reads —
      # `validate_cfg_rewrite` ACCEPTS all 7 functions, VCR-RA-003 reports
      # Consistent on all 7, the ABI observable contract passes all 7, and ONLY
      # this gate fails (3 wrong values). Three static instruments green, one
      # execution instrument red.
      #
      # The awk asserts the NON-ZERO check count, a non-zero engaged-function
      # count, the ≥4 engaged CALL-shape floor AND increment 4's two floors —
      # ≥4 engaged i64-PAIR functions and ≥2 of them containing a REAL i64 shift
      # expansion (detected in the emitted bytes). Exit 0 alone is not trusted,
      # and a run where the allocator stopped reaching one of these classes
      # would pass every comparison while leaving that whole class ungated.
      # Field positions under -F'[=/ ]':
      #   $3/$4 CHECKS, $6 ENGAGED, $8 CALLSHAPES, $10 PAIRSHAPES, $12 SHIFTSHAPES
      - name: Run VCR-DEC-001 join+call+i64-pair allocator execution differential (#242, thumb2)
        run: |
          set -euo pipefail
          SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/vcr_dec_001_join_alloc_execution_differential.py | tee ga_join.out
          grep -q "^VCR-DEC-001-JOIN CHECKS=" ga_join.out
          awk -F'[=/ ]' '/^VCR-DEC-001-JOIN/ { if ($3+0 > 0 && $3 == $4 && $6+0 > 0 && $8+0 >= 4 && $10+0 >= 4 && $12+0 >= 2) 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/oracle_run.py scripts/repro/rv32_data_798_boot_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 30

  instrument-independence-oracle:
    name: VCR-VER-004 instrument independence (#242, v0.53's mutation re-run)
    # 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/oracle_run.py scripts/repro/vcr_ver_004_shipping_path_audit.py | tee vcr_ver_004_ship.out
          grep -q "^VCR-VER-004-SHIPPING .* VIOLATED=0 " vcr_ver_004_ship.out
          test "$(grep -c '^  Holds ' vcr_ver_004_ship.out)" -eq 1
      # The grep asserts the machine-readable 4/4 AND a non-zero OK count (#890):
      # 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/oracle_run.py scripts/repro/vcr_ver_004_instrument_independence.py | tee vcr_ver_004.out
          grep -q "^VCR-VER-004-INDEPENDENCE ASSERTIONS=4/4$" vcr_ver_004.out
          test "$(grep -c '^OK   ' vcr_ver_004.out)" -eq 5
      - name: Assert the tree was restored (the mutation must never persist)
        run: git diff --exit-code
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 2

  fact-spec-oracle:
    name: fact-spec elision oracle (#494 phases 2 + 2b + 3+ + bounds)
    # 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/oracle_run.py scripts/repro/fact_spec_clamp_494_differential.py
      - name: Run wrong-bound loud-decline path
        run: >
          python scripts/oracle_run.py scripts/repro/fact_spec_clamp_494_differential.py
          --fact-lo 0 --fact-hi 4000 --expect-decline
      # #494 phase 2b — divisor-nonzero: in-bounds div/rem differential
      # (specialized ≡ wasmtime ≡ unspecialized over the proven divisor bound,
      # 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/oracle_run.py scripts/repro/fact_spec_div_494_differential.py
      - name: Run divisor-including-zero loud-decline path
        run: python scripts/oracle_run.py scripts/repro/fact_spec_div_494_differential.py --expect-decline
      - name: Run RED force-admit divergence demonstration
        run: python scripts/oracle_run.py scripts/repro/fact_spec_div_494_differential.py --force-admit
      # #494 phase 3 — branchless select-collapse: the sibling of the Phase-2
      # if-elision on the shape LLVM actually emits (min/max clamp via select).
      # In-bounds differential (specialized ≡ wasmtime ≡ unspecialized over the
      # proven bound; 2 collapses + gust_mix 50 B -> 14 B shrink required) and
      # the wrong-bound loud-decline byte-identity leg.
      - name: Run select-collapse in-bounds differential (proven bound)
        run: python scripts/oracle_run.py scripts/repro/fact_spec_select_494_differential.py
      - name: Run select-collapse wrong-bound loud-decline path
        run: >
          python scripts/oracle_run.py scripts/repro/fact_spec_select_494_differential.py
          --fact-lo 0 --fact-hi 4000 --expect-decline
      # #494 phase 3+ — redundant-mask (narrowing) elision: a proven-narrow
      # value makes an `i32.and` mask the identity, so it is deleted. On the
      # 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/oracle_run.py scripts/repro/fact_spec_mask_494_differential.py
      - name: Run mask-elision wrong-bound loud-decline path
        run: >
          python scripts/oracle_run.py scripts/repro/fact_spec_mask_494_differential.py
          --fact-lo 0 --fact-hi 4095 --expect-decline
      # #494 bounds-elision × #390 guard_bool — the `--safety-bounds software`
      # memory bounds guard falls to a per-site certificate:
      # 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/oracle_run.py scripts/repro/fact_spec_bounds_494_differential.py
      - name: Run bounds-including-OOB loud-decline path
        run: python scripts/oracle_run.py scripts/repro/fact_spec_bounds_494_differential.py --expect-decline
      - name: Run RED bounds force-admit divergence demonstration
        run: python scripts/oracle_run.py scripts/repro/fact_spec_bounds_494_differential.py --force-admit
      # #890: the phase-3+ rem_u IDENTITY differential lived in scripts/repro/
      # unwired, so the headline "with the fact, synth deletes the whole rem_u
      # (2 B) where clang -Os needs a 24 B reciprocal multiply-subtract" claim
      # 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/oracle_run.py scripts/repro/fact_spec_rem_494_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 6

  proven-safe-oracle:
    name: proven-safe bounds-elision oracle (VCR-MEM-004, #901)
    # VCR-MEM-004 (#901): `--proven-safe` consumes scry's safe-accesses.json
    # (schema scry/safe-accesses/v1, scry#114) and elides the
    # `--safety-bounds software` inline guard at the access sites scry PROVED
    # in-bounds. This job gates the three safety properties, not the speedup:
    #   (1) FAIL CLOSED on module_sha256 / memory_min_bytes / malformed input;
    #   (2) ABSENCE MEANS "NOT PROVEN" — a partial verdict list leaves exactly
    #       the unproven guards standing, and their out-of-bounds accesses
    #       still TRAP under execution;
    #   (3) a genuine elision that is result-identical to wasmtime.
    # The differential's fail-closed leg is a permanent regression gate: it
    # applies one module's verdicts to a MUTATED module whose keys all still
    # validate, so deleting the hash comparison turns it RED with a real
    # UC_ERR_READ_UNMAPPED (verified by mutation when #901 landed).
    # 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-
      # Unit level: the fail-closed ingestion gates (synth-core) and the
      # dep-free ProvenSafeBoundsChecker trait semantics (synth-memory).
      - name: Run ingestion + BoundsChecker unit gates
        run: cargo test -p synth-core --lib proven_safe && cargo test -p synth-memory --lib
      # Byte evidence: the partial-list partition, the refusals, the key-space
      # canary, and the attestation contents.
      - name: Run --proven-safe byte gates (#901)
        run: cargo test -p synth-cli --test proven_safe_bounds_901
      # The fact-spec combination refusal needs the solver-carrying build (the
      # pass is inert without it), so it is a separate feature-gated run.
      - name: Run the fact-spec-combination refusal gate (verify feature)
        run: cargo test -p synth-cli --features verify --test proven_safe_bounds_901
      - 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 --proven-safe execution differential (#901)
        env:
          SYNTH: ./target/debug/synth
        run: |
          set -euo pipefail
          python scripts/oracle_run.py \
            scripts/repro/proven_safe_bounds_901_differential.py \
            | tee /tmp/proven_safe_901.log
          grep -q '^RESULT: PASS' /tmp/proven_safe_901.log
          # Non-vacuity: a differential that checked nothing must not pass.
          grep -qE '^#901 CHECKS=[1-9][0-9]*/[1-9][0-9]*$' /tmp/proven_safe_901.log
          grep -q 'absence-is-not-safety: [1-9]' /tmp/proven_safe_901.log
          grep -q 'fail-closed: stale verdicts REFUSED' /tmp/proven_safe_901.log

  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/oracle_run.py scripts/repro/shift_fold_riscv_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  rv32-const-addr-fold-oracle:
    name: rv32 const-address-fold execution oracle
    # 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/oracle_run.py scripts/repro/const_addr_fold_riscv_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  rv32-br-table-oracle:
    name: rv32 br_table execution oracle (#882)
    # #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/oracle_run.py scripts/repro/rv32_br_table_882_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  rv32-extern-call-reloc-oracle:
    name: rv32 external-call relocation oracle (#871)
    # #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/oracle_run.py scripts/repro/riscv_extern_call_871_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  rv32-label-return-oracle:
    name: rv32 label/return dead-code oracle (#882)
    # #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/oracle_run.py scripts/repro/rv32_label_882_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  rv32-mem-size-grow-oracle:
    name: rv32 memory.size / memory.grow execution oracle
    # 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/oracle_run.py scripts/repro/rv32_mem_size_grow_242_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  callee-saved-490-oracle:
    name: optimized-path callee-saved preservation oracle
    # 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/oracle_run.py scripts/repro/callee_saved_490_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  call-indirect-642-oracle:
    name: call_indirect bounds-guard oracle (Thumb-2 + A32)
    # 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/oracle_run.py scripts/repro/call_indirect_642_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  call-indirect-650-multitable-oracle:
    name: multi-table call_indirect oracle (Thumb-2 + A32)
    # 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/oracle_run.py scripts/repro/call_indirect_650_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  call-indirect-664-nullslot-oracle:
    name: null-funcref-slot call_indirect oracle (Thumb-2 + A32)
    # 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/oracle_run.py scripts/repro/call_indirect_664_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  call-indirect-676-heterogeneous-oracle:
    name: heterogeneous-table call_indirect oracle (Thumb-2 + A32)
    # 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/oracle_run.py scripts/repro/call_indirect_676_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  call-indirect-275-selfcontained-oracle:
    name: self-contained call_indirect oracle (execution + residual declines)
    # #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/oracle_run.py scripts/repro/call_indirect_275_selfcontained_execution_differential.py
      - name: Run emission + residual-decline oracle
        env:
          SYNTH: ./target/debug/synth
        run: python scripts/oracle_run.py scripts/repro/call_indirect_275_selfcontained_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 2

  block-brif-483-oracle:
    name: optimized-path block/br_if lowering oracle
    # 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/oracle_run.py scripts/repro/block_brif_483_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  spill-frame-499-oracle:
    name: optimized-path spill-frame teardown oracle
    # #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/oracle_run.py scripts/repro/spill_frame_499_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  r12-spill-496-oracle:
    name: optimized-path register-exhaustion oracle
    # 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/oracle_run.py scripts/repro/r12_spill_496_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  flight-seam-570-oracle:
    name: flight-seam relocatable-path execution oracle
    # 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/oracle_run.py scripts/repro/flight_seam_differential.py /tmp/fs.elf
          ./target/debug/synth compile scripts/repro/flight_seam_flat.wasm \
            -o /tmp/fsf.elf --target cortex-m4 --all-exports --relocatable
          python scripts/oracle_run.py scripts/repro/flight_seam_differential.py /tmp/fsf.elf \
            scripts/repro/flight_seam_flat.wasm
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  control-step-584-oracle:
    name: control-step relocatable-path execution oracle
    # 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/oracle_run.py scripts/repro/control_step_differential.py /tmp/cs.elf
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  stack-args-503-oracle:
    name: AAPCS stack-argument path oracle
    # 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/oracle_run.py scripts/repro/stack_args_503_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  i64-completeness-503-587-oracle:
    name: i64 stack-param + spill-pool-grow oracle
    # 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/oracle_run.py scripts/repro/i64_stack_param_503_differential.py
      - name: Run i64 spill-pool-grow oracle (#587)
        env:
          SYNTH: ./target/debug/synth
        run: python scripts/oracle_run.py scripts/repro/i64_spill_pool_587_differential.py
      - name: Run i64-param correctness + decline oracle (#518, d_call now emits #837)
        env:
          SYNTH: ./target/debug/synth
        run: python scripts/oracle_run.py scripts/repro/i64_param_518_differential.py
      - name: Run frame-backing i64-param-with-call oracle (#837 gale gust:os/timer)
        env:
          SYNTH: ./target/debug/synth
        run: python scripts/oracle_run.py scripts/repro/framebacking_i64param_837_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 4

  i64-rot-div-610-oracle:
    name: i64 rotl/rotr/div/rem expansion oracle
    # 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/oracle_run.py scripts/repro/i64_rot_div_610_differential.py target/debug/synth
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  br-table-507-oracle:
    name: optimized-path br_table oracle
    # 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/oracle_run.py scripts/repro/br_table_507_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  const-cse-242-oracle:
    name: const-CSE flag-on execution oracle
    # 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/oracle_run.py scripts/repro/const_cse_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  frame-slot-dce-242-oracle:
    name: frame-slot DCE default+optout execution oracle
    # 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/oracle_run.py scripts/repro/frame_slot_dce_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  stack-layout-687-oracle:
    name: stack-layout=low overflow BusFault oracle
    # 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/oracle_run.py scripts/repro/stack_layout_687_differential.py
      - name: Run the #649 global-init differential under --stack-layout=low
        env:
          SYNTH: ./target/debug/synth
          EXTRA_SYNTH_FLAGS: "--stack-layout low"
        run: python scripts/oracle_run.py scripts/repro/i64_global_init_649_differential.py

  # #418: self-contained binding of the meld-dissolve embedder import
  # `env::__cabi_arena_realloc` — the compile must yield an ET_EXEC image
  # (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.
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 2

  arena-bind-418-oracle:
    name: "#418 arena-bind self-contained execution oracle"
    runs-on: ubuntu-latest
    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/oracle_run.py scripts/repro/cabi_arena_bind_418_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  vcr-ra-003-alloc-validator-gate:
    name: "VCR-RA-003 register-allocation validator (red-first + frozen)"
    # 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/oracle_run.py scripts/repro/vcr_ra_003_phase2_join_call.py ./target/debug/synth
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  vcr-ra-003-rv32-alloc-validator-gate:
    name: "VCR-RA-003 RV32 register-allocation validator (red-first + frozen)"
    # 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/oracle_run.py scripts/repro/vcr_ra_003_rv32_alloc_validator.py ./target/debug/synth
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 1

  vcr-sel-005-cross-backend-op-parity-gate:
    name: "VCR-SEL-005 cross-backend op-parity (universe-complete + red-first)"
    # 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/oracle_run.py scripts/repro/a32_i64_615_differential.py /tmp/a615.o scripts/repro/a32_i64_615.wat
      - name: out-of-range ADD immediate differential (#350)
        run: |
          ./target/debug/synth compile scripts/repro/add_imm_large.wat -o /tmp/ail.elf --target cortex-m4f --all-exports --relocatable
          python scripts/oracle_run.py scripts/repro/add_imm_large_differential.py /tmp/ail.elf
      - name: base-CSE execution differential (#468, default + opt-out)
        run: python scripts/oracle_run.py scripts/repro/base_cse_differential.py
      - name: value-returning-branch differential (#509, both paths)
        run: python scripts/oracle_run.py scripts/repro/br_table_value_509_differential.py
      - name: optimized-path forward-branch shapes (#500)
        run: python scripts/oracle_run.py scripts/repro/cf_shapes_500_differential.py
      - name: const-only-body return differential (#791)
        run: python scripts/oracle_run.py scripts/repro/const_body_791_differential.py
      - name: 5-argument call differential (#359)
        run: |
          ./target/debug/synth compile scripts/repro/call_5args.wat -o /tmp/c5.o --target cortex-m4f --native-pointer-abi --all-exports --relocatable
          python scripts/oracle_run.py scripts/repro/call_5args_differential.py /tmp/c5.o
      - name: 6/7-argument stack-slot call differential (#359)
        run: |
          ./target/debug/synth compile scripts/repro/call_6_7args.wat -o /tmp/cm.o --target cortex-m4 --all-exports --relocatable
          python scripts/oracle_run.py scripts/repro/call_6_7args_differential.py /tmp/cm.o
      - name: call_indirect A32 differential (#594, cortex-r5)
        run: |
          ./target/debug/synth compile scripts/repro/call_indirect_594.wat --target cortex-r5 --all-exports --relocatable --no-optimize -o /tmp/ci594.o
          python scripts/oracle_run.py scripts/repro/call_indirect_594_differential.py /tmp/ci594.o
      - name: call_indirect thumb differential (#597, cortex-m3)
        run: |
          ./target/debug/synth compile scripts/repro/call_indirect_597.wat --target cortex-m3 --all-exports --relocatable --no-optimize -o /tmp/ci597.o
          python scripts/oracle_run.py scripts/repro/call_indirect_597_differential.py /tmp/ci597.o
      - name: constant-divisor strength-reduction differential (#209)
        run: |
          ./target/debug/synth compile scripts/repro/div_const.wat -o /tmp/dc.elf --target cortex-m4 --relocatable
          python scripts/oracle_run.py scripts/repro/div_const_differential.py /tmp/dc.elf
      - name: dynamic-table lookup differential (#359)
        run: |
          ./target/debug/synth compile scripts/repro/dyn_table_359.wat -o /tmp/dt.o --target cortex-m4 --native-pointer-abi --all-exports --relocatable
          python scripts/oracle_run.py scripts/repro/dyn_table_359_differential.py /tmp/dt.o
      - name: branch-transparent reload forwarding on gust (#390)
        run: python scripts/oracle_run.py scripts/repro/gust_spill_fwd_390_differential.py
      - name: i32 register-exhaustion spill differential (#242)
        run: |
          ./target/debug/synth compile scripts/repro/high_pressure_i32.wat -o /tmp/hp.elf --target cortex-m4 --relocatable
          python scripts/oracle_run.py scripts/repro/high_pressure_i32_differential.py /tmp/hp.elf
      - name: i64 pair-spill differential (#242)
        run: |
          ./target/debug/synth compile scripts/repro/high_pressure_i64.wat -o /tmp/hp64.elf --target cortex-m4 --relocatable
          python scripts/oracle_run.py scripts/repro/high_pressure_i64_differential.py /tmp/hp64.elf
      - name: i64.div_s(INT64_MIN,-1) overflow-trap differential (#633)
        run: python scripts/oracle_run.py scripts/repro/i64_divs_overflow_633_differential.py
      - name: i64 global.get/set pair differential (#643, both selectors)
        run: python scripts/oracle_run.py scripts/repro/i64_globals_643_differential.py
      - name: i64 pair-exhaustion spill differential (#587)
        run: |
          SYNTH_SPILL_ON_EXHAUST=1 ./target/debug/synth compile scripts/repro/i64_pair_exhaust_587.wat -o /tmp/pe587.elf --target cortex-m4
          python scripts/oracle_run.py scripts/repro/i64_pair_exhaust_587_differential.py /tmp/pe587.elf
      - name: i64.popcnt scratch-restore clobber differential (#632)
        run: python scripts/oracle_run.py scripts/repro/i64_popcnt_632_differential.py
      - name: i64 shr_u/shr_s single-function path differential (#599)
        run: python scripts/oracle_run.py scripts/repro/i64_shr_599_differential.py
      - name: i64 high-register zero-fill differential (#916)
        run: |
          set -euo pipefail
          ./target/debug/synth compile scripts/repro/i64_high_reg_zero_fill_916.wat \
            -o /tmp/zf916.elf --target cortex-m4 --relocatable --all-exports
          python scripts/oracle_run.py \
            scripts/repro/i64_high_reg_zero_fill_916_differential.py /tmp/zf916.elf
      - name: dead-frame elision differential (#390, both flag states)
        run: python scripts/oracle_run.py scripts/repro/leaf_dead_frame_differential.py
      - name: i32 local-promotion differential (#390, clean + dirty)
        run: |
          ./target/debug/synth compile scripts/repro/local_promote_i32.wat -o /tmp/lp.elf --target cortex-m4 --relocatable
          python scripts/oracle_run.py scripts/repro/local_promote_i32_differential.py /tmp/lp.elf
      - name: param-bounded loop back-edge differential (#663)
        run: python scripts/oracle_run.py scripts/repro/loop_param_bound_663_differential.py
      - name: arg-move-cycle-under-pressure differential (#326)
        run: |
          ./target/debug/synth compile scripts/repro/mutex_pressure.wat -o /tmp/mp.elf --target cortex-m4 --all-exports --relocatable
          python scripts/oracle_run.py scripts/repro/mutex_pressure_differential.py /tmp/mp.elf
      - name: post-exhaustion cycle proxy, execution-matched (#242)
        run: python scripts/oracle_run.py scripts/repro/postex_cycle_proxy.py
      - name: read-before-write local zero-init differential (#457)
        run: |
          ./target/debug/synth compile scripts/repro/read_before_write_local_zeroinit.wat -o /tmp/rbw.elf --target cortex-m4 --relocatable
          python scripts/oracle_run.py scripts/repro/read_before_write_local_zeroinit_differential.py /tmp/rbw.elf
      - name: allocation-time Belady spill differential (#242)
        run: |
          SYNTH_SPILL_ON_EXHAUST=1 ./target/debug/synth compile scripts/repro/spill_on_exhaust_242.wat -o /tmp/soe.elf --target cortex-m4
          python scripts/oracle_run.py scripts/repro/spill_on_exhaust_242_differential.py /tmp/soe.elf
      - name: direct-selector spill-rung differential (#581)
        run: python scripts/oracle_run.py scripts/repro/spill_rung_581_differential.py
      - name: sret shim differential (#359)
        run: |
          ./target/debug/synth compile scripts/repro/sret_decide.wasm -o /tmp/sret.o --target cortex-m4 --native-pointer-abi --all-exports --relocatable
          python scripts/oracle_run.py scripts/repro/sret_decide_differential.py /tmp/sret.o
      - name: u64-unpack differential (#313)
        run: |
          cp scripts/repro/u64_unpack.wat /tmp/u64repro.wat
          ./target/debug/synth compile --target cortex-m4 --all-exports --relocatable scripts/repro/u64_unpack.wat -o /tmp/u64.elf
          python scripts/oracle_run.py scripts/repro/u64_unpack_differential.py
      - name: u64-unpack if-with-result differential (#313)
        run: |
          ./target/debug/synth compile --target cortex-m4 --all-exports --relocatable scripts/repro/u64_unpack_if.wat -o /tmp/u64if.elf
          python scripts/oracle_run.py scripts/repro/u64_unpack_if_differential.py
      - name: uxth/uxtb fold differential (#428, both flag states)
        run: python scripts/oracle_run.py scripts/repro/uxth_fold_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 32

  repro-sweep-memory-oracle:
    name: repro sweep — linear memory / static data / native-pointer differentials
    # #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/oracle_run.py scripts/repro/bulk_memory_374_differential.py /tmp/bmd.elf
      - name: i64 large static offset differential (#382, direct path)
        run: python scripts/oracle_run.py scripts/repro/i64_large_offset_382_differential.py
      - name: large static load/store offset differential (#382, optimized)
        run: python scripts/oracle_run.py scripts/repro/load_store_big_offset_382_differential.py
      - name: memory.grow(0) differential (#539, both ARM paths)
        run: python scripts/oracle_run.py scripts/repro/mem_grow_539_differential.py
      - name: static-src memmove differential (#757, inlined)
        run: python scripts/oracle_run.py scripts/repro/mem757_inlined_memmove_differential.py
      - name: low-const-below-string chunked copy differential (#757)
        run: python scripts/oracle_run.py scripts/repro/mem757_low_const_copy_differential.py
      - name: memory.copy from a static pointer differential (#757)
        run: python scripts/oracle_run.py scripts/repro/mem757_memcopy_static_src_differential.py
      - name: memmove-with-param differential (#757)
        run: python scripts/oracle_run.py scripts/repro/mem757_memmove_param_differential.py
      - name: chunked copy under register pressure differential (#757)
        run: python scripts/oracle_run.py scripts/repro/mem757_pressure_chunks_differential.py
      - name: pointer-base copy differential (#757)
        run: python scripts/oracle_run.py scripts/repro/mem757_ptr_base_copy_differential.py
      - name: multi-provider shared __stack_pointer co-rebase (#707)
        run: |
          ./target/debug/synth compile scripts/repro/mem707_multi_sp.wat -o /tmp/mem707.o --target cortex-m3 --native-pointer-abi --all-exports --relocatable --shadow-stack-size 512
          python scripts/oracle_run.py scripts/repro/multi_sp_707_differential.py /tmp/mem707.o
      - name: native-pointer shadow-stack frame differential (#237)
        run: |
          ./target/debug/synth compile scripts/repro/native_pointer_shadow_stack.wat -o /tmp/np_ss.elf --target cortex-m4 --native-pointer-abi --all-exports --relocatable
          python scripts/oracle_run.py scripts/repro/native_pointer_shadow_stack_differential.py /tmp/np_ss.elf
      - name: inline-statics down-shift differential (#678)
        run: |
          ./target/debug/synth compile scripts/repro/mem678_full.wat -o /tmp/mem678.o --target cortex-m3 --native-pointer-abi --all-exports --relocatable --shadow-stack-size 512
          python scripts/oracle_run.py scripts/repro/native_pointer_static_downshift_678.py /tmp/mem678.o
      - name: volatile DMA-window back-off differential (#543, four builds)
        run: python scripts/oracle_run.py scripts/repro/volatile_segment_543_differential.py
      - name: Install binutils-arm-none-eabi (#359 post-link oracle)
        run: sudo apt-get update -qq && sudo apt-get install -y --no-install-recommends binutils-arm-none-eabi
      - name: post-link static-data placement oracle (#359)
        run: PATH=$PWD/target/debug:$PATH python scripts/oracle_run.py scripts/repro/postlink_359_oracle.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 15

  repro-sweep-rv32-oracle:
    name: repro sweep — RISC-V RV32 execution differentials
    # #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/oracle_run.py scripts/repro/control_step_riscv_differential.py /tmp/cs_rv.o
      - name: controller_step RV32 live-range clobber differential (#226)
        run: |
          ./target/debug/synth compile scripts/repro/controller_step.wat -b riscv -t rv32imac --all-exports --relocatable -o /tmp/ctrl_rv.o
          python scripts/oracle_run.py scripts/repro/controller_step_riscv_differential.py /tmp/ctrl_rv.o
      - name: RV32 callee-saved preservation differential (#220)
        run: |
          ./target/debug/synth compile scripts/repro/filter_axis.wasm -b riscv -t rv32imac --relocatable -o /tmp/fa.o
          python scripts/oracle_run.py scripts/repro/filter_axis_riscv_differential.py /tmp/fa.o
      - name: RV32 i64 div_s/rem_s sign differential (#317)
        run: |
          ./target/debug/synth compile scripts/repro/i64_divs_317.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/i317.o
          python scripts/oracle_run.py scripts/repro/i64_divs_317_riscv_differential.py /tmp/i317.o
      - name: RV32 i64-param LOUD-SKIP contrast oracle (#518)
        run: python scripts/oracle_run.py scripts/repro/i64_param_518_riscv_loudskip.py
      - name: RV32 if-with-result join reconciliation (#343)
        run: |
          ./target/debug/synth compile scripts/repro/if_else_result_343.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/if343.o
          python scripts/oracle_run.py scripts/repro/if_else_result_343_riscv_differential.py /tmp/if343.o
      - name: RV32 mask/software bounds effective-address oracle (#655)
        run: python scripts/oracle_run.py scripts/repro/mask_bounds_655_riscv_differential.py
      - name: RV32 cmp->select fusion differential (#472)
        run: |
          ./target/debug/synth compile scripts/repro/rv32_cmp_select_472.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/cmpsel.o
          python scripts/oracle_run.py scripts/repro/rv32_cmp_select_472_riscv_differential.py /tmp/cmpsel.o
      - name: RV32 i32 local-promotion differential (#472)
        run: |
          ./target/debug/synth compile scripts/repro/rv32_local_promotion_472.wat -b riscv --target riscv32imac --relocatable --all-exports -o /tmp/promo.o
          python scripts/oracle_run.py scripts/repro/rv32_local_promotion_472_riscv_differential.py /tmp/promo.o
      - name: RV32 signed-div-const overflow-guard clobber (#232)
        run: |
          ./target/debug/synth compile scripts/repro/signed_div_const.wasm -b riscv -t rv32imac --all-exports --relocatable -o /tmp/sdiv.o
          python scripts/oracle_run.py scripts/repro/signed_div_const_riscv_differential.py /tmp/sdiv.o
      - name: RV32 u64-unpack differential (#313)
        run: |
          ./target/debug/synth compile scripts/repro/u64_unpack_inlined.wat -b riscv -t rv32imac --all-exports --relocatable -o /tmp/u64_rv32.elf
          python scripts/oracle_run.py scripts/repro/u64_unpack_riscv_differential.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 11

  repro-sweep-wcet-oracle:
    name: repro sweep — WCET bound soundness cross-checks (phases 2-5)
    # #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/oracle_run.py scripts/repro/wcet_phase2_778_unicorn_soundness.py
      - name: WCET phase-3 inter-procedural composition soundness (#778)
        run: python scripts/oracle_run.py scripts/repro/wcet_phase3_778_compose_soundness.py
      - name: WCET phase-4 bounded-recursion soundness (#49)
        run: python scripts/oracle_run.py scripts/repro/wcet_phase4_49_recursion_soundness.py
      - name: WCET phase-5 masked-ceiling loop soundness (#778)
        run: python scripts/oracle_run.py scripts/repro/wcet_phase5_778_masked_loop_soundness.py
      # #910: close the job with what it EXECUTED. Asserts every oracle
      # met its declared floor AND that the expected number of them
      # reported at all — a step deleted, commented out, or skipped by an
      # early exit leaves the ledger short, which is a red job rather than
      # a quietly smaller number. Also writes the measured totals to the
      # step summary, per unit, never summed.
      - name: Differential evidence ledger (#910)
        if: always()
        run: |
          set -euo pipefail
          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 4