pulseengine · avrabe · Jul 23, 2026 · Jul 23, 2026
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -7,6 +7,30 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.16.1] - 2026-07-23
+
+**Patch: the unsigned twin of #97** (issue #101, synth). v0.16.0 fixed the
+derived `bvsrem` lowering; direct users of the native `BvTerm::Urem` enum
+still hit the restoring divider's remainder, so a urem-vs-multiplicative VC
+stayed exponential (synth's `verify_i32_rem_u`: over 7 m 48 s, killed).
+
+### Fixed
+- **The native `Urem` blast rule is multiplicative**: `a − (a udiv b)·b` at
+  the circuit level — exact for all inputs including /0 with no special case
+  (`a udiv 0` is all-ones; `all-ones · 0 = 0`). Measured on synth's VC shape:
+  over 7 m 48 s → **UNSAT in 5.2 ms**. The term-level op stays native.
+- **The Lean proof moved with the encoding**: `blast_urem_bitvec` re-proven
+  against the new composition, same headline (`denotes A % B`, all widths),
+  via the new `umod_eq_sub_smtUDiv_mul` identity (all divisors, including 0).
+  The capstone's proof-coupling held: the encoding change broke exactly the
+  changed rule's proof, and shipped only re-proven.
+- #101 regression guard added beside the #97 one (the VC shape under a 10 s
+  deadline, ~2000x headroom).
+
+### Falsification
+Wrong if: either VC-shape guard (#97 signed, #101 unsigned) exceeds its
+deadline; or any `Blaster*.lean` theorem acquires a `sorry` (CI budget).
+
 ## [0.16.0] - 2026-07-23
 
 **The #97 regression fix + migration ergonomics** (TR-029, issues #97/#71/#57).

diff --git a/Cargo.toml b/Cargo.toml
@@ -3,7 +3,7 @@ resolver = "2"
 members = ["crates/ordeal", "crates/ordeal-lrat"]
 
 [workspace.package]
-version = "0.16.0"
+version = "0.16.1"
 edition = "2024"
 license = "Apache-2.0"
 repository = "https://github.com/pulseengine/ordeal"

diff --git a/README.md b/README.md
@@ -31,7 +31,7 @@
 
 Ordeal (meaning "verdict / judgment") is a specialized, **certificate-checked** QF_BV SMT solver. It decides bitvector equivalence and satisfiability queries for the [PulseEngine](https://github.com/pulseengine) toolchain — specifically the queries that [loom](https://github.com/pulseengine/loom) (verified WASM optimizer) and [synth](https://github.com/pulseengine/synth) (verified WASM→ARM codegen) actually emit.
 
-**Status (v0.16.0, on [crates.io](https://crates.io/crates/ordeal)).** The engine is live: the full bit-blast → AIG → Tseitin CNF → pure-Rust CDCL → LRAT pipeline decides the closed QF_BV fragment, with a semantics-preserving canonicalization pass (commutative-operand ordering + const-folding, v0.8.0) that collapses structural-equivalence cliffs — e.g. `mul(a,b) ≢ mul(b,a)` @ 32, which went from not-finishing-in-590s to an instant certified UNSAT. A `trap` module (v0.9.0) expresses each partial WASM op's trap condition (`div`/`rem` ÷0 + overflow, OOB `load`/`store`, `call_indirect`, `unreachable`) as a QF_BV predicate and composes trap-preservation VCs, so consumers verify **trap**-equivalence and catch a transformation that drops a trap — classification of bits only, no floating-point. A `layout` module (v0.10.0) splits and reassembles little-endian bytes as pure `extract`/`concat`, so a wire-codec round-trip or an AADL↔WIT↔ABI record layout is one certificate-checked `prove_equiv` call; and `bvurem` is native, which makes the whole `bvudiv`/`bvurem`/`bvsdiv`/`bvsrem` family multiplier-free. `Sat` verdicts carry a self-checked counterexample model; `Unsat` verdicts carry an LRAT certificate that the `ordeal-lrat` checker validated before the verdict was returned — and as of v0.7.0 that `Certificate` carries the refuted CNF too (`cert.cnf` + `cert.lrat`), so a consumer can **independently re-check it** with `cert.recheck()` and re-establish UNSAT with zero trust in the solver; `Unknown` stays conservative (never optimize on it). The array/UF sliver (`Solver::check_sliver`), a bool→BV `ite` bridge, derived-op lowering helpers, a resource-bounded `check_with_limit`, and a one-call layout-equivalence oracle (`Solver::prove_equiv`, for spar's codegen checks) are all available. A minimal SMT-LIB2 front-end (`ordeal check foo.smt2`) reads the QF_BV subset loom/synth emit. The array sliver now resolves **symbolic** BV32 indices for `select`/`store` (v0.11.0, a sound read-over-write reduced into the closed fragment), which unblocks loom's verifier migration off Z3. And `ordeal verus <verus --log-all dir>` (v0.12.0) discharges the `by (bit_vector)` obligations **Verus itself emits** — all 62 of gale's, each with a re-checkable LRAT certificate — turning unchecked-Z3 ASIL-D evidence into the CompCert argument, with no hand transcription in the loop. The checker's soundness is now **machine-checked in Lean 4** (Rust → Aeneas → `kernel.spec.lrat_check_sound`, issue #12): if it accepts, the CNF is unsatisfiable — zero `sorry`, no `sorryAx`. The solver stays untrusted; only the now-proven, dependency-free checker is trusted. Each bit-blasting rule is additionally Kani-proven equal to its concrete reference semantics for all inputs (v0.6.0), so the blaster's soundness no longer leans on the Z3 differential. As of v0.5.1 the model↔code drift gap is closed: the committed Lean model is verified (via the real Charon+Aeneas toolchain, CI-guarded) to be the current translation of the shipped `kernel.rs`. Precise scope and trust boundary: [docs/formal-verification.md](docs/formal-verification.md).
+**Status (v0.16.1, on [crates.io](https://crates.io/crates/ordeal)).** The engine is live: the full bit-blast → AIG → Tseitin CNF → pure-Rust CDCL → LRAT pipeline decides the closed QF_BV fragment, with a semantics-preserving canonicalization pass (commutative-operand ordering + const-folding, v0.8.0) that collapses structural-equivalence cliffs — e.g. `mul(a,b) ≢ mul(b,a)` @ 32, which went from not-finishing-in-590s to an instant certified UNSAT. A `trap` module (v0.9.0) expresses each partial WASM op's trap condition (`div`/`rem` ÷0 + overflow, OOB `load`/`store`, `call_indirect`, `unreachable`) as a QF_BV predicate and composes trap-preservation VCs, so consumers verify **trap**-equivalence and catch a transformation that drops a trap — classification of bits only, no floating-point. A `layout` module (v0.10.0) splits and reassembles little-endian bytes as pure `extract`/`concat`, so a wire-codec round-trip or an AADL↔WIT↔ABI record layout is one certificate-checked `prove_equiv` call; and `bvurem` is native, which makes the whole `bvudiv`/`bvurem`/`bvsdiv`/`bvsrem` family multiplier-free. `Sat` verdicts carry a self-checked counterexample model; `Unsat` verdicts carry an LRAT certificate that the `ordeal-lrat` checker validated before the verdict was returned — and as of v0.7.0 that `Certificate` carries the refuted CNF too (`cert.cnf` + `cert.lrat`), so a consumer can **independently re-check it** with `cert.recheck()` and re-establish UNSAT with zero trust in the solver; `Unknown` stays conservative (never optimize on it). The array/UF sliver (`Solver::check_sliver`), a bool→BV `ite` bridge, derived-op lowering helpers, a resource-bounded `check_with_limit`, and a one-call layout-equivalence oracle (`Solver::prove_equiv`, for spar's codegen checks) are all available. A minimal SMT-LIB2 front-end (`ordeal check foo.smt2`) reads the QF_BV subset loom/synth emit. The array sliver now resolves **symbolic** BV32 indices for `select`/`store` (v0.11.0, a sound read-over-write reduced into the closed fragment), which unblocks loom's verifier migration off Z3. And `ordeal verus <verus --log-all dir>` (v0.12.0) discharges the `by (bit_vector)` obligations **Verus itself emits** — all 62 of gale's, each with a re-checkable LRAT certificate — turning unchecked-Z3 ASIL-D evidence into the CompCert argument, with no hand transcription in the loop. The checker's soundness is now **machine-checked in Lean 4** (Rust → Aeneas → `kernel.spec.lrat_check_sound`, issue #12): if it accepts, the CNF is unsatisfiable — zero `sorry`, no `sorryAx`. The solver stays untrusted; only the now-proven, dependency-free checker is trusted. Each bit-blasting rule is additionally Kani-proven equal to its concrete reference semantics for all inputs (v0.6.0), so the blaster's soundness no longer leans on the Z3 differential. As of v0.5.1 the model↔code drift gap is closed: the committed Lean model is verified (via the real Charon+Aeneas toolchain, CI-guarded) to be the current translation of the shipped `kernel.rs`. Precise scope and trust boundary: [docs/formal-verification.md](docs/formal-verification.md).
 
 Part of PulseEngine — a WebAssembly toolchain for safety-critical embedded systems:
 

diff --git a/crates/ordeal/Cargo.toml b/crates/ordeal/Cargo.toml
@@ -21,7 +21,7 @@ path = "src/main.rs"
 # wasip2-clean). The solver depends on the checker to validate certificates;
 # the checker never depends on the solver (the trust boundary, enforced by
 # ordeal-lrat's empty dependency table).
-ordeal-lrat = { path = "../ordeal-lrat", version = "0.16.0" }
+ordeal-lrat = { path = "../ordeal-lrat", version = "0.16.1" }
 
 [features]
 # The Z3 differential oracle. Off by default: the default build has ZERO