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

[tomsib2001]

Yes, I think tezos.v is obsolete and the rest is correct.

[manvithn]

I'm not very familiar with ssreflect or mathcomp either. Is it possible to use the coq-mathcomp-ssreflect package instead of installing coq-ssreflect and coq-mathcomp-algebra? As I understand, there are some namespace differences but coq-mathcomp-ssreflect seems more up-to-date. OPAM gives me the following message when I try to install coq-ssreflect:

The following dependencies couldn't be met:
  - coq-ssreflect -> coq (< 8.5~ | = 8.5~beta2)
Your request can't be satisfied:
  - No package matches coq.8.5~beta2.
  - coq<8.5~ is not available because your system doesn't comply with ocaml-version >= "3.11.2" & ocaml-version < "4.03".

However, I can install coq-mathcomp-ssreflect without any problems with coq 8.8.0 and OCaml 4.06.1.

[jeromesimeon]

@manvithn I'm guessing coq-mathcomp-* is the current release? I saw opam contributions of those packages for coq 8.8 today so it's possible that it works. Otherwise, mathcomp compiled from the source for me with 8.8 as well -- albeit with tons of warnings.

[murbard]

@CoinFormalizer @anton-trunov @benoitrazet while I have you, do you have any objections to releasing the code in this repo under an MIT license? If not I'll upload a license.md file

[CoinFormalizer]

No objection, I approve this release.

[anton-trunov]

@murbard No objections as well, feel free to release.

[murbard]

@cmangin sale question

[cmangin]

No objection, any license will do for me.

[benoitrazet]

That's completely fine by me.

[jeromesimeon]

👍