chore(deps): bump ordeal from 0.16.1 to 0.18.0

[dependabot]

Bumps ordeal from 0.16.1 to 0.18.0.

Release notes

Sourced from ordeal's releases.

ordeal v0.18.0

What's Changed

• feat: v0.18.0 replan + TR-031 executed — BMC practical-k envelope, consumer parallelism by @​avrabe in pulseengine/ordeal#111
• chore(deps): Bump criterion from 0.5.1 to 0.8.2 by @​dependabot[bot] in pulseengine/ordeal#114
• chore(rivet): TR-009 resolved (caching rejected with measurement); VER-028 verified by @​avrabe in pulseengine/ordeal#113
• chore(deps): Bump sha2 from 0.10.9 to 0.11.0 by @​dependabot[bot] in pulseengine/ordeal#115
• feat(release): v0.18.0 — TR-030 rivet ingestion demonstrated; cosign-signed checksums (#116) by @​avrabe in pulseengine/ordeal#117

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

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.18.0] - 2026-08-08

Consumer scale-out: the BMC practical-k envelope, the measured caching rejection, and rivet ingestion demonstrated (FEAT-015; TR-030, TR-031, TR-009 closure; issues #112, #57, #116; rivet#693 Part 2, spar#350). The release shaped by the 2026-07-29 asks sweep — everything consumer-pulled.

Added

• BMC practical-k envelope (TR-031/VER-028, #111, spar#350): a #[doc(hidden)] BMC corpus (bmc_corpus.rs — queue-overflow and two-lock-deadlock shapes over the closed fragment) plus the two-lane criterion bench benches/bmc.rs. Measured certified end-to-end (macOS arm64): queue shape crosses 1 s around k ≈ 90, 2.53 s at k = 128 (own core) vs 2.00 s (cadical accelerator); deadlock shapes stay under ~275 ms through k = 96 — where the accelerator LOSES on fixed DIMACS/proof-file overhead. Seeded defects go SAT with replayable schedules; every UNSAT leg re-checks offline.
• rivet ingestion demonstrated against a released rivet (TR-030/ VER-029): rivet v0.31.0+ ships the ordeal-certificate artifact type (rivet#693 Part 2, rivet PR #743). The new examples/rivet_ingestion.rs produces a bundle from a live solve, re-ingests it the way rivet does (hash-verified parse + recheck()), proves structurally tampered proof/problem payloads are rejected at ingestion, and emits a fixture that released rivet 0.32.0 validates clean — with the never-re-checked negative failing the recheck-gates-verifies rule. The TR-025 evidence spine is closed end-to-end.
• Keyless cosign signing of release checksums (#116, TR-033, varve): the release workflow now signs SHA256SUMS.txt via Sigstore keyless OIDC, publishing .cosign.bundle/.sig/.pem — the org Track-A standard, unblocking ordeal's re-entry into varve toolchain layers. This release is the first signed one.
• Consumer parallelism guidance + compile-time Send + Sync guarantee (#111): docs/consuming-ordeal.md documents the parallelize-across-queries model with the measured envelope; a compile-time assertion pins every API type Send + Sync so the guarantee cannot silently regress.

Changed

• TR-009 term-graph caching: REJECTED with data (#113, closing #57's remainder): at BMC k = 128 the entire frontend (canon + blast + Tseitin) is 7.6 ms of a 2,555 ms certified solve (0.3 %) — caching addresses work that is not where the time goes. Recorded in the rivet graph; re-openable only with a workload where the frontend share is material.
• Seed-portfolio parallelism parked as TR-032 (measure-first activation; certificate-nondeterminism concession documented in the consumer guide).
• Solver internals: shared lower() / decode_and_check() split, and a #[doc(hidden)] check_with_cadical yardstick entry (TR-004 role

... (truncated)

Commits

• 4695e85 feat(release): v0.18.0 — TR-030 rivet ingestion demonstrated; cosign-signed c...
• e1f8c69 chore(deps): Bump sha2 from 0.10.9 to 0.11.0 (#115)
• 1a5a6ee chore(rivet): TR-009 resolved with the caching rejection measured; VER-028 ve...
• 3f3aebc chore(deps): Bump criterion from 0.5.1 to 0.8.2 (#114)
• 3af2bda feat: v0.18.0 replan + TR-031 executed — BMC practical-k envelope, consumer p...
• 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) ...
• 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)

[github-actions]

🔒 0.x MINOR bump — held for manual review. 0.16.1 → 0.18.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]

Dependency-upgrade lane result (0.16.1 → 0.18.0, two 0.x-minor = two breaking steps by repo rule).

Root cause of all six red checks: one mechanical API break. ordeal 0.17.0 sealed BvTerm/BoolTerm with #[non_exhaustive] (ordeal#104 — added explicitly because synth's build broke on 0.x bumps twice). E0004 at 6 match sites in synth-verify/src/term.rs + 2 in the z3-solver-gated translation in solver.rs; Kani failed via synth-backend's dev-dep on synth-verify. No enum variants were added between 0.16.1 and 0.18.0 — the new catch-all arms are dead code today, and they PANIC loudly per ordeal's own consumer policy ("conservative error, never a guess"); the two Display impls emit non-panicking markers. No test weakened, no oracle floor touched, no #[allow].

No behavioral or performance change measured (macOS arm64, warm builds, /usr/bin/time):

• workspace: 2830 passed / 0 failed (rc=0)
• synth-verify default engine: 268/268 on both versions, pure test-exec 35.0s on 0.16.1 AND 0.18.0
• z3-solver,arm differential suite: 270/270 on both, exec 35s vs 38s (~8%, noise; no 0.12-style hang — that regression presented as 4–6h wall)
• feature matrix: default ✅, verify ✅ (fact-spec Beyond parity: proof-carrying specialization + optimal-alloc to BEAT LLVM (0.7× target) #494 + VCR-MEM-004 cargo gates), z3-solver,arm ✅, riscv ✅
• claim_check 49/49; fmt + clippy -D warnings clean

What 0.17/0.18 actually are: 0.17 = sealed enums + opt-in cadical accelerator + cert-bundle (both unused here); 0.18 = BMC bench corpus + internal solver split (check_with_deadline unchanged, check_with_cadical added). Core certified solve path untouched.

Recommendation: upgrade. The pin existed for the 0.12 perf-hang class; 0.18.0 shows no trace of it, and 0.17's sealing + changelog-callout policy makes the next variant addition a loud, documented event instead of a surprise. Auto-merge stays OFF — merge on green CI per the lane coordinator.

[codecov]

Codecov Report

❌ Patch coverage is 0% with 6 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-verify/src/term.rs	0.00%	6 Missing ⚠️

📢 Thoughts on this report? Let us know!