Internal-errors

Gitlab

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.