coq-vsu

Tools for working with Verified Software Units in the Coq ecosystem.

What is a Verified Software Unit?

A verified software unit (VSU) is a C library that has been proven correct using the Verified Software Toolchain.

The theory of VSUs was introduced by Verified Software Units (Beringer 2021). Examples of how to use VST to build VSUs are given in Software Foundations Volume 5: Verifiable C.

What is coq-vsu?

A typical VSU consists of a library written in Coq that proves functional correctness of a library written in C.

This unique project structure is not natively supported by opam. In particular, opam provides no guidance on questions such as Where should the C library be installed to? and How will users configure their compiler to find it?

coq-vsu answers these questions with a single tool: vsu, which has the magic ability to locate paths.

For a simple example of coq-vsu in action, see coq-vsu-int63.

Example: C library paths

The vsu -I command prints a path within the current opam switch that is suitable for installing VSU libraries.

$ echo `vsu -I`
/home/tcarstens/.opam/coq-8.14/lib/coq-vsu/lib/include
$

One important feature of this design is that it is compatible with the -I flag found in compcert, clang, and gcc. For example, the following brings all VSU libraries into scope when compiling main.c:

$(CC) -I`vsu -I` main.c

Example: Coq library paths

compcert

$ echo `vsu --show-coq-variant-path=coq-compcert`
/home/tcarstens/.opam/coq-8.14/lib/coq/user-contrib/compcert
$ echo `vsu --show-coq-variant-path=coq-compcert-32`
/home/tcarstens/.opam/coq-8.14/lib/coq-variant/compcert32/compcert

vst

$ echo `vsu --show-coq-variant-path=coq-vst`
/home/tcarstens/.opam/coq-8.14/lib/coq/user-contrib/VST
$ echo `vsu --show-coq-variant-path=coq-vst-32`
/home/tcarstens/.opam/coq-8.14/lib/coq-variant/VST32/VST
$

certigraph

$ echo `vsu --show-coq-variant-path=coq-certigraph`
/home/tcarstens/.opam/coq-8.14/lib/coq/user-contrib/CertiGraph
$ echo `vsu --show-coq-variant-path=coq-certigraph-32`
/home/tcarstens/.opam/coq-8.14/lib/coq-variant/CertiGraph32/CertiGraph
$

Example: Coq runtime arguments

The --show-coq-q-arg flag prints arguments suitable for coqc, coqtop, etc. For packages which are installed to "default" locations, it silently prints nothing (allowing the default to simply work). For package variants, which are typically not installed to a "default" location, it prints the appropriate flag to set the variant path.

compcert

$ echo `vsu -Q coq-compcert`

$ echo `vsu -Q coq-compcert-32`
-Q /home/tcarstens/.opam/coq-8.14/lib/coq-variant/compcert32/compcert compcert
$

vst

$ echo `vsu -Q coq-vst`

$ echo `vsu -Q coq-vst-32`
-Q /home/tcarstens/.opam/coq-8.14/lib/coq-variant/VST32/VST VST
$

certigraph

$ echo `vsu -Q coq-certigraph`

$ echo `vsu -Q coq-certigraph-32`
-Q /home/tcarstens/.opam/coq-8.14/lib/coq-variant/CertiGraph32/CertiGraph CertiGraph
$

Example: finding tools

compcert/ccomp

$ echo `vsu --show-tool-path=coq-compcert/ccomp`
/home/tcarstens/.opam/coq-8.14/bin/ccomp
$ echo `vsu --show-tool-path=coq-compcert-32/ccomp`
/home/tcarstens/.opam/coq-8.14/variants/compcert32/bin/ccomp
$

compcert/clightgen

$ echo `vsu --show-tool-path=coq-compcert/clightgen`
/home/tcarstens/.opam/coq-8.14/bin/clightgen
$ echo `vsu --show-tool-path=coq-compcert-32/clightgen`
/home/tcarstens/.opam/coq-8.14/variants/compcert32/bin/clightgen
$

Example: show VSU package metadata path

$ echo `vsu --show-unit-metadata-path`
/home/tcarstens/.opam/coq-8.14/lib/coq-vsu/unit-metadata
$

Installing

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

Uninstalling

To remove the pin and uninstall in one step, simply run

$ opam unpin coq-vsu

Building & running without installing

$ dune exec ./src/vsu.exe -- --help