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

[dependabot]

Updates the requirements on ordeal to permit the latest version.

Release notes

Sourced from ordeal's releases.

ordeal v0.15.0

What's Changed

• feat: v0.15.0 — Lean-verified bit-blaster: all 27 rules proven unbounded (FEAT-012 / TR-027, #68) by @​avrabe in pulseengine/ordeal#93
• chore(release): v0.15.0 — the Lean-verified bit-blaster by @​avrabe in pulseengine/ordeal#94

Full Changelog: pulseengine/ordeal@v0.14.0...v0.15.0

Changelog

Sourced from ordeal's changelog.

[0.15.0] - 2026-07-22

P12 — the assurance capstone: Lean-verified bit-blaster (FEAT-012 / TR-027, issue #68). Every bit-blasting rule in the closed fragment now carries an unbounded Lean 4 proof — the encoder joins the checker in the formally-verified core, and the pipeline's soundness argument no longer leans on Kani-bounded evidence.

Added

• All 27 rules proven against BitVec semantics for every width, stated about the Aeneas-generated translation of the blaster model (lean/BlastKernel.lean, pinned Charon+Aeneas via regen-blaster.sh): bitwise, add/sub, all eight comparisons, eq/ne, ite, the four structural rules, the four shifts, the multiplier, and the divider. Six proof developments (~7,400 lines), total-correctness WP (no panic, no divergence), exact gate counts proven as length equalities.
• The divider's w-bit trick is now a theorem. The Rust comment's soundness argument — the shifted-out top bit alone decides the (w+1)-bit compare, and the w-bit modular difference is exact because rem < divisor bounds it below 2^w — is machine-checked (pDivGeStep_eq_decide, pDivRemStep_denotesBits). Division-by-zero is proven precisely: quotient = smtUDiv (all-ones; core's udiv differs, #eval-confirmed), remainder = core % (already SMT-LIB-conformant).
• crates/ordeal/src/blast_kernel.rs — the Charon-translatable model, plus the fidelity differential: every one of the 65,536 width-8 input pairs through the real (strashed) blaster and the model, bit-for-bit, across every rule family.
• CI gates the capstone like the checker: the lean job builds all seven proof libraries and enforces an elaborator-based zero-sorry budget over every Blaster*.lean.

The assurance chain (each link labeled with its actual strength)

shipped blaster =(exhaustive width-8 differential; bounded, test evidence)= model
model           =(Lean 4, ALL widths, zero sorry, three standard axioms)=  BitVec

The Kani harnesses remain as defense-in-depth; they are no longer the claim.

Falsification

Wrong if: any Blaster*.lean theorem acquires a sorry/sorryAx (the CI budget catches this); the fidelity differential finds any input where the model and the shipped blaster disagree; a regenerated BlastKernel.lean breaks a proof (CI lake build); or any proven rule disagrees with the Z3 differential on any query.

[0.14.0] - 2026-07-21

P11a — propositional SAT front-end (FEAT-014 / TR-026, issue #67). The certificate-as-evidence thesis at the Boolean level: decide a caller's CNF through the same certified path as the bit-blaster, so a consistency verdict is

... (truncated)

Commits

• 476e36d chore(release): v0.15.0 — the Lean-verified bit-blaster (#94)
• b111b1a feat: v0.15.0 — Lean-verified bit-blaster: all 27 rules proven unbounded (FEA...
• 47a8601 chore(release): v0.14.0 — propositional SAT front-end (#92)
• 405cda2 feat: v0.14.0 — propositional SAT front-end (FEAT-014 / TR-026, #67 piece 1) ...
• 28073c7 chore(release): v0.13.0 — verify scope, bump, changelog (#89)
• c04e036 feat: v0.13.0 — prove_valid API + consumer recipes (FEAT-010 / TR-024, #66) (...
• fae3a0a chore(release): v0.12.0 — verify scope, bump, changelog, README (#87)
• 28d2bb4 feat: v0.12.0 — Verus VC bridge, 62/62 of gale's obligations (FEAT-009 / TR-0...
• 8cdb6e6 chore(release): v0.11.0 — verify the scope, bump, changelog (#85)
• 87a9b96 feat: v0.11.0 — symbolic-index array select/store (FEAT-013 / TR-028, #70) (#83)
• 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)