feat: add SMT-LIB overflow on addition for bitvectors (uadd_overflow,sadd_overflow, uadd_overflow_eq,sadd_overflow_eq) and support theorems
#6628
Conversation
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
changelog-library |
|
What are your plans for adding theorems about these? |
|
Ideally supporting them in bvdecide - although there are some proofs missing (they're taking me more time than I expected), so I'll draft the PR for now and open it when the proofs are done! |
|
Okay! I'm happy with these definitions, and checked them against the reference, so I'm happy to click merge as soon as we're sure they are going to be used. |
luisacicolini
changed the title
not_overflow,uadd_overflow,sadd_overflow,umul_overflow,smul_overflow)uadd_overflow,sadd_overflow, uadd_overflow_eq,sadd_overflow_eq)
Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Alex Keizer <[email protected]>
| decide_eq_decide, BitVec.toInt_add] | ||
| rw [bmod_two_pow_neg_iff (by omega) (by omega)] | ||
| rw_mod_cast [← @Nat.two_pow_pred_add_two_pow_pred w (by omega)] at * | ||
| omega |
There was a problem hiding this comment.
@luisacicolini, keep these theorems in Lemmas.lean. However, you should add a here lines attribute [bv_normalize] BitVec.saddOverflow_eq ....
src/Init/Data/BitVec/Lemmas.lean
Outdated
| @@ -542,6 +542,62 @@ theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by | |||
| theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by | |||
| simp [BitVec.toInt, show 0 < 2^w by exact Nat.two_pow_pos w] | |||
|
|
|||
| theorem toInt_lt {w : Nat} (x : BitVec w) : x.toInt < 2 ^ (w - 1) := by | |||
| simp only [BitVec.toInt, Nat.cast_pow] | |||
| by_cases hw : w = 0 | |||
There was a problem hiding this comment.
Would using cases or rcases remove the need for a subst here? Similarly, below.
There was a problem hiding this comment.
it should, will give it a try
Co-authored-by: Tobias Grosser <[email protected]>
|
Unfortunately, some theorems live in Mathlib and quite a few things break as a consequence. I'm specializing some of these to see whether we can continue using them, but would be great to just avoid them (and find alternative proof strategies) |
| @@ -3579,7 +3635,6 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) := | |||
| · simp [h] | |||
| · rw [Nat.sub_add_cancel (Nat.two_pow_pos (w - 1)), Nat.two_pow_pred_mod_two_pow (by omega)] | |||
|
|
|||
|
|
|||
There was a problem hiding this comment.
This seems unrelated.
luisacicolini
changed the title
uadd_overflow,sadd_overflow, uadd_overflow_eq,sadd_overflow_eq)uadd_overflow,sadd_overflow, uadd_overflow_eq,sadd_overflow_eq) and support theorems (toInt_lt, le_toInt, toInd_add_toInt_lt_two_pow, neg_two_pow_le_toInd_add_toInt, bmod_two_pow_neg_iff, emod_eq_add_self_emo)
luisacicolini
changed the title
uadd_overflow,sadd_overflow, uadd_overflow_eq,sadd_overflow_eq) and support theorems (toInt_lt, le_toInt, toInd_add_toInt_lt_two_pow, neg_two_pow_le_toInd_add_toInt, bmod_two_pow_neg_iff, emod_eq_add_self_emo)uadd_overflow,sadd_overflow, uadd_overflow_eq,sadd_overflow_eq) and support theorems
|
Fixed what I could, I am now stuck on |
| -- simp only [Int.bmod_def, Nat.cast_pow, Nat.cast_ofNat] | ||
| -- by_cases xpos : 0 ≤ x | ||
| -- · rw [Int.emod_eq_of_lt (by omega) (by omega)]; omega | ||
| -- · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega |
There was a problem hiding this comment.
Why don't you pull the missing theorems from mathlib?
| @@ -319,6 +319,9 @@ attribute [bv_normalize] BitVec.umod_zero | |||
| attribute [bv_normalize] BitVec.umod_one | |||
| attribute [bv_normalize] BitVec.umod_eq_and | |||
|
|
|||
| attribute [bv_normalize] BitVec.saddOverflow_eq | |||
| attribute [bv_normalize] BitVec.uaddOverflow_eq | |||
|
|
|||
There was a problem hiding this comment.
We still need test cases of bv_normalize.
| @@ -1348,3 +1348,16 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1 | |||
| all_goals decide | |||
| · exact ofNat_nonneg x | |||
| · exact succ_ofNat_pos (x + 1) | |||
|
|
|||
| -- stolen from Mathlib as-is | |||
| theorem emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b := | |||
There was a problem hiding this comment.
Drop this comment, instead add it to the PR message.
| (x.toInt + y.toInt) < 2 ^ w := by | ||
| rcases w with _|w' |
There was a problem hiding this comment.
| (x.toInt + y.toInt) < 2 ^ w := by | |
| rcases w with _|w' | |
| x.toInt + y.toInt < 2 ^ w := by | |
| rcases w with _|w' |
This PR adds SMT-LIB operators to detect overflow (
uadd_overflow,sadd_overflow), according to the definitions here, and the theorems proving equivalence of such definitions with theBitVeclibrary functions (uadd_overflow_eq,sadd_overflow_eq). Support theorems for these proofs aretoInt_lt, le_toInt, toInd_add_toInt_lt_two_pow, neg_two_pow_le_toInd_add_toInt, bmod_two_pow_neg_iff, emod_eq_add_self_emo.