Home

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

Docker CI Contributing Code of Conduct Zulip DOI

A formalization of bitset operations in Coq with a corresponding axiomatization and extraction to OCaml native integers.

Meta

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:

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:

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.