coq-vsu-int63

A Verified Software Unit for 63-bit integer arithmetic.

Implemented in C, modeled in Coq, and proven correct using the Verified Software Toolchain.

Compatible with CompCert.

Verification status

Specifications are proven correct for the following targets:

x86_64-linux
x86_32-linux

Proofs are checked by our CI infrastructure.

Packages

coq-int63 - functional model
coq-vsu-int63-src - C source code
coq-vsu-int63-vst - VST spec & proof (x86_64-linux)
coq-vsu-int63-vst-32 - VST spec & proof (x86_32-linux)
coq-vsu-int63 - All of the above

Installing

Installation is performed by opam with help by coq-vsu.

$ opam pin -n -y .
$ opam install coq-vsu-int63

Using the C library

The C library is installed to the path given by vsu -I. For example:

$ tree `vsu -I`
/home/tcarstens/.opam/coq-8.14/lib/coq-vsu/lib/include
└── coq-vsu-int63
    ├── int63.h
    └── src
        └── int63.c

2 directories, 2 files
$

Using the Coq library

We currently publish three Coq libraries:

coq-int63 - functional model
coq-vsu-int63-vst - VST spec & proof (x86_64-linux)
coq-vsu-int63-vst-32 - VST spec & proof (x86_32-linux)

The coq-int63 library is target-agnostic and is therefore always installed into a location within Coq's search path.

However, coq-vsu-int63-vst and coq-vsu-int63-vst-32 are both target-specific. As such, they are sometimes installed into locations outside of Coq's search path. Fortunately, these libraries can be found by calling vsu --show-coq-variant-path=PACKAGE. For example:

$ echo `vsu --show-coq-variant-path=coq-vsu-int63-vst-32`
/home/tcarstens/.opam/coq-8.14/lib/coq/../coq-variant/appliedfm/32/Int63
$

The vsu tool can also be used to supply Coq with the correct arguments for importing the target-specific libraries. For example:

$ tcarstens@pop-os:~/formal_methods/coq-vsu-int63$ coqtop \
    `vsu -Q coq-vsu-int63-vst-32` \
    `vsu -Q coq-compcert-32` \
    `vsu -Q coq-vst-32`
Welcome to Coq 8.14.0

Coq < From VST Require Import floyd.proofauto.

Coq < From appliedfm Require Import Int63.vst.spec.spec.

Coq < From appliedfm Require Import Int63.vst.proof.proof.

Coq < Check encode_int63_spec.
encode_int63_spec
     : ident * funspec

Coq < Check encode_int63_body.
encode_int63_body
     : semax_body ast.Vprog ASI int63.f_encode_int63 encode_int63_spec

Coq <

Building without `opam`

The general pattern looks like this:

$ make [verydeepclean|deepclean|clean]
$ make BITSIZE={opam|64|32} [all|_CoqProject|clightgen|theories]

BITSIZE determines which compcert target to use. If unspecified, the default value is opam:

opam and 64 both use x86_64-linux
32 uses x86_32-linux

Example: `x86_64-linux`

$ make verydeepclean ; make

Example: `x86_32-linux`

$ make verydeepclean ; make BITSIZE=32

Building the docs

Note that this requires Doxygen and Sphinx.

$ make -C docs html
$ xdg-open docs/build/html/index.html

appliedfm/coq-vsu-int63