Ordeal

^{A certificate-checked QF_BV SMT solver for the PulseEngine toolchain}

 

 

Meld · Loom · Synth · Ordeal · Kiln · Sigil

 

Ordeal answers one kind of question: are these two bit-vector computations the same for every input? It is the solver that loom and synth use to check that a WebAssembly optimisation or an ARM lowering does not change behaviour.

What makes it different from asking Z3: you don't have to trust ordeal's answer.

• "Equivalent" (UNSAT) comes with a proof certificate.
• "Different" (SAT) comes with a counterexample and a satisfying assignment.

Both are re-checked by a small checker whose soundness is machine-checked in Lean 4. The solver itself is untrusted.

Pure Rust, no external dependencies, and it runs as a wasm32-wasip2 component as well as natively.

Get ordeal

Pick the path that matches how you work:

You are…	Use
Using the PulseEngine toolchain	the varve layer (below)
Calling it from Rust	cargo add ordeal
Wanting the command-line tool	cargo install ordeal, or a release binary
Building with Bazel	rules_ordeal

varve. varve installs the whole PulseEngine toolchain as one pinned, signed layer. Ordeal is one of the tools in it. With a varve.toml pinning a layer (see varve's Getting started):

varve install && varve shim install   # then: . "$HOME/.varve/env"
ordeal --version                      # dispatched from the pinned layer

Release binaries. Each release ships archives for Linux (glibc and static musl, x86_64 and aarch64) and macOS. SHA256SUMS.txt is cosign-signed, and a CycloneDX SBOM and VEX are listed in it:

gh release download --repo pulseengine/ordeal -p 'ordeal-*-x86_64-unknown-linux-musl.tar.gz' -p 'SHA256SUMS.txt*'
cosign verify-blob --bundle SHA256SUMS.txt.cosign.bundle \
  --certificate-identity-regexp '^https://github\.com/pulseengine/ordeal/\.github/workflows/release\.yml@' \
  --certificate-oidc-issuer https://token.actions.githubusercontent.com SHA256SUMS.txt
sha256sum -c --ignore-missing SHA256SUMS.txt   # macOS: shasum -a 256 -c …

Quick start

Command line

Ordeal reads SMT-LIB2 (the QF_BV subset). Is x + x the same as x << 1? Assert that they differ and ask. unsat means no difference exists:

$ printf '(declare-const x (_ BitVec 32))
(assert (distinct (bvadd x x) (bvshl x #x00000001)))
(check-sat)' | ordeal check -
unsat
; unsat certificate: 10 bytes of checker-validated LRAT

A satisfiable query prints the model:

$ echo '(declare-const x (_ BitVec 32))(assert (= x #x0000002a))(check-sat)' | ordeal check -
sat
((x #x0000002a))

--format json prints one JSON object per query. It carries the full evidence for either answer:

• the CNF and LRAT proof for unsat;
• the satisfying assignment, with its bit map and hashes, for sat.

Anyone can re-check that object without trusting the ordeal binary.

Rust

use ordeal::{BvTerm, CheckResult, Solver, Sort};

// Is x * 2 the same as x << 1 for every 32-bit x?
let x = || Box::new(BvTerm::Var { name: "x".into(), sort: Sort::new(32) });
let c = |v| Box::new(BvTerm::Const { value: v, sort: Sort::new(32) });

match Solver::prove_equiv(BvTerm::Mul(x(), c(2)), BvTerm::Shl(x(), c(1))) {
    CheckResult::Unsat(cert) => {
        // Equivalent. recheck() re-validates the proof with the trusted checker.
        cert.recheck().expect("certificate re-checks");
    }
    CheckResult::Sat(model) => println!("differ, e.g. at {:?}", model.assignments),
    CheckResult::Unknown => { /* no claim: never treat as equivalent */ }
}

The same program, runnable: examples/quickstart.rs (cargo run -p ordeal --example quickstart). CI runs it on every change. For the SAT witness, resource-bounded checks and more patterns, see docs/consuming-ordeal.md.

What it decides

A deliberately closed fragment of QF_BV, bit-widths 1 to 128 (SMT-LIB names):

• arithmetic: bvadd bvsub bvmul bvudiv bvurem, plus bvneg bvsdiv bvsrem (lowered into the core ops)
• bitwise: bvand bvor bvxor bvnot
• shifts and rotation: bvshl bvlshr bvashr rotate_right rotate_left
• structure: extract concat zero_extend sign_extend ite
• comparisons: = distinct bvult bvule bvugt bvuge bvslt bvsle bvsgt bvsge
• the Boolean connectives not and or

There is also a small preprocessed layer for byte arrays (select/store) and uninterpreted pure calls.

Anything else is rejected as unsupported; ordeal never guesses. Not planned: quantifiers, floating point, optimisation, incremental push/pop. Unknown is always a possible answer (for example on a resource limit), and callers must treat it as "no claim".

Why you can trust an answer

formula → bit-blast → AIG → CNF → SAT solver ──unsat──▶ LRAT proof ─┐
                                              └──sat───▶ assignment ─┤
                                                                     ▼
                                                   ordeal-lrat checker (trusted)

Only ordeal-lrat is trusted. It is a small, dependency-free crate. The Rust source is translated to Lean 4 with Aeneas and proven sound: an accepted proof means the formula really is unsatisfiable, and an accepted assignment really satisfies it. The bit-blasting rules are proven against Lean's BitVec semantics too. CI regenerates the Lean model from the Rust source before every proof build, so the proof cannot drift from the code.

A bug anywhere else can make ordeal fail to answer, but cannot make a wrong answer pass the checker. Details and exact scope: docs/formal-verification.md.

Documentation

docs/consuming-ordeal.md	Using ordeal from a tool: API patterns, SAT witness, SBOM/VEX
ARCHITECTURE.md	The pipeline and the trust boundary
docs/formal-verification.md	What is proven, how, and what is not
CHANGELOG.md	What changed in each release
ROADMAP.md	How the plan is tracked (rivet)

Building from source:

cargo build && cargo test
cargo build --target wasm32-wasip2 --release   # the WebAssembly component

The Z3 cross-check used in development is behind the off-by-default oracle feature.

The PulseEngine tools ordeal's own workflow uses (rivet) are pinned as a varve layer in varve.toml: varve install gives you exactly the versions CI and the release job use.

Part of PulseEngine

Project	Role
Loom	WASM optimizer with SMT verification
Synth	WASM-to-ARM AOT compiler with Rocq proofs
Ordeal	Certificate-checked QF_BV SMT solver
Meld	WASM Component Model static fuser
Kiln	WASM runtime for safety-critical systems
Sigil	Supply chain attestation and signing
varve	Toolchain layer manager: pinned, signed bundles of the tools above

License

Apache-2.0. See LICENSE.

---

_{Part of PulseEngine — WebAssembly toolchain for safety-critical systems}