chore(release): v0.49.0 — phase-2 frontier + falcon to zero

.github/workflows/ci.yml

@@ -72,7 +72,7 @@ jobs:
         # Red-first unit tests (both directions of each invariant); covered by
         # `cargo test --workspace` above, run explicitly so a regression in the
         # space-consistency model is unmissable in the log.
-        run: cargo test -p synth-memory --features std space::
+        run: cargo test -p synth-memory --features std 'space::'
       - name: P3 async intrinsic honest-degradation gate (#80)
         # The #80 gate: the ONE lowered async op (error-context.drop) compiles
         # to a field-name BL call site; every declined intrinsic (error-context.new

CHANGELOG.md

@@ -7,6 +7,97 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.49.0] - 2026-07-17
+
+**"Phase-2 frontier + falcon to zero" — the verified allocation validator went
+straight-line → whole-function, the source-semantics proof base grew to 585 Qed,
+and a real self-contained silent-alias soundness bug was reproduced-first and
+fixed.** Seven lanes: four closed the real-module/soundness frontier (Wave 1),
+three deepened the verified core (Wave 2). Every lane oracle-gated red-first;
+frozen anchors byte-identical throughout.
+
+### Added
+
+- **VCR-RA-003 phase 2 (#242): the register-allocation validator is now
+  WHOLE-FUNCTION.** v0.48 bounded it to straight-line segments; this adds two
+  invariants over the whole control-flow graph, both keyed on real in-stream
+  contracts (not vacuous liveness): **across-CALL** — an AAPCS caller-saved reg
+  (R2/R3/R12) held live across a `bl`/`blx` is a `CallerSavedLiveAcrossCall`
+  violation; **across-JOIN** — a reg live-in to a control-flow join (≥2 preds)
+  must be available on every path (a forward MUST-availability fixpoint over a
+  join CFG), else `JoinValueNotAvailable`. Unconditional (default build,
+  hard-errors on a real violation); unverifiable shapes loud-flag
+  `NotAttempted` rather than false-pass. Red-first: a synthetic across-call and
+  across-join clobber are each caught naming the specific violation; 0 false
+  positives across a 130-fixture sweep (found + fixed one real would-be false
+  positive — the R11 linmem base live at a join, by seeding the reserved
+  registers). Residual: optimized-path pre-resolved numeric-branch joins and the
+  RV32/AArch64 arms loud-flag `NotAttempted` (named follow-ups).
+- **VCR-WASM-001 i64 transcription batch (#242): Rocq 536 → 585 Qed.** The i64
+  integer family (add/sub/mul/and/or/xor/shl/shr_s/shr_u/rotl/rotr/eqz + the ten
+  i64 comparisons — 22 ops) transcribed from the pinned coq9.0-wasm-2.2.0
+  WasmCert-Coq sources with line-level provenance and proven refined by
+  `exec_wasm_instr` (bazel-verified green). Still a hand transcription (the real
+  dep stays blocked on unfree CompCert until nixpkgs ships wasmcert ≥ 2.2.1); 6
+  i64 arithmetic/bitwise ops are op-level-only where `exec_wasm_instr` returns
+  `None` (named residual, no `admit`/axiom — the rotate `n=0` boundary was
+  discharged with a real bit-level proof).
+- **Cross-backend op-parity gate (VCR-SEL-005, #223/#232): 16 hidden silent
+  ARM/RV32 op-divergences surfaced and ledgered.** A universe-complete gate now
+  asserts every WASM op is either lowered by BOTH the ARM and RV32 backends or an
+  explicitly-ledgered decline on the one that lacks it — a previously-invisible
+  one-sided gap (ARM lowers X, RV32 silently declines X) now fails CI. Enumeration
+  surfaced 16 gaps beyond the known 5 Zbb declines (`global.get/set`,
+  `memory.size/grow/copy/fill`, `br_table`, the nine sub-word i64 loads/stores),
+  now in a 21-entry rationale'd allowlist; floats/SIMD are structurally excluded
+  (target-parameterized). Red-first: dropping a real ledger entry makes the gate
+  report the divergence. (RV32 allocation-validator reach filed as follow-up #815.)
+- **WCET phase 4 (#778): bounded self-recursion via a verified depth-hint.** The
+  `recursion` decline is converted for the boundable case — an untrusted
+  recursion-depth hint (extending the `--wcet-hints` scry seam) is admissible only
+  if synth verifies the recursion cannot exceed it (straight-line single-entry
+  const-decrement), bounding `depth × per-frame`; otherwise the hint is REJECTED
+  (`hint-below-derived-depth` / `hint-unverifiable-recursion`) and the function
+  still declines. Unbounded/mutual/indirect recursion still LOUD-DECLINE.
+  Byte-invisible sidecar; frozen 10/10.
+- **Sound ARM32 i64 `trunc_sat` (#782): falcon skip 4 → 0.** The four ARM32
+  `i64.trunc_sat_f32/f64_{s,u}` forms (previously loud-declined) now lower as a
+  branch-free FP word-decompose — unsigned via a saturating 2^±32 split, signed
+  via an XOR-signmask conditional two's-complement negate + saturation blend
+  (no register pairs). NaN→0, out-of-range saturates to i64 MIN/MAX, never traps.
+  192,000-random-pattern fuzz bit-identical to wasmtime across ARM32 m7dp, aarch64,
+  and native arm64. (m4f i64 forms still assert-decline. The falcon fused-core's
+  own skip delta is unmeasured — the asset is unfetchable; the skip-class proxy is
+  reported instead of a fabricated number.)
+- **Platform space-consistency invariant (#77) + P3 async intrinsic gate (#80).**
+  #77: `PlatformSpaces::validate()` rejects an execution/memory-space mismatch (a
+  bare-metal core requesting an OS-mapped space; an FP-requiring space on an
+  FPU-less core), red-first. #80: `error-context.drop` lowered (scalar handle);
+  `error-context.new`/`.debug-message`/`stream`/`future`/`waitable-set`/`task`
+  loud-decline by name (the advisor narrowed the lowering to `.drop` — the others
+  take linmem message pointers and would have silently miscompiled).
+
+### Fixed
+
+- **#761 (SOUNDNESS): self-contained `--cortex-m` R9 globals base overlapped the
+  linear-memory page.** The startup placed the R9 globals table at
+  `R11_base + memory_size` while functions addressed linmem at `R11 + 0x100`, so
+  for `(memory 1)` a store to wasm offset `0xFF00` landed exactly on global slot 0
+  — a live global↔linmem alias (a unicorn boot oracle showed `0xDEADBEEF` where
+  wasmtime returns `0xABCD`), in BOTH stack layouts (disproving the issue's
+  `--stack-layout=low` guess). Reproduced-first on the real reset path, then fixed
+  by re-basing R9 above the function-visible page ceiling; guarded by a
+  non-vacuous read-back geometry validator (`validate_linmem_globals_disjoint`,
+  unconditional) whose checked base is read back from the emitted startup bytes —
+  reverting only the R9 formula makes the compile hard-error. Frozen byte-identical
+  (the R9 base lives in the self-contained startup blob, not the `.text` anchors).
+
+### Changed
+
+- **CI**: quoted the `space::` test filter in `ci.yml` — the unquoted `::`
+  tripped strict YAML parsers (PyYAML failed to load the workflow); GitHub Actions'
+  lenient parser accepted it, but any actionlint/PyYAML-based tooling choked.
+
 ## [0.48.0] - 2026-07-17
 
 **"Real modules, verified allocator" — the real falcon fused core drove the

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

artifacts/status.json

@@ -15,7 +15,7 @@
   "sel_dsl_pilot_qed": 7,
   "sel_dsl_rule_qed": 50,
   "sel_dsl_rules": 50,
-  "version": "0.48.0",
+  "version": "0.49.0",
   "verus_spec_fns": 8,
   "wasmcert_bridge_qed": 98
 }

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.48.0" }
+synth-core = { path = "../synth-core", version = "0.49.0" }
 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.48.0" }
+synth-core = { path = "../synth-core", version = "0.49.0" }
 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.48.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.48.0" }
+synth-core = { path = "../synth-core", version = "0.49.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.49.0" }
 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.48.0" }
+synth-core = { path = "../synth-core", version = "0.49.0" }
 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.48.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.48.0", optional = true }
+synth-core = { path = "../synth-core", version = "0.49.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.49.0", 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.48.0", features = ["arm"] }
+synth-verify = { path = "../synth-verify", version = "0.49.0", features = ["arm"] }

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

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.48.0" }
+synth-core = { path = "../synth-core", version = "0.49.0" }
 
 wasmparser.workspace = true
 wasm-encoder.workspace = true

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.48.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.49.0" }
 
 [dev-dependencies]
 criterion = { version = "0.8", features = ["html_reports"] }