feat: add BitVec.cpop and lemmas

[luisacicolini]

This PR adds the definition of BitVec.cpop, which relies on the more general BitVec.cpopNatRec, and build some theory around it. The name cpop aligns with the RISCV ISA nomenclature.

Co-authored-by: @tobiasgrosser, @bollu

[tobiasgrosser]

Some early comments. This is going in a great direction.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9fc90488ce239cfe8e4317269d37fe4160787d0d --onto a106ea053fec080a50204b0ad6dadc69bc3f0937. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-20 20:35:04)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9fc90488ce239cfe8e4317269d37fe4160787d0d --onto 5306a3469d20caa5f9d80384a5c1effdb14e9c67. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-21 11:26:56)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3772bb8685f2fdf414e8aa4af6f1d2964b2f64af --onto b0e6db322421ce368999f08870fd747e45242f86. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-26 11:21:06)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-11-27 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-27 10:17:58)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-11-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-29 17:49:36)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0e83422fb6337985c3354c263a9510cbcb4b1e05 --onto 5bd331e85d9d110a29fb3367dbb21854010ffcbd. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-02 15:24:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0e83422fb6337985c3354c263a9510cbcb4b1e05 --onto dd28f005889dd2fcca6fe0638133de561a655ad1. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-05 10:25:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0e83422fb6337985c3354c263a9510cbcb4b1e05 --onto 455fd0b4488e2adc85f825a52e2ee7d944a5740a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-05 15:21:59)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0e83422fb6337985c3354c263a9510cbcb4b1e05 --onto 2ca3bc28590c5c33f755d3bd18252f25ea266266. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-08 11:12:52)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9fc90488ce239cfe8e4317269d37fe4160787d0d --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-20 20:35:06)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3772bb8685f2fdf414e8aa4af6f1d2964b2f64af --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-26 11:21:08)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-27 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-27 10:18:00)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-29 17:49:38)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0e83422fb6337985c3354c263a9510cbcb4b1e05 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-02 15:24:05)

[bollu]

This is going in a nice direction!

I think we should have a definition called cpopAux (x : BitVec w) : Nat := cpopAuxRec x w, and then define cpop in terms of cpopAux. In some sense cpopAux is the "real population count" (as a number), and cpop is a convenience function we provide to coerce the result into a bitvector.

---

Along similar lines, I would personally decouple the input and output widths of cpop, to have the signature be

def cpop {v : Nat} (w : Nat) (x : BitVec v) : BitVec w := BitVec.ofNat w x

I'm not 100% sure this is the right design, but it feels a lot less arbitrary to me than choosing the output width, when popCount is really counting a natural number.

---

As always, this is not final, and I'm trying to navigate the design space just as much as you are, so I'm happy to pair on this!

[bollu]

Also, note that popcount is uniquely defined by three equations:

popCount (x ++ y) = popCount x + popCount y
popCount (x#0) = 0
popCount (BitVec.ofBool b) = b.toNat

These tell us that popcount is a monoid homomorphism from bitvectors to naturals, and does the "correct" thing. I'd like us to prove these lemmas, and to define popcount such that these hold with small proofs :) So this would have us replace the if b then 1 else 0 with b.toNat

[tobiasgrosser]

Thank you for the update. A first set of comments.

[tobiasgrosser]

• Update the PR message BitVec.cpopAuxRec to BitVec.cpopNatRec

It would also be nice if the default type conversion theorems are implemented, e.g., toNat, toFin, toInt, as well as getMsb, getLsb, msb. We can potentially do this in a fullow-up PR or after having gotten an initial review.

[luisacicolini]

changelog-library

[hargoniX]

Looks quite good! I'll defer to Markus after the two remaining remarks.

[hargoniX]

Why are the toNat versions simp and not these ones?

[luisacicolini]

In the toNat theorem the rhs seems definitely easier than the lhs, for this theorem I don't think that's necessarily true, because of the setWidth. Do you think that is strictly easier even with the setWidth?

[tobiasgrosser]

AFAIU, the convention is to push toNat inwards. I do not think we have a canonical form for the plain cpop_cons.