Awesome
<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->Bits
A formalization of bitset operations in Coq with a corresponding axiomatization and extraction to OCaml native integers.
Meta
- Author(s):
- Andrew Kennedy (initial)
- Arthur Blot (initial)
- Pierre-Évariste Dagand (initial)
- Coq-community maintainer(s):
- Anton Trunov (@anton-trunov)
- License: Apache License 2.0
- Compatible Coq versions: 8.16 or later (use releases for other Coq versions)
- Additional dependencies:
- OCamlbuild
- MathComp 2.0 or later (
algebra
suffices)
- Coq namespace:
Bits
- Related publication(s):
Building and installation instructions
The easiest way to install the latest released version of Bits is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-bits
To instead build and install manually, do:
git clone https://github.com/coq-community/bits.git
cd bits
make # or make -j <number-of-cores-on-your-machine>
make install
Origins
This library has been extracted from Andrew Kennedy et al. 'x86proved' fork. This link presently redirects to https://github.com/nbenton/x86proved repository.
The main paper for this project is Coq: The world’s best macro assembler?.
Using the library
To import the main library, do:
From Bits Require Import bits.
An axiomatic interface supporting efficient extraction to OCaml can be loaded with:
From Bits Require Import extraction.axioms8. (* or 16 or 32 *)
Organization
This library, briefly described in the paper From Sets to Bits in Coq, helps to model operations on bitsets. It's a formalization of logical and arithmetic operations on bit vectors. A bit vector is defined as an SSReflect tuple of bits, i.e. a list of booleans of fixed (word) size.
The key abstractions offered by this library are as follows:
BITS n : Type
- vector ofn
bitsgetBit bs k
- test thek
-th bit ofbs
bit vectorandB xs ys
- bitwise "and"orB xs ys
- bitwise "or"xorB xs ys
- bitwise "xor"invB xs
- bitwise negationshrB xs k
- right shift byk
bitsshlB xs k
- left shift byk
bits
The library characterizes the interactions between these elementary operations and provides embeddings to and from the additive group ℤ/(2ⁿ)ℤ.
The overall structure of the code is as follows:
- src/ssrextra: complements to the Mathcomp library
- src/spec: specification of bit vectors
- src/extraction: axiomatic interface to OCaml, for extraction
For a specific formalization developed in a file A.v
, one will find its
associated properties in the file A/properties.v
. For example, bit-level
operations are defined in src/spec/operations.v,
therefore their properties can be found in
src/spec/operations/properties.v.
Verification axioms
Axioms can be verified for 8-bit and 16-bit (using only extracted code) using the following command:
make verify
For 8bit, the verification process should finish in few seconds. However for 16-bit, depending on your computer speed, it could take more than 6 hours.