https://github.com/avigad/lean-auto

It might be worth mentioning that there is an open Mathlib PR which I believe was based on the same BitVec library as this PR, and has undergone several rounds of review.

It might be better to get this into mathlib first, rather than having to copy things around if it is already under review there. Is there a representative project that is currently using this API? I would feel more comfortable merging a new API like this if I knew it was already meeting the needs of another project, and getting it in mathlib is one way to do that.

@alexkeizer and @digama0 Bit vectors must be in the Std. They are essential for software and hardware verification, and support for bit vectors in lean-auto is blocked because we don't have bit vectors in Std. lean-auto is a package for invoking SMT solvers from Lean. I need lean-auto for applications.
I am happy to move the Mathlib PR here myself or tolerate the duplication for now. Happy with any of these two options, tell me which one you prefer and I will get it done by tomorrow.

@alexkeizer and @digama0 Bit vectors must be in the Std. They are essential for software and hardware verification, and support for bit vectors in lean-auto is blocked because we don't have bit vectors in Std.

To be clear, I don't contest this and would like us to have a bitvectors API in Std. My concern is about whether the API here is the right one, or whether we need to expose things in a different way or with different definitions (e.g. little endian vs big endian). My main tool for evaluating this is to look at usage of the API in a downstream project. It is relatively easier to merge PRs migrating from mathlib because they have already undergone some API battle testing in order to incorporate them in the library.

How exactly is lean-auto blocked? (Not contesting the claim, asking for details.) Should it not be possible to simply have this module in lean-auto since dependencies of it will be able to use this? This is what aesop and mathlib have done in the past when it comes to merging things upstream: they keep a copy of the module and use that instead pending the merge. This practice also helps to get more data and refine the API.

Lean-auto is not necessarily "blocked", but importing the current implementation of BitVec from Mathlib makes compilation and initialization unacceptably slow. @digama0 It seemed to me that there would be no problem to have Bitvec in Std immediately. But since it contradicts the method used to evaluate APIs, I'd be happy to just have this module in Lean-auto.

I'm not trying to block this PR, I'm soliciting information on how it is used. Maybe there could be a test file or something, to demonstrate intended usage?

but importing the current implementation of BitVec from Mathlib makes compilation and initialization unacceptably slow

This is actually very valuable information, it indicates that the Mathlib BitVec API has issues (which I have also long suspected). It would be great to have a summary of how this API differs from it, what the problems were and why this implementation works better.

Lean-auto just imports those Bitvec definitions, and matches their name against constant names in the input so that it can recognize them as Bitvec operations. The actual implementation of Bitvec has no impact on the performance of Lean-auto. What really matters to Lean-auto is the name of the Bitvec operations.

@digama0 I think the slow compilation might not be caused by the specific Bitvec implementation. Generally, whenever I import files from mathlib, the compilation of lean-auto becomes significantly slower, so I've been avoiding importing anything from mathlib, and I have several modules copied from mathlib in Lean-auto (I didn't do the same to Bitvec because I thought it makes sense to have it in std).

@PratherConid Could you provide a list of all definitions you need in the BitVec library? I am assuming you need all the functions that are available on SMT-Lib, correct? The actual names will not be exactly the same, but we can put the corresponding SMT-Lib names in the doc strings.

@digama0 I am going to be using the BitVec library in actual applications, and we will polish the API and add theorems as we go. @joehendrix will help making sure the library is good for software and hardware verification applications. AFACIT, the Bitvec module in Mathlib has no users. So, this PR and future ones will have no impact on Mathlib.
BTW, SMT-Lib is a great reference for bit vectors since SMT solvers are already used in many hardware and software verification applications.

@leodemoura Yes, I only need the functions available on smt-lib 2.6 https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml

We are also looking to use bitvectors in our project. We started using the current bitvector API, but when the discussed refactor was proposed we stopped until it became clear which representation mathlib would use.

I did not necessarily mean to suggest postponing this PR, I would be happy to have bitvectors in STD ASAP, I merely wanted to point out the existing efforts.

The refactor also got discussed on Zulip (https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Proposed.20refactor.20of.20Bitvec).

@alexkeizer Thanks for sharing. The good news is that things will start moving really fast here in Std :) Our plans are

• Std should be great for software/hardware verification projects.
• Std should be great for software development, and should provide a library with the same capabilities of the Rust std.
• Better automation for software/hardware verification projects using Std.

We're lucky to have Joe Hendrix (@joehendrix) on board with us at Lean FRO. He's a pro when it comes to software verification and development. Joe's got our back in hitting our goals and will help us get those PRs merged super fast.

I pushed some changes. Summary:

• Added more documentation to all of the operations
• General style guide things (indentation etc)
• Simplified some of the definitions
• Added fill as a version of replicate that just splats a bool across the vector
• Changed LT and LE to delegate to the Fin LT/LE (which delegates to the Nat one), instead of using the Bool function which will cause spurious decide (x < y) = true things in proofs using these ops
• Clarified things like what zero extension, left/right shift, and other bitwise ops mean in terms of bit positions and also numbers where applicable. I tried to avoid saying things like "the left side" in favor of "the low bits" to avoid ambiguity depending on how the user's mental picture is laid out. (The Rust stdlib also uses this guideline, because RTL languages exist too.)
• Renamed shrink to truncate, because shrink is not particularly explanatory regarding how the shrinking is supposed to happen (are we losing high bits or low bits?), while "truncate" is more consistently used for dropping high bits in integer conversion.
• shrink and zeroExtend are actually aliases, but they have documentation which focuses on the case in the name.

I did not make any changes to the things under discussion (big endian, the # notation).

@digama0 I personally think the comment changes and cleanups improve readability so thanks.

One interesting thing is that most-significant being on the left is part of our Hindu Arabic numeral system -- even traditionally right-to-left languages have most-significant digits on the left.

I don't want the bit order discussion to block this PR from being merged, so if you haven't been persuaded I am ok with avoiding committing to a bit order in this PR.

As things stand currently, the only place where big endian has to be explicitly acknowledged is in the argument order for append, and actually we might also want the reversed argument order not simply because of endianness but also because it would have the addition in the opposite order, which would make it a bit easier re: dependent typing in some cases (note that there are some uses of Nat.add_comm .. ▸ (v1 ++ v2) in this PR, and probably even more in usage code). Given that we are explicitly acknowledging that these functions are intended to be compatible with SMT-lib and the main functions have cross references to it, I don't mind keeping this argument order since we'd need a SMT-lib compatible version anyway.

In general, dependent typing hell will definitely arise when working with this API when the bitwidths are not numeric literals, so we probably need to do something to help with that (although as usual it is difficult to predict in advance what that might be). One thing is that we probably want a ofEq function for coercing between bitvector types with equal but not defeq bitwidth; mathlib makes a point of defining these for all dependent type families because they compute better than Eq.rec terms.

I've pushed ofFin/toFin changes and a change to use hex for rendering bitvectors. I don't know if people will always like that, but is is easy to convert to a Nat if one wants a decimal rendering.

digama0 I can add a ofEq. Is the conventional signature something like ofEq : u = v -> BitVec u -> BitVec v?

I've pushed ofFin/toFin changes and a change to use hex for rendering bitvectors. I don't know if people will always like that, but is is easy to convert to a Nat if one wants a decimal rendering.

Actually I was thinking you might want binary rendering. I can't imagine you would ever want decimal, that seems exceedingly unhelpful for understanding a bitvector value. But binary is a bit too verbose and is probably not suitable for more than 4-8 bits. You could have a delaborator option to control this.

I've pushed ofFin/toFin changes and a change to use hex for rendering bitvectors. I don't know if people will always like that, but is is easy to convert to a Nat if one wants a decimal rendering.

digama0 I can add a ofEq. Is the conventional signature something like ofEq : u = v -> BitVec u -> BitVec v?

The signature is right, but I think these kind of functions are usually called cast, as in https://leanprover-community.github.io/mathlib4_docs/Std/Data/Fin/Basic.html#Fin.cast

Thanks @alexkeizer , @leodemoura , @joehendrix and everyone else for working on this. I think it looks really good now, and although there is still more to do (toList, split, lemmas, automation) this looks like a good starting point from which to start getting user feedback and iterate further.