From 637d8b2a2de3e26c6233c90c9a03f9a889bd720e Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Thu, 20 Mar 2025 12:43:43 +0000
Subject: [PATCH] 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               | 8 ++++++++
 src/Init/Data/BitVec/Bitblast.lean            | 9 +++++++++
 src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 1 +
 tests/lean/run/bv_decide_rewriter.lean        | 2 ++
 4 files changed, 20 insertions(+)

diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 9a7764d3ab..a641294549 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/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. -/
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index aeda7fc646..40e94b945a 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/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) :
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index 01c88ef72b..306616becd 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/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) :
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 114992b676..5df1b2643d 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/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