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.

# 3 posts tagged with "function convergence"

View All Tags## Verifying the skip-list

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).

## Fuel - quiet escape from the halting problem

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).