Skip to content

Formally verified 63-bit integer arithmetic, implemented in C and proven in Coq

License

Notifications You must be signed in to change notification settings

appliedfm/coq-vsu-int63

Folders and files

NameName
Last commit message
Last commit date

Latest commit

132c571 · Mar 4, 2022

History

79 Commits
Jan 18, 2022
Feb 3, 2022
Jan 18, 2022
Mar 4, 2022
Jan 18, 2022
Jan 18, 2022
Jan 16, 2022
Jan 16, 2022
Feb 3, 2022
Jan 20, 2022
Mar 4, 2022
Jan 21, 2022
Jan 17, 2022
Jan 21, 2022
Jan 21, 2022
Jan 17, 2022

Repository files navigation

coq-vsu-int63

Website Documentation Status build

GitHub

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

Coq compcert VST Alectryon Sphinx readthedocs

applied.fm