Skip to content
CI

chore(release): v0.34.0 — multi-table call_indirect + global inits + sound mask bounds #1147

Sign in to view logs

chore(release): v0.34.0 — multi-table call_indirect + global inits + sound mask bounds

chore(release): v0.34.0 — multi-table call_indirect + global inits + sound mask bounds #1147

Workflow file for this run

.github/workflows/ci.yml at 46d6e35
name: CI
on:
push:
branches: [main]
pull_request:
branches: [main]
env:
CARGO_TERM_COLOR: always
jobs:
test:
name: Test
# NOTE: stays on ubuntu-latest for now. It originally moved here from
# [self-hosted, linux, x64, rust-cpu] because z3-sys's C++ build exhausted
# the smithy runners' temp disk — that pressure is gone (#553: synth-verify
# defaults to the pure-Rust ordeal engine, z3 is behind the off-by-default
# `z3-solver` feature), so moving back is a possible follow-up.
runs-on: ubuntu-latest
env:
RUSTFLAGS: -Dwarnings
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 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
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
verify:
name: Z3 Verification
# #553 steps 3/4: this is now the ONLY job that builds 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.
# Stays on ubuntu-latest: needs `sudo apt-get install -y libz3-dev`
# (smithy runners have no sudo). Move once libz3-dev is added to
# the smithy toolchains role.
runs-on: ubuntu-latest
env:
SYNTH_SOLVER_DIFF: "1"
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 Z3
run: sudo apt-get update && sudo apt-get install -y libz3-dev
- name: Run verification tests (differential ordeal vs Z3)
run: cargo test -p synth-verify --features z3-solver,arm
- name: Run comprehensive verification (differential ordeal vs Z3)
run: cargo test -p synth-verify --test comprehensive_verification --features z3-solver,arm
coverage:
name: Code Coverage
needs: [test]
runs-on: [self-hosted, linux, x64, rust-cpu]
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@nightly
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-coverage-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-coverage-
- name: Install cargo-llvm-cov
uses: taiki-e/install-action@v2
with:
tool: cargo-llvm-cov
- name: Generate coverage (LCOV)
# synth-verify is no longer excluded (#553): the default feature set is
# pure Rust (ordeal), so its tests run under llvm-cov like any crate.
run: |
cargo llvm-cov --workspace --lcov --output-path lcov.info \
--exclude synth-qemu \
--exclude synth-backend-awsm --exclude synth-backend-wasker
- name: Upload to Codecov
uses: codecov/codecov-action@v7
with:
files: lcov.info
fail_ci_if_error: false
env:
CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }}
kani:
name: Kani Verification
# Stays on ubuntu-latest: Kani-CBMC bundle is not yet provisioned
# in the smithy toolchains role (tracked in playbook out-of-scope
# table). Move once smithy ships kani-verifier + CBMC.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- name: Install Kani
run: cargo install --locked kani-verifier && cargo kani setup
- name: Run Kani proofs
run: cargo kani -p synth-backend --tests
timeout-minutes: 30
rivet:
name: Rivet Validation
runs-on: [self-hosted, linux, x64, rust-cpu]
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
# Cache the rivet-cli BINARY keyed on its pinned version, NOT on Cargo.lock.
# The old key (hashFiles Cargo.lock) invalidated on every release version
# bump, forcing a full rebuild of rivet-cli's HiGHS C++ dependency — which
# filled a self-hosted runner's disk and red-failed the v0.14.0 release
# (No space left on device). Version-keying means a Cargo.lock change no
# longer triggers the rebuild; the cached binary is reused.
- name: Cache rivet-cli binary
uses: actions/cache@v6
with:
path: ~/.cargo/bin/rivet
key: ${{ runner.os }}-rivet-cli-v0.23.0
# PIN rivet to a release tag (was `--branch main`, unpinned). Unpinned, an
# upstream schema/behaviour bump silently reddened the gate on unchanged
# artifacts (rivet 0.15.0 promoted a WARN→ERROR, #229). v0.23.0 (adds configurable
# release-readiness ready-when/coverage, check verification-evidence, trace-results) is validated clean on this repo's
# artifacts before pinning — the exact CI gate below run locally under
# v0.23.0 gives non-xref ERROR 0, same as v0.22.0. Skip
# the (expensive) build entirely on a cache hit.
- name: Install rivet (pinned v0.23.0)
run: |
if ! rivet --version 2>/dev/null | grep -q "0.23.0"; then
cargo install --force --git https://github.com/pulseengine/rivet --tag v0.23.0 rivet-cli
fi
- name: Validate artifacts
run: |
sed -i '/^externals:/,$d' rivet.yaml
# Allow cross-repo link errors (kiln/gale/sigil haven't set up rivet yet)
# but fail on any non-cross-repo errors (schema, missing fields, broken local refs)
rivet validate 2>&1 | tee /tmp/rivet-output.txt
# Check if all errors are cross-repo links (contain ':' in target)
if grep -q "^ ERROR:" /tmp/rivet-output.txt; then
NON_XREF=$(grep "^ ERROR:" /tmp/rivet-output.txt | grep -v "targets '.*:.*' which does not exist" | grep -cv "missing '.*' link to" || true)
if [ "$NON_XREF" -gt 0 ]; then
echo "::error::Found $NON_XREF non-cross-repo validation errors"
exit 1
fi
echo "::warning::Cross-repo link errors present (expected — external projects need rivet init)"
fi
- name: Check coverage
run: rivet coverage
bazel:
name: Bazel Build & Proofs
# Stays on ubuntu-latest: needs Nix + Bazel + Rocq via Bazel
# (none provisioned on smithy; tracked in playbook out-of-scope
# table for both Bazel and Rocq).
runs-on: ubuntu-latest
timeout-minutes: 45
steps:
- uses: actions/checkout@v7
- name: Install Nix
uses: cachix/install-nix-action@v31
with:
nix_path: nixpkgs=channel:nixos-unstable
- name: Setup Bazel
uses: bazel-contrib/setup-bazel@0.19.0
with:
bazelisk-cache: true
disk-cache: ${{ github.workflow }}
repository-cache: true
- name: Build Rust via Bazel
run: bazel build //crates:synth
- name: Verify Rocq proofs
run: bazel test //coq:verify_proofs
- name: Run Renode emulation tests
run: bazel test //tests/renode/... --test_tag_filters=wast || [ $? -eq 4 ]
timeout-minutes: 10
cmp-select-oracle:
name: cmp-select two-move execution oracle
# VCR-ORACLE-001 (#242, #428): EXECUTE the cmp->select two-move arm under
# unicorn (faithful Thumb-2 IT-block predication) and diff flag-off vs flag-on
# vs wasmtime. This is the runtime validation gale's #428 measurement showed no
# real fixture provides (the two-move arm is reachable but runtime-dead on real
# code). Isolated job: unicorn/wasmtime are pip-installed here ONLY, so the main
# `cargo test --workspace` gate is NOT taxed with a C-library build graph.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run two-move execution oracle
run: python scripts/repro/cmp_select_two_move_differential.py
fact-spec-oracle:
name: fact-spec elision oracle (#494 phases 2 + 2b)
# 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). 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@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run in-bounds differential (proven bound)
run: python scripts/repro/fact_spec_clamp_494_differential.py
- name: Run wrong-bound loud-decline path
run: >
python scripts/repro/fact_spec_clamp_494_differential.py
--fact-lo 0 --fact-hi 4000 --expect-decline
# #494 phase 2b — divisor-nonzero: in-bounds div/rem differential
# (specialized ≡ wasmtime ≡ unspecialized over the proven divisor bound,
# incl. the RETAINED-i64-overflow-guard trap assertion), the
# Sat loud-decline byte-identity leg, and the RED force-admit divergence
# demonstration (the lever exists in debug builds only — CI's synth is
# a debug build).
- name: Run divisor-nonzero in-bounds differential (green)
run: python scripts/repro/fact_spec_div_494_differential.py
- name: Run divisor-including-zero loud-decline path
run: python scripts/repro/fact_spec_div_494_differential.py --expect-decline
- name: Run RED force-admit divergence demonstration
run: python scripts/repro/fact_spec_div_494_differential.py --force-admit
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@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run RV32 shift-fold execution oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/shift_fold_riscv_differential.py
rv32-const-addr-fold-oracle:
name: rv32 const-address-fold execution oracle
# VCR-ORACLE-001 (#242, #472 step 2): EXECUTE the RV32 const-address-fold lever
# under unicorn (UC_ARCH_RISCV) in BOTH flag states and diff the resulting
# linear MEMORY vs wasmtime. Ships flag-off (SYNTH_RV_ADDR_FOLD) awaiting the
# on-silicon flip, so this continuously validates the flag-on path (folding a
# constant address into the access immediate off s11) against regression.
# Isolated job: emulation deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run RV32 const-address-fold execution oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/const_addr_fold_riscv_differential.py
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@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run callee-saved preservation oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/callee_saved_490_differential.py
call-indirect-642-oracle:
name: call_indirect bounds-guard oracle (Thumb-2 + A32)
# VCR-ORACLE-001 (#242, #642): call_indirect emitted NO table bounds check
# and NO type check — an out-of-bounds index read past the table and BLXed
# whatever word lay there (uncontrolled indirect branch) where WASM Core
# §4.4.8 mandates a trap. EXECUTE the fixture under unicorn on BOTH ISAs
# (Thumb-2 cortex-m3 + A32 cortex-r5, table linked at r11) vs the wasmtime
# oracle: in-bounds indices must match; OOB indices must stop AT A UDF.
# Non-vacuous red: the words past the table are seeded with a valid decoy
# function, so an unguarded build "succeeds" at the OOB call and the
# harness fails loudly on the decoy's return value. The type check is
# discharged at compile time (closed-world table verification in the
# selector); its decline paths are unit-gated in synth-core/synth-synthesis.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run call_indirect bounds-guard oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/call_indirect_642_differential.py
call-indirect-650-multitable-oracle:
name: multi-table call_indirect oracle (Thumb-2 + A32)
# VCR-ORACLE-001 (#242, #650): tables are ONE contiguous region of 4-byte
# code pointers at R11 (table N at sum(size(0..N))*4, a compile-time
# constant -- tables are provably fixed-size, #642). EXECUTE a TWO-table
# fixture with OVERLAPPING indices and DISTINCT functions under unicorn on
# BOTH ISAs vs the wasmtime oracle: dispatch through both tables must
# match, OOB on EITHER table must stop at a UDF (bounds guard against THAT
# table's own size), and the aliasing canary (table0[1] != table1[1])
# catches a backend that drops the table index. On <= v0.33.1 this is red
# at compile: table-1 call_indirect loud-declined (capability upgrade --
# red = "declines today", green = correct dispatch). Single-table modules
# stay byte-identical by construction (offset 0 = the pre-#650 expansion),
# pinned by the frozen-fixture job and the #642/#594/#597 oracles.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run multi-table call_indirect oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/call_indirect_650_differential.py
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@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run block/br_if lowering oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/block_brif_483_differential.py
spill-frame-499-oracle:
name: optimized-path spill-frame teardown oracle
# #499: EXECUTE optimized-path functions whose register pressure fires the
# flag-off Const-eviction spill (`sub sp,#N` frame) under unicorn
# (UC_ARCH_ARM / Thumb) and diff linear MEMORY + SP balance vs wasmtime.
# Guards the #499 fix: the bridge appended fall-off-the-end returns WITHOUT
# the `add sp,#N` teardown, so post-#490 the `pop {…,pc}` epilogue read PC
# from a spill slot — a shipped crash on straight-line AND control-flow
# shapes. Compiles with SYNTH_BASE_CSE=0 (the #592 default relieves the
# pressure on these fixtures; the teardown path must stay covered) and
# trips loudly if a fixture stops spilling (vacuity guard). Isolated job:
# emulation deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run spill-frame teardown oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/spill_frame_499_differential.py
r12-spill-496-oracle:
name: optimized-path register-exhaustion oracle
# VCR-ORACLE-001 (#242, #496): EXECUTE the two silicon fixtures
# (control_step, flight_seam_flat) compiled via the DEFAULT optimized path
# (no --relocatable) under unicorn (UC_ARCH_ARM / Thumb) and diff the result
# vs wasmtime. Guards the #496 fix: the optimized path used to borrow R12/IP
# as last-resort scratch when its R4-R8 pool was exhausted, but R12 is the
# encoder's indexed-load base scratch (#212), so under real register pressure
# the value collided — control_step execution-faulted (READ_UNMAPPED from
# `add ip,ip,ip` = 2×base) and flight_seam_flat produced wrong values. The fix
# flags exhaustion and DECLINES the function to the direct selector (which
# spills). The frozen byte gate only covers the --relocatable direct path, so
# nothing else exercises the default self-contained-image path's register
# pressure. Isolated job: emulation deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run register-exhaustion oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/r12_spill_496_differential.py
flight-seam-570-oracle:
name: flight-seam relocatable-path execution oracle
# VCR-ORACLE-001 (#242, #212/#215, #570): EXECUTE the two flight_seam silicon
# fixtures (inlined w/ internal `bl filter_step`, and flat fully-dissolved)
# compiled via the SHIPPED direct path (--relocatable) under unicorn
# (UC_ARCH_ARM / Thumb) and diff flight_algo's result vs wasmtime (anchor
# 0x07FDF307). Guards the #212 R12-scratch reservation and #215 exposure on
# the relocatable path. Previously a dev-only script: it drifted silently
# when the #394 name work changed symbol naming (#570) — CI-gating it here
# so harness drift reddens instead of rotting. Symbols come from the ELF
# symtab, not `synth disasm` text (host-dependent, PR #489). Isolated job:
# emulation deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools capstone
- name: Run flight-seam oracle (inlined #212 + flat #215)
run: |
./target/debug/synth compile scripts/repro/flight_seam.wasm \
-o /tmp/fs.elf --target cortex-m4 --all-exports --relocatable
python scripts/repro/flight_seam_differential.py /tmp/fs.elf
./target/debug/synth compile scripts/repro/flight_seam_flat.wasm \
-o /tmp/fsf.elf --target cortex-m4 --all-exports --relocatable
python scripts/repro/flight_seam_differential.py /tmp/fsf.elf \
scripts/repro/flight_seam_flat.wasm
control-step-584-oracle:
name: control-step relocatable-path execution oracle
# VCR-ORACLE-001 (#242, #209, #584): EXECUTE the control_step silicon fixture
# (4x unsigned constant div_u — the reciprocal-multiply cost-gate repro)
# compiled via the SHIPPED direct path (--relocatable) under unicorn
# (UC_ARCH_ARM / Thumb) and diff control_step_decide's result vs wasmtime
# (anchor 0x00210A55, 13 vectors). Previously a dev-only script: its `synth
# disasm` text parse drifted into a KeyError on current main (#584, same
# class as #570/#489) — symbols now come from the ELF symtab, and CI-gating
# it here (flight-seam-570-oracle pattern) so harness drift reddens instead
# of rotting. The r12_spill_496 oracle covers control_step on the DEFAULT
# optimized path; this covers the --relocatable direct path. Isolated job:
# emulation deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run control-step oracle
run: |
./target/debug/synth compile scripts/repro/control_step.wasm \
-o /tmp/cs.elf --target cortex-m4 --all-exports --relocatable
python scripts/repro/control_step_differential.py /tmp/cs.elf
stack-args-503-oracle:
name: AAPCS stack-argument path oracle
# VCR-ORACLE-001 (#242, #503): EXECUTE functions that need the AAPCS
# stack-argument path with >8 scalar i32 params/args under unicorn
# (UC_ARCH_ARM / Thumb), via the SHIPPED direct path (--relocatable, what
# falcon uses), and diff the result vs wasmtime. Guards the #503 fix: the arm
# backend used to SKIP (emit no code for) any function with >8 scalar params
# or a call passing >8 args — 3 reachable falcon helpers were dropped. The fix
# lifts the conservative caps over the already-generic incoming_params /
# emit_stack_args machinery, leaning on the existing 12-bit [sp,#imm] guards.
# Covers a HIGH param count (sum25, reading param 24) and an outgoing 10-arg
# call. The 64-bit stack-param case stays refused (a #503 follow-up). Isolated
# job: emulation deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools capstone
- name: Run AAPCS stack-argument oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/stack_args_503_differential.py
i64-completeness-503-587-oracle:
name: i64 stack-param + spill-pool-grow oracle
# VCR-ORACLE-001 (#242, #503-i64, #587): EXECUTE the two previously
# loud-skipped direct-selector i64 classes under unicorn and diff vs
# wasmtime, on BOTH paths (--relocatable = falcon's, and the default):
# * #503-i64 — 64-bit params AAPCS-passed on the STACK (past R3 /
# even-align-spilled), incl. the narrow-after-wide shape that was
# silently MIScompiled (p3 of `(i64 i32 i32 i32)` read from R3 = p2),
# a write-back shape, and a has-call shape. Falcon func_58/func_163.
# * #587 — an i64-dense function whose ~16 concurrent pair spills
# exhausted the fixed 8-slot pool; the pool-grow recovery retry (last
# resort, after the #474 promotion-off fallback) sizes the pool from
# the operand-stack-depth bound. Falcon func_60/func_73.
# Isolated job: emulation deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run i64 stack-param oracle (#503-i64)
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/i64_stack_param_503_differential.py
- name: Run i64 spill-pool-grow oracle (#587)
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/i64_spill_pool_587_differential.py
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@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run i64 rot/div/rem expansion oracle (#610)
run: python scripts/repro/i64_rot_div_610_differential.py target/debug/synth
br-table-507-oracle:
name: optimized-path br_table oracle
# VCR-ORACLE-001 (#242, #507): EXECUTE br_table dispatch compiled via the
# DEFAULT optimized path (no --relocatable) under unicorn (UC_ARCH_ARM /
# Thumb) and diff the resulting linear memory vs wasmtime across every
# selector (incl. out-of-range → default arm) and two table shapes. Guards
# the #507 fix: the optimized path DROPPED the br_table dispatch during
# wasm→IR, emitting the arm bodies in fall-through with no selector compare —
# a silent miscompile (every input hit the last arm). The fix detects
# br_table on the raw wasm op stream and forces the direct selector (which
# lowers it as a cmp-chain). The frozen byte gate only covers the
# --relocatable direct path, so nothing else exercises the default path's
# br_table lowering. Isolated job: emulation deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run br_table oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/br_table_507_differential.py
const-cse-242-oracle:
name: const-CSE flag-on execution oracle
# VCR-RA const-CSE (#242): EXECUTE the optimized path compiled with
# SYNTH_CONST_CSE=1 under unicorn (UC_ARCH_ARM / Thumb) and diff the returned
# value vs wasmtime across redundant-const shapes (large/small/negative/mixed
# consts, reuse ACROSS an if/else where the cache must reset, and a
# 12-live-local function that forces real spills). The const cache aliases a
# repeated const to the register already holding it; this proves the aliasing
# is semantics-preserving on the flag-ON path. The flag ships DEFAULT-OFF
# (off ⇒ byte-identical, pinned by const_cse_reduction_242.rs's golden), so
# nothing else exercises the optimized-path const cache. Isolated job:
# emulation deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run const-CSE flag-on oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/const_cse_differential.py
frame-slot-dce-242-oracle:
name: frame-slot DCE default+optout execution oracle
# VCR-RA frame-slot DCE (#242): EXECUTE flat_flight (stack-reload forwarding +
# dead-frame-store elimination, DEFAULT-ON since the #242 feature-loop flip)
# under unicorn (UC_ARCH_ARM / Thumb) and diff flight_algo's return value vs
# wasmtime across several sensor inputs, in BOTH the shipped default AND the
# SYNTH_NO_STACK_FWD=1 opt-out (a default flip is only safe if the shipped path
# AND its rollback both match), with linear memory seeded exactly as wasmtime's.
# Also asserts the two configs emit DIFFERENT bytes (the flip is engaged). The
# paired passes turn frame reloads into register moves and remove the now-dead
# stores (flight_algo sp-traffic 20→7, 139→135 insns). Isolated job: emulation
# deps pip-installed here ONLY.
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
- uses: dtolnay/rust-toolchain@stable
- name: Cache Cargo dependencies
uses: actions/cache@v6
with:
path: |
~/.cargo/registry
~/.cargo/git
target/
key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
restore-keys: |
${{ runner.os }}-cargo-
- name: Build synth
run: cargo build -p synth-cli
- uses: actions/setup-python@v6
with:
python-version: "3.x"
- name: Install emulation deps
run: pip install wasmtime unicorn pyelftools
- name: Run frame-slot DCE flag-on oracle
env:
SYNTH: ./target/debug/synth
run: python scripts/repro/frame_slot_dce_differential.py