feat(verify): model i64.rem_u/rem_s with native BvTerm::Urem/bvsrem (was havoc)#844
Merged
Conversation
…add value+trap VC Replace the I64RemU/I64RemS HAVOC in arm_semantics with a real 64-bit remainder (native ordeal 0.12 BvTerm::Urem via BV::bvurem; signed via bvsrem). Compose the 64-bit operands from the pseudo-op's register halves, apply the remainder, split back to the rd pair. Add verify_i64_rem_value_preservation: a value+trap VC that seeds operands at the FIXED ABI arg registers (dividend R0:R1, divisor R2:R3), reads the result from the FIXED ABI return pair R0:R1 (not the op's rd fields, which would be vacuous), and asserts arm_value == 64-bit remainder guarded under non-trap via DefineOrTrap/prove_trap_equivalence. The div ops stay trap-condition-only (64-bit quotient value VC not well-posed). Whitelist I64RemU/I64RemS in exec_trap_subset_op so encode_sequence_br reaches the value model; the ÷0 ARM trap is field-derived (elide_zero_guard) since the bare pseudo-op carries no expanded UDF. VCR-VER lineage (#242); ordeal 0.12 #825/#836. VERIFY-ONLY, no codegen change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…ejected Prove the native BvTerm::Urem/bvsrem value model is load-bearing: - i64_rem_shipped_value_is_verified: correct R0:R1 lowering -> Verified - i64_rem_wrong_destination_register_is_rejected: rd=R2:R3 (ABI R0:R1 not the remainder) -> Invalid (was accepted under HAVOC) - i64_rem_destination_field_is_load_bearing: opposite verdicts (non-vacuous) - i64_rem_value_model_closes_a_trap_only_gap: EVIDENCE — the old trap-only VC accepts the wrong-dest lowering (Verified, value invisible) while the new value VC rejects it (Invalid); opposite verdicts on the same input. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
This was referenced Jul 22, 2026
Open
avrabe
added a commit
that referenced
this pull request
Jul 23, 2026
… — solver hang #844 replaced the I64RemU/I64RemS HAVOC in arm_semantics with a real 64-bit `dividend.bvsrem/bvurem(&divisor)`. That query is the hardest bitvector class there is, and it HANGS both solvers: the pure-Rust ordeal default (→ the CI "Test" job) and the Z3 differential (→ the "Z3 Verification" job). Both jobs have run 4-6h and timed out on EVERY CI run since #844 landed — the last green CI on main was 2026-07-20 (61acec9). Confirmed independently: the L8 rem test produced no output (hung) in salvage, and a separate agent's full workspace run reached 107 test binaries / 0 failures and stalled only on this synth-verify rem SMT test. This restores the pre-#844 havoc model (byte-invisible — verify-only, no codegen change, frozen anchors untouched by construction) to un-hang CI and unblock the v0.50.0 tag. Native i64 rem re-lands in v0.51 behind a per-query solver timeout so a hard bvurem degrades to `unknown` instead of hanging the whole suite. Tracking: #848 (re-land behind a per-query solver timeout). The term.rs/solver.rs BvTerm::Urem enum arms stay — they are the #836 ordeal-0.12 enum-completeness handlers (harmless; nothing in verify now generates the variant). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Jul 23, 2026
…GS CI ROOT CAUSE of the 4-6h CI hangs (both the ordeal-default Test job and the Z3 Verification job) that have red-mained `main` since 2026-07-20: the ordeal 0.9.1 -> 0.12.0 dependabot bump (#825). 0.12 has a solver-performance regression on bvsrem/bvsdiv that hangs div/rem trap-preservation VCs — even the pre-existing 32-bit `rems_single_zero_guard_is_exactly_right` (I32RemS Sdiv+Mls, #753/v0.43) hangs >240s on 0.12 but runs <1s on 0.9.1. The last GREEN CI on main (61acec9, 2026-07-20 21:45:27) used ordeal 0.9.1 — #825 merged 3 seconds later. NO commit with ordeal 0.12 has ever passed CI; every subsequent lane auto-merged on the required-gate subset while Test/Z3 timed out. #844 (native i64 rem via 0.12 bvsrem/bvurem) made it far worse and was reverted (db0f1f2, re-land #848); this pin is the actual fix. Changes: - crates/synth-verify/Cargo.toml: ordeal "0.12.0" -> "=0.9.1" (exact last-green pin; do-not-bump note added). Cargo.lock: ordeal + ordeal-lrat 0.12.0 -> 0.9.1. - Remove the four #836 `BvTerm::Urem` match arms (term.rs x3, z3-gated solver.rs x1) — that variant exists only in ordeal 0.12. Verified: `cargo test -p synth-verify` = 236 tests, 0 failed, ~41s (was >6h timeout on 0.12). Byte-invisible — verify-only, no codegen change, frozen anchors untouched by construction. Follow-ups (tracked, non-blocking): report the bvsrem/bvsdiv regression upstream to ordeal; tighten .github/workflows/dependabot-auto-merge.yml (#838) to HOLD 0.x MINOR bumps (0.9->0.12 is breaking by 0.x semver but dependabot classified it "minor" and auto-merged it). See #849. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe
added a commit
that referenced
this pull request
Jul 23, 2026
… =0.9.1 pin (#849) #844's native i64 rem value model was reverted (it depended on ordeal 0.12, which has the bvsrem/bvsdiv perf regression that hangs CI). The real v0.50.0 change is the ordeal =0.9.1 pin. Do not advertise a reverted feature. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
v0.50 Lane 8 — puts the ordeal 0.12 upgrade to work in translation validation.
Gap:
arm_semantics.rsmodeled ARM i64.rem_u/rem_s as HAVOC (fresh uninterpretedi64_remu_lo/hiconsts) — the validator could prove NOTHING about an i64 remainder result. Fix: model both with the nativeBvTerm::Urem/bvsremterms (ordeal 0.9→0.12 #825, plumbed via #836), with the ÷0 TRAP handled explicitly (WASM traps on zero divisor — not silently produce a value). Adds value + trap VCs and a non-vacuity gate (a wrong-dest lowering is now REJECTED — was accepted under havoc).Verify-only lane: frozen 10/10 byte-identical (zero codegen change), claim_check 25/25, synth-verify builds clean (default/ordeal). The Z3-differential side is gated by CI's required Z3 Verification job (the #836 lesson — the z3-solver feature build is a separate gate; merge is name-conditioned on it going green).
Salvaged: the authoring agent completed the implementation + non-vacuity test + committed, then died on a platform rate-limit waiting on the slow z3-solver build. Re-verified frozen/claims/build from scratch before this PR; CI's ordeal + Z3 jobs are the authoritative solver gates.
🤖 Generated with Claude Code