From fe986b4533fbe3a3f26cf257146830e18cc90512 Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Wed, 2 Apr 2025 11:06:33 +0100
Subject: [PATCH] feat: BitVec.add_shiftLeft_eq_or_shiftLeft (#7761)

This PR implements the core theorem for the Bitwuzla rewrites
[NORM_BV_NOT_OR_SHL](https://github.com/bitwuzla/bitwuzla/blob/e09c50818b798f990bd84bf61174553fef46d561/src/rewrite/rewrites_bv.cpp#L1495-L1510)
and
[BV_ADD_SHL](https://github.com/bitwuzla/bitwuzla/blob/e09c50818b798f990bd84bf61174553fef46d561/src/rewrite/rewrites_bv.cpp#L395-L401),
which convert the mixed-boolean-arithmetic expression into a purely
arithmetic expression:

```lean
theorem add_shiftLeft_eq_or_shiftLeft {x y : BitVec w} :
    x + (y <<< x) =  x ||| (y <<< x)
```
---
 src/Init/Data/BitVec/Bitblast.lean | 13 +++++++++++++
 src/Init/Data/BitVec/Lemmas.lean   |  6 ++++++
 2 files changed, 19 insertions(+)

diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 103a6d4af8..107b0d6b54 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -1757,4 +1757,17 @@ theorem append_add_append_eq_append {v w : Nat} {x : BitVec v} {y : BitVec w} :
     (x ++ 0#w) + (0#v ++ y) = x ++ y := by
   rw [add_eq_or_of_and_eq_zero] <;> ext i <;> simp
 
+/-- Heuristically, `y <<< x` is much larger than `x`,
+and hence low bits of `y <<< x`. Thus, `x + (y <<< x) = x ||| (y <<< x).` -/
+theorem add_shifLeft_eq_or_shiftLeft {x y : BitVec w} :
+    x + (y <<< x) =  x ||| (y <<< x) := by
+  rw [add_eq_or_of_and_eq_zero]
+  ext i hi
+  simp only [shiftLeft_eq', getElem_and, getElem_shiftLeft, getElem_zero, and_eq_false_imp,
+    not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, Nat.not_lt]
+  intros hxi hxval
+  have : 2^i ≤ x.toNat := two_pow_le_toNat_of_getElem_eq_true hi hxi
+  have : i < 2^i := by exact Nat.lt_two_pow_self
+  omega
+
 end BitVec
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index d80fc88937..b8f06ce3ea 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -136,6 +136,12 @@ protected theorem toNat_lt_twoPow_of_le (h : m ≤ n) {x : BitVec m} :
 
 theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl
 
+theorem two_pow_le_toNat_of_getElem_eq_true {i : Nat} {x : BitVec w}
+    (hi : i < w) (hx : x[i] = true) : 2^i ≤ x.toNat := by
+  apply Nat.testBit_implies_ge
+  rw [← getElem_eq_testBit_toNat x i hi]
+  exact hx
+
 theorem getMsb'_eq_getLsb' (x : BitVec w) (i : Fin w) :
     x.getMsb' i = x.getLsb' ⟨w - 1 - i, by omega⟩ := by
   simp only [getMsb', getLsb']