https://gitlab.com/nomadic-labs/mi-cho-coq
Revision 880aee5ebb4aa263f3f7a98bd1ef71645c8f2b42 authored by Guillaume Claret on 10 March 2020, 21:16:49 UTC, committed by Guillaume Claret on 16 March 2020, 15:12:22 UTC
1 parent b2e65df
Tip revision: 880aee5ebb4aa263f3f7a98bd1ef71645c8f2b42 authored by Guillaume Claret on 10 March 2020, 21:16:49 UTC
[Michocoq] Add parsing of timestamps
[Michocoq] Add parsing of timestamps
Tip revision: 880aee5
README.org
#+Title: Mi-Cho-Coq
This repository is a formalisation of the [[https://www.michelson-lang.com/][Michelson]] language using the
[[https://coq.inria.fr/][Coq]] interactive theorem prover.
* Installation instructions
The simplest way to install the project is to use the OPAM package manager:
#+BEGIN_SRC bash
# Add the coq-released opam repository because it contains the coq-ott dependency
opam repo add coq-released https://coq.inria.fr/opam/released
# Install mi-cho-coq and its dependencies (coq, ott, and coq-ott)
opam pin add -k path coq-mi-cho-coq ./
#+END_SRC
* Introduction
The following parts of the language
are formalized:
- the type system
- the syntax
- the semantics
This formalisation is entirely based on [[https://tezos.gitlab.io/betanet/whitedoc/michelson.html][the specification of
Michelson]]; more precisely, it is currently based on the following
version of this specification:
[[https://gitlab.com/tezos/tezos/blob/16bd2b036439d76a3e89dff8fdfbd36cf1d131fe/docs/whitedoc/michelson.rst]]
* Syntax
** Type system
In Michelson, an important distinction is made between *comparable*
types and non-comparable ones. Comparable types can be used to index
maps and only sets of elements in comparable types are allowed.
Here is the list of comparable types defined in [[./src/michocoq/syntax.v]]:
#+BEGIN_SRC coq
Inductive comparable_type : Set :=
| string
| nat
| int
| bytes
| bool
| mutez
| key_hash
| timestamp.
#+END_SRC
Each comparable type is trivially a Michelson type, here is the full
list of Michelson types as defined in [[./src/michocoq/syntax.v]]:
#+BEGIN_SRC coq
Inductive type : Set :=
| Comparable_type : comparable_type -> type
| key : type
| unit : type
| signature : type
| option_ : type -> type
| list_ : type -> type
| set_ : comparable_type -> type
| contract : type -> type
| address : type
| operation : type
| pair : type -> type -> type
| or : type -> type -> type
| lambda : type -> type -> type
| map : comparable_type -> type -> type
| big_map : comparable_type -> type -> type.
#+END_SRC
Coq let us see the type =comparable_type= as a subtype of the type
=type= by declaring the =Comparable_type= injection as an implicit
coercion.
#+BEGIN_SRC coq
Coercion Comparable_type : comparable_type >-> type.
#+END_SRC
** Instructions
The syntax and typing of Michelson instructions is defined in file
[[./src/michocoq/syntax.v]]. We use a dependent inductive type to rule out
ill-typed instructions.
#+BEGIN_SRC coq
Inductive instruction : list type -> list type -> Set :=
| NOOP {A} : instruction A A
| FAILWITH {A B a} : instruction (a ::: A) B
| SEQ {A B C} : instruction A B -> instruction B C -> instruction A C
| IF_ {A B} : instruction A B -> instruction A B -> instruction (bool ::: A) B
| LOOP {A} : instruction A (bool ::: A) -> instruction (bool ::: A) A
...
#+END_SRC
* Semantics
The semantics of types is defined by interpreting them
by predefined Coq types using the following table (function =data= in file [[./src/michocoq/semantics.v]]:
| Michelson | Coq |
|---------------+---------------------------------------|
| =int= | =Z= |
| =nat= | =N= |
| =string= | =string= |
| =bytes= | =string= |
| =timestamp= | =Z= |
| =mutez= | =int63= |
| =bool= | =bool= |
| =unit= | =unit= |
| =pair a b= | =a * b= |
| =option a= | =option a= |
| =or a b= | =sum a b= |
| =list a= | =list a= |
| =set a= | =set a (lt a)= |
| =map a b= | =map a b (lt a)= |
| =bigmap a b= | idem |
| =lambda a b= | =instruction (a ::: nil) (b ::: nil)= |
| anything else | axiomatized |
with
#+BEGIN_SRC coq
Definition int63 :=
{t : int64.int64 | int64.sign t = false}
Definition set a lt :=
{l : list A | Sorted.StronglySorted lt l}
Definition map a b lt :=
set (a * b) (fun x y => lt (fst x) (fst y))
#+END_SRC
We formalize the semantics of Michelson by defining an evaluator in
file [[./src/michocoq/semantics.v]]. Since evaluating a Michelson instruction might
fail (which Coq functions cannot), we wrap the return type of this
evaluator in the exception monad defined in file
[[./src/michocoq/error.v]]. Moreover, Coq forbids non-terminating function so we
use a common Coq trick to define the evalator on diverging
instructions such as =LOOP=: we make the evaluator structurally
recursive on an extra argument of type =Datatypes.nat= called the
=fuel= of the evaluator.
#+BEGIN_SRC coq
Fixpoint eval {A : stack_type} {B : stack_type}
(i : instruction A B) (fuel : Datatypes.nat) {struct fuel} :
stack A -> M (stack B) :=
match fuel with
| O => fun SA => Failed _ Out_of_fuel
| S n =>
match i in instruction A B return stack A -> M (stack B) with
...
#+END_SRC
* Overloading
A Michelson instruction is called overloaded when it can be assigned
several types. For example, the =NEG= instruction which replaces a
number at the top of the stack by its opposite can have either the
type =int : 'S -> int : 'S= or the type =nat : 'S -> int : 'S=.
To handle this source of ambiguity in our typed AST =instruction=, we
use *canonical structures*, a Coq feature that let the Coq refiner
solve the ambiguity by inferring the missing piece of information from
the context.
Both versions of the =NEG= instruction are defined in [[./src/michocoq/syntax.v]]
as follows:
#+BEGIN_SRC coq
(* NEG takes either a nat or an int as argument *)
Inductive neg_variant : type -> Set :=
| Neg_variant_nat : neg_variant nat
| Neg_variant_int : neg_variant int.
Structure neg_struct (a : type) := Mk_neg { neg_variant_field : neg_variant a }.
Canonical Structure neg_nat : neg_struct nat :=
{| neg_variant_field := Neg_variant_nat |}.
Canonical Structure neg_int : neg_struct int :=
{| neg_variant_field := Neg_variant_int |}.
#+END_SRC
The structure =neg_struct= is then used in the =instruction= datatype as follows:
#+BEGIN_SRC coq
Inductive instruction : list type -> list type -> Set :=
...
| NEG {n} {s : neg_struct n} {S} : instruction (n ::: S) (int ::: S)
...
#+END_SRC
so the =NEG= instruction receives a =neg_struct= as an implicit argument
which is going to be provided by the canonical structure mechanism.
Finally, the evaluator in file [[./src/michocoq/semantics.v]] uses this implicit
argument to call the correct function depending on the chosen type for
the =NEG= instruction:
#+BEGIN_SRC coq
Definition neg a (v : neg_variant a) : data a -> data int :=
match v with
| Neg_variant_nat => fun x => (- Z.of_N x)%Z
| Neg_variant_int => fun x => (- x)%Z
end.
...
Fixpoint eval {A : stack_type} {B : stack_type}
(i : instruction A B) (fuel : Datatypes.nat) {struct fuel} :
stack A -> M (stack B) :=
match fuel with
| O => fun SA => Failed _ Out_of_fuel
| S n =>
match i in instruction A B return stack A -> M (stack B) with
...
| @NEG _ _ _ s =>
fun '(x, SA) => Return _ (neg _ (neg_variant_field _ s) x, SA)
...
#+END_SRC
* TODO
- Play with code extraction
- Define an extension of Michelson where loops are annotated with invariants
- check OCaml implem against the documentation
- turn the type of operations into a Coq inductive
To do this we need to implement the syntactic restriction over the
types allowed for the storage to break the mutual dependency between
this new inductive and the "semantics.data" function because the
Create_contract operation requires an argument of type data
storage_ty.
- replace section variables by functors
- Put notations in their own notation scope
- Formalize gas (and remove fuel)
eval should return (stack SA -> M (stack SB * {remaining_gas | remaining_gas < gas }))
- Handle :-, %-, and @-annotations
* Possible mistakes in Michelson specification
- Full Grammar:
+ =FAILWITH <data>= should be =FAILWITH=
+ the =INT= instruction is undocumented
- NOOP should be documented
- The type of the IF_... instruction is erroneous
- Typo : "these are macros are simply"
- The IF_SOME macro is semantically defined instead of syntactically
- The type address should be comparable
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...