fix: bvurem VCs hung — multiplicative native Urem blast + re-proof (#101) - #102
Merged
Conversation
…cative (#101) The unsigned twin of #97, reported by synth attempting to un-pin: their verify_i32_rem_u (Urem vs a - (a udiv b)*b, 32-bit symbolic) ran over 7 m 48 s on 0.16.0 (killed); the signed siblings were fast. #97's fix covered the DERIVED bvsrem lowering; direct users of the native BvTerm::Urem enum still hit the restoring divider's remainder — the same divider-vs-multiplier cross-circuit class. FIX AT THE BLAST LEVEL so enum users and lowerings both benefit: the term-level op stays native (synth keeps BvTerm::Urem); its CIRCUIT is now `blast_sub(a, blast_mul(blast_udiv(a, b), b))`. Exact for ALL inputs including /0 with no special case (SMT-LIB `a udiv 0` is all-ones, and all-ones * 0 = 0, so the result is a — exactly bvurem by zero; the 0.9.1 derived form relied on the same identity). measured, synth's #101 VC shape (32-bit, symbolic): divider-remainder blast: over 7 m 48 s, killed (synth) multiplicative blast: UNSAT in 5.2 ms Correctness re-verified: exhaustive width-8 blast-vs-evaluator and the SMT-LIB-reference family suites pass; the Kani urem harnesses now prove the NEW circuit against the same reference. #101 regression guard added (the VC shape under a 10 s deadline, like the #97 guard). blast_kernel.rs mirrors the new rule and BlastKernel.lean is regenerated; BlasterDiv's blast_urem_bitvec theorem is being re-proven against the new composition (a follow-up commit on this branch — the build is RED at BlasterDiv until it lands, which is the CI sorry-budget gate doing its job on a changed encoding). Fixes: #101 Trace: skip Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1
) blast_urem_bitvec re-proven for the new composition (udiv -> mul -> sub), SAME headline (output denotes A % B, all widths). The one new mathematical fact, umod_eq_sub_smtUDiv_mul (A % B = A - A.smtUDiv B * B, ALL B including 0), is proven from core lemmas — the /0 case rides umod_zero/smtUDiv_zero/mul_zero. Capacity hypothesis updated to the composition's proven counts (12w^2+8w + 10w^2 + 9w). blast_udiv_bitvec and every other theorem untouched (byte-identical per diff). CLEAN-ROOM VERIFIED: cold lake build 1707 jobs green (upstream baseline sorries only), escape-grep empty, my own #print axioms = [propext, Classical.choice, Quot.sound] (the umod identity needs no Classical.choice), headline statement confirmed unchanged. The capstone invariant held through its first encoding change: the proof broke exactly when the circuit changed, and re-landed only when the new circuit was proven — which is the entire point of proof-coupling. Implements: TR-027 Trace: skip Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1
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.
Fixes #101 (the unsigned twin of #97; synth's
verify_i32_rem_u: >7m48s killed on 0.16.0).Fix at the blast level
BvTerm::Uremstays native (synth keeps the enum); its circuit is nowa − (a udiv b)·b— exact for all inputs including /0 with no special case (a udiv 0 = allOnes,allOnes·0 = 0). Measured on synth's VC shape: >7m48s → UNSAT in 5.2 ms. #101 regression guard added beside the #97 one (10s deadline vs ~5ms).The capstone held
Changing the encoding broke
blast_urem_bitvecexactly as designed — and it's re-proven against the new composition with the same headline (denotes A % B, all widths), via the newumod_eq_sub_smtUDiv_mulidentity (all B, including 0). Clean-room verified: 1707 jobs green, escape-grep empty, axioms = the 3 standard (the umod identity needs only 2).Correctness: exhaustive width-8 + SMT-LIB-reference suites green; Kani harnesses now prove the new circuit. 181 lib tests, clippy 0.
🤖 Generated with Claude Code
https://claude.ai/code/session_01EBJ6kdJ16E3hnsBbq9Lwf1