A template for organizing a Coq program verification project

Using Coq
1

Inspired by Emilio Gallego’s guide and repo for developing Coq plugins, I created a template repository showing how one can organize a Coq program verification project according to current best practices, using Coq 8.12:

To go marginally above the toy example level, the project verifies a classic program in C using the Verified Software Toolchain (VST). When compiled with CompCert, the program’s contract - briefly explained below - is therefore guaranteed to hold down to machine code level (under reasonable assumptions).

The project uses continuous integration (CI) on GitHub made possible by recent packaging of CompCert and VST by @MSoegtropIMC and the Coq Docker Action by @erikmd. The project can be built using either coq_makefile or Dune, at the developer’s discretion; CI uses Dune.

The key C function is as follows, adapted from Joshua Bloch’s Java version:

int binary_search(int a[], int len, int key) {
  int low = 0;
  int high = len - 1;

  while (low <= high) {
    int mid = ((unsigned int)low + (unsigned int)high) >> 1;
    int mid_val = a[mid];
    if (mid_val < key)
      low = mid + 1;
    else if (mid_val > key)
      high = mid - 1;
    else
      return mid;
  }
  return -low - 1;
}

The Coq contract for the function follows the informal contract in the Java standard library API closely. More specifically, the array a (Coq integer list) is assumed to be sorted, and the output is either the array index of some element with value equal to the parameter key, or an “insertion point” where such an element would have appeared.

Feedback on the template is welcome, either here or as issues on GitHub.

5 Likes