27 - Proof of a program

Summary

We illustrate the use of tactical proof (semi)automation on the program shown in Figure 27.1. We compile this source program reverse.c into a C-light abstract-syntax data structure using the front end of CompCert, the clightgen utility. This produces a Coq file reverse.v with a sequence of definitions in the CompCert abstract-syntax tree structures (Figure 27.2).

Clightgen comprises CompCert's (unverified) parser into CompCert C, followed by CompCert's (verified) translation into C light. The fact that one or another of these front-end phases is unverified does not concern us, because we apply the program logic to the output of these translations. If we specify correctness properties of reverse.v and prove them, then the C light program will have those properties, regardless of whether it matches the source program reverse.c. Of course, it is very desirable for reverse.v to match reverse.c, so the programmer may reason informally about unverified properties of reverse.c such as timing, information flow, or resource consumption.

This program uses linked lists of 32-bit integers. Before proceeding with the verification, we should develop the theory of list segments (a “theory” is just what we call a collection of definitions, lemmas, and tactics useful for reasoning about the subject matter). Chapter 19 explained the theory of list segments; in the file list.v we build an lseg theory parameterized by a C structure definition.