  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 assets, which are
often of high financial value, in an adversarial environment and, once
committed to the blockchain, they cannot be changed anymore. 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 faithfully translated the source code's
semantics.
  Classic approaches to compiler correctness tackle the second point. We argue
that translation certification also addresses the first. We describe the proof
architecture of a novel translation certification framework, implemented in
Coq, for a functional smart contract language. We demonstrate that we can model
the compilation pipeline as a sequence of translation relations that facilitate
a modular proof approach and are robust in the face of an evolving compiler
implementation.
