fix(decoder): float-typed global accesses loud-skip — the last silent float path (GI-FPU-001, #369) #1139

Workflow file for this run

	name: CI

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

	env:
	CARGO_TERM_COLOR: always

	jobs:
	test:
	name: Test
	# NOTE: stays on ubuntu-latest for now. It originally moved here from
	# [self-hosted, linux, x64, rust-cpu] because z3-sys's C++ build exhausted
	# the smithy runners' temp disk — that pressure is gone (#553: synth-verify
	# defaults to the pure-Rust ordeal engine, z3 is behind the off-by-default
	# `z3-solver` feature), so moving back is a possible follow-up.
	runs-on: ubuntu-latest
	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

	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

Navigation Menu

Uh oh!

fix(decoder): float-typed global accesses loud-skip — the last silent float path (GI-FPU-001, #369) #1139

Workflow file

fix(decoder): float-typed global accesses loud-skip — the last silent float path (GI-FPU-001, #369) #1139

Uh oh!

Workflow file for this run