Presentation

We worked for the formal verification of parts of the L1 of the Tezos blockchain for two grants with the Tezos Foundation of four months each.

The end result is on this website: https://formal-land.gitlab.io/coq-tezos-of-ocaml/ It includes a blog associated with the project describing the technical progress and the challenges we faced, as well as a link to the source code of the project. Everything is open-source under MIT license.

Tezos

Milestone 1

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

  • Verification: significantly increase the coverage of the proofs in the protocol code:
    • Verify the *_hash.ml files: short files with very few properties to verify.
    • Verify the *_repr.ml files: check the definitions of data-encodings.
    • Verify the *_services.ml files: check the encodings in the RPCs.
  • Translation: add annotations on the Ocaml sources or improve the way coq-of-ocaml translates the code in order for some of the files to translate to Coq. Due to various changes in the protocol, some of the files are currently not translating to Coq. The main difficulty in these files is that they include a lot of pattern-matching on GADTs.
    • Translate the Michelson interpreter script_interpreter.ml (around 2,000 OCaml lines).
    • Translate the Michelson translator script_ir_translator.ml (around 6,000 OCaml lines).

Milestone 2

We take the milestone description from the "milestone review" and complete it with our results for this milestone report. In all this document, we will use the pills:

  • 🟢 for "done",
  • 🟠 for "partially done",
  • 🔴 for "not done".

Our results are for the proto_alpha version of the protocol in the branch master. Given the date of this document, this protocol version is close to the version J of the protocol.

Verification

Storage system

Verify the storage system: show a simulation with a simpler data structure made of records, sets, and maps.

We wrote a specification of the storage.ml file in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/storage/ . This specification is composed of two parts:

  • The definition of a simulation state and change types 🟢;
  • An axiomatization that this simulation is equivalent to the various sub-stores defined in OCaml. This is axiomatized for now but should have been proven 🔴.

To prove that the store simulations are correct, we need to verify the storage functors defined in storage_functors.ml. We wrote these proofs in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/storage_functors/ The functors are the followings:

  • Make_subcontext 🟢
  • Make_single_data_storage 🟠
  • Pair 🟢
  • Make_data_set_storage 🟠
  • Make_carbonated_data_set_storage 🔴
  • Make_indexed_data_storage 🟢
  • Make_indexed_carbonated_data_storage 🟠
  • Make_indexed_data_snapshotable_storage 🔴
  • Make_indexed_subcontext.Raw_context 🟢
  • Make_indexed_subcontext.Make_set 🟠
  • Make_indexed_subcontext.Make_map 🟠
  • Make_indexed_subcontext.Make_carbonated_map 🔴
  • Wrap_indexed_data_storage 🔴

We also need to check that the sub-storages do not interfere with each other (so that we store the data at different sub-trees in the context). This is not done 🔴.

*_storage.ml files

Verify the [*_storage.ml files:] verify the high-level behavior of these functions and specify the invariants on the storage which these files expect.

For most of the files named *_storage.ml in the protocol, we wrote a specification of some of the functions together with corresponding proofs. In addition to validating parts of the code, we believe this also validates our approach to verify the storage interactions using a simulation. The proofs are in the following files:

There are still some properties that are axioms or using axioms because the storage system is not entirely specified. Thus we consider this verification effort to be between 🟠 and 🟢.

Michelson interpreter

Verify the Michelson interpreter, according to the semantics given in Mi-Cho-Coq.

We have done the following steps to verify the Michelson interpreter:

  • The definition of a dependently-typed abstract syntax tree for Michelson in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/simulations/script_typed_ir 🟢
  • The definition of a dependent-typed interpreter following the definition of the OCaml interpreter in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/simulations/script_interpreter 🟠
  • A proof of equivalence between the dependent interpreter and the OCaml version (translated to Coq) in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/script_interpreter 🟠
  • A proof of inclusion of the semantics on Mi-Cho-Coq into the dependently-typed interpreter in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/simulations/micho_to_dep 🟠 The proof is mainly for the individual instructions. What is missing are the control structures or some more complex instructions, primarily related to contract calls or set and map data structures.
  • We found a few changes to make in Mi-Cho-Coq to keep the semantics similar to the one in OCaml, like the change in the order of parameters for one of the instructions (this instruction was not used in the verification of existing smart contracts).

Michelson type-checker

Verify the script translator, in particular for the compatibility of the parsing and unparsing operators.

To verify the Michelson type-checker in script_ir_translator.ml, we have done the following steps:

  • The definition of a dependently-typed version of the various parse and unparse functions in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/simulations/script_ir_translator/ 🟠
  • A proof of equality between the dependently-typed functions and translated OCaml ones in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/script_ir_translator/ 🟠
  • We have not done a proof that each kind of parse and unparse functions are inverses 🔴, although we had partial proofs for previous versions of the protocol that we need to update.

Among the difficulies we had with the type-checker are that:

  • There were a lot of changes in the OCaml code requiring us to change our proofs, like the removal of the annotations. We did not anticipate this difficulty enough.
  • The function definitions are large and slow to evaluate in Coq.

We hope to complete these proofs at some point, especially in the hope of having a proof for the pair's case of the parsing functions.

Gas system

Verify the gas system: check that the saturated arithmetic implementation is valid, and check that the expected computational complexity is coherent with the gas cost for important functions.

  • We checked that the saturation arithmetic functions defined in saturation_repr.ml are correct in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/saturation_repr For each primitive, we check that is it coherent to the equivalent version in Z when we stay in the bounds, and that the output is always in bounds 🟢.
  • We also verified the existing property-based tests for the saturation arithmetic defined in saturation_fuzzing.ml with corresponding lemmas in https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/tests/pbt/saturation_repr These lemmas verify that the tests succeed for any possible inputs 🟢.
  • We did not verify the complexity cost of functions using the gas 🔴.

For the tests, we are working with four students of the Rug Nl University for a part-time internship to:

  • translate the tests to Coq;
  • verify that they are correct in the general case.

This is ongoing work that will last two more months with the students. The students are not being paid, and this is part of a class, so there is no need for funding.

Better communicate with the OCaml developers and share code, therefore it is important to link the verification and testing effort.

We think we need to do more presentations, especially at the proto-call 🟠.

Translate the code in the test folder to Coq. Verify the generalized version of the OCaml tests. We want to make sure that there are no bugs related to properties that are already tested.

  • We have translated and verified two test files by hand:
    • Saturation arithmetic: https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/tests/pbt/saturation_repr
    • Tez arithmetic: https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/tests/pbt/tez_repr
  • We began to automate the translation with coq-of-ocaml of two test files in Coq:
    • Saturation arithmetic: https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/tests/pbt_generated/saturation_fuzzing
    • Sc rollup ticks: https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/tests/pbt_generated/test_sc_rollup_tick_repr

With our technique, we can only cover the tests in the pbt/ folder of the test/ folder of the protocol, and we verified only a few files. So we consider that we are between 🔴 and 🟠 for this task.

Broader support of the Tezos code

Make coq-of-ocaml usable as a library rather than as a configurable executable. This way, the recipient is able to customize the behavior of coq-of-ocaml depending on the kind of code.

We have not done this task 🔴.

Translate and verify the data-encoding library. A challenge in verifying this library in Coq is that it contains optimized code using side-effects such as global references, exceptions, or mutable bytes buffers.

We have not done this task 🔴.

Optimizing the execution of coq-of-ocaml. The translation of the protocol currently takes around one minute on a typical machine, this should be reduced ten fold in order to iterate more rapidly on the code.

We have made some optimizations decreasing the time to translate the protocol by two to three times 🟠.

Deliverables

A) Formally verify more critical parts of the code and reach a significant volume of verified code.

Since the last milestone (end of January 2022), we wrote around 20,000 lines of Coq proofs on the protocol. In addition to verifying properties for this milestone, we also verified utility functions (encoding, comparisons, ...). An example of such verification effort is the file Indexable.v, where we verify the encodings, the comparisons, and the Make functor of the indexable.ml file of the protocol.

B) Improve coq-of-ocaml , reducing the use of unsafe axioms and supporting more OCaml code. In addition to the protocol, we want to support the Tezos libraries and the shell.

We have made incremental changes to coq-of-ocaml to support the recently added code in the protocol. We continue to use unsafe axioms, for example to support the GADTs. We still support most of the protocol code. We do not yet support code in the shell or libraries. We are beginning to support the tests of the protocol. So this is between 🟠 and 🔴.

C) Maintain the existing infrastructure, that is to say the translation pipeline from OCaml to Coq and the existing proofs on the protocol.

We have continued to maintain the translation of the protocol code to Coq, and the existing proofs. The code size increased by more than 50% since the beginning of the grant (four months ago), mainly due to the rollup projects, but we still translate most of the protocol code to Coq 🟢.

Additional remarks

We have not found bugs in the OCaml code of the protocol.

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:

Milestone 2

In this report, we summarize the work we have done in July and August 2022. Thanks for the reading of the report, and the opportunity given to us to work on the verification of Tezos.

Here are some general remarks on our code:

  • We have all our developments in the Git repository https://gitlab.com/formal-land/coq-tezos-of-ocaml with its associated website https://formal-land.gitlab.io/coq-tezos-of-ocaml/, as well as some proofs in https://gitlab.com/formal-land/json-data-encoding for the json-data-encoding library.
  • The website presents a better view of the proofs, with hyperlinks to access the definitions. It also includes a blog and a Guides section with a higher-level presentation of the repository.
  • What we name Proto_alpha is actually the protocol version J. We kept this name to preserve the links, but are planning to change it once we have a proper translation of the development version alpha of the protocol.
  • Instead of making a comparison for the backward compatibility between the protocol version J and alpha (as claimed in the grant proposal), we are making a comparison of versions J and K. This is because the version K was released by the time of the end of this grant.
  • The branch from which we translate the folders of the protocols version J and K of Tezos is in this merge request. It includes some changes so that the translated code compiles in Coq.

Skip-list data structure

We verified the validity of the skip-list data structure in https://gitlab.com/formal-land/coq-tezos-of-ocaml/-/blob/master/src/Proto_K/Proofs/Skip_list_repr.v Our final proof is in the lemma back_path_is_valid. We verify that when the back_path primitive returns some value path then this path is considered as correct for the function valid_back_path.

For our proof of the validity of the back_path function, we added a few hypotheses regarding the way we handle the pointers on the client side of the algorithm. For example, we assume that the cells are all created by a genesis or next operation. To verify the usage of the back-path data structure, we will need to check these hypotheses where the back-path functions are used. We believe these hypotheses to be reasonable and necessary. The whole validity statement is the following:

Lemma back_path_is_valid `{FArgs} {content_type ptr_type : Set}
    (equal_ptr : ptr_type → ptr_type → bool)
    (cell_ptr target_ptr : ptr_type)
    (target_cell : cell content_type ptr_type) (path : list ptr_type)
    (deref : ptr_type → option (cell content_type ptr_type)) (fuel : nat)
    (cell_index_spec : Helper_valid.Cell_Index.Valid.t deref)
    (path_valid : ∀ p x,
                    In p path → deref p = Some x → Cell.Valid.t x)
    (array_len_valid :
       ∀ cptr cval,
         In cptr path →
         deref cptr = Some cval →
           Z.of_nat (Datatypes.length cval.(cell.back_pointers).(t.items))
           < Pervasives.max_int) :
    Compare.Equal.Valid.t (fun _ ⇒ True) equal_ptr →
    deref target_ptr = Some target_cell →
    let target_index := index_value target_cell in
    back_path deref cell_ptr target_index = Some path →
    valid_back_path equal_ptr deref cell_ptr target_ptr path = true.

We do not verify the back_path_is_uniq property that states that the path validated by the boolean function valid_back_path is unique. This property was also claimed in the grant proposal.

Backward compatibility

We verify the backward compatibility over the Michelson interpreter between the versions J and K of the protocol. We put all these developments into the folder src/Proto_K_alpha, following our naming where we use alpha for the protocol J.

We organize our development into several files. In the src/Proto_K_alpha and src/Proto_K_alpha/Simulations folders we put the migrations of the datatypes defined in the corresponding files in src/Proto_alpha. A migration is a function from a datatype defined in the old protocol to the new one. For example, for the mutez values:

Module Old := TezosOfOCaml.Proto_alpha.Tez_repr.
Module New := TezosOfOCaml.Proto_K.Tez_repr.

(** Migrate [Tez_repr.t]. *)
Definition migrate (x : Old.t) : New.t :=
  match x with
  | Old.Tez_tag n => New.Tez_tag n
  end.

we map the old constructor Tez_tag to the new one. We also have such a migration function for the abstract syntax tree of Michelson.

In the folder src/Proto_K_alpha/Proofs we add the proofs of backward compatibility of various functions of the protocol. The main file is src/Proto_K_alpha/Proofs/Script_interpreter.v where we state the backward compatibility of the interpreter:

Error.migrate_monad (Old.dep_step fuel (ctxt, sc) gas i_value ks accu_stack)
  (fun '(output, ctxt, gas) => (
    Script_typed_ir.With_family.migrate_stack_value output,
    Local_gas_counter.migrate_outdated_context ctxt,
    Local_gas_counter.migrate_local_gas_counter gas
  )) =
New.dep_step
  fuel
  (
    Local_gas_counter.migrate_outdated_context ctxt,
    Script_typed_ir.migrate_step_constants sc
  )
  (Local_gas_counter.migrate_local_gas_counter gas)
  (Script_typed_ir.With_family.migrate_kinstr i_value)
  (Script_typed_ir.With_family.migrate_continuation ks)
  (Script_typed_ir.With_family.migrate_stack_value accu_stack)

We say that the two following computations give the same result:

  • taking the dep_step function from the protocol J, running it on an instruction i_value and a stack accu_value, and applying the migration function on the results;
  • taking the dep_step function from the protocol K, and running it on the migrations of an instruction i_value and a stack accu_stack.

At the time of writing, we have verified the backward compatibility of the interpreter on 80% of the instructions. We did not verify the backward compatibility of the parser and type-checker of Michelson. In order to simplify the proofs, we axiomatize that the gas cost is the same for the two protocols. We check that both the success and the error cases of the interpreter are the same for the protocols J and K.

We write our proofs on a dependently typed implementation of the interpreter that we name dep_step in the file src/Proto_K/Simulations/Script_interpreter.v instead of the usual step function from src/Proto_K/Script_interpreter.v. We do so to simplify the reasoning on the code that is originally written using GADTs in OCaml.

For the two protocols J and K, we have a complete definition of a dependent abstract syntax tree, an almost complete definition of the interpreter, and the definition for most of the script_ir_translator.ml file. To these dependent definitions, we attach proofs of equivalence between the dependent implementation and the original translated code. The translated code from OCaml contains cast axioms to implement the match on GADT values. We mostly verified the equivalence for the interpreter and some parts of the script_ir_translator.ml file.

Most of our time was allocated to writing or verifying these dependent implementations for both protocols J and K. A good optimization in our work would be to automatically generate these dependent implementations from the OCaml code.

Absence of internal errors

We did not have time to do more than our initial reports classifying the errors in the Tezos protocol (submitted for the previous half of the grant). With the dependent implementation that we write for Michelson, we verify the absence of assert false, exceptions and non-termination effect for all the parts of the code for which we have a dependent version. For the absence of assert false or exceptions, at a meta-level, our proof relies on the fact that:

  • we axiomatize the assert or exception operators;
  • unless we ignore these values, if they appear in a reachable branch of the translated OCaml code then it would not be able to prove our dependent purely functional implementation equal to the translated code.

We are aware that we did not achieve to do what we planned for the verification of the absence of internal errors.

JSON data encoding

Additionally, we worked on the verification of the JSON data-encoding library used in the protocol for serialization. We verified the implementation of the optimized version of List.map given in src/list_map.ml in the file coq-src/proofs/List_map.v of our fork of the project.

We also began the translation to Coq of the other files of this project. However, we faced some difficulties including:

  • The use of polymorphic variants; for that we refactored the code to avoid using polymorphic variants.
  • A missing definition of the standard library of OCaml in Coq. We have started to complete these definitions in this pull request.

Communication

We published two blog posts:

  • Fixing reused proofs to explain how we typically proceed to port and fix proofs for a version of the protocol to another. In particular, we had to do this work from the protocol version J to K, and complete the proofs for the verification of new data-encodings for example.
  • Verifying json-data-encoding to explain the work we did on the JSON data-encoding library, in particular to translate parts of the code to Coq and verify the optimized List.map implementation.

Milestone 3

To see the work we have done in this additional milestone, please refer to this PDF document: Additional Milestone - Verification of the Internal Errors.