feat: add SMT-LIB overflow on addition for bitvectors (uadd_overflow,sadd_overflow, uadd_overflow_eq,sadd_overflow_eq) and support theorems

src/Init/Data/BitVec/Basic.lean

@@ -669,6 +669,21 @@ def ofBoolListLE : (bs : List Bool) → BitVec bs.length
 | [] => 0#0
 | b :: bs => concat (ofBoolListLE bs) b
 
+/-! ## Overflow -/
+
+/-- Overflow predicate for unsigned addition modulo 2^w.
+
+  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.
+
+  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))
+
 /- ### reverse -/
 
 /-- Reverse the bits in a bitvector. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -1230,4 +1230,38 @@ theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) :
   · simp [of_length_zero]
   · simp [ushiftRightRec_eq]
 
+/-! ### 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
+  )
+
+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]
+
+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 := 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 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
+    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

src/Init/Data/BitVec/Lemmas.lean

@@ -542,6 +542,40 @@ 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]
+  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]
+    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, 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
+  rcases w with _|w'
+  · simp [BitVec.eq_nil x, BitVec.eq_nil y]
+  · 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
+    have hy := le_toInt y
+    rw [Nat.add_sub_cancel] at hx hy
+    omega
+
 /-! ### slt -/
 
 /--

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -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
+
 /-- `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

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 = (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 = (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
+
 
 section
 
@@ -96,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