From 4ac7ea4aab85cab5627763b0a462b66c04813595 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 2 Mar 2026 17:53:45 +0100
Subject: [PATCH] perf: fixup BitVec.cpop termination proof performance
 (#12764)

---
 src/Init/Data/BitVec/Bitblast.lean                         | 3 +++
 .../Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean      | 7 +++++++
 .../BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean      | 2 +-
 .../Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean    | 6 +++++-
 4 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index fcd41de258..9cc24d2b7b 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -2408,6 +2408,7 @@ def extractAndExtendAux (k len : Nat) (x : BitVec w) (acc : BitVec (k * len)) (h
   | n' + 1 =>
     let acc' := extractAndExtendBit k len x ++ acc
     extractAndExtendAux (k + 1) len x (acc'.cast (by simp [Nat.add_mul]; omega)) (by omega)
+termination_by w - k
 
 /-- We instantiate `extractAndExtendAux` to extend each bit to `len`, extending
   each bit in `x` to have width `w` and returning a `BitVec (w * w)`. -/
@@ -2443,6 +2444,7 @@ def cpopTree (l : BitVec (len * w)) : BitVec w :=
     l.cast (by simp [h])
   else
     cpopTree (cpopLayer l 0#(0 * w) (by omega))
+termination_by len
 
 /--
   Given flattened bitvector `x : BitVec w` and a length `l : Nat`,
@@ -2778,6 +2780,7 @@ private theorem addRecAux_cpopTree {x : BitVec (len * w)} :
       · rfl
       · intros j hj
         simp [extractLsb'_cpopLayer]
+termination_by len
 
 private theorem addRecAux_eq_cpopTree {x : BitVec (len * w)} :
     x.addRecAux len 0#w = (x.cpopTree).cast (by simp) := by
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean
index 54934dae4b..605cf8c815 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean
@@ -95,6 +95,7 @@ where
       have hcast : w * idx = outWidth := by
         simp only [show idx = w by omega, h']
       ⟨aig, hcast ▸ acc⟩
+termination_by w - idx
 
 theorem blastExtractAndExtend.go_le_size (aig : AIG α) (idx : Nat) (x : AIG.RefVec aig w)
     (acc : AIG.RefVec aig (w * idx)) (h : idx ≤ w) (h' : outWidth = w * w) :
@@ -105,6 +106,7 @@ theorem blastExtractAndExtend.go_le_size (aig : AIG α) (idx : Nat) (x : AIG.Ref
   · apply Nat.le_trans ?_ (by apply blastExtractAndExtend.go_le_size)
     apply AIG.LawfulVecOperator.le_size (f := blastExtractAndExtendBit)
   · simp
+termination_by w - idx
 
 theorem blastExtractAndExtend.go_decl_eq (aig : AIG α) (idx' : Nat) (x : AIG.RefVec aig w)
     (acc : AIG.RefVec aig (w * idx')) (h : idx' ≤ w) (h' : outWidth = w * w) :
@@ -121,6 +123,7 @@ theorem blastExtractAndExtend.go_decl_eq (aig : AIG α) (idx' : Nat) (x : AIG.Re
     apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastExtract)
     omega
   · simp [← hres]
+termination_by w - idx'
 
 instance : AIG.LawfulVecOperator α blastExtractAndExtendTarget blastExtractAndExtend where
   le_size := by
@@ -195,6 +198,7 @@ theorem blastCpopLayer.go_le_size (aig : AIG α) (iterNum: Nat) (oldLayer : AIG.
   · simp only [AIG.RefVec.cast_cast]
     <;> (refine Nat.le_trans ?_ (by apply blastCpopLayer.go_le_size); apply AIG.LawfulVecOperator.le_size)
   · simp
+termination_by len - iterNum * 2
 
 theorem blastCpopLayer.go_decl_eq (aig : AIG α) (iterNum: Nat) (oldLayer : AIG.RefVec aig (len * w))
     (newLayer : AIG.RefVec aig (iterNum * w)) (hold : 2 * (iterNum - 1) < len) (hout : outWidth = (len + 1) / 2 * w) :
@@ -212,6 +216,7 @@ theorem blastCpopLayer.go_decl_eq (aig : AIG α) (iterNum: Nat) (oldLayer : AIG.
       · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastAdd)
         assumption
   · simp [← hres]
+termination_by len - iterNum * 2
 
 instance : AIG.LawfulVecOperator α blastCpopLayerTarget blastCpopLayer where
   le_size := by
@@ -257,6 +262,7 @@ theorem blastCpopTree.go_le_size (aig : AIG α) (oldLayer : AIG.RefVec aig (len
   · apply Nat.le_trans _ (by apply blastCpopTree.go_le_size)
     apply blastCpopLayer.go_le_size
   · simp
+termination_by len
 
 theorem blastCpopTree.go_decl_eq (aig : AIG α) (oldLayer : AIG.RefVec aig (len * w))
       (h : 0 < len) :
@@ -273,6 +279,7 @@ theorem blastCpopTree.go_decl_eq (aig : AIG α) (oldLayer : AIG.RefVec aig (len
     · apply Nat.lt_of_lt_of_le h2
       apply blastCpopLayer.go_le_size
   · simp [← hres]
+termination_by len
 
 instance : AIG.LawfulVecOperator α blastCpopTreeTarget blastCpopTree where
   le_size := by
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
index 86b1fe7559..9289e6d209 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -17,7 +17,7 @@ public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
 public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
 public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Reverse
 public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Clz
-import all Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
 
 public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
 import Init.ByCases
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean
index 029f43d3d8..d1812ff626 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean
@@ -124,6 +124,7 @@ theorem denote_blastExtractAndExtend.go (assign : α → Bool) (aig : AIG α) (c
   · have hcurr : currIdx = w := by omega
     subst hcurr
     rw [← hgen, ← hacc idx hidx]
+termination_by w - currIdx
 
 theorem denote_blastExtractAndExtend (assign : α → Bool) (aig : AIG α) (w : Nat) (xc : AIG.RefVec aig w)
     (x : BitVec w)
@@ -212,6 +213,7 @@ theorem denote_blastCpopLayer.go (aig : AIG α) (iterNum : Nat)
   · have h : iterNum = (len + 1) / 2 := by omega
     subst h
     rw [← hgen, hnew]
+termination_by len - iterNum * 2
 
 theorem denote_blastCpopLayer (aig : AIG α)
     (oldLayer : AIG.RefVec aig (len * w))
@@ -277,6 +279,7 @@ theorem denote_blastCpopTree.go (aig : AIG α) (len : Nat)
       · apply eqRec_heq
       · apply proof_irrel_heq
     · omega
+termination_by len
 
 
 theorem denote_blastCpopTree (aig : AIG α) (len : Nat)
@@ -293,7 +296,8 @@ theorem denote_blastCpopTree (aig : AIG α) (len : Nat)
   simp [hpar]
 
 @[simp]
-theorem denote_blastCpop (aig : AIG α) (xc : AIG.RefVec aig w) (x : BitVec w) (assign : α → Bool)
+public theorem denote_blastCpop (aig : AIG α) (xc : AIG.RefVec aig w) (x : BitVec w)
+    (assign : α → Bool)
     (hx : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, xc.get idx hidx, assign⟧ = x.getLsbD idx) :
     ∀ (idx : Nat) (hidx : idx < w),
       ⟦