The reference documentation extracted by coqdoc.

We describe how the plugin works under the hood.

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.

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.

You can look at our technical report for more details.

comments powered by Disqus