Technical Articles / Opinions / News / Projects

coqffi in a Nutshell

For each entry of a cmi file, coqffi tries to generate an equivalent (from the extraction mechanism perspective) Coq definition. In this article, we walk through how coqffi works.

Note that we do not dive into the vernacular commands coqffi generates. They are of no concern for users of coqffi.

Revisions

This revisions table has been automatically generated from the git history of this website repository, and the change descriptions may not always be as useful as they should.

You can consult the source of this file in its current version here.

2020-12-10 Spellchecking and revisions table for the coqffi articles 9098a01
2020-12-10 Add a Series on coqffi, and the first literate program of this blog 2706544

1 Getting Started

1.1 Requirements

The latest version of coqffi (1.0.0~beta2 at the time of writing) is compatible with OCaml 4.08 up to 4.11, and Coq 8.12. If you want to use coqffi, but have incompatible requirements of your own, feel free to submit an issue.

1.2 Installing coqffi

The recommended way to install coqffi is through the Opam Coq Archive, in the released repository. If you haven’t activated this repository yet, you can use the following bash command. 

opam repo add coq-released https://coq.inria.fr/opam/released

Then, installing coqffi is as simple as 

opam install coq-coqffi

You can also get the source from the upstream git repository. The README provides the necessary pieces of information to build it from source.

1.3 Additional Dependencies

One major difference between Coq and OCaml is that the former is pure, while the latter is not. Impurity can be modeled in pure languages, and Coq does not lack of frameworks in this respect. coqffi currently supports two of them: coq-simple-io and FreeSpec. It is also possible to use it with Interaction Trees, albeit in a less direct manner.

2 Primitive Types

coqffi supports a set of primitive types, i.e., a set of OCaml types for which it knows an equivalent type in Coq. The list is the following (the Coq types are fully qualified in the table, but not in the generated Coq module as the necessary Import statement are generated too).

OCaml type Coq type
bool Coq.Init.Datatypes.bool
char Coq.Strings.Ascii.ascii
int CoqFFI.Data.Int.i63
'a list Coq.Init.Datatypes.list a
'a option Coq.Init.Datatypes.option a
string Coq.Strings.String.string
unit Coq.Init.Datatypes.unit

The i63 type is introduced by the CoqFFI theory to provide signed primitive integers to Coq users. They are implemented on top of the (sadly unsigned) Coq native integers introduced in Coq 8.10. Hopefully, the i63 type will be deprecated once signed primitive integers find their way to Coq upstream.

When processing the entries of a given interface model, coqffi will check that they only use these types, or types introduced by the interface module itself.

3 Code Generation

coqffi distinguishes three types of entries: types, pure functions, and impure primitives. We now discuss how each one of them is handled.

3.1 Types

By default, coqffi generates axiomatized definitions for each type defined in a .cmi file. This means that type t becomes Axiom t : Type. Polymorphism is supported, i.e., type 'a t becomes Axiom t : forall (a : Type), Type.

It is possible to provide a “model” for a type using the coq_model annotation, for instance for reasoning purposes. For instance, we can specify that a type is equivalent to a list. 

type 'a t [@@coq_model "list"]

This generates the following Coq definition. 

Definition t : forall (a : Type), Type := list.

It is important to be careful when using the coq_model annotation. More precisely, the fact that t is a list in the “Coq universe” shall not be used while the implementation phase, only the verification phase.

Finally, coqffi has got an experimental feature called transparent-types (enable by using the -ftransparent-types command-line argument). If the type definition is given in the module interface, then coqffi tries to generates an equivalent definition in Coq. For instance, 

type 'a llist =
  | LCons of 'a * (unit -> 'a llist)
  | LNil

becomes 

Inductive llist (a : Type) : Type :=
| LCons (x0 : a) (x1 : unit -> llist a) : llist a
| LNil : llist a.

Mutually recursive types are supported, so 

type even = Zero | ESucc of odd
and odd = OSucc of even

becomes 

Inductive odd : Type :=
| OSucc (x0 : even) : odd
with even : Type :=
| Zero : even
| ESucc (x0 : odd) : even.

The transparent-types feature is experimental, and is currently limited to variant types. It notably does not support records. Besides, it may generate incorrect Coq types, because it does not check whether or not the positivity condition is satisfied.

3.2 Pure Functions

coqffi assumes OCaml values are pure by default, and will generate regular axiomatized Coq definitions for them. Similarly to type entries, it is possible to provide a Coq model using the coq_module annotation. 

val unpack : string -> (char * string) option

becomes 

Axiom unpack : string -> option (ascii * string).

Polymorphic functions are supported. 

val map : ('a -> 'b) -> 'a list -> 'b list

becomes 

Axiom map : forall (a : Type) (b : Type), (a -> b) -> list a -> list b.

3.3 Impure Primitives

Finally, coqffi reserves a special treatment for OCaml value explicitly marked as impure, using the impure annotation. Impurity is usually handled in pure programming languages by means of monads, and coqffi is no exception to the rule.

Given the set of impure primitives declared in an interface module, coqffi will (1) generates a typeclass which gathers these primitives, and (2) generates instances of this typeclass for supported backends.

We illustrate the rest of this section with the following impure primitives. 

val echo : string -> unit [@@impure]
val scan : unit -> string [@@impure]

where echo allows writing something the standard output, and scan to read the standard input.

Assuming the processed module interface is named console.mli, the following Coq typeclass is generated. 

Class MonadConsole (m : Type -> Type) := { echo : string -> m unit
                                         ; scan : unit -> m string
                                         }.

Using this typeclass and with the additional support of an additional Monad typeclass, we can specify impure computations which interacts with the console. For instance, with the support of ExtLib, one can write. 

Definition pipe `{Monad m, MonadConsole m} : m unit :=
  let* msg := scan () in
  echo msg.

There is no canonical way to model impurity in Coq, but over the years several frameworks have been released to tackle this challenge.

coqffi provides three features related to impure primitives.

3.3.1 simple-io

When this feature is enabled, coqffi generates an instance of the typeclass for the IO monad introduced in the coq-simple-io package 

Axiom io_echo : string -> IO unit.
Axiom io_scan : unit -> IO string.

Instance IO_MonadConsole : MonadConsole IO := { echo := io_echo
                                              ; scan := io_scan
                                              }.

It is enabled by default, but can be disabled using the -fno-simple-io command-line argument.

3.3.2 interface

When this feature is enabled, coqffi generates an inductive type which describes the set of primitives available, to be used with frameworks like FreeSpec or Interactions Trees 

Inductive CONSOLE : Type -> Type :=
| Echo : string -> CONSOLE unit
| Scan : unit -> CONSOLE string.

Definition inj_echo `{Inject CONSOLE m} (x0 : string) : m unit :=
  inject (Echo x0).

Definition inj_scan `{Inject CONSOLE m} (x0 : unit) : m string :=
  inject (Scan x0).

Instance Inject_MonadConsole `{Inject CONSOLE m} : MonadConsole m :=
  { echo := inj_echo
  ; scan := inj_scan
  }.

Providing an instance of the form forall i, Inject i M is enough for your monad M to be compatible with this feature (see for instance how FreeSpec implements it).

3.3.3 freespec

When this feature in enabled, coqffi generates a semantics for the inductive type generated by the interface feature. 

Axiom unsafe_echo : string -> unit.
Axiom unsafe_scan : uint -> string.

Definition console_unsafe_semantics : semantics CONSOLE :=
  bootstrap (fun a e =>
    local match e in CONSOLE a return a with
          | Echo x0 => unsafe_echo x0
          | Scan x0 => unsafe_scan x0
          end).

4 Moving Forward

coqffi comes with a comprehensive man page. In addition, the interested reader can proceed to the next article of this series, which explains how coqffi can be used to easily implement an echo server in Coq.