[dependabot]

Bumps ordeal from 0.22.1 to 0.27.0.

Release notes

Sourced from ordeal's releases.

ordeal v0.27.0

Falsification statement

well-formed, re-encodes it with the proven encoder, and checks the LRAT proof against that CNF. check_query_sound: an accepted bundle refutes the query DAG, with no assumption beyond acceptance. It ships as an opt-in ordeal-cert/v2 (--with-query); v1 bundles and default output are unchanged. #225: the trusted crate fails closed on overflow in release builds.

Falsification: this release is wrong if a v2 bundle whose query block was altered (with hashes recomputed) still passes recheck with an unchanged proof; or if ordeal 0.27.0's default output differs from 0.26.0 on any query; or if an arithmetic overflow in the released ordeal-lrat wraps instead of panicking.

Release note (rivet, from the trace)

4 artifact(s) in scope: 4 delivered, 0 withheld.

Functionalities provided

sw-req

• TR-062 (verified) — The trusted checker re-checks the query, not only the CNF — check_query and ordeal-cert/v2 (#192 phase 4)
• TR-063 (verified) — The trusted checker fails closed on arithmetic overflow in release builds, matching the proven model (#225)

sw-verification

• VER-062 (verified) — The trusted crate re-checks the query — check_query proven, ordeal-cert/v2 alongside v1, output unchanged (TR-062)
• VER-063 (verified) — Overflow in the trusted crate panics in release builds (TR-063)

Limitations in relation to the committed scope

None — every artifact committed to v0.27.0 is release-ready.

Result of verification measures

Every delivered artifact carries verification evidence:

• TR-062 — 1 link(s), 0 source marker(s)
• TR-063 — 1 link(s), 0 source marker(s)
• VER-062 — 0 link(s), 13 source marker(s)
• VER-063 — 0 link(s), 1 source marker(s)

Changes since v0.26.0

• a82d56bb fix(checker): #225 the trusted ordeal-lrat fails closed on overflow in release builds (TR-063) (#226) — refs #225, #226

... (truncated)

Changelog

Sourced from ordeal's changelog.

[0.27.0] - 2026-10-01

The trusted checker re-checks the query, not just a CNF (#192 phase 4). ordeal_lrat::check_query re-encodes a well-formed term DAG with the proven encoder. check_query_sound states that an accepted bundle refutes the query DAG. It ships as an opt-in ordeal-cert/v2; v1 bundles and default output are unchanged. The trusted crate now fails closed on overflow in release builds (#225).

Fixed

• The trusted checker fails closed on overflow in release builds (TR-063, #225). The Lean proofs model overflow as failure, but release builds wrapped silently. overflow-checks is now on for ordeal-lrat in the release profile. Cost: about 1% on a 30 MB-proof query. Downstream workspaces should add the same override (see docs/consuming-ordeal.md).

The trusted checker re-checks the query, not only the CNF (#192, phase 4). The proven lowering moved into ordeal-lrat, which gains check_query: a proven well-formedness check of the term DAG, the re-encoding through the same proven code the solver runs, and the LRAT check against that CNF — check_query_sound has no side conditions left. ordeal-cert/v2 carries the query alongside the v1 pair; v1 is untouched and default output is byte-identical to v0.26.0.

Added

• ordeal_lrat::check_query (kernel::check_query, #192 phase 4): given a term DAG (DagNode list, constant bits, roots), the solver's compaction hints and an LRAT certificate, it checks the DAG well-formed (dag_wf), re-runs encode / compact / map_word / tseitin and checks the certificate against the CNF it produced, returning that CNF. lean/QueryCheck.lean proves dag_wf_spec (the Rust check returns Ok iff the Lean DagWF predicate holds and every width fits usize) and the capstone check_query_sound (an accepted run ⟹ no assignment to the DAG's variables makes every root true), composed from dag_wf_spec, encode_sound, compact_sound, tseitin_refutes_outputs and lrat_check_sound through phase 3's dag_refuted; both pinned axiom-clean in AxiomCheck.lean, each with a negative control recorded in docs/design/query-cnf-gap.md.
• ordeal-cert/v2 (cert_bundle.rs, cert-bundle feature): the v1 envelope plus a query block (ordeal-dag/v1: nodes as [op, args…], constant bits, roots, hints, sha256) and format: "ordeal-cert/v2". QueryCertificate::to_cert_v2 / from_cert_v2 (all three hashes verified before returning) / QueryBundle::recheck (the trusted check_query, plus a check that the re-encoded CNF is the carried one). Flipping one constant bit of the query fails the recheck while the CNF and the proof are untouched; a stale query hash fails at parse.
• Solver::check_with_query and ordeal::query (QueryDag, QueryCertificate, QueryCheckResult, always compiled): the opt-in entry that returns the certificate together with the lowered query, re-checked by the trusted crate before Unsat is returned.

... (truncated)

Commits

• 97d314f chore(release): v0.27.0 — the trusted checker re-checks the query (check_quer...
• a82d56b fix(checker): #225 the trusted ordeal-lrat fails closed on overflow in releas...
• 0e917f8 proof: #192 phase 4 — the trusted crate re-checks the query: check_query prov...
• 4bf1430 chore(release): v0.26.0 — every query is lowered through proven code (#192 ph...
• 3b2e790 proof: #192 phase 3 — proven term-DAG encoder and folding/hashing pass; the s...
• 65aa715 chore(release): v0.25.0 — the solver runs the Lean-proven blast rules; Tseiti...
• 20ed242 ci(kani): pin Kani 0.68.0 in every tier; record the accepted add_64/sub_64 ga...
• 7f9baa6 proof: #192 phase 2 — the solver runs the Lean-proven blast rules; duplicate ...
• ff71e91 proof: #192 phase 1 — XOR gate identity, proven Tseitin, CNF-size benchmark (...
• 87f5334 chore(release): v0.24.0 — every-width shift/rotate proofs, CI results as rele...
• Additional commits viewable in compare view

[temper-pulseengine]

temper did not enable auto-merge: breaking update ordeal 0.22.1 -> 0.27.0 needs a human review.

[github-actions]

🔒 HELD — not auto-mergeable (class: zerox-minor). 0.22.1 -> 0.27.0: for a 0.x crate the MINOR is the de-facto major (ordeal 0.9->0.12; object 0.39->0.40 / #938)

Auto-merge has been actively disabled and asserted off by the hold gate (#965). For a 0.x crate the MINOR component is the de-facto major (and for 0.0.x, the patch): ordeal 0.9→0.12 auto-merged as "minor" and hung Test+Z3 for days; object 0.39→0.40 (#938) broke 16 call sites across three unrelated newtype surfaces. Merge this BY HAND only once the FULL suite is green, including the separate --features z3-solver path (required context "Z3 Verification") — the discriminator is CI, not a read of the diff.

[github-actions]

🔒 HELD — not auto-mergeable (class: zerox-minor). 0.22.1 -> 0.27.0: for a 0.x crate the MINOR is the de-facto major (ordeal 0.9->0.12; object 0.39->0.40 / #938)

Auto-merge has been actively disabled and asserted off by the hold gate (#965). For a 0.x crate the MINOR component is the de-facto major (and for 0.0.x, the patch): ordeal 0.9→0.12 auto-merged as "minor" and hung Test+Z3 for days; object 0.39→0.40 (#938) broke 16 call sites across three unrelated newtype surfaces. Merge this BY HAND only once the FULL suite is green, including the separate --features z3-solver path (required context "Z3 Verification") — the discriminator is CI, not a read of the diff.

[github-actions]

🔒 HELD — not auto-mergeable (class: zerox-minor). 0.22.1 -> 0.27.0: for a 0.x crate the MINOR is the de-facto major (ordeal 0.9->0.12; object 0.39->0.40 / #938)

Auto-merge has been actively disabled and asserted off by the hold gate (#965). For a 0.x crate the MINOR component is the de-facto major (and for 0.0.x, the patch): ordeal 0.9→0.12 auto-merged as "minor" and hung Test+Z3 for days; object 0.39→0.40 (#938) broke 16 call sites across three unrelated newtype surfaces. Merge this BY HAND only once the FULL suite is green, including the separate --features z3-solver path (required context "Z3 Verification") — the discriminator is CI, not a read of the diff.

[dependabot]

Superseded by #1561.