[avrabe]

chore(deps): bump ordeal =0.22.1 -> =0.36.0 and teach synth-verify the five 0.28 derived-op nodes

Refs #1693. Refs #1590.

This PR supersedes dependabot #1693, which bumps ordeal to 0.36.0 and fails 4 checks, and dependabot #1590, the earlier 0.34.0 attempt. The version is the same as #1693's, with the API breaks repaired and measured evidence attached. The pin stays exact (=).

Why #1590 failed

The failures had one cause. ordeal 0.28 (#192 phase 5) admitted bvnot, bvneg, bvrotl, bvsdiv and bvsrem to the closed fragment as their own BvTerm nodes, each with a Lean-proven blasting rule. ordeal::lowering::* now returns those nodes instead of a rewrite into core ops. synth-verify's loud catch-all in canonicalize_bv (term.rs:310) fired on them, which caused all 15 panics in Test and in Z3 Verification. It fired as designed, so no verdict was ever minted over an unmodeled node. The mutation survey red on #1590 was a runner shutdown (The runner has received a shutdown signal), not a finding.

Changes

• crates/synth-verify/src/term.rs
  • bv_rank: unique ranks 19..23 for Not/Neg/Rotl/Sdiv/Srem. They are appended, so no existing commutative operand order, and therefore no CNF, moves.
  • ord_bv: same-variant arms for all five.
  • canonicalize_bv: recurses into the children and never reorders operands, because none of the five commutes.
  • fmt_bv: real SMT-LIB mnemonics.
• crates/synth-verify/src/solver.rs: the Z3 oracle maps the five nodes to Z3's native bvnot/bvneg/bvrotl/bvsdiv/bvsrem (bvsrem, not bvsmod). The oracle therefore checks ordeal's composite rules against an independent implementation.
• Every loud catch-all stays.
• Cargo.toml: the pin rationale is extended. Cargo.lock gains ordeal-cert 0.36.0, the certificate types split out in 0.36 and re-exported at their old paths, and ordeal-lrat moves to 0.36.0.
• Bazel: crates/BUILD.bazel references @crates//:ordeal, which crate.from_cargo reads from Cargo.lock. MODULE.bazel.lock lists no ordeal entry, so there was nothing to edit.

Other upstream changes read in CHANGELOG 0.23 to 0.36:

• From 0.32, the trusted term-DAG and query re-check runs on every check*. A trusted rejection degrades to Unknown, never to a wrong answer.
• 0.34 changes the QueryTerm::flatten signature. 0.36 moves flatten to a trait. synth uses neither.
• No other API that synth uses changed: Solver::new/assert/check/check_with_limit/check_with_deadline, CheckResult, Model, ordeal::trap::* and ordeal::eval::*.

Evidence: ordeal 0.22.1 vs 0.36.0, same machine, same commands

	0.22.1	0.36.0
cargo test -p synth-verify --no-fail-fast	276 pass / 0 fail	276 / 0
... --features z3-solver,arm (CI Z3 job)	278 / 0	278 / 0
serial ordeal+Z3 differential, SYNTH_SOLVER_DIFF=1 --test-threads=1, per-test verdict sequence	182 tests, 1283 verdicts	identical (diff empty)
differential pairs (unsat/unsat, sat/sat, disagreements)	476 / 79 / 0	476 / 79 / 0
ordeal-only trap path (unsat / sat)	94 / 59	94 / 59
synth-cli --features verify solver tests (6 binaries)	29 / 0	29 / 0
synth-backend solver-heavy tests (i64_expansion_certification, issue_1055_reread_window)	12 / 0	12 / 0

40 of the differential queries on 0.36.0 carry a Rotl (39) or Sdiv (1) node, so the new Z3 arms are exercised by the real suite. Srem and Neg reach the seam only through the controls below.

Planted miscompiles. These were applied to a scratch state, never committed, and reverted with git diff crates/ empty afterwards. Each was run under ordeal alone and under the ordeal+Z3 differential, on both versions. The results are identical across versions.

• ARM ADD modelled as SUB: verify_i32_add gives Invalid, counterexample input_1 = 0xC0000000. Z3 agrees (sat/sat).
• ARM ROR modelled as ROTL, which puts a Rotl node on both sides: verify_i32_rotl_transformation gives Invalid, counterexample 0x80000000. Z3 agrees.
• ARM SDIV modelled as UDIV: verify_i32_div_s is rejected by the trap gate. That path is ordeal-only, so Z3 does not see it, and it is reported here as such.
• Seam controls for all five nodes, at widths 8 and 32:
  • True identities give Unsat: a = (a sdiv b)*b + (a srem b), neg a = not a + 1, rotl(a,b) = rotr(a,-b).
  • Planted ones give Sat: sdiv as udiv, srem as urem, neg as not, rotl as rotr, and the srem identity with udiv.
  • All agree with Z3 on both versions.

Timing. These are exec times with binaries prebuilt, on a shared machine.

	0.22.1	0.36.0
synth-verify serial differential	81 s	73 s
synth-verify z3-solver,arm (parallel)	47 s	41 s
issue_1055_reread_window	66.8 s	67.8 s / 70.5 s

One 0.36.0 reading of issue_1055_reread_window was 93.5 s, taken under load average 19 on 10 cores. A re-run gave 67.8 s and 70.5 s. No query lost its bound: the seam and trap.rs still call check_with_deadline, unchanged.

Rebased onto z3 0.22.0 (#1702)

The evidence above was measured on a base with z3 0.21.1. This branch is now rebased onto ef9897c, which carries z3 0.22.0 / z3-sys 0.14.1. The rebase was clean, cargo metadata --locked accepts the merged Cargo.lock, and on the rebased head:

• cargo test -p synth-verify --no-fail-fast: 276 pass / 0 fail.
• cargo test -p synth-verify --features z3-solver,arm --no-fail-fast: 278 / 0.
• cargo fmt --check and cargo clippy --workspace --all-targets -- -D warnings: clean.
• cc_sweep.py: steps=55 failures=0.

The serial ordeal+Z3 verdict-sequence differential and the planted-miscompile controls were not re-run against z3 0.22.0.

Gates (local)

• cargo fmt --check, cargo clippy --workspace --all-targets -- -D warnings: clean.
• cargo test --workspace --no-fail-fast: 3271 passed / 0 failed (288 s).
• python3 scripts/mutation_survey.py ci: MUTANTS-CI subset=10 controls=3 non-killed=7 failures=0; ci_mutants_gate.py ok; mutant_residue_check.py residue=0; afterwards pgrep -fl mutation_survey empty and git diff crates/ empty.
• Claim Check sweep (cc_sweep.py): steps=55 failures=0. The commit subject is deliberately chore(deps): ...: a lane-shaped v0.91 ORDEAL: subject reds R10-lane because no RQ-91-ORDEAL artifact exists. Keep the PR title chore(deps): ... too, or add the artifact first.

The z3-feature build still warns unused import: z3::ast::Ast (solver.rs:257). That warning is pre-existing on 0.22.1 and is not touched here.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 34.78261% with 15 lines in your changes missing coverage. Please review.

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

📢 Thoughts on this report? Let us know!