💾 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.V8.
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

    remove : context → Raw_context.t;
  }.
End Single_data_storage.
Definition Single_data_storage := @Single_data_storage.signature.
Arguments Single_data_storage {_ _}.

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.

    remove : context → key → Raw_context.t;
  }.
End Non_iterable_indexed_data_storage.
Definition Non_iterable_indexed_data_storage :=
  @Non_iterable_indexed_data_storage.signature.
Arguments Non_iterable_indexed_data_storage {_ _ _}.

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_storage_with_local_context_Local.
  Record signature {value local_context : Set} : Set := {
    value := value;
    local_context := local_context;
    context := local_context;
    

Tells if the data is already defined

    mem : context → bool;
    

Retrieves 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? context;
    

Updates the content of the bucket; returns a {!Storage_Error Missing_key} if the value does not exist

    update : context → value → M? context;
    

Allocates the data and initializes it with a value ; just updates it if the bucket exists

    add : context → value → context;
    

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], deletes the storage bucket; it does nothing if the bucket does not exists.

    add_or_remove : context → option value → context;
    

Delete the storage bucket ; returns a {!Storage_error Missing_key} if the bucket does not exists

    remove_existing : context → M? context;
    

Removes the storage bucket and its contents; does nothing if the bucket does not exist

    remove : context → context;
    _sig_Local : unit;
  }.
End Indexed_data_storage_with_local_context_Local.
Definition Indexed_data_storage_with_local_context_Local :=
  @Indexed_data_storage_with_local_context_Local.signature.
Arguments Indexed_data_storage_with_local_context_Local {_ _}.

Module Indexed_data_storage_with_local_context.
  Record signature {t key value local_context : 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;
    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;
    local_context := local_context;
    Local :
      Indexed_data_storage_with_local_context_Local (value := value)
        (local_context := local_context);
  }.
End Indexed_data_storage_with_local_context.
Definition Indexed_data_storage_with_local_context :=
  @Indexed_data_storage_with_local_context.signature.
Arguments Indexed_data_storage_with_local_context {_ _ _ _}.

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}
    {local_context Raw_context_local_context : Set} : Set := {
    t := t;
    context := t;
    key := key;
    ipath := ipath;
    local_context := local_context;
    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;
    with_local_context :
      ∀ {a : Set},
      context → key → (local_context → M? (local_context × a)) →
      M? (context × a);
    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_with_local_context (t := t) (key := key)
        (value := V.(VALUE.t)) (local_context := local_context);
    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) (local_context := Raw_context_local_context);
  }.
End Indexed_raw_context.
Definition Indexed_raw_context := @Indexed_raw_context.signature.
Arguments Indexed_raw_context {_ _ _ _ _}.