Milestone 1

Here we present what we have completed for the first milestone of this grant.

Skip-lists

We have already specified what the skip-lists data structure should do in Skip_list_repr.v. Without condidering the properties that were trivial, we verified:

  • S.Valid.equal the fact that the equality check of two skip-lists is valid;
  • S.Valid.encoding the fact that the data-encoding function on skip-lists is valid

We missed the verification of the following two properties (the most important ones):

  • S.Valid.back_path_is_valid the fact that the check of a path generated by back_path always returns true;
  • S.Valid.back_path_is_uniq the fact that the path generated by back_path is indeed minimal.

We plan to complete the proofs of the skip-lists for the second milestone of the grant, but this was not completed for this first milestone.

Carbonated maps

We have already specified what the carbonated maps should do. We verified all of these specifications in Carbonated_map.v. We verify that:

  • the carbonated maps behave as normal maps, up to the gas cost calculation;
  • the size of the maps is correctly pre-calculated.

Classification of errors

We have classified all the errors appearing in the protocol in the following three reports:

In the file Error.v we give a predicate to specify what are the internal errors for the extensible error type. Our plan to verify the exceptions and asserts is to write proven equal definitions without using exceptions or assertions. We already have many of such simulations for the interpreter and translator of Michelson in the files:

Translation of the protocol J

We have a full translation of the protocol J available in https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/tree/master/src/Proto_alpha and browsable online starting from Alpha_context.v.

We have done this translation running coq-of-ocaml on our fork https://gitlab.com/clarus1/tezos/-/commits/guillaume-claret@proto_alpha-coq-of-ocaml-proto-j that include some changes added in our fork, mainly to make it compile once translated to Coq. The only functions for which we use the @coq_axiom_with_reason attribute of coq-of-ocaml (disabling the translation and replacing the corresponding definition by an axiom) are the followings:

  • Script_interpreter.log because we ignore the logging feature of Michelson in our formalization of the interpreter. Indeed, this feature is only used in debug mode and would accidentally complexify a lot our dependent type definitions for Michelson.
  • Script_interpreter.klog Disabled for the same reasons as log.
  • The top-level initialization calls in Storage_functors.v with code such as let () = ... The reasons are that:
    • These code elements are only doing side-effects so cannot study them in Coq as it is;
    • These code examples are creating a stack-overflow error in Coq for an unknown reason.

In addition to the translation of the Tezos code using coq-of-ocaml, we spent a lot of time writing simulations for the Michelson interpreter. These are proven-equivalent definitions using dependent types instead of GADTs. The issue with definitions with GADTs in our Coq translation is that they use dynamic cast axioms in the match, what makes the proofs on them more complex in our experience. Our main files with simulations are the followings:

Additional proofs

We have continued to maintain our existing proofs and verified most of the compare functions as presented on this page: Status compare. We have also continued our verification effort on the property-based tests. We have a Coq translation and at least a part of the proofs for the following test files:

Communication

Our communication was mainly in the form of blog posts. We published the following posts: