Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 50 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
34 changes: 17 additions & 17 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Expand Down
2 changes: 1 addition & 1 deletion MODULE.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion crates/synth-backend-awsm/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions crates/synth-backend-riscv/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion crates/synth-backend-wasker/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions crates/synth-backend/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
16 changes: 8 additions & 8 deletions crates/synth-cli/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion crates/synth-frontend/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion crates/synth-opt/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"] }
Expand Down
6 changes: 3 additions & 3 deletions crates/synth-synthesis/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions crates/synth-verify/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down
Loading