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.

## Specification of the storageโ

The storage described by Storage.v is composed of around one hundred sub-stores. We create these sub-stores on top of the key-value database of Tezos using the Storage_functors.v. For now we axiomatize the behavior of these sub-stores using a simulation in Raw_context_generated.v. This simulation behaves as the actual store, but uses simpler data structures such as records, OCaml sets and maps. Even if it would be impractical for performance reasons to run this simulation, this alternative implementation of the storage simplifies the reasoning for us.

As the storage contains a lot of repetitive declarations, we use a Ruby script to generate the simulation. When we need to make a change, it is easier to change this script than manually replicate the changes on each of the sub-stores. We also generate a file Storage_generated.v with axioms stating that our simulation is valid. An example of axiom about a read operation is the following:

`Axiom get : forall (ctxt : Simulations.Raw_context.t),`

Storage.Block_round

.(Storage.Simple_single_data_storage.get)

(Raw_context.to_t ctxt) =

match Helpers.get ctxt with

| Some x => Pervasives.Ok x

| None =>

Raw_context.storage_error_value

(Raw_context.Missing_key Helpers.name Raw_context.Get)

end.

The context `ctxt`

is a simulated storage value. The function `Raw_context.to_t`

converts a simulated store to an actual store. It is not possible to do the reverse, that is to say there are no functions from an actual store to a simulated store. The function `Helpers.get`

is:

`Definition get (ctxt : Simulations.Raw_context.t) :=`

ctxt

.(Raw_context.t.back)

.(Raw_context.back.context)

.(Context.t.Storage)

.(Context_generated.t.Block_round).

reading into a simulated store using standard record field accesses.

An axiom about a write operation is:

`Axiom update : forall (ctxt : Simulations.Raw_context.t) value,`

Storage.Block_round

.(Storage.Simple_single_data_storage.update)

(Raw_context.to_t ctxt) value =

match Helpers.get ctxt with

| Some _ =>

return? Helpers.set ctxt (Some value)

| None =>

Raw_context.storage_error_value

(Raw_context.Existing_key Helpers.name)

end.

The helper `Helpers.set`

updates the record of the simulated store and converts the result to an actual store.

We are not verifying our axioms about the storage and intend to do it later.

## Validity predicateโ

A typical statement about the absence of internal errors is the following in Apply.ex_ticket_size_is_valid:

`(** The function [ex_ticket_size] is valid. *)`

Lemma ex_ticket_size_is_valid ctxt ticket :

Raw_context.Valid.t ctxt ->

Ticket_scanner.Ex_ticket.Valid.t ticket ->

letP? '(ctxt, size) :=

Apply.ex_ticket_size ctxt ticket in

Raw_context.Valid.t ctxt /\ Pervasives.Int.Valid.t size.

There we state that the function `Apply.ex_ticket_size`

, when applied to a valid `ctxt`

and `ticket`

, both:

- returns a valid
`ctxt`

and`size`

, - does not contain internal errors

We found that is was generally convenient to state and prove both at the same time. The combinator `letP?`

is a notation for:

`Definition bind_prop {a : Set} (x : M? a) (P : a -> Prop) : Prop :=`

match x with

| Pervasives.Ok x => P x

| Pervasives.Error err => Error.not_internal err

end.

stating that the value `x`

in the error monad `M? a`

is either successful verifying the property `P`

, or an error that is not internal.

## Example of proofโ

A function such as Apply.ex_ticket_size verified above is a succession of calls to other functions, separated by the monadic combinator `let?`

of the error monad:

`Definition ex_ticket_size`

(ctxt : Alpha_context.context) (function_parameter : Ticket_scanner.ex_ticket)

: M? (Alpha_context.context * int) :=

let 'Ticket_scanner.Ex_ticket ty_value ticket := function_parameter in

let? ty_value := Script_typed_ir.ticket_t Micheline.dummy_location ty_value in

let? '(ty', ctxt) :=

Script_ir_unparser.unparse_ty Micheline.dummy_location ctxt ty_value in

let '(ty_nodes, ty_size) := Script_typed_ir_size.node_size ty' in

let ty_size := Saturation_repr.to_int ty_size in

let ty_size_cost := Script_typed_ir_size_costs.nodes_cost ty_nodes in

let? ctxt := Alpha_context.Gas.consume ctxt ty_size_cost in

(* ... *)

We split these calls with the lemma split_letP:

`Lemma split_letP {a b : Set}`

(x : M? a) (f : a -> M? b) (P : a -> Prop) (Q : b -> Prop) :

(letP? x := x in P x) ->

(forall x, P x -> letP? y := f x in Q y) ->

letP? y := (let? x := x in f x) in Q y.

This states that if we can prove that:

`x`

is valid with the post-condition`P`

,`f`

if valid with the post-condition`Q`

when given a pre-condition`P`

then `let? x := x in f x`

is valid with the post-condition `Q`

. In practice, `Q`

is given by the lemma statement and `P`

is automatically instantiated as we write the proof. Using existing proofs (or axioms) for the absence of internal errors in the functions called by `ex_ticket_size`

we can then complete the proof of the lemma.

## Conclusionโ

We are still at the beginning of verification for internal errors. One interest of this task is that we can state properties about various parts of the code. It also forces us to express the pre and post-conditions of each definition. We are now focusing on functions with a simple structure (no recursion) and will prove more complex ones later.

An example of difficulty that we faced is verifying the absence of integer overflows, when the limit is hard to reach in practice but not checked in the code.