coq-of-ocaml

Import OCaml programs to Coq for formal verification

Documentation on https://clarus.github.io/coq-of-ocaml/

Aim

coq-of-ocaml aims to enable formal verification of OCaml programs 🦄. The more you prove, the happier you are. By transforming OCaml code into similar Coq programs, it is possible to prove arbitrarily complex properties using the existing power of Coq. The sweet spot of coq-of-ocaml is purely functional and monadic programs. Side-effects outside of a monad, like references, and advanced features like object-oriented programming, may never be supported. By sticking to the supported subset of OCaml, you should be able to import millions of lines of code to Coq and write proofs at large. Running coq-of-ocaml after each code change, you can make sure that your proofs are still valid. The generated Coq code is designed to be stable, with no generated variable names for example. We recommend organizing your proof files as you would organize your unit-test files.

The guiding idea of coq-of-ocaml is TypeScript. Instead of bringing types to an untyped language, we are bringing proofs to an already typed language. The approach stays the same: finding the right sweet spot, using heuristics when needed, guiding the user with error messages. We use coq-of-ocaml at Tezos, a crypto-currency implemented in OCaml, in the hope to have near-zero bugs thanks to formal proofs. Tezos is currently one of the most advanced crypto-currencies, with smart contracts, proof-of-stake, encrypted transactions, and protocol upgrades. It aims to compete with Ethereum. Formal verification is claimed to be important for crypto-currencies as there are no central authorities to forbid bug exploits and a lot of money at stake. A Coq translation of the core components of Tezos is available in the project coq-tezos-of-ocaml. Protecting the money.

There are still some open problems with coq-of-ocaml, like the axiom-free compilation of GADTs (an ongoing project). If you are willing to work on a particular project, please contact us by opening an issue in this repository.

Example

Start with the file main.ml 🐫:

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

Run:

coq-of-ocaml main.ml

Get a file Main.v 🦄:

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.

You can now write proofs by induction over the sum function using Coq. To see how you can write proofs, you can simply look at the Coq documentation. Learning to write proofs is like learning a new programming paradigm. It can take time, but be worthwhile! Here is an example of proof:

(** Definition of a tree with only positive integers *)
Inductive positive : tree int -> Prop :=
| Positive_leaf : forall n, n > 0 -> positive (Leaf n)
| Positive_node : forall tree1 tree2,
  positive tree1 -> positive tree2 -> positive (Node tree1 tree2).

Require Import Coq.micromega.Lia.

Lemma positive_plus n m : n > 0 -> m > 0 -> n + m > 0.
  lia.
Qed.

(** Proof that if a tree is positive, then its sum is positive too *)
Fixpoint positive_sum (tree : tree int) (H : positive tree)
  : sum tree > 0.
  destruct tree; simpl; inversion H; trivial.
  apply positive_plus; now apply positive_sum.
Qed.

Install

Using the OCaml package manager opam, run:

opam install coq-of-ocaml

Usage

The basic command is:

coq-of-ocaml file.ml

You can start to experiment with the test files in tests/ or look at our online examples. coq-of-ocaml compiles the .ml or .mli files using Merlin to understand the dependencies of a project. One first needs to have a compiled project with a working configuration of Merlin. This is automatically the case if you use dune as a build system.

Documentation

You can read the documentation on the website of the project at https://clarus.github.io/coq-of-ocaml/.

Supported

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) ✔️
.ml and .mli files ✔️
existential types (we use impredicative sets to avoid a universe explosion) ✔️
partial support of GADTs 🌊
partial support of polymorphic variants 🌊
partial support of extensible types 🌊
ignores side-effects outside of a monad ❌
no object-oriented programming ❌

Even in case of errors, we try to generate some Coq code along with an error message. The generated Coq code should be readable and with a size similar to the OCaml source. The generated code does not necessarily compile after a first try. This can be due to various errors, such as name collisions. Do not hesitate to fix these errors by updating the OCaml source accordingly. If you want more assistance, please contact us by opening an issue in this repository.

Contribute

If you want to contribute to the project, you can submit a pull-requests.

Build with opam

To install the current development version:

opam pin add https://github.com/clarus/coq-of-ocaml.git#master

Build manually

Clone the Git submodule for Merlin:

git submodule init
git submodule update

Then read the coq-of-ocaml.opam file at the root of the project to know the dependencies to install and get the list of commands to build the project.

License

MIT (open-source software)

d-plaindoux/coq-of-ocaml