This repository contains the current development state of a new verified extraction from Coq to OCaml, based on MetaCoq.
Technically, the extraction targets Malfunction, which is a specification of Lambda, the internal language of the OCaml compiler.
We use Malfunction as target for extraction from Coq, and rely on the Malfunction and OCaml compilers to obtain .cmx
files that will behave like .cmx
files created by Coq's current extraction process and the Ocaml compiler.
In particular, Coq programs extracted like this can interact with other OCaml programs and with Coq programs extracted using the existing extraction.
The implementation of extraction is fully functional and supports primitive integers and floats, but no cofixpoints yet. Verification is work in progress.
opam switch create coq-malfunction --packages="ocaml-variants.4.14.1+options,ocaml-option-flambda"
eval $(opam env --switch=coq-malfunction)
opam repo add coq-released https://coq.inria.fr/opam/released
opam pin -n -y "https://github.com/MetaCoq/metacoq.git#v1.3.1-8.19"
opam pin -n -y "https://github.com/stedolan/malfunction.git#master"
opam install . --deps-only
make -j 4
After From VerifiedExtraction Require Import Extraction.
the commands Verified Extraction <definition>
and Verified Extraction <definition> "<file>.mlf"
can be used to run the new extraction process.
Multiple functions can be extracted at the same time with Verified Extraction (<d1>,<d2>,...)
.
To add an mli
file one can add the output of the (unverified) generator MetaCoq Run Print mli <definition>.
to a .mli
file.
- the
theories
directory contains the Coq files with implementation and verification of the pluginMalfunction.v
contains the syntax definition of Malfunction. It is a direct, line-to-line port of the OCaml filemalfunction.ml
to Coq.SemanticsSpec.v
defines an inductive big-step evaluation predicate.Compile.v
defines a compilation function of lambda box to Malfunction.CompileCorrect.v
proves the correctness of this function, using the correctness proof of case analysis inMcase.v
Interpreter.v
contains an interpretation function, which is close tomalfunction_interpreter.ml
, and a proof that values according to the evaluation predicate are also found by the interpreter. Note that since the interpreter is not necessarily terminating we switch of Coq's termination checker, meaning this proof can only be seen as a sanity check.Serialize.v
contains seralization functions into s-expressions. There is also a parser inDeserialize.v
, used for testing.Pipeline.v
composes the full extraction pipeline from Coq to MalfunctionPipelineCorrect.v
composes the correctness proof of the extraction pipelineFirstorder.v
derives interoperability results for first-order functions
- the
plugin
directory contains the code of the extraction plugin extracted using Coq's OCaml extraction viatheories/Extraction.v
. This is packaged into an intermediate extraction plugin. - the
plugin/plugin-bootstrap
directory contains the code of the extraction plugin extracted using the intermediate extraction plugin. This is packaged into the final verified extraction plugin. - the
examples
directory contains various examples how to use the new verified extraction plugin. - the
benchmarks
directory allows re-producing benchmarks from the paper.
The project is developed by Yannick Forster, Matthieu Sozeau, Pierre-Marie Pédrot, and Nicolas Tabareau.
Copyright (c) 2022--2024 Yannick Forster, Matthieu Sozeau, Nicolas Tabareau