bitblasting of bitvectors

Stream: new members

[Harun Khan]

Hi
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]

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]

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

[Scott Morrison]

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]

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]

@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]

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

[Scott Morrison]

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

[Scott Morrison]

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