Skip to content
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

feat: add BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod) #6795

Merged
merged 10 commits into from
Feb 4, 2025
Merged

feat: add BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod) #6795

merged 10 commits into from
Feb 4, 2025

Conversation

luisacicolini
Copy link
Contributor

@luisacicolini luisacicolini commented Jan 27, 2025 •
edited
Loading

This PR adds theorems BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod). For the defiition of these theorems we rely on divRec, excluding the case where d=0#w, which is treated separately because there is no infrastructure to reason about this case within divRec. In particular, our implementation follows the mathlib standard where division by 0 yields 0, while in SMTLIB this yields allOnes.

Co-authored by @bollu.

@luisacicolini luisacicolini changed the title feat: add 'BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod) and support BitVec.le_zero_eq_zero` feat: add BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod) and support BitVec.le_zero_eq_zero Jan 27, 2025
@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 Jan 27, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 27, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4ca98dcca2b0995dddff444cfef1f3ccc89c7b12 --onto 69a73a18fbfa1fc045bfbf1c4cf93b155d4c9387. (2025-01-27 15:48:51)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7c1e091c9f07ae6f8e8ff7246eb7650e2740dcb --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-28 11:10:40)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7c1e091c9f07ae6f8e8ff7246eb7650e2740dcb --onto e922edfc218090ab2e54092336c67fe3b970dfc2. (2025-01-30 16:34:13)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7c1e091c9f07ae6f8e8ff7246eb7650e2740dcb --onto 412389f71f8a24307e3adba69b38b4b685b04f72. (2025-02-04 14:36:32)

@tobiasgrosser
Copy link
Contributor

Thank you. Could you add 1-2 sentences of motivation of why you choose these right-hand-sides that you see here.

@luisacicolini
feat: add `BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, ge…
2c3028e 
…tMsbD_umod)` and support `BitVec.le_zero_eq_zero`

This PR adds theorems `BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod)` and support theorem `BitVec.le_zero_eq_zero`. For the defiition of these theorems we rely on `divRec`, excluding the case where `d=0#w`, which is treated separately because there is no infrastructure to reason about this case within `divRec`. In particular, our implementation follows the mathlib standard [where division by 0 yields 0](https://github.com/leanprover/lean4/blob/c7c1e091c9f07ae6f8e8ff7246eb7650e2740dcb/src/Init/Data/BitVec/Basic.lean#L217), while in [SMTLIB this yields `allOnes`](https://github.com/leanprover/lean4/blob/c7c1e091c9f07ae6f8e8ff7246eb7650e2740dcb/src/Init/Data/BitVec/Basic.lean#L237).

Co-authored by @bollu.
@luisacicolini luisacicolini changed the title feat: add BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod) and support BitVec.le_zero_eq_zero feat: add BitVec.(getElem_umod_of_lt, getElem_umod, getLsbD_umod, getMsbD_umod) Jan 28, 2025
bollu
bollu reviewed Jan 29, 2025
View reviewed changes
Copy link
Contributor

@bollu bollu left a comment

Choose a reason for hiding this comment

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

LGTM, modulo my comments about proof reuse. It would be nice to not repeat the same proof, as that's a bit brittle.

@luisacicolini luisacicolini requested a review from bollu January 29, 2025 15:07
bollu
bollu approved these changes Jan 30, 2025
View reviewed changes
Copy link
Contributor

@bollu bollu left a comment

Choose a reason for hiding this comment

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

LGTM. These straightforwardly use the bitblasting theorems as getElem/getLsbD/getMsb.

@luisacicolini @bollu
chore: terminal simp
6cc0c58 
Co-authored-by: Siddharth <[email protected]>
@luisacicolini
Copy link
Contributor Author

awaiting-review

@luisacicolini luisacicolini marked this pull request as ready for review January 30, 2025 15:55
@luisacicolini luisacicolini requested a review from kim-em as a code owner January 30, 2025 15:55
@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Jan 30, 2025
@luisacicolini
Copy link
Contributor Author

changelog-library

@github-actions github-actions bot added the changelog-library Library label Jan 30, 2025
@luisacicolini luisacicolini marked this pull request as draft January 30, 2025 16:01
alexkeizer
alexkeizer reviewed Jan 30, 2025
View reviewed changes
src/Init/Data/BitVec/Bitblast.lean Outdated Show resolved Hide resolved
src/Init/Data/BitVec/Bitblast.lean Show resolved Hide resolved
src/Init/Data/BitVec/Bitblast.lean Outdated Show resolved Hide resolved
@luisacicolini luisacicolini marked this pull request as ready for review February 3, 2025 14:40
bollu
bollu approved these changes Feb 4, 2025
View reviewed changes
Copy link
Contributor

@bollu bollu left a comment

Choose a reason for hiding this comment

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

LGTM

@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Feb 4, 2025
@hargoniX hargoniX added this pull request to the merge queue Feb 4, 2025
Merged via the queue into leanprover:master with commit 3b41e43 Feb 4, 2025
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@bollu bollu bollu approved these changes

@tobiasgrosser tobiasgrosser Awaiting requested review from tobiasgrosser

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

@alexkeizer alexkeizer Awaiting requested review from alexkeizer

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR changelog-library Library P-medium We may work on this issue if we find the time 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.
7 participants
@luisacicolini @leanprover-community-bot @tobiasgrosser @bollu @alexkeizer @hargoniX @leanprover-bot