# package coq-of-ocaml

## Install

## Dune Dependency

## Authors

## Maintainers

## Sources

`sha256=1c6d414ae8e4babfd79f82cb667cdaaf11b4c3b76dc83de4c23f6ee8ec6affff`

`sha512=4b017b5892ef0c665a5ff5da292ec5cbdd1a103dfb7193553b78d25693787acd359a30028c335b300883d555786d3787258fe7a57d63cd53b94edc6b40e8ffbe`

## Description

## README

## ππ« coq-of-ocaml

Translate OCaml programs to **similar-looking code in Coq**, an extremely expressive formal language to express and formally verify **any kinds of properties** (preservation of invariants, absence of assert failures, backward compatibility, ...). We use `coq-of-ocaml`

to formally verify the "protocol" (core part) of the crypto-currency Tezos, composed of **100,000 lines of OCaml**. We cover most of the code: **80% of files** have at least one formally verified property in the project coq-tezos-of-ocaml. This is formal verification at a **large scale**.

π€ Do not hesitate to schedule a quick meeting with us for more information by going on https://koalendar.com/e/meet-with-formal-land. We offer formal verification services and advices and are always there for a quick chat π². |
---|

**π Documentation on https://formal.land/docs/coq-of-ocaml/introduction**

### π― Aim

`coq-of-ocaml`

enables formal verification for OCaml programsΒ π¦. *The more you prove, the happier you are.*

By transforming OCaml code into similar Coq programs, we can 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 can import millions of lines of code to Coq and write proofs at large. By running `coq-of-ocaml`

after each code change, you make sure that your proofs are still valid. The generated Coq code is designed to be stable, with no generated variable names. We recommend organizing your proof files as you would organize your tests, with one proof file per code file.

The guiding idea of `coq-of-ocaml`

Β is TypeScript. Instead of bringing types to an untyped language, we bring proofs to a typed language. The approach is the same: finding the right sweet spot, using heuristics when needed, guiding the user with error messages. We use `coq-of-ocaml`

for the crypto-currency Tezos in the hope of having 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 key for crypto-currencies as there are no central authorities to forbid bug exploits and stealing 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, you can contact us at contact@formal.land.

### 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 it can 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://formal.land/docs/coq-of-ocaml/introduction.

### 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

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)