A formalization of bitset operations in Coq with a corresponding axiomatization and extraction to OCaml native integers.
- 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 (
algebrasuffices)
- Coq namespace:
Bits - Related publication(s):
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-bitsTo 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 installThis 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?.
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 *)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 ofnbitsgetBit bs k- test thek-th bit ofbsbit vectorandB xs ys- bitwise "and"orB xs ys- bitwise "or"xorB xs ys- bitwise "xor"invB xs- bitwise negationshrB xs k- right shift bykbitsshlB xs k- left shift bykbits
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.
Axioms can be verified for 8-bit and 16-bit (using only extracted code) using the following command:
make verifyFor 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.
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent