Skip to main content

💾 Storage_sigs.v

Translated OCaml

See simulations, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.
Require TezosOfOCaml.Proto_alpha.Raw_context.

The generic signature of a single data accessor (a single value bound to a specific key in the hierarchical (key x value) database).
Module Single_data_storage.
  Record signature {t value : Set} : Set := {
    t := t;
    context := t;
    
The type of the value
    value := value;
    
Tells if the data is already defined
    mem : context bool;
    
Retrieve the value from the storage bucket ; returns a {!Storage_error} if the key is not set or if the deserialisation fails
    get : context M? value;
    
Retrieves the value from the storage bucket ; returns [None] if the data is not initialized, or {!Storage_helpers.Storage_error} if the deserialisation fails
    find : context M? (option value);
    
Allocates the storage bucket and initializes it ; returns a {!Storage_error Existing_key} if the bucket exists
    init_value : context value M? Raw_context.t;
    
Updates the content of the bucket ; returns a {!Storage_Error Missing_key} if the value does not exists
    update : context value M? Raw_context.t;
    
Allocates the data and initializes it with a value ; just updates it if the bucket exists
    add : context value Raw_context.t;
    
When the value is [Some v], allocates the data and initializes it with [v] ; just updates it if the bucket exists. When the value is [None], delete the storage bucket when the value ; does nothing if the bucket does not exists.
    add_or_remove : context option value Raw_context.t;
    
Delete the storage bucket ; returns a {!Storage_error Missing_key} if the bucket does not exists
    remove_existing : context M? Raw_context.t;
    
Removes the storage bucket and its contents ; does nothing if the bucket does not exists
Restricted version of {!Indexed_data_storage} w/o iterators.
Module Non_iterable_indexed_data_storage.
  Record signature {t key value : Set} : Set := {
    t := t;
    context := t;
    
An abstract type for keys
    key := key;
    
The type of values
    value := value;
    
Tells if a given key is already bound to a storage bucket
    mem : context key bool;
    
Retrieve a value from the storage bucket at a given key ; returns {!Storage_error Missing_key} if the key is not set ; returns {!Storage_error Corrupted_data} if the deserialisation fails.
    get : context key M? value;
    
Retrieve a value from the storage bucket at a given key ; returns [None] if the value is not set ; returns {!Storage_error Corrupted_data} if the deserialisation fails.
    find : context key M? (option value);
    
Updates the content of a bucket ; returns A {!Storage_Error Missing_key} if the value does not exists.
    update : context key value M? Raw_context.t;
    
Allocates a storage bucket at the given key and initializes it ; returns a {!Storage_error Existing_key} if the bucket exists.
    init_value : context key value M? Raw_context.t;
    
Allocates a storage bucket at the given key and initializes it with a value ; just updates it if the bucket exists.
    add : context key value Raw_context.t;
    
When the value is [Some v], allocates the data and initializes it with [v] ; just updates it if the bucket exists. When the value is [None], delete the storage bucket when the value ; does nothing if the bucket does not exists.
    add_or_remove : context key option value Raw_context.t;
    
Delete a storage bucket and its contents ; returns a {!Storage_error Missing_key} if the bucket does not exists.
    remove_existing : context key M? Raw_context.t;
    
Removes a storage bucket and its contents ; does nothing if the bucket does not exists.
Variant of {!Non_iterable_indexed_data_storage} with gas accounting.
Module Non_iterable_indexed_carbonated_data_storage.
  Record signature {t key value : Set} : Set := {
    t := t;
    context := t;
    
An abstract type for keys
    key := key;
    
The type of values
    value := value;
    
Tells if a given key is already bound to a storage bucket. Consumes [Gas_repr.read_bytes_cost Z.zero].
    mem : context key M? (Raw_context.t × bool);
    
Retrieve a value from the storage bucket at a given key ; returns {!Storage_error Missing_key} if the key is not set ; returns {!Storage_error Corrupted_data} if the deserialisation fails. Consumes [Gas_repr.read_bytes_cost <size of the value>].
    get : context key M? (Raw_context.t × value);
    
Retrieve a value from the storage bucket at a given key ; returns [None] if the value is not set ; returns {!Storage_error Corrupted_data} if the deserialisation fails. Consumes [Gas_repr.read_bytes_cost <size of the value>] if present or [Gas_repr.read_bytes_cost Z.zero].
    find : context key M? (Raw_context.t × option value);
    
Updates the content of a bucket ; returns A {!Storage_Error Missing_key} if the value does not exists. Consumes serialization cost. Consumes [Gas_repr.write_bytes_cost <size of the new value>]. Returns the difference from the old to the new size.
    update : context key value M? (Raw_context.t × int);
    
Allocates a storage bucket at the given key and initializes it ; returns a {!Storage_error Existing_key} if the bucket exists. Consumes serialization cost. Consumes [Gas_repr.write_bytes_cost <size of the value>]. Returns the size.
    init_value : context key value M? (Raw_context.t × int);
    
Allocates a storage bucket at the given key and initializes it with a value ; just updates it if the bucket exists. Consumes serialization cost. Consumes [Gas_repr.write_bytes_cost <size of the new value>]. Returns the difference from the old (maybe 0) to the new size, and a boolean indicating if a value was already associated to this key.
    add : context key value M? (Raw_context.t × int × bool);
    
When the value is [Some v], allocates the data and initializes it with [v] ; just updates it if the bucket exists. When the value is [None], delete the storage bucket when the value ; does nothing if the bucket does not exists. Consumes serialization cost. Consumes the same gas cost as either {!remove} or {!init_set}. Returns the difference from the old (maybe 0) to the new size, and a boolean indicating if a value was already associated to this key.
    add_or_remove :
      context key option value M? (Raw_context.t × int × bool);
    
Delete a storage bucket and its contents ; returns a {!Storage_error Missing_key} if the bucket does not exists. Consumes [Gas_repr.write_bytes_cost Z.zero]. Returns the freed size.
    remove_existing : context key M? (Raw_context.t × int);
    
Removes a storage bucket and its contents ; does nothing if the bucket does not exists. Consumes [Gas_repr.write_bytes_cost Z.zero]. Returns the freed size, and a boolean indicating if a value was already associated to this key.
    remove : context key M? (Raw_context.t × int × bool);
    
Returns the list of all storage bucket keys. Not carbonated (i.e. gas is not consumed); use with care.
    keys_unaccounted : context M? (list key);
  }.
End Non_iterable_indexed_carbonated_data_storage.
Definition Non_iterable_indexed_carbonated_data_storage :=
  @Non_iterable_indexed_carbonated_data_storage.signature.
Arguments Non_iterable_indexed_carbonated_data_storage {_ _ _}.

Module Indexed_carbonated_data_storage.
  Record signature {t key value : Set} : Set := {
    t := t;
    context := t;
    key := key;
    value := value;
    mem : context key M? (Raw_context.t × bool);
    get : context key M? (Raw_context.t × value);
    find : context key M? (Raw_context.t × option value);
    update : context key value M? (Raw_context.t × int);
    init_value : context key value M? (Raw_context.t × int);
    add : context key value M? (Raw_context.t × int × bool);
    add_or_remove :
      context key option value M? (Raw_context.t × int × bool);
    remove_existing : context key M? (Raw_context.t × int);
    remove : context key M? (Raw_context.t × int × bool);
    keys_unaccounted : context M? (list key);
    
[list_key_values ?offset ?length storage] lists the key and value pairs of each entry in the given [storage]. The first [offset] values are ignored (if passed). Negative offsets are treated as [0]. There will be no more than [length] values in the result list (if passed). Negative values are treated as [0].
The returned {!context} takes into account gas consumption of traversing the keys and loading values.
    list_key_values :
      option int option int t M? (Raw_context.t × list (key × value));
  }.
End Indexed_carbonated_data_storage.
Definition Indexed_carbonated_data_storage :=
  @Indexed_carbonated_data_storage.signature.
Arguments Indexed_carbonated_data_storage {_ _ _}.

Module Indexed_carbonated_data_storage_INTERNAL.
  Record signature {t key value : Set} : Set := {
    t := t;
    context := t;
    key := key;
    value := value;
    mem : context key M? (Raw_context.t × bool);
    get : context key M? (Raw_context.t × value);
    find : context key M? (Raw_context.t × option value);
    update : context key value M? (Raw_context.t × int);
    init_value : context key value M? (Raw_context.t × int);
    add : context key value M? (Raw_context.t × int × bool);
    add_or_remove :
      context key option value M? (Raw_context.t × int × bool);
    remove_existing : context key M? (Raw_context.t × int);
    remove : context key M? (Raw_context.t × int × bool);
    keys_unaccounted : context M? (list key);
    list_key_values :
      option int option int t M? (Raw_context.t × list (key × value));
    fold_keys_unaccounted :
       {a : Set}, context Variant.t a (key a a) M? a;
  }.
End Indexed_carbonated_data_storage_INTERNAL.
Definition Indexed_carbonated_data_storage_INTERNAL :=
  @Indexed_carbonated_data_storage_INTERNAL.signature.
Arguments Indexed_carbonated_data_storage_INTERNAL {_ _ _}.

The generic signature of indexed data accessors (a set of values of the same type indexed by keys of the same form in the hierarchical (key x value) database).
Module Indexed_data_storage.
  Record signature {t key value : Set} : Set := {
    t := t;
    context := t;
    key := key;
    value := value;
    mem : context key bool;
    get : context key M? value;
    find : context key M? (option value);
    update : context key value M? Raw_context.t;
    init_value : context key value M? Raw_context.t;
    add : context key value Raw_context.t;
    add_or_remove : context key option value Raw_context.t;
    remove_existing : context key M? Raw_context.t;
    remove : context key Raw_context.t;
    
Empties all the keys and associated data.
    clear : context M? Raw_context.t;
    
Lists all the keys.
    keys : context M? (list key);
    
Lists all the keys and associated data.
    bindings : context M? (list (key × value));
    
Iterates over all the keys and associated data.
    fold :
       {a : Set},
      context Variant.t a (key value a M? a) M? a;
    
Iterate over all the keys.
    fold_keys :
       {a : Set}, context Variant.t a (key a M? a) M? a;
  }.
End Indexed_data_storage.
Definition Indexed_data_storage := @Indexed_data_storage.signature.
Arguments Indexed_data_storage {_ _ _}.

Module Indexed_data_snapshotable_storage.
  Record signature {snapshot key t value : Set} : Set := {
    snapshot := snapshot;
    key := key;
    t := t;
    context := t;
    value := value;
    mem : context key bool;
    get : context key M? value;
    find : context key M? (option value);
    update : context key value M? Raw_context.t;
    init_value : context key value M? Raw_context.t;
    add : context key value Raw_context.t;
    add_or_remove : context key option value Raw_context.t;
    remove_existing : context key M? Raw_context.t;
    remove : context key Raw_context.t;
    clear : context M? Raw_context.t;
    keys : context M? (list key);
    bindings : context M? (list (key × value));
    fold :
       {a : Set},
      context Variant.t a (key value a M? a) M? a;
    fold_keys :
       {a : Set}, context Variant.t a (key a M? a) M? a;
    Snapshot :
      Indexed_data_storage (t := t) (key := snapshot × key) (value := value);
    snapshot_exists : context snapshot bool;
    snapshot_value : context snapshot M? Raw_context.t;
    fold_snapshot :
       {a : Set},
      context snapshot Variant.t a (key value a M? a)
      M? a;
    delete_snapshot : context snapshot Raw_context.t;
  }.
End Indexed_data_snapshotable_storage.
Definition Indexed_data_snapshotable_storage :=
  @Indexed_data_snapshotable_storage.signature.
Arguments Indexed_data_snapshotable_storage {_ _ _ _}.

The generic signature of a data set accessor (a set of values bound to a specific key prefix in the hierarchical (key x value) database).
Module Data_set_storage.
  Record signature {t elt : Set} : Set := {
    t := t;
    context := t;
    
The type of elements.
    elt := elt;
    
Tells if a elt is a member of the set
    mem : context elt bool;
    
Adds a elt is a member of the set
    add : context elt Raw_context.t;
    
Removes a elt of the set ; does nothing if not a member
    remove : context elt Raw_context.t;
    
Returns the elements of the set, deserialized in a list in no particular order.
    elements : context M? (list elt);
    
Iterates over the elements of the set.
    fold :
       {a : Set}, context Variant.t a (elt a M? a) M? a;
    
Removes all elements in the set
    clear : context M? Raw_context.t;
  }.
End Data_set_storage.
Definition Data_set_storage := @Data_set_storage.signature.
Arguments Data_set_storage {_ _}.

Variant of {!Data_set_storage} with gas accounting.
Module Carbonated_data_set_storage.
  Record signature {t elt : Set} : Set := {
    t := t;
    context := t;
    
The type of elements.
    elt := elt;
    
Tells whether an elt is a member of the set. Consumes [Gas_repr.read_bytes_cost Z.zero]
    mem : context elt M? (Raw_context.t × bool);
    
Adds an elt as a member of the set. Consumes [Gas_repr.write_bytes_cost <size of the new value>]. Returns the the new size.
    init_value : context elt M? (Raw_context.t × int);
    
Adds an elt as a member of the set. Consumes [Gas_repr.write_bytes_cost <size of the new value>]. Returns the new size, and true if the value previously existed.
    add : context elt M? (Raw_context.t × int × bool);
    
Removes an elt from the set ; does nothing if not a member. Consumes [Gas_repr.write_bytes_cost Z.zero]. Returns the freed size, and a boolean indicating if a value was already associated to this key.
    remove : context elt M? (Raw_context.t × int × bool);
    fold_keys_unaccounted :
       {acc : Set},
      context Variant.t acc (elt acc acc) M? acc;
  }.
End Carbonated_data_set_storage.
Definition Carbonated_data_set_storage :=
  @Carbonated_data_set_storage.signature.
Arguments Carbonated_data_set_storage {_ _}.

Module NAME.
  Record signature : Set := {
    name : Raw_context.key;
  }.
End NAME.
Definition NAME := NAME.signature.

Module VALUE.
  Record signature {t : Set} : Set := {
    t := t;
    encoding : Data_encoding.t t;
  }.
End VALUE.
Definition VALUE := @VALUE.signature.
Arguments VALUE {_}.

Module REGISTER.
  Record signature : Set := {
    ghost : bool;
  }.
End REGISTER.
Definition REGISTER := REGISTER.signature.

Module Indexed_raw_context.
  Record signature {t key : Set} {ipath : Set Set} : Set := {
    t := t;
    context := t;
    key := key;
    ipath := ipath;
    clear : context Raw_context.t;
    fold_keys :
       {a : Set}, context Variant.t a (key a M? a) M? a;
    keys : context M? (list key);
    remove : context key context;
    copy : context key key M? context;
    Make_set :
       (_ : REGISTER),
       (_ : NAME), Data_set_storage (t := t) (elt := key);
    Make_map :
       {V_t : Set},
       (_ : REGISTER),
       (_ : NAME),
       (V : VALUE (t := V_t)),
      Indexed_data_storage (t := t) (key := key) (value := V.(VALUE.t));
    Make_carbonated_map :
       {V_t : Set},
       (_ : REGISTER),
       (_ : NAME),
       (V : VALUE (t := V_t)),
      Non_iterable_indexed_carbonated_data_storage (t := t) (key := key)
        (value := V.(VALUE.t));
    Raw_context : Raw_context.T (t := ipath t);
  }.
End Indexed_raw_context.
Definition Indexed_raw_context := @Indexed_raw_context.signature.
Arguments Indexed_raw_context {_ _ _}.