Verified compositional compilation (VCC) is a notion of modular verification of compilers that supports compilation of heterogeneous programs. The key to achieve VCC is to design a semantic interface that enables composition of correctness theorems for compiling individual modules. Most of the existing techniques for VCC fix a semantic interface from the very beginning and force it down to every single compiler pass. This requires significant changes to the existing framework and makes it difficult to understand the relationship between conditions enforced by the semantic interface and the actual requirements of compiler passes. A different approach is to design appropriate semantic interfaces for individual compiler passes and combine them into a unified interface which faithfully reflects the requirements of underlying compiler passes. However, this requires vertically composable simulation relations, which were traditionally considered very difficult to construct even with extensive changes to compiler verification frameworks. We propose a solution to construction of unified semantic interfaces for VCC with a bottom-up approach. Our starting point is CompCertO, an extension of CompCert -- the state-of-the-art verified compiler -- that supports VCC but lacks a unified interface. We discover that a CompCert Kripke Logical Relation (CKLR) in CompCertO provides a uniform notion of memory protection for evolving memory states across modules and is transitively composable. Based on this uniform and composable CKLR, we then merge the simulation relations for all the compiler pass in CompCertO (except for three value analysis passes) into a unified interface. We demonstrate the conciseness and effectiveness of this unified interface by applying it to verify the compositional compilation of a non-trivial heterogeneous program with mutual recursion.

翻译：验证性组合编译（VCC）是一种支持异构程序编译的模块化编译器验证概念。实现VCC的关键在于设计一种语义接口，使得各模块编译的正确性定理能够组合。现有的大多数VCC技术从一开始就固定一种语义接口，并将其强制应用于每个编译器遍。这需要对现有框架进行重大修改，且难以理解语义接口所施加的条件与编译器遍实际需求之间的关系。另一种方法是为各个编译器遍设计合适的语义接口，并将其组合成一个统一的接口，该接口能够忠实地反映底层编译器遍的需求。然而，这需要垂直可组合的模拟关系，传统上即使对编译器验证框架进行大量修改，此类关系也被认为极难构造。我们提出了一种通过自底向上方法构造VCC统一语义接口的解决方案。我们的起点是CompCertO——它是对最先进的已验证编译器CompCert的扩展，支持VCC但缺乏统一接口。我们发现CompCertO中的CompCert克里普克逻辑关系（CKLR）为跨模块的演化内存状态提供了一种统一的内存保护概念，且具有可传递的组合性。基于这种统一且可组合的CKLR，我们将CompCertO中所有编译器遍（除三个值分析遍外）的模拟关系合并为一个统一的接口。我们通过将该接口应用于验证一个包含相互递归的非平凡异构程序的组合编译，展示了该统一接口的简洁性和有效性。