🐆 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 {_ _}.