Skip to main content

🐆 Tx_rollup_l2_storage_sig.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

The necessary monadic operators the monad of the storage backend is required to provide.
Module SYNTAX.
  Record signature {m : Set Set} : Set := {
    m := m;
    op_letplus : {a b : Set}, m a (a b) m b;
    op_letstar : {a b : Set}, m a (a m b) m b;
    
[fail err] shortcuts the current computation by raising an error.
Said error can be handled with the [catch] combinator.
    fail : {a : Set}, Error_monad._error m a;
    
[catch p k h] tries to executes the monadic computation [p]. If [p] terminates without an error, then its result is passed to the continuation [k]. On the contrary, if an error [err] is raised, it is passed to the error handler [h].
    catch :
       {a b : Set},
      m a (a m b) (Error_monad._error m b) m b;
    
[return x] is the simplest computation inside the monad [m] which simply computes [x] and nothing else.
    _return : {a : Set}, a m a;
    
[list_fold_left_m f] is a monadic version of [List.fold_left f], wherein [f] is not a pure computation, but a computation in the monad [m].
    list_fold_left_m :
       {a b : Set}, (a b m a) a list b m a;
  }.
End SYNTAX.
Definition SYNTAX := @SYNTAX.signature.
Arguments SYNTAX {_}.

This module type is the minimal API a storage backend has to implement to be compatible with the [Tx_rollup] layer-2 implementation.
In a nutshell, the [Tx_rollup] only needs a simple key-value store, where both keys and values are raw bytes buffers. We build a type-safe abstraction on top of this simple (but potentially unsafe) interface in [Tx_rollup_l2_context].
Module STORAGE.
  Record signature {t : Set} {m : Set Set} : Set := {
    
The state of the storage.
The API adopts a functional paradigm, where the [set] function returns a new state for the storage, and where it should be possible to reuse a previous state.
    t := t;
    
The monad of the storage backend.
    m := m;
    Syntax : SYNTAX (m := fun (a : Set) ⇒ m a);
    
[get storage key] returns the value stored in [storage] for [key], if it exists. Returns [None] if it does not.
    get : t bytes m (option bytes);
    
[set storage key] computes a new state for the storage wherein the value associated to [key] is [value].
[storage] is expected to remain usable and consistent even after the execution of [set].
    set : t bytes bytes m t;
    
[remove storage key] removes [key] from the [storage].
    remove : t bytes m t;
  }.
End STORAGE.
Definition STORAGE := @STORAGE.signature.
Arguments STORAGE {_ _}.