Conditional Contextual Refinement (CCR)

TL;DR

This paper introduces Conditional Contextual Refinement (CCR), a new refinement notion that supports full compositionality, rich contextual conditions, and full programming features, enabling modular verification from high-level code to assembly.

Contribution

It proposes CCR, a novel refinement framework that combines modularity, rich context conditions, and full programming features, formalized in Coq and integrated with CompCert.

Findings

CCR supports modular and incremental verification.

Formalization in Coq ensures rigorous correctness proofs.

Integration with CompCert enables verified compilation from high-level to assembly.

Abstract

Contextual refinement (CR) is one of the standard notions of specifying open programs. CR has two main advantages: (i) (horizontal and vertical) compositionality that allows us to decompose a large contextual refinement into many smaller ones enabling modular and incremental verification, and (ii) no restriction on programming features thereby allowing, e.g., mutually recursive, pointer-value passing, and higher-order functions. However, CR has a downside that it cannot impose conditions on the context since it quantifies over all contexts, which indeed plays a key role in support of full compositionality and programming features. In this paper, we address the problem of finding a notion of refinement that satisfies all three requirements: support of full compositionality, full (sequential) programming features, and rich conditions on the context. As a solution, we propose a new theory of refinement, called CCR (Conditional Contextual Refinement), and develop a verification framework based on it, which allows us to modularly and incrementally verify a concrete module against an abstract module under separation-logic-style pre and post conditions about external modules. It is fully formalized in Coq and provides a proof mode that combines (i) simulation reasoning about preservation of sideffects such as IO events and termination and (ii) propositional reasoning about pre and post conditions. Also, the verification results are combined with CompCert, so that we formally establish behavioral refinement from top-level abstract programs, all the way down to their assembly code.