Formally Verified Defensive Programming
(efficient Coq-verified computations from untrusted ML oracles)
[ HAL | pdf | slides | video ]

Publicly defended in hybrid mode on September 27, 2021 in front of the following jury

• Reviewers
  • Andrew W. Appel, Professor at Princeton University
  • Sandrine Blazy, Professeur à l’Université de Rennes 1
  • Greg Morrisett, Professor, Dean of Cornell Tech
• Examiners
  • Hugo Herbelin, Directeur de Recherche à l’Inria
  • Xavier Leroy, Professeur au Collège de France
• Chair (Président) Jean-François Monin, Professeur à l'UGA

Un résumé "grand public" d'une partie du manuscrit a été publiée en 2024 sous le titre Construire des logiciels fiables dans la revue Interstices.

This document presents a lightweight approach – combining Coq and OCaml typecheckers – in order to formally verify higher-order imperative programs for partial correctness. In this approach, called FVDP (Formally Verified Defensive Programming), Coq-verified programs also contain some OCaml written functions, called oracles, which are untrusted: their implementation is simply ignored by the formal proof. Formal guarantees on the results of these oracles are obtained by combining dynamic tests in Coq with static properties deduced from OCaml types.

Indeed, the simplest way to obtain a Coq-verified solver for a complex problem, often consists in combining an efficient OCaml oracle searching for "good" solutions with a verified defensive test able to ensure that the results found by the oracle have the expected properties. Hence, the solver benefits from the powerful imperative feature of OCaml, while hiding many complex details of its computation process to its formal proof: the theory of the defensive test is usually much simpler than the one of the oracle.

The embedding of OCaml oracles into Coq is realized through a “may-return monad”, a structure that abstracts their side-effects by representing them as non-deterministic functions, and provided by the Impure library. This library also provides a very simple embedding of OCaml pointer equality, but powerful enough for defensive checks of some memoizing oracles (e.g. hash-consing of terms, memoized recursion). The document also shows how to deduce expressive invariants from the static OCaml type of polymorphic oracles, by adapting Wadler's “theorems for free” (based on Reynold's parametric polymorphism). This technique is exploited within a design pattern—for certificate producing oracles—called Polymorphic LCF Style (or Polymorphic Factory Style).

Large Coq proofs on these higher-order impure defensive computations are decomposed thanks to data-refinement techniques in order to cleanly separate reasoning on pure data-structures and algorithms from reasonings on sequences of impure computations. Then, the latter are (semi)automated thanks to computations of weakest liberal preconditions.

FVDP is detailed on several “realistic” applications: in optimizing compilation (instruction scheduling with CompCert-KVX), in static analysis (abstract domain of convex polyhedra with VPL) and in automated deduction (Boolean SAT-solving with SatAnsCert and linear rational arithmetic with VplTactic). The document explains how FVDP, instantiated with a careful software design, both alleviates development times and running times of such formally verified applications.