feat: add leading zero counter BitVec.clz and bitblaster circuit/infrastructure

[luisacicolini]

This PR adds a new BitVec.clz operation and a corresponding clz circuit to bv_decide, allowing to bitblast the count leading zeroes operation. The AIG circuit is linear in the number of bits of the original expression, making the bitblasting convenient wrt. rewriting. clz is common in numerous compiler intrinsics (see here) and architectures (see here).

Co-authored by @bollu.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-12 17:07:15)
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-13 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-13 09:58:42)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-06-13 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-06-13 19:32:46)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b3a53d5d013d705acf1c664495e74bd7cee32460 --onto fdf6d2ea3bdbebb736aa5d05d00b27a5abaa8fb8. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-17 14:50:15)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b3a53d5d013d705acf1c664495e74bd7cee32460 --onto 3b2990b3816b7e7ec289ad498496a61d18bd85f4. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-18 08:04:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b3a53d5d013d705acf1c664495e74bd7cee32460 --onto e83b7681407043c75f5167c2e4da13e25078a0c0. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-18 11:13:40)

[tobiasgrosser]

https://en.wikipedia.org/wiki/Find_first_set states:

Many architectures include instructions to rapidly perform find first set and/or related operations, listed below. The most common operation is count leading zeros (clz), likely because all other operations can be implemented efficiently in terms of it.

You may want to use this as a justification in the commit message of why you implement clz.

See also https://clang.llvm.org/docs/LanguageExtensions.html#intrinsics-support-within-constant-expressions.

[tobiasgrosser]

This looks great to me. I have a couple of minor nit-picking comments, but am otherwise happy with this.

For the PR title/body:

• add a . at the end of your PR/commit message
• make sure BitVec is mentioned in the PR title
• the PR adds clz as a new operation to BitVec/Basic.lean. It would be good if this is mentioned and justified. E.g., "This PR adds a new operation BitVec.clz together with bitlasting support via bv_decide. `Count leading zeros (clz) is ... We add a specialized bitblaster which requires only AIG nodes linear in the number of bits of the original bitvector expressions and consequently should be easier to bitblast than just a rewrite to existing bitvector expressions.

[luisacicolini]

changelog-library

[hargoniX]

Looks generally like a fine approach!

I did not comment on the clz BitVec proofs yet as I suspect making the definition tail recursive might cause these proofs to turn out quite differently.

I also wonder whether we should add seval simprocs for BitVec.clz right away as well.

[luisacicolini]

thanks @hargoniX for the review! To have a tail-recursive function, I reused BitVec.clzAuxRec: a lot of proofs are thus not needed anymore and the overall structure is simpler. Moreover, to avoid unfolding of BitVec.clzAuxRec, the proof of the correctness of the circuit now relies on two lemmas BitVec.clzAuxRec_zero and BitVec.clzAuxRec_succ that characterize the behavior of BitVec.clzAuxRec, analogously to BitVec.mulRec.