# Internal-errors

The goal for the verification of the internal errors ๐งจ is to show that a certain class of errors is not reachable. We check the errors that are in the error monad. As we represent errors with extensible types in OCaml, we can test for the string of their name in the Coq representation. Look for examples of extensible types in the protocol and how they are translated to Coq with `Build_extensible`

to get a better understanding.

The list of forbidden errors is in Error.internal_errors. An important error is `"Asserted"`

, corresponding to `assert ...`

in OCaml that we translate to the error monad when we can. These assertions can be inserted by the OCaml developers to represent arbitrary properties. Another frequent error is `"Storage_error"`

corresponding to access to unexpected locations and such in the storage system. This forces us to properly specify the storage to show these errors are unreachable.

## Conversion of `assert false`

โ

For now, `coq-of-ocaml`

does not make monadic translations to convert the OCaml `assert`

or exceptions to the error monad. We do it by hand in our fork of the protocol. We hope to automate that translation at some point. We keep the OCaml changes on a different commit in our fork, so that we distinguish the changes for the errors and the changes to fix the translation to Coq.

## Stating the lemmasโ

We state the absence of internal errors, we make validity lemmas name `my_function_is_valid`

and use the `letP?`

combinator:

`(** 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 are many examples in Apply.v. The `letP?`

combinator checks that there is a certain property in case of success, and no internal errors in case of error.

We generally have a few validity predicates over the inputs, and then express the validity predicates over the results. We should use as many validity predicates as possible for the inputs and outputs, even if they do not seem immediately useful. This simplifies the maintenance of the proofs if they become useful later. A typical case where a new predicate is needed is when an admitted lemma is verified, and new conditions appear.

## Proofs techniquesโ

A variable that occurs often is `ctxt`

of type `Raw_context.t`

used to represent the state of the protocol. We generally use the predicate Raw_context.Valid.t on `ctxt`

and transmit it from function calls to function calls. The main code using `ctxt`

is the storage specified in Storage_generated.v. The storage properties are working on a **simulation** of the storage. To access to the simulation, you can either:

- destruct the
`Raw_context.Valid.t`

property manually, or - use the
`Raw_context.Valid.destruct_rewrite`

tactic.

There is also the Raw_context.Valid.on predicate to specify additional properties about the simulation of the context. An example can be the existence of a certain key in a certain map.

When a goal contains a `let?`

such as:

`...`

--------------------------

(1/1)

letP? ' (p, _) := (

let? ' _ := Apply.assert_tx_rollup_feature_enabled ctxt in

(* some other code... *)) in

Valid.t p

we can split it into two with Error.split_letP. We use one validity lemma per function, so here we call the validity lemma `assert_tx_rollup_feature_enabled_is_valid`

to solve the first part.