From 8e26dee691df78490feedac8c9b5baf91fc6509f Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Mon, 13 Jan 2025 13:24:42 +0000 Subject: [PATCH 01/57] feat; add overflow defs --- src/Init/Data/BitVec/Basic.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 44c883f746ff..08a001c41970 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -669,4 +669,24 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length | [] => 0#0 | b :: bs => concat (ofBoolListLE bs) b +/-- Overflow predicate for 2's complement unary minus -/ + +def not_overflow {w : Nat} (x : BitVec w) : Bool := x.toInt == - (2 ^ (w - 1)) + +/-- Overflow predicate for unsigned addition modulo 2^m -/ + +def uadd_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w + +/-- Overflow predicate for signed addition on m-bit 2's complement -/ + +def sadd_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1)) + +/-- Overflow predicate for unsigned multiplication modulo 2^m -/ + +def umul_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w + +/-- Overflow predicate for signed multiplication on m-bit 2's complement -/ + +def smul_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1)) + end BitVec From 8c64c87b7dbb57830e98feda839b568d7c619d90 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Mon, 13 Jan 2025 13:26:34 +0000 Subject: [PATCH 02/57] chore: add smtlib names in docstrings --- src/Init/Data/BitVec/Basic.lean | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 08a001c41970..e652f148081b 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -669,23 +669,38 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length | [] => 0#0 | b :: bs => concat (ofBoolListLE bs) b -/-- Overflow predicate for 2's complement unary minus -/ +/-- Overflow predicate for 2's complement unary minus. + + SMT-Lib name: `bvnego`. +-/ def not_overflow {w : Nat} (x : BitVec w) : Bool := x.toInt == - (2 ^ (w - 1)) -/-- Overflow predicate for unsigned addition modulo 2^m -/ +/-- Overflow predicate for unsigned addition modulo 2^m. + + SMT-Lib name: `bvuaddo`. +-/ def uadd_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w -/-- Overflow predicate for signed addition on m-bit 2's complement -/ +/-- Overflow predicate for signed addition on m-bit 2's complement. + + SMT-Lib name: `bvsaddo`. +-/ def sadd_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1)) -/-- Overflow predicate for unsigned multiplication modulo 2^m -/ +/-- Overflow predicate for unsigned multiplication modulo 2^m. + + SMT-Lib name: `bvumulo`. +-/ def umul_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w -/-- Overflow predicate for signed multiplication on m-bit 2's complement -/ +/-- Overflow predicate for signed multiplication on m-bit 2's complement. + + SMT-Lib name: `bvsmulo`. +-/ def smul_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1)) From 8c3448f146137e074ea771b83a0a5f777db1a102 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 14 Jan 2025 10:21:22 +0000 Subject: [PATCH 03/57] chore: fix docstrings --- src/Init/Data/BitVec/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index e652f148081b..0e16c7bc1bf9 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -676,28 +676,28 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length def not_overflow {w : Nat} (x : BitVec w) : Bool := x.toInt == - (2 ^ (w - 1)) -/-- Overflow predicate for unsigned addition modulo 2^m. +/-- Overflow predicate for unsigned addition modulo 2^w. SMT-Lib name: `bvuaddo`. -/ def uadd_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w -/-- Overflow predicate for signed addition on m-bit 2's complement. +/-- Overflow predicate for signed addition on w-bit 2's complement. SMT-Lib name: `bvsaddo`. -/ def sadd_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1)) -/-- Overflow predicate for unsigned multiplication modulo 2^m. +/-- Overflow predicate for unsigned multiplication modulo 2^w. SMT-Lib name: `bvumulo`. -/ def umul_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w -/-- Overflow predicate for signed multiplication on m-bit 2's complement. +/-- Overflow predicate for signed multiplication on w-bit 2's complement. SMT-Lib name: `bvsmulo`. -/ From c8ed74e9eae9a20f388b0349d214b6631d845fc8 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 14 Jan 2025 14:09:22 +0000 Subject: [PATCH 04/57] chore: fix definition case --- src/Init/Data/BitVec/Basic.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 0e16c7bc1bf9..5fb26a483a5a 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -669,39 +669,41 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length | [] => 0#0 | b :: bs => concat (ofBoolListLE bs) b +/-! ## Overflow -/ + /-- Overflow predicate for 2's complement unary minus. SMT-Lib name: `bvnego`. -/ -def not_overflow {w : Nat} (x : BitVec w) : Bool := x.toInt == - (2 ^ (w - 1)) +def notOverflow {w : Nat} (x : BitVec w) : Bool := x.toInt == - (2 ^ (w - 1)) /-- Overflow predicate for unsigned addition modulo 2^w. SMT-Lib name: `bvuaddo`. -/ -def uadd_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w +def uaddOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w /-- Overflow predicate for signed addition on w-bit 2's complement. SMT-Lib name: `bvsaddo`. -/ -def sadd_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1)) +def saddOverflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1)) /-- Overflow predicate for unsigned multiplication modulo 2^w. SMT-Lib name: `bvumulo`. -/ -def umul_overflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w +def umulOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w /-- Overflow predicate for signed multiplication on w-bit 2's complement. SMT-Lib name: `bvsmulo`. -/ -def smul_overflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1)) +def smulOverflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1)) end BitVec From 7026bd1e9b4996365ab4d07c850fb1908ee86d5a Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 11:53:33 +0000 Subject: [PATCH 05/57] chore: only add --- src/Init/Data/BitVec/Basic.lean | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 5fb26a483a5a..676faefc7422 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -692,18 +692,4 @@ def uaddOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ def saddOverflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1)) -/-- Overflow predicate for unsigned multiplication modulo 2^w. - - SMT-Lib name: `bvumulo`. --/ - -def umulOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat * y.toNat ≥ 2 ^ w - -/-- Overflow predicate for signed multiplication on w-bit 2's complement. - - SMT-Lib name: `bvsmulo`. --/ - -def smulOverflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt * y.toInt ≥ 2 ^ (w - 1)) || (x.toInt * y.toInt < - 2 ^ (w - 1)) - end BitVec From 7d0c8734ae5267522b7a6242745a712c249b82d3 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 11:54:29 +0000 Subject: [PATCH 06/57] chore: uadd, sadd --- src/Init/Data/BitVec/Lemmas.lean | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 377ab5cc885f..9c506c1fb407 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3536,6 +3536,33 @@ 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)] +/-! ### Overflow definitions -/ + +theorem uadd_overflow_eq {w : Nat} (x y : BitVec w) : + uadd_overflow x y = BitVec.carry w x y false := by + simp only [uadd_overflow, BitVec.carry] + by_cases h : 2 ^ w ≤ x.toNat + y.toNat <;> simp [h] + +theorem sadd_overflow_eq {w : Nat} (x y : BitVec w) : + sadd_overflow x y = true ↔ x.msb = y.msb ∧ ¬(x + y).msb = x.msb := by + simp only [sadd_overflow] + rcases w with _|w' + · revert x y + decide + · have h : 0 < w' + 1 := by omega + generalize w' + 1 = w at * + have := le_toInt x + have := le_toInt y + have := toInt_lt y + have := toInt_lt x + have := toInd_add_toInt_lt_two_pow x y + have := neg_two_pow_le_toInd_add_toInt x y + simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, + 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 + /-! ### Non-overflow theorems -/ From 686141a2e4eeb43ee87f22f85db89fabe99ce1ce Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 11:55:25 +0000 Subject: [PATCH 07/57] chore: add theorems --- src/Init/Data/BitVec/Lemmas.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 9c506c1fb407..9fde55093171 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3538,6 +3538,14 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) := /-! ### Overflow definitions -/ + +theorem Int.bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : + (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by + 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 + theorem uadd_overflow_eq {w : Nat} (x y : BitVec w) : uadd_overflow x y = BitVec.carry w x y false := by simp only [uadd_overflow, BitVec.carry] From b005e45607ee7b0ec139fcf9898ba08998a54ecd Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 11:57:23 +0000 Subject: [PATCH 08/57] chore: remove not-overflow --- src/Init/Data/BitVec/Basic.lean | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 676faefc7422..25dd3a2c2656 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -671,13 +671,6 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length /-! ## Overflow -/ -/-- Overflow predicate for 2's complement unary minus. - - SMT-Lib name: `bvnego`. --/ - -def notOverflow {w : Nat} (x : BitVec w) : Bool := x.toInt == - (2 ^ (w - 1)) - /-- Overflow predicate for unsigned addition modulo 2^w. SMT-Lib name: `bvuaddo`. From 3f33283bb386d2402e5ea712e1fdb81742f5ffa6 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 22 Jan 2025 12:51:59 +0000 Subject: [PATCH 09/57] chore: formatting Co-authored-by: Tobias Grosser --- src/Init/Data/BitVec/Lemmas.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 9fde55093171..c21e1615d9f7 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3546,9 +3546,9 @@ theorem Int.bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 · 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 -theorem uadd_overflow_eq {w : Nat} (x y : BitVec w) : - uadd_overflow x y = BitVec.carry w x y false := by - simp only [uadd_overflow, BitVec.carry] +theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : + uaddOverflow x y = BitVec.carry w x y false := by + simp only [uaddOverflow, BitVec.carry] by_cases h : 2 ^ w ≤ x.toNat + y.toNat <;> simp [h] theorem sadd_overflow_eq {w : Nat} (x y : BitVec w) : From 95e3c013f8daa4abca71182f6f9dd2755577da97 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 22 Jan 2025 12:52:09 +0000 Subject: [PATCH 10/57] chore: formatting Co-authored-by: Tobias Grosser --- src/Init/Data/BitVec/Lemmas.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index c21e1615d9f7..b3f0f66cffd8 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3551,9 +3551,9 @@ theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : simp only [uaddOverflow, BitVec.carry] by_cases h : 2 ^ w ≤ x.toNat + y.toNat <;> simp [h] -theorem sadd_overflow_eq {w : Nat} (x y : BitVec w) : - sadd_overflow x y = true ↔ x.msb = y.msb ∧ ¬(x + y).msb = x.msb := by - simp only [sadd_overflow] +theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : + saddOverflow x y = true ↔ x.msb = y.msb ∧ ¬(x + y).msb = x.msb := by + simp only [saddOverflow] rcases w with _|w' · revert x y decide From 65be5854a09c08a91f510fa207d08cecb2a125aa Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 12:56:47 +0000 Subject: [PATCH 11/57] choire: move to normalize --- src/Init/Data/BitVec/Lemmas.lean | 36 ------------------- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 36 +++++++++++++++++++ 2 files changed, 36 insertions(+), 36 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index b3f0f66cffd8..3b21016fa5a5 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3536,42 +3536,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)] -/-! ### Overflow definitions -/ - - -theorem Int.bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : - (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by - 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 - -theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : - uaddOverflow x y = BitVec.carry w x y false := by - simp only [uaddOverflow, BitVec.carry] - by_cases h : 2 ^ w ≤ x.toNat + y.toNat <;> simp [h] - -theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : - saddOverflow x y = true ↔ x.msb = y.msb ∧ ¬(x + y).msb = x.msb := by - simp only [saddOverflow] - rcases w with _|w' - · revert x y - decide - · have h : 0 < w' + 1 := by omega - generalize w' + 1 = w at * - have := le_toInt x - have := le_toInt y - have := toInt_lt y - have := toInt_lt x - have := toInd_add_toInt_lt_two_pow x y - have := neg_two_pow_le_toInd_add_toInt x y - simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, - 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 - - /-! ### Non-overflow theorems -/ /-- If `x.toNat * y.toNat < 2^w`, then the multiplication `(x * y)` does not overflow. -/ diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 09088f9eb595..cc2ee4b944f0 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -309,5 +309,41 @@ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat) have : BitVec.ofNat w n = BitVec.twoPow w k := by simp [bv_toNat, hk] rw [this, BitVec.udiv_twoPow_eq_of_lt (hk := by omega)] + +/-! ### Overflow definitions -/ + +theorem Int.bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : + (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by + 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 + +theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : + uaddOverflow x y = BitVec.carry w x y false := by + simp only [uaddOverflow, BitVec.carry] + by_cases h : 2 ^ w ≤ x.toNat + y.toNat <;> simp [h] + +theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : + saddOverflow x y = true ↔ x.msb = y.msb ∧ ¬(x + y).msb = x.msb := by + simp only [saddOverflow] + rcases w with _|w' + · revert x y + decide + · have h : 0 < w' + 1 := by omega + generalize w' + 1 = w at * + have := le_toInt x + have := le_toInt y + have := toInt_lt y + have := toInt_lt x + have := toInd_add_toInt_lt_two_pow x y + have := neg_two_pow_le_toInd_add_toInt x y + simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, + 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 + + end Normalize end Std.Tactic.BVDecide From 58de7823183e360e35115c1148b9fcf5b2ffb619 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 22 Jan 2025 12:58:31 +0000 Subject: [PATCH 12/57] chore: formatting Co-authored-by: Alex Keizer --- src/Init/Data/BitVec/Basic.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 25dd3a2c2656..05f45733c636 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -675,7 +675,6 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length SMT-Lib name: `bvuaddo`. -/ - def uaddOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w /-- Overflow predicate for signed addition on w-bit 2's complement. From 7f4f48457c5392a2964eeae5e6aac9f106dc822d Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 22 Jan 2025 12:58:41 +0000 Subject: [PATCH 13/57] chore: formatting Co-authored-by: Alex Keizer --- src/Init/Data/BitVec/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 05f45733c636..0579ee4de7a8 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -681,7 +681,7 @@ def uaddOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ SMT-Lib name: `bvsaddo`. -/ - -def saddOverflow {w : Nat} (x y : BitVec w) : Bool := (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1)) +def saddOverflow {w : Nat} (x y : BitVec w) : Bool := + (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1)) end BitVec From befd15a1be3ffa0772d67c753e1e413f907acfae Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 12:59:15 +0000 Subject: [PATCH 14/57] chore: formatting --- src/Init/Data/BitVec/Lemmas.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 3b21016fa5a5..377ab5cc885f 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3536,6 +3536,7 @@ 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)] + /-! ### Non-overflow theorems -/ /-- If `x.toNat * y.toNat < 2^w`, then the multiplication `(x * y)` does not overflow. -/ From cd84f3af5923f1b3025a2cabf6eb144b0faba4d7 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 12:59:55 +0000 Subject: [PATCH 15/57] chore: move overflow theorems back --- src/Init/Data/BitVec/Lemmas.lean | 33 +++++++++++++++++ src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 36 ------------------- 2 files changed, 33 insertions(+), 36 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 377ab5cc885f..0ca0b2fcbcf1 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3536,6 +3536,39 @@ 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)] +/-! ### Overflow definitions -/ + +theorem Int.bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : + (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by + 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 + +theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : + uaddOverflow x y = BitVec.carry w x y false := by + simp only [uaddOverflow, BitVec.carry] + by_cases h : 2 ^ w ≤ x.toNat + y.toNat <;> simp [h] + +theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : + saddOverflow x y = true ↔ x.msb = y.msb ∧ ¬(x + y).msb = x.msb := by + simp only [saddOverflow] + rcases w with _|w' + · revert x y + decide + · have h : 0 < w' + 1 := by omega + generalize w' + 1 = w at * + have := le_toInt x + have := le_toInt y + have := toInt_lt y + have := toInt_lt x + have := toInd_add_toInt_lt_two_pow x y + have := neg_two_pow_le_toInd_add_toInt x y + simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, + 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 /-! ### Non-overflow theorems -/ diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index cc2ee4b944f0..09088f9eb595 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -309,41 +309,5 @@ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat) have : BitVec.ofNat w n = BitVec.twoPow w k := by simp [bv_toNat, hk] rw [this, BitVec.udiv_twoPow_eq_of_lt (hk := by omega)] - -/-! ### Overflow definitions -/ - -theorem Int.bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : - (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by - 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 - -theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : - uaddOverflow x y = BitVec.carry w x y false := by - simp only [uaddOverflow, BitVec.carry] - by_cases h : 2 ^ w ≤ x.toNat + y.toNat <;> simp [h] - -theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : - saddOverflow x y = true ↔ x.msb = y.msb ∧ ¬(x + y).msb = x.msb := by - simp only [saddOverflow] - rcases w with _|w' - · revert x y - decide - · have h : 0 < w' + 1 := by omega - generalize w' + 1 = w at * - have := le_toInt x - have := le_toInt y - have := toInt_lt y - have := toInt_lt x - have := toInd_add_toInt_lt_two_pow x y - have := neg_two_pow_le_toInd_add_toInt x y - simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, - 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 - - end Normalize end Std.Tactic.BVDecide From 77bb9748979cd9428f8d7ef858aae60abc566bef Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 13:02:19 +0000 Subject: [PATCH 16/57] chore: move all theorems --- src/Init/Data/BitVec/Lemmas.lean | 56 ++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 0ca0b2fcbcf1..082c144132a1 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -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 + · subst hw + simp [BitVec.eq_nil x] + · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] + split + case neg.isTrue h => + norm_cast + omega + case neg.isFalse h => + rw [sub_lt_iff_lt_add] + norm_cast + omega + +theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by + simp only [BitVec.toInt, Nat.cast_pow] + by_cases hw : w = 0 + · subst hw + simp [BitVec.eq_nil x] + · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] + simp only [zero_lt_two, mul_lt_mul_left, Nat.cast_ofNat] + split + case neg.isTrue h => + norm_cast + omega + case neg.isFalse h => + simp only [neg_le_sub_iff_le_add] + norm_cast + rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] + omega + +theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : + (x.toInt + y.toInt) < 2 ^ w := by + by_cases hw : w = 0 + · subst hw + simp [BitVec.eq_nil x, BitVec.eq_nil y] + · norm_cast + rw [←Nat.two_pow_pred_add_two_pow_pred (by omega)] + have hx := toInt_lt x + have hy := toInt_lt y + push_cast + omega + +theorem neg_two_pow_le_toInd_add_toInt (x y : BitVec w) : + - 2 ^ w ≤ x.toInt + y.toInt := by + by_cases hw : w = 0 + · subst hw + simp [BitVec.eq_nil x, BitVec.eq_nil y] + · norm_cast + rw [←Nat.two_pow_pred_add_two_pow_pred (by omega)] + have hx := le_toInt x + have hy := le_toInt y + push_cast + omega + /-! ### slt -/ /-- From a8470b4b40658e7dce7e58b4f811ab35c6fea15d Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 13:03:26 +0000 Subject: [PATCH 17/57] chore: add attribute to normalize --- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 09088f9eb595..0a2aa2ac22e8 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -303,6 +303,10 @@ 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 + + /-- `x / (BitVec.ofNat n)` where `n = 2^k` is the same as shifting `x` right by `k`. -/ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat) (hk : 2 ^ k = n) (hlt : k < w) : x / (BitVec.ofNat w n) = x >>> k := by From 4c582c26c77c60fb8d6b362cef769746db150773 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 13:04:47 +0000 Subject: [PATCH 18/57] chore: move int theorem --- src/Init/Data/BitVec/Lemmas.lean | 7 ------- src/Init/Data/Int/DivModLemmas.lean | 7 +++++++ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 082c144132a1..f92a536242e1 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3594,13 +3594,6 @@ theorem getLsbD_intMax (w : Nat) : (intMax w).getLsbD i = decide (i + 1 < w) := /-! ### Overflow definitions -/ -theorem Int.bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : - (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by - 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 - theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : uaddOverflow x y = BitVec.carry w x y false := by simp only [uaddOverflow, BitVec.carry] diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index b8f121043a55..dc5bc9ea6cbd 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -1348,3 +1348,10 @@ 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) + +theorem bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : + (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by + 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 From 1e3e07b8a3570ef50df38818293f89f4c9b14978 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 14:01:09 +0000 Subject: [PATCH 19/57] chore: update housing of theorems --- src/Init/Data/BitVec/Bitblast.lean | 27 +++++++++++++ src/Init/Data/BitVec/Lemmas.lean | 60 ++++++++--------------------- src/Init/Data/Int/DivModLemmas.lean | 10 ++--- 3 files changed, 49 insertions(+), 48 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 003d35aa2ca3..8d073fb9e919 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1230,4 +1230,31 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) : · simp [of_length_zero] · simp [ushiftRightRec_eq] +/-! ### Overflow definitions -/ + +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] + +theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : + saddOverflow x y ↔ (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by + simp only [saddOverflow] + rcases w with _|w' + · revert x y + decide + · have h : 0 < w' + 1 := by omega + generalize w' + 1 = w at * + have := le_toInt x + have := le_toInt y + have := toInt_lt y + have := toInt_lt x + have := toInd_add_toInt_lt_two_pow x y + have := neg_two_pow_le_toInd_add_toInt x y + simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, + decide_eq_decide, BitVec.toInt_add] + rw [Int.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 + end BitVec diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 16b5f8aa82f1..7c478c613e7c 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -543,7 +543,7 @@ 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] + simp only [BitVec.toInt] by_cases hw : w = 0 · subst hw simp [BitVec.eq_nil x] @@ -552,27 +552,28 @@ theorem toInt_lt {w : Nat} (x : BitVec w) : x.toInt < 2 ^ (w - 1) := by case neg.isTrue h => norm_cast omega - case neg.isFalse h => - rw [sub_lt_iff_lt_add] - norm_cast - omega + case neg.isFalse h => sorry + -- rw [Nat.sub_lt_iff_lt_add] + -- norm_cast + -- omega theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by - simp only [BitVec.toInt, Nat.cast_pow] + simp only [BitVec.toInt] by_cases hw : w = 0 · subst hw simp [BitVec.eq_nil x] · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - simp only [zero_lt_two, mul_lt_mul_left, Nat.cast_ofNat] - split - case neg.isTrue h => - norm_cast - omega - case neg.isFalse h => - simp only [neg_le_sub_iff_le_add] - norm_cast - rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - omega + sorry + -- simp only [zero_lt_two, mul_lt_mul_left, Nat.cast_ofNat] + -- split + -- case neg.isTrue h => + -- norm_cast + -- omega + -- case neg.isFalse h => + -- simp only [neg_le_sub_iff_le_add] + -- norm_cast + -- rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] + -- omega theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : (x.toInt + y.toInt) < 2 ^ w := by @@ -3635,33 +3636,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)] -/-! ### Overflow definitions -/ - -theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : - uaddOverflow x y = BitVec.carry w x y false := by - simp only [uaddOverflow, BitVec.carry] - by_cases h : 2 ^ w ≤ x.toNat + y.toNat <;> simp [h] - -theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : - saddOverflow x y = true ↔ x.msb = y.msb ∧ ¬(x + y).msb = x.msb := by - simp only [saddOverflow] - rcases w with _|w' - · revert x y - decide - · have h : 0 < w' + 1 := by omega - generalize w' + 1 = w at * - have := le_toInt x - have := le_toInt y - have := toInt_lt y - have := toInt_lt x - have := toInd_add_toInt_lt_two_pow x y - have := neg_two_pow_le_toInd_add_toInt x y - simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, - 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 - /-! ### Non-overflow theorems -/ /-- If `x.toNat + y.toNat < 2^w`, then the addition `(x + y)` does not overflow. -/ diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index dc5bc9ea6cbd..27ddc410a424 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -1350,8 +1350,8 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1 · exact succ_ofNat_pos (x + 1) theorem bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : - (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by - 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 + (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by sorry + -- 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 From ab1d3d570c6f5000a9cb36ab93a15e0fa1c23fee Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 22 Jan 2025 14:02:30 +0000 Subject: [PATCH 20/57] chore: formatting Co-authored-by: Tobias Grosser --- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 91aa202f728a..3142fa39419f 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -321,8 +321,6 @@ attribute [bv_normalize] BitVec.umod_eq_and attribute [bv_normalize] BitVec.saddOverflow_eq attribute [bv_normalize] BitVec.uaddOverflow_eq - - /-- `x / (BitVec.ofNat n)` where `n = 2^k` is the same as shifting `x` right by `k`. -/ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat) (hk : 2 ^ k = n) (hlt : k < w) : x / (BitVec.ofNat w n) = x >>> k := by From ffe861ecc85a084eee6f2f864ef4345b399eabc6 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 14:25:23 +0000 Subject: [PATCH 21/57] chore: everyone found their spot but everything is broken --- src/Init/Data/BitVec/Lemmas.lean | 21 ++++++++++----------- src/Init/Data/Int/DivModLemmas.lean | 10 +++++----- 2 files changed, 15 insertions(+), 16 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 7c478c613e7c..c5b4fcecb58b 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -563,17 +563,16 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by · subst hw simp [BitVec.eq_nil x] · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - sorry - -- simp only [zero_lt_two, mul_lt_mul_left, Nat.cast_ofNat] - -- split - -- case neg.isTrue h => - -- norm_cast - -- omega - -- case neg.isFalse h => - -- simp only [neg_le_sub_iff_le_add] - -- norm_cast - -- rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - -- omega + simp only [zero_lt_two, mul_lt_mul_left, Nat.cast_ofNat] + split + case neg.isTrue h => + norm_cast + omega + case neg.isFalse h => + simp only [neg_le_sub_iff_le_add] + norm_cast + rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] + omega theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : (x.toInt + y.toInt) < 2 ^ w := by diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index 27ddc410a424..d4b01f86169b 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -1350,8 +1350,8 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1 · exact succ_ofNat_pos (x + 1) theorem bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : - (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by sorry - -- 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 + (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by + simp [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 From 7af6bb8c3ea5e9a1c01b130130578c3c2261bce3 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 15:36:53 +0000 Subject: [PATCH 22/57] chore: more fixing in places --- src/Init/Data/BitVec/Lemmas.lean | 21 ++++++++++--------- src/Init/Data/Int/DivModLemmas.lean | 13 ++++++++---- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 1 + 3 files changed, 21 insertions(+), 14 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index c5b4fcecb58b..7c478c613e7c 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -563,16 +563,17 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by · subst hw simp [BitVec.eq_nil x] · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - simp only [zero_lt_two, mul_lt_mul_left, Nat.cast_ofNat] - split - case neg.isTrue h => - norm_cast - omega - case neg.isFalse h => - simp only [neg_le_sub_iff_le_add] - norm_cast - rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - omega + sorry + -- simp only [zero_lt_two, mul_lt_mul_left, Nat.cast_ofNat] + -- split + -- case neg.isTrue h => + -- norm_cast + -- omega + -- case neg.isFalse h => + -- simp only [neg_le_sub_iff_le_add] + -- norm_cast + -- rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] + -- omega theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : (x.toInt + y.toInt) < 2 ^ w := by diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index d4b01f86169b..6684569741bf 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -1349,9 +1349,14 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1 · 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 := + add_emod_self.symm + theorem bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by - simp [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 + sorry + -- 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 diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 3142fa39419f..29c05600877a 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -321,6 +321,7 @@ attribute [bv_normalize] BitVec.umod_eq_and attribute [bv_normalize] BitVec.saddOverflow_eq attribute [bv_normalize] BitVec.uaddOverflow_eq + /-- `x / (BitVec.ofNat n)` where `n = 2^k` is the same as shifting `x` right by `k`. -/ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat) (hk : 2 ^ k = n) (hlt : k < w) : x / (BitVec.ofNat w n) = x >>> k := by From 4115b362a8f949926c8451de5dca136cff2fdeba Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 15:58:46 +0000 Subject: [PATCH 23/57] chore: le_toInt works --- src/Init/Data/BitVec/Lemmas.lean | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 7c478c613e7c..bb4cafd0d963 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -554,26 +554,23 @@ theorem toInt_lt {w : Nat} (x : BitVec w) : x.toInt < 2 ^ (w - 1) := by omega case neg.isFalse h => sorry -- rw [Nat.sub_lt_iff_lt_add] - -- norm_cast - -- omega + -- norm_cast; omega + theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by simp only [BitVec.toInt] - by_cases hw : w = 0 - · subst hw - simp [BitVec.eq_nil x] + rcases w with _|w' + · omega · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - sorry - -- simp only [zero_lt_two, mul_lt_mul_left, Nat.cast_ofNat] - -- split - -- case neg.isTrue h => - -- norm_cast - -- omega - -- case neg.isFalse h => - -- simp only [neg_le_sub_iff_le_add] - -- norm_cast - -- rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - -- omega + by_cases h2 : 2 * x.toNat < 2 * 2 ^ (w' - 1) + · simp only [Nat.add_one_sub_one, Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, + Int.Nat.cast_ofNat_Int] + norm_cast + omega + · simp only [Nat.add_one_sub_one, Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, + Int.Nat.cast_ofNat_Int] + norm_cast + omega theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : (x.toInt + y.toInt) < 2 ^ w := by From 04f49e49aa7e72a7a106475082578e68368dc18b Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 16:04:03 +0000 Subject: [PATCH 24/57] chore: fix toInt_lt --- src/Init/Data/BitVec/Lemmas.lean | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index bb4cafd0d963..739a0e0b4ab0 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -544,25 +544,22 @@ theorem toInt_zero {w : Nat} : (0#w).toInt = 0 := by theorem toInt_lt {w : Nat} (x : BitVec w) : x.toInt < 2 ^ (w - 1) := by simp only [BitVec.toInt] - by_cases hw : w = 0 - · subst hw - simp [BitVec.eq_nil x] + rcases w with _|w' + · omega · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - split - case neg.isTrue h => - norm_cast + by_cases h : 2 * x.toNat < 2 * 2 ^ (w' + 1 - 1) + · norm_cast omega - case neg.isFalse h => sorry - -- rw [Nat.sub_lt_iff_lt_add] - -- norm_cast; omega - + · simp only [Nat.add_one_sub_one, Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, + Int.Nat.cast_ofNat_Int] + norm_cast; omega theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by simp only [BitVec.toInt] rcases w with _|w' · omega - · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - by_cases h2 : 2 * x.toNat < 2 * 2 ^ (w' - 1) + · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul] + by_cases h : 2 * x.toNat < 2 * 2 ^ (w' - 1) -- i tried using split here but the final omega stops working?! im confused · simp only [Nat.add_one_sub_one, Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] norm_cast From ddceb186ee2b0e8f62a17164d57a8f66568e8455 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 22 Jan 2025 16:14:35 +0000 Subject: [PATCH 25/57] chore: replace rcases --- src/Init/Data/BitVec/Lemmas.lean | 12 ++++++------ src/Init/Data/Int/DivModLemmas.lean | 1 + 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 739a0e0b4ab0..bc933101630b 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -571,26 +571,26 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : (x.toInt + y.toInt) < 2 ^ w := by - by_cases hw : w = 0 - · subst hw - simp [BitVec.eq_nil x, BitVec.eq_nil y] + rcases w with _|w' + · simp [BitVec.eq_nil x, BitVec.eq_nil y] · norm_cast rw [←Nat.two_pow_pred_add_two_pow_pred (by omega)] have hx := toInt_lt x have hy := toInt_lt y push_cast + rw [Nat.add_sub_cancel] at hx hy omega theorem neg_two_pow_le_toInd_add_toInt (x y : BitVec w) : - 2 ^ w ≤ x.toInt + y.toInt := by - by_cases hw : w = 0 - · subst hw - simp [BitVec.eq_nil x, BitVec.eq_nil y] + rcases w with _|w' + · simp [BitVec.eq_nil x, BitVec.eq_nil y] · norm_cast rw [←Nat.two_pow_pred_add_two_pow_pred (by omega)] have hx := le_toInt x have hy := le_toInt y push_cast + rw [Nat.add_sub_cancel] at hx hy omega /-! ### slt -/ diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index 6684569741bf..2f7b5944a251 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -1355,6 +1355,7 @@ theorem emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b := theorem bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by + sorry -- simp only [Int.bmod_def, Nat.cast_pow, Nat.cast_ofNat] -- by_cases xpos : 0 ≤ x From bd24dbda50b1fd5ba968204bfc0fe66d3c361944 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 23 Jan 2025 10:16:20 +0000 Subject: [PATCH 26/57] chore: uncomment proofs --- src/Init/Data/Int/DivModLemmas.lean | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index 2f7b5944a251..f0d0606c5a8c 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -1349,15 +1349,17 @@ theorem bmod_natAbs_plus_one (x : Int) (w : 1 < x.natAbs) : bmod x (x.natAbs + 1 · 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 := - add_emod_self.symm +theorem emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b := add_emod_self.symm + +theorem Nat.cast_pow (m n : Nat) : ↑(m ^ n) = (m ^ n) := by simp + +theorem Nat.cast_ofNat {n : Nat} : Nat.cast (OfNat.ofNat n) = OfNat.ofNat n := rfl theorem bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by - - sorry - -- 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 + simp only [Int.bmod_def, Nat.cast_pow, Nat.cast_ofNat] + by_cases xpos : 0 ≤ x + · -- rw [Int.emod_eq_of_lt xpos (by omega)]; omega + sorry + · -- rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega + sorry From df55e51b1e157dc776b11671e30b263446f2a6b9 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 23 Jan 2025 10:17:01 +0000 Subject: [PATCH 27/57] chore: parentheses format --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index bc933101630b..754294fcd57b 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -570,7 +570,7 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by omega theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : - (x.toInt + y.toInt) < 2 ^ w := by + x.toInt + y.toInt < 2 ^ w := by rcases w with _|w' · simp [BitVec.eq_nil x, BitVec.eq_nil y] · norm_cast From cf259c0fa08ed12331405dbc8b534406971fb828 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 23 Jan 2025 11:17:49 +0000 Subject: [PATCH 28/57] feat: add tests --- tests/lean/run/bv_decide_rewriter.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean index 882dc72536a6..2c5ec606695a 100644 --- a/tests/lean/run/bv_decide_rewriter.lean +++ b/tests/lean/run/bv_decide_rewriter.lean @@ -87,6 +87,11 @@ example {x : BitVec 16} : x / (BitVec.twoPow 16 2) = x >>> 2 := by bv_normalize 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 +example (x y : BitVec 16) : BitVec.uaddOverflow x y = BitVec.carry 16 x y false := by bv_normalize +example (x y : BitVec 16) : BitVec.saddOverflow x y = (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by bv_normalize +example (x y : BitVec w) : BitVec.uaddOverflow x y = BitVec.carry w x y false := by bv_normalize +example (x y : BitVec w) : BitVec.saddOverflow x y = (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by bv_normalize + section From b7deb99fe05fc701f0b49d05e780ece9620a2331 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 Jan 2025 07:31:39 +0000 Subject: [PATCH 29/57] make it compile --- src/Init/Data/BitVec/Bitblast.lean | 8 +++++++- src/Init/Data/Int/DivModLemmas.lean | 15 --------------- 2 files changed, 7 insertions(+), 16 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 8d073fb9e919..07d194f12f2d 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1253,7 +1253,13 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : have := neg_two_pow_le_toInd_add_toInt x y simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, decide_eq_decide, BitVec.toInt_add] - rw [Int.bmod_two_pow_neg_iff (by omega) (by omega)] + have bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) : + (x.bmod m) < 0 ↔ (-(m / 2) ≤ x ∧ x < 0) ∨ ((m + 1) / 2 ≤ x) := by + simp only [Int.bmod_def] + by_cases xpos : 0 ≤ x + · rw [Int.emod_eq_of_lt xpos (by omega)]; omega + · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega + rw [bmod_neg_iff (by norm_cast at *) (by norm_cast at *)] rw_mod_cast [← @Nat.two_pow_pred_add_two_pow_pred w (by omega)] at * omega diff --git a/src/Init/Data/Int/DivModLemmas.lean b/src/Init/Data/Int/DivModLemmas.lean index f0d0606c5a8c..b8f121043a55 100644 --- a/src/Init/Data/Int/DivModLemmas.lean +++ b/src/Init/Data/Int/DivModLemmas.lean @@ -1348,18 +1348,3 @@ 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) - -theorem emod_eq_add_self_emod {a b : Int} : a % b = (a + b) % b := add_emod_self.symm - -theorem Nat.cast_pow (m n : Nat) : ↑(m ^ n) = (m ^ n) := by simp - -theorem Nat.cast_ofNat {n : Nat} : Nat.cast (OfNat.ofNat n) = OfNat.ofNat n := rfl - -theorem bmod_two_pow_neg_iff {w : Nat} {x : Int} (h1 : x < 2 ^ w) (h2 : -(2 ^ w) ≤ x) : - (x.bmod (2 ^ w)) < 0 ↔ (-(2 ^ w) ≤ 2 * x ∧ x < 0) ∨ (2 ^ w ≤ 2 * x) := by - simp only [Int.bmod_def, Nat.cast_pow, Nat.cast_ofNat] - by_cases xpos : 0 ≤ x - · -- rw [Int.emod_eq_of_lt xpos (by omega)]; omega - sorry - · -- rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega - sorry From e963a5b0b3f3bb3dcab189281ab2d1f572ce10a8 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 Jan 2025 07:36:08 +0000 Subject: [PATCH 30/57] Further cleanup --- src/Init/Data/BitVec/Bitblast.lean | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 07d194f12f2d..25d81d7f5f53 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1240,15 +1240,12 @@ theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : saddOverflow x y ↔ (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by simp only [saddOverflow] - rcases w with _|w' + rcases w with _|w · revert x y decide - · have h : 0 < w' + 1 := by omega - generalize w' + 1 = w at * - have := le_toInt x - have := le_toInt y - have := toInt_lt y - have := toInt_lt x + · have h : 0 < w + 1 := by omega + have := le_toInt x; have := toInt_lt x + have := le_toInt y; have := toInt_lt y have := toInd_add_toInt_lt_two_pow x y have := neg_two_pow_le_toInd_add_toInt x y simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, @@ -1260,7 +1257,7 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : · rw [Int.emod_eq_of_lt xpos (by omega)]; omega · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega rw [bmod_neg_iff (by norm_cast at *) (by norm_cast at *)] - rw_mod_cast [← @Nat.two_pow_pred_add_two_pow_pred w (by omega)] at * + rw_mod_cast [← @Nat.two_pow_pred_add_two_pow_pred (w + 1) (by omega)] at * omega end BitVec From c275d431ed703e10d6e2d535ad773973b16af7b5 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 Jan 2025 07:38:19 +0000 Subject: [PATCH 31/57] make it compile again --- src/Init/Data/BitVec/Bitblast.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 25d81d7f5f53..97b1961f109c 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1255,7 +1255,7 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : simp only [Int.bmod_def] by_cases xpos : 0 ≤ x · rw [Int.emod_eq_of_lt xpos (by omega)]; omega - · rw [Int.emod_eq_add_self_emod, Int.emod_eq_of_lt (by omega) (by omega)]; omega + · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega rw [bmod_neg_iff (by norm_cast at *) (by norm_cast at *)] rw_mod_cast [← @Nat.two_pow_pred_add_two_pow_pred (w + 1) (by omega)] at * omega From 3b713645d63a4d06f283f4d50c1a7029a4656d77 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 Jan 2025 07:40:26 +0000 Subject: [PATCH 32/57] clean a bit --- src/Init/Data/BitVec/Bitblast.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 97b1961f109c..d47b409321ca 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1248,16 +1248,18 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : have := le_toInt y; have := toInt_lt y have := toInd_add_toInt_lt_two_pow x y have := neg_two_pow_le_toInd_add_toInt x y - simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, - decide_eq_decide, BitVec.toInt_add] + have bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) : (x.bmod m) < 0 ↔ (-(m / 2) ≤ x ∧ x < 0) ∨ ((m + 1) / 2 ≤ x) := by simp only [Int.bmod_def] by_cases xpos : 0 ≤ x · rw [Int.emod_eq_of_lt xpos (by omega)]; omega · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega - rw [bmod_neg_iff (by norm_cast at *) (by norm_cast at *)] - rw_mod_cast [← @Nat.two_pow_pred_add_two_pow_pred (w + 1) (by omega)] at * + + simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, + decide_eq_decide, BitVec.toInt_add] + rw_mod_cast [bmod_neg_iff (by assumption) (by assumption), + ← @Nat.two_pow_pred_add_two_pow_pred (w + 1) (by omega)] at * omega end BitVec From 8be4e02b56f5e94d2058c65266a83ce9b08faf0b Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 Jan 2025 07:42:56 +0000 Subject: [PATCH 33/57] simplify further --- src/Init/Data/BitVec/Bitblast.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index d47b409321ca..1c55a5db515a 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1243,8 +1243,7 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : rcases w with _|w · revert x y decide - · have h : 0 < w + 1 := by omega - have := le_toInt x; have := toInt_lt x + · have := le_toInt x; have := toInt_lt x have := le_toInt y; have := toInt_lt y have := toInd_add_toInt_lt_two_pow x y have := neg_two_pow_le_toInd_add_toInt x y From f5d228c17d591de6c24ed59529bb634bf0822e4c Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 24 Jan 2025 08:25:55 +0000 Subject: [PATCH 34/57] 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 From 9f24743cd0d1f8ce86f31d819a9fe43914a2176d Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 09:42:01 +0000 Subject: [PATCH 35/57] chore: simplify uadd_overflow --- src/Init/Data/BitVec/Bitblast.lean | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 80da0ad961d9..8742dd1c6969 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1232,25 +1232,16 @@ 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 := +@[simp] theorem toNat_mod_lt_cancel {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 = (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? + uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w + 1)).msb := by + simp [uaddOverflow, msb_add, msb_setWidth, carry] theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : saddOverflow x y ↔ (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by @@ -1262,7 +1253,6 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : have := le_toInt y; have := toInt_lt y have := toInd_add_toInt_lt_two_pow x y have := neg_two_pow_le_toInd_add_toInt x y - have bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) : (x.bmod m) < 0 ↔ (-(m / 2) ≤ x ∧ x < 0) ∨ ((m + 1) / 2 ≤ x) := by simp only [Int.bmod_def] From 4bb440bf3f514c8c8bd0a70ee41a5754dcd67d6a Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 09:43:35 +0000 Subject: [PATCH 36/57] feat: example with bv_decide proof --- tests/lean/run/bv_decide_rewriter.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean index 2c5ec606695a..5f753a3329d0 100644 --- a/tests/lean/run/bv_decide_rewriter.lean +++ b/tests/lean/run/bv_decide_rewriter.lean @@ -101,6 +101,8 @@ example (x y : BitVec 256) : x * y = y * x := by example {x y z : BitVec 64} : ~~~(x &&& (y * z)) = (~~~x ||| ~~~(z * y)) := by bv_decide (config := { acNf := true }) +example {x : BitVec 16} : (x = BitVec.allOnes 16) → (BitVec.uaddOverflow x x) := by bv_decide + end def foo (x : Bool) : Prop := x = true From 214c61376ab3e2231e9bcdee25c0eeb3cae1817a Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 09:45:45 +0000 Subject: [PATCH 37/57] chore: undo unrelated change --- src/Init/Data/BitVec/Lemmas.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 754294fcd57b..687ddfcdd84c 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3630,6 +3630,7 @@ 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)] + /-! ### Non-overflow theorems -/ /-- If `x.toNat + y.toNat < 2^w`, then the addition `(x + y)` does not overflow. -/ From d45bfc995e1541434047838169ac648d7df33b8c Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 09:49:33 +0000 Subject: [PATCH 38/57] chore: correct tests for bv_norm --- tests/lean/run/bv_decide_rewriter.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean index 5f753a3329d0..7b59c3cc56e5 100644 --- a/tests/lean/run/bv_decide_rewriter.lean +++ b/tests/lean/run/bv_decide_rewriter.lean @@ -87,9 +87,9 @@ example {x : BitVec 16} : x / (BitVec.twoPow 16 2) = x >>> 2 := by bv_normalize 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 -example (x y : BitVec 16) : BitVec.uaddOverflow x y = BitVec.carry 16 x y false := by bv_normalize +example (x y : BitVec 16) : BitVec.uaddOverflow x y = (x.setWidth (17) + y.setWidth (17)).msb := by bv_normalize example (x y : BitVec 16) : BitVec.saddOverflow x y = (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by bv_normalize -example (x y : BitVec w) : BitVec.uaddOverflow x y = BitVec.carry w x y false := by bv_normalize +example (x y : BitVec w) : BitVec.uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w + 1)).msb := by bv_normalize example (x y : BitVec w) : BitVec.saddOverflow x y = (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by bv_normalize From bcf668e8cd2dd03e71543368f6e423eebe53dd96 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 10:07:06 +0000 Subject: [PATCH 39/57] chore: update theorem name --- src/Init/Data/BitVec/Bitblast.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 8742dd1c6969..8ee70c40c261 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1233,7 +1233,7 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) : /-! ### Overflow definitions -/ -@[simp] theorem toNat_mod_lt_cancel {x : BitVec n} (h : n < m): x.toNat % (2 ^ m) = x.toNat := +@[simp] theorem toNat_mod_lt_eq {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 @@ -1247,8 +1247,7 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : saddOverflow x y ↔ (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by simp only [saddOverflow] rcases w with _|w - · revert x y - decide + · revert x y; decide · have := le_toInt x; have := toInt_lt x have := le_toInt y; have := toInt_lt y have := toInd_add_toInt_lt_two_pow x y @@ -1259,7 +1258,6 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : by_cases xpos : 0 ≤ x · rw [Int.emod_eq_of_lt xpos (by omega)]; omega · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega - simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, decide_eq_decide, BitVec.toInt_add] rw_mod_cast [bmod_neg_iff (by assumption) (by assumption), From b7bf54321c980e4c4778862a56cb2389b9bd58ff Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 10:29:20 +0000 Subject: [PATCH 40/57] chore: simplify toInt_lt --- src/Init/Data/BitVec/Lemmas.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 687ddfcdd84c..74bc5831a098 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -546,12 +546,10 @@ theorem toInt_lt {w : Nat} (x : BitVec w) : x.toInt < 2 ^ (w - 1) := by simp only [BitVec.toInt] rcases w with _|w' · omega - · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul] - by_cases h : 2 * x.toNat < 2 * 2 ^ (w' + 1 - 1) - · norm_cast - omega - · simp only [Nat.add_one_sub_one, Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, - Int.Nat.cast_ofNat_Int] + · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul, Nat.add_sub_cancel] + by_cases h : x.toNat < 2 ^ w' + · norm_cast; omega + · simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] norm_cast; omega theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by From 1243ed7dcdf2cca979297c21b0bcdbb996b9c420 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 10:32:52 +0000 Subject: [PATCH 41/57] chore: simpler le_toInt proof --- src/Init/Data/BitVec/Lemmas.lean | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 74bc5831a098..65656f627674 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -556,16 +556,10 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by simp only [BitVec.toInt] rcases w with _|w' · omega - · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul] - by_cases h : 2 * x.toNat < 2 * 2 ^ (w' - 1) -- i tried using split here but the final omega stops working?! im confused - · simp only [Nat.add_one_sub_one, Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, - Int.Nat.cast_ofNat_Int] - norm_cast - omega - · simp only [Nat.add_one_sub_one, Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, - Int.Nat.cast_ofNat_Int] - norm_cast - omega + · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul, Nat.add_sub_cancel] + simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]; + norm_cast + omega theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : x.toInt + y.toInt < 2 ^ w := by From 978ace8e5977738500dac452a541ef550e57bb4b Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 10:33:32 +0000 Subject: [PATCH 42/57] chore: simpler toInt_lt proof too --- src/Init/Data/BitVec/Lemmas.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 65656f627674..01edd209414e 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -547,10 +547,8 @@ theorem toInt_lt {w : Nat} (x : BitVec w) : x.toInt < 2 ^ (w - 1) := by rcases w with _|w' · omega · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul, Nat.add_sub_cancel] - by_cases h : x.toNat < 2 ^ w' - · norm_cast; omega - · simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] - norm_cast; omega + simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] + norm_cast; omega theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by simp only [BitVec.toInt] @@ -558,8 +556,7 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by · omega · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul, Nat.add_sub_cancel] simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]; - norm_cast - omega + norm_cast; omega theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : x.toInt + y.toInt < 2 ^ w := by From 81c9071c325d4d2119d6710ed5a88f8a62894d88 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 10:37:38 +0000 Subject: [PATCH 43/57] chore: golf toInd_add_toInt_lt_two_pow --- src/Init/Data/BitVec/Lemmas.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 01edd209414e..3d986fc5d49a 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -564,10 +564,9 @@ theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : · simp [BitVec.eq_nil x, BitVec.eq_nil y] · norm_cast rw [←Nat.two_pow_pred_add_two_pow_pred (by omega)] - have hx := toInt_lt x - have hy := toInt_lt y + have hx := toInt_lt x; rw [Nat.add_sub_cancel] at * + have hy := toInt_lt y; rw [Nat.add_sub_cancel] at * push_cast - rw [Nat.add_sub_cancel] at hx hy omega theorem neg_two_pow_le_toInd_add_toInt (x y : BitVec w) : From 4266a24e6485b76cdeeb24bf2aeccb06a29d8956 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 10:38:09 +0000 Subject: [PATCH 44/57] chore: golf neg_two_pow_le_toInd_add_toInt --- src/Init/Data/BitVec/Lemmas.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 3d986fc5d49a..afff4d9f2dbb 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -575,10 +575,9 @@ theorem neg_two_pow_le_toInd_add_toInt (x y : BitVec w) : · simp [BitVec.eq_nil x, BitVec.eq_nil y] · norm_cast rw [←Nat.two_pow_pred_add_two_pow_pred (by omega)] - have hx := le_toInt x - have hy := le_toInt y + have hx := le_toInt x; rw [Nat.add_sub_cancel] at * + have hy := le_toInt y; rw [Nat.add_sub_cancel] at * push_cast - rw [Nat.add_sub_cancel] at hx hy omega /-! ### slt -/ From f72ad6166d6f97cb0dc48754f7fe397e1d54f690 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 10:45:36 +0000 Subject: [PATCH 45/57] chore: golf toInd_add_toInt_lt_two_pow and neg_two_pow_le_toInd_add_toInt --- src/Init/Data/BitVec/Lemmas.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index afff4d9f2dbb..30143bfea703 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -562,22 +562,16 @@ theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : x.toInt + y.toInt < 2 ^ w := by rcases w with _|w' · simp [BitVec.eq_nil x, BitVec.eq_nil y] - · norm_cast - rw [←Nat.two_pow_pred_add_two_pow_pred (by omega)] - have hx := toInt_lt x; rw [Nat.add_sub_cancel] at * + · have hx := toInt_lt x; rw [Nat.add_sub_cancel] at * have hy := toInt_lt y; rw [Nat.add_sub_cancel] at * - push_cast omega theorem neg_two_pow_le_toInd_add_toInt (x y : BitVec w) : - 2 ^ w ≤ x.toInt + y.toInt := by rcases w with _|w' · simp [BitVec.eq_nil x, BitVec.eq_nil y] - · norm_cast - rw [←Nat.two_pow_pred_add_two_pow_pred (by omega)] - have hx := le_toInt x; rw [Nat.add_sub_cancel] at * + · have hx := le_toInt x; rw [Nat.add_sub_cancel] at * have hy := le_toInt y; rw [Nat.add_sub_cancel] at * - push_cast omega /-! ### slt -/ From 8c76c622c7d5447dad6f607b91bac6a33d23e2e2 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 24 Jan 2025 11:00:08 +0000 Subject: [PATCH 46/57] chore: erstore previous version and remove commas --- src/Init/Data/BitVec/Lemmas.lean | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 30143bfea703..05f00d87c218 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -546,7 +546,7 @@ theorem toInt_lt {w : Nat} (x : BitVec w) : x.toInt < 2 ^ (w - 1) := by simp only [BitVec.toInt] rcases w with _|w' · omega - · rw [←Nat.two_pow_pred_add_two_pow_pred (by omega), ←Nat.two_mul, Nat.add_sub_cancel] + · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul, Nat.add_sub_cancel] simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] norm_cast; omega @@ -555,23 +555,25 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by rcases w with _|w' · omega · rw [← Nat.two_pow_pred_add_two_pow_pred (by omega), ← Nat.two_mul, Nat.add_sub_cancel] - simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int]; + simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] norm_cast; omega theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : x.toInt + y.toInt < 2 ^ w := by rcases w with _|w' · simp [BitVec.eq_nil x, BitVec.eq_nil y] - · have hx := toInt_lt x; rw [Nat.add_sub_cancel] at * - have hy := toInt_lt y; rw [Nat.add_sub_cancel] at * + · have hx := toInt_lt x + have hy := toInt_lt y + rw [Nat.add_sub_cancel] at hx hy omega theorem neg_two_pow_le_toInd_add_toInt (x y : BitVec w) : - 2 ^ w ≤ x.toInt + y.toInt := by rcases w with _|w' · simp [BitVec.eq_nil x, BitVec.eq_nil y] - · have hx := le_toInt x; rw [Nat.add_sub_cancel] at * - have hy := le_toInt y; rw [Nat.add_sub_cancel] at * + · have hx := le_toInt x + have hy := le_toInt y + rw [Nat.add_sub_cancel] at hx hy omega /-! ### slt -/ From fc22884917fe453ff3b76b14b261429bedd4689e Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Mon, 27 Jan 2025 12:19:31 +0000 Subject: [PATCH 47/57] chore: fix bool coercion --- src/Init/Data/BitVec/Bitblast.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 8ee70c40c261..a270c36cf2ca 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1244,7 +1244,7 @@ theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : simp [uaddOverflow, msb_add, msb_setWidth, carry] theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : - saddOverflow x y ↔ (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by + saddOverflow x y = (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by simp only [saddOverflow] rcases w with _|w · revert x y; decide @@ -1262,6 +1262,7 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : decide_eq_decide, BitVec.toInt_add] rw_mod_cast [bmod_neg_iff (by assumption) (by assumption), ← @Nat.two_pow_pred_add_two_pow_pred (w + 1) (by omega)] at * + rw [_root_.eq_iff_iff] omega end BitVec From 4537011e5fa7e112aaf6b2cfd4ed7499e61dd12d Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Mon, 27 Jan 2025 15:20:06 +0000 Subject: [PATCH 48/57] chore: parentheses and brackets --- src/Init/Data/BitVec/Bitblast.lean | 8 ++++---- src/Init/Data/BitVec/Lemmas.lean | 16 ++++++++-------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index a270c36cf2ca..992f7d44cd8d 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1248,10 +1248,10 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : simp only [saddOverflow] rcases w with _|w · revert x y; decide - · have := le_toInt x; have := toInt_lt x - have := le_toInt y; have := toInt_lt y - have := toInd_add_toInt_lt_two_pow x y - have := neg_two_pow_le_toInd_add_toInt x y + · have := le_toInt (x := x); have := toInt_lt (x := x) + have := le_toInt (x := y); have := toInt_lt (x := y) + have := toInd_add_toInt_lt_two_pow (x := x) (y := y) + have := neg_two_pow_le_toInd_add_toInt (x := x) (y := y) have bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) : (x.bmod m) < 0 ↔ (-(m / 2) ≤ x ∧ x < 0) ∨ ((m + 1) / 2 ≤ x) := by simp only [Int.bmod_def] diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 05f00d87c218..ac16f82acf14 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -542,7 +542,7 @@ 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 +theorem toInt_lt {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1) := by simp only [BitVec.toInt] rcases w with _|w' · omega @@ -550,7 +550,7 @@ theorem toInt_lt {w : Nat} (x : BitVec w) : x.toInt < 2 ^ (w - 1) := by simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] norm_cast; omega -theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by +theorem le_toInt {w : Nat} {x : BitVec w} : -2 ^ (w - 1) ≤ x.toInt := by simp only [BitVec.toInt] rcases w with _|w' · omega @@ -558,21 +558,21 @@ theorem le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt := by simp only [Nat.zero_lt_succ, Nat.mul_lt_mul_left, Int.natCast_mul, Int.Nat.cast_ofNat_Int] norm_cast; omega -theorem toInd_add_toInt_lt_two_pow (x y : BitVec w) : +theorem toInd_add_toInt_lt_two_pow {x y : BitVec w} : x.toInt + y.toInt < 2 ^ w := by rcases w with _|w' · simp [BitVec.eq_nil x, BitVec.eq_nil y] - · have hx := toInt_lt x - have hy := toInt_lt y + · have hx := toInt_lt (x := x) + have hy := toInt_lt (x := y) rw [Nat.add_sub_cancel] at hx hy omega -theorem neg_two_pow_le_toInd_add_toInt (x y : BitVec w) : +theorem neg_two_pow_le_toInd_add_toInt {x y : BitVec w} : - 2 ^ w ≤ x.toInt + y.toInt := by rcases w with _|w' · simp [BitVec.eq_nil x, BitVec.eq_nil y] - · have hx := le_toInt x - have hy := le_toInt y + · have hx := le_toInt (x := x) + have hy := le_toInt (x := y) rw [Nat.add_sub_cancel] at hx hy omega From e1fbe8b6e1f940b96408be982d3c145ea406783e Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Tue, 28 Jan 2025 09:05:38 +0000 Subject: [PATCH 49/57] chore: golf proof Co-authored-by: Tobias Grosser --- src/Init/Data/BitVec/Bitblast.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 992f7d44cd8d..0f3a87d35d9d 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1233,11 +1233,9 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) : /-! ### Overflow definitions -/ -@[simp] theorem toNat_mod_lt_eq {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 - ) +@[simp] theorem toNat_mod_lt_eq {x : BitVec n} (h : n < m) : x.toNat % (2 ^ m) = x.toNat := by + have : 2 ^ n < 2 ^ m := Nat.pow_lt_pow_of_lt (by omega) h + exact Nat.mod_eq_of_lt (by omega) theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w + 1)).msb := by From e97dfed74cb18a032cb8afb08cf08202f4a259dd Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Tue, 28 Jan 2025 10:51:26 +0000 Subject: [PATCH 50/57] chore: rename and move toNat_mod_cancel_of_lt --- src/Init/Data/BitVec/Bitblast.lean | 5 ----- src/Init/Data/BitVec/Lemmas.lean | 4 ++++ 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 0f3a87d35d9d..0d96bda163c1 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1232,11 +1232,6 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) : /-! ### Overflow definitions -/ - -@[simp] theorem toNat_mod_lt_eq {x : BitVec n} (h : n < m) : x.toNat % (2 ^ m) = x.toNat := by - have : 2 ^ n < 2 ^ m := Nat.pow_lt_pow_of_lt (by omega) h - exact Nat.mod_eq_of_lt (by omega) - theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w + 1)).msb := by simp [uaddOverflow, msb_add, msb_setWidth, carry] diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index ac16f82acf14..8af300ae1e5d 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -326,6 +326,10 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) : simp only [toNat_eq, toNat_ofNat, Nat.zero_mod] at h rw [Nat.mod_eq_of_lt (by omega)] +@[simp] theorem toNat_mod_cancel_of_lt {x : BitVec n} (h : n < m) : x.toNat % (2 ^ m) = x.toNat := by + have : 2 ^ n < 2 ^ m := Nat.pow_lt_pow_of_lt (by omega) h + exact Nat.mod_eq_of_lt (by omega) + @[simp] theorem sub_sub_toNat_cancel {x : BitVec w} : 2 ^ w - (2 ^ w - x.toNat) = x.toNat := by simp [Nat.sub_sub_eq_min, Nat.min_eq_right] From 6ddf15074ac67bd9614acb07e0b9136c9be00e53 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 30 Jan 2025 22:42:08 +0000 Subject: [PATCH 51/57] chore: indentation --- src/Init/Data/BitVec/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 8af300ae1e5d..6075e2cc96eb 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -327,8 +327,8 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) : rw [Nat.mod_eq_of_lt (by omega)] @[simp] theorem toNat_mod_cancel_of_lt {x : BitVec n} (h : n < m) : x.toNat % (2 ^ m) = x.toNat := by - have : 2 ^ n < 2 ^ m := Nat.pow_lt_pow_of_lt (by omega) h - exact Nat.mod_eq_of_lt (by omega) + have : 2 ^ n < 2 ^ m := Nat.pow_lt_pow_of_lt (by omega) h + exact Nat.mod_eq_of_lt (by omega) @[simp] theorem sub_sub_toNat_cancel {x : BitVec w} : 2 ^ w - (2 ^ w - x.toNat) = x.toNat := by From aaf2b46aa09edb6bf9a23b9084193a7906067e39 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 30 Jan 2025 22:42:31 +0000 Subject: [PATCH 52/57] chore: typo --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 6075e2cc96eb..911243aac8ab 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -571,7 +571,7 @@ theorem toInd_add_toInt_lt_two_pow {x y : BitVec w} : rw [Nat.add_sub_cancel] at hx hy omega -theorem neg_two_pow_le_toInd_add_toInt {x y : BitVec w} : +theorem neg_two_pow_le_toInt_add_toInt {x y : BitVec w} : - 2 ^ w ≤ x.toInt + y.toInt := by rcases w with _|w' · simp [BitVec.eq_nil x, BitVec.eq_nil y] From 204633f323e34d34b5f98f2f7d36343ea2628e16 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Thu, 30 Jan 2025 22:49:26 +0000 Subject: [PATCH 53/57] chore: docstring Co-authored-by: Alex Keizer --- src/Init/Data/BitVec/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 4ded4ab196e7..3374d1d25b0e 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -671,7 +671,7 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length /-! ## Overflow -/ -/-- Overflow predicate for unsigned addition modulo 2^w. +/-- `uaddOverflow x y` returns `true` if addition of `x` and `y` results in *unsigned* overflow. SMT-Lib name: `bvuaddo`. -/ From bdff0b70a816ac157b9d7a3c6e97d10df0934baf Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Thu, 30 Jan 2025 22:49:45 +0000 Subject: [PATCH 54/57] chore: docstring Co-authored-by: Alex Keizer --- src/Init/Data/BitVec/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 3374d1d25b0e..0a9de079b54d 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/src/Init/Data/BitVec/Basic.lean @@ -677,7 +677,8 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length -/ def uaddOverflow {w : Nat} (x y : BitVec w) : Bool := x.toNat + y.toNat ≥ 2 ^ w -/-- Overflow predicate for signed addition on w-bit 2's complement. +/-- `saddOverflow x y` returns `true` if addition of `x` and `y` results in *signed* overflow, +treating `x` and `y` as 2's complement signed bitvectors. SMT-Lib name: `bvsaddo`. -/ From 62b551cfc70f925ddb963917848aa50e45241f11 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Thu, 30 Jan 2025 22:50:02 +0000 Subject: [PATCH 55/57] chore: docstring Co-authored-by: Alex Keizer --- src/Init/Data/BitVec/Bitblast.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 0d96bda163c1..1bddd6bb2ea9 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1232,6 +1232,7 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) : /-! ### Overflow definitions -/ +/-- Unsigned addition overflows iff the final carry bit of the addition circuit is `true`. -/ theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : uaddOverflow x y = (x.setWidth (w + 1) + y.setWidth (w + 1)).msb := by simp [uaddOverflow, msb_add, msb_setWidth, carry] From ce311f8f6324001bf97acf24b300548d0958ce28 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 30 Jan 2025 23:08:06 +0000 Subject: [PATCH 56/57] chore: fix typo and fix build --- src/Init/Data/BitVec/Bitblast.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 1bddd6bb2ea9..78d0d1caaad7 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1245,7 +1245,7 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : · have := le_toInt (x := x); have := toInt_lt (x := x) have := le_toInt (x := y); have := toInt_lt (x := y) have := toInd_add_toInt_lt_two_pow (x := x) (y := y) - have := neg_two_pow_le_toInd_add_toInt (x := x) (y := y) + have := neg_two_pow_le_toInt_add_toInt (x := x) (y := y) have bmod_neg_iff {m : Nat} {x : Int} (h2 : -m ≤ x) (h1 : x < m) : (x.bmod m) < 0 ↔ (-(m / 2) ≤ x ∧ x < 0) ∨ ((m + 1) / 2 ≤ x) := by simp only [Int.bmod_def] From 2697dc0ebfe72e6fac263e36deb0382f2cadd6f4 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 31 Jan 2025 15:13:17 +0000 Subject: [PATCH 57/57] chore: fix boolean ops --- src/Init/Data/BitVec/Bitblast.lean | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 78d0d1caaad7..84d41fde527b 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/src/Init/Data/BitVec/Bitblast.lean @@ -1238,11 +1238,12 @@ theorem uaddOverflow_eq {w : Nat} (x y : BitVec w) : simp [uaddOverflow, msb_add, msb_setWidth, carry] theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : - saddOverflow x y = (x.msb = y.msb ∧ ¬(x + y).msb = x.msb) := by + saddOverflow x y = (x.msb == y.msb && !((x + y).msb == x.msb)) := by simp only [saddOverflow] rcases w with _|w · revert x y; decide - · have := le_toInt (x := x); have := toInt_lt (x := x) + · simp [decide_eq_true] + have := le_toInt (x := x); have := toInt_lt (x := x) have := le_toInt (x := y); have := toInt_lt (x := y) have := toInd_add_toInt_lt_two_pow (x := x) (y := y) have := neg_two_pow_le_toInt_add_toInt (x := x) (y := y) @@ -1252,11 +1253,12 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) : by_cases xpos : 0 ≤ x · rw [Int.emod_eq_of_lt xpos (by omega)]; omega · rw [Int.add_emod_self.symm, Int.emod_eq_of_lt (by omega) (by omega)]; omega - simp only [ge_iff_le, Bool.or_eq_true, decide_eq_true_eq, BitVec.msb_eq_toInt, - decide_eq_decide, BitVec.toInt_add] - rw_mod_cast [bmod_neg_iff (by assumption) (by assumption), - ← @Nat.two_pow_pred_add_two_pow_pred (w + 1) (by omega)] at * - rw [_root_.eq_iff_iff] - omega + simp only [← decide_or, msb_eq_toInt, decide_beq_decide, toInt_add, ← decide_not, ← decide_and, + decide_eq_decide] + rw [bmod_neg_iff (by rw [← Nat.two_pow_pred_add_two_pow_pred (by omega)]; push_cast; omega) + (by rw [← Nat.two_pow_pred_add_two_pow_pred (by omega)]; push_cast; omega), + ← @Nat.two_pow_pred_add_two_pow_pred (w + 1) (by omega), Nat.add_one_sub_one] at * + · push_cast + omega end BitVec