Coq-of-ocaml to translate OCaml to Coq

Community
1

I am pleased to present the coq-of-ocaml project, to translate a subset of OCaml to the Coq proof assistant. The aim is to do formal verification on OCaml programs. The idea is to generate a Coq translation as close as possible to the original code in terms of intent but using the Coq syntax. As a short example, if we take the following OCaml code and run coq-of-ocaml:

type 'a tree =
| Leaf of 'a
| Node of 'a tree * 'a tree

let rec sum tree =
  match tree with
  | Leaf n -> n
  | Node (tree1, tree2) -> sum tree1 + sum tree2

we get the following Coq file:

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Inductive tree (a : Set) : Set :=
| Leaf : a -> tree a
| Node : tree a -> tree a -> tree a.

Arguments Leaf {_}.
Arguments Node {_}.

Fixpoint sum (tree : tree int) : int :=
  match tree with
  | Leaf n => n
  | Node tree1 tree2 => Z.add (sum tree1) (sum tree2)
  end.

We support the following OCaml features:

  • the core of OCaml (functions, let bindings, pattern-matching,…)
  • type definitions (records, inductive types, synonyms, mutual types)
  • monadic programs
  • modules as namespaces
  • modules as polymorphic records (signatures, functors, first-class modules)
  • multiple-file projects (thanks to Merlin)
  • both .ml and .mli files
  • existential types (we use impredicative sets option in Coq)

We also have some support for the GADTs, the polymorphic variants, and the extensible types. We are in particular working on having an axiom-free translation of the GADTs to Coq. We do not support:

  • side-effects outside of a monad (references, exceptions, …);
  • object-oriented programming;
  • various combinations of OCaml features for which coq-of-ocaml should generate a warning.

Our main example and use case is the coq-tezos-of-ocaml project. This contains a translation of most of the economic protocol of the Tezos blockchain (around 30.000 lines of OCaml translated to 40.000 lines of Coq). For example, we verify the comparison functions defined in src/proto_alpha/lib_protocol/script_comparable.ml with src/Proto_alpha/Proofs/Script_comparable.v.

We are looking for the application to other projects too.

We think the best way to use coq-of-ocaml is to continue developing in OCaml and run coq-of-ocaml to keep a synchronized translation in Coq. Having a working Coq translation (as compiling in Coq) forces us to avoid some OCaml constructs. We believe these constructs would probably be hard to verify anyway. Then, on the Coq side, we can verify some important or easy to catch properties. If there is a regression in the OCaml code, re-running coq-of-ocaml should make the proofs break.

20 Likes
2

I noticed that your implementation uses Merlin. Does Merlin provide something that compiler-libs don’t? As I understand it Merlin strives to provide something useful even if the code isn’t compilable (as in an editing session) but that is not an issue for your use case, right? I am genuinely curious and am interested in learning the advantage offered by Merlin over plain-vanilla compiler-libs.

BTW I think your project is really cool and I look forward to learning more about OCaml source code analysis through it.

3

Hello, thanks for your support! The main thing I get from Merlin which is not in the compiler-libs is the environment of types and definitions accessible from each file. This is known to Merlin by communicating with Dune. Using compiler-libs directly would require providing the right parameters to find where the libraries are I guess. At first, we were using compiler-libs and switching to Merlin was the simplest way I found to get access to all of the environment (unless I missed something).

2 Likes