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?
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”): https://arxiv.org/abs/1908.09478
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.
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: