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


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:

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?


1 Like

Sifive uses bbv, maybe it suits you:

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”):

1 Like

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

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:

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:

This might be worth a look?