From 13fc272ce3a0b38b26e52deacc42da4d1983c824 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Mon, 22 Jun 2026 06:32:36 +0200 Subject: [PATCH] =?UTF-8?q?chore(release):=20v0.11.51=20=E2=80=94=20VCR-ME?= =?UTF-8?q?M-001=20layer-1=20shadow-stack=20shrink=20+=20pin=20sweep=20+?= =?UTF-8?q?=20changelog?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Headline: #383 native-pointer shadow-stack shrink (--shadow-stack-size B now active), the feature gale held the release for — gust 8 KiB STM32F100 boot unblocked (.bss 1048720→4240), opt-in/default-off, on-silicon confirmed (#383 closed COMPLETED). Also: cross-backend op-parity oracle (#387), register-polymorphic i32 pilot (#386), scry regalloc/stack-depth substrate (#392/#397), DWARF Tier-1 read→compose→emit logic frozen-safe (#399/#403/#413/ #414/#415, toward v0.12.0), and VCR traceability/roadmap (#400/#407/#410/#411). Pin sweep 0.11.50 → 0.11.51 across the workspace + path-deps + MODULE.bazel. Co-Authored-By: Claude Opus 4.8 --- CHANGELOG.md | 50 ++++++++++++++++++++++++++ Cargo.lock | 34 +++++++++--------- Cargo.toml | 2 +- MODULE.bazel | 2 +- crates/synth-backend-awsm/Cargo.toml | 2 +- crates/synth-backend-riscv/Cargo.toml | 4 +-- crates/synth-backend-wasker/Cargo.toml | 2 +- crates/synth-backend/Cargo.toml | 4 +-- crates/synth-cli/Cargo.toml | 16 ++++----- crates/synth-frontend/Cargo.toml | 2 +- crates/synth-opt/Cargo.toml | 2 +- crates/synth-synthesis/Cargo.toml | 6 ++-- crates/synth-verify/Cargo.toml | 8 ++--- 13 files changed, 92 insertions(+), 42 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 10107ae1..7d86b0e9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,56 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +## [0.11.51] - 2026-06-22 + +**NATIVE-POINTER SHADOW-STACK SHRINK — #383 (VCR-MEM-001 layer-1): the +`--shadow-stack-size B` flag is now ACTIVE.** Under `--native-pointer-abi` synth +reserved the wasm linear memory up to the declared page top (the `__stack_pointer` +global's init), so a module that declares a large memory but lives in a few KB +(gale's `gust` kernel: `(memory 17)` ≈ 1 MiB) could not be placed on a small-RAM +MCU. `--shadow-stack-size B` re-bases the shadow-stack top to `B` and shrinks the +NOBITS `.bss` reservation accordingly, unblocking the 8 KiB STM32F100 gust boot. + +- **#383 — `--shadow-stack-size B` shrink** (was: honest-Err scaffold, #388). + Re-bases the `__stack_pointer` global slot `sp_init → B` and resizes the + reservation to `B + static-tail`. Measured on `gust_kernel.wasm`: + `--shadow-stack-size 4096` → `.bss` 1048720 → 4240 B, SP slot 1048576 → 4096, + `.text`/`.data` + all relocations unchanged. + - Correct-by-construction for the verified stack-first geometry (statics + at/above `sp_init` retargeted into the packed `.data` per #354, the only + `.bss` static relocs being addend-0 region-base pointers, stable under the + shrink). **Refuses honestly** (typed Err) for any geometry it cannot prove + safe: one-PROGBITS fallback, `B > sp_init`, a non-zero inline static addend, + a non-Abs32 reservation reloc, or an ambiguous SP global. + - **Opt-in**: default unset reserves the full page ⇒ frozen fixtures + bit-identical. The footprint is ASSERTED (the budget is trusted), not proven; + the budget must cover everything live in linear memory above address 0. + - Verification: flag-off byte-identical on `msgq_put_359` (the native-pointer + path); the native-pointer differential passes; flag-on runtime exercised on + `native_pointer_shadow_stack` (the store through the re-based SP lands + in-region). gale confirmed on-silicon (issue #383 closed COMPLETED). + - Tests `shadow_stack_shrink_383.rs`; tracked `VCR-MEM-001`. + +- **Cross-backend op-parity oracle** (#387, `VCR-SEL-005`): the ARM-vs-RISC-V + op-lowering parity ledger surfaces "selector missed an op" gaps (the #223/#232 + class) as a gate rather than on silicon. +- **Register-polymorphic i32 lowering pilot** (#386, `VCR-SEL-001`): first + discharge-under-generalization measurement toward the verified selector DSL. +- **scry-for-regalloc + shadow-stack-depth substrate** (#392, #397, `VCR-RA-010` + / `VCR-MEM-001` layer-2): scry's const-remat signal and longest-path + shadow-stack bound (`scry-sai-core` v1.12) verified in-tree as DEV-dependency + substrate (no production dep). +- **DWARF Tier-1 read→compose→emit logic** (#399, #403, #413, #414, #415, + `VCR-DBG-001`, toward v0.12.0): the decoder records per-op wasm byte offsets; + the input `.debug_line` parses to (offset → file:line); the op-index → source + composer normalizes and joins; and the emit round-trips faithfully — all + frozen-safe (no production gimli dep, no output-ELF change). The gated ELF + wiring is the v0.12.0 release step. +- **Traceability + roadmap**: requirement→test `verifies` bindings for the + implemented VCR features (#410, #411), the VCR-MEM-002 multi-memory structural + isolation decision (#407, meld#300), and the VCR-PERF-001 silicon size-gap + attribution (#391, gale #390). Cross-repo scry traceability (#400). + ## [0.11.50] - 2026-06-19 **LARGE LOAD/STORE OFFSET — #382: a static memory `offset > 0xFFF` (4095) no diff --git a/Cargo.lock b/Cargo.lock index a89d63ee..43773083 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2022,14 +2022,14 @@ dependencies = [ [[package]] name = "synth-abi" -version = "0.11.50" +version = "0.11.51" dependencies = [ "synth-wit", ] [[package]] name = "synth-analysis" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "synth-core", @@ -2038,7 +2038,7 @@ dependencies = [ [[package]] name = "synth-backend" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "synth-core", @@ -2048,7 +2048,7 @@ dependencies = [ [[package]] name = "synth-backend-awsm" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "synth-core", @@ -2057,7 +2057,7 @@ dependencies = [ [[package]] name = "synth-backend-riscv" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "proptest", @@ -2069,7 +2069,7 @@ dependencies = [ [[package]] name = "synth-backend-wasker" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "synth-core", @@ -2078,11 +2078,11 @@ dependencies = [ [[package]] name = "synth-cfg" -version = "0.11.50" +version = "0.11.51" [[package]] name = "synth-cli" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "clap", @@ -2105,7 +2105,7 @@ dependencies = [ [[package]] name = "synth-core" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "gimli", @@ -2119,7 +2119,7 @@ dependencies = [ [[package]] name = "synth-frontend" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "synth-core", @@ -2133,14 +2133,14 @@ dependencies = [ [[package]] name = "synth-memory" -version = "0.11.50" +version = "0.11.51" dependencies = [ "bitflags", ] [[package]] name = "synth-opt" -version = "0.11.50" +version = "0.11.51" dependencies = [ "criterion", "synth-cfg", @@ -2148,11 +2148,11 @@ dependencies = [ [[package]] name = "synth-qemu" -version = "0.11.50" +version = "0.11.51" [[package]] name = "synth-synthesis" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "proptest", @@ -2167,7 +2167,7 @@ dependencies = [ [[package]] name = "synth-test" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "clap", @@ -2183,7 +2183,7 @@ dependencies = [ [[package]] name = "synth-verify" -version = "0.11.50" +version = "0.11.51" dependencies = [ "anyhow", "chrono", @@ -2201,7 +2201,7 @@ dependencies = [ [[package]] name = "synth-wit" -version = "0.11.50" +version = "0.11.51" [[package]] name = "tempfile" diff --git a/Cargo.toml b/Cargo.toml index 26437731..ea579c9b 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.50" +version = "0.11.51" edition = "2024" rust-version = "1.88" authors = ["PulseEngine Team"] diff --git a/MODULE.bazel b/MODULE.bazel index 2a550454..f67a4000 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.50", + version = "0.11.51", ) # Bazel dependencies diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml index 3e1c96fc..1ca47caf 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.50" } +synth-core = { path = "../synth-core", version = "0.11.51" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml index 7c982f0b..4f905fd4 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.50" } -synth-synthesis = { path = "../synth-synthesis", version = "0.11.50" } +synth-core = { path = "../synth-core", version = "0.11.51" } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.51" } 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 5320fce8..e690c8db 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.50" } +synth-core = { path = "../synth-core", version = "0.11.51" } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml index 71632d02..8f665787 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.50" } -synth-synthesis = { path = "../synth-synthesis", version = "0.11.50", optional = true } +synth-core = { path = "../synth-core", version = "0.11.51" } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.51", optional = true } anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index 64e814a3..60999dfd 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.50" } -synth-frontend = { path = "../synth-frontend", version = "0.11.50" } -synth-synthesis = { path = "../synth-synthesis", version = "0.11.50" } -synth-backend = { path = "../synth-backend", version = "0.11.50" } +synth-core = { path = "../synth-core", version = "0.11.51" } +synth-frontend = { path = "../synth-frontend", version = "0.11.51" } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.51" } +synth-backend = { path = "../synth-backend", version = "0.11.51" } # Optional external backends -synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.11.50", optional = true } -synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.11.50", optional = true } -synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.11.50", optional = true } +synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.11.51", optional = true } +synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.11.51", optional = true } +synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.11.51", optional = true } # Optional verification (requires z3) -synth-verify = { path = "../synth-verify", version = "0.11.50", optional = true, features = ["z3-solver", "arm"] } +synth-verify = { path = "../synth-verify", version = "0.11.51", 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 87ff5705..c392a394 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.50" } +synth-core = { path = "../synth-core", version = "0.11.51" } wasmparser.workspace = true wasm-encoder.workspace = true diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml index d19f129e..91b8c818 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.50" } +synth-cfg = { path = "../synth-cfg", version = "0.11.51" } [dev-dependencies] criterion = { version = "0.8", features = ["html_reports"] } diff --git a/crates/synth-synthesis/Cargo.toml b/crates/synth-synthesis/Cargo.toml index 540751e9..24a2a0a7 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.50" } -synth-cfg = { path = "../synth-cfg", version = "0.11.50" } -synth-opt = { path = "../synth-opt", version = "0.11.50" } +synth-core = { path = "../synth-core", version = "0.11.51" } +synth-cfg = { path = "../synth-cfg", version = "0.11.51" } +synth-opt = { path = "../synth-opt", version = "0.11.51" } serde.workspace = true anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml index e389ef98..8ab8b4d0 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.50" } -synth-cfg = { path = "../synth-cfg", version = "0.11.50" } -synth-opt = { path = "../synth-opt", version = "0.11.50" } +synth-core = { path = "../synth-core", version = "0.11.51" } +synth-cfg = { path = "../synth-cfg", version = "0.11.51" } +synth-opt = { path = "../synth-opt", version = "0.11.51" } # ARM synthesis (optional, behind 'arm' feature) -synth-synthesis = { path = "../synth-synthesis", version = "0.11.50", optional = true } +synth-synthesis = { path = "../synth-synthesis", version = "0.11.51", optional = true } # SMT solver for formal verification z3 = { version = "0.19", features = ["static-link-z3"], optional = true }