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

## [Unreleased]

## [0.13.0] - 2026-06-24

**cmp→select fusion is now DEFAULT-ON (VCR-SEL-004, #428, epic #242).** The ARM
backend's compare→select lowering no longer materializes a boolean and re-tests
it (`cmp; SetCond; cmp #0; movne; moveq`); it predicates the moves directly on
the compare's own flags (`cmp; mov{c}; mov{invert(c)}`), −2 instructions per
select. This is a **byte-changing** release: `.text` shrinks on every function
with a select (control_step 354→324 B, flight_seam 1016→902, flight_seam_flat
1240→1122; −262 B across the frozen fixtures), and gale's `gust_mix` measured
2.375×→2.125× vs LLVM with a 132→116 B function.

Execution **results are preserved** — validated three ways before shipping: (1)
the named-anchor differentials re-run with fusion on (control_step still
`0x00210A55`, flat+inlined flight_algo still `0x07FDF307`); (2) a unicorn
execution oracle that runs the two-move `mov{invert(c)}` arm (`cmp-select-oracle`
CI job, 11/11 result-identical); (3) gale's `gale_decider_diff` sweep across all
8 verified primitives (10,596 cases, native ≡ unfused ≡ fused). The byte gates
were re-frozen to the fused `.text` on this commit.

**Escape hatch:** `SYNTH_NO_CMP_SELECT_FUSE=1` reverts to the pre-fusion lowering.
**Pending follow-up:** the on-silicon G474RE DWT cycle no-regression check is
tracked post-ship (gale); the qemu `-icount` proxy showed a monotonic win.

## [0.12.0] - 2026-06-23

**DWARF SOURCE-LINE DEBUGGING — `--debug-line` (VCR-DBG-001, #394, epic #242).**
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.12.0"
version = "0.13.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.12.0",
version = "0.13.0",
)

# Bazel dependencies
Expand Down
11 changes: 10 additions & 1 deletion artifacts/verified-codegen-roadmap.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -737,7 +737,16 @@ artifacts:
exhaustive sweep); precond (2) (G474RE silicon no-regression) still OWED —
gale's bench is thumbv7m/qemu today — flip stays held on it (user call
2026-06-23: keep the silicon gate; close the exec gap first).
status: approved
FLIP SHIPPED v0.13.0 (2026-06-24, #428): default-on landed. User authorized
shipping on the qemu+sweep+oracle evidence and WAIVING precond (2) for the
release (gale takes the on-silicon G474RE DWT no-regression as a tracked
post-ship follow-up). Re-froze the fused .text on the same commit the
named-anchor differentials were re-run on (control_step preserved 0x00210A55,
flat+inlined flight_algo preserved 0x07FDF307; .text −262 B across the frozen
fixtures). Escape hatch SYNTH_NO_CMP_SELECT_FUSE=1 reverts the lowering.
SCOPE: the select half shipped; the br_if→predicated-branch half remains a
separate follow-up (branch consumers unmodeled by reg_effect).
status: implemented
tags: [codegen, selector, peephole, compare-select, flag-fusion, gale-209, perf, track-b, vcr-oracle-001]
links:
- type: derives-from
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.12.0" }
synth-core = { path = "../synth-core", version = "0.13.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.12.0" }
synth-synthesis = { path = "../synth-synthesis", version = "0.12.0" }
synth-core = { path = "../synth-core", version = "0.13.0" }
synth-synthesis = { path = "../synth-synthesis", version = "0.13.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.12.0" }
synth-core = { path = "../synth-core", version = "0.13.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.12.0" }
synth-synthesis = { path = "../synth-synthesis", version = "0.12.0", optional = true }
synth-core = { path = "../synth-core", version = "0.13.0" }
synth-synthesis = { path = "../synth-synthesis", version = "0.13.0", optional = true }
anyhow.workspace = true
thiserror.workspace = true
19 changes: 12 additions & 7 deletions crates/synth-backend/src/arm_backend.rs
Original file line number Diff line number Diff line change
Expand Up @@ -433,15 +433,20 @@ fn compile_wasm_to_arm(
// sound (flags reused only when nothing clobbers them in the window; the
// boolean deleted only when provably dead) — see `fuse_cmp_select`.
//
// BEHIND `SYNTH_CMP_SELECT_FUSE=1` while it is validated against the
// differential oracle + gale's on-target gust_codegen_bench (G474RE). Off by
// default ⇒ a literal no-op ⇒ every fixture stays bit-identical
// (control_step 0x00210A55 / flat+inlined flight_algo 0x07FDF307 / divseam).
// The default-on flip is the held byte-changing step, gated on silicon.
let arm_instrs = if std::env::var("SYNTH_CMP_SELECT_FUSE").is_ok() {
// DEFAULT-ON as of v0.13.0 (#428): cmp→select fusion ships by default. The
// byte-changing flip is validated by (a) the unicorn execution oracle that runs
// the two-move `mov{invert(c)}` arm (cmp_select_two_move_differential.py), (b)
// gale's gale_decider_diff 10,596-case sweep across all 8 verified primitives
// (native ≡ flag-off ≡ flag-on = 0x88e73178d232bcf5), and (c) the named-anchor
// differentials re-run with fusion ON — control_step still 0x00210A55, flat+
// inlined flight_algo still 0x07FDF307 (results preserved; bytes deliberately
// changed, re-frozen on this commit). Escape hatch: `SYNTH_NO_CMP_SELECT_FUSE=1`
// reverts to the pre-fusion lowering. The on-silicon G474RE DWT no-regression
// check is a tracked post-ship follow-up (gale owns it).
let arm_instrs = if std::env::var("SYNTH_NO_CMP_SELECT_FUSE").is_err() {
// The rewritten stream is identical to `fuse_cmp_select`'s 2-tuple form;
// the extra `two_move` count is diagnostic only (the fusion census /
// blast-radius datum for the flip decision — #7 made that arm reachable).
// blast-radius datum — #7 made that arm reachable).
let (out, fused, two_move) =
synth_synthesis::liveness::fuse_cmp_select_with_stats(&arm_instrs);
if std::env::var("SYNTH_FUSE_STATS").is_ok() {
Expand Down
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.12.0" }
synth-frontend = { path = "../synth-frontend", version = "0.12.0" }
synth-synthesis = { path = "../synth-synthesis", version = "0.12.0" }
synth-backend = { path = "../synth-backend", version = "0.12.0" }
synth-core = { path = "../synth-core", version = "0.13.0" }
synth-frontend = { path = "../synth-frontend", version = "0.13.0" }
synth-synthesis = { path = "../synth-synthesis", version = "0.13.0" }
synth-backend = { path = "../synth-backend", version = "0.13.0" }

# Optional external backends
synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.12.0", optional = true }
synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.12.0", optional = true }
synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.12.0", optional = true }
synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.13.0", optional = true }
synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.13.0", optional = true }
synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.13.0", optional = true }

# Optional verification (requires z3)
synth-verify = { path = "../synth-verify", version = "0.12.0", optional = true, features = ["z3-solver", "arm"] }
synth-verify = { path = "../synth-verify", version = "0.13.0", optional = true, features = ["z3-solver", "arm"] }

# Optional PulseEngine WASM optimizer
# Uncomment when loom crate is available:
Expand Down
31 changes: 19 additions & 12 deletions crates/synth-cli/tests/frozen_codegen_bytes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,15 +55,16 @@ fn fixture(name: &str) -> std::path::PathBuf {

/// Compile a frozen fixture for `(backend, target)` with the exact `--all-exports
/// --relocatable` config the `.py` differentials use, and return the SHA-256 hex
/// of its `.text` and the section length. `SYNTH_CMP_SELECT_FUSE` / `SYNTH_CONST_CSE`
/// are explicitly removed so an enabled-in-the-environment flag can never silently
/// re-freeze the gate — it locks the SHIPPED, flag-off lowering. The `object`
/// crate reads `.text` arch-agnostically (ARM Thumb-2 and RV32 alike).
/// of its `.text` and the section length. `SYNTH_NO_CMP_SELECT_FUSE` (the v0.13.0
/// cmp→select opt-out) / `SYNTH_CONST_CSE` are explicitly removed so a flag set in
/// the environment can never silently re-freeze the gate — it locks the SHIPPED
/// lowering, which since v0.13.0 INCLUDES cmp→select fusion (default-on). The
/// `object` crate reads `.text` arch-agnostically (ARM Thumb-2 and RV32 alike).
fn text_sha256(wasm: &str, backend: &str, target: &str) -> (String, usize) {
let path = fixture(wasm);
let elf = format!("/tmp/frozenbytes_{backend}_{wasm}.elf");
let out = Command::new(synth())
.env_remove("SYNTH_CMP_SELECT_FUSE")
.env_remove("SYNTH_NO_CMP_SELECT_FUSE")
.env_remove("SYNTH_CONST_CSE")
.args([
"compile",
Expand Down Expand Up @@ -125,24 +126,30 @@ fn assert_frozen(cases: &[(&str, &str, usize)], backend: &str, target: &str) {
/// the `.py` differentials cover): control_step ↔ 0x00210A55, flight_seam_flat ↔
/// flat+inlined flight_algo 0x07FDF307, plus flight_seam and the div seam.
///
/// Goldens derived on main @ ef97f86 (post-#444 cmp→select, flag-off), 2026-06-23.
/// Goldens RE-FROZEN for v0.13.0 (#428): cmp→select fusion is now default-on, so
/// these lock the FUSED .text. The execution RESULTS are preserved — re-verified on
/// this commit with fusion on: control_step still 0x00210A55 (control_step_differential
/// .py 13/13), flat+inlined flight_algo still 0x07FDF307 (flight_seam_differential.py
/// MATCH). .text shrank: control_step 354→324, flight_seam 1016→902, flight_seam_flat
/// 1240→1122 (−262 B total); signed_div_const (0 fusion sites) unchanged. Prior
/// flag-off goldens were on main @ ef97f86 (post-#444), 2026-06-23.
#[test]
fn frozen_fixtures_text_is_bit_identical_oracle_001() {
let cases = [
(
"control_step.wasm",
"5efa58ca2667fb2f910b5ebf0ef8020a7fc1b9224f3ec070e9e0028de9d83a57",
354usize,
"b4c4c290be2c8a83055d4c9696ae4ebb16486a8fd3fc268531607eeef35325e5",
324usize,
),
(
"flight_seam.wasm",
"1f39b77b65f0695693deda9ee56e3a7fb3af4127858a8ac6c3ce0fd3398de516",
1016,
"300fdf3b92a0941da63b3215441a799d9b32ef942fd404b4803a83a6efb1bb60",
902,
),
(
"flight_seam_flat.wasm",
"f6244f35f932aac7661b9ed1cbf70dc1b5353a9f5c03178ebad3a38a891d7b8f",
1240,
"23d0b6829414a855f365d84c7c3301c256f1843fe46b2cc9b369fec30610913d",
1122,
),
(
"signed_div_const.wasm",
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.12.0" }
synth-core = { path = "../synth-core", version = "0.13.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.12.0" }
synth-cfg = { path = "../synth-cfg", version = "0.13.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.12.0" }
synth-cfg = { path = "../synth-cfg", version = "0.12.0" }
synth-opt = { path = "../synth-opt", version = "0.12.0" }
synth-core = { path = "../synth-core", version = "0.13.0" }
synth-cfg = { path = "../synth-cfg", version = "0.13.0" }
synth-opt = { path = "../synth-opt", version = "0.13.0" }
serde.workspace = true
anyhow.workspace = true
thiserror.workspace = true
Expand Down
Loading
Loading