Foreign Function Verification Through Metaprogramming

Abstract

CertiCoq is a compiler from Coq to C that is verified in Coq. Thanks to CertiCoq’s mechanically checked proof of compiler correctness, users can be sure that programs they write and verify in Coq’s rich type system output the same results when compiled to C (and to machine language, via the CompCert verified compiler). However, in practice, large programs are rarely written in a single language; additional languages are used for better performance or for capabilities that the primary language lacks. In particular, because Coq lacks user-defined primitive types, mutation, and input/output actions, CertiCoq-compiled code must interact with another language to have those capabilities. Specifically, Coq code must be able to call C code and C code must be able to inspect and generate Coq values and call Coq code. But what happens to the correctness proofs when these two languages interact? A foreign C function has to be memory-safe, return the expected result, and have only the expected side effect. A specification that expresses these requirements must combine plain Coq, for the functional parts, and a program logic for C (such as the Verified Software Toolchain [VST]), for the verification of C functions. While VST is embedded in Coq, its specification language is quite different. VST proofs about C foreign functions do not directly translate to proofs about Coq primitives either. Bridging this gap by connecting plain Coq and VST theorems requires a system of techniques and methods, many of which are made feasible by using metaprogramming as a general methodological approach. In this dissertation, I describe these techniques and methods. Using these methods, the user can relate foreign functions and types to their functional models, generate VST specifications about the foreign C functions, and write plain Coq proofs about the Coq counterparts of the foreign functions. I also provide examples of Coq programs with primitive types, mutation, and I/O actions, along with specifications and proofs about these programs, to demonstrate VeriFFI, the verified foreign function interface for CertiCoq.