During our work on verification of Tezos source code,
we run into an interesting question: how to implement OCaml's `GADTs`

in Coq?
The essence of this problem, as well as its solution, were described in
the article: Translating the Michelson interpreter
where we show how we introduce casts in the generated Coq code.

In this article, we will consider subsequent work in this direction.
To reach one of our main goals, proof of the compatibility of the parsing
and unparsing functions for the Michelson types and values,
we need to avoid `casts`

. A powerful Coq's instrument, the dependent types, will help
us to solve the `casts`

problem. We create a kind of clone of `coq-of-ocaml`

's
code, which is a dependently typed version.

The whole process can be structured as follows:

- the
`Simulations`

folder (along with its purpose and content), - definition of dependent types,
- definition of functions with dependent types (analogs of functions with casts),
- proof of the equivalence between functions with dependent types and functions with casts,
- proof of assertions and properties for functions with dependent types.

and this is how it is all organized in the repository:

- we keep files, generated by
`coq-of-ocaml`

in folder`Proto_alpha`

- we keep dependently-defined types and functions in folder
`Simulations`

- we keep our proofs in folder
`Proofs`

## Purpose and content of the `Simulations`

folderโ

In the `Proto_alpha`

folder, we keep files generated by `coq-of-ocaml`

. In
the `Simulations`

folder, we keep the simulation files. File names are the same
(we follow the naming of the OCaml definitions), but for files in
the `Simulations`

folder we redefine all the functions and types we need,
using Coq's dependent types mechanism.

## Definition of dependent typesโ

We define a dependently typed version of the Michelson Abstract Syntax Tree. We parametrize our types using type families, which are values describing a "class" of types. This gives us some benefits and flexibility, like pattern-matching on values and dependent pattern-matching.

We also define Fixpoints for type conversion.

For example, consider this code below (the definition of `ty`

analog)

`Module Family.`

Module Ty.

Module Num.

Inductive t : Set :=

| Int : t

| Nat : t.

End Num.

Inductive t : Set :=

| Unit : t

| Num : Num.t -> t

| Pair : t -> t -> t

...

Module With_family.

Import Family.

Inductive ty : Ty.t -> Set :=

| Unit_t : Script_typed_ir.ty_metadata -> ty Ty.Unit

| Int_t : Script_typed_ir.ty_metadata -> ty (Ty.Num Ty.Num.Int)

| Nat_t : Script_typed_ir.ty_metadata -> ty (Ty.Num Ty.Num.Nat)

| Pair_t {t1 t2} :

ty t1 ->

ty t2 ->

Script_typed_ir.ty_metadata ->

ty (Ty.Pair t1 t2)

...

Fixpoint to_ty {a} (t : ty a) : Script_typed_ir.ty :=

match t with

| Unit_t m => Script_typed_ir.Unit_t

| Int_t m => Script_typed_ir.Int_t

| Nat_t m => Script_typed_ir.Nat_t

| Pair_t t1 t2 m =>

Script_typed_ir.Pair_t (to_ty t1) (to_ty t2) m

## Definition of functions with dependent typesโ

Functions from the `Simulations`

folder have the same titles as their counterparts from
the `Proto_alpha`

folder. But they are prefixed with `dep_`

.
Let's consider the function `dep_parse_comparable_ty_aux`

- the dependent-typed
version of `parse_comparable_ty_aux`

function from the `Proto_alpha`

folder.
We also define the Inductive existential type (analog of `ex_comparable_ty`

).
For `ex_family_comparable_ty`

we also have to
prove equality with the original type.

`Inductive ex_family_comparable_ty : Set :=`

| Ex_family_comparable_ty {t : Family.Ty.t} :

With_family.comparable_ty t -> ex_family_comparable_ty.

Fixpoint dep_parse_comparable_ty_aux

(stack_depth : int) (ctxt : Alpha_context.context)

(ty : Alpha_context.Script.node) {struct ty}

: M? (ex_family_comparable_ty * Alpha_context.context).

## Proof of the equivalence between `dep_functions`

and the original onesโ

The next step after defining functions with dependent types is to prove their
equality with original functions, the ones that were generated by `coq-of-ocaml`

(the ones with casts we are aiming to avoid).

Consider the code below, followed by a conscientious analysis of what is happening:

`Fixpoint dep_ty_of_comparable_ty_eq {t} (ty : With_family.comparable_ty t) :`

With_family.to_ty (dep_ty_of_comparable_ty ty) =

ty_of_comparable_ty (With_family.to_comparable_ty ty).

destruct ty; Tactics.destruct_pairs; simpl;

repeat rewrite dep_ty_of_comparable_ty_eq; reflexivity.

Qed.

This is a function entitled

`dep_ty_of_comparable_ty_eq`

, from folder`Proofs`

.

It proves that two functions (type converter from folder`Simulations`

with prefix`dep_`

) and (type converter from folder`Proto_alpha`

) are equal.This is a dependent type (

`ty: With_family.comparable_ty t`

), defined in the folder`Simulations`

.This is a fixpoint

`dep_ty_of_comparable_ty`

, defined in the folder`Simulations`

.- Its signature is:

`forall t : Family.Ty.t, With_family.comparable_ty t ->`

With_family.ty t

It can convert dependently-typed `comparable_ty`

into dependently_typed `ty`

(both from the Simulations folder)

This is a fixpoint

`With_family.to_ty`

, from the`Simulations`

folder.- Its signature is:

`Fixpoint to_ty {a} (t : ty a) : Script_typed_ir.ty`

It can convert dependently-typed `ty`

into original `ty`

(defined in `Proto_alpha`

folder)

This is a fixpoint

`ty_of_comparable_ty`

, it can convert`comparable_ty`

into`ty`

(all three from folder`Proto_alpha`

)This is the function

`With_family.to_comparable_ty`

.- Its signature is:

`forall t : Family.Ty.t, With_family.comparable_ty t ->`

Script_typed_ir.comparable_ty

It can convert dependently-typed `comparable_ty`

(from `Simulation`

folder)
into initial `comparable_ty`

(from `Proto_alpha`

folder)

Summarizing: `dep_ty_of_comparable_ty`

is equivalent to `ty_of_comparable_ty`

.

So, everything that we prove for the one with the `prefix _dep`

will be true
for the second.

## Proof of assertions and properties for functions with dependent typesโ

Thanks to simulations with dependent types we simplified further reasoning on
the interpreter for ourselves. We do not have to deal with `casts`

anymore.
Instead, we have all the benefits of Coq's pattern-matching.