From dc96024e821bc116750048778f1cc5547abcf190 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 23:31:07 +0200 Subject: [PATCH] =?UTF-8?q?chore(release):=20v0.16.1=20=E2=80=94=20the=20#?= =?UTF-8?q?101=20unsigned-urem=20patch?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Verifies: TR-027 Trace: skip Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1 --- CHANGELOG.md | 24 ++++++++++++++++++++++++ Cargo.toml | 2 +- README.md | 2 +- crates/ordeal/Cargo.toml | 2 +- 4 files changed, 27 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1fa5fbd..512eeac 100644 --- 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 index 7555a1e..f4c0b6f 100644 --- 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 index 4bb5b54..6f95667 100644 --- 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 ` (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 ` (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 index 70e5e24..fbcc9df 100644 --- 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