Modular Certification of Low-Level Intermediate Representation Programs

Modular certification of low-level intermediate representation (IR) programs is one of the key steps of proof-transforming compilation. The major challenges are the complexity of abstract control stacks and the lack of control flow information due to their flat nature.To tackle these challenges, we present in this paper a novel Hoare-style logic framework for modular certification of p-machine style bytecode as IR programs. This logic can fully support abstract control stacks and unstructured control flows for modular certification of IR programs involving while loops, procedure call/return, recursive procedures, and even nested procedures. It applies foundational proof-carrying code (FPCC) concepts to IR level. This system is expressive and fully mechanized. We prove its soundness and demonstrate its power by certifying the implementation of some IR programs in the Coq proof assistant. This work not only provides a solid theoretical foundation for reasoning about IR programs, but also makes an important advance toward building proof-transforming compilation environment in which certified IR code with proofs can be compiled to machine checkable proof-carrying low-level assembly code.