一句话：提出可传递组合的逻辑关系验证框架，支持多趟编译器优化与分离编译，并在 Coq 中验证 CertiCoq 中端管线。
组合式编译器验证需支持由不同已验证编译器编译组件的分离编译。逻辑关系虽用于高阶语言变换证明，但缺乏传递性，难以扩展到多趟编译器；PILS 方法又过于复杂。本文提出轻量级组合式验证框架：约束组件经过相同中间表示序列，使逻辑关系证明可传递组合，得到多趟管线的端到端组合规约；并用一对关系不变量参数化逻辑关系，即使变换减少程序步数也能保持发散性。该框架用于验证 CertiCoq 的多趟优化中端管线：它把无类型函数式中间语言（ANF/CPS）优化并闭包转换，执行比已有验证编译更复杂的闭包分配优化。结果在 Coq 中机械化，证明覆盖终止与发散，适用于整体与分离编译。
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 lightweight compositional compiler correctness . We demonstrate that by imposing the additional restriction that program components are compiled by pipelines that go through 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 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.
@article{paperbot1136,
title = {Compositional optimizations for CertiCoq},
author = {Zoe Paraskevopoulou and John M. Li and Andrew W. Appel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473591}
}