[BLOCKED] ordeal un-pin 0.9.1→0.16: bvsrem fixed but bvurem still hangs i32 rem_u — keep pinned by avrabe · Pull Request #854 · pulseengine/synth

avrabe · 2026-07-23T17:49:08Z

STATUS: BLOCKED — do not merge. ordeal 0.16 fixed `bvsrem` but NOT `bvurem`, and the deadline does not bound it.

This PR un-pins ordeal =0.9.1 → 0.16.0, wires a per-query wall-clock deadline, and re-lands the native i64 rem_u/rem_s value model (#844). The un-pin is not clean and this PR must not merge as-is.

The blocker (measured, decisive)

The pre-existing i32 verify_i32_rem_u VC (tests/comprehensive_verification.rs, present + fast at the last-green baseline 61acec99) proves the full rem_u(a,b) = a − (a/b)·b equivalence — a cross-circuit bvurem-vs-(bvsub, bvudiv, bvmul) bit-blast. On ordeal 0.16 it does not decide in bounded time:

0.9.1 baseline (commit 4ad175e): whole -p synth-verify suite = 236 tests, ~41 s, green.
0.16, isolated, deadline disabled (SYNTH_ORDEAL_DEADLINE_MS=0 → check_with_limit(1M), the exact path 0.9.1 used): verify_i32_rem_u ran >7 m 48 s and was killed without terminating.

The deadline does NOT save it (blast-bound, not SAT-bound)

Probed verify_i32_rem_u with SYNTH_ORDEAL_DEADLINE_MS=15000 and a hard 50 s wall timeout: the test binary reached execution and ran to the 50 s kill with no Unknown (wall-clock deadline 15000 ms) line and no result — i.e. the 15 s deadline never fired. ordeal 0.16's check_with_deadline doc says it bounds the SAT search, not blasting/canonicalization; bvurem's cost is in bit-blasting the circuit, which the deadline does not bound. So the deadline is correct insurance against a SAT-search cliff (like the div/rem trap VCs) but is ineffective against this bvurem blasting cliff — it would still hang the CI Test job.

Discriminator: signed fixed, unsigned still exponential

From the 0.16 run, the sibling VCs all pass fast — only rem_u is slow. Confirmed verify_i32_rem_s is the exact SIGNED twin (SDIV+MLS, same full rem_s = a−(a/b)·b equivalence, asserts Verified), so this is a clean symmetric discriminator:

verify_i32_div_u ... ok        # bvudiv
verify_i32_div_s ... ok        # bvsdiv
verify_i32_rem_s ... ok        # bvsrem — the PR#99/ordeal#97 fix works
verify_i32_rem_u ... >8 min, killed   # bvurem — still exponential, deadline ineffective

ordeal 0.16 fixed bvsrem/bvsdiv (signed — exactly the PR#99 / ordeal#97 claim) but bvurem (unsigned remainder) remains an exponential bit-blast. Reported upstream (ordeal#101).

What IS sound (for when upstream fixes bvurem)

The native i64 rem re-land (feat(verify): model i64.rem_u/rem_s with native BvTerm::Urem/bvsrem (was havoc) #844) is correct; its tests pass fast (the i64 rem value VC is structurally identical on both sides, not a hard cross-circuit equivalence).
The per-query deadline correctly bounds SAT-search cliffs and degrades to a conservative Unknown (never Verified). It just cannot bound a blasting cliff.
The un-pin is coupled: re-landing feat(verify): model i64.rem_u/rem_s with native BvTerm::Urem/bvsrem (was havoc) #844 requires 0.16 (BvTerm::Urem + check_with_deadline), so the good half can't be split from the blocked half.

Not exercised

The Z3 differential path (SYNTH_SOLVER_DIFF=1) was not run — the default ordeal-only Test job is already the blocker, so STOP was reached before the Z3 gate. (The same bvurem VC would be expected slow in Z3 too; not measured.)

Recommendation

Keep ordeal = "=0.9.1" pinned until upstream fixes the bvurem blasting regression (ordeal#101). Then re-adopt 0.16+ with this PR's deadline + #844 re-land. #848 and #849 stay open with this finding.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…-land native i64 rem The ordeal 0.12 bvsrem/bvsdiv solver-performance regression that HUNG the div/rem trap-preservation VCs (4-6h CI timeouts, #849) is fixed upstream (ordeal PR#99 / ordeal#97 — bvsrem is multiplicative again). 0.16.0 also adds `Solver::check_with_deadline(ms)`, a per-query wall-clock timeout — the real insurance against a future perf cliff. - crates/synth-verify/Cargo.toml + Cargo.lock: ordeal =0.9.1 -> 0.16.0 (pin-rationale comment rewritten). The lock's stale 0.50.0 path-dep versions sync to the workspace's 0.50.1 as a side effect. - solver.rs: wire ordeal `check_with_deadline` into `OrdealSolver` (default 10s, `SYNTH_ORDEAL_DEADLINE_MS`; 0 = fall back to the conflict budget). A conflict budget bounds SAT logic but NOT wall time — the 0.12 cliff hung queries while under the conflict limit. A deadline exhaustion is a conservative `Unknown`, never a verdict (the never-`Unknown`-to-`Verified` mapping is the soundness basis). Also give the Z3 differential oracle its own per-query timeout (`Params::set_u32("timeout", ms)`, default 10s, `SYNTH_Z3_TIMEOUT_MS`) — #848 records the 64-bit rem VC hanging Z3 too, and under `SYNTH_SOLVER_DIFF=1` the CI Z3 job runs z3.check() unconditionally. On Z3 timeout the DifferentialSolver keeps ordeal's cert-checked verdict (the "z3 unknown, keep ordeal" branch), degrading gracefully rather than red. - term.rs / z3-gated solver.rs: re-add the four #836 `BvTerm::Urem` match arms (bv_rank cost 5, canonicalize_bv rebuild, bvurem SMT-LIB formatter, z3 bvurem) — that variant exists only in ordeal 0.12+. - arm_semantics.rs / translation_validator.rs: re-land #844 (revert of revert db0f1f2) — native 64-bit `dividend.bvurem/bvsrem(&divisor)` value model for I64RemU/I64RemS + the value+trap VC and its non-vacuity gate (wrong-dest rejected). Now re-landed behind the deadline (the #848 acceptance shape). Verify-only, no codegen change — byte-invisible, frozen anchors untouched by construction. Full-suite fast-gate timing follows. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

…ot bvurem Investigation result (STOP, do not merge — PR #854 drafted): un-pinning ordeal to 0.16 and re-landing native i64 rem is NOT clean. Decisive measurement: the pre-existing i32 `verify_i32_rem_u` VC (full `rem_u(a,b) = a - (a/b)*b` equivalence, a cross-circuit `bvurem` bit-blast, present + fast at the last-green baseline 61acec9 / whole suite ~41s on 0.9.1) does NOT decide on ordeal 0.16 — ran >7m48s isolated with the deadline disabled and was killed. Under the 120s deadline it degrades to `Unknown`, and the test asserts `Verified` -> RED. Discriminator (from the 0.16 run): verify_i32_div_u / div_s / rem_s all pass FAST; only rem_u is slow. So 0.16 fixed bvsrem/bvsdiv (signed — the PR#99 / ordeal#97 claim) but bvurem (unsigned rem) is still exponential. - solver.rs: raise the deadline default 10s -> 120s (the slowest LEGITIMATE query, the 32-bit popcount HAKMEM fold, decides Unsat in ~41s; 120s gives headroom) and document the bvurem BLOCKER at DEFAULT_DEADLINE_MS. The Z3 timeout tracks at 120s. - CHANGELOG: replace the (premature) shipped-entry with a BLOCKED note — no [Unreleased] entry is claimed; ordeal stays pinned =0.9.1 until upstream fixes bvurem. The deadline wiring + #844 i64 re-land themselves are sound (i64 rem tests pass fast — structurally identical both sides); they are COUPLED to 0.16 (need BvTerm::Urem + check_with_deadline) so cannot ship split from the blocked bvurem half. Keep pinned; re-adopt when upstream lands a bvurem fix. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

avrabe · 2026-07-23T18:21:23Z

Upstream: filed pulseengine/ordeal#101 for the bvurem cliff. This PR stays a draft (do-not-merge) until ordeal#101 is fixed and released.

…urem cliff Follow-up probe: ran verify_i32_rem_u with SYNTH_ORDEAL_DEADLINE_MS=15000 and a hard 50s wall timeout. The 15s deadline NEVER FIRED — the test ran to the 50s kill with no `Unknown (wall-clock deadline 15000 ms)` line and no result. Per ordeal 0.16's `check_with_deadline` doc, the deadline bounds the SAT SEARCH but NOT blasting/canonicalization; bvurem's cost is in BLASTING the circuit, so the deadline is INEFFECTIVE against this specific cliff (it remains sound insurance against a SAT-search cliff, e.g. the div/rem trap VCs). Also confirmed verify_i32_rem_s is the exact SIGNED twin of the slow rem_u (same SDIV+MLS, same full rem=a-(a/b)*b equivalence, asserts Verified) — so signed-fast/unsigned-slow is a clean symmetric discriminator isolating the regression to bvurem. Corrected the code comment, CHANGELOG note, PR #854 body, and filed the detail on ordeal#101. Upstream tracker renumbered #97 -> #101 (new issue for the distinct unsigned regression; #97 was the closed signed one). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

avrabe changed the title ~~feat(#848/#849): un-pin ordeal 0.9.1→0.16.0 + per-query solver deadline + re-land native i64 rem~~ [BLOCKED] ordeal un-pin 0.9.1→0.16: bvsrem fixed but bvurem still hangs i32 rem_u — keep pinned Jul 23, 2026

avrabe marked this pull request as draft July 23, 2026 18:19

This was referenced Jul 23, 2026

ordeal 0.12.0 solver-performance regression HANGS div/rem trap-preservation VCs — pinned back to 0.9.1 #849

Open

Re-land native i64.rem_u/rem_s value model behind a per-query solver timeout (reverted #844) #848

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[BLOCKED] ordeal un-pin 0.9.1→0.16: bvsrem fixed but bvurem still hangs i32 rem_u — keep pinned#854

[BLOCKED] ordeal un-pin 0.9.1→0.16: bvsrem fixed but bvurem still hangs i32 rem_u — keep pinned#854
avrabe wants to merge 3 commits into
mainfrom
feat/ordeal-016-unpin-848

avrabe commented Jul 23, 2026 •

edited

Loading

Uh oh!

avrabe commented Jul 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

avrabe commented Jul 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

STATUS: BLOCKED — do not merge. ordeal 0.16 fixed bvsrem but NOT bvurem, and the deadline does not bound it.

The blocker (measured, decisive)

The deadline does NOT save it (blast-bound, not SAT-bound)

Discriminator: signed fixed, unsigned still exponential

What IS sound (for when upstream fixes bvurem)

Not exercised

Recommendation

Uh oh!

avrabe commented Jul 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

avrabe commented Jul 23, 2026 •

edited

Loading

STATUS: BLOCKED — do not merge. ordeal 0.16 fixed `bvsrem` but NOT `bvurem`, and the deadline does not bound it.