From 89bbe804a51ecdbbee4f5f3da2055554fbdc20f6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 18 Dec 2025 09:20:16 +0100
Subject: [PATCH] perf: turn more bv_normalize rules into simprocs (#11717)

This PR improves the performance of `bv_decide`'s rewriter on large
problems.

The baseline for this PR is `QF_BV/sage/app7/bench_1222.smt2` on
`chonk3` at 8 minutes. After this
PR it takes about 1min and 23 seconds. This improvement is achieved by
turning frequently used simp
rules into simprocs in order to avoid spending time performing
unification to see if they are
applicable.
---
 .../BVDecide/Frontend/Normalize/Simproc.lean  | 126 ++++++++++++++++--
 src/Std/Tactic/BVDecide/Normalize/BitVec.lean |  12 --
 .../BVDecide/Normalize/Canonicalize.lean      |   2 -
 3 files changed, 115 insertions(+), 25 deletions(-)

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
index f19d1d44ea..89d30f4c04 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
@@ -46,6 +46,16 @@ private def mkOr (lhs rhs : Expr) (wExpr : Expr) : Expr :=
   let inst := mkApp2 (mkConst ``instHOrOfOrOp [0]) ty (mkApp (mkConst ``BitVec.instOrOp) wExpr)
   mkApp6 (mkConst ``HOr.hOr [0, 0, 0]) ty ty ty inst lhs rhs
 
+private def mkAnd (lhs rhs : Expr) (wExpr : Expr) : Expr :=
+  let ty := mkApp (mkConst ``BitVec) wExpr
+  let inst := mkApp2 (mkConst ``instHAndOfAndOp [0]) ty (mkApp (mkConst ``BitVec.instAndOp) wExpr)
+  mkApp6 (mkConst ``HAnd.hAnd [0, 0, 0]) ty ty ty inst lhs rhs
+
+private def mkXor (lhs rhs : Expr) (wExpr : Expr) : Expr :=
+  let ty := mkApp (mkConst ``BitVec) wExpr
+  let inst := mkApp2 (mkConst ``instHXorOfXorOp [0]) ty (mkApp (mkConst ``BitVec.instXorOp) wExpr)
+  mkApp6 (mkConst ``HXor.hXor [0, 0, 0]) ty ty ty inst lhs rhs
+
 private def mkAdd (lhs rhs : Expr) (wExpr : Expr) : Expr :=
   let ty := mkApp (mkConst ``BitVec) wExpr
   let inst := mkApp2 (mkConst ``instHAdd [0]) ty (mkApp (mkConst ``BitVec.instAdd) wExpr)
@@ -230,23 +240,84 @@ builtin_simproc [bv_normalize] bv_add ((_ : BitVec _) + (_ : BitVec _)) := fun e
     else if let some step ← shiftLeftAdd then return step
     else return .continue
 
-builtin_simproc [bv_normalize] shiftRight_self ((_ : BitVec _) >>> (_ : BitVec _)) := fun e => do
+builtin_simproc [bv_normalize] shiftRight ((_ : BitVec _) >>> (_ : BitVec _)) := fun e => do
   let_expr HShiftRight.hShiftRight ty _ _ _ lhs rhs := e | return .continue
   let_expr BitVec wExpr := ty | return .continue
   let some w ← getNatValue? wExpr | return .continue
-  if lhs != rhs then return .continue
-  let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_self) wExpr lhs
-  return .visit { expr := toExpr 0#w, proof? := some proof }
+  if lhs == rhs then
+    let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_self) wExpr lhs
+    return .visit { expr := toExpr 0#w, proof? := some proof }
+  else
+    let_expr BitVec.ofNat nExpr kExpr := rhs | return .continue
+    let some n ← getNatValue? nExpr | return .continue
+    if w != n then return .continue
+    let some k ← getNatValue? kExpr | return .continue
+    let expr := BitVec.mkNatShiftRight lhs (toExpr (k % 2 ^ w)) wExpr
+    let proof := mkApp3 (mkConst ``BitVec.ushiftRight_ofNat_eq) wExpr lhs kExpr
+    return .visit { expr, proof? := some proof }
 
-builtin_simproc [bv_normalize] extract_full (BitVec.extractLsb' _ _ _) := fun e => do
+builtin_simproc [bv_normalize] extractLsb' (BitVec.extractLsb' _ _ _) := fun e => do
   let_expr BitVec.extractLsb' wExpr startExpr lenExpr targetExpr := e | return .continue
+  match_expr targetExpr with
+  | HAnd.hAnd _ _ _ _ lhs rhs =>
+    let lhs' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr lhs
+    let rhs' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr rhs
+    let expr := BitVec.mkAnd lhs' rhs' lenExpr
+    let proof := mkApp5 (mkConst ``BitVec.extractLsb'_and) wExpr lhs rhs startExpr lenExpr
+    return .visit { expr, proof? := some proof }
+  | HXor.hXor _ _ _ _ lhs rhs =>
+    let lhs' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr lhs
+    let rhs' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr rhs
+    let expr := BitVec.mkXor lhs' rhs' lenExpr
+    let proof := mkApp5 (mkConst ``BitVec.extractLsb'_xor) wExpr lhs rhs startExpr lenExpr
+    return .visit { expr, proof? := some proof }
+  | cond _ discr thenExpr elseExpr =>
+    let thenExpr' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr thenExpr
+    let elseExpr' := mkApp4 (mkConst ``BitVec.extractLsb') wExpr startExpr lenExpr elseExpr
+    let newTy := mkApp (mkConst ``BitVec) lenExpr
+    let expr := mkApp4 (mkConst ``cond [1]) newTy discr thenExpr' elseExpr'
+    let proof :=
+      mkApp6 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.extractLsb'_if)
+        wExpr
+        discr
+        thenExpr
+        elseExpr
+        startExpr
+        lenExpr
+     return .visit { expr, proof? := some proof }
+  | _ =>
+    let some w ← getNatValue? wExpr | return .continue
+    let some start ← getNatValue? startExpr | return .continue
+    let some len ← getNatValue? lenExpr | return .continue
+    if start != 0 then return .continue
+    if len != w then return .continue
+    let proof := mkApp2 (mkConst ``BitVec.extractLsb'_eq_self) wExpr targetExpr
+    return .visit { expr := targetExpr, proof? := some proof }
+
+builtin_simproc [bv_normalize] shiftLeft ((_ : BitVec _) <<< (_ : BitVec _)) := fun e => do
+  let_expr HShiftLeft.hShiftLeft ty _ _ _ lhs rhs := e | return .continue
+  let_expr BitVec wExpr := ty | return .continue
   let some w ← getNatValue? wExpr | return .continue
-  let some start ← getNatValue? startExpr | return .continue
-  let some len ← getNatValue? lenExpr | return .continue
-  if start != 0 then return .continue
-  if len != w then return .continue
-  let proof := mkApp2 (mkConst ``BitVec.extractLsb'_eq_self) wExpr targetExpr
-  return .visit { expr := targetExpr, proof? := some proof }
+  let_expr BitVec.ofNat nExpr kExpr := rhs | return .continue
+  let some n ← getNatValue? nExpr | return .continue
+  if w != n then return .continue
+  let some k ← getNatValue? kExpr | return .continue
+  let expr := BitVec.mkNatShiftLeft lhs (toExpr (k % 2 ^ w)) wExpr
+  let proof := mkApp3 (mkConst ``BitVec.shiftLeft_ofNat_eq) wExpr lhs kExpr
+  return .visit { expr, proof? := some proof }
+
+builtin_simproc [bv_normalize] sshiftRight' (BitVec.sshiftRight' _ _) := fun e => do
+  let_expr BitVec.sshiftRight' nExpr mExpr lhs rhs := e | return .continue
+  let some n ← getNatValue? nExpr | return .continue
+  let some m ← getNatValue? mExpr | return .continue
+  if n != m then return .continue
+  let_expr BitVec.ofNat wExpr kExpr := rhs | return .continue
+  let some w ← getNatValue? wExpr | return .continue
+  if n != w then return .continue
+  let some k ← getNatValue? kExpr | return .continue
+  let expr := mkApp3 (mkConst ``BitVec.sshiftRight) wExpr lhs (toExpr (k % 2 ^ w))
+  let proof := mkApp3 (mkConst ``BitVec.sshiftRight'_ofNat_eq_sshiftRight) wExpr lhs kExpr
+  return .visit { expr, proof? := some proof }
 
 def eqSelfProc : Simp.Simproc := fun e => do
   let_expr Eq ty lhs rhs := e | return .continue
@@ -341,6 +412,39 @@ builtin_simproc [bv_normalize] bool_beq ((_ : Bool) == (_ : Bool)) := fun e => d
     else if let some step ← selfRight then return step
     else return .continue
 
+builtin_simproc [bv_normalize] cast (BitVec.cast _ _) := fun e => do
+  let_expr BitVec.cast nExpr mExpr hExpr targetExpr := e | return .continue
+  let some n ← getNatValue? nExpr | return .continue
+  let some m ← getNatValue? mExpr | return .continue
+  if n != m then return .continue
+  let proof := mkApp3 (mkConst ``BitVec.cast_eq) nExpr hExpr targetExpr
+  return .visit { expr := targetExpr, proof? := some proof }
+
+builtin_simproc [bv_normalize] bool_or_elim ((_ : Bool) || (_ : Bool)) := fun e => do
+  let_expr Bool.or lhs rhs := e | return .continue
+  let newLhs := mkApp (mkConst ``Bool.not) lhs
+  let newRhs := mkApp (mkConst ``Bool.not) rhs
+  let expr := mkApp (mkConst ``Bool.not) (mkApp2 (mkConst ``Bool.and) newLhs newRhs)
+  let proof := mkApp2 (mkConst ``Std.Tactic.BVDecide.Normalize.Bool.or_elim) lhs rhs
+  return .visit { expr, proof? := some proof }
+
+builtin_simproc [bv_normalize] bv_or_elim ((_ : BitVec _) ||| (_ : BitVec _)) := fun e => do
+  let_expr HOr.hOr ty _ _ _ lhs rhs := e | return .continue
+  let_expr BitVec wExpr := ty | return .continue
+  let newLhs := BitVec.mkComplement lhs wExpr
+  let newRhs := BitVec.mkComplement rhs wExpr
+  let expr := BitVec.mkComplement (BitVec.mkAnd newLhs newRhs wExpr) wExpr
+  let proof := mkApp3 (mkConst ``Std.Tactic.BVDecide.Normalize.BitVec.or_elim) wExpr lhs rhs
+  return .visit { expr, proof? := some proof }
+
+builtin_simproc [bv_normalize] bv_sub_elim ((_ : BitVec _) - (_ : BitVec _)) := fun e => do
+  let_expr HSub.hSub ty _ _ _ lhs rhs := e | return .continue
+  let_expr BitVec wExpr := ty | return .continue
+  let newRhs := BitVec.mkNeg rhs wExpr
+  let expr := BitVec.mkAdd lhs newRhs wExpr
+  let proof := mkApp3 (mkConst ``BitVec.sub_eq_add_neg) wExpr lhs rhs
+  return .visit { expr, proof? := some proof }
+
 end SimpleUnifiers
 
 builtin_simproc ↓ [bv_normalize] reduceCond (cond _ _ _) := fun e => do
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index b89880a560..5b48381671 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -24,8 +24,6 @@ namespace Normalize
 
 section Reduce
 
-attribute [bv_normalize] BitVec.sub_eq_add_neg
-
 @[bv_normalize]
 theorem BitVec.le_ult (x y : BitVec w) : (x ≤ y) ↔ ((!y.ult x) = true) := by
   have : x ≤ y ↔ (x.ule y = true) := by
@@ -164,7 +162,6 @@ attribute [bv_normalize] BitVec.not_not
 attribute [bv_normalize] decide_true
 attribute [bv_normalize] decide_false
 attribute [bv_normalize] decide_not
-attribute [bv_normalize] BitVec.cast_eq
 
 end Constant
 
@@ -259,11 +256,6 @@ theorem BitVec.add_const_right' {a : BitVec w} :
 attribute [bv_normalize] BitVec.mul_zero
 attribute [bv_normalize] BitVec.zero_mul
 
-
-attribute [bv_normalize] BitVec.shiftLeft_ofNat_eq
-attribute [bv_normalize] BitVec.ushiftRight_ofNat_eq
-attribute [bv_normalize] BitVec.sshiftRight'_ofNat_eq_sshiftRight
-
 @[bv_normalize]
 theorem BitVec.neg_mul (x y : BitVec w) : (~~~x + 1#w) * y = ~~~(x * y) + 1#w := by
   rw [← BitVec.neg_eq_not_add, ← BitVec.neg_eq_not_add, _root_.BitVec.neg_mul]
@@ -370,10 +362,6 @@ theorem BitVec.udiv_ofNat_eq_of_lt (w : Nat) (x : BitVec w) (n : Nat) (k : Nat)
   have : BitVec.ofNat w n = BitVec.twoPow w k := by simp [bitvec_to_nat, hk]
   rw [this, BitVec.udiv_twoPow_eq_of_lt (hk := by omega)]
 
-attribute [bv_normalize] BitVec.extractLsb'_and
-attribute [bv_normalize] BitVec.extractLsb'_xor
-
-@[bv_normalize]
 theorem BitVec.extractLsb'_if {x y : BitVec w} (s l : Nat) :
     BitVec.extractLsb' s l (bif c then x else y) = bif c then (BitVec.extractLsb' s l x) else (BitVec.extractLsb' s l y) := by
   cases c <;> simp
diff --git a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
index b3d307403b..78ac61c0c1 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
@@ -80,10 +80,8 @@ theorem BitVec.lt_ult (x y : BitVec w) : (x < y) = (BitVec.ult x y = true) := by
   simp only [(· < ·)]
   simp
 
-@[bv_normalize]
 theorem Bool.or_elim : ∀ (a b : Bool), (a || b) = !(!a && !b) := by decide
 
-@[bv_normalize]
 theorem BitVec.or_elim (x y : BitVec w) : x ||| y = ~~~(~~~x &&& ~~~y) := by
   ext
   simp