Simulations - dependently-typed version

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.