From f673facdbe3818cd65d62d88e6c5cc98c1cbd715 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 21 Mar 2025 10:31:12 +0100
Subject: [PATCH] feat: add BV_EXTRACT_ADD to bv_decide (#7615)

This PR adds the ADD part of bitwuzlas BV_EXTRACT_ADD_MUL rule to
bv_decide's preprocessor.
---
 .../BVDecide/Frontend/Normalize/Simproc.lean  | 22 +++++++++++++++++++
 tests/lean/run/bv_decide_rewriter.lean        |  5 +++++
 2 files changed, 27 insertions(+)

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
index be3864b098..bfd37decc6 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
@@ -457,5 +457,27 @@ builtin_simproc [bv_normalize] bv_extract_concat
     -- extract is not limited to side
     return .continue
 
+builtin_simproc [bv_normalize] extract_add
+    (BitVec.extractLsb' _ _ ((_ : BitVec _) + (_ : BitVec _))) := fun e => do
+  let_expr BitVec.extractLsb' widthExpr startExpr lenExpr targetExpr := e | return .continue
+  let_expr HAdd.hAdd _ _ _ _ lhsExpr rhsExpr := targetExpr | return .continue
+  let some start ← getNatValue? startExpr | return .continue
+  let some len ← getNatValue? lenExpr | return .continue
+  let some width ← getNatValue? widthExpr | return .continue
+  if !(start == 0 && len ≤ width) then return .continue
+
+  let newLhsExpr := mkApp4 (mkConst ``BitVec.extractLsb') widthExpr startExpr lenExpr lhsExpr
+  let newRhsExpr := mkApp4 (mkConst ``BitVec.extractLsb') widthExpr startExpr lenExpr rhsExpr
+  let expr ← mkAdd newLhsExpr newRhsExpr
+  let proof :=
+    mkApp5
+      (mkConst ``BitVec.extractLsb'_add)
+      widthExpr
+      lenExpr
+      lhsExpr
+      rhsExpr
+      (← mkDecideProof (← mkLe lenExpr widthExpr))
+  return .visit { expr := expr, proof? := some proof }
+
 end Frontend.Normalize
 end Lean.Elab.Tactic.BVDecide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 5df1b2643d..2e2756e140 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -623,6 +623,11 @@ example {x : BitVec 16} : (x = BitVec.allOnes 16) → (BitVec.uaddOverflow x x)
 
 example {x : BitVec 64} : (x = BitVec.intMin 64) ↔ (BitVec.negOverflow x) := by bv_decide
 
+-- BV_EXTRACT_ADD_MUL
+example {x y : BitVec 8} :
+    BitVec.extractLsb' 0 4 (x + y) = BitVec.extractLsb' 0 4 x + BitVec.extractLsb' 0 4 y := by
+  bv_normalize
+
 section
 
 namespace NormalizeMul