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.

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

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