feat: add BitVec multiplication simp lemmas #6718
Conversation
This PR adds BitVec lemmas required to cancel multiplicative negatives, and plumb support through to bv_normalize to make use of this result in the normalized twos-complement form. I include some bmod lemmas I found useful to prove this result, the two helper lemmas I add use the same naming/proofs as their emod equivalents.
| @@ -88,6 +88,14 @@ example {x : BitVec 16} : x / (BitVec.ofNat 16 8) = x >>> 3 := by bv_normalize | |||
| example {x y : Bool} (h1 : x && y) : x || y := by bv_normalize | |||
| example (a b c: Bool) : (if a then b else c) = (if !a then c else b) := by bv_normalize | |||
|
|
|||
| -- neg_mul' / mul_neg' | |||
| example (x y : BitVec 16) : (-x) * y = -(x * y) := by bv_normalize | |||
There was a problem hiding this comment.
It seemed useful to me to have both the normalized and unnormalized forms, but happy to reduce this to just the normalized if you prefer.
There was a problem hiding this comment.
I think this is fine but please also add test cases for the symmetric variants mentioned above.
|
This is rows 181/182 of the spreadsheet. |
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
| theorem add_bmod_eq_add_bmod_right (i : Int) | ||
| (H : bmod x n = bmod y n) : bmod (x + i) n = bmod (y + i) n := by | ||
| rw [← bmod_add_bmod_congr, ← @bmod_add_bmod_congr y, H] | ||
|
|
||
| theorem bmod_add_cancel_right (i : Int) : bmod (x + i) n = bmod (y + i) n ↔ bmod x n = bmod y n := | ||
| ⟨fun H => by | ||
| have := add_bmod_eq_add_bmod_right (-i) H | ||
| rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this, | ||
| fun H => by rw [← bmod_add_bmod_congr, H, bmod_add_bmod_congr]⟩ |
There was a problem hiding this comment.
I haven't checked, but are there analogues of these for the other *mod variants? I would like to try to keep the discrepancy between the versions monotonically decreasing if possible. :-)
There was a problem hiding this comment.
Yes, as I mention in the commit message, these two are direct copies of their emod equivalents in both name and proof. bmod_neg_bmod is new as there isn't
| @@ -257,6 +257,14 @@ theorem BitVec.add_const_right' (a b c : BitVec w) : (a + b) + c = (b + c) + a : | |||
| attribute [bv_normalize] BitVec.mul_zero | |||
| attribute [bv_normalize] BitVec.zero_mul | |||
|
|
|||
| @[bv_normalize] | |||
| theorem BitVec.neg_mul' (x y : BitVec w) : (~~~x + 1#w) * y = ~~~(x * y) + 1#w := by | |||
There was a problem hiding this comment.
As a general principle, unless there is a clear local convention, I would like all theorems with primes in their names to have a doc-comment explaining the naming convention / name clash / difficulty in naming.
There was a problem hiding this comment.
@hargoniX can comment here as to his convention for the bv_normalize code, as I think I'm following his local convention. (The lemma is specifically applied to the normalized form where negation has been expanded to twos complement, and isn't 'user-facing' in that sense.)
There was a problem hiding this comment.
These lemmas should be named neg_mul (note that they exist in their own namespace separate from regular BitVec theory so you can reuse the name). The reason that there is ' lemmas above is that you also need to match on (1#w + ~~~x) * y = ~~~(x * y) + 1#w. This is what the symmetries remark in the spreadsheet is alluding to. If you read the Bitwuzla code you will see they have a function is_bv_neg https://github.com/bitwuzla/bitwuzla/blob/main/src/rewrite/rewriter.cpp#L293 that checks for all these symmetries.
| example (x y : BitVec 16) : (~~~x + 1) * y = ~~~(x * y) + 1 := by bv_normalize | ||
| example (x y : BitVec 16) : x * (~~~y + 1) = ~~~(x * y) + 1 := by bv_normalize | ||
| example (x y : BitVec 16) : (~~~x + 1) * (~~~y + 1) = x * y := by bv_normalize | ||
|
|
There was a problem hiding this comment.
Is there a difference in the behaviour of bv_decide after adding these normalizations? If so, can we have a test demonstrating it?
There was a problem hiding this comment.
That's a good question, I don't think there is an easily testable difference from bv_decides perspective.
There was a problem hiding this comment.
In general the idea here is mostly to copy what Bitwuzla is doing, given that Bitwuzla has done extensive experimentation with rewrites on BitVec it is likely that these rules are good for us. The purpose is mostly to reduce the pressure on the SAT solver/bitblaster further below. So for example when we have (~~~x + 1) * y and x * (~~~y + 1) in our goal somewhere these were previously mostly distinct multiplication circuits that the SAT solver had to reason about but they are now shared.
In the past the approach to verify that these rules actually bring benefit in practice ™️ has been to run it against SMTLIB on the Stanford cluster and observe speedups, though that is a very expensive operation (takes about half a day) so we don't do that for every rule, just every now and then to see that the trend is going upwards.
This PR adds BitVec lemmas required to cancel multiplicative negatives, and plumb support through to bv_normalize to make use of this result in the normalized twos-complement form.
I include some bmod lemmas I found useful to prove this result, the two helper lemmas I add use the same naming/proofs as their emod equivalents.