Coq Program Verification Template

Template project for program verification in Coq. Uses the Verified Software Toolchain and a classic binary search program in C as an example.

Meta

• License: Unlicense (change to your license of choice)
• Compatible Coq versions: 8.14 or later
• Additional dependencies:
  • CompCert 3.12 or later
  • Verified Software Toolchain 2.12 or later
• Coq namespace: ProgramVerificationTemplate

Building instructions

Installing dependencies

The recommended way to install Coq and other dependencies is via the Coq Platform. To install dependencies manually via opam:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq.8.16.1 coq-compcert.3.12 coq-vst.2.12

Obtaining the project

git clone https://github.com/coq-community/coq-program-verification-template.git
cd coq-program-verification-template

Option 1: building the project using coq_makefile

With make and the coq_makefile tool bundled with Coq:

make   # or make -j <number-of-cores-on-your-machine> 

Option 2: building the project using Dune

With the Dune build system, version 3.8.1 or later:

dune build

Compiling the program using CompCert (optional)

ccomp -o bsearch src/binary_search.c

File and directory structure

Core files

• src/binary_search.c: C program that performs binary search in a sorted array, inspired by Joshua Bloch's Java version.
• theories/binary_search.v: Coq representation of the binary search C program in CompCert's Clight language.
• theories/binary_search_theory.v: General Coq definitions and facts relevant to binary search, adapted from code in the Verified Software Toolchain.
• theories/binary_search_verif.v: Contract for the Clight program following the Java specification and a Coq proof using the Verified Software Toolchain that the program upholds the contract.

General configuration

• coq-program-verification-template.opam: Project opam package definition, including dependencies.
• _CoqProject: File used by Coq editors to determine the Coq logical path, and by the make-based build to obtain the list of files to include.
• .github/workflows/docker-action.yml: GitHub Actions continuous integration configuration for Coq, using the opam package definition.

Make configuration

• Makefile: Generic delegating makefile using coq_makefile.
• Makefile.coq.local: Custom optional Make tasks, including compilation of the C program.

Dune configuration

• dune-project: General configuration for the Dune build system.
• theories/dune: Dune build configuration for Coq.

Caveats

coq_makefile vs. Dune

coq_makefile and Dune builds are independent. However, for local development, it is recommended to use coq_makefile, since Coq editors may not be able find files compiled by Dune. Due to its build hygiene requirements, Dune will refuse to build when binary (.vo) files are present in theories; run make clean to remove them.

Generating Clight for Coq

The Coq representation of the C program (binary_search.v) is kept in version control due to licensing concerns for CompCert's clightgen tool. If you have a license to use clightgen, you can delete the generated file and have the build system regenerate it. To regenerate the file manually, you need to run:

clightgen -o theories/binary_search.v -normalize src/binary_search.c