lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

feat: add `BitVec.cpop` and lemmas

Open luisacicolini opened this issue 1 month ago • 6 comments

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

luisacicolini avatar Nov 19 '25 13:11 luisacicolini

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)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eee58f4506d28a14c9a171165f999445a0663d93 --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-11 08:49:08)

leanprover-community-bot avatar Nov 20 '25 20:11 leanprover-community-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)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase eee58f4506d28a14c9a171165f999445a0663d93 --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force reference manual CI using the force-manual-ci label. (2025-12-11 08:49:10)

leanprover-bot avatar Nov 20 '25 20:11 leanprover-bot

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

bollu avatar Nov 26 '25 09:11 bollu

  • 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.

tobiasgrosser avatar Nov 27 '25 05:11 tobiasgrosser

changelog-library

luisacicolini avatar Dec 05 '25 15:12 luisacicolini

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

Thank you for the review @hargoniX :) I have addressed the comments and rebased the PR! This is good to go for me, @TwoFX I would appreciate your review.

luisacicolini avatar Dec 11 '25 12:12 luisacicolini

thank you for the review!! :)

luisacicolini avatar Dec 17 '25 09:12 luisacicolini