From 7d651d559ab7a4cf6a12622f14edcd690c44772b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 24 Mar 2025 11:50:42 +0100
Subject: [PATCH] feat: BV_EXTRACT_MUL (#7655)

This PR adds the preprocessing rule for extraction over multiplication
to bv_decide.
---
 .../BVDecide/Frontend/Normalize/Simproc.lean  | 22 +++++++++++++++++++
 tests/lean/run/bv_decide_rewriter.lean        |  4 ++++
 2 files changed, 26 insertions(+)

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
index bfd37decc6..971b34fe75 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
@@ -479,5 +479,27 @@ builtin_simproc [bv_normalize] extract_add
       (← mkDecideProof (← mkLe lenExpr widthExpr))
   return .visit { expr := expr, proof? := some proof }
 
+builtin_simproc [bv_normalize] extract_mul
+    (BitVec.extractLsb' _ _ ((_ : BitVec _) * (_ : BitVec _))) := fun e => do
+  let_expr BitVec.extractLsb' widthExpr startExpr lenExpr targetExpr := e | return .continue
+  let_expr HMul.hMul _ _ _ _ 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 ← mkMul newLhsExpr newRhsExpr
+  let proof :=
+    mkApp5
+      (mkConst ``BitVec.extractLsb'_mul)
+      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 abdbc4588f..95602f8fef 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -633,6 +633,10 @@ example {x y : BitVec 8} :
     BitVec.extractLsb' 0 4 (x + y) = BitVec.extractLsb' 0 4 x + BitVec.extractLsb' 0 4 y := by
   bv_normalize
 
+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