Skip to main content

· 10 min read
Pierre Vial

In this blog post, I propose to make you discover how we deal with internal errors and show that they do not occur while running the protocol! I will first give you a glimpse of the so-called error monad (but without going into the details of the notion of monad 🙂). You actually don't need to have any knowledge of monads in computer programming or elsewhere to read this article: we will take them step by step. But if you are already familiar on them, you can skim through the first parts of this post and have a look at the monadic let ... ins we use and how we articulate them with validity predicates. We conclude by giving a first glimpse at how we use these validity predicates to manually specify information which is lost during the automatic translation from OCaml to Coq.

· 5 min read
Guillaume Claret

We are currently verifying the absence of internal errors in the protocol of Tezos. We show that no unexpected errors are reachable in the code, such as assert false or critical errors. We describe here what we have done recently towards the verification of such errors.

· 6 min read

In Tezos, the skip-list data structure is used in several places. Verification of skip-list required many days of painstaking work, and this work is not yet finished. In this post, we will talk about the techniques we used. In particular, we describe the verification of function mem - one of the functions operating in this data structure. More information about formal verification of skip list can be found here.

· 5 min read

Formal verification of the skip list of Tezos includes the work on verification of the following properties :

  • Validity of a cell (containing content and a list of back pointers),
  • Validity of a dereferencing operator,
  • Validity of encoding functions for cell and pointer,
  • Validity of backpointers,
  • Verification of equality definition,
  • Verification of group of functions and definitions serving the organization of data-structure : next, genesis, best_skip, mem, pp and others,
  • Validity of a back_path (the list of backpointers),
  • Uniqueness of express line (back_path, list of pointers, generated with usage of best_skip function).

· 4 min read
Tait van Strien

Tezos uses the json-data-encoding library throughout the protocol to serialize data for use in RPC, writing to disk or placing in a block. RPC is a synchronous operation. Consequently, it is paramount to verify the correctness of code as well as the logical equivalence and semantics of performance-enhanced procedures to proven ones.

This library has been subject to stack overflows, as seen in issues like this. We will translate and verify this library to validate its logic and simplify debugging these issues.

· 5 min read

After each new release of the protocol there comes a need to validate it. One of the options would be to start from scratch, but fortunately there is no need for that since many parts of the protocol are only slightly changed or stay the same. That allows us to reuse old proofs in consequent versions and speed up the validation.

Of course there is a small number of proofs which stop working due to the changes and that has to be repaired. This process can sometimes be tricky since it requires an understanding of how different functions and proofs depend on each other, but that makes it very interesting. In this post, we will show examples of broken proofs, discuss reasons for their failure, and show techniques we used to fix issues.

· 7 min read
Guillaume Claret

Property based tests are a way to find bugs in the code by running a boolean function (representing an expected property) on randomly generated inputs. In this blog post, we show how we translate these tests to corresponding Coq theorems. Once we have a formal representation, we prove them correct on any inputs. Thanks to this technique, we can:

  • have a bridge between the specification given by the tests and the specification in Coq;
  • make sure that the properties verified in the tests are true with a mathematical degree of certainty.

We have done this work with students from the University of Groningen:

· 5 min read
Guillaume Claret

The backward compatibility is an important property to maintain between two releases of the protocol of Tezos. For example, this ensures that existing smart contracts still work after a protocol upgrade. That property can be hard to ensure by the protocol developers as the codebase's size increases. At the time of writing, there are 86,346 lines of code in src/proto_alpha/lib_protocol in the master branch of Tezos, counting all the .ml and .mli files.

We propose using formal verification to check that the backward compatibility is preserved after each protocol release, with a mathematical degree of certainty. More precisely, we show that for every inputs and storage contexts, a smart contract working with version Jakarta of Tezos will generate the exact same output running on the next version K. Even if there are infinitely many possible inputs, we can verify all of them by writing a mathematical proof in the formal system Coq.

In this blog post, we describe our plan for this verification effort.

· 8 min read
Natalie Klaus

OCaml developers at Tezos often use fold_left function in the code. Maybe the reason is that it is a bit easier to write efficient code using fold_left than fold_right.

fold_left and fold_right from OCaml library: List

val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a

fold_left f init [b1; ...; bn] is f (... (f (f init b1) b2) ...) bn.

val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b

fold_right f [a1; ...; an] init is f a1 (f a2 (... (f an init) ...)).
Not tail-recursive.

And from formal verification point of view, it is much easier to prove statements about fold_right either than about fold_left. Why? The reason is in how these functions are organized. Formal verification often uses mathematical induction as an instrument for proving statements on the lists.

· 4 min read
Natasha Klaus

As you may already know from the article Simulations - dependently-typed version, in the Proto_alpha folder we keep code, generated by the coq-of-ocaml. Many of the fixpoints here are preceded by the annotation #[bypass_check(guard)], which means that guard checking is locally disabled. And this means that we can not consider these functions to be total. In such cases, proof engineers usually feel irritation, because "total" is one of their favorite words. We know that total functions never crush and they always return a well-typed result within a finite time.

note

Thanks to Alan Turing we know that the halting problem - the difficulty of determining whether a specific program terminates or not - is undecidable. Coq can't determine if a function is total in general, according to the original definition of totality. Instead, it analyzes a function's syntax and makes a conservative approximation.

Our current goal is that the doubles defined in the folder Simulations, whose equivalence with their prototypes from Proto_alpha should be proved, would be total (have enabled Coqs guard checking on fixpoint). We already mentioned the Guard Checking question here.

Coq is analyzing the function's syntax to consider it to be total. One way to convince Coq that a function is total is to show that there is a decreasing argument that converges to the base case.

Let's consider the function parse_ty_aux from Proto_alpha and its clone dep_parse_ty_aux from the Simulations folder. parse_ty_aux is having {struct node_value} annotation. The point of the {struct ident} annotation is to tell the Coq, which argument decreases along the recursive calls. node_value : Alpha_context.Script.node is designed in such a way that it is not trivial to show that the function converges. Coq can not detect that each and every recursion call is done on the direct subterm of a given node_value argument (and it is indeed actually not the case).