🐆 Tx_rollup_l2_storage_sig.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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;
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.
[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].
[return x] is the simplest computation inside the monad [m] which simply
computes [x] and nothing else.
[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 {_}.
∀ {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].
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.
The monad of the storage backend.
[get storage key] returns the value stored in [storage] for
[key], if it exists. Returns [None] if it does not.
[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].
[remove storage key] removes [key] from the [storage].