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

• Author(s):
  • Karl Palmskog
• License: MIT License
• Compatible Coq versions: 8.14 or later
• Additional dependencies:
  • CompCert 3.11
  • Verified Software Toolchain 2.10 or later
• Coq namespace: ProgramVerificationTemplate

Building instructions

Installing dependencies

The recommended way to install Coq and other dependencies is via OPAM, for example:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq.8.15.2 coq-compcert.3.11 coq-vst.2.11

Obtaining the project

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

Option 1: building the project using coq_makefile

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

Option 2: building the project using Dune

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, adapted from 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.
• theories/binary_search_verif.v: Contract for the C 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 IDEs to determine the Coq logical path, and by the Make-based build to obtain the list of files to include.
• .github/workflows/coq-ci.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 IDEs may not be able find files compiled by Dune. Due to its build hygiene requirements, Dune will refuse to build when compiled (.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