Documentation

Library

The reference documentation extracted by coqdoc.

How it works

We describe how the plugin works under the hood.

Effects and extraction

We define a monad to encode effects in Coq. This monad combines states, exceptions, non-termination and printing in a classical way. Here is its definition:

Definition M (sig : Sig.t) (A : Type) :=
    State.t sig → (A + string) × State.t sig.
with:
Record State.t (sig : Sig.t) := Make {
    NbSteps : nat;
    InputMem : Mem.t (Sig.input_mem_sig sig);
    TmpMem : Mem.t (Sig.tmp_mem_sig sig);
    Output : list Dynamic.t }.

For non-termination we use the counter NbSteps to bound the fixpoints. We print debugging informations in Output. The memory is divided into two parts: InputMem and TmpMem, both specified by a sig which is the list of types which can appear in the heap. We prefer to make this list explicit because the strong typing policy of Coq makes it hard to have a type-agnostic heap, and because most decision procedures only allocate values using a finite number of types.

The monad provides the basic operations you would expect, such as:

try sig A (x : unit → M sig A) (handler : string → M sig A) : M sig A
fix_ sig A B (F : (A → M sig B) → A → M sig B) : A → M sig B
write sig T (ref : Ref.t sig T) (value : T) : M sig unit
print_string sig (msg : string) : M sig unit

Decision procedures written in the monad are extracted to OCaml to be executed efficiently. Since OCaml already provides all these effects, we tune the extraction mechanism to extract the monad to the identity monad and the basic operations to their OCaml equivalents.

Communication from OCaml to Coq

The generated OCaml code is instrumented to compute a prophecy p. By default, this prophecy only contains the number nb_steps used to run the non-termination monad in Coq being sure to complete. It is computed incrementing a counter every time we enter a fixpoint. We then have a lemma:

Lemma proof_by_reflection sig A (x : M sig A) (p : Prophecy.t sig)
  : is_computable x p = true → A.
which returns an element in A from a computation x in M sig A given a witness that the computation is successful. This witness is a proof that x reduces to something:
Definition is_computable sig A (x : M sig A) (p : Prophecy.t sig) : bool :=
  match prophecy_run x p with
  | (inl _, _) ⇒ true
  | (inr _, _) ⇒ false
  end.

Obviously the evaluation of prophecy_run in Coq can be really slow since we use an explicit encoding of effects, and to have the right nb_steps from OCaml is a little gain. To pre-compute complex results in OCaml and pass them to Coq in the prophecy we combine two elements: the input memory and the select operator:

select (T : Type) (f g : unit → T) : T

The command select f g executes f in Coq but g in OCaml. This is the basic construct to permit to change the extraction to OCaml. The input memory has the nice property to be saved and serialized in the prophecy after the execution of the OCaml code, and is given as an initialization value to Coq. The only constrain is to use types implementing the Reifiable.t interface:

Record Reifiable.t (T : Type) : Type := New {
    Export : T → SExpr.t;
    Import : SExpr.t → T}.

This interface explains how to serialize and deserialize a value to a binary tree SExpr.t. It can be done for common data structures, such as integers or lists, but not for abstractions or proofs. A common pattern is then to do a:

let r := input_ref sig i init in
do! select (fun _ ⇒ ret tt) (fun _ ⇒ r :=! some complex computations...) in
let! x := !r in
...

The OCaml run does the complex computations and save the result to the reference r which is read in x. The result is serialized in the prophecy and the Coq run can directly read r without re-doing the computations.

An important use case is the backtracking, often used in decision procedures algorithms. The exploration of the space can be done in OCaml saving the successful path in the input memory. Since Coq does not have to do the exploration anymore, the gain can be exponential in time. An other use case is the implementation of provers as unsafe external OCaml plugins generating a Coq certificate. You can simply use our plugin for the extraction and serialization instead of writing OCaml code and all the infrastructure to communicate from OCaml to Coq.

Research papers

You can look at our technical report for more details.

comments powered by Disqus