From 6e75677bb554bae3e9726403d6c1ba5911752896 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Thu, 26 Sep 2024 23:01:55 -0500
Subject: [PATCH] feat: add sdiv_eq, smod_eq to allow sdiv/smod bitblasting in
 terms of udiv/umod

We use the same implementation as Bitwuzla, as evidenced by the following rewrite rules:
- sdiv: https://github.com/bitwuzla/bitwuzla/blob/f229d64be7c4a8c6817332a41d0d2764dbdfbfe4/src/rewrite/rewrites_bv.cpp#L3168C30-L3168C42
- smod: https://github.com/bitwuzla/bitwuzla/blob/f229d64be7c4a8c6817332a41d0d2764dbdfbfe4/src/rewrite/rewrites_bv.cpp#L3282C30-L3282C39
---
 src/Init/Data/BitVec/Lemmas.lean | 35 ++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 61e68c58cbc9..e56c3694d565 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1312,6 +1312,41 @@ theorem umod_eq {x y : BitVec n} :
 theorem toNat_umod {x y : BitVec n} :
     (x.umod y).toNat = x.toNat % y.toNat := rfl
 
+/-! ### sdiv -/
+
+/-- Equation theorem for `sdiv` in terms of `udiv`. -/
+theorem sdiv_eq (x y : BitVec w) : x.sdiv y =
+  match x.msb, y.msb with
+  | false, false => udiv x y
+  | false, true  =>  - (x.udiv (- y))
+  | true,  false => - ((- x).udiv y)
+  | true,  true  => (- x).udiv (- y) := by
+  rw [BitVec.sdiv]
+  rcases x.msb <;> rcases y.msb <;> simp
+
+theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
+  have hx : x = 0#1 \/ x = 1#1 := by bv_omega
+  have hy : y = 0#1 \/ y = 1#1 := by bv_omega
+  rcases hx with rfl | rfl <;>
+    rcases hy with rfl | rfl <;>
+      rfl
+
+/-! ### smod -/
+
+/-- Equation theorem for `smod` in terms of `umod`. -/
+theorem smod_eq (x y : BitVec w) : x.smod y =
+  match x.msb, y.msb with
+  | false, false => x.umod y
+  | false, true =>
+    let u := x.umod (- y)
+    (if u = 0#w then u else u + y)
+  | true, false =>
+    let u := umod (- x) y
+    (if u = 0#w then u else y - u)
+  | true, true => - ((- x).umod (- y)) := by
+  rw [BitVec.smod]
+  rcases x.msb <;> rcases y.msb <;> simp
+
 /-! ### signExtend -/
 
 /-- Equation theorem for `Int.sub` when both arguments are `Int.ofNat` -/