Verified Optimizations for Functional Languages

Abstract:

Coq is one of the most widely adopted proof development systems. It allows programmers to write purely functional programs and verify them against specifications
with machine-checked proofs. After verification, one can use Coq’s extraction plugin to obtain a program (in OCaml, Haskell, or Scheme) that can be compiled and
executed. However, bugs in either the extraction function or the compiler of the
extraction language may cause the executable to exhibit unexpected behaviors, rendering source-level verification futile.
A verified compiler is a compiler whose output provably preserves the semantics
of the source language. CertiCoq is a verified compiler, currently under development,
for Coq’s specification language, Gallina. CertiCoq targets Clight, a subset of the
C language, that can be compiled with the CompCert verified compiler to obtain a
certified executable, bridging the gap between the formally verified source program
and the compiled target program.
In this thesis, I present the implementation and verification of CertiCoq’s optimizing middle-end pipeline. CertiCoq’s middle end consists of seven different transformations and is responsible for efficiently compiling an untyped purely functional
intermediate language to a subset of the same language, which can be readily compiled to a first-order, low-level intermediate language. CertiCoq’s middle-end pipeline
performs crucial optimizations for functional languages including closure conversion,
uncurrying, shrink-reductions and inlining. It advances the state of the art of verified optimizing compilers for functional languages by implementing more efficient
closure-allocation strategies.
For proving CertiCoq correct, I develop a framework based on the technique of
logical relations, making novel technical contributions. I extend logical relations with
notions of relational preconditions and postconditions that facilitate reasoning about
the resource consumption of programs simultaneously with functional correctness. I
demonstrate how this enables reasoning about preservation of non-terminating behaviors, which is not supported by traditional logical relations. Moreover, I develop
a novel, lightweight technique that allows logical-relation proofs to be composed in
order to obtain a top-level compositional compiler correctness theorem. This technique is used to obtain a separate compilation theorem that guarantees that programs
compiled separately through CertiCoq, perhaps using different sets of optimizations,
can be safely linked at the target level. Lastly, I use the framework to prove that
CertiCoq’s closure conversion is not only functionally correct but also safe for time
and space, meaning that it is guaranteed to preserve the asymptotic time and space
complexity of the source program