8000 feat: add leading zero counter `BitVec.clz` and bitblaster circuit/infrastructure by luisacicolini · Pull Request #8546 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 119 commits into from
Jun 18, 2025
Merged

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

merged 119 commits into from
Jun 18, 2025

Conversation

luisacicolini
Copy link
Contributor
@luisacicolini luisacicolini commented May 30, 2025 •
edited
Loading

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.

tobiasgrosser
tobiasgrosser reviewed May 30, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed May 30, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed May 30, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed May 30, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed May 30, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed May 30, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed May 30, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed May 30, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed May 30, 2025
View reviewed changes
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 12, 2025
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented Jun 12, 2025 •
edited
Loading

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
tobiasgrosser reviewed Jun 13, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed Jun 13, 2025
View reviewed changes
luisacicolini
luisacicolini commented Jun 13, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed Jun 13, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser reviewed Jun 13, 2025
View reviewed changes
@tobiasgrosser
Copy link
Contributor
tobiasgrosser commented Jun 13, 2025 •
edited
Loading

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.

bollu
bollu reviewed Jun 13, 2025
View reviewed changes
bollu 8000
bollu reviewed Jun 13, 2025
View reviewed changes
bollu
bollu reviewed Jun 13, 2025
View reviewed changes
bollu
bollu reviewed Jun 13, 2025
View reviewed changes
bollu
bollu reviewed Jun 13, 2025
View reviewed changes
bollu
bollu reviewed Jun 13, 2025
View reviewed changes
tobiasgrosser
tobiasgrosser approved these changes Jun 16, 2025
View reviewed changes
Copy link
Contributor
@tobiasgrosser tobiasgrosser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
luisacicolini commented Jun 17, 2025
View reviewed changes
@luisacicolini luisacicolini marked this pull request as ready for review June 17, 2025 15:37
@luisacicolini
Copy link
Contributor Author

changelog-library

@github-actions github-actions bot added the changelog-library Library label Jun 17, 2025
@luisacicolini luisacicolini changed the title feat: add leading zero counter BitVec.clz and bitblaster infrastructure feat: add leading zero counter BitVec.clz and bitblaster circuit/infrastructure Jun 17, 2025
hargoniX
hargoniX requested changes Jun 17, 2025
View reviewed changes
Copy link
Contributor
@hargoniX hargoniX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 luisacicolini requested a review from hargoniX June 18, 2025 11:04
@luisacicolini
Copy link
Contributor Author
luisacicolini commented Jun 18, 2025 •
edited
Loading

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.

@hargoniX hargoniX added this pull request to the merge queue Jun 18, 2025
Merged via the queue into leanprover:master with commit 62f3ee2 Jun 18, 2025
15 checks passed
algebraic-dev pushed a commit to algebraic-dev/lean4 that referenced this pull request Jun 18, 2025
@luisacicolini @tobiasgrosser
@bollu @algebraic-dev
feat: add leading zero counter BitVec.clz and bitblaster circuit/in…
fe5d29f 
…frastructure (leanprover#8546)

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](https://clang.llvm.org/docs/LanguageExtensions.html#intrinsics-support-within-constant-expressions))
and architectures (see
[here](https://en.wikipedia.org/wiki/Find_first_set)).

Co-authored by @bollu.

---------

Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Siddharth <siddu.druid@gmail.com>
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 24, 2025
@luisacicolini @tobiasgrosser
@bollu @wkrozowski
feat: add leading zero counter BitVec.clz and bitblaster circuit/in…
c5a2d11 
…frastructure (leanprover#8546)

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](https://clang.llvm.org/docs/LanguageExtensions.html#intrinsics-support-within-constant-expressions))
and architectures (see
[here](https://en.wikipedia.org/wiki/Find_first_set)).

Co-authored by @bollu.

---------

Co-authored-by: Tobias Grosser <github@grosser.es>
Co-authored-by: Siddharth <siddu.druid@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tobiasgrosser tobiasgrosser tobiasgrosser approved these changes

@bollu bollu bollu approved these changes

@hargoniX hargoniX hargoniX approved these changes

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees
No one assigned
Labels
changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@luisacicolini @leanprover-community-bot @tobiasgrosser @bollu @hargoniX
0