Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra

Our concern is the modular development of a certified static analyzer in the Coq proof assistant. We focus on the extension of the Verified Polyhedra Library—a certified abstract domain of convex polyhedra—with a linearization procedure to handle polynomial guards. Based on ring rewriting strategies and interval arithmetic, this procedure partitions the variable space to infer precise affine terms which over-approximate polynomials. In order to help formal development, we propose a proof framework, embedded in Coq, that implements a refinement calculus. It is dedicated to the certification of parts of the analyzer—like our linearization procedure—whose correctness does not depend on the implementation of the underlying certified abstract domain. Like standard refinement calculi, it introduces data-refinement diagrams. These diagrams relate “abstract states” computed by the analyzer to “concrete states” of the input program. However, our notions of “specification” and “implementation” are exchanged w.r.t. standard uses: the “specification” (computing on “concrete states”) refines the “implementation” (computing on “abstract states”). Our stepwise refinements of specifications hide several low-level aspects of the computations on abstract domains. In particular, they ignore that the latter may use hints from external untrusted imperative oracles (e.g. a linear programming solver). Moreover, refinement proofs are naturally simplified thanks to computations of weakest preconditions. Using our refinement calculus, we elegantly define our partitioning procedure with a continuation-passing style, thus avoiding an explicit datatype of partitions. This illustrates that our framework is convenient to prove the correctness of such higher-order imperative computations on abstract domains.