Translation certification for smart contracts

Compiler correctness is an old problem, but with the emergence of smart contracts on blockchains that problem presents itself in a new light. Smart contracts are self-contained pieces of software that control (valuable) assets in an adversarial environment; once committed to the blockchain, these smart contracts cannot be modified. Smart contracts are typically developed in a high-level contract language and compiled to low-level virtual machine code before being committed to the blockchain. For a smart contract user to trust a given piece of low-level code on the blockchain, they must convince themselves that (a) they are in possession of the matching source code and (b) that the compiler has correctly translated the source code to the given low-level code. Classic approaches to compiler correctness tackle the second point. We argue that translation certification also squarely addresses the first. We describe the proof architecture of a translation certification framework and demonstrate how we can model the compilation pipeline as a sequence of translation relations. We give a detailed account of such relations for most passes of the Plutus Tx compiler, which we formalised in Coq. This approach facilitates a modular verification methodology and is robust in the face of an evolving compiler implementation.