🖼️ Raw_context_intf.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
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;
  }.
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;
    

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

Module T.
  Record signature {root t tree : 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;
    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;
  }.
End T.
Definition T := @T.signature.
Arguments T {_ _ _}.