From 4ab1b2875c7e523a3073f649cd4117750d398c82 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 28 Oct 2024 16:41:38 +0100
Subject: [PATCH 1/2] feat: add _eq lemmas for SMTLIB BitVec ops

---
 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 64174c3b3c34..e018e27672a4 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2383,6 +2383,11 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
     rcases hy with rfl | rfl <;>
       rfl
 
+/-! ### smtUDiv -/
+
+theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0 then allOnes w else x / y := by
+  simp [smtUDiv]
+
 /-! ### sdiv -/
 
 /-- Equation theorem for `sdiv` in terms of `udiv`. -/
@@ -2439,6 +2444,28 @@ theorem sdiv_self {x : BitVec w} :
       rcases x.msb with msb | msb <;> simp
     · rcases x.msb with msb | msb <;> simp [h]
 
+/-! ### smtSDiv -/
+
+theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
+  match x.msb, y.msb with
+  | false, false => smtUDiv x y
+  | false, true  => -(smtUDiv x (-y))
+  | true,  false => -(smtUDiv (-x) y)
+  | true,  true  => smtUDiv (-x) (-y) := by
+  rw [BitVec.smtSDiv]
+  rcases x.msb <;> rcases y.msb <;> simp
+
+/-! ### srem -/
+
+theorem srem_eq (x y : BitVec w) : srem x y =
+  match x.msb, y.msb with
+  | false, false => x % y
+  | false, true  => x % (-y)
+  | true,  false => - ((-x) % y)
+  | true,  true  => -((-x) % (-y)) := by
+  rw [BitVec.srem]
+  rcases x.msb <;> rcases y.msb <;> simp
+
 /-! ### smod -/
 
 /-- Equation theorem for `smod` in terms of `umod`. -/

From f891cf761f2ec25666f1f606f49e84b39f0392a5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 28 Oct 2024 16:58:28 +0100
Subject: [PATCH 2/2] chore: integrate with bv_decide

---
 src/Init/Data/BitVec/Lemmas.lean              |  2 +-
 src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 34 +++++++++++++++++++
 tests/lean/run/bv_arith.lean                  | 12 +++++++
 3 files changed, 47 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index e018e27672a4..1e9d3ca20714 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2385,7 +2385,7 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by
 
 /-! ### smtUDiv -/
 
-theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0 then allOnes w else x / y := by
+theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by
   simp [smtUDiv]
 
 /-! ### sdiv -/
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index 21d2ac3b04e6..2b5d4465a40c 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -84,6 +84,40 @@ theorem BitVec.smod_umod (x y : BitVec w) :
   rw [BitVec.smod_eq]
   cases x.msb <;> cases y.msb <;> simp
 
+attribute [bv_normalize] BitVec.smtUDiv_eq
+
+@[bv_normalize]
+theorem BitVec.smtSDiv_smtUDiv (x y : BitVec w) :
+    x.smtSDiv y =
+      if x.msb then
+        if y.msb then
+          (-x).smtUDiv (-y)
+        else
+          -((-x).smtUDiv y)
+      else
+        if y.msb then
+          -(x.smtUDiv (-y))
+        else
+          x.smtUDiv y := by
+  rw [BitVec.smtSDiv_eq]
+  cases x.msb <;> cases y.msb <;> simp
+
+@[bv_normalize]
+theorem BitVec.srem_umod (x y : BitVec w) :
+    x.srem y =
+      if x.msb then
+        if y.msb then
+          -((-x) % (-y))
+        else
+          -((-x) % y)
+      else
+        if y.msb then
+          x % (-y)
+        else
+          x % y := by
+  rw [BitVec.srem_eq]
+  cases x.msb <;> cases y.msb <;> simp
+
 attribute [bv_normalize] Bool.cond_eq_if
 attribute [bv_normalize] BitVec.abs_eq
 
diff --git a/tests/lean/run/bv_arith.lean b/tests/lean/run/bv_arith.lean
index db01746eaf12..b40fe2360619 100644
--- a/tests/lean/run/bv_arith.lean
+++ b/tests/lean/run/bv_arith.lean
@@ -60,3 +60,15 @@ theorem arith_unit_14 (x y : BitVec 8) (hx : x.msb = true) (hy : y.msb = true) :
 
 theorem arith_unit_15 (x : BitVec 32) : BitVec.sle x (BitVec.abs x) := by
   bv_decide
+
+theorem arith_unit_16 (x y : BitVec 8)  (hy : y ≠ 0) : x.smtUDiv y = x / y := by
+  bv_decide
+
+theorem arith_unit_17 (x y : BitVec 8)  (hy : y = 0) : x.smtUDiv y = -1#8 := by
+  bv_decide
+
+theorem arith_unit_18 (x y : BitVec 8)  (hx : x.msb = true) (h : y.msb = true) : x.smtSDiv y = (-x).smtUDiv (-y) := by
+  bv_decide
+
+theorem arith_unit_19 (x y : BitVec 8)  (hx : x.msb = true) (h : y.msb = true) : x.srem y = -((-x) % (-y)) := by
+  bv_decide