Skip to main content

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