Compositional compiler verification is a difficult problem that
focuses on separate compilation of program components with
possibly different verified compilers. Logical relations are
widely used in proving correctness of program transformations in
higher-order languages; however, they do not scale to
compositional verification of multi-pass compilers due to their
lack of transitivity. The only known technique to apply to
compositional verification of multi-pass compilers for
higher-order languages is parametric inter-language
simulations (PILS), which is
however significantly more complicated than traditional proof
techniques for compiler correctness. In this paper, we present a
novel verification framework for \emph{lightweight compositional
compiler correctness}. We demonstrate that by imposing the
additional restriction that program components are compiled by
pipelines that go through \emph{the same sequence of intermediate
representations}, logical relation proofs can be transitively
composed in order to derive an end-to-end compositional
specification for multi-pass compiler pipelines. Unlike
traditional logical-relation frameworks, our framework supports
divergence preservation—even when transformations reduce the
number of program steps. We achieve this by parameterizing our
logical relations with a pair of \emph{relational invariants}.

We apply this technique to verify a multi-pass, optimizing
middle-end pipeline for CertiCoq, a compiler from Gallina (Coq's
specification language) to C. The pipeline optimizes and
closure-converts an untyped functional intermediate language (ANF
or CPS) to a subset of that language without nested functions,
which can be easily code-generated to low-level languages.
Notably, our pipeline performs more complex closure-allocation
optimizations than the state of the art in verified compilation.
Using our novel verification framework, we prove an end-to-end
theorem for our pipeline that covers both termination and
divergence and applies to whole-program and separate compilation,
even when different modules are compiled with different
optimizations. Our results are mechanized in the Coq proof
assistant.