feat: add BitVec.(negOverflow, negOverflow_eq) (#7554)

This PR adds SMT-LIB operators to detect overflow `BitVec.negOverflow`,
according to the [SMTLIB
standard](https://github.com/SMT-LIB/SMT-LIB-2/blob/2.7/Theories/FixedSizeBitVectors.smt2),
and the theorem proving equivalence of such definition with the `BitVec`
library functions (`negOverflow_eq`).

Co-authored by @bollu and @alexkeizer

---------

Co-authored-by: Siddharth <siddu.druid@gmail.com>

src/Init/Data/BitVec/Basic.lean

@@ -690,6 +690,14 @@ treating `x` and `y` as 2's complement signed bitvectors.
 def saddOverflow {w : Nat} (x y : BitVec w) : Bool :=
   (x.toInt + y.toInt ≥ 2 ^ (w - 1)) || (x.toInt + y.toInt < - 2 ^ (w - 1))
 
+/-- `negOverflow x` returns `true` if the negation of `x` results in overflow. 
+For a BitVec `x` with width `0 < w`, this only happens if `x = intMin`. 
+
+  SMT-Lib name: `bvnego`.
+-/
+def negOverflow {w : Nat} (x : BitVec w) : Bool :=
+  x.toInt == - 2 ^ (w - 1)
+
 /- ### reverse -/
 
 /-- Reverse the bits in a bitvector. -/

src/Init/Data/BitVec/Bitblast.lean

@@ -1299,6 +1299,15 @@ theorem saddOverflow_eq {w : Nat} (x y : BitVec w) :
     simp
     omega
 
+theorem negOverflow_eq {w : Nat} (x : BitVec w) :
+    (negOverflow x) = (decide (0 < w) && (x == intMin w)) := by
+  simp only [negOverflow]
+  rcases w with _|w
+  · simp [toInt_of_zero_length, Int.min_eq_right]
+  · suffices - 2 ^ w = (intMin (w + 1)).toInt by simp [beq_eq_decide_eq, ← toInt_inj, this]
+    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])]
+
 /- ### umod -/
 
 theorem getElem_umod {n d : BitVec w} (hi : i < w) :

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

@@ -353,6 +353,7 @@ attribute [bv_normalize] BitVec.umod_eq_and
 
 attribute [bv_normalize] BitVec.saddOverflow_eq
 attribute [bv_normalize] BitVec.uaddOverflow_eq
+attribute [bv_normalize] BitVec.negOverflow_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

@@ -621,6 +621,8 @@ example {x y : BitVec 8} : (-x) <<< y = -(x <<< y) := by bv_normalize
 
 example {x : BitVec 16} : (x = BitVec.allOnes 16) → (BitVec.uaddOverflow x x) := by bv_decide
 
+example {x : BitVec 64} : (x = BitVec.intMin 64) ↔ (BitVec.negOverflow x) := by bv_decide
+
 section
 
 namespace NormalizeMul