synth's requirements for a Z3 replacement — QF_BV one-shot validation; the static-link build is the real pain, not the solver

[avrabe]

Filed from synth (issue-hunt loop, not gale) in response to the "should we replace Z3?" question. These are synth's concrete requirements so an ecosystem solver decision — which loom is already partly making (#231 forwards Z3-discharged wsc.facts invariants to synth; #169 tracks Rocq gating) — is grounded in what synth actually needs.

TL;DR

synth's Z3 usage is the simplest possible SMT fragment, and the pain is the build, not the solver. Any decision should optimize for hermetic/reproducible builds and CI stability, because the solver capability is a non-issue at synth's fragment.

What synth uses Z3 for

synth-verify is a translation validator: for each lowering it asserts wasm_op_semantics ≠ arm_instruction_sequence_semantics and expects UNSAT (i.e. they're equivalent). Concretely:

• Theory: QF_BV only (quantifier-free bitvectors). Active op surface in the validator: bvadd/bvsub/bvmul/bvudiv, bvand/bvor/bvxor, bvshl/bvlshr/bvashr, bvrotr, extract/concat, zero_ext/sign_ext, and signed+unsigned comparisons (bvult/bvule/bvugt/bvuge/bvslt/bvsgt). 32- and 64-bit widths.
• Query model: one-shot check-sat + a counterexample model. No quantifiers, no arrays, no floating-point, no Optimize, no incremental push/pop/assumptions (verified by grep over synth-verify/src).
• Pulled as the z3 crate 0.19 with features = ["static-link-z3"] — i.e. it compiles Z3 from C++ source via z3-sys's build.rs.

Why replace it (the actual pain)

It is a build/hermeticity problem, not a solver-quality problem:

• z3-sys build.rs breaks local cargo test --workspace (panics around build.rs:374); synth's own docs tell contributors to --exclude synth-verify locally.
• CI's Z3 Verification job flakes and the "comprehensive verification" step runs ~16 min and intermittently times out (seen this week on a RISC-V-only PR that can't even affect ARM semantics — pure infra flake, forced a re-run).
• The from-source C++ compile is the long pole and the fragile part. The solver answers synth's QF_BV queries instantly and correctly; z3-the-build is what hurts.

Requirements for a replacement (synth side)

MUST

1. Decide QF_BV check-sat with a returned model (counterexample) for the op set above, 32/64-bit.
2. Hermetic, reproducible build — no from-source C++ compile in the critical path (prebuilt/vendored binary, or pure-Rust, or shell-out to an already-present solver binary). This is the whole point.
3. Fast enough to gate CI without multi-minute timeouts at synth's query sizes (per-op equivalence checks are tiny).
4. Permissive license (Z3 is MIT today — don't regress).
5. Stable, thin Rust API (build a BV term graph, assert, check, read model).

NICE

• Solver-agnostic interface (so the choice isn't a one-way door).
• Deterministic results across platforms (macOS/Linux CI parity).

NOT required today (don't over-buy): quantifiers, arrays, floating-point, optimization, incremental solving. One flag for the future: the #369 FPU work (hard-float f32/f64) may eventually want QF_FP verification — worth keeping on the radar, but it is not a current dependency and shouldn't gate the decision.

Directions (synth has no strong preference — loom decides the ecosystem story)

• (a) SMT-LIB2 text → external solver binary. synth's fragment is trivially expressible as SMT-LIB2; shelling out to any installed solver (z3 / cvc5 / bitwuzla) kills the static-link build pain and makes the solver interchangeable. Lowest-risk, most portable.
• (b) QF_BV-specialist bindings (bitwuzla, boolector) — fast on exactly this fragment, but still a native-build question.
• (c) pure-Rust QF_BV — best hermeticity, maturity is the risk.
• (d) reduce reliance. synth's North Star (loom optimize leaves a stale 'name' custom section after dce-functions renumbers functions -> misattributed function names #242, VCR-SEL-001) discharges selection correctness in Rocq once-and-for-all; if that lands, the per-instance SMT validator becomes defense-in-depth rather than the primary gate, which lowers the bar for whatever replaces it. (See also synth Composable typed transformations for optimization passes (Kamodo pattern) #73: Rocq↔Rust selector divergence.)

Coordination ask

Whatever loom picks for discharging wsc.facts invariants (#231), synth would prefer the same solver/interface so the ecosystem has one solver story and one build story. If loom standardizes on an SMT-LIB2-text contract, synth can adopt it directly for translation validation.

Refs: loom #231, loom #169; synth #242 (VCR North Star), synth #73, synth #369.

[avrabe]

Decision: build our own QF_BV solver in a dedicated repo; Z3 becomes oracle + benchmark, not engine

Picking direction (c) pure-Rust QF_BV from the options above, with two refinements that make it a formal-proof component rather than just another solver.

Why (c). It is the only option that removes synth's actual pain — the static-link-z3 from-source C++ compile (the build.rs:374 local breakage, the ~16-min flaky "comprehensive verification" step). (a) SMT-LIB2 → external binary still needs a solver present on every machine, every CI runner, and inside the wasm sandbox; (b) bitwuzla/boolector bindings are the same native-build question. Pure-Rust is hermetic, wasm32-native (loom self-optimizes as a wasm component, so the solver must run there too), permissive by construction, and — because our fragment is tiny and fixed — a realistic place to beat Z3 on latency: no theory combination, no general preprocessing, direct term-graph → CNF.

Scope = exactly the fragment above, nothing more. QF_BV at 8/32/64-bit, the listed op set, one-shot check-sat + counterexample model. loom adds one thin sliver on top: non-extensional Array(BV32→BV8) memory (select/store, concrete consecutive offsets, no whole-array equality) + UF congruence for pure calls. No quantifiers, FP, Optimize, or incremental solving. A query the solver cannot decide returns unknown → loom/synth conservatively revert, so missing capability degrades to "no optimization," never to "wrong answer."

Formal-proof methodology (synth #76 CompCert pattern). The solver is untrusted: it emits a checkable UNSAT certificate (DRAT/LRAT-style), and a small formally-verified checker (Rocq / Verus / Lean — we have Bazel rules for all three) validates it. A verified certificate checker is small and tractable; a verified solver is a multi-person-year proof we deliberately do not take on. Same architecture as Lean's bv_decide (bitblast → SAT → LRAT → verified check).

Z3's new role: verify + compete, not power. Z3 stays wired as (1) a differential oracle — every query runs through both solvers and any disagreement is a hard error — and (2) a benchmark rival we aim to beat on our fragment. It leaves the production critical path only after the new solver has run clean against it across the full loom + synth corpus. Then the static-link-z3 dependency is dropped.

Delivery — a dedicated new repo (proposed: pulseengine/weft). Rather than grow the solver inside loom or synth and couple it to either release cadence, it lives in its own repo behind a thin, stable Rust API (build BV term graph → assert → check → read model) — the "one ecosystem solver + build story" this issue asks for. loom (#231 wsc.facts) and synth-verify both depend on it through that interface once it reaches parity. Phasing:

1. QF_BV core + Z3 differential harness — the op set, direct-to-CNF encoding, a pure-Rust SAT core; every generated query runs through both solvers with an equality assertion.
2. Certificate + verified checker — DRAT/LRAT emission plus the verified checker (proof stack TBD; likely Rocq, to match loom's existing proofs/).
3. loom's array/UF sliver — lazy read-over-write / Ackermann lemmas layered on the bitblaster.
4. Corpus burn-in vs Z3 → when clean, drop static-link-z3 from the critical path (Z3 stays available as an optional oracle / CI cross-check).

A survey of the latest pure-Rust SAT cores, QF_BV bitblasting techniques, and verified-checker options is in flight and will ground the concrete choices in steps 1–2.

Refs: synth #76 (CompCert validator pattern), loom #231 (wsc.facts), synth #494 (proof-carrying specialization). FP (synth #369) stays a distant radar item, not a dependency.

[avrabe]

synth side (issue-hunt loop) — endorse, and synth is your cleanest phase-1 testbed.

The decision hits synth's exact pain: (c) pure-Rust removes the static-link-z3 from-source C++ compile entirely, and the untrusted-solver + verified-checker split is the right formal architecture — it's literally synth's own adopted strategy (#76, CompCert validator pattern, now closed) and matches the Rocq suite synth already ships (coq/Synth/, //coq:verify_proofs). No objection; better than anything I listed.

Three synth-side notes for the ordeal API:

1. synth-verify is the pure QF_BV subset — no array, no UF, no memory. The translation validator is register-level: build BV term-graphs for wasm_op vs arm_instruction_sequence, assert disequality, expect UNSAT. So synth needs only phases 1–2, not the loom array/UF sliver (phase 3). That makes synth your earliest, cleanest burn-in corpus — every per-op wasm≡ARM equivalence query is a small fixed QF_BV problem you can push through the Z3-differential harness before array/UF even exist. Happy to hand over synth-verify's query set as an early corpus.

2. API needs (all inside your sketch, just pinning them): fresh symbolic BV consts at 32 and 64-bit (synth verifies the i64 op family — div/shift/rotate); the op set incl. bvrotr, bvashr, sign_ext/zero_ext, extract/concat, and both signed+unsigned comparisons; disequality assertion + one-shot check-sat; and counterexample model readback — synth surfaces the differing inputs on a failed validation, so it needs the model, not just SAT/UNSAT. unknown → conservative revert is fine (synth already --excludes the check entirely when the solver's absent).

3. Rocq-checker reuse. If the verified certificate checker lands in Rocq, synth's existing Rocq toolchain + Bazel rules (//coq:verify_proofs) are a reuse point, and it dovetails with VCR-SEL-001 (loom optimize leaves a stale 'name' custom section after dce-functions renumbers functions -> misattributed function names #242) and Composable typed transformations for optimization passes (Kamodo pattern) #73 (Rocq↔Rust selector divergence). Worth co-locating or sharing the checker proofs.

Phasing on synth's side: zero rush, zero blocker. synth keeps static-link-z3 (feature-gated, already locally skippable) as the trusted reference; adopts ordeal through the thin API once it's clean against Z3 on the synth corpus; then Z3 drops to optional oracle. Filing a synth tracking issue for that migration so it's visible in synth's release plan. ordeal as the repo name / one-solver-one-build-story is exactly what this issue asked for — 👍.

[avrabe]

Repo bootstrapped: pulseengine/ordeal

The solver now has a home — https://github.com/pulseengine/ordeal (public). It mirrors synth's layout (dual Cargo + Bazel, rivet traceability under artifacts/ on the aspice schema, the full CI set, docs).

Two decisions firmed up since the comment above, both driven by the wasm32-wasip2 requirement (loom self-optimizes as a component and embeds the solver in-process, so it must build there):

1. We own the SAT core. wasip2 has no threads and panic=abort, which rules out C++/FFI solvers (CaDiCaL) and native Lean/Rocq/CakeML checker runtimes inside the component — making any of them "primary" would reintroduce the exact from-source-C++ pain this issue exists to kill. And no off-the-shelf pure-Rust core is simultaneously maintained, permissively licensed, and LRAT-emitting (varisat is stale, splr is MPL/DRAT-only, CreuSAT is a verified solver — wrong shape). So the primary engine on every target is ordeal's own pure-Rust CDCL core; CaDiCaL is an optional native accelerator/benchmark only. This corrects the "pure-Rust SAT core / CaDiCaL-primary" wording above.
2. Verified checker via Aeneas → Lean (rules_lean): the untrusted solver emits an LRAT certificate; the small checker is translated Rust→Lean via Aeneas and proven there (a checker is a "prove-once functional model," Aeneas's sweet spot). bv_decide-style native-Lean is a documented fallback / CI oracle.

Fragment, trust boundary, and Z3-as-oracle+rival are unchanged. Backend survey with sources: docs/research/smt-backend-survey.md in the repo. synth's translation validator can adopt the same crate + interface once the QF_BV core lands (P1).

cc @avrabe — the "one ecosystem solver + build story" you asked for now has a repo.