Best practices for machine-level representation of numbers and bitwise operations

Using Coq
1

Hello!

I was wondering what libraries would people tend to favor when wanting to represent machine words of different (fixed) sizes. There seem to be quite a few different options, some axiomatic, some more concrete.

I found these two axiomatic interfaces:

https://coq.inria.fr/library/Coq.Numbers.Natural.Abstract.NBits.html

https://coq.github.io/doc/master/stdlib/Coq.Numbers.NatInt.NZBits.html

But I’m not sure whether either of them is ever realized anywhere, or if their main purpose was abstract reasoning.

There also are some small formalization efforts here and there:

(this seems like the most recent, with some extraction capabilities too)

But I’m unsure whether I am missing some better alternative. So, what do people use, or what do people wish existed in this space?

Thanks!

1 Like
2

Sifive uses bbv, maybe it suits you:

3

I think CompCert’s approach to parameterized machine words (using the Z type) could be useful as inspiration as well, see the main file here.

Another recent paper on bit vectors is the following (“Verifying Bit-vector Invertibility Conditions in Coq”): https://arxiv.org/abs/1908.09478

1 Like
4

There is also the “coqword” library, mainly by P.-Y. Strub, that is used in the Jasmin compiler.

The representation of a machine word is a subtype of Z (binary), as in CompCert, but it uses dependent types to avoid the “functor hell”: you can easily reason about operations that deal with several word sizes.

1 Like
5

The Coq library for the bit-vector invertibility paper linked above is here:

According to one of the authors, it was based on a previous bit-vector library used in the SMTCoq plugin:

6

For completeness, here is a paper related to the coq-bits library linked above: From Sets to Bits in Coq

And here is a variation of the coq-bits library that includes some extensions:

7

This might be worth a look? https://github.com/mit-plv/coqutil/tree/master/src/coqutil/Word