Adopt ordeal for certificate-checked optimization-rule verification (replace loom's own Z3 path)

[avrabe]

Field report from ordeal (certificate-checked QF_BV engine). Not a bug in loom — an adoption opportunity surfaced while wiring ordeal's v0.7.0 consumer surface.

What I observed (origin/main)

loom-core verifies its optimization rules with Z3 directly, behind the verification = ["z3"] feature (verify_rules / examples/verify_rules_demo.rs — "uses Z3 to PROVE optimization rules are correct"). The Z3 Unsat verdict ("rule holds for all inputs") is trusted with no independent certificate, and the build pulls in a Z3 link dependency (the real pain called out in #246).

The opportunity

Rule verification here is QF_BV equivalence (bitvector op ≡ op, widths 8/32/64) — squarely inside ordeal's closed fragment. Two moves, both already precedented in the org:

1. Swap the engine. ordeal::Solver::prove_equiv(a, b) is the one-call equivalence-as-UNSAT primitive; Unsat = "equal for every input". Pure-Rust, zero-dep default build, builds on wasm32-wasip2 — no static-link-z3. This is exactly what synth-verify did (synth#553, completed: ordeal default, Z3 demoted to optional differential oracle).
2. Get a certificate you can re-check. As of ordeal v0.7.0 the Unsat Certificate carries both the refuted CNF (cert.cnf) and the LRAT proof (cert.lrat), and cert.recheck() re-validates the pair through the formally-verified ordeal-lrat checker. So "these rules are equivalent" becomes evidence loom can reproduce, not solver faith — the certifying-validator direction (cf. synth#667).

Scope / honesty

• Not urgent and not a soundness bug: Z3 is sound in practice. The value is (a) a checkable certificate instead of trust, and (b) dropping the Z3 build/link burden.
• If any rule uses a construct outside the closed fragment (quantifiers, FP, non-consecutive symbolic array indices), ordeal returns Unknown (conservative) — tell us the exact term and it becomes a missing-capability on ordeal.

Refs

• Relates to synth's requirements for a Z3 replacement — QF_BV one-shot validation; the static-link build is the real pain, not the solver #246 (Z3 replacement requirements — QF_BV one-shot validation; static-link pain).
• Precedent: synth#553 (adopted), synth#667 (certifying validator).
• Guide + runnable example: ordeal docs/consuming-ordeal.md, cargo run -p ordeal --example translation_validation.