feat: add bitblasting circuit for BitVec.cpop

[luisacicolini]

This PR adds a bitblasting circuit for BitVec.cpop.

[luisacicolini]

changelog-library

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 57c5efe309336d173bee324b28d7fefdd955f9df --onto 4cdc199f772977113bd6c1bf87a6c02b78d5c4d3. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-11 16:16:02)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 92aec450578f47e4a04abcd72ad6c2372ed17b2c --onto 6ca23a7b8bee57152110ce500ce795148707d4ed. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-13 14:51:27)

[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 57c5efe309336d173bee324b28d7fefdd955f9df --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-11 16:16:04)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 92aec450578f47e4a04abcd72ad6c2372ed17b2c --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-13 14:51:28)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 92aec450578f47e4a04abcd72ad6c2372ed17b2c --onto 9da8f5dce42832b8411d58446653f3640a94a6e3. You can force reference manual CI using the force-manual-ci label. (2026-02-13 15:44:30)

[bollu]

I did a full pass. I've checked for nonterminal simps, naming conventions, and I've asked to move all the casts that occur in the theorem statements to become hypotheses with default arguments (it makes the theorem statement much more sane to read).