diff --git a/CHANGELOG.md b/CHANGELOG.md index f63e5e56..2e88975e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,19 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +## [0.47.0] - 2026-07-17 + +**"Close the loops" — every v0.46 loud-decline converted to a proven capability +(or an honestly sharper decline), driven by real-module needs.** WCET bounds +statically-proven loops and sound-checks untrusted hints (the scry seam); aarch64 +gains SOUND trapping float→int + IEEE-754-2019 min/max (35→46 ops, all 32 trap +cases execution-verified); the #275 finale ships self-contained `call_indirect` +(falcon unblocked, #275 CLOSED); the addressing validator extends to spans, the +self-contained ROM image, and RV32; the WasmCert anchor grows 489→536 Qed; and +`cabi-arena-realloc` binds natively on self-contained dissolves (**#418 remains +open** for the real dissolved fixture). The #791 soundness fix shipped same-day +as v0.46.1. + ### Added - **Self-contained `--cortex-m` `call_indirect` — the #275 finale (falcon's @@ -28,13 +41,6 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 `select_default` demo path. `--relocatable` output is byte-identical; self-contained modules without `call_indirect` are byte-identical. -### Found (tracked separately) - -- **#791: the optimized path miscompiles const-only-body functions** (result - materialized in r4, never moved to R0) — surfaced by the first execution - gate that runs dispatch targets in a default self-contained image; present - on main independent of this change (`--no-optimize` is correct). - - **WCET phase 2 — statically-proven loop bounds + the `--wcet-hints` seam (#778).** `--emit-wcet` now BOUNDS canonical const-bound counted loops instead of declining them: a conservative symbolic walk over the final @@ -66,6 +72,88 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 additionally executed under unicorn at authoring time (result correct, executed machine instructions ≤ bound). +- **aarch64 milestone 4 — sound trapping float→int + IEEE-754-2019 min/max + + copysign (#538, 35 → 46 ops).** `i32.trunc_f32/f64_s/u` lower behind a + two-sided WASM §4.3.3 domain guard (exact boundary constants, ordered + `fcmp`+`b.cond` skipping a `brk #0` only on the proven-in-range path — NaN + fails every ordered condition → trap) with `FCVTZS/FCVTZU` only where + saturate ≡ trunc; `f32/f64.min/max` use single `FMIN/FMAX` (IEEE 754-2019 + minimum/maximum = exactly WASM NaN-propagation + −0<+0, verified vs wasmtime + — `FMINNM/FMAXNM` would be the wrong minNum semantics); `copysign` via GP-file + bit surgery; `f32.sqrt` un-dropped at decode (now reachable on aarch64 AND + ARM32). Gate: 167-case boundary differential, **all 32 trap cases + execution-verified** (unicorn brk-exception + native SIGTRAP). Two latent + bugs found and fixed: an m3 `mov_imm64` halfword-shift bug (constants with + all-zero low halfwords materialized wrong) and the ARM32 `F32Min/F32Max` + pseudo-op (NaN/±0-wrong, previously dead code) now loud-declines until the + VMINNM twin lands. **Still declines (loud, gate-pinned):** f32/f64 rounding + ops (ceil/floor/trunc/nearest), i64↔float conversions, div/rem, popcnt — + the m2 decline oracle and #554 loudskip test were moved to these. + +- **VCR-VER-003 phase 2 — addressing validation for spans, the self-contained + ROM image, and RV32 (#777).** The per-compilation static-data addressing + validator now checks the FULL access span (a reloc whose access crosses a + segment's runtime-owned range no longer validates on byte 0 alone), the + self-contained `--cortex-m` packed ROM image (the #758 layout), and the RV32 + static-data path. Unconditional as in phase 1 (` + validate_reloc_resolutions_spanned`, hard compile error on mismatch); + red-first gated per class (e2e gate grew 1 → 6 tests). The RV32 probe found + **#798** (active data segments silently dropped on RV32 — interim warning + landed; the ship-or-hard-decline fix is tracked there). + +- **WasmCert-Coq anchor phase 2 — 489 → 536 Qed (+47) and a concrete real-dep + path (VCR-WASM-001, epic #242).** 19 i32 ops (arithmetic, bitwise, shifts, + eqz, full compare family) transcribed with line-level provenance pinned to + the nix-built coq9.0-wasm-2.2.0 sources; 49 real Qed / 0 Admitted in the + bridge (genuine discharges — mod-arithmetic, bit-level testbit facts, + shift-count normalization collapse, the gt/le/ge orientation gap). + Feasibility verdict sharpened from "no-go": `coqPackages.wasmcert` exists in + the exact pinned nixpkgs and **nix-builds green**; three named bazel blockers + documented in the roadmap, including a **license policy point — CompCert 3.16 + is unfree** (deliberately NOT taken into CI); upstream wasmcert ≥ 2.2.1 drops + the CompCert dep, so the real dep lands with the ruleset hook + the next + nixpkgs bump. + +- **`cabi-arena-realloc` binds natively on self-contained dissolves (#418 — + remains open for the real fixture).** When the wit-bindgen + `cabi-realloc-extern` arena import is the module's ONLY import, synth removes + it and prepends a defined wasm allocator (an index-preserving wasm→wasm + rewrite compiled through the ordinary pipeline — no hand-written machine + code, every existing validator applies), so the dissolve produces a real + self-contained image instead of degrading to a link-me ET_REL object. + Red-first execution differential: the image's own startup + each export vs + wasmtime with a host arena at a deliberately different base + (pointer-independent observables; exhaustion traps on both sides). + **Decline matrix (test-asserted):** `--relocatable` keeps the #420 + undefined-symbol seam; modules with OTHER imports keep the host seam entirely + (never a half-bound hybrid); `--native-pointer-abi` declines (SP-promotion + hazard with the cursor global); wrong signature / no memory / non-const data + offsets / zero arena room refuse loudly; pinned opt-out + `--no-bind-cabi-arena`. #418 stays open on the maintainer ask for the real + dissolved `.wasm` as a pinned fixture. + +### Found (tracked separately) + +- **#791: the optimized path miscompiled const-only-body functions** (result + materialized in r4, never moved to R0) — surfaced by the first execution + gate that runs dispatch targets in a default self-contained image. Fixed + same-day; shipped as the **v0.46.1** backport (see below). +- **#798: RV32 active data segments silently dropped** — found by the + VCR-VER-003 phase-2 RV32 probe; interim warning landed, ship-or-decline fix + tracked on #798. + +## [0.46.1] - 2026-07-17 + +**Soundness backport — #791.** The optimized (default) path miscompiled functions +whose body is a bare constant: `Opcode::Const` was the one value-producing arm +that never recorded its dest as `last_result_vreg`, so the epilogue never moved +the result to R0 and the export returned caller residue. Found by the #275 +finale's execution differential (the first gate to run dispatch targets in a +default self-contained image). Tagged from v0.46.0 + the cherry-picked fix +(pure patch); also on main. Red-first `const_body_791_differential.py`; frozen +anchors unchanged; `base_cse_flip_468` goldens re-pinned (+2 B harmless +`mov r0,rX` on void stored-const tails) after a full differential sweep. + ## [0.46.0] - 2026-07-16 **Qualification depth + capability breadth.** The sequel to the #757 arc: synth's diff --git a/Cargo.lock b/Cargo.lock index 605d3e88..0e562ff1 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1100,14 +1100,14 @@ dependencies = [ [[package]] name = "synth-abi" -version = "0.46.0" +version = "0.47.0" dependencies = [ "synth-wit", ] [[package]] name = "synth-analysis" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "synth-core", @@ -1116,7 +1116,7 @@ dependencies = [ [[package]] name = "synth-backend" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "synth-core", @@ -1127,7 +1127,7 @@ dependencies = [ [[package]] name = "synth-backend-aarch64" -version = "0.46.0" +version = "0.47.0" dependencies = [ "synth-core", "thiserror", @@ -1136,7 +1136,7 @@ dependencies = [ [[package]] name = "synth-backend-awsm" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "synth-core", @@ -1145,7 +1145,7 @@ dependencies = [ [[package]] name = "synth-backend-riscv" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "proptest", @@ -1157,7 +1157,7 @@ dependencies = [ [[package]] name = "synth-backend-wasker" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "synth-core", @@ -1166,11 +1166,11 @@ dependencies = [ [[package]] name = "synth-cfg" -version = "0.46.0" +version = "0.47.0" [[package]] name = "synth-cli" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "clap", @@ -1197,7 +1197,7 @@ dependencies = [ [[package]] name = "synth-core" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "gimli", @@ -1212,7 +1212,7 @@ dependencies = [ [[package]] name = "synth-frontend" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "synth-core", @@ -1226,14 +1226,14 @@ dependencies = [ [[package]] name = "synth-memory" -version = "0.46.0" +version = "0.47.0" dependencies = [ "bitflags", ] [[package]] name = "synth-opt" -version = "0.46.0" +version = "0.47.0" dependencies = [ "criterion", "synth-cfg", @@ -1241,11 +1241,11 @@ dependencies = [ [[package]] name = "synth-qemu" -version = "0.46.0" +version = "0.47.0" [[package]] name = "synth-synthesis" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "proptest", @@ -1260,7 +1260,7 @@ dependencies = [ [[package]] name = "synth-test" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "clap", @@ -1276,7 +1276,7 @@ dependencies = [ [[package]] name = "synth-verify" -version = "0.46.0" +version = "0.47.0" dependencies = [ "anyhow", "chrono", @@ -1295,7 +1295,7 @@ dependencies = [ [[package]] name = "synth-wit" -version = "0.46.0" +version = "0.47.0" [[package]] name = "tempfile" diff --git a/Cargo.toml b/Cargo.toml index d8ab2dfa..256c635d 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.46.0" +version = "0.47.0" edition = "2024" rust-version = "1.88" authors = ["PulseEngine Team"] diff --git a/MODULE.bazel b/MODULE.bazel index 4c6bdcb9..06958600 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.46.0", + version = "0.47.0", ) # Bazel dependencies diff --git a/crates/synth-backend-aarch64/Cargo.toml b/crates/synth-backend-aarch64/Cargo.toml index b9f5d46b..5b6e52f8 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.46.0" } +synth-core = { path = "../synth-core", version = "0.47.0" } thiserror.workspace = true tracing.workspace = true diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml index 0e22ef70..1beb7db0 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.46.0" } +synth-core = { path = "../synth-core", version = "0.47.0" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml index 901c61b3..da0dc543 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.46.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.46.0" } +synth-core = { path = "../synth-core", version = "0.47.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.47.0" } anyhow.workspace = true thiserror.workspace = true tracing.workspace = true diff --git a/crates/synth-backend-wasker/Cargo.toml b/crates/synth-backend-wasker/Cargo.toml index c8fb2109..424c579a 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.46.0" } +synth-core = { path = "../synth-core", version = "0.47.0" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml index c747efa3..a6f01911 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.46.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.46.0", optional = true } +synth-core = { path = "../synth-core", version = "0.47.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.47.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.46.0", features = ["arm"] } +synth-verify = { path = "../synth-verify", version = "0.47.0", features = ["arm"] } diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index 721d0a5a..245dfc72 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.46.0" } -synth-frontend = { path = "../synth-frontend", version = "0.46.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.46.0" } -synth-backend = { path = "../synth-backend", version = "0.46.0" } +synth-core = { path = "../synth-core", version = "0.47.0" } +synth-frontend = { path = "../synth-frontend", version = "0.47.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.47.0" } +synth-backend = { path = "../synth-backend", version = "0.47.0" } # AArch64 host-native backend (#538) — small pure-Rust crate, always on. -synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.46.0" } +synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.47.0" } # Optional external backends -synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.46.0", optional = true } -synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.46.0", optional = true } -synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.46.0", optional = true } +synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.47.0", optional = true } +synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.47.0", optional = true } +synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.47.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.46.0", optional = true, features = ["arm"] } +synth-verify = { path = "../synth-verify", version = "0.47.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 66578da9..132a56b7 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.46.0" } +synth-core = { path = "../synth-core", version = "0.47.0" } wasmparser.workspace = true wasm-encoder.workspace = true diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml index 15c899a4..3b69a459 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.46.0" } +synth-cfg = { path = "../synth-cfg", version = "0.47.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 a465f3b7..997f0a17 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.46.0" } -synth-cfg = { path = "../synth-cfg", version = "0.46.0" } -synth-opt = { path = "../synth-opt", version = "0.46.0" } +synth-core = { path = "../synth-core", version = "0.47.0" } +synth-cfg = { path = "../synth-cfg", version = "0.47.0" } +synth-opt = { path = "../synth-opt", version = "0.47.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 0c1af32c..df947078 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.46.0" } -synth-cfg = { path = "../synth-cfg", version = "0.46.0" } -synth-opt = { path = "../synth-opt", version = "0.46.0" } +synth-core = { path = "../synth-core", version = "0.47.0" } +synth-cfg = { path = "../synth-cfg", version = "0.47.0" } +synth-opt = { path = "../synth-opt", version = "0.47.0" } # ARM synthesis (optional, behind 'arm' feature) -synth-synthesis = { path = "../synth-synthesis", version = "0.46.0", optional = true } +synth-synthesis = { path = "../synth-synthesis", version = "0.47.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/npm/package.json b/npm/package.json index df363672..a943e005 100644 --- a/npm/package.json +++ b/npm/package.json @@ -1,6 +1,6 @@ { "name": "@pulseengine/synth", - "version": "0.46.0", + "version": "0.47.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"