feat(verify): re-land native i64 rem value model behind a per-query solver deadline (closes #848)

[avrabe]

Closes #848. Supersedes #854 (which can be closed as superseded).

What

Two changes that belong together — the second is only safe because of the first.

1. A per-query wall-clock deadline on every SMT solve (the real insurance)

The #849 incident (4–6 h CI runs, every run for three days, Test and
Z3 Verification) happened because there was no wall-clock floor anywhere in
the stack. The existing conflict budget does not map to time, and — worse —
the div/rem trap VCs did not even go through the budgeted seam:
synth_verify::trap::prove_trap_* called ordeal::trap::prove_trap_*, which
delegates to the unbounded Solver::prove_valid. So the hardest VC class in
the whole validator had no bound at all.

Solver::check_with_deadline (ordeal ≥0.15) is now wired into both seams:

seam	before	after
solver::OrdealSolver::check	check_with_limit(1_000_000) conflicts	check_with_deadline(ms)
trap::prove_trap_{equivalence,condition_equivalence}	unbounded Solver::prove_valid	builds the same goal (ot::trap_equivalence_vc / ot::trap_condition_equivalence) and discharges it under the deadline
Z3 differential oracle	unbounded per-solver	z3 timeout param, same budget

Honest scope note: the trap VCs are ordeal-only by construction — they do
not go through new_solver, so SYNTH_SOLVER_DIFF never cross-checks them.
The CI Z3 Verification job hung in #849 because it runs the same ordeal
tests, not because Z3 was slow. The z3 timeout is defence in depth for the
value-VC path that does use the oracle. Routing trap VCs through the
differential seam is a named follow-up.

• Default 300 000 ms; override SYNTH_ORDEAL_DEADLINE_MS. 0 disables the
  deadline and falls back to the pre-existing SYNTH_ORDEAL_MAX_CONFLICTS
  conflict cap — ordeal's Bound is one-of (None | Conflicts | Deadline), so
  a query carries a deadline or a conflict cap, never both.
• Soundness: expiry yields CheckOutcome::Unknown →
  ValidationResult::Unknown / TrapVerdict::Unknown. An undecided query is
  never reported Verified/Preserved. ordeal's LRAT certificate gate and
  model self-check are untouched, so the bound costs completeness only.
• Documented limitation (in the code): check_with_deadline bounds the SAT
  search, not bit-blasting/canonicalization. A query whose blast alone is
  pathological can still exceed the budget before the clock is consulted. This
  is a strong bound on the dominant cost, not a universal wall-clock guard.
• Outer floor too: the CI Test and Z3 Verification jobs had no
  timeout-minutes — which is exactly why ordeal 0.12.0 solver-performance regression HANGS div/rem trap-preservation VCs — pinned back to 0.9.1 #849 cost days instead of minutes.
  Added (60 / 45).

Why 300 s and not the 10–15 s originally suggested

A tight budget converts a sound proof into a spurious Unknown. Measured here
(debug build, ordeal 0.16.1, dev host):

query	time
expansion_validator popcnt-HAKMEM link 1 (pre-existing)	40.6 s
all four re-landed i64-rem value+trap VCs (8 × 64-bit bvurem/bvsrem)	2.4 s

A 15 s default cut off the popcnt query — a genuinely hard but perfectly
decidable obligation, nothing to do with rem. 300 s is ~7× the measured pacer
(headroom for a slower, parallel-loaded CI runner) and still turns a solver
cliff from 6 hours into 5 minutes; the new timeout-minutes bounds the
aggregate.

2. Re-land the native i64 rem_u/rem_s value model (#844)

Reverts db0f1f2. ArmSemantics no longer HAVOCs the i64 remainder:
I64RemU/I64RemS compose the 64-bit operands from their register halves
(concat), apply the native bvurem/bvsrem, and split back to the rd pair,
with the ÷0 trap reconstructed from the pseudo-op's elide_zero_guard field.
verify_i64_rem_value_preservation asserts the full obligation (trap clause
and guarded value clause) against the ABI return pair R0:R1.

Safe to re-land now because ordeal 0.16.1 fixes both blast regressions —
signed bvsrem (ordeal#97) and unsigned bvurem (ordeal#101) — and the
deadline above is the standing insurance against the next cliff.

Evidence

Non-vacuity (this is the point of the value model) — the wrong-destination
lowering (rd = R2:R3 instead of the ABI R0:R1) is REJECTED; under HAVOC
it was accepted:

test translation_validator::tests::i64_rem_shipped_value_is_verified ... ok
test translation_validator::tests::i64_rem_wrong_destination_register_is_rejected ... ok
test translation_validator::tests::i64_rem_destination_field_is_load_bearing ... ok
test translation_validator::tests::i64_rem_value_model_closes_a_trap_only_gap ... ok
test result: ok. 4 passed; 0 failed; finished in 2.42s

i64_rem_value_model_closes_a_trap_only_gap is the concrete discriminator: the
old trap-only VC returns Verified for the wrong-destination lowering while
the new value VC returns Invalid — opposite verdicts on the same input.

Deadline mechanism, red-first:
solver::tests::deadline_degrades_to_unknown_never_to_proven — a 1 ms budget on
a hard query (width-8 mul associativity, >30 s unbounded) must yield Unknown,
must not yield Unsat, and the reason must name the deadline; the same
construction at width 3 decides Unsat in ms, so the gate is not vacuous.

Suite timing — the hard gate (cargo test -p synth-verify, debug, dev host):

run	result	time
default (ordeal)	242 passed / 0 failed	37.5 s + 0.33 s + 0.39 s ≈ 38 s
--features z3-solver,arm	244 passed / 0 failed	38.5 s + 0.33 s + 0.39 s ≈ 39 s
--features z3-solver,arm + SYNTH_SOLVER_DIFF=1	244 passed / 0 failed, 0 solver disagreements, 0 ordeal-Unknown fall-throughs	≈ 39.5 s

No test runs anywhere near the 2-minute intolerance threshold; the pacer is the
pre-existing popcnt query, not rem.

Byte-invisible: verify-only change, no codegen path touched;
cargo test -p synth-cli --test frozen_codegen_bytes 10/10 unchanged.

The 64-bit rem_u VC shape

The re-landed rem_u VC is a direct bvurem-vs-bvurem equivalence, not a
bvurem-vs-multiplicative-reconstruction one: both sides of the value clause
build the identical concat of the same four 32-bit half-symbols and apply
bvurem, so the valid case is structural. The hard work is the guarded-value

• trap-equivalence conjunction over the 64-bit bvurem blast and the
  wrong-destination Sat search — which is what used to cross circuits.
  On 0.16.1 the whole class decides in 2.4 s.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

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

Files with missing lines	Patch %	Lines
crates/synth-verify/src/translation_validator.rs	91.54%	12 Missing ⚠️
crates/synth-verify/src/solver.rs	96.66%	2 Missing ⚠️
crates/synth-verify/src/trap.rs	90.00%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!

[avrabe]

Independent verification (fresh worktree, re-verified from scratch)

The authoring agent died on a session limit before its gate ran, so nothing below is inherited — every number was re-measured on feat/i64-rem-deadline-848 merged with origin/main (62d45bf, the #866 ordeal 0.16.1 hotfix). The merge was clean: the branch's own 40152e1 and main's 62d45bf are the same change, so nothing had to be reconciled.

1. THE HARD GATE — the suite runs fast (this is the whole point)

cargo test -p synth-verify (debug, dev host). Measured three ways, all agreeing:

binary	tests	test execution
unittests src/lib.rs	179	37.7 s
comprehensive_verification	53	0.33 s
trap_preservation	11	0.40 s
total	243	≈ 38 s, 0 failed

End-to-end cargo test -p synth-verify wall including cargo's freshness pass: 79 s. (The table above is from running the built test binaries directly, because several sibling lanes were contending for the same cargo lock and target volume — it is the clean signal. Two full cargo test invocations earlier gave 36.2 s / 38.8 s of execution, same band.)

Per-class breakdown of the re-landed model:

• the four correctness/destination i64-rem tests: 2.44 s (matches the CHANGELOG's 2.4 s claim exactly)
• the two deadline-mechanism tests: 0.03 s
• long pole of the whole suite is pre-existing and unrelated: expansion_validator::tests::popcnt_hakmem_formula_is_popcnt alone is 39.8 s. The i64-rem work is not visible in the suite wall.

No test anywhere near the 2-minute cliff threshold. ordeal 0.16.1 has no cliff on these queries. Verdict: PASS.

2. The z3 path builds and passes

Both the plain feature build and CI's exact differential invocation:

cargo test -p synth-verify --features z3-solver        → 244 passed, 0 failed (35.6 s)
cargo test -p synth-verify --features z3-solver,arm    → 245 passed, 0 failed (41.5 s)   <- CI's exact invocation, rebuilt after my test addition
SYNTH_SOLVER_DIFF=1 ... --features z3-solver,arm       → 244 passed, 0 failed (36.0 s)

bv_to_z3's BvTerm::Urem arm compiles and is exercised. (Z3_SYS_Z3_HEADER=/opt/homebrew/include/z3.h locally; CI uses /usr/include/z3.h.) I deliberately re-ran this after adding the test in step 3 — a feature-gated build is exactly where an unhandled match site hides.

3. Non-vacuity — verified, and then strengthened

The shipped gates do genuinely flip verdicts; I read the assertions and re-ran them:

• i64_rem_wrong_destination_register_is_rejected — rem written to R2:R3 instead of the ABI R0:R1 ⇒ Invalid. The VC seeds R0..R3 and reads back the fixed ABI pair, so arm_value is the untouched dividend while wasm_value is dividend % divisor — SAT, genuinely rejected, not a tautology.
• i64_rem_value_model_closes_a_trap_only_gap — the same input through the old trap-only VC returns Verified and through the new value VC returns Invalid. That is the accepted-under-havoc → rejected-now discriminator made executable rather than narrated.

Added in this review (7f6d579): the destination test pins the register file, not the arithmetic. A lowering that writes the right registers, preserves the ÷0 trap, and computes the wrong remainder would pass it. i64_rem_wrong_signedness_is_rejected closes that: rem_u lowered to the signed pseudo-op (and rem_s to the unsigned one), correct ABI destination. Both come back Invalid with exactly the expected counterexamples —

rem_u-as-rem_s => Invalid { dividend_hi: 4099844512 (sign bit set), ... }
rem_s-as-rem_u => Invalid { divisor_hi: 4294967295, divisor_lo: 2147483648, ... }

— a negative dividend and a negative divisor, the only region where bvurem and bvsrem differ. That is a strictly stronger claim than the destination gate and could not pass under HAVOC. Cost: ~23 s of SAT search (12× under the deadline), but free in suite wall-clock — it runs behind the 39.8 s popcnt proof; lib suite went 38.8 s → 36.2 s (noise).

4. Deadline soundness — read against ordeal's own source, not just synth's

Traced ordeal-0.16.1/src/solver.rs + sat.rs:

• check_with_deadline(ms) → solve_pipeline(Bound::Deadline) → on expiry Pipeline::Unknown → CheckResult::Unknown → CheckOutcome::Unknown → ValidationResult::Unknown / TrapVerdict::Unknown. No path turns an expired query into Verified/Preserved. Confirmed at every consumer (translation_validator.rs:254, validator_pattern.rs:1196, fact_spec.rs ×8, expansion_validator.rs:1471).
• The certificate re-check in trap::verdict is untouched, so the bound costs completeness only.
• The documented limitation is accurate, and I verified it against the source: solve_pipeline runs canonicalization, blast_bool and tseitin before the Bound is ever consulted (solver.rs:715-731), and the deadline is then polled at the per-conflict site only (sat.rs:399). So it bounds the SAT search, not bit-blasting, exactly as the PR says. The Bound enum is genuinely one-of (None | Conflicts | Deadline) — the deadline-XOR-conflict-cap wording is correct too.
• The doc's check_with_deadline(0) note ("admits only queries decided before the first conflict") is also exactly right: the check sits after conflicts += 1, so propagation-only decisions still land.

Mechanism non-vacuity — the one thing the committed test cannot show. deadline_degrades_to_unknown_never_to_proven asserts Unknown at 1 ms with a width-3 control at the other end, which rules out a malformed goal but not "ordeal returns Unknown for this shape at any budget". I probed the same query across budgets (throwaway, not committed):

budget=1ms       elapsed=3.2ms      Unknown("... wall-clock deadline 1 ms")
budget=2000ms    elapsed=2.002s     Unknown("... wall-clock deadline 2000 ms")
budget=20000ms   elapsed=20.014s    Unknown("... wall-clock deadline 20000 ms")
budget=120000ms  elapsed=120.035s   Unknown("... wall-clock deadline 120000 ms")

Elapsed tracks the budget to within 35 ms at 120 s. The deadline is doing real wall-clock enforcement — the gate is not vacuous. (Also: the width-8 instance is >120 s hard, not the ">30 s" the comment claims — understated, so harmless.)

5. Is 300 s justified? Yes — with one caveat worth stating

Measured pacers on this host: slowest legitimate query is popcnt-HAKMEM at 39.8 s; the new signedness SAT search is 23 s; the i64-rem UNSAT VCs are sub-second. 300 s is ~7.5× the slowest legitimate query. A ubuntu-latest runner under load is plausibly 1.5–3× slower, so the real headroom is ~2.5–5×. Tightening to, say, 120 s would sit only ~1–2× above the CI-side popcnt time — and the failure mode of a too-tight deadline is bad: a spurious Unknown silently degrades a real proof, and under SYNTH_SOLVER_DIFF=1 an ordeal Unknown falls through to Z3, quietly reducing the differential to Z3-only without failing. For a verification tool, erring long is the right side to err on. Endorsed as-is.

Caveat, stated plainly rather than fixed: the per-query deadline does not bound the aggregate. A future cliff that hits a whole VC class (say 8 queries × 300 s = 40 min) still exceeds what the Test job can absorb — the timeout-minutes is what actually caps that. Confirmed both outer guards are in place and on the right jobs: Test = 60 min (ci.yml:26), Z3 Verification = 45 min (ci.yml:202) — confirmed by parsing the YAML, not by eyeballing indentation. The PR says exactly this; no overclaim.

The honest-scoping commit is also correct: the trap VCs build ordeal::Solver directly and never route through new_solver, so SYNTH_SOLVER_DIFF really does not cross-check them — the Z3 job hung on ordeal queries. Verified by reading trap::prove_valid_bounded.

6. Byte-invisibility and hygiene

cargo test -p synth-cli --test frozen_codegen_bytes   → 10 passed, 0 failed  (ARM + RV32 bit-identical oracles, all 8 escape hatches)
python3 scripts/claim_check.py claims.yaml            → 25/25 claims hold
cargo fmt --all --check                               → clean
cargo clippy --workspace --all-targets -- -D warnings → clean (0 errors, 0 warnings)

Frozen 10/10 confirms the verify-only claim: .text is untouched.

CHANGELOG re-read against the code: accurate, no overclaiming. I extended the non-vacuity paragraph to cover the new arithmetic-level gate and corrected "the four i64-rem tests" to name what those four actually cover.

What I changed

1. Merged origin/main (fix(main): restore BvTerm::Urem arms for ordeal 0.16.1 + latent ord_bv panic + hold 0.x-minor dependabot bumps #866) — clean, no reconciliation needed.
2. Added i64_rem_wrong_signedness_is_rejected + CHANGELOG (7f6d579) — the value model now has an arithmetic-level red-first gate, not only a register-level one.

Nothing was weakened to make anything pass. Not merged — evidence only.

[avrabe]

Addendum — the CI evidence, which beats any local measurement

All 46 checks pass on the final head (7f6d579). The two that matter here are the two that burned 4–6 hours each in #849, on a real ubuntu-latest runner:

job	#849	this PR
Test	4–6 h, timed out on the GitHub default, every run for three days	5 m 02 s (05:17:01Z → 05:22:03Z)
Z3 Verification	hung alongside it on the same ordeal queries	1 m 49 s (05:22:38Z → 05:24:27Z)

That is the gate. The native i64-rem value model is back and the suite is fast on the machine class where it previously hung — 5 m against a 60 m outer guard, ~12× margin. Claim Check (25/25), Clippy, Format, Bazel Build & Proofs, Kani Verification, Code Coverage and all 30-odd differential oracles are green too.

Recommendation: this is safe to merge. Not merging, per instructions.

Local hygiene note, unrelated to the change: my cargo test --workspace run hit No space left on device on the shared build volume (100 % full — 233 GB of it is devcache.sparseimage, the rest lane target dirs; several lanes hit it at once). I reclaimed my own trees and re-ran; the per-crate suites, frozen anchors, workspace clippy and the whole CI matrix are the authoritative signal here, and all are green.