Zulip Chat Archive

Stream: new members

Topic: bitblasting of bitvectors

Harun Khan (Jun 10 2023 at 23:07):

I've been working on a project that involves proving the correctness of bitblast rules for bitvectors (e.g., Fin.add corresponds to 2's complement addition). So far we proved the correspondence for addition, unsigned less than, multiplication, negation etc...
I'd like to PR this to mathlib in steps. I'll start with unsigned less than and addition (i.e. the first 173 lines of the first link). My github is mhk119.
See https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.
(I'm putting this here for context https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/BitVec.lean but I'm interested in PR-ing the former.)
How do I initiate the process and is it ok to PR to mathlib4 now?

Scott Morrison (Jun 11 2023 at 01:02):

My initial concern here is that there some doubt about how much algebraic structure we should put on Fin in the first place, and if in particular you even mention multiplication, then probably you should use ZMod instead of Fin.

Scott Morrison (Jun 11 2023 at 01:04):

Also, all of your pow_two names should be two_pow, I think.

Scott Morrison (Jun 11 2023 at 01:06):

I can't really work out what is happening in that file -- most of the defs don't have docstrings, and without knowing the intended semantics of the definitions I can't guess what the theorems are even saying. :-)

Harun Khan (Jun 11 2023 at 07:21):

Thank you very much for your reply. I've seperated unsigned less than and addition from the rest of the operators now and added docstrings.
So a good-looking file I'd like to PR is here: https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean whereas the rest of the operations need some proof refactoring https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwisemain.lean. I've also edited the original message to reflect this change.

Scott Morrison (Jun 11 2023 at 09:20):

@Harun Khan , I've sent you an invitation. Please make a PR, and add the awaiting-CI and awaiting-review labels. You can also write a message here to say it's ready.

Your file will certainly need some review and cleanup --- I'm not an expert on SMT interfaces, so I won't be the one to merge the PR, and I'll just apologise ahead of time if the process is slow. We are still all very involved in finishing the port from mathlib3 to mathlib4, and the "normal" review process is still somewhat in limbo.

Harun Khan (Jun 12 2023 at 04:01):

Thanks for the invite! It's now ready so I made a PR (!4#4979).

Scott Morrison (Jun 12 2023 at 04:34):

For now you still need to write !4#4979 for the linkifier to link to mathlib4 PRs.

Scott Morrison (Jun 12 2023 at 04:42):

I added some review comments to get you started. :-)

Last updated: Dec 20 2023 at 11:08 UTC