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
36 changes: 36 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,42 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0

## [Unreleased]

## [0.34.0] - 2026-07-08

**Multi-table call_indirect ships (falcon's fused-component blocker); float
and i64 global initializers actually reach the image; the mask bounds mode
becomes sound. Six gale filings closed same-day across two waves.**

### Added

- **Multi-table call_indirect (#650, PR #653).** Tables form one contiguous
region at R11 (table N at a compile-time constant offset — sound because
tables are provably fixed-size per #646); the dispatch folds the offset
via R12; the #642 bounds guard checks the dispatched table's own size and
the closed-world type verification runs per (table, expected-type).
Single-table modules are byte-identical BY CONSTRUCTION (offset-0 emits
the literal pre-#650 sequence — verified by whole-ELF cmp across three
targets). New CI oracle: two-table aliasing canary + per-table OOB traps,
26/26 (both ISAs).

### Fixed

- **Global initializers never reached the self-contained image (#649,
PR #652; float side GI-FPU-001, PR #648).** The decoder only captured
i32.const inits, and the default Cortex-M image never materialized the
globals table at all — R9 was uninitialized and reads returned
vector-table garbage. Now the startup stub sets R9 and stores every init
word (width-aware #645 layout, i64 = two words); float-typed globals
loud-skip (GI-FPU-001). New oracle executes the image's real reset path
in unicorn: 4 divergences → 0. Sibling filed: #655 (RV32 mask-order twin).
- **--safety-bounds mask applied the mask before the static offset (#651,
PR #654)** — the offset escaped the bound; AND the old mask used the
memory SIZE (not size-1), remapping in-bounds accesses to 0. All 8 mask
sites now share one helper: min((operand + offset) & (size-1),
size - access_size), with the u33-soundness argument documented and
large offsets materialized (no decline). Mini-interpreter oracle: 8/8
FAIL → 8/8 ok. Non-power-of-two memories decline loudly under mask.

## [0.33.1] - 2026-07-08

**Two more gale-filed silent miscompiles fixed same-day: call_indirect gets
Expand Down
36 changes: 18 additions & 18 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 @@ -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.33.1"
version = "0.34.0"
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.33.1",
version = "0.34.0",
)

# Bazel dependencies
Expand Down
2 changes: 1 addition & 1 deletion crates/synth-backend-aarch64/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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.33.1" }
synth-core = { path = "../synth-core", version = "0.34.0" }
thiserror.workspace = true
tracing.workspace = true
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.33.1" }
synth-core = { path = "../synth-core", version = "0.34.0" }
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.33.1" }
synth-synthesis = { path = "../synth-synthesis", version = "0.33.1" }
synth-core = { path = "../synth-core", version = "0.34.0" }
synth-synthesis = { path = "../synth-synthesis", version = "0.34.0" }
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.33.1" }
synth-core = { path = "../synth-core", version = "0.34.0" }
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.33.1" }
synth-synthesis = { path = "../synth-synthesis", version = "0.33.1", optional = true }
synth-core = { path = "../synth-core", version = "0.34.0" }
synth-synthesis = { path = "../synth-synthesis", version = "0.34.0", optional = true }
anyhow.workspace = true
thiserror.workspace = true
18 changes: 9 additions & 9 deletions crates/synth-cli/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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.33.1" }
synth-frontend = { path = "../synth-frontend", version = "0.33.1" }
synth-synthesis = { path = "../synth-synthesis", version = "0.33.1" }
synth-backend = { path = "../synth-backend", version = "0.33.1" }
synth-core = { path = "../synth-core", version = "0.34.0" }
synth-frontend = { path = "../synth-frontend", version = "0.34.0" }
synth-synthesis = { path = "../synth-synthesis", version = "0.34.0" }
synth-backend = { path = "../synth-backend", version = "0.34.0" }

# AArch64 host-native backend (#538) — small pure-Rust crate, always on.
synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.33.1" }
synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.34.0" }

# Optional external backends
synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.33.1", optional = true }
synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.33.1", optional = true }
synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.33.1", optional = true }
synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.34.0", optional = true }
synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.34.0", optional = true }
synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.34.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.33.1", optional = true, features = ["arm"] }
synth-verify = { path = "../synth-verify", version = "0.34.0", optional = true, features = ["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.33.1" }
synth-core = { path = "../synth-core", version = "0.34.0" }

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.33.1" }
synth-cfg = { path = "../synth-cfg", version = "0.34.0" }

[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.33.1" }
synth-cfg = { path = "../synth-cfg", version = "0.33.1" }
synth-opt = { path = "../synth-opt", version = "0.33.1" }
synth-core = { path = "../synth-core", version = "0.34.0" }
synth-cfg = { path = "../synth-cfg", version = "0.34.0" }
synth-opt = { path = "../synth-opt", version = "0.34.0" }
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 @@ -20,12 +20,12 @@ arm = ["synth-synthesis"]

[dependencies]
# Core dependencies (always required)
synth-core = { path = "../synth-core", version = "0.33.1" }
synth-cfg = { path = "../synth-cfg", version = "0.33.1" }
synth-opt = { path = "../synth-opt", version = "0.33.1" }
synth-core = { path = "../synth-core", version = "0.34.0" }
synth-cfg = { path = "../synth-cfg", version = "0.34.0" }
synth-opt = { path = "../synth-opt", version = "0.34.0" }

# ARM synthesis (optional, behind 'arm' feature)
synth-synthesis = { path = "../synth-synthesis", version = "0.33.1", optional = true }
synth-synthesis = { path = "../synth-synthesis", version = "0.34.0", optional = true }

# Default SMT engine: pure-Rust, certificate-checked QF_BV solver (#553)
ordeal = "0.4"
Expand Down
Loading