Verified Optimizations for Functional Languages
Report ID: TR-006-20Author: Paraskevopoulou, Zoe
Date: 2020-11-02
Pages: 174
Download Formats: |PDF|
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