chore(release): v0.8.0 — honest i64 verification foundation

CHANGELOG.md

@@ -7,20 +7,104 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.8.0] - 2026-05-26
+
+**Theme: honest i64 verification foundation.**
+
+v0.8.0 was originally scoped as "i64 T1 result-correspondence parity"
+(umbrella issue #147). A clean-room check of the first foundation PR
+(#149) surfaced that `coq/Synth/Synth/Compilation.v` modeled i64 ops
+as single 32-bit ARM instructions (e.g., `I64Add → [ADD R0 R0 R1]`,
+inline comment: *"Simplified: just add low 32 bits"*) while the real
+Rust compiler at `crates/synth-synthesis/src/instruction_selector.rs:1450`
+emits proper register-pair sequences (`ADDS R0,R0,R2; ADC R1,R1,R3`).
+The umbrella's own falsification clause forbade shipping T1 proofs
+that "prove a different operation than the compiler emits."
+
+Rather than overclaim or paper over the gap, v0.8.0 ships the
+**aligned model + proof tooling** layer, and the actual T2→T1
+promotions become v0.9.0's theme. This is a smaller user-visible
+delta but a much bigger verification-soundness delta: the existing
+i64 proofs now reason about the operation the compiler actually
+emits, instead of a degenerate 32-bit slice of it.
+
+**Falsification statement.** v0.8.0 is wrong if (a) the aligned
+`Compilation.v` clauses do not match what the Rust compiler emits
+(cross-checked against the per-op survey in
+[`docs/analysis/I64_CODEGEN_SURVEY.md`](docs/analysis/I64_CODEGEN_SURVEY.md)),
+(b) `bazel test //coq:verify_proofs` goes red on a clean v0.8.0
+checkout, or (c) any of the 5 strategically-`Admitted` i64 theorems
+(4 div/rem + 1 i64_const) are claimed to be Qed anywhere in the
+release artifacts.
+
+### Changed
+- **`coq/Synth/Synth/Compilation.v` aligned with real Rust i64 codegen** (PR #150).
+  28 i64 op clauses updated: I64Add/Sub now emit `ADDS R0,R0,R2; ADC R1,R1,R3`
+  (and SUBS/SBC); I64And/Or/Xor emit parallel lo/hi binops; i64 comparison ops
+  emit a single `I64SetCond[Z]` pseudo-op; div/rem/mul/shifts/rotates/bit-manip
+  emit ArmOp::I64* pseudo-ops mirroring the Rust ArmOp variants. ArmSemantics.v
+  gains the real ADDS/ADC/SUBS/SBC instructions plus ~25 axiomatized result
+  functions for the pseudo-ops (parallel to how VFP is axiomatized).
+  Per-op cross-check against the Rust source is documented in
+  [`docs/analysis/I64_CODEGEN_SURVEY.md`](docs/analysis/I64_CODEGEN_SURVEY.md).
+- ~36 existence-only (T2) i64 proofs re-proved against the aligned model
+  using the existing `solve_single_arm` / `solve_cmp_mov` / `solve_mem_single`
+  tactics. **Net: previously had 29 i64 theorems Qed against a model that
+  proved the wrong operation; now has 36 i64 theorems Qed against the
+  correct model, plus 5 strategically-Admitted theorems pending the
+  v0.9.0 lift queue.**
+
+### Added
+- **Proof tooling for i64 T1 lifts** (PR #149). Three new tactics in
+  `coq/Synth/Synth/Tactics.v`: `synth_binop_proof_i64`,
+  `synth_cmp_binop_proof_i64`, and `synth_cmp_unop_proof_i64`. Eleven
+  new i64 flag-correspondence lemmas in `coq/Synth/ARM/ArmFlagLemmas.v`
+  (`z_flag_sub_eq_i64`, `flags_ne_i64`, `nv_flag_sub_lts_i64`,
+  `flags_ltu_i64`, `flags_ges_i64`, `flags_geu_i64`, `flags_gts_i64`,
+  `flags_gtu_i64`, `flags_les_i64`, `flags_leu_i64`,
+  `z_flag_sub_eqz_i64`), plus 14 supporting boundedness helpers. All
+  proofs Qed; 0 Admitted in #149's diff. These are the infrastructure
+  the v0.9.0 lift PRs will consume.
+
 ### Documentation
-- **Architectural finding: ARMv7-M FPv5 has no F64↔I64 VCVT.** The four
-  WASM ops `F64ConvertI64S/U` and `I64TruncF64S/U` listed under v0.7.0's
-  "Deferred to follow-up" cannot be implemented as single-instruction
-  VCVTs on Cortex-M7DP — the 64-bit integer ↔ floating-point VCVT
-  encodings are ARMv8-A FEAT_FP only, not present in M-profile FPv5-D16
-  (Cortex-M7DP, M33-DP, M55, M85). Closing these properly requires a
-  multi-instruction software sequence (or a soft-float helper) plus
-  WASM-trap integration for the trunc family, plus matching Rocq
-  proofs — out of scope for v0.8.0's i64-T1-promotion theme. Deferred
-  to a later floating-point milestone. Full analysis in
-  [`docs/analysis/ARMV7M_F64_I64_VCVT_FINDING.md`](docs/analysis/ARMV7M_F64_I64_VCVT_FINDING.md).
-  The selector continues to surface a typed `Error::Synthesis` for
-  these ops; no behavior change vs. v0.7.0.
+- **Architectural finding: ARMv7-M FPv5 has no F64↔I64 VCVT** (PR #148).
+  The four WASM ops `F64ConvertI64S/U` and `I64TruncF64S/U` listed under
+  v0.7.0's "Deferred to follow-up" cannot be implemented as
+  single-instruction VCVTs on Cortex-M7DP — the 64-bit integer ↔
+  floating-point VCVT encodings are ARMv8-A FEAT_FP only, not present
+  in M-profile FPv5-D16. Closing these requires a multi-instruction
+  software sequence plus WASM-trap integration plus matching Rocq
+  proofs — deferred to a later floating-point milestone. Full analysis
+  in [`docs/analysis/ARMV7M_F64_I64_VCVT_FINDING.md`](docs/analysis/ARMV7M_F64_I64_VCVT_FINDING.md).
+  Selector continues to surface a typed `Error::Synthesis`; no
+  behavior change vs. v0.7.0.
+- **I64 codegen survey** at [`docs/analysis/I64_CODEGEN_SURVEY.md`](docs/analysis/I64_CODEGEN_SURVEY.md):
+  per-op extraction of what the Rust compiler emits for every i64 WASM
+  op, with line citations into `instruction_selector.rs`. Reviewers
+  audit Compilation.v against the Rust source mechanically using this
+  file.
+
+### Fixed
+- **Bazel rocq_library dep wiring**. `rules_rocq_rust` requires every
+  `Require Import Synth.X.Y.` in a `.v` file to be matched by a
+  corresponding `:y` target in the library's `deps` list — transitive
+  deps through intermediate targets do **not** propagate the `-Q`
+  flags to `coqc`. Synth's `:arm_instructions`, `:arm_semantics`,
+  `:compilation`, `:tactics`, and `:correctness_*` rocq_libraries were
+  relying on transitive resolution that happened to work on main only
+  because cached `.vo` files masked the missing flags. PR #150's
+  alignment changes broke the happy accident; the deps are now
+  explicit (matches the pattern in
+  `pulseengine/loom/proofs/BUILD.bazel`).
+
+### Deferred to v0.9.0
+- **i64 T1 result-correspondence promotions.** The original umbrella's
+  scope: 30 T2 → T1 lifts (arithmetic, bitwise, shifts/rotates,
+  comparisons, bit-manip) plus discharging the 5 admits #150 introduced
+  (4 div/rem T1 + 1 i64_const T1). These now ride into v0.9.0 as the
+  primary theme, against the now-aligned model. Tracked in #147.
+- F64↔I64 conversion implementations (see Documentation section).
+- F32DemoteF64 (deferred from v0.7.0).
 
 ## [0.7.0] - 2026-05-25
 

Cargo.toml

@@ -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.7.0"
+version = "0.8.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.7.0",
+    version = "0.8.0",
 )
 
 # Bazel dependencies

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.7.0" }
+synth-core = { path = "../synth-core", version = "0.8.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.7.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.7.0" }
+synth-core = { path = "../synth-core", version = "0.8.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.8.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.7.0" }
+synth-core = { path = "../synth-core", version = "0.8.0" }
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-backend/Cargo.toml

@@ -15,7 +15,7 @@ default = ["arm-cortex-m"]
 arm-cortex-m = ["synth-synthesis"]
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.7.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.7.0", optional = true }
+synth-core = { path = "../synth-core", version = "0.8.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.8.0", optional = true }
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-cli/Cargo.toml

@@ -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.7.0" }
-synth-frontend = { path = "../synth-frontend", version = "0.7.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.7.0" }
-synth-backend = { path = "../synth-backend", version = "0.7.0" }
+synth-core = { path = "../synth-core", version = "0.8.0" }
+synth-frontend = { path = "../synth-frontend", version = "0.8.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.8.0" }
+synth-backend = { path = "../synth-backend", version = "0.8.0" }
 
 # Optional external backends
-synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.7.0", optional = true }
-synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.7.0", optional = true }
-synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.7.0", optional = true }
+synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.8.0", optional = true }
+synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.8.0", optional = true }
+synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.8.0", optional = true }
 
 # Optional verification (requires z3)
-synth-verify = { path = "../synth-verify", version = "0.7.0", optional = true, features = ["z3-solver", "arm"] }
+synth-verify = { path = "../synth-verify", version = "0.8.0", optional = true, features = ["z3-solver", "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.7.0" }
+synth-core = { path = "../synth-core", version = "0.8.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.7.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.8.0" }
 
 [dev-dependencies]
 criterion = { version = "0.5", features = ["html_reports"] }

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.7.0" }
-synth-cfg = { path = "../synth-cfg", version = "0.7.0" }
-synth-opt = { path = "../synth-opt", version = "0.7.0" }
+synth-core = { path = "../synth-core", version = "0.8.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.8.0" }
+synth-opt = { path = "../synth-opt", version = "0.8.0" }
 serde.workspace = true
 anyhow.workspace = true
 thiserror.workspace = true

crates/synth-verify/Cargo.toml

@@ -17,12 +17,12 @@ arm = ["synth-synthesis"]
 
 [dependencies]
 # Core dependencies (always required)
-synth-core = { path = "../synth-core", version = "0.7.0" }
-synth-cfg = { path = "../synth-cfg", version = "0.7.0" }
-synth-opt = { path = "../synth-opt", version = "0.7.0" }
+synth-core = { path = "../synth-core", version = "0.8.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.8.0" }
+synth-opt = { path = "../synth-opt", version = "0.8.0" }
 
 # ARM synthesis (optional, behind 'arm' feature)
-synth-synthesis = { path = "../synth-synthesis", version = "0.7.0", optional = true }
+synth-synthesis = { path = "../synth-synthesis", version = "0.8.0", optional = true }
 
 # SMT solver for formal verification
 z3 = { version = "0.19", features = ["static-link-z3"], optional = true }