From 62ccaefc4a357c88c2fff5af603554a5287ca6e1 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 13:04:24 +0200 Subject: [PATCH 1/2] =?UTF-8?q?chore(release):=20v0.54.0=20=E2=80=94=20"Cl?= =?UTF-8?q?ose=20what=20we=20measured"=20(6=20lanes)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Version sweep: workspace + all intra-workspace path-dep pins + MODULE.bazel + npm + status.json; Cargo.lock refreshed to 0.54.0 (no CI job builds --locked, so this stays a release-process gate rather than a CI one). Docs regenerated once at assembly per #805. claim_check 37/37 · check_version_pins OK · oracle-wiring gate clean · frozen anchors 10/10 · build 0 · fmt 0 · aarch64_selector_ops 184. CHANGELOG headline added by the coordinator over the 10 lane-written entries. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CHANGELOG.md | 53 +++++++++++++++++++++++++ Cargo.lock | 36 ++++++++--------- Cargo.toml | 2 +- MODULE.bazel | 2 +- artifacts/status.json | 2 +- crates/synth-backend-aarch64/Cargo.toml | 2 +- crates/synth-backend-awsm/Cargo.toml | 2 +- crates/synth-backend-riscv/Cargo.toml | 6 +-- crates/synth-backend-wasker/Cargo.toml | 2 +- crates/synth-backend/Cargo.toml | 6 +-- crates/synth-cli/Cargo.toml | 18 ++++----- crates/synth-frontend/Cargo.toml | 2 +- crates/synth-opt/Cargo.toml | 2 +- crates/synth-synthesis/Cargo.toml | 6 +-- crates/synth-verify/Cargo.toml | 8 ++-- docs/status/FEATURE_MATRIX.md | 2 +- npm/package.json | 2 +- 17 files changed, 103 insertions(+), 50 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3ca9aa85..291317a9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,59 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +## [0.54.0] - 2026-08-05 + +**"Close what we measured."** v0.53 built the instruments; this release acts on +what they said. Every lane targeted a gap a v0.53 gate named *mechanically* — +not one someone guessed at — which inverts the usual order and is only possible +because the measurement landed first. + +- **aarch64 is no longer a subset with a hand-written excuse list.** The scalar + float surface is COMPLETE (rounding via `FRINT{P,M,Z,N}`, FP memory, i64↔float + converts, and domain-guarded trapping i64-target truncations), and the two + largest structural declines are gone: `call_indirect` with all three WASM + §4.4.8 trap guards emitted inline, and WASM globals. The selector goes + **161 → 184 ops**; gale's acceptance matrix goes **45 → 61 ops / 119 → 355 + native checks with an empty declined frontier**. Every op closed was picked + off the VCR-SEL-005 third-backend oracle's own complement, and each flipped + its `Err(reason)` ledger entry to `Ok(())` in the same commit that made it + lower — a gap claim must not outlive the gap. +- **The allocator reaches across calls (#242).** VCR-DEC-001 increment 3 takes + 57 of the 68 `call` declines; measured delta doubles to **−100 B relocatable / + −120 B self-contained, 0 WCET-bound regressions**. Still flag-off: the honest + read is that reach improved and the flip criterion is not met. +- **VCR-VER-004 — a validator that fails *differently*.** v0.53 found that a + wrong-return-register rewrite was accepted by BOTH existing per-compilation + validators, caught only by execution. Both are backward liveness analyses + whose obligation set is a variable — and ∅ is a fixpoint, so an emptied seed + is vacuously green. The new check is FORWARD and value-level: exactly one + obligation per return site, so there is no seed to shrink. The v0.53 mutation + is now caught **statically**, with zero false rejections on the corpus. + +### The pattern this release kept finding + +Nine of the defects fixed here were in **checkers, not in the code they check**: +a differential that printed `MISMATCH <-- BUG` and exited 0; the oracle-wiring +gate's own CI step passing while the gate failed; three `set -o pipefail` steps +without `-e`, where the step's status is its *last* command's; two test files +that located the `synth` binary by walking up from `current_exe()`, which held +`Code Coverage` RED repo-wide while the required `Test` job — same assertions, +different target-dir layout — stayed green; and, at fan-in, an aarch64 decline +oracle whose two sides were stale in OPPOSITE directions, each lane correctly +updating the honesty ledger for its own work and being wrong about the other's. + +That last one is worth stating plainly: the error existed in **neither parent** +and was created by the merge. Resolving it meant re-deriving what actually ships +rather than choosing a side — and the oracle then confirmed the result, which is +the only reason to trust it. + +**#890 remains the load-bearing open item.** The oracle-wiring gate took the +repo from **70 undeclared scripts to 0** (145 wired / 7 manual with reasons), +and it is enforced inside an already-required check so it cannot sit red +unnoticed. But the count it fixed had *risen* over the preceding releases while +individual instances were being fixed — the reminder that a bug factory is not +addressed by fixing its output. + ### Added - **aarch64 `call_indirect` and WASM globals — the two largest remaining diff --git a/Cargo.lock b/Cargo.lock index 2c1f2f86..76b17313 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1111,14 +1111,14 @@ dependencies = [ [[package]] name = "synth-abi" -version = "0.53.0" +version = "0.54.0" dependencies = [ "synth-wit", ] [[package]] name = "synth-analysis" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "synth-core", @@ -1127,7 +1127,7 @@ dependencies = [ [[package]] name = "synth-backend" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "synth-core", @@ -1138,7 +1138,7 @@ dependencies = [ [[package]] name = "synth-backend-aarch64" -version = "0.53.0" +version = "0.54.0" dependencies = [ "synth-core", "thiserror", @@ -1147,7 +1147,7 @@ dependencies = [ [[package]] name = "synth-backend-awsm" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "synth-core", @@ -1156,7 +1156,7 @@ dependencies = [ [[package]] name = "synth-backend-riscv" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "proptest", @@ -1169,7 +1169,7 @@ dependencies = [ [[package]] name = "synth-backend-wasker" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "synth-core", @@ -1178,11 +1178,11 @@ dependencies = [ [[package]] name = "synth-cfg" -version = "0.53.0" +version = "0.54.0" [[package]] name = "synth-cli" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "clap", @@ -1209,7 +1209,7 @@ dependencies = [ [[package]] name = "synth-core" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "gimli", @@ -1224,7 +1224,7 @@ dependencies = [ [[package]] name = "synth-frontend" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "synth-core", @@ -1238,14 +1238,14 @@ dependencies = [ [[package]] name = "synth-memory" -version = "0.53.0" +version = "0.54.0" dependencies = [ "bitflags", ] [[package]] name = "synth-opt" -version = "0.53.0" +version = "0.54.0" dependencies = [ "criterion", "synth-cfg", @@ -1253,11 +1253,11 @@ dependencies = [ [[package]] name = "synth-qemu" -version = "0.53.0" +version = "0.54.0" [[package]] name = "synth-synthesis" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "proptest", @@ -1272,7 +1272,7 @@ dependencies = [ [[package]] name = "synth-test" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "clap", @@ -1288,7 +1288,7 @@ dependencies = [ [[package]] name = "synth-verify" -version = "0.53.0" +version = "0.54.0" dependencies = [ "anyhow", "chrono", @@ -1307,7 +1307,7 @@ dependencies = [ [[package]] name = "synth-wit" -version = "0.53.0" +version = "0.54.0" [[package]] name = "tempfile" diff --git a/Cargo.toml b/Cargo.toml index 6218c65a..e26e5ea1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -28,7 +28,7 @@ resolver = "2" # semver to publish, so the convention now catches up: workspace # version follows the release tag, bumped pre-tag in the release # checklist. See docs/release-process.md. -version = "0.53.0" +version = "0.54.0" edition = "2024" rust-version = "1.88" authors = ["PulseEngine Team"] diff --git a/MODULE.bazel b/MODULE.bazel index f2911017..295460db 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -7,7 +7,7 @@ module( name = "synth", # Kept in lockstep with [workspace.package] version in Cargo.toml. # Both are bumped pre-tag — see docs/release-process.md. - version = "0.53.0", + version = "0.54.0", ) # Bazel dependencies diff --git a/artifacts/status.json b/artifacts/status.json index e599645c..2ea55f37 100644 --- a/artifacts/status.json +++ b/artifacts/status.json @@ -21,7 +21,7 @@ "sel_dsl_rule_qed": 50, "sel_dsl_rules": 50, "sel_rules_simplified_basis": 50, - "version": "0.53.0", + "version": "0.54.0", "verus_spec_fns": 8, "wasmcert_bridge_qed": 104 } diff --git a/crates/synth-backend-aarch64/Cargo.toml b/crates/synth-backend-aarch64/Cargo.toml index 6f309da0..e5bfb746 100644 --- a/crates/synth-backend-aarch64/Cargo.toml +++ b/crates/synth-backend-aarch64/Cargo.toml @@ -11,6 +11,6 @@ categories.workspace = true description = "AArch64 (A64) host-native backend for synth — integer subset (milestone 1, #538)" [dependencies] -synth-core = { path = "../synth-core", version = "0.53.0" } +synth-core = { path = "../synth-core", version = "0.54.0" } thiserror.workspace = true tracing.workspace = true diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml index 6b3a4ec6..a89ff72a 100644 --- a/crates/synth-backend-awsm/Cargo.toml +++ b/crates/synth-backend-awsm/Cargo.toml @@ -11,6 +11,6 @@ categories.workspace = true description = "aWsm backend integration for the Synth compiler" [dependencies] -synth-core = { path = "../synth-core", version = "0.53.0" } +synth-core = { path = "../synth-core", version = "0.54.0" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml index 12dacbd8..30c3f51c 100644 --- a/crates/synth-backend-riscv/Cargo.toml +++ b/crates/synth-backend-riscv/Cargo.toml @@ -11,8 +11,8 @@ categories.workspace = true description = "RISC-V encoder, ELF builder, PMP allocator, and bare-metal startup for synth" [dependencies] -synth-core = { path = "../synth-core", version = "0.53.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.53.0" } +synth-core = { path = "../synth-core", version = "0.54.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.54.0" } anyhow.workspace = true thiserror.workspace = true tracing.workspace = true @@ -21,4 +21,4 @@ tracing.workspace = true proptest.workspace = true # VCR-SEL-005 (#851): the cross-backend op-parity oracle probes the AArch64 # selector as the THIRD backend (tests/cross_backend_op_parity.rs only). -synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.53.0" } +synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.54.0" } diff --git a/crates/synth-backend-wasker/Cargo.toml b/crates/synth-backend-wasker/Cargo.toml index e129e6bf..120212d7 100644 --- a/crates/synth-backend-wasker/Cargo.toml +++ b/crates/synth-backend-wasker/Cargo.toml @@ -11,6 +11,6 @@ categories.workspace = true description = "Wasker backend integration for the Synth compiler" [dependencies] -synth-core = { path = "../synth-core", version = "0.53.0" } +synth-core = { path = "../synth-core", version = "0.54.0" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml index b419a72a..104c7aab 100644 --- a/crates/synth-backend/Cargo.toml +++ b/crates/synth-backend/Cargo.toml @@ -15,8 +15,8 @@ default = ["arm-cortex-m"] arm-cortex-m = ["synth-synthesis"] [dependencies] -synth-core = { path = "../synth-core", version = "0.53.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.53.0", optional = true } +synth-core = { path = "../synth-core", version = "0.54.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.54.0", optional = true } anyhow.workspace = true thiserror.workspace = true @@ -24,4 +24,4 @@ thiserror.workspace = true # #667 move 2: the i64 pseudo-op expansion certification oracle # (tests/i64_expansion_certification.rs) feeds THIS crate's emitted encoder # bytes to the synth-verify expansion validator. Dev-only — no prod-dep edge. -synth-verify = { path = "../synth-verify", version = "0.53.0", features = ["arm"] } +synth-verify = { path = "../synth-verify", version = "0.54.0", features = ["arm"] } diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index 1f75187b..5a6cdd60 100644 --- a/crates/synth-cli/Cargo.toml +++ b/crates/synth-cli/Cargo.toml @@ -58,23 +58,23 @@ exports_only_275_probe = [] # Path deps carry `version` so `cargo publish` rewrites them to the # crates.io coordinate. Bumping the workspace version requires # updating these in lockstep — see docs/release-process.md. -synth-core = { path = "../synth-core", version = "0.53.0" } -synth-frontend = { path = "../synth-frontend", version = "0.53.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.53.0" } -synth-backend = { path = "../synth-backend", version = "0.53.0" } +synth-core = { path = "../synth-core", version = "0.54.0" } +synth-frontend = { path = "../synth-frontend", version = "0.54.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.54.0" } +synth-backend = { path = "../synth-backend", version = "0.54.0" } # AArch64 host-native backend (#538) — small pure-Rust crate, always on. -synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.53.0" } +synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.54.0" } # Optional external backends -synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.53.0", optional = true } -synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.53.0", optional = true } -synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.53.0", optional = true } +synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.54.0", optional = true } +synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.54.0", optional = true } +synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.54.0", optional = true } # Optional translation validation — pure-Rust ordeal engine by default (#553), # no C++ toolchain needed. For the Z3 differential oracle build with # `--features verify,synth-verify/z3-solver` (+ SYNTH_SOLVER_DIFF=1 at runtime). -synth-verify = { path = "../synth-verify", version = "0.53.0", optional = true, features = ["arm"] } +synth-verify = { path = "../synth-verify", version = "0.54.0", optional = true, features = ["arm"] } # Optional PulseEngine WASM optimizer # Uncomment when loom crate is available: diff --git a/crates/synth-frontend/Cargo.toml b/crates/synth-frontend/Cargo.toml index 82d85d35..0021366e 100644 --- a/crates/synth-frontend/Cargo.toml +++ b/crates/synth-frontend/Cargo.toml @@ -14,7 +14,7 @@ description = "WASM/WAT parser and module decoder frontend for the Synth compile # Internal path deps carry an explicit version so `cargo publish` # can rewrite to the crates.io coordinate. `path` is used for # in-workspace builds; `version` is what crates.io sees. -synth-core = { path = "../synth-core", version = "0.53.0" } +synth-core = { path = "../synth-core", version = "0.54.0" } wasmparser.workspace = true wasm-encoder.workspace = true diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml index cb66a9a1..c41c4b71 100644 --- a/crates/synth-opt/Cargo.toml +++ b/crates/synth-opt/Cargo.toml @@ -11,7 +11,7 @@ categories.workspace = true description = "Peephole optimization passes for the Synth compiler" [dependencies] -synth-cfg = { path = "../synth-cfg", version = "0.53.0" } +synth-cfg = { path = "../synth-cfg", version = "0.54.0" } [dev-dependencies] criterion = { version = "0.8", features = ["html_reports"] } diff --git a/crates/synth-synthesis/Cargo.toml b/crates/synth-synthesis/Cargo.toml index 0f945079..58ce659f 100644 --- a/crates/synth-synthesis/Cargo.toml +++ b/crates/synth-synthesis/Cargo.toml @@ -11,9 +11,9 @@ categories.workspace = true description = "WASM-to-ARM instruction selection and peephole optimizer" [dependencies] -synth-core = { path = "../synth-core", version = "0.53.0" } -synth-cfg = { path = "../synth-cfg", version = "0.53.0" } -synth-opt = { path = "../synth-opt", version = "0.53.0" } +synth-core = { path = "../synth-core", version = "0.54.0" } +synth-cfg = { path = "../synth-cfg", version = "0.54.0" } +synth-opt = { path = "../synth-opt", version = "0.54.0" } serde.workspace = true anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml index 14ee2bda..ff390cf6 100644 --- a/crates/synth-verify/Cargo.toml +++ b/crates/synth-verify/Cargo.toml @@ -22,12 +22,12 @@ arm = ["synth-synthesis"] [dependencies] # Core dependencies (always required) -synth-core = { path = "../synth-core", version = "0.53.0" } -synth-cfg = { path = "../synth-cfg", version = "0.53.0" } -synth-opt = { path = "../synth-opt", version = "0.53.0" } +synth-core = { path = "../synth-core", version = "0.54.0" } +synth-cfg = { path = "../synth-cfg", version = "0.54.0" } +synth-opt = { path = "../synth-opt", version = "0.54.0" } # ARM synthesis (optional, behind 'arm' feature) -synth-synthesis = { path = "../synth-synthesis", version = "0.53.0", optional = true } +synth-synthesis = { path = "../synth-synthesis", version = "0.54.0", optional = true } # Default SMT engine: pure-Rust, certificate-checked QF_BV solver (#553). # 0.9 adds the `ordeal::trap` module (trap-preservation VCs, VCR-VER-002 / #166); diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index 08722232..4bd88c92 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -7,7 +7,7 @@ > stale. All numbers come from [`artifacts/status.json`](../../artifacts/status.json), > which is re-derived from source on every run — never hand-edited. -**Workspace version:** 0.53.0 +**Workspace version:** 0.54.0 --- diff --git a/npm/package.json b/npm/package.json index 9ad69538..8e8ccdc2 100644 --- a/npm/package.json +++ b/npm/package.json @@ -1,6 +1,6 @@ { "name": "@pulseengine/synth", - "version": "0.53.0", + "version": "0.54.0", "description": "synth — a WebAssembly-to-ARM/RISC-V/AArch64 compiler with mechanized correctness proofs. Produces bare-metal ELF binaries for embedded targets.", "bin": { "synth": "./run.js" From 692aaf5b8368a673b811ca62f3ba4681ecbb6788 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 13:40:51 +0200 Subject: [PATCH 2/2] =?UTF-8?q?fix(release):=20cold-review=20blockers=20?= =?UTF-8?q?=E2=80=94=20two=20shipped=20capabilities=20called=20"declined"?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit F1 (BLOCK) — the CHANGELOG carried a THIRD stale copy of the aarch64 decline list, naming `call_indirect` and globals as "still genuinely declined" when both SHIP in this release. Written by the float lane before the call_indirect/globals lane landed; the fan-in reconciled the decline ORACLE and the FEATURE_MATRIX row and missed the prose. Same defect as v0.51, in the document that becomes the frozen public record at tag time. F2 (BLOCK) — "f32 complete" was an overclaim CREATED BY THIS RELEASE. v0.54 makes `f32.{ceil,floor,trunc,nearest}` LOUD-DECLINE on ARM (the legacy pseudo-op round-tripped through a saturating VCVT, so ceil(1e30)/ceil(±inf)/ceil(NaN) were all wrong — the #709 more-total-than-WASM class), and three docs still claimed completeness: the f32 matrix row ("Complete op set"), the honest summary ("complete i32/i64/f32/f64"), and README's "the remaining float residual" (singular, when there are now five). Row is now P with the residual named. Verified on the release binary: f32.ceil declines on BOTH cortex-m4f and cortex-m7dp; f64.ceil lowers on m7dp (declines on m4f only for want of a double FPU, which is the pre-existing single-precision limit, not this change). F4 — the anti-vacuity gate had its OWN vacuity hole. `oracle_wiring_check.py` appended `run:` bodies verbatim, and YAML only eats `#` in a single-line plain scalar — so commenting out the body of a `run: |` step (nearly every oracle step here) left the script "referenced" and the gate GREEN while the step ran nothing. The earlier comment-demotion mutation passed only because it targeted a single-line `run:`. Now strips shell comments; proven red-first: commenting the gpio-thin invocation inside its block scalar reddens the gate with "only in a COMMENT — prose does not run an oracle". F3 — FEATURE_MATRIX stated #890's residual in its PRE-fix form ("57 of 130 not CI-wired and nothing distinguishes manual from forgotten"): both halves are now false. Restated as what is actually still open (the 7 `manual` scripts + the sweeps asserting exit status rather than per-script check counts). F5 — stale measured numbers from fan-in drift: VCR-VER-004's shipping-path audit is Holds 431 / NotAttempted 202 / Violated 0 over 633 (not 422/195/617) and the allocator histogram moved 174->175 / 11->17, because the corpus is `scripts/repro/*.{wat,wasm}` and GREW by 16 fixtures during this release's own fan-in. Corrected, and both sites now say the counts are a snapshot while `Violated 0` and the byte/cycle deltas are the durable claims. F6 — two more bare `set -o pipefail` steps (the VCR-VER-004 ones, landed after #900's sweep). Without `-e` the step's status is its LAST command's. Gates: build 0 · fmt 0 · cargo test --workspace 130 suites / exit 0 · claim_check 37/37 · oracle-wiring 0 · check_version_pins 0 · frozen 10/10. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 4 ++-- CHANGELOG.md | 28 ++++++++++++++++++------ README.md | 2 +- docs/status/FEATURE_MATRIX.md | 22 +++++++++++-------- scripts/oracle_wiring_check.py | 18 ++++++++++++++- scripts/templates/feature_matrix.md.tmpl | 22 +++++++++++-------- 6 files changed, 67 insertions(+), 29 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 457ddce0..b6069e16 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1078,7 +1078,7 @@ jobs: # emitting no verdicts) — see the script docstring. - name: Audit the SHIPPING allocator against the ABI contract (#242) run: | - set -o pipefail + set -euo pipefail SYNTH=./target/debug/synth python scripts/repro/vcr_ver_004_shipping_path_audit.py | tee vcr_ver_004_ship.out grep -q "^VCR-VER-004-SHIPPING .* VIOLATED=0 " vcr_ver_004_ship.out test "$(grep -c '^ Holds ' vcr_ver_004_ship.out)" -eq 1 @@ -1087,7 +1087,7 @@ jobs: # assertion would otherwise pass while gating nothing. - name: Re-run the v0.53 mutation against all three instruments (#242) run: | - set -o pipefail + set -euo pipefail python scripts/repro/vcr_ver_004_instrument_independence.py | tee vcr_ver_004.out grep -q "^VCR-VER-004-INDEPENDENCE ASSERTIONS=4/4$" vcr_ver_004.out test "$(grep -c '^OK ' vcr_ver_004.out)" -eq 5 diff --git a/CHANGELOG.md b/CHANGELOG.md index 291317a9..c77dba86 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -209,9 +209,14 @@ addressed by fixing its output. (renamed `call-indirect-pseudo` — the high-level `Call`/`CallIndirect` pseudo-ops are expanded downstream into a bounds guard + table load + result move, so the register footprint here is not the one that ships, and they stay - declined by name). The residual buckets are `unmodeled-op` 174, `single-block` - 73, `identity-colouring` 31, `unreachable-block` 11, `call-indirect-pseudo` 11, - `numeric-branch` 10. + declined by name). Measured at the release commit, the residual buckets are + `unmodeled-op` 175, `single-block` 73, `identity-colouring` 31, + `unreachable-block` 11, `call-indirect-pseudo` 17, `numeric-branch` 10. + (The corpus is `scripts/repro/*.{wat,wasm}` and therefore GROWS as lanes add + fixtures — it went 617 → 633 functions during this release's own fan-in, which + moved two of these buckets after the lane measured them. The durable claims + are the byte/cycle deltas and `Violated 0`; the absolute bucket counts are a + snapshot.) Still **flag-off by default** (`SYNTH_GRAPH_ALLOC`): this is a measurement spike, not a behaviour change. Frozen anchors byte-identical, 10/10. @@ -308,10 +313,19 @@ addressed by fixing its output. op; declining keeps it latent rather than shipping it. A real `VRINT.F32` lowering (the f32 twin of the shipping f64 path) is the follow-up. - The aarch64 decline-matrix oracle and the #554 float-honesty fixture were - repointed at constructs that are still genuinely declined (structural ones: - `call_indirect`, `br_table`, param writes, globals, bulk memory, - value-carrying blocks, SIMD), and the #554 assertion was strengthened to - require the diagnostic to come from the aarch64 SELECTOR and name its reason. + repointed at constructs that are still genuinely declined: `br_table`, writing + a PARAM local in a leaf function, `memory.copy`/`fill`, value-carrying blocks + and loops, v128/SIMD, multi-memory, `>8` args, float-result callees, import + calls — plus the six "rather than guess" refusals (imported global, global + with no decoded const initializer, non-leaf float param, growable imported + table, non-statically-verifiable element segment, table slot holding an + imported function). The #554 assertion was strengthened to require the + diagnostic to come from the aarch64 SELECTOR and to name its reason. + (An earlier draft of this sentence also listed `call_indirect` and globals — + both of which SHIP in this release, below. That draft was written by the float + lane before the call_indirect/globals lane landed; it was the third copy of a + list this release had to reconcile at fan-in, and the one the oracle and the + matrix row did not cover. Caught by cold review.) - **VCR-VER-004 — the ABI observable-contract validator: a per-compilation check that fails *differently*** (#242). diff --git a/README.md b/README.md index a4865620..695b46a3 100644 --- a/README.md +++ b/README.md @@ -36,7 +36,7 @@   -Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code, with additional backends for ARM Cortex-R5 (A32, `--target cortex-r5`), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), and AArch64 (host-native, `-b aarch64`). It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), scalar f32/f64 via VFP on FPU targets (f32 complete v0.41, f64 complete v0.43 — #369 closed; the falcon `--relocatable cortex-m7dp` VFP-exhaustion tail closed in v0.53 via register-file spilling, #881; the remaining float residual is `i64.trunc_sat_f32_*` declining on single-precision FPUs, which needs the f64 promote), control flow, and memory operations; any construct without a lowering declines loudly rather than miscompiling (the #369/#554 gate class). Mechanized correctness proofs in [Rocq](https://rocq-prover.org/) cover the i32 and i64 instruction selection with result-correspondence (T1) proofs; float/SIMD selection has existence-only (T2) proofs. +Synth is an ahead-of-time compiler from WebAssembly to ARM Cortex-M machine code, with additional backends for ARM Cortex-R5 (A32, `--target cortex-r5`), RISC-V RV32IMAC (qemu_riscv32 / ESP32-C3), and AArch64 (host-native, `-b aarch64`). It produces bare-metal ELF binaries targeting embedded microcontrollers. The compiler handles i32, i64 (via register pairs), scalar f32/f64 via VFP on FPU targets (f32 complete v0.41, f64 complete v0.43 — #369 closed; the falcon `--relocatable cortex-m7dp` VFP-exhaustion tail closed in v0.53 via register-file spilling, #881; the remaining float residuals are `f32.{ceil,floor,trunc,nearest}`, which loud-decline on every ARM target pending a real `VRINT.F32` lowering (v0.54 — the legacy pseudo-op was unsound via a saturating `VCVT`), and `i64.trunc_sat_f32_*` declining on single-precision FPUs, which needs the f64 promote), control flow, and memory operations; any construct without a lowering declines loudly rather than miscompiling (the #369/#554 gate class). Mechanized correctness proofs in [Rocq](https://rocq-prover.org/) cover the i32 and i64 instruction selection with result-correspondence (T1) proofs; float/SIMD selection has existence-only (T2) proofs. **This is pre-release software.** Generated code is validated by unit tests, Renode/QEMU emulation, execution differentials against wasmtime, and — for specific fixtures — cycle- and correctness-gated runs on real Cortex-M silicon (NUCLEO-G474RE, STM32F100, via the gale test loop). Broad hardware validation is still missing. Use at your own risk. diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index 4bd88c92..dd21747c 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -43,7 +43,7 @@ soundness feature, not an absence. |----------|--------|-------| | i32 arithmetic / bitwise / comparison / shift / rotate | Y | Full Rocq T1 proofs; Renode + silicon (gale) execution evidence | | i64 (register pairs) — arithmetic, shifts, rotates, div/rem, compare | Y | Pair lowering complete (#599, #610, #615); execution differentials vs wasmtime | -| f32 scalar via VFP | Y (FPU targets) | Complete op set incl. all six comparisons, NaN-aware (v0.41); requires an FPU target (e.g. `cortex-m4f`) | +| f32 scalar via VFP | P (FPU targets) | Arithmetic, all six comparisons, min/max/abs/neg/copysign, load/store and conversions — NaN-aware (v0.41); requires an FPU target (e.g. `cortex-m4f`). **Residual: `f32.{ceil,floor,trunc,nearest}` LOUD-DECLINE on every ARM target** (v0.54): the legacy pseudo-op round-tripped through a saturating `VCVT`, so `ceil(1e30)`, `ceil(±inf)` and `ceil(NaN)` were all wrong — the #709 more-total-than-WASM class. Declining keeps it latent rather than shipping it; a real `VRINT.F32` lowering (the f32 twin of the shipping f64 path) is the follow-up. The f64 rounding ops lower on a double-FPU target (`cortex-m7dp`). | | f64 scalar via VFP | Y (FPU targets) | Complete (v0.43, #369 closed); marshalling + AAPCS-VFP mixed params | | Trapping float→int truncations | Y | Domain-guarded (trap, not saturate) — the #709 soundness class | | Non-trapping `trunc_sat` (0xFC prefix) | Y (FPU targets) | Decoded and lowered as bare saturating VCVT (§4.3.2: NaN→0, out-of-range saturates, never traps). i32-target forms on any FPU target; i64-target forms on a double-FPU target (`cortex-m7dp`) via a branch-free FP word-decompose (v0.49, #782); aarch64 lowers all eight. Residual: i64-from-f32 declines on single-precision FPUs (needs the f64 promote). The falcon `--relocatable cortex-m7dp` D-register-pressure + RA tail closed in v0.53 via VFP register-file spilling (#881); #782 closed v0.49 | @@ -124,19 +124,23 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. ## Honest Summary -- The primary ARM Thumb-2 path is a complete i32/i64/f32/f64 compiler with +- The primary ARM Thumb-2 path is a complete i32/i64/f64 compiler — and f32 + complete except the four rounding ops, which loud-decline (see the f32 row) — with mechanized proofs on the integer selection and per-compilation validators (translation, trap-preservation, static-data addressing) on every build. - The other three backends are honest subsets: their gaps decline loudly and their coverage is listed above, not implied. - Broad hardware validation is still missing: silicon evidence is fixture-scoped (gale), emulation is Renode/QEMU/unicorn. -- Known open soundness/coverage residuals are tracked as issues (e.g. #890: - 57 of 130 differential oracles are not CI-wired and nothing distinguishes - "manual by design" from "forgotten" — an absent gate is invisible to a green - board; #851: the aarch64 op-surface gaps the VCR-SEL-005 third-backend oracle - now enumerates mechanically; #846: two `gpio-thin` CRL/CRH sites still need - relational ranges). +- Known open soundness/coverage residuals are tracked as issues (e.g. #890: the + oracle-wiring gate now leaves 0 undeclared and 0 unwired scripts, so a + forgotten gate is no longer indistinguishable from a deliberately manual one + — what remains open is the 7 `manual` scripts (external fixture, measurement + and scratch categories) and the fact that the newly-wired sweeps assert exit + status rather than a per-script non-zero check count; #851: the aarch64 + op-surface gaps the VCR-SEL-005 third-backend oracle now enumerates + mechanically; #846: two `gpio-thin` CRL/CRH sites still need relational + ranges). - Two residuals live in code comments rather than issues, and are restated here so they are not implied away: `validate_segment_rewrite` does NOT catch a recoloured `Pop {…, PC}` in the MIDDLE of a segment (pinned at the pass via @@ -156,7 +160,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. - What VCR-VER-004 does **not** close, stated plainly: - It is a **gate only on the flag-off** graph-colouring allocator. On the DEFAULT path it is a report-only audit held to a CI floor — measured - `Holds 422 / NotAttempted 195 / Violated 0` over 617 corpus functions, so it + `Holds 431 / NotAttempted 202 / Violated 0` over 633 corpus functions (the corpus is `scripts/repro/*.{wat,wasm}`, so it GROWS as lanes add fixtures — the invariant is `Violated 0`, not the absolute counts), so it proves the observable return contract on ~68 % of the shipping path — `bl`/`blx` calls included, via the shared AAPCS `liveness::call_effect` — and declines (never guesses) on the rest. Making it gate the default path means diff --git a/scripts/oracle_wiring_check.py b/scripts/oracle_wiring_check.py index 81862fbf..6ce07fd6 100644 --- a/scripts/oracle_wiring_check.py +++ b/scripts/oracle_wiring_check.py @@ -141,7 +141,23 @@ def executable_surface(workflows): if not isinstance(st, dict): continue if isinstance(st.get("run"), str): - chunks.append(st["run"]) + # Strip SHELL comments before counting a reference. + # + # The gate's whole point is that a mention must be something + # that RUNS. YAML eats `#` only in a single-line plain scalar; + # in a `run: |` block — which is nearly every oracle step here + # — the `#` survives into the script body, so commenting the + # body out left the script still "referenced" and the gate + # GREEN while the step executed nothing. Commenting out a + # flaky step is the most common way a gate goes inert, i.e. + # precisely the #890 failure this exists to reject. + # Found by the v0.54 cold review; the earlier + # comment-demotion mutation passed only because it happened + # to target a single-line `run:`. + for line in st["run"].splitlines(): + code = line.split("#", 1)[0] + if code.strip(): + chunks.append(code) for block in ("with", "env"): for v in (st.get(block) or {}).values(): chunks.append(str(v)) diff --git a/scripts/templates/feature_matrix.md.tmpl b/scripts/templates/feature_matrix.md.tmpl index 206fae7d..a7d99938 100644 --- a/scripts/templates/feature_matrix.md.tmpl +++ b/scripts/templates/feature_matrix.md.tmpl @@ -43,7 +43,7 @@ soundness feature, not an absence. |----------|--------|-------| | i32 arithmetic / bitwise / comparison / shift / rotate | Y | Full Rocq T1 proofs; Renode + silicon (gale) execution evidence | | i64 (register pairs) — arithmetic, shifts, rotates, div/rem, compare | Y | Pair lowering complete (#599, #610, #615); execution differentials vs wasmtime | -| f32 scalar via VFP | Y (FPU targets) | Complete op set incl. all six comparisons, NaN-aware (v0.41); requires an FPU target (e.g. `cortex-m4f`) | +| f32 scalar via VFP | P (FPU targets) | Arithmetic, all six comparisons, min/max/abs/neg/copysign, load/store and conversions — NaN-aware (v0.41); requires an FPU target (e.g. `cortex-m4f`). **Residual: `f32.{ceil,floor,trunc,nearest}` LOUD-DECLINE on every ARM target** (v0.54): the legacy pseudo-op round-tripped through a saturating `VCVT`, so `ceil(1e30)`, `ceil(±inf)` and `ceil(NaN)` were all wrong — the #709 more-total-than-WASM class. Declining keeps it latent rather than shipping it; a real `VRINT.F32` lowering (the f32 twin of the shipping f64 path) is the follow-up. The f64 rounding ops lower on a double-FPU target (`cortex-m7dp`). | | f64 scalar via VFP | Y (FPU targets) | Complete (v0.43, #369 closed); marshalling + AAPCS-VFP mixed params | | Trapping float→int truncations | Y | Domain-guarded (trap, not saturate) — the #709 soundness class | | Non-trapping `trunc_sat` (0xFC prefix) | Y (FPU targets) | Decoded and lowered as bare saturating VCVT (§4.3.2: NaN→0, out-of-range saturates, never traps). i32-target forms on any FPU target; i64-target forms on a double-FPU target (`cortex-m7dp`) via a branch-free FP word-decompose (v0.49, #782); aarch64 lowers all eight. Residual: i64-from-f32 declines on single-precision FPUs (needs the f64 promote). The falcon `--relocatable cortex-m7dp` D-register-pressure + RA tail closed in v0.53 via VFP register-file spilling (#881); #782 closed v0.49 | @@ -124,19 +124,23 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. ## Honest Summary -- The primary ARM Thumb-2 path is a complete i32/i64/f32/f64 compiler with +- The primary ARM Thumb-2 path is a complete i32/i64/f64 compiler — and f32 + complete except the four rounding ops, which loud-decline (see the f32 row) — with mechanized proofs on the integer selection and per-compilation validators (translation, trap-preservation, static-data addressing) on every build. - The other three backends are honest subsets: their gaps decline loudly and their coverage is listed above, not implied. - Broad hardware validation is still missing: silicon evidence is fixture-scoped (gale), emulation is Renode/QEMU/unicorn. -- Known open soundness/coverage residuals are tracked as issues (e.g. #890: - 57 of 130 differential oracles are not CI-wired and nothing distinguishes - "manual by design" from "forgotten" — an absent gate is invisible to a green - board; #851: the aarch64 op-surface gaps the VCR-SEL-005 third-backend oracle - now enumerates mechanically; #846: two `gpio-thin` CRL/CRH sites still need - relational ranges). +- Known open soundness/coverage residuals are tracked as issues (e.g. #890: the + oracle-wiring gate now leaves 0 undeclared and 0 unwired scripts, so a + forgotten gate is no longer indistinguishable from a deliberately manual one + — what remains open is the 7 `manual` scripts (external fixture, measurement + and scratch categories) and the fact that the newly-wired sweeps assert exit + status rather than a per-script non-zero check count; #851: the aarch64 + op-surface gaps the VCR-SEL-005 third-backend oracle now enumerates + mechanically; #846: two `gpio-thin` CRL/CRH sites still need relational + ranges). - Two residuals live in code comments rather than issues, and are restated here so they are not implied away: `validate_segment_rewrite` does NOT catch a recoloured `Pop {…, PC}` in the MIDDLE of a segment (pinned at the pass via @@ -156,7 +160,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. - What VCR-VER-004 does **not** close, stated plainly: - It is a **gate only on the flag-off** graph-colouring allocator. On the DEFAULT path it is a report-only audit held to a CI floor — measured - `Holds 422 / NotAttempted 195 / Violated 0` over 617 corpus functions, so it + `Holds 431 / NotAttempted 202 / Violated 0` over 633 corpus functions (the corpus is `scripts/repro/*.{wat,wasm}`, so it GROWS as lanes add fixtures — the invariant is `Violated 0`, not the absolute counts), so it proves the observable return contract on ~68 % of the shipping path — `bl`/`blx` calls included, via the shared AAPCS `liveness::call_effect` — and declines (never guesses) on the rest. Making it gate the default path means