diff --git a/CHANGELOG.md b/CHANGELOG.md index 48f439b..034b361 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,38 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +## [0.11.40] - 2026-06-11 + +**THE ALLOCATOR ACCEPTANCE RELEASE — VCR-RA-001's five criteria are all met, +and gale's k_mutex_unlock lane unblocks (#242, #326).** + +- **i64 pair-spill via param frame-backing** (#325): the last acceptance + criterion closes. The true pair-exhaustion blocker was pinned param home + registers (no stack spill can free them); a third retry-ladder rung forces + the proven #204 param frame-backing onto call-free functions, after which + a consecutive pair always exists (pigeonhole over the freed pool). Ladder: + default -> spill-only (#320) -> spill+param-backing, each rung triggered + only by its predecessor's exact error — bit-identity stays structural. + NEW high-pressure-i64 lane: hard Err on v0.11.39 -> 6/6 vs wasmtime. +- **Arg-move cycles via the parallel-move resolver** (#327, gale #326): the + call-marshal cycle-breaker no longer demands a callee-saved register — + VCR-RA-004's resolver (v0.11.38) breaks cycles via a stack-scratch cell + when registers are saturated. This unblocks the dissolved k_mutex_unlock + (gale's exact error reproduced on main by the committed mutex_pressure + lane; 7/7 vs wasmtime on the fix) AND killed a latent wrong-code bug: the + old cycle-breaker miscompiled genuine 2-swaps (duplicated a value). +- **VCR-RA-001 status: implemented.** All five criteria verified: no + hard-fail on high-pressure i32 AND i64 modules; fixtures bit-identical + through six releases; cycles equal-or-better on the G474RE (gale); the + v0.11.20 cost-gate revert EXECUTED (#322); the backward-dataflow validator + guarding every re-allocated segment (#323). Honest bounds: the 8-slot + spill pool, stack-passed params, the R8-pair/i64-param class (tracked). + +Falsification: wrong if gale's mutex lane fails on silicon (native ref 124), +any previously-compiling module's bytes change, or any pressure lane +disagrees with wasmtime. + + ## [0.11.39] - 2026-06-11 **The assurance carrier: a backward-dataflow translation validator now guards diff --git a/Cargo.lock b/Cargo.lock index a3d5196..f16e959 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1933,14 +1933,14 @@ dependencies = [ [[package]] name = "synth-abi" -version = "0.11.39" +version = "0.11.40" dependencies = [ "synth-wit", ] [[package]] name = "synth-analysis" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "synth-core", @@ -1949,7 +1949,7 @@ dependencies = [ [[package]] name = "synth-backend" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "synth-core", @@ -1959,7 +1959,7 @@ dependencies = [ [[package]] name = "synth-backend-awsm" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "synth-core", @@ -1968,7 +1968,7 @@ dependencies = [ [[package]] name = "synth-backend-riscv" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "proptest", @@ -1980,7 +1980,7 @@ dependencies = [ [[package]] name = "synth-backend-wasker" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "synth-core", @@ -1989,11 +1989,11 @@ dependencies = [ [[package]] name = "synth-cfg" -version = "0.11.39" +version = "0.11.40" [[package]] name = "synth-cli" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "clap", @@ -2015,7 +2015,7 @@ dependencies = [ [[package]] name = "synth-core" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "serde", @@ -2028,7 +2028,7 @@ dependencies = [ [[package]] name = "synth-frontend" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "synth-core", @@ -2042,14 +2042,14 @@ dependencies = [ [[package]] name = "synth-memory" -version = "0.11.39" +version = "0.11.40" dependencies = [ "bitflags", ] [[package]] name = "synth-opt" -version = "0.11.39" +version = "0.11.40" dependencies = [ "criterion", "synth-cfg", @@ -2057,11 +2057,11 @@ dependencies = [ [[package]] name = "synth-qemu" -version = "0.11.39" +version = "0.11.40" [[package]] name = "synth-synthesis" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "proptest", @@ -2076,7 +2076,7 @@ dependencies = [ [[package]] name = "synth-test" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "clap", @@ -2092,7 +2092,7 @@ dependencies = [ [[package]] name = "synth-verify" -version = "0.11.39" +version = "0.11.40" dependencies = [ "anyhow", "chrono", @@ -2110,7 +2110,7 @@ dependencies = [ [[package]] name = "synth-wit" -version = "0.11.39" +version = "0.11.40" [[package]] name = "tempfile" diff --git a/Cargo.toml b/Cargo.toml index 104cefe..4a6d621 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -27,7 +27,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.11.39" +version = "0.11.40" edition = "2024" rust-version = "1.88" authors = ["PulseEngine Team"] diff --git a/MODULE.bazel b/MODULE.bazel index f4d16fe..f7f3e52 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.11.39", + version = "0.11.40", ) # Bazel dependencies diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 674f263..6140ec9 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -143,7 +143,7 @@ artifacts: shortcuts be reverted toward the clean form. Must keep the reserved-reg architecture (R9 globals / R11 mem-base / R12 IP-scratch) and the bounds-mode R10 invariant. - status: proposed + status: implemented tags: [codegen, register-allocation, ssa, regalloc2, track-a, release-v0.11.40] links: - type: derives-from diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml index 1203047..7bb3f68 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.11.39" } +synth-core = { path = "../synth-core", version = "0.11.40" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml index 8d1ac54..c379226 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.11.39" } -synth-synthesis = { path = "../synth-synthesis", version = "0.11.39" } +synth-core = { path = "../synth-core", version = "0.11.40" } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.40" } 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 e036928..7e6560a 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.11.39" } +synth-core = { path = "../synth-core", version = "0.11.40" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml index a937cbc..99b4ae9 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.11.39" } -synth-synthesis = { path = "../synth-synthesis", version = "0.11.39", optional = true } +synth-core = { path = "../synth-core", version = "0.11.40" } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.40", optional = true } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index 160fd95..a7b6c2e 100644 --- a/crates/synth-cli/Cargo.toml +++ b/crates/synth-cli/Cargo.toml @@ -27,18 +27,18 @@ 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.11.39" } -synth-frontend = { path = "../synth-frontend", version = "0.11.39" } -synth-synthesis = { path = "../synth-synthesis", version = "0.11.39" } -synth-backend = { path = "../synth-backend", version = "0.11.39" } +synth-core = { path = "../synth-core", version = "0.11.40" } +synth-frontend = { path = "../synth-frontend", version = "0.11.40" } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.40" } +synth-backend = { path = "../synth-backend", version = "0.11.40" } # Optional external backends -synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.11.39", optional = true } -synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.11.39", optional = true } -synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.11.39", optional = true } +synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.11.40", optional = true } +synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.11.40", optional = true } +synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.11.40", optional = true } # Optional verification (requires z3) -synth-verify = { path = "../synth-verify", version = "0.11.39", optional = true, features = ["z3-solver", "arm"] } +synth-verify = { path = "../synth-verify", version = "0.11.40", optional = true, features = ["z3-solver", "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 e1363e3..78acd45 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.11.39" } +synth-core = { path = "../synth-core", version = "0.11.40" } wasmparser.workspace = true wasm-encoder.workspace = true diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml index 527b5de..6ccf838 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.11.39" } +synth-cfg = { path = "../synth-cfg", version = "0.11.40" } [dev-dependencies] criterion = { version = "0.5", features = ["html_reports"] } diff --git a/crates/synth-synthesis/Cargo.toml b/crates/synth-synthesis/Cargo.toml index 17ca3f6..f479b3e 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.11.39" } -synth-cfg = { path = "../synth-cfg", version = "0.11.39" } -synth-opt = { path = "../synth-opt", version = "0.11.39" } +synth-core = { path = "../synth-core", version = "0.11.40" } +synth-cfg = { path = "../synth-cfg", version = "0.11.40" } +synth-opt = { path = "../synth-opt", version = "0.11.40" } serde.workspace = true anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml index 88a10a8..93843bf 100644 --- a/crates/synth-verify/Cargo.toml +++ b/crates/synth-verify/Cargo.toml @@ -17,12 +17,12 @@ arm = ["synth-synthesis"] [dependencies] # Core dependencies (always required) -synth-core = { path = "../synth-core", version = "0.11.39" } -synth-cfg = { path = "../synth-cfg", version = "0.11.39" } -synth-opt = { path = "../synth-opt", version = "0.11.39" } +synth-core = { path = "../synth-core", version = "0.11.40" } +synth-cfg = { path = "../synth-cfg", version = "0.11.40" } +synth-opt = { path = "../synth-opt", version = "0.11.40" } # ARM synthesis (optional, behind 'arm' feature) -synth-synthesis = { path = "../synth-synthesis", version = "0.11.39", optional = true } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.40", optional = true } # SMT solver for formal verification z3 = { version = "0.19", features = ["static-link-z3"], optional = true }