sailfish009/coq_bits

A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]

Bits

A formalization of bitset operations in Coq and the 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.7 or later (use releases for other Coq versions)

• Compatible OCaml versions: 4.05 or later (not tested on previous versions)

• Additional dependencies:

  • MathComp 1.7.0 or later (algebra suffices)

• Coq namespace: Bits

• Related publication(s):

  • From Sets to Bits in Coq doi:10.1007/978-3-319-29604-3_2
  • Coq: The world’s best macro assembler? doi:10.1145/2505879.2505897

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 of n bits
• getBit bs k - test the k-th bit of bs bit vector
• andB xs ys - bitwise "and"
• orB xs ys - bitwise "or"
• xorB xs ys - bitwise "xor"
• invB xs - bitwise negation
• shrB xs k - right shift by k bits
• shlB xs k - left shift by k 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