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

• License: Unlicense (change to your license of choice)
• Compatible Rocq versions: 9.0 or later
• Additional dependencies:
  • CompCert 3.16 or later
  • Verified Software Toolchain 2.16
• Rocq namespace: ProgramVerificationTemplate

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

opam repo add rocq-released https://rocq-prover.org/opam/released
opam install coq-vst.2.16

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

With make and the rocq makefile tool bundled with Rocq:

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

With the Dune build system, version 3.21 or later:

dune build

ccomp -o bsearch src/binary_search.c

• 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: Rocq representation of the binary search C program in CompCert's Clight language.
• theories/binary_search_theory.v: General Rocq 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 Rocq proof using the Verified Software Toolchain that the program upholds the contract.

• rocq-program-verification-template.opam: Project opam package definition, including dependencies.
• _CoqProject: File used by Rocq editors to determine the Rocq 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 Rocq, using the opam package definition.

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

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

rocq makefile and Dune builds are independent. However, for local development, it is recommended to use rocq makefile, since Rocq IDEs 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.

The Rocq 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