No description, website, or topics provided.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
examples
src
.gitignore
LICENSE
Makefile
README.md
_CoqProject
mkhtml.sh

README.md

coq-bitset

Description

The purpose of this library is to help proving bit-level algorithms written in Coq/SSReflect by providing a trivial conversion from operations over bitsets to finite sets and efficient proved extraction to Caml.

A paper describing this library has been accepted at FLOPS2016. The version used for the conference is tagged flops.

A documentation of the library can be found here.

Installation

Installing with OPAM (strongly recommended)

Everything can be installed everything by using OPAM.

You first need to add some coq-related repositories:

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev

Then, you can directly install coq-bitset, coq-bits and the other dependencies will be installed automatically:

opam install coq-bitset

Installing by hand

You may be able to install the library by hand, although it has not been tested.

The dependencies are:

  • Coq 8.5~beta2 (other versions are untested)
  • SSReflect & Mathcomp 1.5.1~beta2 (other versions are untested)
  • coq-bits

Then, just doing the usual:

make
make install

should work.

Usage

In order to import the library, simply use:

From Bitset
  Require Import repr_op.

All the operations are detailed in src/extractions/axioms*.v in the coq-bits repository.

Then, the relation between finite sets and bitsets is defined as:

machine_repr: Int -> {set 'I_wordsize} -> Prop.

Depending on your program, you may have to prove validity by proving a machine_repr relation, or an equality.

All of them can by proved by using the lemmas in src/repr_op.v from this repository, using the OP_repr lemmas, where OP is an "high-level" operation defined in the file using bitset operations (for example: get for getting a bit, inter for computing the intersection, etc.).

You can also look at the examples/ directory for usage examples.