Verified Compiler Optimisations

Abstract

This thesis explores how to formally verify the correctness of a certifying compiler where the correctness of individual compiler runs is specified by translation relations, each of which characterises the admissible behaviour of a single compiler pass. Whereas the correctness of compiler passes follows from the fact that we can recognise compiler behaviour, there is no guarantee that the recognised behaviour is correct. This motivates the need for formal guarantees that express that translation relations themselves are well-behaved.

We use the Coq Proof Assistant to demonstrate how we can prove that a well-behaved translation relation preserves the static and dynamic semantics of programs. In a preliminary study, we show positive results in the context of a simply typed lambda calculus: we define static and dynamic semantics preservation, and we prove both properties for several example translation relations. The main takeaway of this study is that we can use logical relations to express and prove dynamic semantics preservation.

The preliminary study serves as a starting point for scaling up our methods to a more complex lambda calculus that is based on System 𝐹𝜔𝜇. Though the proof method for dynamic semantics preservation does not scale up easily, we research and demonstrate how step-indexed logical relations solve the issues that arise such that we can define and prove dynamic semantics preservation. Furthermore, we prove static and dynamic semantics preservation for a realistic translation relation.

The semantics preservation proof method is developed for use in a certification engine for the Plutus Tx compiler: a smart contract language compiler intended for commercial use that is developed and maintained by IOHK. As such, we show a promising proof method that can be applied in realistic compilers and verification tools.