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——它是支持VCC但缺乏统一接口的先进已验证编译器CompCert的扩展。我们发现CompCertO中的CompCert Kripke逻辑关系（CKLR）为模块间演化内存状态提供了统一的内存保护概念，且具有传递可组合性。基于这种统一且可组合的CKLR，我们将CompCertO中所有编译器遍（除三个值分析遍外）的模拟关系合并为统一接口。通过将该接口应用于验证包含互递归的非平凡异构程序的组合编译，我们证明了该统一接口的简洁性与有效性。