Room 206 (2nd floor, badged access)
17 June 2024 - 14h00
Toward a FFI (Foreign Function Interface) for embedding untrusted imperative OCaml into Coq-verified computations.
by Sylvain BOULME from Verimag, Grenoble-INP Ensimag
Abstract: The naive embedding of imperative OCaml functions as Coq functions with linking at extraction is unsound. A famous example of such an unsound embedding is the register allocator of CompCert. In the case of CompCert, we can reasonably argue that this unsoundness should not produce a bug, but this is quite inconvenient.
Alternatively, I conjecture that a given embedding of imperative OCaml functions into Coq through May-Return monads is sound for partial correctness. This embedding considers foreign functions as nondeterministic untrusted oracles: the formal proofs only consider their ML type, but never their side-effects nor other functional properties. This gives a lightweight approach – combining Coq and OCaml typecheckers – for formally verified programming, where complex computations are delegated to an efficient but untrusted imperative oracle, and where the proof effort is focused on a defensive validator of their results.
Actually, the embedding of polymorphic higher-order OCaml oracles is quite expressive. Through parametric reasoning (i.e. theorems for free à la Wadler), it extends Coq with exception raising, a limited form of exception-handling, generic memoized recursion, etc. Moreover, this enables a design pattern--for certificate producing oracles--called Polymorphic LCF Style (or Polymorphic Factory Style). In this style, each oracle is parametrized by a formally verified API that enables the oracle to produced directly formally verified results for free. This FFI has been applied on several realistic applications: in optimizing compilation with Chamois CompCert, in static analysis (abstract domain of convex polyhedra with VPL) and in automated deduction (Boolean SAT-solving with SatAnsCert).
The talk will detail this OCaml>>=Coq binding, its limits and possible improvements. Formalizing it (e.g. in MetaCoq) seems a great challenge.
Séminaire dans le cadre de la visite de M. Sozeau et Y. Forster à Verimag.
