chore(deps): bump ordeal from 0.16.1 to 0.17.0

[dependabot]

Bumps ordeal from 0.16.1 to 0.17.0.

Release notes

Sourced from ordeal's releases.

ordeal v0.17.0

What's Changed

• feat: #[non_exhaustive] on the public term enums + variant-addition policy (#104) by @​avrabe in pulseengine/ordeal#105
• feat: criterion latency benchmarks — the honest numbers (TR-009 item 3, #57) by @​avrabe in pulseengine/ordeal#106
• feat: ordeal-cert/v1 bundle serialization (TR-025 ordeal half, #91) by @​avrabe in pulseengine/ordeal#107
• chore(rivet): VER-010 executed — benchmark numbers in the trace by @​avrabe in pulseengine/ordeal#108
• feat: optional CaDiCaL accelerator backend with checker-gated LRAT (TR-004 / VER-008) by @​avrabe in pulseengine/ordeal#109
• chore(release): v0.17.0 — certificate as evidence + the CaDiCaL accelerator by @​avrabe in pulseengine/ordeal#110

Full Changelog: pulseengine/ordeal@v0.16.1...v0.17.0

Changelog

Sourced from ordeal's changelog.

[0.17.0] - 2026-07-29

Certificate as evidence + the optional CaDiCaL accelerator (FEAT-011, TR-025, TR-004/VER-008; issues #91, #57-adjacent). The certificate becomes audit-grade evidence consumable outside this repo, and TR-004's reserved CaDiCaL option is real — held to the identical soundness contract.

Added

• cadical feature — the optional CaDiCaL accelerator (TR-004, VER-008). sat_cadical::solve runs CaDiCaL 2.1.3 (vendored hermetically by cadical-sys; native-only, never load-bearing, never on the wasm path) and returns Unsat only with an LRAT proof the verified checker accepted, Sat only with a self-checked model. The load-bearing detail: CaDiCaL emits standard LRAT numbering only via DIMACS input (its parser reserves ids 1..=n for the originals; the incremental add() API interleaves derived ids and the checker rightly rejects those proofs), so the CNF goes in through a temp DIMACS file. Three-way parity executed (VE-019/VV-041): own core vs CaDiCaL vs Z3 on 150 corpus queries + 200 random CNFs — zero disagreements. CI gains a blocking cadical job; the oracle job runs the three-way parity.
• ordeal-cert/v1 bundle serialization (cert-bundle feature, #107): Certificate::to_cert_v1/from_cert_v1 with both content sha256s verified before parsing returns (integrity before mathematics), and UnsatBundle::recheck() for offline re-validation.
• rules_ordeal v0.1.0 (separate repo, pulseengine/rules_ordeal): hermetic ordeal_check/ordeal_verus_check Bazel test rules over a sha256-pinned ordeal release download; a non-unsat verdict fails the gate. The rivet-ingestion leg of TR-025 is split to TR-030 (v0.18.0), blocked on rivet#693.
• Criterion latency benchmarks (#106, VER-010/VE-018): the honest two-lane numbers — certified ordeal vs unchecked Z3 — including the concessions (Z3 wins genuine search 42x on the srem VC).

Falsification

This release is wrong if: the cadical feature can surface an Unsat whose LRAT proof ordeal_lrat::check did not accept; or the default build's dependency tree contains anything beyond ordeal-lrat; or an ordeal_check Bazel gate passes on a file whose verdict is not unsat; or a tampered ordeal-cert/v1 bundle (proof or problem) survives from_cert_v1.

Commits

• 22c4e34 chore(release): v0.17.0 — certificate as evidence + the CaDiCaL accelerator (...
• d37829b feat: optional CaDiCaL accelerator backend with checker-gated LRAT (TR-004 / ...
• 621b784 chore(rivet): VER-010 executed — the benchmark numbers land in the trace (VE-...
• 79cd181 feat(v0.17.0): ordeal-cert/v1 bundle serialization (TR-025 ordeal half, #91) ...
• 95ceb46 feat: criterion latency benchmarks — the honest numbers (TR-009 item 3, #57) ...
• 21e78c0 feat: #[non_exhaustive] on the public term enums + variant-addition policy (#...
• See full diff in compare view

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

---

Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

• @dependabot rebase will rebase this PR
• @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
• @dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
• @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)

[github-actions]

🔒 0.x MINOR bump — held for manual review. 0.16.1 → 0.17.0: for a 0.x crate the MINOR component is the de-facto major, so this is BREAKING even though Dependabot labels it semver-minor. This gap broke synth twice on ordeal (0.9→0.12 added BvTerm::Urem, breaking every exhaustive match; 0.9→0.16 in #864 landed with no CI run and left main uncompilable). Build EVERY affected feature set (incl. --features z3-solver) and run the full synth-verify suite before merging.

[avrabe]

Holding this bump — not merging.

ordeal is the SMT solver behind synth-verify, and it is pinned =0.16.1 deliberately. Because its major version is 0, Cargo/dependabot classify 0.16.1 → 0.17.0 as a minor update, but under semver a 0.x-minor bump is breaking. This repo has been burned by exactly that before: the 0.9 → 0.12 bump auto-merged as "minor" and its bvsrem/bvsdiv behaviour hung Test and Z3 for 4–6 hours a run, for days, until the pin was restored.

This PR is not a theoretical risk — it is currently failing five real checks:

• Test
• Clippy
• Z3 Verification
• Kani Verification
• fact-spec elision oracle (#494 phases 2 + 2b + 3+ + bounds)

The last one matters most: the fact-spec oracle is what certifies proof-carrying specialization elisions, so a solver change that moves it is a change to what the compiler is willing to prove, not just how fast it proves it.

What un-blocking this needs, per the standing rule for solver dependencies:

1. The full suite green, including the separate --features z3-solver path (a default-feature build does not exercise every solver call site — that gap is how fix(ci): repair red main — Cargo.lock wasmparser dedup + ordeal 0.12 BvTerm::Urem #836 shipped an unhandled BvTerm::Urem match arm).
2. An explanation of what changed semantically in 0.17.0 for the QF_BV operations synth actually emits.
3. Re-verification that the LRAT certificates are still checked and still validate — the elision path trusts Unsat only because a proof accompanies it.

Closing rather than leaving it open, since dependabot will re-open with a fresh branch when there is a newer release to evaluate. Tracked against the ordeal pin.

[dependabot]

OK, I won't notify you again about this release, but will get in touch when a new version is available. If you'd rather skip all updates until the next major or minor version, let me know by commenting @dependabot ignore this major version or @dependabot ignore this minor version. You can also ignore all major, minor, or patch releases for a dependency by adding an ignore condition with the desired update_types to your config file.

If you change your mind, just re-open this PR and I'll resolve any conflicts on it.