chore(deps): update ordeal requirement from 0.15.0 to 0.17.0

[dependabot]

Updates the requirements on ordeal to permit the latest version.

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.

[0.16.1] - 2026-07-23

Patch: the unsigned twin of #97 (issue #101, synth). v0.16.0 fixed the derived bvsrem lowering; direct users of the native BvTerm::Urem enum still hit the restoring divider's remainder, so a urem-vs-multiplicative VC stayed exponential (synth's verify_i32_rem_u: over 7 m 48 s, killed).

Fixed

• The native Urem blast rule is multiplicative: a − (a udiv b)·b at the circuit level — exact for all inputs including /0 with no special case

... (truncated)

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 (#...
• ffaa872 chore(release): v0.16.1 — the #101 unsigned-urem patch (#103)
• da052b7 fix: bvurem VCs hung — multiplicative native Urem blast + re-proof (#101) (#102)
• 264c650 chore(release): v0.16.0 — the #97 fix + migration ergonomics (#100)
• d090ae6 fix: srem VCs hung against multiplicative consumer models (#97) (#99)
• Additional commits viewable 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)