feat: add BitVec.sdivOverflow definition and lemmas for overflow in signed and unsigned division (#7671)

This PR contains the theorem proving that signed division x.toInt /
y.toInt only overflows when `x = intMin w` and `y = allOnes w` (for `0 <
w`).
To show that this is the *only* case in which overflow happens, we refer
to overflow for negation
(`BitVec.sdivOverflow_eq_negOverflow_of_neg_one`): in fact,
`x.toInt/(allOnes w).toInt = - x.toInt`, i.e., the overflow conditions
are the same as `negOverflow` for `x`, and then reason about the signs
of the operands with the respective theorems.
These BitVec theorems themselves rely on numerous `Int.ediv_*` theorems,
that carefully set the bounds of signed division for integers.

co-authored by @bollu, @tobiasgrosser

src/Init/Data/BitVec/Basic.lean

@@ -769,6 +769,15 @@ SMT-Lib name: `bvnego`.
 def negOverflow {w : Nat} (x : BitVec w) : Bool :=
   x.toInt == - 2 ^ (w - 1)
 
+/--
+Checks whether the signed division of `x` by `y` results in overflow.
+For BitVecs `x` and `y` with nonzero width, this only happens if `x = intMin` and `y = allOnes w`.
+
+SMT-LIB name: `bvsdivo`.
+-/
+def sdivOverflow {w : Nat} (x y : BitVec w) : Bool :=
+  (2 ^ (w - 1) ≤ x.toInt / y.toInt) || (x.toInt / y.toInt <  - 2 ^ (w - 1))
+
 /- ### reverse -/
 
 /-- Reverses the bits in a bitvector. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -1361,6 +1361,38 @@ theorem negOverflow_eq {w : Nat} (x : BitVec w) :
     simp only [toInt_intMin, Nat.add_one_sub_one, Int.ofNat_emod, Int.neg_inj]
     rw_mod_cast [Nat.mod_eq_of_lt (by simp [Nat.pow_lt_pow_succ])]
 
+/--
+  Prove that signed division `x.toInt / y.toInt` only overflows when `x = intMin w` and `y = allOnes w` (for `0 < w`).
+-/
+theorem sdivOverflow_eq {w : Nat} (x y : BitVec w) :
+    (sdivOverflow x y) = (decide (0 < w) && (x = intMin w) && (y = allOnes w)) := by
+  rcases w with _|w
+  · simp [sdivOverflow, of_length_zero]
+  · have yle := le_two_mul_toInt (x := y)
+    have ylt := two_mul_toInt_lt (x := y)
+    -- if y = allOnes (w + 1), thus y.toInt = -1,
+    -- the division overflows iff x = intMin (w + 1), as for negation
+    by_cases hy : y = allOnes (w + 1)
+    · simp [sdivOverflow_eq_negOverflow_of_eq_allOnes, negOverflow_eq, ← hy, beq_eq_decide_eq]
+    · simp only [sdivOverflow, hy, bool_to_prop]
+      have := BitVec.neg_two_pow_le_toInt_ediv (x := x) (y := y)
+      simp only [Nat.add_one_sub_one] at this
+      by_cases hx : 0 ≤ x.toInt
+      · by_cases hy' : 0 ≤ y.toInt
+        · have := BitVec.toInt_ediv_toInt_lt_of_nonneg_of_nonneg
+                (x := x) (y := y) (by omega) (by omega)
+          simp only [Nat.add_one_sub_one] at this; simp; omega
+        · have := BitVec.toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos
+                (x := x) (y := y) (by omega) (by omega)
+          simp; omega
+      · by_cases hy' : 0 ≤ y.toInt
+        · have :=  BitVec.toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg
+                (x := x) (y := y) (by omega) (by omega)
+          simp; omega
+        · have := BitVec.toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one
+                (x := x) (y := y) (by omega) (by rw [← toInt_inj, toInt_allOnes] at hy; omega)
+          simp only [Nat.add_one_sub_one] at this; simp; omega
+
 theorem umulOverflow_eq {w : Nat} (x y : BitVec w) :
     umulOverflow x y =
       (0 < w && BitVec.twoPow (w * 2) w ≤ x.zeroExtend (w * 2) * y.zeroExtend (w * 2)) := by

src/Init/Data/BitVec/Lemmas.lean

@@ -4150,6 +4150,110 @@ theorem sdiv_self {x : BitVec w} :
       rcases x.msb with msb | msb <;> simp
     · rcases x.msb with msb | msb <;> simp [h]
 
+/-- Unsigned division never overflows. -/
+theorem toNat_div_toNat_lt {w : Nat} {x y : BitVec w} :
+    x.toNat / y.toNat < 2 ^ w := by
+  have hy : y.toNat = 0 ∨ y.toNat = 1 ∨ 1 < y.toNat := by omega
+  rcases hy with hy|hy|hy
+  · simp [hy]; omega
+  · simp [hy]; omega
+  · rw [Nat.div_lt_iff_lt_mul (k := y.toNat) (x := x.toNat) (y := 2 ^ w) (by omega), show x.toNat = x.toNat * 1 by omega]
+    apply Nat.mul_lt_mul_of_le_of_lt (by omega) (by omega) (by omega)
+
+/-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonneg. -/
+theorem toInt_ediv_toInt_lt_of_nonneg_of_nonneg {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : 0 ≤ y.toInt) :
+    x.toInt / y.toInt < 2 ^ (w - 1) := by
+  rcases w with _|w
+  · simp [of_length_zero]
+  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
+    by_cases hy' : y.toInt = 1
+    · simp [hy', Int.ediv_one]; omega
+    · by_cases hx' : x.toInt = 0
+      · simp only [hx', Int.zero_ediv, Nat.add_one_sub_one, gt_iff_lt]
+        norm_cast
+        exact Nat.two_pow_pos (w := w)
+      · have := Int.ediv_lt_self_of_pos_of_ne_one (x := x.toInt) (y := y.toInt) (by omega) (by omega)
+        simp; omega
+
+/-- Non-overflowing signed division bounds when numerator is nonpos, denominator is nonneg. -/
+theorem toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : 0 ≤ y.toInt) :
+    x.toInt / y.toInt ≤ 0 := by
+  rcases w with _|w
+  · simp [of_length_zero]
+  · by_cases hx' : x.toInt = 0
+    · simp [hx']
+    · by_cases hy' : y.toInt = 0
+      · simp [hy']
+      · have := Int.ediv_neg_of_neg_of_pos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
+        simp; omega
+
+/-- Non-overflowing signed division bounds when numerator is nonneg, denominator is nonpos. -/
+theorem toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : y.toInt ≤ 0) :
+   x.toInt / y.toInt ≤ 0 := by
+  rcases w with _|w
+  · simp [of_length_zero]
+  · by_cases hy' : y.toInt = -1
+    · simp [hy']; omega
+    · have := Int.ediv_nonpos_of_nonneg_of_nonpos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
+      simp; omega
+
+/-- Given the definition of ediv/emod for signed integer division (https://dl.acm.org/doi/pdf/10.1145/128861.128862)
+  we have that for two integers `x` and `y`: `x/y = q ↔ x.ediv y = q ↔ r = x.emod y`
+  and in particular: `-1/y = q ↔ -1.ediv y = q ↔ r = -1.emod y`.
+  from which it follows that:
+  (-1)/0 = 0
+  (-1)/y = -1 when 0 < y
+  (-1)/(-5) = 1 when y < 0
+-/
+theorem neg_one_ediv_toInt_eq {w : Nat} {y : BitVec w} :
+    (-1) / y.toInt = if y.toInt = 0 then 0 else if 0 < y.toInt then -1 else 1 := by
+  rcases w with _|_|w
+  · simp [of_length_zero]
+  · cases eq_zero_or_eq_one y
+    · case _ h => simp [h]
+    · case _ h => simp [h]
+  · by_cases 0 < y.toInt
+    · simp [Int.sign_eq_one_of_pos (a := y.toInt) (by omega), Int.neg_one_ediv]
+      omega
+    · by_cases hy : y.toInt = 0
+      · simp [hy]
+      · simp [Int.sign_eq_neg_one_of_neg (a := y.toInt) (by omega), Int.neg_one_ediv]
+        omega
+
+/-- Non-overflowing signed division bounds when numerator is nonpos, denominator is less than -1. -/
+theorem toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : y.toInt < -1) :
+    x.toInt / y.toInt < 2 ^ (w - 1) := by
+  rcases w with _|_|w
+  · simp [of_length_zero]
+  · have hy := eq_zero_or_eq_one (a := y)
+    simp [← toInt_inj, toInt_zero, toInt_one] at hy
+    omega
+  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
+    have hx' : x.toInt = 0 ∨ x.toInt = - 1 ∨ x.toInt < - 1 := by omega
+    rcases hx' with hx'|hx'|hx'
+    · simp [hx']; omega
+    · have := BitVec.neg_one_ediv_toInt_eq (y := y)
+      simp only [toInt_allOnes, Nat.lt_add_left_iff_pos, Nat.zero_lt_succ, ↓reduceIte,
+        Int.reduceNeg] at this
+      simp [hx', this]
+      omega
+    · have := Int.ediv_lt_natAbs_self_of_lt_neg_one_of_lt_neg_one (x := x.toInt) (y := y.toInt) (by omega) hy
+      simp; omega
+
+/-- Signed division of (x y : BitVec w) is always -2 ^ w ≤ x.toInt / y.toInt. -/
+theorem neg_two_pow_le_toInt_ediv {x y : BitVec w} :
+    - 2 ^ (w - 1) ≤ x.toInt / y.toInt := by
+  have xlt := @toInt_lt w x; have lex := @le_toInt w x
+  by_cases hx : 0 ≤ x.toInt <;> by_cases hy : 0 ≤ y.toInt
+  · have := Int.ediv_nonneg_of_nonneg_of_nonneg (x := x.toInt) (y := y.toInt) hx hy
+    omega
+  · have := Int.neg_self_le_ediv_of_nonneg_of_nonpos (x := x.toInt) (y := y.toInt) hx (by omega)
+    omega
+  · have := Int.self_le_ediv_of_nonpos_of_nonneg (x := x.toInt) (y := y.toInt) (by omega) hy
+    omega
+  · have := Int.ediv_nonneg_of_nonpos_of_nonpos (a := x.toInt) (b := y.toInt) (by omega) (by omega)
+    omega
+
 /-! ### smtSDiv -/
 
 theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
@@ -5147,6 +5251,22 @@ theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
     BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]
   omega
 
+theorem sdiv_neg_one {w : Nat} {x : BitVec w} :
+    x.toInt / -1 = -x.toInt := by
+  rcases w with _|w
+  · simp [of_length_zero]
+  · simp [toInt_allOnes]
+
+theorem sdivOverflow_eq_negOverflow_of_eq_allOnes {w : Nat} {x y : BitVec w} (hy : y = allOnes w) :
+    sdivOverflow x y = negOverflow x := by
+  rcases w with _|w
+  · simp [sdivOverflow, negOverflow, of_length_zero]
+  · have xle := le_two_mul_toInt (x := x); have xlt := two_mul_toInt_lt (x := x)
+    simp only [sdivOverflow, hy, show ¬2 ^ w < x.toInt by omega, negOverflow]
+    by_cases hx : x.toInt = - 2 ^ w
+    · simp [hx]
+    · simp [show ¬x.toInt == -2 ^ w by simp only [beq_iff_eq, hx, not_false_eq_true]]; omega
+
 theorem two_pow_le_toInt_mul_toInt_iff {x y : BitVec w} :
     2 ^ (w - 1) ≤ x.toInt * y.toInt ↔
       (signExtend (w * 2) (intMax w)).slt (signExtend (w * 2) x * signExtend (w * 2) y) := by

src/Init/Data/Int/DivMod/Lemmas.lean

@@ -2896,6 +2896,65 @@ theorem bmod_eq_self_of_le_mul_two {x : Int} {y : Nat} (hle : -y ≤ x * 2) (hlt
     x.bmod y = x :=
   bmod_eq_of_le_mul_two hle hlt
 
+/- ### ediv -/
+
+theorem ediv_lt_self_of_pos_of_ne_one {x y : Int} (hx : 0 < x) (hy : y ≠ 1) :
+    x / y < x := by
+  by_cases hy' : 1 < y
+  · obtain ⟨xn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := x) (by omega)
+    obtain ⟨yn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := y) (by omega)
+    rw [← Int.ofNat_ediv]
+    norm_cast
+    apply Nat.div_lt_self (by omega) (by omega)
+  · have := @Int.ediv_nonpos_of_nonneg_of_nonpos x y (by omega) (by omega)
+    omega
+
+theorem ediv_nonneg_of_nonneg_of_nonneg {x y : Int} (hx : 0 ≤ x) (hy : 0 ≤ y) :
+    0 ≤ x / y := by
+  obtain ⟨xn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := x) (by omega)
+  obtain ⟨yn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := y) (by omega)
+  rw [← Int.ofNat_ediv]
+  exact Int.ofNat_zero_le (xn / yn)
+
+/--  When both x and y are negative we need stricter bounds on x and y
+  to establish the upper bound of x/y, i.e., x / y < x.natAbs.
+  In particular, consider the following counter examples:
+  · (-1) / (-2) = 1 and ¬ 1 < (-1).natAbs
+    (note that Int.neg_one_ediv already handles `ediv` where the numerator is -1)
+  · (-2) / (-1) = 2 and ¬ 1 < (-2).natAbs
+  To exclude these cases, we enforce stricter bounds on the values of x and y.
+-/
+theorem ediv_lt_natAbs_self_of_lt_neg_one_of_lt_neg_one {x y : Int} (hx : x < -1) (hy : y < -1) :
+    x / y < x.natAbs := by
+  obtain ⟨xn, rfl⟩ := Int.eq_negSucc_of_lt_zero (a := x) (by omega)
+  obtain ⟨yn, rfl⟩ := Int.eq_negSucc_of_lt_zero (a := y) (by omega)
+  simp only [negSucc_ediv_negSucc, Int.natCast_add, natCast_ediv, cast_ofNat_Int, natAbs_negSucc,
+    Nat.succ_eq_add_one, Int.add_lt_add_iff_right]
+  rw_mod_cast [Nat.div_lt_iff_lt_mul (x := xn) (k := yn + 1) (y := xn) (by omega),
+    show (xn < xn * (yn + 1)) = (1 * xn < (yn + 1) * xn) by rw [Nat.one_mul, Nat.mul_comm]]
+  apply Nat.mul_lt_mul_of_lt_of_le (a := 1) (b := xn) (c := yn + 1) (d := xn) (by omega) (by omega) (by omega)
+
+theorem self_le_ediv_of_nonpos_of_nonneg {x y : Int} (hx : x ≤ 0) (hy : 0 ≤ y) :
+    x ≤ x / y := by
+  by_cases hx' : x = 0
+  · simp [hx', zero_ediv]
+  · by_cases hy : y = 0
+    · simp [hy]; omega
+    · simp only [ge_iff_le, Int.le_ediv_iff_mul_le (c := y) (a := x) (b := x) (by omega),
+        show (x * y ≤ x) = (x * y ≤ x * 1) by rw [Int.mul_one], Int.mul_one]
+      apply Int.mul_le_mul_of_nonpos_left (a := x) (b := y) (c  := (1 : Int)) (by omega) (by omega)
+
+theorem neg_self_le_ediv_of_nonneg_of_nonpos (x y : Int) (hx : 0 ≤ x) (hy : y ≤ 0) :
+    -x ≤ x / y := by
+  by_cases hy' : y = 0
+  · simp [hy']; omega
+  · obtain ⟨xn, rfl⟩ := Int.eq_ofNat_of_zero_le (a := x) (by omega)
+    obtain ⟨yn, rfl⟩ := Int.eq_negSucc_of_lt_zero (a := y) (by omega)
+    rw [show xn = ofNat xn by norm_cast, Int.ofNat_ediv_negSucc (a := xn)]
+    simp only [ofNat_eq_coe, natCast_ediv, Int.natCast_add, cast_ofNat_Int, Int.neg_le_neg_iff]
+    norm_cast
+    apply Nat.le_trans (m := xn) (by exact Nat.div_le_self xn (yn + 1)) (by omega)
+
 /-! Helper theorems for `dvd` simproc -/
 
 protected theorem dvd_eq_true_of_mod_eq_zero {a b : Int} (h : b % a == 0) : (a ∣ b) = True := by

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

@@ -362,6 +362,7 @@ attribute [bv_normalize] BitVec.umulOverflow_eq
 attribute [bv_normalize] BitVec.smulOverflow_eq
 attribute [bv_normalize] BitVec.usubOverflow_eq
 attribute [bv_normalize] BitVec.ssubOverflow_eq
+attribute [bv_normalize] BitVec.sdivOverflow_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) :

tests/lean/run/bv_decide_rewriter.lean

@@ -647,6 +647,8 @@ example {x y : BitVec 64} : ((x = 0#64) ∧ (y = BitVec.allOnes 64)) → (BitVec
 
 example {x y : BitVec 64} : ((x = BitVec.twoPow 64 62) ∧ (y = BitVec.twoPow 64 63)) → (BitVec.ssubOverflow x y) := by bv_decide
 
+example {x y : BitVec 64} : ((x = BitVec.intMin 64) ∧ (y = BitVec.allOnes 64)) ↔ (BitVec.sdivOverflow x y) := by bv_decide
+
 -- BV_EXTRACT_ADD_MUL
 example {x y : BitVec 8} :
     BitVec.extractLsb' 0 4 (x + y) = BitVec.extractLsb' 0 4 x + BitVec.extractLsb' 0 4 y := by