Cookbook

Here we list typical situations where we need to change the OCaml source code so that the translated code compiles in Coq.

Abstractions in `.mli` files

When generating the Coq code, we do not use the notion of .mli because there are no such interface files in Coq. So the typical setup is to generate a .v file for each .ml file, and only translate the .mli files of the external dependencies to axiom files.

An issue in this process is that there can be differences between what a .v file sees and what a .ml file was seeing. For example, let us say that we have the following files:

a.ml:

module type S = sig
  val pub : int -> int
end

module type S_internal = sig
  val pub : int -> int
  val priv : int -> int
end

module M : S_internal = struct
  let pub x = x + 1
  let priv x = x - 1
end

a.mli:

module type S = sig
  val pub : int -> int
end

module M : S

b.ml:

let f x = A.M.pub x

Then from the point of view of b.ml, A.M is of signature A.S and there are no ways to know about A.S_internal. However, in Coq, since we did not translate the .mli file, A.M appears as having the signature S_internal. Since we translate signatures to records, which do not have the notion of inclusion, A.M does not have the same type in Coq and OCaml. This can introduce bugs when we translate a signature annotation S to Coq, as Coq expects a signature S_internal.

A solution for this issue is to open the abstraction in a.mli by using the signature S_internal instead of S. A general solution on the side of coq-of-ocaml would be to translate the .mli to .v files doing the plumbing from S to S_internal. We have not done that yet, because of lack of time and because we believe that having .v files to do plumbing can also have a cost for the proofs.

Fixpoint struct annotations

In Coq, fixpoints (recursive functions) must be structurally decreasing on one of the arguments to make sure that the function always terminates. When structural termination is not obvious, we can disable this check with the configuration option without_guard_checking. However, Coq still requires to consider one of the parameters as the decreasing one, even if this is not structurally the case. A decreasing parameter is still required to know how far to unfold recursive definitions while doing proofs.

The way to specify the decreasing parameter is to use the attribute coq_struct. For example we annotate the operator --> as follows:

let[@coq_struct "i"] rec ( --> ) i j =
  (* [i; i+1; ...; j] *)
  if Compare.Int.(i > j) then [] else i :: (succ i --> j)

Here i is decreasing when we consider the natural order on -i. This generates the following Coq code:

Fixpoint op_minusminusgt (i : int) (j : int) {struct i} : list int :=
  if i >i j then
    nil
  else
    cons i (op_minusminusgt (Pervasives.succ i) j).

The annotation {struct i} specifies in Coq that the decreasing parameter is i.

Ignored functions

Sometimes definitions are too complex to translate to Coq, but we still want to go on with the rest of the files. A solution is to add the coq_axiom_with_reason to ignore a definition and replace it with an axiom of the same type.

For example, the following definition would not work in Coq as is it is, due to the use of GADTs:

  let fold_all f set acc =
    List.fold_left
      (fun acc (_, Ex_Kind kind) -> fold kind (f.f kind) set acc)
      acc
      all

We then add the attribute @coq_axiom_with_reason:

let fold_all f set acc =
    List.fold_left
      (fun acc (_, Ex_Kind kind) -> fold kind (f.f kind) set acc)
      acc
      all
    [@@coq_axiom_with_reason "gadt"]

This generates the following Coq code:

Axiom fold_all : forall {A : Set}, fold_f A -> t -> A -> A.

which compiles and has the right type, even if we lost the translation of the body of fold_all. With this attribute we must add a reason, so that we document we chose to introduce an axiom. Among frequent reasons are the use of GADTs and complex recursive functions.

Mutual definitions as notations

Sometimes mutual definitions for a recursive function are used more as notations rather than to express a true mutual recursion. See the attribute coq_mutual_as_notation for more details about how to handle this kind of definition. Here is an example where this attribute is needed:

let rec double_list l =
  match l with
  | [] -> l
  | n :: l -> double n :: double_list l

and[@coq_mutual_as_notation] double n = 2 * n

which translates in Coq to:

Reserved Notation "'double".

Fixpoint double_list (l : list int) : list int :=
  let double := 'double in
  match l with
  | [] => l
  | cons n l => cons (double n) (double_list l)
  end

where "'double" := (fun (n : int) => Z.mul 2 n).

Definition double := 'double.

Named signatures

We translate modules used in functors as records in Coq. We require a name for the signatures to have a name for the corresponding records. Sometimes, in OCaml, when a signature is used just once it is inlined and not named. Here is an example of code with an anonymous signature for the return signature of the functor Make_indexed_carbonated_data_storage:

module Make_indexed_carbonated_data_storage
    (C : Raw_context.T)
    (I : INDEX)
    (V : VALUE) : sig
  include
    Non_iterable_indexed_carbonated_data_storage
      with type t = C.t
       and type key = I.t
       and type value = V.t

  val list_values :
    ?offset:int ->
    ?length:int ->
    C.t ->
    (Raw_context.t * V.t list) tzresult Lwt.t
end = struct
  include Make_indexed_carbonated_data_storage_INTERNAL (C) (I) (V)
end

This generates the following error message in coq-of-ocaml:

--- storage_functors.ml:527:19 --------------------------------------------- not_supported (1/1) ---

  525 |     (C : Raw_context.T)
  526 |     (I : INDEX)
> 527 |     (V : VALUE) : sig
> 528 |   include
> 529 |     Non_iterable_indexed_carbonated_data_storage
> 530 |       with type t = C.t
> 531 |        and type key = I.t
> 532 |        and type value = V.t
> 533 | 
> 534 |   val list_values :
> 535 |     ?offset:int ->
> 536 |     ?length:int ->
> 537 |     C.t ->
> 538 |     (Raw_context.t * V.t list) tzresult Lwt.t
> 539 | end = struct
  540 |   include Make_indexed_carbonated_data_storage_INTERNAL (C) (I) (V)
  541 | end
  542 | 


Anonymous definition of signatures is not handled

We replace it by the following OCaml code, which translates into Coq without errors:

module type Non_iterable_indexed_carbonated_data_storage_with_values = sig
  include Non_iterable_indexed_carbonated_data_storage

  val list_values :
    ?offset:int ->
    ?length:int ->
    t ->
    (Raw_context.t * value list) tzresult Lwt.t
end

module Make_indexed_carbonated_data_storage
    (C : Raw_context.T)
    (I : INDEX)
    (V : VALUE) :
  Non_iterable_indexed_carbonated_data_storage_with_values
    with type t = C.t
     and type key = I.t
     and type value = V.t = struct
  include Make_indexed_carbonated_data_storage_INTERNAL (C) (I) (V)
end

There we named the return signature of the functor Non_iterable_indexed_carbonated_data_storage_with_values.

Named polymorphic variant types

In the following OCaml code, the type of the parameter depth is a polymorphic variant type:

val fold :
  ?depth:[`Eq of int | `Le of int | `Lt of int | `Ge of int | `Gt of int] ->
  t ->
  key ->
  init:'a ->
  f:(key -> tree -> 'a -> 'a Lwt.t) ->
  'a Lwt.t

We do not handle this kind of type in coq-of-ocaml, because there are no clear equivalent features in Coq. In most of the code, we would replace this declaration with an algebraic datatype as follows:

type depth =
  | Eq of int
  | Le of int
  | Lt of int
  | Ge of int
  | Gt of int

val fold :
  ?depth:depth ->
  t ->
  key ->
  init:'a ->
  f:(key -> tree -> 'a -> 'a Lwt.t) ->
  'a Lwt.t

Sometimes it is not possible to do this kind of change, for backward compatibility of an API for example. In this case we name the polymorphic variant type:

type depth = [`Eq of int | `Le of int | `Lt of int | `Ge of int | `Gt of int]

val fold :
  ?depth:depth ->
  t ->
  key ->
  init:'a ->
  f:(key -> tree -> 'a -> 'a Lwt.t) ->
  'a Lwt.t

We translate the definition of depth as if it was an algebraic datatype:

Inductive depth : Set :=
| Ge : int -> depth
| Lt : int -> depth
| Eq : int -> depth
| Le : int -> depth
| Gt : int -> depth.

Then, using the configuration parameters variant_constructors and variant_types, we instruct coq-of-ocaml to recognize that there is a type depth whenever it finds a constructor `Eq, ..., or `Gt in the OCaml code.

Nested anonymous signatures

There is support for nested anonymous signatures in coq-of-ocaml, but this often does not work well for various reasons. The key reason is that we translate signatures to records, which can only be flat. An example of a nested anonymous signature is the following:

module type TitleWithId = sig
  val title : string

  module Id : sig
    include ID

    module Temp : Temp_id with type t = private t
  end

  module IdSet : Set.S with type elt = Id.t
end

Here the signature of Id is anonymous and nested in the signature TitleWithId. By default, coq-of-ocaml will try to prefix all the fields of the sub-module Id by Id_ and flatten these fields into the fields of TitleWithId:

Module TitleWithId.
  Record signature {Id_t IdSet_t : Set} : Set := {
    title : string;
    Id_t := Id_t;
    Id_compare : Id_t -> Id_t -> int;
    (* ... included fields from [ID] *)
    Id_Temp : Temp_id (t := t); (* there is an error: should be [(t := Id_t)] *)
    IdSet : _Set.S (elt := Id.(IdWithTemp.t)) (t := IdSet_t);
  }.
End TitleWithId.
Definition TitleWithId := @TitleWithId.signature.
Arguments TitleWithId {_ _}.

This works well if Id is used as a namespace in TitleWithId to group the fields in different categories. However, this fails if we aim to directly reference the sub-module Id later on.

A better solution is often to name the anonymous sub-signatures, by doing:

module type IdWithTemp = sig
  include ID

  module Temp : Temp_id with type t = private t
end

module type TitleWithId = sig
  val title : string

  module Id : IdWithTemp

  module IdSet : Set.S with type elt = Id.t
end

The translation is then:

Module IdWithTemp.
  Record signature {t : Set} : Set := {
    t := t;
    compare : t -> t -> int;
    (* ... included fields from [ID] *)
    Temp : Temp_id (t := t);
  }.
End IdWithTemp.
Definition IdWithTemp := @IdWithTemp.signature.
Arguments IdWithTemp {_}.

Module TitleWithId.
  Record signature {Id_t IdSet_t : Set} : Set := {
    title : string;
    Id : IdWithTemp (t := Id_t);
    IdSet : _Set.S (elt := Id.(IdWithTemp.t)) (t := IdSet_t);
  }.
End TitleWithId.
Definition TitleWithId := @TitleWithId.signature.
Arguments TitleWithId {_ _}.

Non-mutually recursive types

Sometimes, because this is convenient, we use the syntax type ... and for types which are not mutually dependent. For example, we could write in OCaml:

type 'a matching_function = 'a -> match_result

and match_result = (string * int option) list

to show the definition of matching_function first. This example would not work in Coq because mutually recursive definitions have to be with at least one algebraic type definition. Even for cases where the translation works, having too many mutually recursive type definitions may complexify the proofs.

For all these reasons, it is better to only use the and keyword for types that are truly mutually recursive. In this case, we rewrite our example as:

type match_result = (string * int option) list

type 'a matching_function = 'a -> match_result

Top-level name collisions

In Coq, it is not possible to have two definitions of the same name at top-level. For example, if we translate the following OCaml code:

let path = RPC_path.(open_root / "context" / "delegates")

let path = RPC_path.(path /: Signature.Public_key_hash.rpc_arg)

we get in Coq:

Definition path : RPC_path.path Updater.rpc_context Updater.rpc_context :=
  RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "delegates".

Definition path
  : RPC_path.path Updater.rpc_context
    (Updater.rpc_context * Signature.public_key_hash) :=
  RPC_path.op_divcolon path
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.rpc_arg).

which generates the error:

Error: path already exists.

A solution is to rename one of the two paths in OCaml:

let raw_path = RPC_path.(open_root / "context" / "delegates")

let path = RPC_path.(raw_path /: Signature.Public_key_hash.rpc_arg)

This kind of situation can also happen when including modules. For example, there is a collision if an included module has names that already exist at the current level. We believe this is a good thing that Coq forbids redefining names at top-level. So using coq-of-ocaml can be a good thing to forbid this practice in OCaml. Note however that it is still possible to redefine names inside an expression in Coq.

Abstractions in .mli files​

Fixpoint struct annotations​

Ignored functions​

Mutual definitions as notations​

Named signatures​

Named polymorphic variant types​

Nested anonymous signatures​

Non-mutually recursive types​

Top-level name collisions​