From f5d228c17d591de6c24ed59529bb634bf0822e4c Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 Jan 2025 08:25:55 +0000 Subject: [PATCH] WIP --- src/Init/Data/BitVec/Bitblast.lean | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 1c55a5db515a..80da0ad961d9 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1232,10 +1232,25 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) : /-! ### Overflow definitions -/ +theorem msb_setWidth_plus_one {x : BitVec w} : + (setWidth (w + 1) x).msb = false := sorry + +theorem helper {x : BitVec w}: (setWidth (w + 1) x).toNat % 2 ^ w = x.toNat := sorry + +@[simp] theorem toNat_mod_cancel_2 (x : BitVec n) (h : n < m): x.toNat % (2^m) = x.toNat := + Nat.mod_eq_of_lt (by + have := (@Nat.pow_lt_pow_iff_right 2 n m (by omega)).mpr (by omega) + omega + ) + + theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : - uaddOverflow x y = carry w x y false := by - simp only [uaddOverflow, BitVec.carry] - by_cases h : 2 ^ w ≤ x.toNat + y.toNat <;> simp [h] + uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w+1)).msb := by + simp only [uaddOverflow] + rw [msb_add] + simp [msb_setWidth_plus_one] + simp only [carry] + simp? theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : saddOverflow x y ↔ (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by