fix(#846): recover gpio-thin +44 B — flip shift-mask-elide default-on

CHANGELOG.md

@@ -7,16 +7,42 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
-## [0.50.0] - 2026-07-22
+## [0.50.1] - 2026-07-23
+
+### Changed
+
+- **gpio-thin size regression (#846): `SYNTH_SHIFT_MASK_ELIDE` now default-on.**
+  The #686 shift-mask elision (dropping a redundant `and rN, #31` mask-of-shift-
+  amount when the amount is provably <32, incl. the `and X,#0x1f`-masked-operand
+  Pattern B) shipped flag-off in v0.49. gale's real 656 B `gpio.loom.wasm` emitted
+  10 such redundant `and.w ip, rN, #31` sites → the +9% (490 → 534 B) regression.
+  Flipping the elision on by default recovers **534 → 506 B** (−28 B; 6 of the 10
+  masks proven redundant). Execution proven bit-identical vs wasmtime on gale's
+  driver (75/75 mmio traces incl. pin ≥ 32) and the corpus sweep. Opt-out
+  `SYNTH_SHIFT_MASK_ELIDE=0`. The 4 residual masks (the ones the elision can't
+  prove <32, ~16 B to gale's 490 B target) are a tracked follow-up.
+
+### Fixed
+
+- **[0.50.0 doc correction] The v0.50.0 notes described "the SMT validator models
+  i64 remainder natively instead of havoc" — that lane (#844) was reverted before
+  the v0.50.0 tag** (the ordeal 0.12 solver-perf regression it depended on hung CI;
+  ordeal pinned to =0.9.1, #849). i64 remainder is modeled as havoc in 0.50.0 and
+  0.50.1; the native model re-lands behind a per-query solver timeout (#848). The
+  0.50.0 intro prose below is left as-shipped for the historical record; this note
+  is the correction.
+
+## [0.50.0] - 2026-07-23
 
 **"Cross-backend verified core, and the allocator endgame begins."** The
 whole-function register-allocation validator is now cross-backend (ARM incl.
-optimized joins + RV32), the SMT validator models i64 remainder natively instead
-of havoc, and — the headline — **a from-construction graph-colouring register
-allocator lands (flag-off), with every function it emits validated by that same
-verified oracle.** That is the North Star's first foothold: the verified checker
-gating its own replacement. Seven parallel lanes; every one oracle-gated red-first;
-frozen anchors byte-identical throughout.
+optimized joins + RV32) and — the headline — **a from-construction graph-colouring
+register allocator lands (flag-off), with every function it emits validated by that
+same verified oracle.** That is the North Star's first foothold: the verified
+checker gating its own replacement. Seven parallel lanes; every one oracle-gated
+red-first; frozen anchors byte-identical throughout. *(Correction: an earlier draft
+of these notes claimed native i64-remainder SMT modeling; that lane was reverted
+pre-tag — see the [0.50.1] Fixed note.)*
 
 ### Added
 

Cargo.toml

@@ -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.50.0"
+version = "0.50.1"
 edition = "2024"
 rust-version = "1.88"
 authors = ["PulseEngine Team"]

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.50.0",
+    version = "0.50.1",
 )
 
 # Bazel dependencies

artifacts/parity-benchmark.md

@@ -92,7 +92,7 @@ Regenerate everything on this page:
 | gust_poll bounds (8 sw guards) | synth AOT --safety-bounds software (no facts) | 184 | MEASURED | 1.77x | OPEN — gale silicon (DWT) |
 | gust_poll bounds (8 sw guards) | synth AOT sw bounds + SYNTH_FACT_SPEC=1 (proven slot∈[0,63]) | 104 | MEASURED (8 ordeal ADMITs) | 1.00x | OPEN — gale silicon (DWT) |
 | gust_poll bounds (8 sw guards) | synth AOT unguarded floor (no --safety-bounds) — group ref | 104 | MEASURED | ref | OPEN — gale silicon (DWT) |
-| flat_flight | synth AOT (default) | 458 | MEASURED | 2.54x | OPEN — gale silicon (DWT) |
+| flat_flight | synth AOT (default) | 384 | MEASURED | 2.13x | OPEN — gale silicon (DWT) |
 | flat_flight | native C — arm-none-eabi-gcc -Os | 180 | MEASURED | ref | OPEN — gale silicon (DWT) |
 | falcon_axis (f32) | synth AOT (cortex-m4f, VFP) | 72 | MEASURED | 1.64x | OPEN — gale silicon (DWT) |
 | falcon_axis (f32) | native C — arm-none-eabi-gcc -Os | 44 | MEASURED | ref | OPEN — gale silicon (DWT) |
@@ -153,7 +153,7 @@ The gap is CLOSING release-over-release, lever by lever, each evidence-gated:
 Open, tracked, and honestly not yet won: general regalloc overhead
 (gust_poll 3.48x,
 spill_reload ~31%, #390/#242 Track A), flat_flight at
-2.54x vs gcc, falcon f32 at
+2.13x vs gcc, falcon f32 at
 1.64x vs gcc (constant materialization
 via `movw/movt+vmov` instead of a literal pool, unused callee-save push), and
 every cycles cell.

artifacts/size_attribution_390.md

@@ -15,11 +15,11 @@ thumbv7m baseline (gust_poll 208 B, gust_mix 12 B, 3.9x) is **CITED** from issue
 
 | function | synth .text (measured) | LLVM (cited #390) | ratio | #390 cited synth |
 |---|---|---|---|---|
-| gust_poll | 716 B | 208 B | 3.44x | 816 B (v0.11.50) |
+| gust_poll | 692 B | 208 B | 3.33x | 816 B (v0.11.50) |
 | gust_mix  | 32 B | 12 B | 2.67x | 44 B (v0.11.50) |
 
 synth has already shrunk since #390 was filed (levers landed v0.12–v0.39): the
-gap is now ~3.44x / ~2.67x, not 3.9x / 3.7x. In particular the
+gap is now ~3.33x / ~2.67x, not 3.9x / 3.7x. In particular the
 `and #0xffff -> uxth` peephole (issue Pass 5) has landed — gust_mix now emits
 `uxth r3, r0`, not the `movw+and` pair. Still open: spill churn, address
 re-materialization, the shadow-stack dance, and bool materialization.
@@ -28,10 +28,10 @@ re-materialization, the shadow-stack dance, and bool materialization.
 
 | function | .text B | spill_reload | addr_materialize | redundant_const | prologue_shadow | guard_bool | copy_move | productive | align_pad |
 |---|---|---|---|---|---|---|---|---|---|
-| gust_poll | 716 | 196 | 56 | 62 | 36 | 108 | 66 | 192 | 0 |
+| gust_poll | 692 | 196 | 56 | 58 | 36 | 96 | 66 | 184 | 0 |
 | gust_mix | 32 | 4 | 0 | 0 | 16 | 0 | 6 | 6 | 0 |
-| func_0 | 408 | 8 | 44 | 130 | 8 | 46 | 14 | 156 | 2 |
-| func_1 | 76 | 0 | 0 | 28 | 8 | 12 | 8 | 20 | 0 |
+| func_0 | 380 | 8 | 44 | 138 | 8 | 26 | 14 | 142 | 0 |
+| func_1 | 60 | 0 | 0 | 24 | 8 | 4 | 8 | 16 | 0 |
 
 Each instruction is assigned to exactly ONE bucket by
 `size_attribution_390.py::classify`; the buckets plus the `productive` residual

artifacts/status.json

@@ -15,7 +15,7 @@
   "sel_dsl_pilot_qed": 7,
   "sel_dsl_rule_qed": 50,
   "sel_dsl_rules": 50,
-  "version": "0.50.0",
+  "version": "0.50.1",
   "verus_spec_fns": 8,
   "wasmcert_bridge_qed": 104
 }

crates/synth-backend-aarch64/Cargo.toml

@@ -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.50.0" }
+synth-core = { path = "../synth-core", version = "0.50.1" }
 thiserror.workspace = true
 tracing.workspace = true

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.50.0" }
+synth-core = { path = "../synth-core", version = "0.50.1" }
 anyhow.workspace = true
 thiserror.workspace = true

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.50.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.50.0" }
+synth-core = { path = "../synth-core", version = "0.50.1" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.50.1" }
 anyhow.workspace = true
 thiserror.workspace = true
 tracing.workspace = true

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.50.0" }
+synth-core = { path = "../synth-core", version = "0.50.1" }
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-backend/Cargo.toml

@@ -15,13 +15,13 @@ default = ["arm-cortex-m"]
 arm-cortex-m = ["synth-synthesis"]
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.50.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.50.0", optional = true }
+synth-core = { path = "../synth-core", version = "0.50.1" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.50.1", optional = true }
 anyhow.workspace = true
 thiserror.workspace = true
 
 [dev-dependencies]
 # #667 move 2: the i64 pseudo-op expansion certification oracle
 # (tests/i64_expansion_certification.rs) feeds THIS crate's emitted encoder
 # bytes to the synth-verify expansion validator. Dev-only — no prod-dep edge.
-synth-verify = { path = "../synth-verify", version = "0.50.0", features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.50.1", features = ["arm"] }

crates/synth-backend/src/arm_backend.rs

@@ -1257,23 +1257,30 @@ fn compile_wasm_to_arm(
     // shift) and before branch resolution (removal/rewrite-only ⇒
     // offset-neutral).
     //
-    // FLAG-OFF (opt-in via `SYNTH_SHIFT_MASK_ELIDE=1`) because the elision
-    // moves the frozen anchors: const-amount shifts in control_step (−20 B),
-    // flight_seam (−164 B) and flight_seam_flat (−168 B) fold back to the
-    // immediate form — byte-shapes the corpus had BEFORE the #682 mask, now
-    // with the mask soundly kept for every unproven amount. Flipping
-    // default-on is a deliberate byte-changing refreeze (all differentials
-    // re-run on the new bytes, goldens re-pinned) owned by the maintainer.
-    let arm_instrs = if std::env::var("SYNTH_SHIFT_MASK_ELIDE").is_ok_and(|v| v != "0") {
+    // DEFAULT-ON since v0.50.1 (opt-out via `SYNTH_SHIFT_MASK_ELIDE=0`; #846).
+    // gale's gpio-thin driver regressed +44 B / +9% on synth 0.49 — its pin
+    // bit-arithmetic (`pin & 31` then a register shift) emits the source
+    // `and rN,#0x1f` IMMEDIATELY followed by the #682 mod-32 re-mask
+    // `and r12,rN,#0x1f`; the second is provably redundant (Pattern B: an
+    // operand produced by `and X,#c`, c<32, is already in [0,31]), so the
+    // pass drops it. Flipping default-on is a deliberate byte-changing
+    // refreeze: the elision also moves the frozen anchors (const-amount
+    // shifts fold back to the immediate form) — control_step −20 B,
+    // flight_seam −166 B, flight_seam_flat −168 B — all size DECREASES with
+    // the mask soundly kept for every unproven amount. All differentials were
+    // re-run on the new bytes and the goldens re-pinned (see #846 PR /
+    // `frozen_codegen_bytes.rs`). `SYNTH_SHIFT_MASK_ELIDE=0` restores the
+    // pre-flip bytes (opt-out gate in `shift_mask_elide_686.rs`).
+    let arm_instrs = if std::env::var("SYNTH_SHIFT_MASK_ELIDE").is_ok_and(|v| v == "0") {
+        arm_instrs
+    } else {
         let (out, elisions) = synth_synthesis::liveness::elide_shift_masks(&arm_instrs);
         if std::env::var("SYNTH_FUSE_STATS").is_ok() {
             eprintln!(
                 "[shift-mask-elide] {elisions} provably-<32 shift-amount mask(s) elided (#686)"
             );
         }
         out
-    } else {
-        arm_instrs
     };
 
     // VCR-RA uxth/uxtb fold (#428, #242): `movw rM,#0xffff; and rD,rN,rM` →

crates/synth-cli/Cargo.toml

@@ -58,23 +58,23 @@ exports_only_275_probe = []
 # 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.50.0" }
-synth-frontend = { path = "../synth-frontend", version = "0.50.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.50.0" }
-synth-backend = { path = "../synth-backend", version = "0.50.0" }
+synth-core = { path = "../synth-core", version = "0.50.1" }
+synth-frontend = { path = "../synth-frontend", version = "0.50.1" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.50.1" }
+synth-backend = { path = "../synth-backend", version = "0.50.1" }
 
 # AArch64 host-native backend (#538) — small pure-Rust crate, always on.
-synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.50.0" }
+synth-backend-aarch64 = { path = "../synth-backend-aarch64", version = "0.50.1" }
 
 # Optional external backends
-synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.50.0", optional = true }
-synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.50.0", optional = true }
-synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.50.0", optional = true }
+synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.50.1", optional = true }
+synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.50.1", optional = true }
+synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.50.1", 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.50.0", optional = true, features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.50.1", optional = true, features = ["arm"] }
 
 # Optional PulseEngine WASM optimizer
 # Uncomment when loom crate is available:

crates/synth-cli/tests/fact_spec_bounds_494.rs

@@ -232,14 +232,21 @@ fn proven_slot_bound_elides_all_eight_guards_494() {
     assert_eq!(s.halfword_count("poll", UDF0), 0, "all guards elided");
 
     // The measured byte win — pinned exactly so a regression (or an
-    // improvement) shows as a required update, like the size oracle.
+    // improvement) shows as a required update, like the size oracle. These are
+    // the SHIPPED-DEFAULT sizes: SYNTH_SHIFT_MASK_ELIDE is default-on since
+    // v0.50.1 (#846), so the elision also trims the poll fixture — 6 B off the
+    // guarded build (232->226) and 10 B off the specialized one (104->94). The
+    // guard-elision win itself is unchanged (still 8 guards x 16 B = 128 B; see
+    // the UDF census 16->0 above); the elision just shaves 4 B MORE off the
+    // specialized build, so the measured delta is 128 + 4 = 132.
     let (b_len, s_len) = (b.func("poll").len(), s.func("poll").len());
-    assert_eq!(b_len, 232, "baseline poll size drifted");
-    assert_eq!(s_len, 104, "specialized poll size drifted");
+    assert_eq!(b_len, 226, "baseline poll size drifted");
+    assert_eq!(s_len, 94, "specialized poll size drifted");
     assert_eq!(
         b_len - s_len,
-        128,
-        "8 guards x 16 B (#752 shape: SUB.W+CMP+BHS+UDF+CMP+BLS+UDF)"
+        132,
+        "128 B guard elision (8 guards x 16 B, #752 SUB.W+CMP+BHS+UDF+CMP+BLS+UDF) \
+         + 4 B shift-mask elision on the specialized poll (#846, default-on)"
     );
 
     // Certificate trail: one ADMIT per access, naming the obligation.