feat: udiv/urem bitblasting #18
Closed
Conversation
This file contains 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
alexkeizer
reviewed
Aug 29, 2024
alexkeizer
requested changes
Aug 29, 2024
src/Init/Data/BitVec/Bitblast.lean
Outdated
Comment on lines
437
to
441
| /- | ||
| r = n - d * q | ||
| r = n - d * (∑ i, 2^i * q.getLsb i) | ||
|
|
||
| -/ |
There was a problem hiding this comment.
This comment should either go, or have a bit more context
src/Init/Data/BitVec/Bitblast.lean
Outdated
Comment on lines
444
to
458
| /-! | ||
| Let us study an instructive counterexample to the claim that | ||
| `n = d * q + r` for (`0 ≤ r < d`) uniquely determining q and r *over bitvectors*. | ||
|
|
||
| - Let `bitwidth = 3` | ||
| - Let `n = 0, d = 3` | ||
| - If we choose `q = 2, r = 2`, then d * q + r = 6 + 2 = 8 ≃ 0 (mod 8) so satisfies. | ||
| - But see that `q = 0, r = 0` also satisfies, as 0 * 3 + 0 = 0. | ||
| - So for (`n = 0, d = 3`), both: | ||
| `q = 2, r = 2` as well as | ||
| `q = 0, r = 0` are solutions! | ||
|
|
||
| It's easy to cook up such examples, by chosing `(q, r)` for a fixed `(d, n)` | ||
| such that `(d * q + r)` overflows. | ||
| -/ |
There was a problem hiding this comment.
It wouldn't hurt to have a bit more context to this counter-example, why do we care?
src/Init/Data/BitVec/Bitblast.lean
Outdated
Comment on lines
467
to
472
| /-- TODO: This theorem surely exists somewhere. -/ | ||
| theorem Nat.div_add_eq_left_of_lt {x y z : Nat} (hx : z ∣ x) (hy : y < z) (hz : 0 < z): | ||
| (x + y) / z = x / z := by | ||
| refine Nat.div_eq_of_lt_le ?lo ?hi | ||
| · apply Nat.le_trans | ||
| · exact div_mul_le_self x z | ||
| · omega | ||
| · simp only [succ_eq_add_one, Nat.add_mul, Nat.one_mul] | ||
| apply Nat.add_lt_add_of_le_of_lt | ||
| · apply Nat.le_of_eq | ||
| exact (Nat.div_eq_iff_eq_mul_left hz hx).mp rfl | ||
| · exact hy |
There was a problem hiding this comment.
Could you double check whether it exists? If not, this should be moved to a more appropriate file
src/Init/Data/BitVec/Bitblast.lean
Outdated
| -/ | ||
|
|
||
|
|
||
| /-- TODO: This theorem surely exists somewhere, but I can't find it. -/ |
There was a problem hiding this comment.
This needs to move into its place. And you can probably drop this comment if you cannot find it.
There was a problem hiding this comment.
@tobiasgrosser It feels a bit too special case to move into Nat, but I'm happy to move it...
There was a problem hiding this comment.
Also, there are too many linebreaks before this theorem.
src/Init/Data/BitVec/Bitblast.lean
Outdated
| case succ n ih => | ||
| simp only [sshiftRightRec_succ_eq, and_twoPow, ih] | ||
| by_cases h : y.getLsb (n + 1) | ||
| · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsb_true h, | ||
| sshiftRight'_or_of_and_eq_zero (by simp), h] | ||
| simp | ||
| · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsb_false (i := n + 1) | ||
| (by simp [h])] | ||
| (by simp only [h])] |
There was a problem hiding this comment.
The changes in this file are unrelated and actually not needed. Drop them?
alexkeizer
reviewed
Sep 4, 2024
alexkeizer
reviewed
Sep 4, 2024
src/Init/Data/BitVec/Bitblast.lean
Outdated
Comment on lines
595
to
606
| /-! | ||
| A `LawfulShiftSubtract` is a `Lawful` DivModState that is also a legal input to the shift subtractor. | ||
| So in particular, we must have at least one dividend bit left over `(0 < wn)` | ||
| to perform a round of shift subtraction. | ||
| -/ | ||
|
|
||
| /-- | ||
| The input to the shift subtractor is a legal input to `divrem`, and we also need to have an | ||
| input bit to perform shift subtraction on, and thus we need `0 < wn`. | ||
| -/ | ||
| structure DivModState.LawfulShiftSubtract (w wr wn : Nat) (n d : BitVec w) (qr : DivModState w) | ||
| extends DivModState.Lawful w wr wn n d qr : Type where | ||
| /-- Only perform a round of shift-subtract if we have dividend bits. -/ | ||
| hwn_lt : 0 < wn |
There was a problem hiding this comment.
Just merge this into a single docstring
alexkeizer
reviewed
Sep 4, 2024
alexkeizer
reviewed
Sep 4, 2024
…into upstream-div-alt
refactor: bundle `wn` and `wr` into DivModState
Co-authored-by: Tobias Grosser <[email protected]>
Sorry this is coming through in tiny pieces; I'm still hitting a bootstrapping problem and getting things through piecemeal to localise it.
Fixes a mixed up between the parameter and global variable for `json_output` the occurred during some name juggling in leanprover#3939.
Update the Lake-specific package configuration with the proper root for the executable (after leanprover#5143).
This should be tested against Mathlib, but there are conflicts with the `nightly-with-mathlib` branch right now, so I'll wait until tomorrow.
…iftLeft_and_shiftLeft, one_shiftLeft_mul] (leanprover#5469) Co-authored-by: Tobias Grosser <[email protected]>
Just saw some bad markdown, thought I’ll quickly fix it.
building upon leanprover#3714, this (almost) implements the second half of leanprover#3302. The main effect is that we now get a better error message when `rfl` fails. For ```lean example : n+1+m = n + (1+m) := by rfl ``` instead of the wall of text ``` The rfl tactic failed. Possible reasons: - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma). - The arguments of the relation are not equal. Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or `exact HEq.rfl` etc. n m : Nat ⊢ n + 1 + m = n + (1 + m) ``` we now get ``` error: tactic 'rfl' failed, the left-hand side n + 1 + m is not definitionally equal to the right-hand side n + (1 + m) n m : Nat ⊢ n + 1 + m = n + (1 + m) ``` Unfortunately, because of very subtle differences in semantics (which transparency setting is used when reducing the goal and whether the “implicit lambda” feature applies) I could not make this simply the only `rfl` implementation. So `rfl` remains a macro and is still expanded to `eq_refl` (difference transparency setting) and `exact Iff.rfl` and `exact HEq.rfl` (implicit lambda) to not break existing code. This can be revised later, so this still closes: leanprover#3302. A user might still be puzzled *why* to terms are not defeq. Explaining that better (“reduced to… and reduces to… etc.”) would also be great, but that’s not specific to `rfl`, so better left for some other time.
We make sure that we can pull `List.toArray` out through all operations (well, for now "most" rather than "all"). As we also push `Array.toList` inwards, this hopefully has the effect of them cancelling as they meet, and `simp` naturally rewriting Array operations into List operations wherever possible. This is not at all complete yet.
Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
We introduce bitblasting lemmas for
udivandumod, which builds the circuit that computesudivandumodas a shift-subtracter circuit. We follow the Bitwuzla implementation closely, and prove their algorithm correct by means of the standard division recurrence.