State of the coq implementation of Michelson?

[dheeraj-chakilam]

Hello! I'd like to prove correctness of a few simple Michelson programs in Coq. Since the language specification has changed in the last two years, (i) which branch should I be working with? (ii) what current language constructs are correctly defined in Coq as of now?

[murbard]

As you say the language has changed a bit since this work was done. I would start from the master branch of this repo and update it. For the Michelson language, look at the "gas à tous les étages" branch which makes all calls asynchronous.

[jeromesimeon]

@dheeraj-chakilam I'm interested in doing the same. I'll be happy to contribute as well.

[manvithn]

Hi, I'm also interesting in helping with this. Where are the formal semantics for Michelson defined in the "gas à tous les étages" branch? Also, is this repository a clone for a GitLab repository or is it independent?

[murbard]

The gas parameters are very rough. The best formal semantic we currently have is http://doc.tzalpha.net/whitedoc/michelson.html

This repo is independent from the Gitlab repo

[tomsib2001]

The most advanced branch in terms of complete datatypes (more opcodes) and formalization, (e.g. correctness lemmas) is https://github.com/tezos/tezoscoq/tree/new_map_implementation . However as Arthur pointed out the language has changed quite a bit since then. I don't have the time to do it right this moment but if someone is interested, I could explain how the code is structured and generally help out.

[jeromesimeon]

Thanks @tomsib2001 I'm curious to know the motivation for using ssreflect in the development?

[tomsib2001]

Well it's a matter of personal preferences, I suppose. My own Coq education was done in the ssreflect community and I am more productive using it. Moreover, the path library was useful for the semantics of evaluation.
However, I'm sure there are all the tools needed in the Vanilla Coq world as well, as I said it's just a personal choice.

[jeromesimeon]

Thanks, that's what I was wondering. mathcomp is a big dependency and I'm not too familiar with ssreflect, but I just wanted to get a sense of the options. It's probably fine either way but I'll try and familiarize myself with ssreflect.

[anton-trunov]

Let me make a couple of observations: coq-mathcomp-ssreflect package is about 15 kLoC (i.e. not huge) and the SSReflect proof language and several basic libraries are now in the standard Coq distribution; also mathcomp is imho designed really well.

[jeromesimeon]

As I said, I'm not against it :) I'm just not educated. I didn't realize that ssreflect was in recent versions of Coq -- I was only trying to get the branch @tomsib2001 mentioned to compile and the first thing of course was to get those to work:

From mathcomp.ssreflect
  Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
From mathcomp.algebra
  Require Import ssralg ssrnum ssrint.

It probably didn't help that I switched to 8.8 already -- I was able to get everything to compile with a fresh checkout of mathcomp (it isn't in opam yet as far as I can tell).

Then there are lots of other questions such as:

Inductive tagged_data :=
| Int : int -> tagged_data
...

is int different/better than using Z ?

[tomsib2001]

The type int is mathematically the same as Z. For the use we make of it (correctness of factorial), there is certainly the same amount of theory on both sides. However, as @anton-trunov mentioned, the mathcomp library is very well designed which makes (in my very subjective opinion) proving easier.
If we had to extract though, we would probably want to use Z as int is basically two copies of nat which is quite inefficient for computation.

[jeromesimeon]

Thanks @tomsib2001, that's helpful. In part I'm asking because I'm hoping to use tezoscoq (or a variant of it) as a target for a compiler so those questions will come up down the road (I'm using Z for the time being for example). In terms of proving being easier: any general idea of what kind of properties you would want to prove?

[tomsib2001]

I meant proving properties of smart contracts which involve computations on integers; mathcomp has all possible mathematical lemmas you might want about integers, with a systematic, well-thought naming convention. Moreover, most lemmas are stated as equalities between booleans (rather than implications or equivalences between Prop's) which makes it easy to chain their application using rewrite. This also makes it easy to directly rewrite expressions inside a program and to reason by case on decidable properties.

However, I'm sure there are people who think that all these things can be done just as easily and directly using vanilla Coq; this is just my biased vision.

[anton-trunov]

This is also very helpful for subset types. You don't need axioms to work with subset types if you have decidable equality.

[jeromesimeon]

I can relate to that part at least: "Moreover, most lemmas are stated as equalities between booleans (rather than implications or equivalences between Prop's) which makes it easy to chain their application using rewrite. " 😀 I will try and find some time getting familiar with mathcomp...

About the way the code is organized, are any of the following correct:

• language.v contains syntax and type checking
• blockchain.v models the state and is used in semantics.v
• language.v is supposed to replace tezos.v? --