feat: add bitblasting circuit for BitVec.cpop (#12433)

This PR adds a bitblasting circuit for `BitVec.cpop` with a
divide-and-conquer for a parallel-prefix-sum.

This is the [most efficient circuit we could
fine](https://docs.google.com/spreadsheets/d/1dJ5uUY4-eWIQmMjIui3H4U-wBxBxy-qYuqJZFZD1xvA/edit?usp=sharing),
after comparing with Kernighan's algorithm and with the intuitive
addition circuit.

---------

Co-authored-by: Henrik Böving <hargonix@gmail.com>

src/Init/Data/BitVec/Bitblast.lean

@@ -2393,4 +2393,409 @@ theorem fastUmulOverflow (x y : BitVec w) :
         simp [← Nat.pow_add, show w + 1 - (k - 1) + k = w + 1 + 1 by omega] at this
         omega
 
+/-! ### Population Count -/
+
+/-- Extract the `k`-th bit from `x` and extend it to have length `len`. -/
+def extractAndExtendBit (idx len : Nat) (x : BitVec w) : BitVec len :=
+  BitVec.zeroExtend len (BitVec.extractLsb' idx 1 x)
+
+
+/-- Recursively extract one bit at a time and extend it to width `w` -/
+def extractAndExtendAux (k len : Nat) (x : BitVec w) (acc : BitVec (k * len)) (hle : k ≤ w) :
+    BitVec (w * len) :=
+  match hwi : w - k with
+  | 0 => acc.cast (by simp [show w = k by omega])
+  | n' + 1 =>
+    let acc' := extractAndExtendBit k len x ++ acc
+    extractAndExtendAux (k + 1) len x (acc'.cast (by simp [Nat.add_mul]; omega)) (by omega)
+
+/-- We instantiate `extractAndExtendAux` to extend each bit to `len`, extending
+  each bit in `x` to have width `w` and returning a `BitVec (w * w)`. -/
+def extractAndExtend (len : Nat) (x : BitVec w) : BitVec (w * len) :=
+  extractAndExtendAux 0 len x ((0#0).cast (by simp)) (by omega)
+
+/--
+  Construct a layer of the parallel-prefix-sum tree by summing two-by-two all the
+  `w`-long words in `oldLayer`, returning a bitvector containing `(oldLen + 1) / 2`
+  flattened `w`-long words, each resulting from an addition.
+-/
+def cpopLayer (oldLayer : BitVec (len * w)) (newLayer : BitVec (iterNum * w))
+    (hold : 2 * (iterNum - 1) < len) : BitVec (((len + 1)/2) * w) :=
+  if hlen : len - (iterNum * 2) = 0 then
+    have : ((len + 1)/2) = iterNum := by omega
+    newLayer.cast (by simp [this])
+  else
+    let op1 := oldLayer.extractLsb' ((2 * iterNum) * w) w
+    let op2 := oldLayer.extractLsb' ((2 * iterNum + 1) * w) w
+    let newLayer' := (op1 + op2) ++ newLayer
+    have hcast : w + iterNum * w = (iterNum + 1) * w := by simp [Nat.add_mul]; omega
+    cpopLayer oldLayer (newLayer'.cast hcast) (by omega)
+termination_by len - (iterNum * 2)
+
+/--
+  Given a `BitVec (len * w)` of `len` flattened `w`-long words,
+  construct a binary tree that sums two-by-two the `w`-long words in the previous layer,
+  ultimately returning a single `w`-long words corresponding to the whole addition.
+-/
+def cpopTree (l : BitVec (len * w)) : BitVec w :=
+  if h : len = 0 then 0#w
+  else if h : len = 1 then
+    l.cast (by simp [h])
+  else
+    cpopTree (cpopLayer l 0#(0 * w) (by omega))
+
+/--
+  Given flattened bitvector `x : BitVec w` and a length `l : Nat`,
+  construct a parallel prefix sum circuit adding each available `l`-long word in `x`.
+-/
+def cpopRec (x : BitVec w) : BitVec w :=
+  if hw : 1 < w then
+    let extendedBits := x.extractAndExtend w
+    (cpopTree extendedBits).cast (by simp)
+  else if hw' : 0 < w then
+    x
+  else
+    0#w
+
+/-- Recursive addition of the elements in a flattened bitvec, starting from the `rem`-th element. -/
+private def addRecAux (x : BitVec (l * w)) (rem : Nat) (acc : BitVec w) : BitVec w :=
+  match rem with
+  | 0 => acc
+  | n + 1 => x.addRecAux n (acc + x.extractLsb' (n * w) w)
+
+/-- Recursive addition of the elements in a flattened bitvec. -/
+private def addRec (x : BitVec (l * w)) : BitVec w := addRecAux x l 0#w
+
+theorem getLsbD_extractAndExtendBit {x : BitVec w} :
+    (extractAndExtendBit k len x).getLsbD i =
+    (decide (i = 0) && decide (0 < len) && x.getLsbD k) := by
+  simp only [extractAndExtendBit, truncate_eq_setWidth, getLsbD_setWidth, getLsbD_extractLsb',
+    Nat.lt_one_iff]
+  by_cases hi : i = 0
+  <;> simp [hi]
+
+@[simp]
+private theorem extractAndExtendAux_zero {k len : Nat} {x : BitVec w}
+    {acc : BitVec (k * len)} (heq : w = k) :
+    extractAndExtendAux k len x acc (by omega) = acc.cast (by simp [heq]) := by
+  unfold extractAndExtendAux
+  split
+  · simp
+  · omega
+
+private theorem extractLsb'_extractAndExtendAux {k len : Nat} {x : BitVec w}
+    (acc : BitVec (k * len)) (hle : k ≤ w) :
+    (∀ i (_ : i < k), acc.extractLsb' (i * len) len = (x.extractLsb' i 1).setWidth len) →
+    (extractAndExtendAux k len x acc (by omega)).extractLsb' (i * len) len =
+    (x.extractLsb' i 1).setWidth len := by
+  intros hacc
+  induction hwi : w - k generalizing acc k
+  · case zero =>
+    rw [extractAndExtendAux_zero (by omega)]
+    by_cases hj : i < k
+    · apply hacc
+      exact hj
+    · ext l hl
+      have := mul_le_mul_right (n := k) (m := i) len (by omega)
+      simp [← getLsbD_eq_getElem, getLsbD_extractLsb', hl, getLsbD_setWidth,
+        show w ≤ i + l by omega, getLsbD_of_ge acc (i * len + l) (by omega)]
+  · case succ n' ihn' =>
+    rw [extractAndExtendAux]
+    split
+    · omega
+    · apply ihn'
+      · intros i hi
+        have hcast : len + k * len = (k + 1) * len := by
+            simp [Nat.mul_comm, Nat.mul_add, Nat.add_comm]
+
+        by_cases hi' : i < k
+        · have heq : extractLsb' (i * len) len (BitVec.cast hcast (extractAndExtendBit k len x ++ acc))  =
+              extractLsb' (i * len) len ((extractAndExtendBit k len x ++ acc)) := by
+            ext; simp
+          rw [heq, extractLsb'_append_of_lt hi']
+          apply hacc
+          exact hi'
+        · have heq : extractLsb' (i * len) len (BitVec.cast hcast (extractAndExtendBit k len x ++ acc))   =
+              extractLsb' (i * len) len ((extractAndExtendBit k len x ++ acc)) := by
+            ext; simp
+          rw [heq, extractLsb'_append_of_eq (by omega)]
+          simp [show i = k by omega, extractAndExtendBit]
+      · omega
+
+theorem extractLsb'_cpopLayer {w iterNum i oldLen : Nat} {oldLayer : BitVec (oldLen * w)}
+    {newLayer : BitVec (iterNum * w)} (hold : 2 * (iterNum - 1) < oldLen) :
+    (∀ i (_hi: i < iterNum),
+      newLayer.extractLsb' (i * w) w =
+      oldLayer.extractLsb' ((2 * i) * w) w + (oldLayer.extractLsb' ((2 * i + 1) * w) w)) →
+    extractLsb' (i * w) w (oldLayer.cpopLayer newLayer hold) =
+      extractLsb' (2 * i * w) w oldLayer + extractLsb' ((2 * i + 1) * w) w oldLayer := by
+  intro proof_addition
+  rw [cpopLayer]
+  split
+  · by_cases hi : i < iterNum
+    · simp only [extractLsb'_cast]
+      apply proof_addition
+      exact hi
+    · ext j hj
+      have : iterNum * w ≤ i * w := by refine mul_le_mul_right w (by omega)
+      have : oldLen * w ≤ (2 * i) * w := by refine mul_le_mul_right w (by omega)
+      have : oldLen * w ≤ (2 * i + 1) * w := by refine mul_le_mul_right w (by omega)
+      have hz : extractLsb' (2 * i * w) w oldLayer = 0#w := by
+        ext j hj
+        simp [show oldLen * w ≤ 2 * i * w + j by omega]
+      have hz' : extractLsb' ((2 * i + 1) * w) w oldLayer = 0#w := by
+        ext j hj
+        simp [show oldLen * w ≤ (2 * i + 1) * w + j by omega]
+      simp [show iterNum * w ≤ i * w + j by omega, hz, hz']
+  · generalize hop1 : oldLayer.extractLsb' ((2 * iterNum) * w) w = op1
+    generalize hop2 : oldLayer.extractLsb' ((2 * iterNum + 1) * w) w = op2
+    have hcast : w + iterNum * w = (iterNum + 1) * w := by simp [Nat.add_mul]; omega
+    apply extractLsb'_cpopLayer
+    intros i hi
+    by_cases hlt : i < iterNum
+    · rw [extractLsb'_cast, extractLsb'_append_eq_of_add_le]
+      · apply proof_addition
+        exact hlt
+      · rw [show i * w + w = i * w + 1 * w by omega, ← Nat.add_mul]
+        exact mul_le_mul_right w hlt
+    · rw [extractLsb'_cast, show i = iterNum by omega, extractLsb'_append_eq_left, hop1, hop2]
+termination_by oldLen - 2 * (iterNum + 1 - 1)
+
+theorem getLsbD_cpopLayer {w iterNum: Nat} {oldLayer : BitVec (oldLen * w)}
+    {newLayer : BitVec (iterNum * w)} (hold : 2 * (iterNum - 1) < oldLen) :
+    (∀ i (_hi: i < iterNum),
+          newLayer.extractLsb' (i * w) w =
+          oldLayer.extractLsb' ((2 * i) * w) w + (oldLayer.extractLsb' ((2 * i + 1) * w) w)) →
+    (oldLayer.cpopLayer newLayer hold).getLsbD k =
+      (extractLsb' (2 * ((k - k % w) / w) * w) w oldLayer +
+        extractLsb' ((2 * ((k - k % w) / w) + 1) * w) w oldLayer).getLsbD (k % w) := by
+  intro proof_addition
+  by_cases hw0 : w = 0
+  · subst hw0
+    simp
+  · simp only [← extractLsb'_cpopLayer (hold := by omega) proof_addition,
+      Nat.mod_lt (x := k) (y := w) (by omega), getLsbD_eq_getElem, getElem_extractLsb']
+    congr
+    by_cases hmod : k % w = 0
+    · rw [hmod, Nat.sub_zero, Nat.add_zero, Nat.div_mul_cancel (by omega)]
+    · rw [Nat.div_mul_cancel (by exact dvd_sub_mod k), Nat.sub_add_cancel (by exact mod_le k w)]
+
+@[simp]
+private theorem addRecAux_zero {x : BitVec (l * w)} {acc : BitVec w} :
+    x.addRecAux 0 acc = acc := rfl
+
+@[simp]
+private theorem addRecAux_succ {x : BitVec (l * w)} {n : Nat} {acc : BitVec w} :
+    x.addRecAux (n + 1) acc = x.addRecAux n (acc + extractLsb' (n * w) w x) := rfl
+
+private theorem addRecAux_eq {x : BitVec (l * w)} {n : Nat} {acc : BitVec w} :
+     x.addRecAux n acc = x.addRecAux n 0#w + acc := by
+  induction n generalizing acc
+  · case zero =>
+    simp
+  · case succ n ihn =>
+    simp only [addRecAux_succ, BitVec.zero_add, ihn (acc := extractLsb' (n * w) w x),
+      BitVec.add_assoc, ihn (acc := acc + extractLsb' (n * w) w x), BitVec.add_right_inj]
+    rw [BitVec.add_comm (x := acc)]
+
+private theorem extractLsb'_addRecAux_of_le {x : BitVec (len * w)} (h : r ≤ k):
+    (extractLsb' 0 (k * w) x).addRecAux r 0#w = x.addRecAux r 0#w := by
+  induction r generalizing x len k
+  · case zero =>
+    simp [addRecAux]
+  · case succ diff ihdiff =>
+    simp only [addRecAux_succ, BitVec.zero_add]
+    have hext : diff * w + w ≤ k * w := by
+      simp only [show diff * w + w = (diff + 1) * w by simp [Nat.add_mul]]
+      exact Nat.mul_le_mul_right w h
+    rw [extractLsb'_extractLsb'_of_le hext, addRecAux_eq (x := x),
+        addRecAux_eq (x := extractLsb' 0 (k * w) x), ihdiff (x := x) (by omega) (k := k)]
+
+private theorem extractLsb'_extractAndExtend_eq {i len : Nat} {x : BitVec w} :
+    (extractAndExtend len x).extractLsb' (i * len) len = extractAndExtendBit i len x := by
+  unfold extractAndExtend
+  by_cases hilt : i < w
+  · ext j hj
+    simp [extractLsb'_extractAndExtendAux, extractAndExtendBit]
+  · ext k hk
+    have := Nat.mul_le_mul_right (n := w) (k := len) (m := i) (by omega)
+    simp only [extractAndExtendBit, cast_ofNat, getElem_extractLsb', truncate_eq_setWidth,
+      getElem_setWidth, getLsbD_extractLsb', Nat.lt_one_iff]
+    rw [getLsbD_of_ge, getLsbD_of_ge]
+    · simp
+    · omega
+    · omega
+
+private theorem addRecAux_append_extractLsb' {x : BitVec (len * w)} (ha : 0 < len) :
+    ((x.extractLsb' ((len - 1) * w) w ++
+      x.extractLsb' 0 ((len - 1) * w)).cast (m := len * w) hcast).addRecAux len 0#w =
+    x.extractLsb' ((len - 1) * w) w +
+      (x.extractLsb' 0 ((len - 1) * w)).addRecAux (len - 1) 0#w := by
+  simp only [extractLsb'_addRecAux_of_le (k := len - 1) (r := len - 1) (by omega),
+    BitVec.append_extractLsb'_of_lt (hcast := hcast)]
+  have hsucc := addRecAux_succ (x := x) (acc := 0#w) (n := len - 1)
+  rw [BitVec.zero_add, Nat.sub_one_add_one (by omega)] at hsucc
+  rw [hsucc, addRecAux_eq, BitVec.add_comm]
+
+private theorem Nat.mul_add_le_mul_of_succ_le {a b c : Nat} (h : a + 1 ≤ c) :
+    a * b + b ≤ c * b := by
+  rw [← Nat.succ_mul]
+  exact mul_le_mul_right b h
+
+/--
+  The recursive addition of `w`-long words on two flattened bitvectors `x` and `y` (with different
+  number of words `len` and `len'`, respectively) returns the same value, if we can prove
+  that each `w`-long word in `x` results from the addition of two `w`-long words in `y`,
+  using exactly all `w`-long words in `y`.
+-/
+private theorem addRecAux_eq_of {x : BitVec (len * w)} {y : BitVec (len' * w)}
+    (hlen : len = (len' + 1) / 2) :
+    (∀ (i : Nat) (_h : i < (len' + 1) / 2),
+      extractLsb' (i * w) w x = extractLsb' (2 * i * w) w y + extractLsb' ((2 * i + 1) * w) w y) →
+    x.addRecAux len 0#w = y.addRecAux len' 0#w := by
+  intro hadd
+  induction len generalizing len' y
+  · case zero =>
+    simp [show len' = 0 by omega]
+  · case succ len ih =>
+    have hcast : w + (len + 1 - 1) * w = (len + 1) * w := by
+      simp [Nat.add_mul, Nat.add_comm]
+    have hcast' :  w + (len' - 1) * w = len' * w := by
+      rw [Nat.sub_mul, Nat.one_mul,
+        ← Nat.add_sub_assoc (by refine Nat.le_mul_of_pos_left w (by omega)), Nat.add_comm]
+      simp
+    rw [addRecAux_succ, ← BitVec.append_extractLsb'_of_lt (x := x) (hcast := hcast)]
+    have happ := addRecAux_append_extractLsb' (len := len + 1) (x := x) (hcast := hcast) (by omega)
+    simp only [Nat.add_one_sub_one, addRecAux_succ, BitVec.zero_add] at happ
+    simp only [Nat.add_one_sub_one, BitVec.zero_add, happ]
+    have := Nat.succ_mul (n := len' - 1) (m := w)
+    rw [succ_eq_add_one, Nat.sub_one_add_one (by omega)] at this
+    by_cases hmod : len' % 2 = 0
+    · /- `sum` results from the addition of the two last elements in `y`, `sum = op1 + op2` -/
+      have := Nat.mul_le_mul_right (n := len' - 1 - 1) (m := len' - 1) (k := w) (by omega)
+      have := Nat.succ_mul (n := len' - 1 - 1) (m := w)
+      have hcast'' :  w + (len' - 1 - 1) * w = (len' - 1) * w := by
+        rw [Nat.sub_mul, Nat.one_mul,
+          ← Nat.add_sub_assoc (k := w) (by refine Nat.le_mul_of_pos_left w (by omega))]
+        simp
+      rw [succ_eq_add_one, Nat.sub_one_add_one (by omega)] at this
+      rw [← BitVec.append_extractLsb'_of_lt (x := y) (hcast := hcast'),
+        addRecAux_append_extractLsb' (by omega),
+        ← BitVec.append_extractLsb'_of_lt (x := extractLsb' 0 ((len' - 1) * w) y) (hcast := hcast''),
+        addRecAux_append_extractLsb' (by omega),
+        extractLsb'_extractLsb'_of_le (by exact Nat.mul_add_le_mul_of_succ_le (by omega)),
+        extractLsb'_extractLsb'_of_le (by omega), ← BitVec.add_assoc, hadd (_h := by omega)]
+      congr 1
+      · rw [show len = (len' + 1) / 2 - 1 by omega, BitVec.add_comm]
+        congr <;> omega
+      · apply ih
+        · omega
+        · intros
+          rw [extractLsb'_extractLsb'_of_le (by exact Nat.mul_add_le_mul_of_succ_le (by omega)),
+            extractLsb'_extractLsb'_of_le (by exact Nat.mul_add_le_mul_of_succ_le (by omega)),
+            extractLsb'_extractLsb'_of_le (by exact Nat.mul_add_le_mul_of_succ_le (by omega)),
+            hadd (_h := by omega)]
+    · /- `sum` results from the addition of the last elements in `y` with `0#w` -/
+      have : len' * w ≤ (len' - 1 + 1) * w := by exact mul_le_mul_right w (by omega)
+      rw [← BitVec.append_extractLsb'_of_lt (x := y) (hcast := hcast'),
+        addRecAux_append_extractLsb' (by omega), hadd (_h := by omega),
+        show 2 * len = len' - 1 by omega]
+      congr 1
+      · rw [BitVec.add_right_eq_self]
+        ext k hk
+        simp only [getElem_extractLsb', getElem_zero]
+        apply getLsbD_of_ge y ((len' - 1 + 1) * w + k) (by omega)
+      · apply ih
+        · omega
+        · intros
+          rw [extractLsb'_extractLsb'_of_le (by exact Nat.mul_add_le_mul_of_succ_le (by omega)),
+            extractLsb'_extractLsb'_of_le (by exact Nat.mul_add_le_mul_of_succ_le (by omega)),
+            extractLsb'_extractLsb'_of_le (by exact Nat.mul_add_le_mul_of_succ_le (by omega)),
+            hadd (_h := by omega)]
+
+private theorem getLsbD_extractAndExtend_of_lt {x : BitVec w} (hk : k < v) :
+    (x.extractAndExtend v).getLsbD (pos * v + k) = (extractAndExtendBit pos v x).getLsbD k := by
+  simp [← extractLsb'_extractAndExtend_eq (w := w) (len := v) (i := pos) (x := x)]
+  omega
+
+/--
+  Extracting a bit from a `BitVec.extractAndExtend` is the same as extracting a bit
+  from a zero-extended bit at a certain position in the original bitvector.
+-/
+theorem getLsbD_extractAndExtend {x : BitVec w} (hv : 0 < v) :
+    (BitVec.extractAndExtend v x).getLsbD k =
+    (BitVec.extractAndExtendBit ((k - (k % v)) / v) v x).getLsbD (k % v):= by
+  rw [← getLsbD_extractAndExtend_of_lt (by exact mod_lt k hv)]
+  congr
+  by_cases hmod : k % v = 0
+  · simp only [hmod, Nat.sub_zero, Nat.add_zero]
+    rw [Nat.div_mul_cancel (by omega)]
+  · rw [← Nat.div_eq_sub_mod_div]
+    exact Eq.symm (div_add_mod' k v)
+
+private theorem addRecAux_extractAndExtend_eq_cpopNatRec {x : BitVec w} :
+    (extractAndExtend w x).addRecAux n 0#w = x.cpopNatRec n 0 := by
+  induction n
+  · case zero =>
+    simp
+  · case succ n' ihn' =>
+    rw [cpopNatRec_succ, Nat.zero_add, natCast_eq_ofNat, addRecAux_succ, BitVec.zero_add,
+      addRecAux_eq, cpopNatRec_eq, ihn', ofNat_add, natCast_eq_ofNat, BitVec.add_right_inj,
+      extractLsb'_extractAndExtend_eq]
+    ext k hk
+    simp only [extractAndExtendBit, ← getLsbD_eq_getElem, getLsbD_ofNat, hk, decide_true,
+      Bool.true_and, truncate_eq_setWidth, getLsbD_setWidth, getLsbD_extractLsb', Nat.lt_one_iff]
+    by_cases hk0 : k = 0
+    · simp only [hk0, testBit_zero, decide_true, Nat.add_zero, Bool.true_and]
+      cases x.getLsbD n' <;> simp
+    · simp only [show ¬k = 0 by omega, decide_false, Bool.false_and]
+      symm
+      apply testBit_lt_two_pow ?_
+      have : (x.getLsbD n').toNat ≤ 1 := by
+        cases x.getLsbD n' <;> simp
+      have : 1 < 2 ^ k := by exact Nat.one_lt_two_pow hk0
+      omega
+
+private theorem addRecAux_extractAndExtend_eq_cpop {x : BitVec w} :
+    (extractAndExtend w x).addRecAux w 0#w = x.cpop := by
+  simp only [cpop]
+  apply addRecAux_extractAndExtend_eq_cpopNatRec
+
+private theorem addRecAux_cpopTree {x : BitVec (len * w)} :
+    addRecAux ((cpopTree x).cast (m := 1 * w) (by simp)) 1 0#w = addRecAux x len 0#w := by
+  unfold cpopTree
+  split
+  · case _ h =>
+    subst h
+    simp [addRecAux]
+  · case _ h =>
+    split
+    · case _ h' =>
+      simp only [addRecAux_succ, Nat.zero_mul, BitVec.zero_add, addRecAux_zero, h']
+      ext; simp
+    · rw [addRecAux_cpopTree]
+      apply BitVec.addRecAux_eq_of (x := cpopLayer x 0#(0 * w) (by omega)) (y := x)
+      · rfl
+      · intros j hj
+        simp [extractLsb'_cpopLayer]
+
+private theorem addRecAux_eq_cpopTree {x : BitVec (len * w)} :
+    x.addRecAux len 0#w = (x.cpopTree).cast (by simp) := by
+  rw [← addRecAux_cpopTree, addRecAux_succ, Nat.zero_mul, BitVec.zero_add, addRecAux_zero]
+  ext k hk
+  simp [← getLsbD_eq_getElem, hk]
+
+theorem cpop_eq_cpopRec {x : BitVec w} :
+    BitVec.cpop x = BitVec.cpopRec x := by
+  unfold BitVec.cpopRec
+  split
+  · simp [← addRecAux_extractAndExtend_eq_cpop, addRecAux_eq_cpopTree (x := extractAndExtend w x)]
+  · split
+    · ext k hk
+      cases hx : x.getLsbD 0
+      <;> simp [hx, cpop, ← getLsbD_eq_getElem, show k = 0 by omega, show w = 1 by omega]
+    · have hw : w = 0 := by omega
+      subst hw
+      simp [of_length_zero]
+
 end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -2786,6 +2786,14 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   rw [getElem_append] -- Why does this not work with `simp [getElem_append]`?
   simp
 
+theorem append_of_zero_width (x : BitVec w) (y : BitVec v) (h : w = 0) :
+    (x ++ y) = y.cast (by simp [h]) := by
+  ext i ih
+  subst h
+  simp [← getLsbD_eq_getElem, getLsbD_append]
+  omega
+
+set_option backward.isDefEq.respectTransparency false in
 @[grind =]
 theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ y).toInt = if n == 0 then y.toInt else (2 ^ m) * x.toInt + y.toNat := by
@@ -3012,6 +3020,34 @@ theorem extractLsb'_append_extractLsb'_eq_extractLsb' {x : BitVec w} (h : start
   congr 1
   omega
 
+theorem append_extractLsb'_of_lt {x : BitVec (x_len * w)} :
+    (x.extractLsb' ((x_len - 1) * w) w ++ x.extractLsb' 0 ((x_len - 1) * w)).cast hcast = x := by
+  ext i hi
+  simp only [getElem_cast, getElem_append, getElem_extractLsb', Nat.zero_add, dite_eq_ite]
+  rw [← getLsbD_eq_getElem, ite_eq_left_iff, Nat.not_lt]
+  intros
+  simp only [show (x_len - 1) * w + (i - (x_len - 1) * w) = i by omega]
+
+
+theorem extractLsb'_append_of_lt {x : BitVec (k * w)} {y : BitVec w} (hlt : i < k) :
+    extractLsb' (i * w) w (y ++ x) = extractLsb' (i * w) w x := by
+  ext j hj
+  simp only [← getLsbD_eq_getElem, getLsbD_extractLsb', hj, decide_true, getLsbD_append,
+    Bool.true_and, ite_eq_left_iff, Nat.not_lt]
+  intros h
+  by_cases hw0 : w = 0
+  · subst hw0
+    simp
+  · have : i * w ≤ (k - 1) * w := Nat.mul_le_mul_right w (by omega)
+    have h' : i * w + j < (k - 1 + 1) * w := by simp [Nat.add_mul]; omega
+    rw [Nat.sub_one_add_one (by omega)] at h'
+    omega
+
+theorem extractLsb'_append_of_eq {x : BitVec (k * w)} {y : BitVec w} (heq : i = k) :
+    extractLsb' (i * w) w (y ++ x) = y := by
+  ext j hj
+  simp [← getLsbD_eq_getElem, getLsbD_append, hj, heq]
+
 /-- Combine adjacent `~~~ (extractLsb _)'` operations into a single `~~~ (extractLsb _)'`. -/
 theorem not_extractLsb'_append_not_extractLsb'_eq_not_extractLsb' {x : BitVec w} (h : start₂ = start₁ + len₁) :
     (~~~ (x.extractLsb' start₂ len₂) ++ ~~~ (x.extractLsb' start₁ len₁)) =

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -44,6 +44,7 @@ instance : ToExpr BVUnOp where
     | .arithShiftRightConst n => mkApp (mkConst ``BVUnOp.arithShiftRightConst) (toExpr n)
     | .reverse => mkConst ``BVUnOp.reverse
     | .clz => mkConst ``BVUnOp.clz
+    | .cpop => mkConst ``BVUnOp.cpop
   toTypeExpr := mkConst ``BVUnOp
 
 instance : ToExpr (BVExpr w) where

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean

@@ -192,6 +192,8 @@ where
       unaryReflection innerExpr .reverse ``Std.Tactic.BVDecide.Reflect.BitVec.reverse_congr origExpr
     | BitVec.clz _ innerExpr =>
       unaryReflection innerExpr .clz ``Std.Tactic.BVDecide.Reflect.BitVec.clz_congr origExpr
+    | BitVec.cpop _ innerExpr =>
+      unaryReflection innerExpr .cpop ``Std.Tactic.BVDecide.Reflect.BitVec.cpop_congr origExpr
     | _ => return none
 
   /--

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -166,6 +166,8 @@ builtin_dsimproc [simp, seval] reduceGetLsb (getLsbD _ _) := reduceGetBit ``getL
 builtin_dsimproc [simp, seval] reduceGetMsb (getMsbD _ _) := reduceGetBit ``getMsbD getMsbD
 /-- Simplification procedure for `clz` (count leading zeros) on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceClz (clz _) := reduceUnary ``BitVec.clz 2 BitVec.clz
+/-- Simplification procedure for `cpop` (population count) on `BitVec`. -/
+builtin_dsimproc [simp, seval] reduceCpop (cpop _) := reduceUnary ``BitVec.cpop 2 BitVec.cpop
 
 /-- Simplification procedure for `getElem`  on `BitVec`. -/
 builtin_dsimproc [simp, seval] reduceGetElem ((_ : BitVec _)[_]) := fun e => do

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean

@@ -149,6 +149,10 @@ inductive BVUnOp where
   Count leading zeros.
   -/
   | clz
+  /--
+  Population count.
+  -/
+  | cpop
   deriving Hashable, DecidableEq
 
 namespace BVUnOp
@@ -160,6 +164,7 @@ def toString : BVUnOp → String
   | arithShiftRightConst n => s!">>a {n}"
   | reverse => "rev"
   | clz => "clz"
+  | cpop => "cpop"
 
 instance : ToString BVUnOp := ⟨toString⟩
 
@@ -173,6 +178,7 @@ def eval : BVUnOp → (BitVec w → BitVec w)
   | arithShiftRightConst n => (BitVec.sshiftRight · n)
   | reverse =>  BitVec.reverse
   | clz => BitVec.clz
+  | cpop => BitVec.cpop
 
 @[simp] theorem eval_not : eval .not = ((~~~ ·) : BitVec w → BitVec w) := by rfl
 
@@ -192,6 +198,8 @@ theorem eval_arithShiftRightConst : eval (arithShiftRightConst n) = (BitVec.sshi
 
 @[simp] theorem eval_clz : eval .clz = (BitVec.clz : BitVec w → BitVec w) := by rfl
 
+@[simp] theorem eval_cpop : eval .cpop = (BitVec.cpop : BitVec w → BitVec w) := by rfl
+
 end BVUnOp
 
 /--

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean

@@ -17,6 +17,7 @@ public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
 public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
 public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse
 public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Clz
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
 import Init.Data.Nat.Linear
 import Init.Omega
 
@@ -232,6 +233,12 @@ where
           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastClz)
           omega
         ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastClz) ..)⟩
+      | .cpop =>
+        let res := bitblast.blastCpop eaig evec
+        have := by
+          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastCpop)
+          omega
+        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastCpop) ..)⟩
     | .append lhs rhs h =>
       let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache
       let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache
@@ -343,7 +350,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
         · apply Nat.le_trans <;> assumption
   next op expr =>
     match op with
-    | .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. | .reverse | .clz =>
+    | .not | .rotateLeft .. | .rotateRight .. | .arithShiftRightConst .. | .reverse | .clz | .cpop =>
       rw [AIG.LawfulVecOperator.decl_eq]
       rw [goCache_decl_eq]
       have := (goCache aig expr cache).result.property

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Cpop.lean

@@ -0,0 +1,344 @@
+/-
+Copyright (c) 2026 University of Cambridge. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Luisa Cicolini, Siddharth Bhat, Henrik Böving
+-/
+module
+
+prelude
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sub
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ZeroExtend
+public import Std.Sat.AIG.If
+
+import Init.Omega
+
+@[expose] public section
+
+/-!
+This module contains the implementation of a bitblaster for `BitVec.cpop`.
+-/
+
+namespace Std.Tactic.BVDecide
+
+open Std.Sat
+
+variable [Hashable α] [DecidableEq α]
+
+namespace BVExpr
+namespace bitblast
+
+structure ExtractAndExtendBitTarget (aig : AIG α) (w : Nat) where
+  start : Nat
+  x : AIG.RefVec aig w
+
+/-- Extract a single bit in position `start` in `target` and extend it to have width `w`-/
+def blastExtractAndExtendBit (aig : AIG α) (target : ExtractAndExtendBitTarget aig w) :
+    AIG.RefVecEntry α w :=
+  -- extract 1 bit starting from start
+  let ⟨start, x⟩ := target
+  let res := blastExtract aig ⟨x, start⟩
+  let aig := res.aig
+  let extract := res.vec
+  -- zero-extend the extracted portion to have
+  let res := blastZeroExtend aig (newWidth := w) ⟨1, extract⟩
+  let aig := res.aig
+  let extend := res.vec
+  ⟨aig, extend⟩
+
+instance : AIG.LawfulVecOperator α ExtractAndExtendBitTarget blastExtractAndExtendBit where
+  le_size := by
+    intros
+    unfold blastExtractAndExtendBit
+    dsimp only
+    apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastZeroExtend)
+    apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastExtract)
+    omega
+  decl_eq := by
+    intros
+    unfold blastExtractAndExtendBit
+    dsimp only
+    rw [AIG.LawfulVecOperator.decl_eq (f := blastZeroExtend),
+      AIG.LawfulVecOperator.decl_eq (f := blastExtract)]
+    apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+    omega
+
+structure blastExtractAndExtendTarget (aig : AIG α) (outWidth : Nat) where
+  {w : Nat}
+  x : AIG.RefVec aig w
+  h : outWidth = w * w
+
+/-- Extract one bit at a time from the initial vector, zero-extend it to width `w`,
+  and append it the result to `acc`, which eventually will have size `outWidth = w * w`-/
+def blastExtractAndExtend (aig : AIG α) (target : blastExtractAndExtendTarget aig outWidth) :
+    AIG.RefVecEntry α outWidth :=
+  let ⟨x, h⟩ := target
+  let initAcc := blastConst (aig := aig) (w := 0) (val := 0)
+  go 0 x initAcc (by omega) h
+where
+  go {aig : AIG α} {w : Nat} (idx : Nat) (x : AIG.RefVec aig w) (acc : AIG.RefVec aig (w * idx))
+      (h : idx ≤ w) (h' : outWidth = w * w) :=
+    if hidx : idx < w then
+      let res := blastExtractAndExtendBit aig ⟨idx, x⟩
+      have := AIG.LawfulVecOperator.le_size (f := blastExtractAndExtendBit) ..
+      let aig := res.aig
+      let bv := res.vec
+      let acc := acc.cast this
+      let x := x.cast this
+      let acc := acc.append bv
+      have hcast : w * (idx + 1) = w * idx + w := by simp [Nat.mul_add]
+      have acc := hcast ▸ acc
+      go (idx + 1) (x := x) (acc := acc) (by omega) h'
+    else
+      have hcast : w * idx = outWidth := by
+        simp only [show idx = w by omega, h']
+      ⟨aig, hcast ▸ acc⟩
+
+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) :
+    aig.decls.size ≤ (go idx x acc h h').aig.decls.size := by
+  unfold go
+  dsimp only
+  split
+  · apply Nat.le_trans ?_ (by apply blastExtractAndExtend.go_le_size)
+    apply AIG.LawfulVecOperator.le_size (f := blastExtractAndExtendBit)
+  · simp
+
+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) :
+    ∀ (idx : Nat) (h1) (h2),
+      (go idx' x acc h h').aig.decls[idx]'h2 = aig.decls[idx]'h1 := by
+  generalize hres : go idx' x acc h h' = res
+  unfold go at hres
+  dsimp only at hres
+  split at hres
+  · rw [← hres]
+    intros
+    rw [blastExtractAndExtend.go_decl_eq, AIG.LawfulVecOperator.decl_eq (f := blastExtractAndExtendBit)]
+    apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastZeroExtend)
+    apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastExtract)
+    omega
+  · simp [← hres]
+
+instance : AIG.LawfulVecOperator α blastExtractAndExtendTarget blastExtractAndExtend where
+  le_size := by
+    intros
+    unfold blastExtractAndExtend
+    dsimp only
+    apply blastExtractAndExtend.go_le_size
+  decl_eq := by
+    intros
+    unfold blastExtractAndExtend
+    apply blastExtractAndExtend.go_decl_eq
+
+structure blastCpopLayerTarget (aig : AIG α) (outWidth : Nat) where
+  {w len : Nat}
+  oldLayer : AIG.RefVec aig (len * w)
+  h : outWidth = (len + 1) / 2 * w
+  hlen : 0 < len
+
+/-- Given a vector of references `oldLayer`, add the `iterNum`-th couple of elements and
+  append the result of the addition to `newLayer` -/
+def blastCpopLayer (aig : AIG α) (target : blastCpopLayerTarget aig outWidth) :
+    AIG.RefVecEntry α outWidth :=
+  let ⟨oldLayer, h, hlen⟩ := target
+  let initAcc := blastConst aig (w := 0 * _) (val := 0)
+  go 0 oldLayer initAcc
+    (by simp only [Nat.zero_le, Nat.sub_eq_zero_of_le, Nat.mul_zero, hlen]) h
+where
+  go {aig : AIG α} {w len : Nat} (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) :=
+  if  hlen : 0 < len - (iterNum * 2) then
+    -- lhs
+    let res := blastExtract aig ⟨oldLayer, 2 * iterNum * w⟩
+    let aig := res.aig
+    let op1 : aig.RefVec w := res.vec
+    have := AIG.LawfulVecOperator.le_size (f := blastExtract) ..
+    let oldLayer := oldLayer.cast this
+    let newLayer := newLayer.cast this
+    -- rhs
+    let res := blastExtract aig ⟨oldLayer, (2 * iterNum + 1) * w⟩
+    let aig := res.aig
+    let op2 : aig.RefVec w := res.vec
+    have := AIG.LawfulVecOperator.le_size (f := blastExtract) ..
+    let oldLayer := oldLayer.cast this
+    let newLayer := newLayer.cast this
+    let op1 := op1.cast this
+    -- add
+    let res := blastAdd aig ⟨op1, op2⟩
+    let aig := res.aig
+    let add := res.vec
+    have := AIG.LawfulVecOperator.le_size (f := blastAdd) ..
+    let oldLayer := oldLayer.cast this
+    let newLayer := newLayer.cast this
+    let res := blastAppend (aig := aig) ⟨add, newLayer, by simp [Nat.add_mul]⟩
+    let aig := res.aig
+    let newLayer := res.vec
+    have := AIG.LawfulVecOperator.le_size (f := blastAppend) ..
+    let oldLayer := oldLayer.cast this
+    go (iterNum + 1) oldLayer newLayer (by omega) hout
+  else
+    have hcast : iterNum * w = outWidth := by
+      simp [show iterNum = (len + 1)/ 2 by omega, hout]
+    ⟨aig, hcast ▸ newLayer⟩
+termination_by len - iterNum * 2
+
+theorem blastCpopLayer.go_le_size (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) :
+    aig.decls.size ≤ (go iterNum oldLayer newLayer hold hout).aig.decls.size := by
+  unfold go
+  dsimp only
+  split
+  · simp only [AIG.RefVec.cast_cast]
+    <;> (refine Nat.le_trans ?_ (by apply blastCpopLayer.go_le_size); apply AIG.LawfulVecOperator.le_size)
+  · simp
+
+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) :
+    ∀ (idx : Nat) h1 h2,
+      (go iterNum oldLayer newLayer hold hout).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
+  generalize hres : go iterNum oldLayer newLayer hold hout = res
+  unfold go at hres
+  dsimp only at hres
+  split at hres
+  · simp at hres
+    · rw [← hres]
+      intros
+      rw [blastCpopLayer.go_decl_eq]
+      · apply AIG.LawfulVecOperator.decl_eq (f := blastAdd)
+      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastAdd)
+        assumption
+  · simp [← hres]
+
+instance : AIG.LawfulVecOperator α blastCpopLayerTarget blastCpopLayer where
+  le_size := by
+    intros
+    unfold blastCpopLayer
+    dsimp only
+    apply blastCpopLayer.go_le_size
+  decl_eq := by
+    intros
+    unfold blastCpopLayer
+    dsimp only
+    apply blastCpopLayer.go_decl_eq
+
+structure blastCpopTreeTarget (aig : AIG α) (w : Nat) where
+  {len : Nat}
+  x : AIG.RefVec aig (len * w)
+  h : 0 < len
+
+/--
+  Construct a parallel-prefix-sum circuit, invoking `blastCpopLayer` for
+  each layer, until a single addition node is left.
+-/
+def blastCpopTree (aig : AIG α) (target : blastCpopTreeTarget aig w) :
+    AIG.RefVecEntry α w :=
+  let ⟨x, h⟩ := target
+  go x h
+where
+  go {aig : AIG α} {len : Nat} (x : AIG.RefVec aig (len * w)) (h : 0 < len) :=
+    if hlt : 1 < len  then
+      let res := blastCpopLayer aig ⟨x, by simp, h⟩ (outWidth := (len + 1) / 2 * w)
+      go res.vec (by omega)
+    else
+      have hcast : len * w = w := by simp [show len = 1 by omega]
+      ⟨aig, hcast ▸ x⟩
+  termination_by len
+
+theorem blastCpopTree.go_le_size (aig : AIG α) (oldLayer : AIG.RefVec aig (len * w))
+    (h : 0 < len) :
+    aig.decls.size ≤ (go oldLayer h).aig.decls.size := by
+  unfold go
+  dsimp only
+  split
+  · apply Nat.le_trans _ (by apply blastCpopTree.go_le_size)
+    apply blastCpopLayer.go_le_size
+  · simp
+
+theorem blastCpopTree.go_decl_eq (aig : AIG α) (oldLayer : AIG.RefVec aig (len * w))
+      (h : 0 < len) :
+    ∀ (idx : Nat) h1 h2,
+      (go oldLayer h).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
+  generalize hres : go oldLayer h = res
+  unfold go at hres
+  dsimp only at hres
+  split at hres
+  · rw [← hres]
+    intros i h1 h2
+    rw [blastCpopTree.go_decl_eq]
+    · apply blastCpopLayer.go_decl_eq
+    · apply Nat.lt_of_lt_of_le h2
+      apply blastCpopLayer.go_le_size
+  · simp [← hres]
+
+instance : AIG.LawfulVecOperator α blastCpopTreeTarget blastCpopTree where
+  le_size := by
+    intros
+    unfold blastCpopTree
+    apply blastCpopTree.go_le_size
+  decl_eq := by
+    intros
+    unfold blastCpopTree
+    apply blastCpopTree.go_decl_eq
+
+/-- Extend all the  bits in the input BitVec w `x` to have width `w`,
+  then construct the parallel-prefix-sum circuit. -/
+def blastCpop (aig : AIG α) (x : AIG.RefVec aig w) : AIG.RefVecEntry α w :=
+  if hw : 1 < w then
+    let res := blastExtractAndExtend aig (outWidth := w * w) ⟨x, by rfl⟩
+    let aig := res.aig
+    let extendedBits := res.vec
+    blastCpopTree aig ⟨extendedBits, by omega⟩
+  else if hw' : 0 < w then
+    ⟨aig, x⟩
+  else
+    let zero := blastConst aig (w := w) 0
+    ⟨aig, zero⟩
+
+theorem blastCpop_le_size (aig : AIG α) (input : AIG.RefVec aig w) :
+    aig.decls.size ≤ (blastCpop aig input).aig.decls.size := by
+  unfold blastCpop
+  split
+  · let initAcc := blastConst (aig := aig) (w := 0) (val := 0)
+    dsimp only
+    let res := blastExtractAndExtend aig (outWidth := w * w) ⟨input, by omega⟩
+    have hext := blastExtractAndExtend.go_le_size aig 0 (outWidth := w * w)
+      (x := input) (by omega) (acc := initAcc)
+    have := blastCpopTree.go_le_size (aig := res.aig) (oldLayer := res.vec) (by omega)
+    exact Nat.le_trans (hext rfl) this
+  · split
+    · simp
+    · simp
+
+theorem blastCpop_decl_eq (aig : AIG α) (input : AIG.RefVec aig w) :
+    ∀ (idx : Nat) h1 h2, (blastCpop aig input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
+  unfold blastCpop
+  split
+  · simp only [Lean.Elab.WF.paramLet]
+    intros idx hidx hidx'
+    unfold blastCpopTree blastExtractAndExtend
+    dsimp only
+    rw [blastCpopTree.go_decl_eq]
+    · rw [blastExtractAndExtend.go_decl_eq]
+    · apply Nat.lt_of_lt_of_le hidx' (by apply blastExtractAndExtend.go_le_size)
+  · split
+    · simp
+    · simp
+
+instance : AIG.LawfulVecOperator α AIG.RefVec blastCpop where
+  le_size := by
+    intros
+    unfold blastCpop
+    apply blastCpop_le_size
+  decl_eq := by
+    intros
+    unfold blastCpop
+    apply blastCpop_decl_eq
+
+end bitblast
+end BVExpr
+
+end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean

@@ -17,6 +17,8 @@ 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.Impl.Expr
 import Init.ByCases
 import Init.Data.Nat.Linear
@@ -433,6 +435,12 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment)
       intro idx hidx
       rw [goCache_denote_eq]
       exact hinv
+    · rw [← hres]
+      simp only [eval_un, BVUnOp.eval_cpop]
+      rw [denote_blastCpop]
+      intro idx hidx
+      rw [goCache_denote_eq]
+      exact hinv
   next h =>
     subst h
     rw [← hres]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Cpop.lean

@@ -0,0 +1,325 @@
+/-
+Copyright (c) 2026 University of Cambridge. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Luisa Cicolini, Siddharth Bhat, Henrik Böving
+-/
+module
+
+prelude
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Basic
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Const
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Sub
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Append
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Eq
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ZeroExtend
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Extract
+public import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
+
+import Init.Data.BitVec.Bootstrap
+import Init.Omega
+
+/-!
+This module contains the verification of the bitblaster for `BitVec.cpop`, implemented in
+`Impl.Operations.Cpop`.
+-/
+
+namespace Std.Tactic.BVDecide
+
+open Std.Sat
+open Std.Sat.AIG
+
+variable [Hashable α] [DecidableEq α]
+
+namespace BVExpr
+
+namespace bitblast
+
+theorem denote_blastExtractAndExtendBit (aig : AIG α) (xc : AIG.RefVec aig w)
+    (x : BitVec w) (start : Nat) (hx : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, xc.get idx hidx, assign⟧ = x.getLsbD idx) :
+    ∀ (idx : Nat) (hidx : idx < w),
+      ⟦
+        (blastExtractAndExtendBit aig ⟨start, xc⟩).aig,
+        (blastExtractAndExtendBit aig ⟨start, xc⟩).vec.get idx hidx,
+        assign
+      ⟧ = (BitVec.extractAndExtendBit start w x).getLsbD idx := by
+  intros idx hidx
+  generalize hext : blastExtractAndExtendBit aig ⟨start, xc⟩ = res
+  unfold blastExtractAndExtendBit at hext
+  dsimp only [Lean.Elab.WF.paramLet] at hext
+  rw [← hext]
+  simp only [denote_blastZeroExtend, Nat.lt_one_iff, denote_blastExtract,
+    BitVec.getLsbD_extractAndExtendBit]
+  split
+  · split
+    · simp [hx, show idx = 0 by omega, show 0 < w by omega]
+    · simp [show 0 < w by omega, show w ≤ start by omega]
+  · simp [show ¬ idx = 0 by omega]
+
+theorem blastExtractAndExtendBit_denote_mem_prefix (aig : AIG α) (curr : Nat)
+    (xc : RefVec aig w) (hstart : start < aig.decls.size) :
+    ⟦
+      (blastExtractAndExtendBit aig ⟨curr, xc⟩).aig,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart;
+                      apply AIG.LawfulVecOperator.le_size (f := blastExtractAndExtendBit)⟩,
+      assign
+    ⟧ = ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
+  apply IsPrefix.of
+  · intros
+    apply AIG.LawfulVecOperator.decl_eq (f := blastExtractAndExtendBit)
+  · intros
+    apply AIG.LawfulVecOperator.le_size (f := blastExtractAndExtendBit)
+
+theorem denote_append_blastExtractAndExtendBit (assign : α → Bool) (aig : AIG α)
+    (currIdx w : Nat) (x : BitVec w) (xc : AIG.RefVec aig w) (acc : AIG.RefVec aig (w * currIdx))
+    (hidx : idx < w * currIdx + w)
+    (hacc : ∀ (idx : Nat) (hidx : idx < w * currIdx),
+                ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.extractAndExtend w x).getLsbD idx)
+              (hx : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, xc.get idx hidx, assign⟧ = x.getLsbD idx) :
+    ⟦
+      (blastExtractAndExtendBit aig ⟨currIdx, xc⟩).aig,
+      ((acc.cast (by apply AIG.LawfulVecOperator.le_size (f := blastExtractAndExtendBit))).append
+        (blastExtractAndExtendBit aig ⟨currIdx, xc⟩).vec).get idx hidx,
+      assign
+    ⟧ = (BitVec.extractAndExtend w x).getLsbD idx := by
+  rw [RefVec.get_append]
+  split
+  · rw [blastExtractAndExtendBit_denote_mem_prefix (xc := xc)]
+    apply hacc
+    simp only [RefVec.get_cast, Ref.cast_eq]
+    apply acc.hrefs (i := idx)
+  · rw [BitVec.getLsbD_extractAndExtend (by omega)]
+    have h := Nat.div_eq_of_lt_le (k := currIdx) (m := idx) (n := w)
+      (by rw [Nat.mul_comm]; omega)
+      (by rw [Nat.add_mul, Nat.mul_comm currIdx w]; omega)
+    have h' := Nat.mod_eq_sub_mul_div (k := w) (x := idx)
+    rw [h] at h'
+    simp only [← h', ← Nat.div_eq_sub_mod_div (m := idx) (n := w), h]
+    apply denote_blastExtractAndExtendBit (hx := hx)
+
+theorem denote_blastExtractAndExtend.go (assign : α → Bool) (aig : AIG α) (currIdx w : Nat) (xc : AIG.RefVec aig w)
+    (x : BitVec w) (acc : AIG.RefVec aig (w * currIdx)) (hlt : currIdx ≤ w)
+    (hacc : ∀ (idx : Nat) (hidx : idx < w * currIdx),
+                ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.extractAndExtend w x).getLsbD idx)
+    (hx : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, xc.get idx hidx, assign⟧ = x.getLsbD idx) :
+    ∀ (idx : Nat) (hidx : idx < w * w),
+      ⟦
+        (blastExtractAndExtend.go (outWidth := w * w) currIdx xc acc (by omega) (by rfl)).aig,
+        (blastExtractAndExtend.go (outWidth := w * w) currIdx xc acc (by omega) (by rfl)).vec.get idx hidx,
+        assign
+      ⟧ = (BitVec.extractAndExtend w x).getLsbD idx := by
+  intros idx hidx
+  generalize hgen : blastExtractAndExtend.go (outWidth := w * w) currIdx xc acc (by omega) (by rfl) = gen
+  unfold blastExtractAndExtend.go at hgen
+  split at hgen
+  · case _ hlt =>
+    rw [← hgen]
+    rw [denote_blastExtractAndExtend.go]
+    · intros
+      apply denote_append_blastExtractAndExtendBit (hx := hx) (hacc := hacc)
+    · intros i hi
+      rw [blastExtractAndExtendBit_denote_mem_prefix (xc := xc)]
+      apply hx
+      simp [(xc.get i hi).hgate]
+  · have hcurr : currIdx = w := by omega
+    subst hcurr
+    rw [← hgen, ← hacc idx hidx]
+
+theorem denote_blastExtractAndExtend (assign : α → Bool) (aig : AIG α) (w : Nat) (xc : AIG.RefVec aig w)
+    (x : BitVec w)
+    (hx : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, xc.get idx hidx, assign⟧ = x.getLsbD idx) :
+    ∀ (idx : Nat) (hidx : idx < w * w),
+      ⟦
+        (blastExtractAndExtend (outWidth := w * w) aig ⟨xc, by rfl⟩).aig,
+        (blastExtractAndExtend (outWidth := w * w) aig ⟨xc, by rfl⟩).vec.get idx hidx,
+        assign
+      ⟧ = (BitVec.extractAndExtend w x).getLsbD idx := by
+  unfold blastExtractAndExtend
+  apply denote_blastExtractAndExtend.go
+  · simp
+  · exact hx
+
+theorem denote_blastCpopLayer.go (aig : AIG α) (iterNum : Nat)
+    (oldLayer : AIG.RefVec aig (len * w)) (newLayer : AIG.RefVec aig (iterNum * w))
+    (oldLayerBv : BitVec (len * w)) (hold' : 2 * (iterNum - 1) < len)
+    (hold : ∀ (idx : Nat) (hidx : idx < len * w),
+            ⟦aig, oldLayer.get idx hidx, assign⟧ = oldLayerBv.getLsbD idx)
+    (hnew : ∀ (idx : Nat) (hidx : idx < iterNum * w),
+            ⟦aig, newLayer.get idx hidx, assign⟧ =
+        (BitVec.cpopLayer (oldLayer := oldLayerBv) 0#(0 * w) (by simp; omega)).getLsbD idx) :
+    ∀ (idx : Nat) (hidx : idx < (len + 1) / 2 * w),
+      ⟦
+        (blastCpopLayer.go iterNum oldLayer newLayer hold' (by rfl)).aig,
+        (blastCpopLayer.go iterNum oldLayer newLayer hold' (by rfl)).vec.get idx hidx,
+        assign
+      ⟧ = (BitVec.cpopLayer oldLayerBv 0#(0 * w) (by omega)).getLsbD idx := by
+  intros idx hidx
+  generalize hgen : blastCpopLayer.go (outWidth := (len + 1) / 2 * w) iterNum oldLayer newLayer
+    hold' (by rfl) = res
+  unfold blastCpopLayer.go at hgen
+  split at hgen
+  · rw [← hgen]
+    simp only
+    apply denote_blastCpopLayer.go (hold' := by omega)
+    · intros idx hidx
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAppend),
+        AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd),
+        AIG.LawfulVecOperator.denote_mem_prefix (f := blastExtract),
+        AIG.LawfulVecOperator.denote_mem_prefix (f := blastExtract)]
+      simp only [RefVec.cast_cast, RefVec.get_cast, Ref.cast_eq, hold]
+      · exact (oldLayer.get idx hidx).hgate
+      all_goals
+        simp only [RefVec.cast_cast, RefVec.get_cast, Ref.cast_eq]
+        apply LawfulVecOperator.lt_size_of_lt_aig_size
+        apply Ref.hgate
+    · intros idx hidx
+      simp only [RefVec.cast_cast, denote_blastAppend, RefVec.get_cast, Ref.cast_eq]
+      split
+      · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd),
+          AIG.LawfulVecOperator.denote_mem_prefix (f := blastExtract),
+          AIG.LawfulVecOperator.denote_mem_prefix (f := blastExtract)]
+        simp only [hnew]
+        · exact (newLayer.get idx (by omega)).hgate
+        all_goals
+          apply LawfulVecOperator.lt_size_of_lt_aig_size
+          apply Ref.hgate
+      · have hiter : idx / w = iterNum := Nat.div_eq_of_lt_le (by omega) hidx
+        subst hiter
+        rw [BitVec.getLsbD_cpopLayer (oldLayer := oldLayerBv) (by intros; omega) (by omega),
+          ← Nat.div_eq_sub_mod_div (m := idx) (n := w)]
+        simp only [show idx - idx / w * w = idx % w by exact Eq.symm Nat.mod_eq_sub_div_mul]
+        apply denote_blastAdd
+        · intros idx' hidx'
+          simp only [RefVec.get_cast, Ref.cast_eq, hidx', BitVec.getLsbD_eq_getElem,
+            BitVec.getElem_extractLsb']
+          rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastExtract), denote_blastExtract]
+          · split
+            · simp [hold]
+            · case _ hnot =>
+              simp only [Nat.not_lt] at hnot
+              exact Eq.symm (BitVec.getLsbD_of_ge oldLayerBv (2 * (idx / w) * w + idx') hnot)
+          · simp [Ref.hgate]
+        · intros idx'' hidx''
+          simp only [denote_blastExtract, RefVec.get_cast, Ref.cast_eq, BitVec.getLsbD_extractLsb']
+          split
+          · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastExtract)]
+            · simp [hold, hidx'']
+            · apply Ref.hgate
+          · case _ hnot =>
+            simp only [hidx'', decide_true, Bool.true_and, Bool.false_eq]
+            simp only [Nat.not_lt] at hnot
+            apply BitVec.getLsbD_of_ge oldLayerBv (ge := hnot)
+  · have h : iterNum = (len + 1) / 2 := by omega
+    subst h
+    rw [← hgen, hnew]
+
+theorem denote_blastCpopLayer (aig : AIG α)
+    (oldLayer : AIG.RefVec aig (len * w))
+    (oldLayerBv : BitVec (len * w)) (hold' : 2 * (iterNum - 1) < len)
+    (hold : ∀ (idx : Nat) (hidx : idx < len * w),
+            ⟦aig, oldLayer.get idx hidx, assign⟧ = oldLayerBv.getLsbD idx) :
+    ∀ (idx : Nat) (hidx : idx < (len + 1) / 2 * w),
+      ⟦
+        (blastCpopLayer (outWidth := (len + 1) / 2 * w) aig ⟨oldLayer, by rfl, by omega⟩).aig,
+        (blastCpopLayer (outWidth := (len + 1) / 2 * w) aig ⟨oldLayer, by rfl, by omega⟩).vec.get idx hidx,
+        assign
+      ⟧ = (BitVec.cpopLayer oldLayerBv 0#(0 * w) (by omega)).getLsbD idx := by
+  unfold blastCpopLayer
+  dsimp only
+  intros
+  apply denote_blastCpopLayer.go
+  · exact hold
+  · simp
+
+theorem blastCpopLayer_denote_mem_prefix.go (aig : AIG α) (iterNum : Nat)  (hstart : _)
+    (hold' : 2 * (iterNum - 1) < len)
+    (oldLayer : AIG.RefVec aig (len * w)) (newLayer : AIG.RefVec aig (iterNum * w)) :
+    ⟦
+      (blastCpopLayer.go (outWidth := (len + 1) / 2 * w) iterNum oldLayer newLayer hold' (by rfl)).aig,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply blastCpopLayer.go_le_size⟩,
+      assign
+    ⟧ = ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
+  apply IsPrefix.of
+  · intros
+    apply blastCpopLayer.go_decl_eq
+  · intros
+    apply blastCpopLayer.go_le_size
+
+theorem denote_blastCpopTree.go (aig : AIG α) (len : Nat)
+    (l : AIG.RefVec aig (len * w)) (h : 0 < len) (bv : BitVec (len * w))
+    (hpar : ∀ (idx : Nat) (hidx : idx < len * w), ⟦aig, l.get idx hidx, assign⟧ = bv.getLsbD idx) :
+    ∀ (idx : Nat) (hidx : idx < w),
+      ⟦
+        (blastCpopTree.go l h).aig,
+        (blastCpopTree.go l h).vec.get idx hidx,
+        assign
+      ⟧ = (BitVec.cpopTree bv).getLsbD idx := by
+  intros idx hidx
+  generalize hgen : blastCpopTree.go l h = res
+  unfold blastCpopTree.go at hgen
+  split at hgen
+  · rw [← hgen]
+    unfold BitVec.cpopTree
+    simp only [Lean.Elab.WF.paramLet, show ¬len = 0 by omega, reduceDIte, show ¬len = 1 by omega]
+    apply denote_blastCpopTree.go
+    apply denote_blastCpopLayer (iterNum := 0)
+    · simp
+      omega
+    · simp [hpar]
+  · have : len = 1 := by omega
+    subst this
+    rw [← hgen, BitVec.cpopTree]
+    simp only [Lean.Elab.WF.paramLet, Nat.succ_ne_self, reduceDIte, BitVec.getLsbD_cast]
+    rw [← hpar]
+    · congr
+      · simp
+      · apply eqRec_heq
+      · apply proof_irrel_heq
+    · omega
+
+
+theorem denote_blastCpopTree (aig : AIG α) (len : Nat)
+    (l : AIG.RefVec aig (len * w)) (h : 0 < len) (bv : BitVec (len * w))
+    (hpar : ∀ (idx : Nat) (hidx : idx < len * w), ⟦aig, l.get idx hidx, assign⟧ = bv.getLsbD idx) :
+    ∀ (idx : Nat) (hidx : idx < w),
+      ⟦
+        (blastCpopTree aig ⟨l, h⟩).aig,
+        (blastCpopTree aig ⟨l, h⟩).vec.get idx hidx,
+        assign
+      ⟧ = (BitVec.cpopTree bv).getLsbD idx := by
+  unfold blastCpopTree
+  apply denote_blastCpopTree.go
+  simp [hpar]
+
+@[simp]
+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),
+      ⟦
+        (blastCpop aig xc).aig,
+        (blastCpop aig xc).vec.get idx hidx,
+        assign
+      ⟧ = (BitVec.cpop x).getLsbD idx := by
+    generalize hgen : blastCpop aig xc = res
+    rw [BitVec.cpop_eq_cpopRec]
+    unfold blastCpop at hgen
+    split at hgen
+    · simp only at hgen
+      rw [← hgen]
+      unfold BitVec.cpopRec
+      simp only [show 1 < w by omega, reduceDIte, BitVec.cast_eq]
+      apply denote_blastCpopTree
+      apply denote_blastExtractAndExtend
+      simp [hx]
+    · unfold BitVec.cpopRec
+      split at hgen
+      · rw [← hgen]
+        simp [show w = 1 by omega, hx]
+      · rw [← hgen]
+        simp [show w = 0 by omega]
+
+end bitblast
+end BVExpr
+
+end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Reflect.lean

@@ -126,6 +126,10 @@ theorem clz_congr (w : Nat) (x x' : BitVec w) (h : x = x') :
     BitVec.clz x' = BitVec.clz x := by
   simp [*]
 
+theorem cpop_congr (w : Nat) (x x' : BitVec w) (h : x = x') :
+    BitVec.cpop x' = BitVec.cpop x := by
+  simp [*]
+
 end BitVec
 
 namespace Bool

tests/elab/bv_decide_rewriter.lean

@@ -679,6 +679,13 @@ example {x : BitVec 8} (h : x = 0#8) : x.ctz = x.clz := by bv_decide
 example {x : BitVec 8} (h : ¬ x = 0#8) : (x <<< 1).ctz = x.ctz + 1 := by bv_decide
 example {x : BitVec 8} : x.ctz ≤ 8 := by bv_decide
 
+-- CPOP
+example : (BitVec.allOnes 3).cpop = 3#3 := by bv_decide
+example : (0#64).cpop = 0#64 := by bv_decide
+example {x : BitVec 8} : x.cpop = (x.reverse).cpop := by bv_decide
+example {x y : BitVec 8} : (x ++ y).cpop = (x.zeroExtend 16).cpop + (y.zeroExtend 16).cpop:= by bv_decide
+example {x y : BitVec 8} : (x ++ y).cpop = (x.cpop + y.cpop).zeroExtend 16 := by bv_decide
+
 section
 
 namespace NormalizeMul

tests/elab/bv_decide_rewriter.lean.out.expected

@@ -1,2 +1,2 @@
-bv_decide_rewriter.lean:689:0-689:7: warning: declaration uses `sorry`
-bv_decide_rewriter.lean:702:0-702:7: warning: declaration uses `sorry`
+bv_decide_rewriter.lean:696:0-696:7: warning: declaration uses `sorry`
+bv_decide_rewriter.lean:709:0-709:7: warning: declaration uses `sorry`