🖼️ Raw_context_intf.v

Translated OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Storage_description.

The type for context configuration. If two trees or stores have the same configuration, they will generate the same context hash.

Definition config : Set := Context.config.

Module VIEW.
Record signature {t tree : Set} : Set := {

The type for context views.

t := t;

The type for context keys.

key := list string;

The type for context values.

value := bytes;

The type for context trees.

tree := tree;

[mem t k] is an Lwt promise that resolves to [true] iff [k] is bound to a value in [t].

mem : t → key → bool;

[mem_tree t k] is like {!mem} but for trees.

mem_tree : t → key → bool;

[get t k] is an Lwt promise that resolves to [Ok v] if [k] is bound to the value [v] in [t] and {!Storage_Error Missing_key} otherwise.

get : t → key → M ? value;

[get_tree] is like {!get} but for trees.

get_tree : t → key → M ? tree;

[find t k] is an Lwt promise that resolves to [Some v] if [k] is bound to the value [v] in [t] and [None] otherwise.

find : t → key → option value;

[find_tree t k] is like {!find} but for trees.

find_tree : t → key → option tree;

[list t key] is the list of files and sub-nodes stored under [k] in [t]. The result order is not specified but is stable.

[offset] and [length] are used for pagination.

list_value : t → option int → option int → key → list (string × tree);

[init t k v] is an Lwt promise that resolves to [Ok c] if: - [k] is unbound in [t]; [k] is bound to [v] in [c]; and [c] is similar to [t] otherwise.

It is {!Storage_error Existing_key} if [k] is already bound in [t].

init_value : t → key → value → M ? t;

[init_tree] is like {!init} but for trees.

init_tree : t → key → tree → M ? t;

[update t k v] is an Lwt promise that resolves to [Ok c] if: - [k] is bound in [t]; [k] is bound to [v] in [c]; and [c] is similar to [t] otherwise.

It is {!Storage_error Missing_key} if [k] is not already bound in [t].

update : t → key → value → M ? t;

[update_tree] is like {!update} but for trees.

update_tree : t → key → tree → M ? t;

[add t k v] is an Lwt promise that resolves to [c] such that: - [k] is bound to [v] in [c]; and [c] is similar to [t] otherwise.

If [k] was already bound in [t] to a value that is physically equal to [v], the result of the function is a promise that resolves to [t]. Otherwise, the previous binding of [k] in [t] disappears.

add : t → key → value → t;

[add_tree] is like {!add} but for trees.

add_tree : t → key → tree → t;

[remove t k v] is an Lwt promise that resolves to [c] such that: - [k] is unbound in [c]; and [c] is similar to [t] otherwise.

remove : t → key → t;

[remove_existing t k v] is an Lwt promise that resolves to [Ok c] if: - [k] is bound in [t] to a value; [k] is unbound in [c]; and [c] is similar to [t] otherwise.

remove_existing : t → key → M ? t;

[remove_existing_tree t k v] is an Lwt promise that reolves to [Ok c] if: - [k] is bound in [t] to a tree; [k] is unbound in [c]; and [c] is similar to [t] otherwise.

remove_existing_tree : t → key → M ? t;

[add_or_remove t k v] is: - [add t k x] if [v] is [Some x]; [remove t k] otherwise.

add_or_remove : t → key → option value → t;

[add_or_remove_tree t k v] is: - [add_tree t k x] if [v] is [Some x]; [remove t k] otherwise.

add_or_remove_tree : t → key → option tree → t;

[fold ?depth t root ~order ~init ~f] recursively folds over the trees and values of [t]. The [f] callbacks are called with a key relative to [root]. [f] is never called with an empty key for values; i.e., folding over a value is a no-op.

The depth is 0-indexed. If [depth] is set (by default it is not), then [f] is only called when the conditions described by the parameter is true: - [Eq d] folds over nodes and values of depth exactly [d]. [Lt d] folds over nodes and values of depth strictly less than [d]. [Le d] folds over nodes and values of depth less than or equal to [d]. [Gt d] folds over nodes and values of depth strictly more than [d]. [Ge d] folds over nodes and values of depth more than or equal to [d].

If [order] is [`Sorted] (the default), the elements are traversed in lexicographic order of their keys. For large nodes, it is memory-consuming, use [`Undefined] for a more memory efficient [fold].

    fold :
      ∀ {a : Set},
      option Context.depth → t → key → Variant.t → a →
      (key → tree → a → a) → a;

[config t] is [t]'s hash configuration.

config_value : t → config;

[length t key] is an Lwt promise that resolves to the number of files and sub-nodes stored under [k] in [t].

It is equivalent to [list t k >|= List.length] but has a constant-time complexity.

Most of the time, this function does not perform any I/O as the length is cached in the tree. It may perform one read to load the root node of the tree in case it has not been loaded already. The initial constant is the same between [list] and [length]. They both perform the same kind of I/O reads. While [list] usually performs a linear number of reads, [length] does at most one.

    length : t → key → int;
  }.
End VIEW.
Definition VIEW := @VIEW.signature.
Arguments VIEW {_ _}.

Module TREE.
  Record signature {t tree : Set} : Set := {

The type for context views.

t := t;

The type for context trees.

    tree := tree;
    key := list string;
    value := bytes;
    mem : tree → key → bool;
    mem_tree : tree → key → bool;
    get : tree → key → M ? value;
    get_tree : tree → key → M ? tree;
    find : tree → key → option value;
    find_tree : tree → key → option tree;
    list_value :
      tree → option int → option int → key → list (string × tree);
    init_value : tree → key → value → M ? tree;
    init_tree : tree → key → tree → M ? tree;
    update : tree → key → value → M ? tree;
    update_tree : tree → key → tree → M ? tree;
    add : tree → key → value → tree;
    add_tree : tree → key → tree → tree;
    remove : tree → key → tree;
    remove_existing : tree → key → M ? tree;
    remove_existing_tree : tree → key → M ? tree;
    add_or_remove : tree → key → option value → tree;
    add_or_remove_tree : tree → key → option tree → tree;
    fold :
      ∀ {a : Set},
      option Context.depth → tree → key → Variant.t → a →
      (key → tree → a → a) → a;
    config_value : tree → config;
    length : tree → key → int;

[empty _] is the empty tree.

empty : t → tree;

[is_empty t] is true iff [t] is [empty _].

is_empty : tree → bool;

[kind t] is [t]'s kind. It's either a tree node or a leaf value.

kind_value : tree → Context.Kind.t;

[to_value t] is an Lwt promise that resolves to [Some v] if [t] is a leaf tree and [None] otherwise. It is equivalent to [find t ☐].

to_value : tree → option value;

[hash t] is [t]'s Merkle hash.

hash_value : tree → Context_hash.t;

[equal x y] is true iff [x] and [y] have the same Merkle hash.

equal : tree → tree → bool;

[clear ?depth t] clears all caches in the tree [t] for subtrees with a depth higher than [depth]. If [depth] is not set, all of the subtrees are cleared.

clear : option int → tree → unit;
}.
End TREE.
Definition TREE := @TREE.signature.
Arguments TREE {_ _}.

The type for (internal) inode proofs.

These proofs encode large directories into a tree-like structure. This reflects irmin-pack's way of representing nodes and computing hashes (tree-like representations for nodes scales better than flat representations).

[length] is the total number of entries in the children of the inode. It's the size of the "flattened" version of that inode. [length] can be used to prove the correctness of operations such [Tree.length] and [Tree.list ~offset ~length] in an efficient way.

In proofs with [version.is_binary = false], an inode at depth 0 has a [length] of at least [257]. Below that threshold a [Node] tag is used in [tree]. That threshold is [3] when [version.is_binary = true].

[proofs] contains the children proofs. It is a sparse list of ['a] values. These values are associated to their index in the list, and the list is kept sorted in increasing order of indices. ['a] can be a concrete proof or a hash of that proof.

In proofs with [version.is_binary = true], inodes have at most 2 proofs (indexed 0 or 1).

In proofs with [version.is_binary = false], inodes have at most 32 proofs (indexed from 0 to 31).

Module inode.
  Record record {a index : Set} : Set := Build {
    length : int;
    proofs : list (index × a);
  }.
  Arguments record : clear implicits.
  Definition with_length {t_a t_index} length (r : record t_a t_index) :=
    Build t_a t_index length r.(proofs).
  Definition with_proofs {t_a t_index} proofs (r : record t_a t_index) :=
    Build t_a t_index r.(length) proofs.
End inode.
Definition inode := inode.record.

The type for inode extenders.

An extender is a compact representation of a sequence of [inode] which contain only one child. As for inodes, The ['a] parameter can be a concrete proof or a hash of that proof.

If an inode proof contains singleton children [i_0, ..., i_n] such as: [{length=l; proofs = [ (i_0, {proofs = ... { proofs = [ (i_n, p) ] }})]}], then it is compressed into the inode extender [{length=l; segment = [i_0;..;i_n]; proof=p}] sharing the same lenght [l] and final proof [p].

Module inode_extender.
  Record record {a index : Set} : Set := Build {
    length : int;
    segment : list index;
    proof : a;
  }.
  Arguments record : clear implicits.
  Definition with_length {t_a t_index} length (r : record t_a t_index) :=
    Build t_a t_index length r.(segment) r.(proof).
  Definition with_segment {t_a t_index} segment (r : record t_a t_index) :=
    Build t_a t_index r.(length) segment r.(proof).
  Definition with_proof {t_a t_index} proof (r : record t_a t_index) :=
    Build t_a t_index r.(length) r.(segment) proof.
End inode_extender.
Definition inode_extender := inode_extender.record.

The type for compressed and partial Merkle tree proofs.

Tree proofs do not provide any guarantee with the ordering of computations. For instance, if two effects commute, they won't be distinguishable by this kind of proofs.

[Value v] proves that a value [v] exists in the store.

[Blinded_value h] proves a value with hash [h] exists in the store.

[Node ls] proves that a a "flat" node containing the list of files [ls] exists in the store.

In proofs with [version.is_binary = true], the length of [ls] is at most 2.

In proofs with [version.is_binary = false], the length of [ls] is at most 256.

[Blinded_node h] proves that a node with hash [h] exists in the store.

[Inode i] proves that an inode [i] exists in the store.

[Extender e] proves that an inode extender [e] exist in the store.

The type for file and directory names.

step := string;

The type for values.

value := bytes;

The type of indices for inodes' children.

index := int;

The type for hashes.

    hash := Context_hash.t;
    inode := fun (a : Set) ⇒ inode a index;
    inode_extender := fun (a : Set) ⇒ inode_extender a index;
    tree := tree step value index hash;
    inode_tree := inode_tree step value index hash;

The type for kinded hashes.

kinded_hash := Context.Kind.t;

The type for elements of stream proofs.

[Value v] is a proof that the next element read in the store is the value [v].

[Node n] is a proof that the next element read in the store is the node [n].

[Inode i] is a proof that the next element read in the store is the inode [i].

[Inode_extender e] is a proof that the next element read in the store is the node extender [e].

Stream_elt := Stream_elt;

The type for stream proofs.

The sequence [e_1 ... e_n] proves that the [e_1], ..., [e_n] are read in the store in sequence.

    Stream_t := Seq.t Stream_elt;
    stream := Stream_t;

The type for proofs of kind ['a].

A proof [p] proves that the state advanced from [before p] to [after p]. [state p]'s hash is [before p], and [state p] contains the minimal information for the computation to reach [after p].

[version p] is the proof version, it packs several informations.

[is_stream] discriminates between the stream proofs and the tree proofs.

[is_binary] discriminates between proofs emitted from [Tezos_context(_memory).Context_binary] and [Tezos_context(_memory).Context].

It will also help discriminate between the data encoding techniques used.

The version is meant to be decoded and encoded using the {!Tezos_context_helpers.Context.decode_proof_version} and {!Tezos_context_helpers.Context.encode_proof_version}.

    t := t;
  }.
End PROOF.
Definition PROOF := @PROOF.signature.
Arguments PROOF {_ _}.

Module S_Local_context.
  Record signature {local_context tree : Set} : Set := {
    local_context := local_context;
    tree := tree;
    key := list string;
    value := bytes;
    t := local_context;
    mem : t → key → bool;
    mem_tree : t → key → bool;
    get : t → key → M ? value;
    get_tree : t → key → M ? tree;
    find : t → key → option value;
    find_tree : t → key → option tree;
    list_value : t → option int → option int → key → list (string × tree);
    init_value : t → key → value → M ? t;
    init_tree : t → key → tree → M ? t;
    update : t → key → value → M ? t;
    update_tree : t → key → tree → M ? t;
    add : t → key → value → t;
    add_tree : t → key → tree → t;
    remove : t → key → t;
    remove_existing : t → key → M ? t;
    remove_existing_tree : t → key → M ? t;
    add_or_remove : t → key → option value → t;
    add_or_remove_tree : t → key → option tree → t;
    fold :
      ∀ {a : Set},
      option Context.depth → t → key → Variant.t → a →
      (key → tree → a → a) → a;
    config_value : t → config;
    length : t → key → int;

Internally used in {!Storage_functors} to consume gas from within a view. May raise {!Block_quota_exceeded} or {!Operation_quota_exceeded}.

consume_gas : local_context → Gas_limit_repr.cost → M ? local_context;

Internally used in {!Storage_functors} to retrieve the full key of a partial key relative to the [local_context].

    absolute_key : local_context → key → key;
  }.
End S_Local_context.
Definition S_Local_context := @S_Local_context.signature.
Arguments S_Local_context {_ _}.

Module T.
  Record signature {root t tree local_context : Set} : Set := {

The type for root contexts.

    root := root;
    t := t;
    key := list string;
    value := bytes;
    tree := tree;
    mem : t → key → bool;
    mem_tree : t → key → bool;
    get : t → key → M ? value;
    get_tree : t → key → M ? tree;
    find : t → key → option value;
    find_tree : t → key → option tree;
    list_value : t → option int → option int → key → list (string × tree);
    init_value : t → key → value → M ? t;
    init_tree : t → key → tree → M ? t;
    update : t → key → value → M ? t;
    update_tree : t → key → tree → M ? t;
    add : t → key → value → t;
    add_tree : t → key → tree → t;
    remove : t → key → t;
    remove_existing : t → key → M ? t;
    remove_existing_tree : t → key → M ? t;
    add_or_remove : t → key → option value → t;
    add_or_remove_tree : t → key → option tree → t;
    fold :
      ∀ {a : Set},
      option Context.depth → t → key → Variant.t → a →
      (key → tree → a → a) → a;
    config_value : t → config;
    length : t → key → int;
    Tree : TREE (t := t) (tree := tree);

[verify p f] runs [f] in checking mode. [f] is a function that takes a tree as input and returns a new version of the tree and a result. [p] is a proof, that is a minimal representation of the tree that contains what [f] should be expecting.

Therefore, contrary to trees found in a storage, the contents of the trees passed to [f] may not be available. For this reason, looking up a value at some [path] can now produce three distinct outcomes: A value [v] is present in the proof [p] and returned : [find tree path] is a promise returning [Some v]; [path] is known to have no value in [tree] : [find tree path] is a promise returning [None]; and [path] is known to have a value in [tree] but [p] does not provide it because [f] should not need it: [verify] returns an error classifying [path] as an invalid path (see below).

The same semantics apply to all operations on the tree [t] passed to [f] and on all operations on the trees built from [f].

The generated tree is the tree after [f] has completed. That tree is disconnected from any storage (i.e. [index]). It is possible to run operations on it as long as they don't require loading shallowed subtrees.

The result is [Error (`Msg _)] if the proof is rejected: For tree proofs: when [p.before] is different from the hash of [p.state]; For tree and stream proofs: when [p.after] is different from the hash of [f p.state]; For tree proofs: when [f p.state] tries to access invalid paths in [p.state]; For stream proofs: when the proof is not consumed in the exact same order it was produced; For stream proofs: when the proof is too short or not empty once [f] is done.

@raise Failure if the proof version is invalid or incompatible with the verifier.

    verifier :=
      fun (proof result : Set) ⇒
        proof → (tree → tree × result) →
        Pervasives.result (tree × result) Variant.t;

The type for tree proofs.

Guarantee that the given computation performs exactly the same state operations as the generating computation, *in some order*.

tree_proof := Context.Proof.t Context.Proof.tree;

[verify_tree_proof] is the verifier of tree proofs.

verify_tree_proof : ∀ {a : Set}, verifier tree_proof a;

The type for stream proofs.

Guarantee that the given computation performs exactly the same state operations as the generating computation, in the exact same order.

stream_proof := Context.Proof.t Context.Proof.stream;

[verify_stream] is the verifier of stream proofs.

verify_stream_proof : ∀ {a : Set}, verifier stream_proof a;

The equality function for context configurations. If two context have the same configuration, they will generate the same context hashes.

equal_config : config → config → bool;

Internally used in {!Storage_functors} to escape from a view.

project : t → root;

Internally used in {!Storage_functors} to retrieve a full key from partial key relative a view.

absolute_key : t → key → key;

Raised if block gas quota is exhausted during gas consumption. Raised if operation gas quota is exhausted during gas consumption. Internally used in {!Storage_functors} to consume gas from within a view. May raise {!Block_quota_exceeded} or {!Operation_quota_exceeded}.

consume_gas : t → Gas_limit_repr.cost → M ? t;

Check if consume_gas will fail

    check_enough_gas : t → Gas_limit_repr.cost → M ? unit;
    description : Storage_description.t t;

The type for local context accesses instead from the root. In order for the carbonated storage functions to consume the gas, this has gas infomation

local_context := local_context;

[with_local_context ctxt key f] runs function [f] over the local context at path [key] of the global [ctxt]. Using the local context [f] can perform faster context accesses under [key].

    with_local_context :
      ∀ {a : Set},
      t → key → (local_context → M ? (local_context × a )) → M ? (t × a );

[Local_context] provides functions for local access from a specific directory.

    Local_context :
      S_Local_context (local_context := local_context) (tree := tree);
  }.
End T.
Definition T := @T.signature.
Arguments T {_ _ _ _}.