diff --git a/CHANGELOG.md b/CHANGELOG.md index 17e5b86..c4df217 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,60 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +## [0.36.0] - 2026-07-08 + +**`unreachable` finally traps (it was decode-dropped as an "intentional no-op" +on every backend — WASM §4.4.5); RV32 rem_s stops over-trapping; sparse +funcref tables dispatch with null-slot traps (falcon complete); the verified +selector DSL reaches 40 rules and the Sail/ASL bridge reaches 81 Qed — +catching two latent bugs in our own hand-written model.** + +### Changed + +- **Post-exhaustion code quality (PR #672, #242 — the VCR-VER-001-named + capability):** spill-cleanup now reaches allocation-time Belady slots + (exit-dead scratch renaming, const rematerialization, bounded cleanup + fixpoint, const-divisor guard elision under spill) — all scoped to + `SYNTH_SPILL_ON_EXHAUST` firings; flag-off bit-identical. Cycle-proxy vs + PR #659: spill_rung +32.4% → +8.8%, exhaust +30.4% → +17.4%, + high_pressure_i32 and signed_div_const now BEAT the decline path (−24%, + −33%). Residual named: the bridge's fixed 5-register destination pool — + i.e. the Track-A allocator replacement itself. Flip stays held (#580). + +### Fixed + +- **WASM `unreachable` compiled to a no-op on thumb-2 AND rv32 (#665, PR + #668).** One decode drop: `Unreachable` was whitelisted as intentionally + ignorable next to `Nop`, so every backend's existing trap arm was dead + code. Now decoded; UDF/ebreak/brk fire per backend; optimized path + loud-declines to direct. Differential: 5 red → green with non-vacuity. +- **RV32 i32.rem_s(INT_MIN,-1) spuriously trapped (#666, PR #668)** — rem_s + had inherited div_s's overflow guard; M-ext REM already returns 0 per + spec. The ARM #633 twin-pins now exist on RV32 (rem_s carries only the + zero guard). + +### Added + +- **Null-funcref-slot call_indirect (#664, PR #669):** sparse tables no + longer decline — initialized slots type-verified closed-world, null slots + trap at runtime (check emitted only when the table has nulls; fully- + initialized tables whole-ELF byte-identical, 24/24). Contract: null slots + link as zero words (BSS satisfies). falcon's dispatch story is complete. +- **VCR-SEL-001 increment 4 (PR #670, #242/#667):** 40 rules / 40 Qed — + clz, ctz (scratch=dest, no side condition), popcnt (pseudo-op tier), and + the ten binary i64 comparisons (the #615 cond-mapping class, register- + polymorphic). New DSL-coverage metric in coq/STATUS.md: 26% DSL-served / + 62% model-only / 12% unverified — the #73 divergence now retires by + measurable subtraction. Named executor gap (SBCS flags-chain) converges + with the ISA spike's PC-executor gap. +- **VCR-ISA-001 round 2 (PR #671, #242):** SailArmBridge.v 23 → **81 Qed** + (28 whole-instruction bridges: AddWithCarry family incl. live-carry + ADC/SBC, flag-free ALU, all four shifts in both forms, MOV/MOVW/MOVT). + **Found two latent hand-model divergences from ARM's ASL** (LSR/ASR #32, + register shift amounts ≥ 32 — unreachable via WASM masking, documented). + Amortization beat the spike estimate: six-plus classes in ~half a day. + VCR-ISA-001 → approved. + ## [0.35.0] - 2026-07-08 **The North-Star acceleration wave: the verified selector DSL enters the i64 diff --git a/Cargo.lock b/Cargo.lock index e715c86..1b3deec 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2060,14 +2060,14 @@ dependencies = [ [[package]] name = "synth-abi" -version = "0.35.0" +version = "0.36.0" dependencies = [ "synth-wit", ] [[package]] name = "synth-analysis" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "synth-core", @@ -2076,7 +2076,7 @@ dependencies = [ [[package]] name = "synth-backend" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "synth-core", @@ -2086,7 +2086,7 @@ dependencies = [ [[package]] name = "synth-backend-aarch64" -version = "0.35.0" +version = "0.36.0" dependencies = [ "synth-core", "thiserror", @@ -2095,7 +2095,7 @@ dependencies = [ [[package]] name = "synth-backend-awsm" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "synth-core", @@ -2104,7 +2104,7 @@ dependencies = [ [[package]] name = "synth-backend-riscv" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "proptest", @@ -2116,7 +2116,7 @@ dependencies = [ [[package]] name = "synth-backend-wasker" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "synth-core", @@ -2125,11 +2125,11 @@ dependencies = [ [[package]] name = "synth-cfg" -version = "0.35.0" +version = "0.36.0" [[package]] name = "synth-cli" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "clap", @@ -2156,7 +2156,7 @@ dependencies = [ [[package]] name = "synth-core" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "gimli", @@ -2170,7 +2170,7 @@ dependencies = [ [[package]] name = "synth-frontend" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "synth-core", @@ -2184,14 +2184,14 @@ dependencies = [ [[package]] name = "synth-memory" -version = "0.35.0" +version = "0.36.0" dependencies = [ "bitflags", ] [[package]] name = "synth-opt" -version = "0.35.0" +version = "0.36.0" dependencies = [ "criterion", "synth-cfg", @@ -2199,11 +2199,11 @@ dependencies = [ [[package]] name = "synth-qemu" -version = "0.35.0" +version = "0.36.0" [[package]] name = "synth-synthesis" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "proptest", @@ -2218,7 +2218,7 @@ dependencies = [ [[package]] name = "synth-test" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "clap", @@ -2234,7 +2234,7 @@ dependencies = [ [[package]] name = "synth-verify" -version = "0.35.0" +version = "0.36.0" dependencies = [ "anyhow", "chrono", @@ -2253,7 +2253,7 @@ dependencies = [ [[package]] name = "synth-wit" -version = "0.35.0" +version = "0.36.0" [[package]] name = "tempfile" diff --git a/Cargo.toml b/Cargo.toml index 22249ac..373f28c 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.35.0" +version = "0.36.0" edition = "2024" rust-version = "1.88" authors = ["PulseEngine Team"] diff --git a/MODULE.bazel b/MODULE.bazel index a3fafe0..74d0db8 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.35.0", + version = "0.36.0", ) # Bazel dependencies diff --git a/crates/synth-backend-aarch64/Cargo.toml b/crates/synth-backend-aarch64/Cargo.toml index 9c68f46..e5a9abb 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.35.0" } +synth-core = { path = "../synth-core", version = "0.36.0" } thiserror.workspace = true tracing.workspace = true diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml index 10078ca..14203dc 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.35.0" } +synth-core = { path = "../synth-core", version = "0.36.0" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml index 10064ce..7c17491 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.35.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.35.0" } +synth-core = { path = "../synth-core", version = "0.36.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.36.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 cbd28ac..5819240 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.35.0" } +synth-core = { path = "../synth-core", version = "0.36.0" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml index 66c966f..fc616ca 100644 --- a/crates/synth-backend/Cargo.toml +++ b/crates/synth-backend/Cargo.toml @@ -15,7 +15,7 @@ default = ["arm-cortex-m"] arm-cortex-m = ["synth-synthesis"] [dependencies] -synth-core = { path = "../synth-core", version = "0.35.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.35.0", optional = true } +synth-core = { path = "../synth-core", version = "0.36.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.36.0", optional = true } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index 66a4897..4e8aba4 100644 --- a/crates/synth-cli/Cargo.toml +++ b/crates/synth-cli/Cargo.toml @@ -44,23 +44,23 @@ verify = ["synth-verify"] # 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.35.0" } -synth-frontend = { path = "../synth-frontend", version = "0.35.0" } -synth-synthesis = { path = "../synth-synthesis", version = "0.35.0" } -synth-backend = { path = "../synth-backend", version = "0.35.0" } +synth-core = { path = "../synth-core", version = "0.36.0" } +synth-frontend = { path = "../synth-frontend", version = "0.36.0" } +synth-synthesis = { path = "../synth-synthesis", version = "0.36.0" } +synth-backend = { path = "../synth-backend", version = "0.36.0" } # AArch64 host-native backend (#538) — small pure-Rust crate, always on. -synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.35.0" } +synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.36.0" } # Optional external backends -synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.35.0", optional = true } -synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.35.0", optional = true } -synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.35.0", optional = true } +synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.36.0", optional = true } +synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.36.0", optional = true } +synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.36.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.35.0", optional = true, features = ["arm"] } +synth-verify = { path = "../synth-verify", version = "0.36.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 0a1a4bc..3f6c1f3 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.35.0" } +synth-core = { path = "../synth-core", version = "0.36.0" } wasmparser.workspace = true wasm-encoder.workspace = true diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml index a895a43..eb266a1 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.35.0" } +synth-cfg = { path = "../synth-cfg", version = "0.36.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 6c705cd..aeacecb 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.35.0" } -synth-cfg = { path = "../synth-cfg", version = "0.35.0" } -synth-opt = { path = "../synth-opt", version = "0.35.0" } +synth-core = { path = "../synth-core", version = "0.36.0" } +synth-cfg = { path = "../synth-cfg", version = "0.36.0" } +synth-opt = { path = "../synth-opt", version = "0.36.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 6cf9d92..d10d12d 100644 --- a/crates/synth-verify/Cargo.toml +++ b/crates/synth-verify/Cargo.toml @@ -20,12 +20,12 @@ arm = ["synth-synthesis"] [dependencies] # Core dependencies (always required) -synth-core = { path = "../synth-core", version = "0.35.0" } -synth-cfg = { path = "../synth-cfg", version = "0.35.0" } -synth-opt = { path = "../synth-opt", version = "0.35.0" } +synth-core = { path = "../synth-core", version = "0.36.0" } +synth-cfg = { path = "../synth-cfg", version = "0.36.0" } +synth-opt = { path = "../synth-opt", version = "0.36.0" } # ARM synthesis (optional, behind 'arm' feature) -synth-synthesis = { path = "../synth-synthesis", version = "0.35.0", optional = true } +synth-synthesis = { path = "../synth-synthesis", version = "0.36.0", optional = true } # Default SMT engine: pure-Rust, certificate-checked QF_BV solver (#553) ordeal = "0.4"