Retire Z3: migrate the core translation validator to ordeal and drop the C++ dependency

[avrabe]

Decision: standardize on ordeal as loom's only solver and remove Z3. Recording it as an issue because it is an architecture change with consequences beyond the verifier, and because the evidence for doing it now has accumulated rather than been argued.

Why now — four independent pressures, not a preference

1. It is shipping broken binaries. release: the x86_64-unknown-linux-gnu binary needs GLIBC 2.38 — won't load on ubuntu-22.04 (a supported GitHub runner) #311: the v1.2.0 Linux release required GLIBCXX_3.4.31 and would not load on ubuntu-22.04. That symbol requirement exists only because loom links Z3 (C++). v1.3.0 pins the builder image and asserts the floor, but that is a workaround for a dependency we intend to delete.
2. It is the wasip2 friction. Building loom for wasm32-wasip2 locally fails in z3-sys with could not find native static library c++`` — we carry a forked z3.rs branch for wasi-sdk support to get as far as we do. A pure-Rust solver removes the fork and the C++ sysroot problem together.
3. Tier-1 already proved the pattern. Adopt ordeal for certificate-checked optimization-rule verification (replace loom's own Z3 path) #277 moved the algebraic rule verifier behind a swappable backend: 38/38 rules proven, reported identically by both engines, and in both mode the harness runs both per obligation and panics on divergence — it did not. The migration seam, the differential harness and the answer to "do they agree" all exist already.
4. The last capability blocker is gone. ordeal#70 (symbolic-index array select/store) shipped in 0.11.0; loom is on 0.17.0. There is no longer a modelling gap that forces Z3 for the memory fragment.

Measured surface — smaller than the line count suggests

verify.rs is 9,696 lines, but the Z3 API surface across the whole crate is eight types in five files:

verify.rs        use z3::ast::{Array, BV, Bool};
                 use z3::{Config, FuncDecl, SatResult, Solver, Sort, with_z3_config};
verify_rules.rs  verify_e2e.rs  islands.rs  rule_solver.rs

Every one has a direct ordeal counterpart — BvTerm/BoolTerm, Solver/CheckResult, Sort, and sliver's array + uninterpreted-function support for Array/FuncDecl. The bulk of those 9.7k lines is term construction over BV/Bool, which is mechanical to port, not a redesign.

Plan

• Tier-2, behind the same backend seam Adopt ordeal for certificate-checked optimization-rule verification (replace loom's own Z3 path) #277 established: port the validator slice by slice — pure BV, then UF/congruence, then havoc, then concrete memory, then symbolic memory.
• Run LOOM_VERIFY_BACKEND=both through the migration so every obligation is cross-checked against the incumbent while it is still present. Divergence is a hard failure, not a warning.
• Drop the z3 dependency and the forked z3.rs only once both mode is clean across the full suite.
• Then delete the release workflow's glibc-floor assertion, ship a musl artifact, and close release: the x86_64-unknown-linux-gnu binary needs GLIBC 2.38 — won't load on ubuntu-22.04 (a supported GitHub runner) #311's option 2 for free.

Sequencing with #300 — this is the important one

#300 asks for refinement-based validation with traps as first-class state, rather than value-equivalence plus guards. Do not port the current total-model encoding to ordeal and then re-architect it. Tier-2 and #300 are one piece of work: port and change the relation in the same pass, keeping the existing static guards as a floor throughout. Porting twice is the only way to make this expensive.

What it buys

• No C++ toolchain in the build — Linux portability, musl, and wasip2 stop being three separate fights.
• Certificates we can re-check: ordeal returns an LRAT proof for every Unsat and loom validates it before believing the verdict. That is evidence the incumbent never offered.
• One solver to reason about, and it is one we can fix — Investigate: verify.rs opaque-float shared const name may unify distinct float ops (verifier soundness) #283 (float constant naming) is currently a question we can only file upstream.

Honest risks

• verify.rs is the safety-critical core; a silent regression here is the worst failure mode loom has. The both-mode differential is the mitigation and it must stay on for the whole migration, not just the start.
• Float modelling (Investigate: verify.rs opaque-float shared const name may unify distinct float ops (verifier soundness) #283) must be resolved during the port, not transcribed. Carrying a suspected soundness bug across a migration would launder it into 'new code'.
• Performance is unmeasured at the core-validator scale. Tier-1 showed agreement, not throughput parity. If ordeal is materially slower on the big obligations, that is a finding to publish, not to hide.

Refs #277, #300, #311, #283, #246

[avrabe]

Closing step: archive the z3.rs fork

The migration is not done when the dependency is dropped from Cargo.toml — it is done when the fork we maintain to support it is retired. Adding that as an explicit exit criterion so it does not quietly become permanent infrastructure for a dependency we deleted.

We carry pulseengine/z3.rs (branch wasi-sdk-support) solely to get z3-sys building against a wasi-sdk sysroot. Verified state:

pulseengine/z3.rs   fork=true   archived=false   last updated 2025-12-20

loom is its only consumer. An org-wide code search for pulseengine/z3.rs returns exactly two hits, both in this repository:

pulseengine/loom  Cargo.toml
pulseengine/loom  .github/workflows/ci.yml

So nothing else has to migrate first — the archive is gated on this issue alone. (Worth re-running that search at archive time rather than trusting this snapshot; search indexes lag and private repos may not appear.)

Exit sequence, in order:

1. Tier-2 complete, LOOM_VERIFY_BACKEND=both clean across the full suite.
2. Drop z3 and z3-sys from Cargo.toml; remove the Z3 steps and the Z3_SYS_Z3_HEADER plumbing from CI.
3. Confirm no remaining reference: the org search above must return zero hits, and the wasm32-wasip2 build must pass without a wasi-sdk C++ sysroot.
4. Delete the glibc-floor assertion added for release: the x86_64-unknown-linux-gnu binary needs GLIBC 2.38 — won't load on ubuntu-22.04 (a supported GitHub runner) #311 and ship the musl artifact — both exist only because of the C++ link.
5. Archive pulseengine/z3.rs — read-only, not deleted. The commit history is the record of why the patches existed, and anyone hitting the same wasi-sdk problem should still be able to read them.

An unmaintained fork that nothing consumes is the infrastructure equivalent of the dead code this project keeps finding: it looks maintained because it exists, and it costs attention every time someone audits the dependency graph. Archiving states plainly that it is finished.

Refs #311