mit-plv/bbv

Bedrock Bit Vector Library

bbv's Issues

bulky representation of concrete words

Because of indices (which nest), every concrete 64 bit word has 2080 S constructors, even though it has only 64 WS constructors. Should we opt for a less intrinisically dependently typed variant like Word s := {n:N | log n< s}?

Fixpoint sumFirstN (n : nat) : nat :=
match n with
| O => O
| S n => (S n) + (sumFirstN n)
end.

Eval compute in (sumFirstN 64)

bbv makes it impossible to use $ as a prefix printing notation without parentheses

Word.v defines "$ x" to be a notation at level 0 (and similarly with #). This conflicts with the notations I want to use in fiat-crypto. Please put these notations in a Module (e.g., WordNotations) and do not export this module by default from any file.

need coq 8.18 compatible release

The current git version builds with coq-8.18. Could we please have a new release in OPAM? Thanks!

Make new 8.14 compatible release

omega was officially dropped from 8.14 and bbv already replaced omega with lia in 51e6f99 but a lia-only release is missing.

Incompatibility with coq.8.17.1

When trying to resintall coq-bbv.1.3 after upgrading coq in opam to 8.17.1, the following error is produced:

File "./src/bbv/DepEq.v", line 17, characters 0-32:
Error: The default value for rewriting hint locality is currently "global"
outside sections, but is scheduled to change to "export" in the next release
(Coq 8.18). In Coq 8.17, not providing an explicit locality outside sections
triggers a fatal warning, to ensure that hint localities are made explicit
before the upcoming change in the default value. It is recommended to use
"export" whenever possible. Use the attributes #[local], #[global] and
#[export] depending on your choice. For example: "#[export] Hint Rewrite foo
: bar." This is supported since Coq 8.14.
[deprecated-hint-rewrite-without-locality,deprecated]

bbv/theories checkin breaks all projects using bbv

Looks like I didn't realize this affects all the projects using bbv :(

In my setup, my _CoqProject using bbv has the following:

-R . Kami
-R ../bbv bbv

And inside my files (in Kami), I do "Require Import bbv/Word.".

The following change to _CoqProject does not work.
-R . Kami
-R ../bbv/theories bbv

Also, why is this a good idea as opposed to storing the .vo files directly in the directories named after the project?

Building theories/Word.vo is slow

It takes about 24 seconds on my machine, which is about 10% of the total time spent building util files in fiat-crypto (and is 1.5x slower than the next-slowest file). It'd be nice for it to be faster. Alternatively (or additionally), it might make sense to split it into a file that defines word and the operations on word, and another file that proves things about words, so that files that just want to compute with words don't have to wait for the proofs.

Update opam package

Are people ok with me cutting a new release that is compatible with coq-8.9 and making an opam package for it?

Make an opam package

We should make an opam package for this (once the PRs are merged).

Extracting [hexDigitToN] in Haskell creates Data.Bits.testBit and Data.Char.ord

Since the generated Haskell does not import Data.Bits.testBit and Data.Char.ord, the overall compilation of the Haskell program fails. Any ideas to avoid generating these functions during Extraction?