Skip to main content

Proof-grounded bootstrapping of a verified compiler: Producing a verified read-eval-print loop for CakeML

Ramana Kumar, Magnus O. Myreen, Scott Owens, and Yong Kiam Tan

Discussion led by Ryan Doenges on September 22, 2017

Compiler verification aims to provide strong quality guarantees about the correctness of compilers. Ultimately, compiler verification aims to remove the need to trust the compiler implementation, i.e. to remove it from the trusted computing base (TCB) of other verification projects. Previous compiler verification projects have, however, not gone far enough towards removing compilers from TCBs. The reason is that previous projects require the use of unverified software for compiling the verified compiler, and thus a significant unverified compiler is still included in the TCB. In this paper, we describe a technique, called proof-grounded bootstrapping, for reducing the TCB further. In particular, we explain how one can produce a verified machine-code implementation of a verified compiler by applying the verified compiler to itself. This self-application of the verified compiler is done with proof within the logic of the theorem prover used for verification of the compiler. We show how such a verified compiler can be packaged and used as part of a larger machine-code program. Our example is a verified implementation of a read-eval-print loop (REPL) for the source language. The TCB for this REPL implementation includes only the operating system, the hardware, and the theorem prover: assumptions about the compiler and runtime are replaced by proof. We demonstrate our technique by producing a verified REPL for CakeML, a substantial subset of Standard ML, in x86-64 machine code.