[dependabot]

Bumps ordeal from 0.22.1 to 0.32.0.

Release notes

Sourced from ordeal's releases.

ordeal v0.32.0

Falsification statement

• The default entry points (check, check_with_limit, check_with_deadline, check_with_witness, and the sliver one-shots) go through one pipeline and one trusted gate.
  • unsat: check_term_dag, then check_query (LRAT checked once, against the re-encoded CNF).
  • sat: the eval.rs self-check, the CNF witness, check_term_dag, check_query_model and check_input_value. canon.rs, dag.rs and eval.rs leave every answer's trust path. A rejection is Unknown.
• dag::term_map resolves its choices from the DAG roots. v0.31.0's opt-in --with-term returned Unknown on 6 of gen_corpus(0xC0FFEE, 1000); this release decides them.
• Verdicts and certificate digests are identical to v0.31.0 on 8230 queries. Output is byte-identical. The overhead is 1.21x on the latency corpus.

Falsification: this release is wrong if check (or any default entry point) returns Unsat for a query some assignment satisfies, or Sat with a model that leaves a root of the query as asked false; or if it returns a different verdict or certificate than v0.31.0 on any query that v0.31.0 decided, other than a deadline-bounded Unknown.

Release note (rivet, from the trace)

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

Functionalities provided

sw-req

• TR-070 (verified) — Every answer rests on the proven term check — the default entry points run check_term_dag + check_query / check_query_model + check_input_value, so canon.rs, dag.rs and eval.rs leave every answer's trust path (#192, v0.32.0)

sw-verification

• VER-070 (verified) — The default path rests on the trusted term check — the tamper-hook negative control on every entry point, the term_map root resolution, the verdict scan, byte identity against the published v0.31.0, the cost table (TR-070)

Limitations in relation to the committed scope

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

Result of verification measures

Every delivered artifact carries verification evidence:

• TR-070 — 1 link(s), 0 source marker(s)
• VER-070 — 0 link(s), 7 source marker(s)

... (truncated)

Changelog

Sourced from ordeal's changelog.

[0.32.0] - 2026-10-15

Every answer rests on the term check (#192, TR-070). The proven query and term checks of v0.31.0 stop being opt-in: Solver::check, check_with_limit, check_with_deadline, check_with_witness, the sliver one-shots and the CLI's default output now return a verdict only after the trusted crate has related the assertions, flattened as asked, to the DAG the solver lowered them to (check_term_dag) and either re-encoded that DAG and checked the LRAT proof against the CNF it produced (check_query) or evaluated every root under the model and bound every model value through the term's variable map (check_query_model, check_input_value). canon.rs, dag.rs and eval.rs leave every answer's trust path. Output is byte-identical to v0.31.0: same verdicts, same certificate bytes, same models, no new JSON fields unless --with-term is given.

Changed

• One pipeline, one trusted gate (TR-070). Solver::solve_core replaces the three former pipelines (solve_pipeline, solve_witness and query_verdict / check_with_term on top of them): lower, search, then gate_unsat (check_term_dag + check_query, which checks the LRAT proof once; the solver's CNF is compared with the trusted re-encoding) or gate_sat (the eval.rs self-check kept as defence in depth, then check_term_dag, the CNF-level witness check, check_query_model and the per-value check_input_value). Every entry point is a projection of the same TermCheckResult: check keeps the certificate or model, check_with_witness the witness, check_with_query the query block, check_with_term all of it — so the opt-in entries now cost nothing beyond check. The CaDiCaL lane runs the same gate. Anything the trusted crate rejects degrades to Unknown on every entry point.
• dag::term_map resolves the map from the roots (found by the default-path verdict scan): two input constants with equal low bits are two DAG constant nodes, and a parent key can exist for both; the greedy first-hit choice refused queries at the root. On the new default path that would have been an Unknown regression. It also affects v0.31.0's opt-in --with-term / check_with_term: those return Unknown, never a wrong answer, on 6 of the 1000 queries of oracle::gen_corpus(0xC0FFEE, 1000) (q140, q150, q169, q216, q419, q620). This release decides all six. Every term node now keeps every candidate image with the operand images its key used, and the DAG's roots fix the choice top-down. The function takes the DAG's roots as a new parameter. The denotation guard and a new regression test cover it; the trusted check is unchanged.
• Still trusted, stated honestly (docs/formal-verification.md): the 1:1 flattening of the assertions into the term (dag::flatten), the variable names, the sliver lowering and the SMT-LIB / Verus front ends.

Added

... (truncated)

Commits

• 9074d1a chore(release): v0.32.0 — every answer rests on the proven term check (#192) ...
• daa7409 feat: #192 every answer rests on the proven term check — the default path run...
• 2847a2b chore(release): v0.31.0 — the answer is about the term as asked (#192 phase 7...
• c197a66 proof: #192 phase 7 — the answer is about the term as asked: check_term_dag p...
• bf269d9 chore(release): v0.30.0 — bounded sliver entry points (#236); the term-to-DAG...
• 8e5bdb5 test: #192 the term-to-DAG translation is checked against the evaluator (TR-0...
• 01d7335 chore(deps): Bump cadical-sys from 0.7.0 to 0.8.0 (#237)
• 181e9a7 feat(sliver): #236 bounded sliver entry points; the refusal stays visible; do...
• ca424f0 chore(deps): Bump serde_json from 1.0.151 to 1.0.154 (#238)
• 9f889f9 chore(release): v0.29.0 — both answers rest on the query (#192 phase 6); the ...
• 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)

[temper-pulseengine]

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

[github-actions]

🔒 HELD — not auto-mergeable (class: zerox-minor). 0.22.1 -> 0.32.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.