From 36952faa082f1cfc8518e0ecc8d002b71ab785f6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 17 Jul 2026 16:54:41 +0200 Subject: [PATCH] =?UTF-8?q?chore(release):=20v0.49.0=20=E2=80=94=20phase-2?= =?UTF-8?q?=20frontier=20+=20falcon=20to=20zero=20(7-lane=20hub)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Wave 1 (real-module + soundness): #782 ARM32 i64 trunc_sat (falcon skip 4→0), #761 self-contained R9/linmem silent-alias fix (SOUNDNESS), WCET ph4 bounded recursion (#778), #77 space-consistency + #80 async error-context.drop gate. Wave 2 (verified core): VCR-RA-003 ph2 whole-function allocation validator (across-CALL + across-JOIN), VCR-WASM-001 i64 batch (Rocq 536→585 Qed), cross-backend op-parity gate (#223/#232, 16 silent gaps surfaced). Plus the ci.yml strict-YAML fix. Pin sweep 0.48.0→0.49.0; status.json/FEATURE_MATRIX regenerated; 25/25 claims; frozen 10/10. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 2 +- CHANGELOG.md | 91 +++++++++++++++++++++++++ Cargo.lock | 36 +++++----- Cargo.toml | 2 +- MODULE.bazel | 2 +- artifacts/status.json | 2 +- crates/synth-backend-aarch64/Cargo.toml | 2 +- crates/synth-backend-awsm/Cargo.toml | 2 +- crates/synth-backend-riscv/Cargo.toml | 4 +- crates/synth-backend-wasker/Cargo.toml | 2 +- crates/synth-backend/Cargo.toml | 6 +- crates/synth-cli/Cargo.toml | 18 ++--- crates/synth-frontend/Cargo.toml | 2 +- crates/synth-opt/Cargo.toml | 2 +- crates/synth-synthesis/Cargo.toml | 6 +- crates/synth-verify/Cargo.toml | 8 +-- docs/status/FEATURE_MATRIX.md | 2 +- npm/package.json | 2 +- 18 files changed, 141 insertions(+), 50 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f003e312..7235d36c 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/CHANGELOG.md b/CHANGELOG.md index 2241df04..0d19e5c6 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/Cargo.lock b/Cargo.lock index 2f222435..3521e297 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1100,14 +1100,14 @@ dependencies = [ [[package]] name = "synth-abi" -version = "0.48.0" +version = "0.49.0" dependencies = [ "synth-wit", ] [[package]] name = "synth-analysis" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "synth-core", @@ -1116,7 +1116,7 @@ dependencies = [ [[package]] name = "synth-backend" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "synth-core", @@ -1127,7 +1127,7 @@ dependencies = [ [[package]] name = "synth-backend-aarch64" -version = "0.48.0" +version = "0.49.0" dependencies = [ "synth-core", "thiserror", @@ -1136,7 +1136,7 @@ dependencies = [ [[package]] name = "synth-backend-awsm" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "synth-core", @@ -1145,7 +1145,7 @@ dependencies = [ [[package]] name = "synth-backend-riscv" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "proptest", @@ -1157,7 +1157,7 @@ dependencies = [ [[package]] name = "synth-backend-wasker" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "synth-core", @@ -1166,11 +1166,11 @@ dependencies = [ [[package]] name = "synth-cfg" -version = "0.48.0" +version = "0.49.0" [[package]] name = "synth-cli" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "clap", @@ -1197,7 +1197,7 @@ dependencies = [ [[package]] name = "synth-core" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "gimli", @@ -1212,7 +1212,7 @@ dependencies = [ [[package]] name = "synth-frontend" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "synth-core", @@ -1226,14 +1226,14 @@ dependencies = [ [[package]] name = "synth-memory" -version = "0.48.0" +version = "0.49.0" dependencies = [ "bitflags", ] [[package]] name = "synth-opt" -version = "0.48.0" +version = "0.49.0" dependencies = [ "criterion", "synth-cfg", @@ -1241,11 +1241,11 @@ dependencies = [ [[package]] name = "synth-qemu" -version = "0.48.0" +version = "0.49.0" [[package]] name = "synth-synthesis" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "proptest", @@ -1260,7 +1260,7 @@ dependencies = [ [[package]] name = "synth-test" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "clap", @@ -1276,7 +1276,7 @@ dependencies = [ [[package]] name = "synth-verify" -version = "0.48.0" +version = "0.49.0" dependencies = [ "anyhow", "chrono", @@ -1295,7 +1295,7 @@ dependencies = [ [[package]] name = "synth-wit" -version = "0.48.0" +version = "0.49.0" [[package]] name = "tempfile" diff --git a/Cargo.toml b/Cargo.toml index 3855984a..626d18d0 100644 --- a/Cargo.toml +++ b/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"] diff --git a/MODULE.bazel b/MODULE.bazel index c03eff87..27abc426 100644 --- a/MODULE.bazel +++ b/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 diff --git a/artifacts/status.json b/artifacts/status.json index 3748229d..9c5c3820 100644 --- a/artifacts/status.json +++ b/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 } diff --git a/crates/synth-backend-aarch64/Cargo.toml b/crates/synth-backend-aarch64/Cargo.toml index 470e8d2b..1ff337b1 100644 --- a/crates/synth-backend-aarch64/Cargo.toml +++ b/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 diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml index 94b561c8..751db645 100644 --- a/crates/synth-backend-awsm/Cargo.toml +++ b/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 diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml index e942c685..eb6f75a9 100644 --- a/crates/synth-backend-riscv/Cargo.toml +++ b/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 diff --git a/crates/synth-backend-wasker/Cargo.toml b/crates/synth-backend-wasker/Cargo.toml index 4d921786..5c37c408 100644 --- a/crates/synth-backend-wasker/Cargo.toml +++ b/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 diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml index c88298bc..3099329a 100644 --- a/crates/synth-backend/Cargo.toml +++ b/crates/synth-backend/Cargo.toml @@ -15,8 +15,8 @@ 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 @@ -24,4 +24,4 @@ thiserror.workspace = true # #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"] } diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index 09e0853d..ba5d4eee 100644 --- a/crates/synth-cli/Cargo.toml +++ b/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: diff --git a/crates/synth-frontend/Cargo.toml b/crates/synth-frontend/Cargo.toml index c3649ed3..16b7ec3e 100644 --- a/crates/synth-frontend/Cargo.toml +++ b/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 diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml index 7aca5b44..87859d1a 100644 --- a/crates/synth-opt/Cargo.toml +++ b/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"] } diff --git a/crates/synth-synthesis/Cargo.toml b/crates/synth-synthesis/Cargo.toml index c9dfb24b..97919067 100644 --- a/crates/synth-synthesis/Cargo.toml +++ b/crates/synth-synthesis/Cargo.toml @@ -11,9 +11,9 @@ categories.workspace = true description = "WASM-to-ARM instruction selection and peephole optimizer" [dependencies] -synth-core = { path = "../synth-core", version = "0.48.0" } -synth-cfg = { path = "../synth-cfg", version = "0.48.0" } -synth-opt = { path = "../synth-opt", version = "0.48.0" } +synth-core = { path = "../synth-core", version = "0.49.0" } +synth-cfg = { path = "../synth-cfg", version = "0.49.0" } +synth-opt = { path = "../synth-opt", version = "0.49.0" } serde.workspace = true anyhow.workspace = true thiserror.workspace = true diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml index 8857bcc7..c2add190 100644 --- a/crates/synth-verify/Cargo.toml +++ b/crates/synth-verify/Cargo.toml @@ -22,12 +22,12 @@ arm = ["synth-synthesis"] [dependencies] # Core dependencies (always required) -synth-core = { path = "../synth-core", version = "0.48.0" } -synth-cfg = { path = "../synth-cfg", version = "0.48.0" } -synth-opt = { path = "../synth-opt", version = "0.48.0" } +synth-core = { path = "../synth-core", version = "0.49.0" } +synth-cfg = { path = "../synth-cfg", version = "0.49.0" } +synth-opt = { path = "../synth-opt", version = "0.49.0" } # ARM synthesis (optional, behind 'arm' feature) -synth-synthesis = { path = "../synth-synthesis", version = "0.48.0", optional = true } +synth-synthesis = { path = "../synth-synthesis", version = "0.49.0", optional = true } # Default SMT engine: pure-Rust, certificate-checked QF_BV solver (#553). # 0.9 adds the `ordeal::trap` module (trap-preservation VCs, VCR-VER-002 / #166); diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index 2c77cc15..c149678b 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -7,7 +7,7 @@ > stale. All numbers come from [`artifacts/status.json`](../../artifacts/status.json), > which is re-derived from source on every run — never hand-edited. -**Workspace version:** 0.48.0 +**Workspace version:** 0.49.0 --- diff --git a/npm/package.json b/npm/package.json index ccda301d..6d01a9d6 100644 --- a/npm/package.json +++ b/npm/package.json @@ -1,6 +1,6 @@ { "name": "@pulseengine/synth", - "version": "0.48.0", + "version": "0.49.0", "description": "synth — a WebAssembly-to-ARM/RISC-V/AArch64 compiler with mechanized correctness proofs. Produces bare-metal ELF binaries for embedded targets.", "bin": { "synth": "./run.js"