Skip to main content

💾 Storage_functors.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.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Misc.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_context_intf.
Require TezosOfOCaml.Proto_alpha.Storage_costs.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Module Registered.
  Definition ghost : bool := false.

  (* Registered *)
  Definition module :=
    {|
      Storage_sigs.REGISTER.ghost := ghost
    |}.
End Registered.
Definition Registered := Registered.module.

Module Ghost.
  Definition ghost : bool := true.

  (* Ghost *)
  Definition module :=
    {|
      Storage_sigs.REGISTER.ghost := ghost
    |}.
End Ghost.
Definition Ghost := Ghost.module.

Module ENCODER.
  Record signature {t : Set} : Set := {
    t := t;
    of_bytes : (unit list string) bytes M? t;
    to_bytes : t bytes;
  }.
End ENCODER.
Definition ENCODER := @ENCODER.signature.
Arguments ENCODER {_}.

Module Make_encoder.
  Class FArgs {V_t : Set} := {
    V : Storage_sigs.VALUE (t := V_t);
  }.
  Arguments Build_FArgs {_}.

  Definition of_bytes `{FArgs}
    (key_value : unit list string) (b_value : bytes)
    : M? V.(Storage_sigs.VALUE.t) :=
    match
      Data_encoding.Binary.of_bytes_opt V.(Storage_sigs.VALUE.encoding) b_value
      with
    | None
      Error_monad.error_value
        (Build_extensible "Storage_error" Raw_context.storage_error
          (Raw_context.Corrupted_data (key_value tt)))
    | Some v_valuePervasives.Ok v_value
    end.

  Definition to_bytes `{FArgs} (v_value : V.(Storage_sigs.VALUE.t)) : bytes :=
    match
      Data_encoding.Binary.to_bytes_opt None V.(Storage_sigs.VALUE.encoding)
        v_value with
    | Some b_valueb_value
    | NoneBytes.empty
    end.

  (* Make_encoder *)
  Definition functor `{FArgs} :=
    {|
      ENCODER.of_bytes := of_bytes;
      ENCODER.to_bytes := to_bytes
    |}.
End Make_encoder.
Definition Make_encoder {V_t : Set} (V : Storage_sigs.VALUE (t := V_t))
  : ENCODER (t := V.(Storage_sigs.VALUE.t)) :=
  let '_ := Make_encoder.Build_FArgs V in
  Make_encoder.functor.

Definition len_name : string := "len".

Definition data_name : string := "data".

Definition encode_len_value (bytes_value : bytes) : bytes :=
  let length := Bytes.length bytes_value in
  Data_encoding.Binary.to_bytes_exn None Data_encoding.int31 length.

Definition decode_len_value (key_value : list string) (len : bytes) : M? int :=
  match Data_encoding.Binary.of_bytes_opt Data_encoding.int31 len with
  | None
    Error_monad.error_value
      (Build_extensible "Storage_error" Raw_context.storage_error
        (Raw_context.Corrupted_data key_value))
  | Some lenreturn? len
  end.

Module Make_subcontext.
  Class FArgs {C_t C_local_context : Set} := {
    R : Storage_sigs.REGISTER;
    C : Raw_context.T (t := C_t) (local_context := C_local_context);
    N : Storage_sigs.NAME;
  }.
  Arguments Build_FArgs {_ _}.

  Definition t `{FArgs} : Set := C.(Raw_context_intf.T.t).

  Definition local_context `{FArgs} : Set :=
    C.(Raw_context_intf.T.local_context).

  Definition to_key `{FArgs} (k_value : list string) : list string :=
    Pervasives.op_at N.(Storage_sigs.NAME.name) k_value.

  Definition mem `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string) : bool :=
    C.(Raw_context_intf.T.mem) t_value (to_key k_value).

  Definition mem_tree `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string) : bool :=
    C.(Raw_context_intf.T.mem_tree) t_value (to_key k_value).

  Definition get `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    : M? Raw_context.value :=
    C.(Raw_context_intf.T.get) t_value (to_key k_value).

  Definition get_tree `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    : M? Raw_context.tree :=
    C.(Raw_context_intf.T.get_tree) t_value (to_key k_value).

  Definition find `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    : option Raw_context.value :=
    C.(Raw_context_intf.T.find) t_value (to_key k_value).

  Definition find_tree `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    : option Raw_context.tree :=
    C.(Raw_context_intf.T.find_tree) t_value (to_key k_value).

  Definition add `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    (v_value : Raw_context.value) : C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.add) t_value (to_key k_value) v_value.

  Definition add_tree `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    (v_value : Raw_context.tree) : C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.add_tree) t_value (to_key k_value) v_value.

  Definition init_value `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    (v_value : Raw_context.value) : M? C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.init_value) t_value (to_key k_value) v_value.

  Definition init_tree `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    (v_value : Raw_context.tree) : M? C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.init_tree) t_value (to_key k_value) v_value.

  Definition update `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    (v_value : Raw_context.value) : M? C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.update) t_value (to_key k_value) v_value.

  Definition update_tree `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    (v_value : Raw_context.tree) : M? C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.update_tree) t_value (to_key k_value) v_value.

  Definition add_or_remove `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    (v_value : option Raw_context.value) : C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.add_or_remove) t_value (to_key k_value) v_value.

  Definition add_or_remove_tree `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    (v_value : option Raw_context.tree) : C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.add_or_remove_tree) t_value (to_key k_value) v_value.

  Definition remove_existing `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    : M? C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.remove_existing) t_value (to_key k_value).

  Definition remove_existing_tree `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    : M? C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.remove_existing_tree) t_value (to_key k_value).

  Definition remove `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    : C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.remove) t_value (to_key k_value).

  Definition list_value `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (offset : option int)
    (length : option int) (k_value : list string)
    : list (string × Raw_context.tree) :=
    C.(Raw_context_intf.T.list_value) t_value offset length (to_key k_value).

  Definition fold `{FArgs} {A : Set}
    (depth : option Context.depth) (t_value : C.(Raw_context_intf.T.t))
    (k_value : list string) (order : Variant.t) (init_value : A)
    (f_value : Raw_context.key Raw_context.tree A A) : A :=
    C.(Raw_context_intf.T.fold) depth t_value (to_key k_value) order init_value
      f_value.

  Definition config_value `{FArgs} (t_value : C.(Raw_context_intf.T.t))
    : Raw_context_intf.config := C.(Raw_context_intf.T.config_value) t_value.

  Definition Tree `{FArgs} := C.(Raw_context_intf.T.Tree).

  Definition verify_tree_proof `{FArgs} {A : Set}
    : Context.Proof.t Context.Proof.tree
    (Raw_context.tree Raw_context.tree × A)
    Pervasives.result (Raw_context.tree × A) Variant.t :=
    C.(Raw_context_intf.T.verify_tree_proof).

  Definition verify_stream_proof `{FArgs} {A : Set}
    : Context.Proof.t Context.Proof.stream
    (Raw_context.tree Raw_context.tree × A)
    Pervasives.result (Raw_context.tree × A) Variant.t :=
    C.(Raw_context_intf.T.verify_stream_proof).

  Definition equal_config `{FArgs}
    : Raw_context_intf.config Raw_context_intf.config bool :=
    C.(Raw_context_intf.T.equal_config).

  Definition project `{FArgs} : C.(Raw_context_intf.T.t) Raw_context.root :=
    C.(Raw_context_intf.T.project).

  Definition absolute_key `{FArgs}
    (c_value : C.(Raw_context_intf.T.t)) (k_value : list string)
    : Raw_context.key :=
    C.(Raw_context_intf.T.absolute_key) c_value (to_key k_value).

  Definition consume_gas `{FArgs}
    : C.(Raw_context_intf.T.t) Gas_limit_repr.cost
    M? C.(Raw_context_intf.T.t) := C.(Raw_context_intf.T.consume_gas).

  Definition check_enough_gas `{FArgs}
    : C.(Raw_context_intf.T.t) Gas_limit_repr.cost M? unit :=
    C.(Raw_context_intf.T.check_enough_gas).

  Definition description `{FArgs}
    : Storage_description.t C.(Raw_context_intf.T.t) :=
    let description :=
      if R.(Storage_sigs.REGISTER.ghost) then
        Storage_description.create tt
      else
        C.(Raw_context_intf.T.description) in
    Storage_description.register_named_subcontext description
      N.(Storage_sigs.NAME.name).

  Definition length `{FArgs}
    : C.(Raw_context_intf.T.t) Raw_context.key int :=
    C.(Raw_context_intf.T.length).

  Definition with_local_context `{FArgs} {A : Set}
    (ctxt : C.(Raw_context_intf.T.t)) (k_value : list string)
    (f_value :
      C.(Raw_context_intf.T.local_context)
      M? (C.(Raw_context_intf.T.local_context) × A))
    : M? (C.(Raw_context_intf.T.t) × A) :=
    C.(Raw_context_intf.T.with_local_context) ctxt (to_key k_value) f_value.

  Definition Local_context `{FArgs} := C.(Raw_context_intf.T.Local_context).

  (* Make_subcontext *)
  Definition functor `{FArgs} :=
    {|
      Raw_context_intf.T.mem := mem;
      Raw_context_intf.T.mem_tree := mem_tree;
      Raw_context_intf.T.get := get;
      Raw_context_intf.T.get_tree := get_tree;
      Raw_context_intf.T.find := find;
      Raw_context_intf.T.find_tree := find_tree;
      Raw_context_intf.T.list_value := list_value;
      Raw_context_intf.T.init_value := init_value;
      Raw_context_intf.T.init_tree := init_tree;
      Raw_context_intf.T.update := update;
      Raw_context_intf.T.update_tree := update_tree;
      Raw_context_intf.T.add := add;
      Raw_context_intf.T.add_tree := add_tree;
      Raw_context_intf.T.remove := remove;
      Raw_context_intf.T.remove_existing := remove_existing;
      Raw_context_intf.T.remove_existing_tree := remove_existing_tree;
      Raw_context_intf.T.add_or_remove := add_or_remove;
      Raw_context_intf.T.add_or_remove_tree := add_or_remove_tree;
      Raw_context_intf.T.fold _ := fold;
      Raw_context_intf.T.config_value := config_value;
      Raw_context_intf.T.length := length;
      Raw_context_intf.T.Tree := Tree;
      Raw_context_intf.T.verify_tree_proof _ := verify_tree_proof;
      Raw_context_intf.T.verify_stream_proof _ := verify_stream_proof;
      Raw_context_intf.T.equal_config := equal_config;
      Raw_context_intf.T.project := project;
      Raw_context_intf.T.absolute_key := absolute_key;
      Raw_context_intf.T.consume_gas := consume_gas;
      Raw_context_intf.T.check_enough_gas := check_enough_gas;
      Raw_context_intf.T.description := description;
      Raw_context_intf.T.with_local_context _ := with_local_context;
      Raw_context_intf.T.Local_context := Local_context
    |}.
End Make_subcontext.
Definition Make_subcontext {C_t C_local_context : Set}
  (R : Storage_sigs.REGISTER)
  (C : Raw_context.T (t := C_t) (local_context := C_local_context))
  (N : Storage_sigs.NAME)
  : Raw_context.T (t := C.(Raw_context_intf.T.t))
    (local_context := C.(Raw_context_intf.T.local_context)) :=
  let '_ := Make_subcontext.Build_FArgs R C N in
  Make_subcontext.functor.

Module Make_single_data_storage.
  Class FArgs {C_t C_local_context V_t : Set} := {
    R : Storage_sigs.REGISTER;
    C : Raw_context.T (t := C_t) (local_context := C_local_context);
    N : Storage_sigs.NAME;
    V : Storage_sigs.VALUE (t := V_t);
  }.
  Arguments Build_FArgs {_ _ _}.

  Definition t `{FArgs} : Set := C.(Raw_context_intf.T.t).

  Definition context `{FArgs} : Set := t.

  Definition value `{FArgs} : Set := V.(Storage_sigs.VALUE.t).

  Definition mem `{FArgs} (t_value : C.(Raw_context_intf.T.t)) : bool :=
    C.(Raw_context_intf.T.mem) t_value N.(Storage_sigs.NAME.name).

  Definition Make_encoder_include `{FArgs} := Make_encoder V.

Inclusion of the module [Make_encoder_include]
  Definition of_bytes `{FArgs} := Make_encoder_include.(ENCODER.of_bytes).

  Definition to_bytes `{FArgs} := Make_encoder_include.(ENCODER.to_bytes).

  Definition get `{FArgs} (t_value : C.(Raw_context_intf.T.t))
    : M? V.(Storage_sigs.VALUE.t) :=
    let? b_value :=
      C.(Raw_context_intf.T.get) t_value N.(Storage_sigs.NAME.name) in
    let key_value (function_parameter : unit) : Raw_context.key :=
      let '_ := function_parameter in
      C.(Raw_context_intf.T.absolute_key) t_value N.(Storage_sigs.NAME.name) in
    of_bytes key_value b_value.

  Definition find `{FArgs} (t_value : C.(Raw_context_intf.T.t))
    : M? (option V.(Storage_sigs.VALUE.t)) :=
    let function_parameter :=
      C.(Raw_context_intf.T.find) t_value N.(Storage_sigs.NAME.name) in
    match function_parameter with
    | NoneResult.return_none
    | Some b_value
      let key_value (function_parameter : unit) : Raw_context.key :=
        let '_ := function_parameter in
        C.(Raw_context_intf.T.absolute_key) t_value N.(Storage_sigs.NAME.name)
        in
      let? v_value := of_bytes key_value b_value in
      return? (Some v_value)
    end.

  Definition init_value `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (v_value : V.(Storage_sigs.VALUE.t))
    : M? Raw_context.root :=
    let? t_value :=
      C.(Raw_context_intf.T.init_value) t_value N.(Storage_sigs.NAME.name)
        (to_bytes v_value) in
    return? (C.(Raw_context_intf.T.project) t_value).

  Definition update `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (v_value : V.(Storage_sigs.VALUE.t))
    : M? Raw_context.root :=
    let? t_value :=
      C.(Raw_context_intf.T.update) t_value N.(Storage_sigs.NAME.name)
        (to_bytes v_value) in
    return? (C.(Raw_context_intf.T.project) t_value).

  Definition add `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (v_value : V.(Storage_sigs.VALUE.t))
    : Raw_context.root :=
    let t_value :=
      C.(Raw_context_intf.T.add) t_value N.(Storage_sigs.NAME.name)
        (to_bytes v_value) in
    C.(Raw_context_intf.T.project) t_value.

  Definition add_or_remove `{FArgs}
    (t_value : C.(Raw_context_intf.T.t))
    (v_value : option V.(Storage_sigs.VALUE.t)) : Raw_context.root :=
    let t_value :=
      C.(Raw_context_intf.T.add_or_remove) t_value N.(Storage_sigs.NAME.name)
        (Option.map to_bytes v_value) in
    C.(Raw_context_intf.T.project) t_value.

  Definition remove `{FArgs} (t_value : C.(Raw_context_intf.T.t))
    : Raw_context.root :=
    let t_value :=
      C.(Raw_context_intf.T.remove) t_value N.(Storage_sigs.NAME.name) in
    C.(Raw_context_intf.T.project) t_value.

  Definition remove_existing `{FArgs} (t_value : C.(Raw_context_intf.T.t))
    : M? Raw_context.root :=
    let? t_value :=
      C.(Raw_context_intf.T.remove_existing) t_value N.(Storage_sigs.NAME.name)
      in
    return? (C.(Raw_context_intf.T.project) t_value).

  (* Make_single_data_storage *)
  Definition functor `{FArgs} :=
    {|
      Storage_sigs.Single_data_storage.mem := mem;
      Storage_sigs.Single_data_storage.get := get;
      Storage_sigs.Single_data_storage.find := find;
      Storage_sigs.Single_data_storage.init_value := init_value;
      Storage_sigs.Single_data_storage.update := update;
      Storage_sigs.Single_data_storage.add := add;
      Storage_sigs.Single_data_storage.add_or_remove := add_or_remove;
      Storage_sigs.Single_data_storage.remove_existing := remove_existing;
      Storage_sigs.Single_data_storage.remove := remove
    |}.
End Make_single_data_storage.
Definition Make_single_data_storage {C_t C_local_context V_t : Set}
  (R : Storage_sigs.REGISTER)
  (C : Raw_context.T (t := C_t) (local_context := C_local_context))
  (N : Storage_sigs.NAME) (V : Storage_sigs.VALUE (t := V_t))
  : Storage_sigs.Single_data_storage (t := C.(Raw_context_intf.T.t))
    (value := V.(Storage_sigs.VALUE.t)) :=
  let '_ := Make_single_data_storage.Build_FArgs R C N V in
  Make_single_data_storage.functor.

Module INDEX.
  Record signature {t : Set} {ipath : Set Set} : Set := {
    t := t;
    to_path : t list string list string;
    of_path : list string M? (option t);
    path_length : M? int;
    ipath := ipath;
    args : Storage_description.args;
  }.
End INDEX.
Definition INDEX := @INDEX.signature.
Arguments INDEX {_ _}.

Module Pair.
  Class FArgs {I1_t : Set} {I1_ipath : Set Set} {I2_t : Set}
    {I2_ipath : Set Set} := {
    I1 : INDEX (t := I1_t) (ipath := I1_ipath);
    I2 : INDEX (t := I2_t) (ipath := I2_ipath);
  }.
  Arguments Build_FArgs {_ _ _ _}.

  Definition t `{FArgs} : Set := I1.(INDEX.t) × I2.(INDEX.t).

  Definition path_length `{FArgs} : M? int :=
    let? p1 := I1.(INDEX.path_length) in
    let? p2 := I2.(INDEX.path_length) in
    return? (p1 +i p2).

  Definition to_path `{FArgs} (function_parameter : I1.(INDEX.t) × I2.(INDEX.t))
    : list string list string :=
    let '(x_value, y_value) := function_parameter in
    fun (l_value : list string) ⇒
      I1.(INDEX.to_path) x_value (I2.(INDEX.to_path) y_value l_value).

  Definition of_path `{FArgs} (l_value : list string)
    : M? (option (I1.(INDEX.t) × I2.(INDEX.t))) :=
    let? pl := I1.(INDEX.path_length) in
    match Misc.take pl l_value with
    | Nonereturn? None
    | Some (l1, l2)
      let? opl1 := I1.(INDEX.of_path) l1 in
      let? opl2 := I2.(INDEX.of_path) l2 in
      match (opl1, opl2) with
      | (Some x_value, Some y_value)return? (Some (x_value, y_value))
      | _return? None
      end
    end.

  Definition ipath `{FArgs} (a : Set) : Set :=
    I2.(INDEX.ipath) (I1.(INDEX.ipath) a).

  Definition args `{FArgs} : Storage_description.args :=
    Storage_description.Pair I1.(INDEX.args) I2.(INDEX.args).

  (* Pair *)
  Definition functor `{FArgs} : INDEX.signature (ipath := ipath) :=
    {|
      INDEX.to_path := to_path;
      INDEX.of_path := of_path;
      INDEX.path_length := path_length;
      INDEX.args := args
    |}.
End Pair.
Definition Pair
  {I1_t : Set} {I1_ipath : Set Set} {I2_t : Set} {I2_ipath : Set Set}
  (I1 : INDEX (t := I1_t) (ipath := I1_ipath))
  (I2 : INDEX (t := I2_t) (ipath := I2_ipath))
  : INDEX (t := I1.(INDEX.t) × I2.(INDEX.t)) (ipath := _) :=
  let '_ := Pair.Build_FArgs I1 I2 in
  Pair.functor.

Module Make_data_set_storage.
  Class FArgs {C_t C_local_context I_t : Set} {I_ipath : Set Set} := {
    C : Raw_context.T (t := C_t) (local_context := C_local_context);
    I : INDEX (t := I_t) (ipath := I_ipath);
  }.
  Arguments Build_FArgs {_ _ _ _}.

  Definition t `{FArgs} : Set := C.(Raw_context_intf.T.t).

  Definition context `{FArgs} : Set := t.

  Definition elt `{FArgs} : Set := I.(INDEX.t).

  Definition inited `{FArgs} : bytes := Bytes.of_string "inited".

  Definition mem `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t)) : bool :=
    C.(Raw_context_intf.T.mem) s_value (I.(INDEX.to_path) i_value nil).

  Definition add `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : Raw_context.root :=
    let t_value :=
      C.(Raw_context_intf.T.add) s_value (I.(INDEX.to_path) i_value nil) inited
      in
    C.(Raw_context_intf.T.project) t_value.

  Definition remove `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : Raw_context.root :=
    let t_value :=
      C.(Raw_context_intf.T.remove) s_value (I.(INDEX.to_path) i_value nil) in
    C.(Raw_context_intf.T.project) t_value.

  Definition clear `{FArgs} {A : Set} (s_value : C.(Raw_context_intf.T.t))
    : Pervasives.result Raw_context.root A :=
    let t_value := C.(Raw_context_intf.T.remove) s_value nil in
    return? (C.(Raw_context_intf.T.project) t_value).

  Definition fold `{FArgs} {A : Set}
    (s_value : C.(Raw_context_intf.T.t)) (order : Variant.t) (init_value : A)
    (f_value : I.(INDEX.t) A M? A) : M? A :=
    let? path_length := I.(INDEX.path_length) in
    C.(Raw_context_intf.T.fold) (Some (Context.Eq path_length)) s_value nil
      order (return? init_value)
      (fun (file : Raw_context.key) ⇒
        fun (tree_value : Raw_context.tree) ⇒
          fun (acc_value : M? A) ⇒
            match
              C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.kind_value)
                tree_value with
            | Context.Kind.Value
              let? of_path := I.(INDEX.of_path) file in
              match of_path with
              | Noneacc_value
              | Some p_value
                let? acc_value := acc_value in
                let? res := f_value p_value acc_value in
                return? res
              end
            | Context.Kind.Treeacc_value
            end).

  Definition elements `{FArgs} (s_value : C.(Raw_context_intf.T.t))
    : M? (list I.(INDEX.t)) :=
    fold s_value (Variant.Build "Sorted" unit tt) nil
      (fun (p_value : I.(INDEX.t)) ⇒
        fun (acc_value : list I.(INDEX.t)) ⇒ return? (cons p_value acc_value)).

  (* Make_data_set_storage *)
  Definition functor `{FArgs} :=
    {|
      Storage_sigs.Data_set_storage.mem := mem;
      Storage_sigs.Data_set_storage.add := add;
      Storage_sigs.Data_set_storage.remove := remove;
      Storage_sigs.Data_set_storage.elements := elements;
      Storage_sigs.Data_set_storage.fold _ := fold;
      Storage_sigs.Data_set_storage.clear := clear
    |}.
End Make_data_set_storage.
Definition Make_data_set_storage
  {C_t C_local_context I_t : Set} {I_ipath : Set Set}
  (C : Raw_context.T (t := C_t) (local_context := C_local_context))
  (I : INDEX (t := I_t) (ipath := I_ipath))
  : Storage_sigs.Data_set_storage (t := C.(Raw_context_intf.T.t))
    (elt := I.(INDEX.t)) :=
  let '_ := Make_data_set_storage.Build_FArgs C I in
  Make_data_set_storage.functor.

Module Make_indexed_data_storage.
  Class FArgs {C_t C_local_context I_t : Set} {I_ipath : Set Set} {V_t : Set}
    := {
    C : Raw_context.T (t := C_t) (local_context := C_local_context);
    I : INDEX (t := I_t) (ipath := I_ipath);
    V : Storage_sigs.VALUE (t := V_t);
  }.
  Arguments Build_FArgs {_ _ _ _ _}.

  Definition t `{FArgs} : Set := C.(Raw_context_intf.T.t).

  Definition context `{FArgs} : Set := t.

  Definition key `{FArgs} : Set := I.(INDEX.t).

  Definition value `{FArgs} : Set := V.(Storage_sigs.VALUE.t).

  Definition Make_encoder_include `{FArgs} := Make_encoder V.

Inclusion of the module [Make_encoder_include]
  Definition of_bytes `{FArgs} := Make_encoder_include.(ENCODER.of_bytes).

  Definition to_bytes `{FArgs} := Make_encoder_include.(ENCODER.to_bytes).

  Definition mem `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t)) : bool :=
    C.(Raw_context_intf.T.mem) s_value (I.(INDEX.to_path) i_value nil).

  Definition get `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? V.(Storage_sigs.VALUE.t) :=
    let? b_value :=
      C.(Raw_context_intf.T.get) s_value (I.(INDEX.to_path) i_value nil) in
    let key_value (function_parameter : unit) : Raw_context.key :=
      let '_ := function_parameter in
      C.(Raw_context_intf.T.absolute_key) s_value
        (I.(INDEX.to_path) i_value nil) in
    of_bytes key_value b_value.

  Definition find `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (option V.(Storage_sigs.VALUE.t)) :=
    let function_parameter :=
      C.(Raw_context_intf.T.find) s_value (I.(INDEX.to_path) i_value nil) in
    match function_parameter with
    | NoneResult.return_none
    | Some b_value
      let key_value (function_parameter : unit) : Raw_context.key :=
        let '_ := function_parameter in
        C.(Raw_context_intf.T.absolute_key) s_value
          (I.(INDEX.to_path) i_value nil) in
      let? v_value := of_bytes key_value b_value in
      return? (Some v_value)
    end.

  Definition update `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    (v_value : V.(Storage_sigs.VALUE.t)) : M? Raw_context.root :=
    let? t_value :=
      C.(Raw_context_intf.T.update) s_value (I.(INDEX.to_path) i_value nil)
        (to_bytes v_value) in
    return? (C.(Raw_context_intf.T.project) t_value).

  Definition init_value `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    (v_value : V.(Storage_sigs.VALUE.t)) : M? Raw_context.root :=
    let? t_value :=
      C.(Raw_context_intf.T.init_value) s_value (I.(INDEX.to_path) i_value nil)
        (to_bytes v_value) in
    return? (C.(Raw_context_intf.T.project) t_value).

  Definition add `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    (v_value : V.(Storage_sigs.VALUE.t)) : Raw_context.root :=
    let t_value :=
      C.(Raw_context_intf.T.add) s_value (I.(INDEX.to_path) i_value nil)
        (to_bytes v_value) in
    C.(Raw_context_intf.T.project) t_value.

  Definition add_or_remove `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    (v_value : option V.(Storage_sigs.VALUE.t)) : Raw_context.root :=
    let t_value :=
      C.(Raw_context_intf.T.add_or_remove) s_value
        (I.(INDEX.to_path) i_value nil) (Option.map to_bytes v_value) in
    C.(Raw_context_intf.T.project) t_value.

  Definition remove `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : Raw_context.root :=
    let t_value :=
      C.(Raw_context_intf.T.remove) s_value (I.(INDEX.to_path) i_value nil) in
    C.(Raw_context_intf.T.project) t_value.

  Definition remove_existing `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? Raw_context.root :=
    let? t_value :=
      C.(Raw_context_intf.T.remove_existing) s_value
        (I.(INDEX.to_path) i_value nil) in
    return? (C.(Raw_context_intf.T.project) t_value).

  Definition clear `{FArgs} {A : Set} (s_value : C.(Raw_context_intf.T.t))
    : Pervasives.result Raw_context.root A :=
    let t_value := C.(Raw_context_intf.T.remove) s_value nil in
    return? (C.(Raw_context_intf.T.project) t_value).

  Definition fold `{FArgs} {A : Set}
    (s_value : C.(Raw_context_intf.T.t)) (order : Variant.t) (init_value : A)
    (f_value : I.(INDEX.t) V.(Storage_sigs.VALUE.t) A M? A) : M? A :=
    let? path_length := I.(INDEX.path_length) in
    C.(Raw_context_intf.T.fold) (Some (Context.Eq path_length)) s_value nil
      order (return? init_value)
      (fun (file : Raw_context.key) ⇒
        fun (tree_value : Raw_context.tree) ⇒
          fun (acc_value : M? A) ⇒
            let function_parameter :=
              C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.to_value)
                tree_value in
            match function_parameter with
            | Some v_value
              let? of_path := I.(INDEX.of_path) file in
              match of_path with
              | Noneacc_value
              | Some path
                let key_value (function_parameter : unit) : Raw_context.key :=
                  let '_ := function_parameter in
                  C.(Raw_context_intf.T.absolute_key) s_value file in
                match of_bytes key_value v_value with
                | Pervasives.Ok v_value
                  let? acc_value := acc_value in
                  let? res := f_value path v_value acc_value in
                  return? res
                | Pervasives.Error _acc_value
                end
              end
            | Noneacc_value
            end).

  Definition fold_keys `{FArgs} {A : Set}
    (s_value : C.(Raw_context_intf.T.t)) (order : Variant.t) (init_value : A)
    (f_value : I.(INDEX.t) A M? A) : M? A :=
    fold s_value order init_value
      (fun (k_value : I.(INDEX.t)) ⇒
        fun (function_parameter : V.(Storage_sigs.VALUE.t)) ⇒
          let '_ := function_parameter in
          fun (acc_value : A) ⇒ f_value k_value acc_value).

  Definition bindings `{FArgs} (s_value : C.(Raw_context_intf.T.t))
    : M? (list (I.(INDEX.t) × V.(Storage_sigs.VALUE.t))) :=
    fold s_value (Variant.Build "Sorted" unit tt) nil
      (fun (p_value : I.(INDEX.t)) ⇒
        fun (v_value : V.(Storage_sigs.VALUE.t)) ⇒
          fun (acc_value : list (I.(INDEX.t) × V.(Storage_sigs.VALUE.t))) ⇒
            return? (cons (p_value, v_value) acc_value)).

  Definition keys `{FArgs} (s_value : C.(Raw_context_intf.T.t))
    : M? (list I.(INDEX.t)) :=
    fold_keys s_value (Variant.Build "Sorted" unit tt) nil
      (fun (p_value : I.(INDEX.t)) ⇒
        fun (acc_value : list I.(INDEX.t)) ⇒ return? (cons p_value acc_value)).

  (* Make_indexed_data_storage *)
  Definition functor `{FArgs} :=
    {|
      Storage_sigs.Indexed_data_storage.mem := mem;
      Storage_sigs.Indexed_data_storage.get := get;
      Storage_sigs.Indexed_data_storage.find := find;
      Storage_sigs.Indexed_data_storage.update := update;
      Storage_sigs.Indexed_data_storage.init_value := init_value;
      Storage_sigs.Indexed_data_storage.add := add;
      Storage_sigs.Indexed_data_storage.add_or_remove := add_or_remove;
      Storage_sigs.Indexed_data_storage.remove_existing := remove_existing;
      Storage_sigs.Indexed_data_storage.remove := remove;
      Storage_sigs.Indexed_data_storage.clear := clear;
      Storage_sigs.Indexed_data_storage.keys := keys;
      Storage_sigs.Indexed_data_storage.bindings := bindings;
      Storage_sigs.Indexed_data_storage.fold _ := fold;
      Storage_sigs.Indexed_data_storage.fold_keys _ := fold_keys
    |}.
End Make_indexed_data_storage.
Definition Make_indexed_data_storage
  {C_t C_local_context I_t : Set} {I_ipath : Set Set} {V_t : Set}
  (C : Raw_context.T (t := C_t) (local_context := C_local_context))
  (I : INDEX (t := I_t) (ipath := I_ipath)) (V : Storage_sigs.VALUE (t := V_t))
  : Storage_sigs.Indexed_data_storage (t := C.(Raw_context_intf.T.t))
    (key := I.(INDEX.t)) (value := V.(Storage_sigs.VALUE.t)) :=
  let '_ := Make_indexed_data_storage.Build_FArgs C I V in
  Make_indexed_data_storage.functor.

Module Make_indexed_carbonated_data_storage_INTERNAL.
  Class FArgs {C_t C_local_context I_t : Set} {I_ipath : Set Set} {V_t : Set}
    := {
    C : Raw_context.T (t := C_t) (local_context := C_local_context);
    I : INDEX (t := I_t) (ipath := I_ipath);
    V : Storage_sigs.VALUE (t := V_t);
  }.
  Arguments Build_FArgs {_ _ _ _ _}.

  Definition t `{FArgs} : Set := C.(Raw_context_intf.T.t).

  Definition context `{FArgs} : Set := t.

  Definition key `{FArgs} : Set := I.(INDEX.t).

  Definition value `{FArgs} : Set := V.(Storage_sigs.VALUE.t).

  Definition Make_encoder_include `{FArgs} := Make_encoder V.

Inclusion of the module [Make_encoder_include]
  Definition of_bytes `{FArgs} := Make_encoder_include.(ENCODER.of_bytes).

  Definition to_bytes `{FArgs} := Make_encoder_include.(ENCODER.to_bytes).

  Definition data_key `{FArgs} (i_value : I.(INDEX.t)) : list string :=
    I.(INDEX.to_path) i_value [ data_name ].

  Definition len_key `{FArgs} (i_value : I.(INDEX.t)) : list string :=
    I.(INDEX.to_path) i_value [ len_name ].

  Definition consume_mem_gas `{FArgs}
    (c_value : C.(Raw_context_intf.T.t)) (key_value : Raw_context.key)
    : M? C.(Raw_context_intf.T.t) :=
    let path_length :=
      List.length (C.(Raw_context_intf.T.absolute_key) c_value key_value) in
    C.(Raw_context_intf.T.consume_gas) c_value
      (Storage_costs.read_access path_length 0).

  Definition existing_size `{FArgs}
    (c_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (int × bool) :=
    let function_parameter :=
      C.(Raw_context_intf.T.find) c_value (len_key i_value) in
    match function_parameter with
    | Nonereturn? (0, false)
    | Some len
      let? len := decode_len_value (len_key i_value) len in
      return? (len, true)
    end.

  Definition consume_read_gas `{FArgs}
    (get : C.(Raw_context_intf.T.t) list string M? bytes)
    (c_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? C.(Raw_context_intf.T.t) :=
    let len_key := len_key i_value in
    let? len := get c_value len_key in
    let path_length :=
      List.length (C.(Raw_context_intf.T.absolute_key) c_value len_key) in
    let? read_bytes := decode_len_value len_key len in
    let cost := Storage_costs.read_access path_length read_bytes in
    C.(Raw_context_intf.T.consume_gas) c_value cost.

  Definition consume_serialize_write_gas `{FArgs} {A : Set}
    (set : C.(Raw_context_intf.T.t) list string bytes M? A)
    (c_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    (v_value : V.(Storage_sigs.VALUE.t)) : M? (A × bytes) :=
    let bytes_value := to_bytes v_value in
    let len := Bytes.length bytes_value in
    let? c_value :=
      C.(Raw_context_intf.T.consume_gas) c_value
        (Gas_limit_repr.alloc_mbytes_cost len) in
    let cost := Storage_costs.write_access len in
    let? c_value := C.(Raw_context_intf.T.consume_gas) c_value cost in
    let? c_value := set c_value (len_key i_value) (encode_len_value bytes_value)
      in
    return? (c_value, bytes_value).

  Definition consume_remove_gas `{FArgs} {A : Set}
    (del : C.(Raw_context_intf.T.t) list string M? A)
    (c_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t)) : M? A :=
    let? c_value :=
      C.(Raw_context_intf.T.consume_gas) c_value (Storage_costs.write_access 0)
      in
    del c_value (len_key i_value).

  Definition mem `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (Raw_context.root × bool) :=
    let key_value := data_key i_value in
    let? s_value := consume_mem_gas s_value key_value in
    let _exists := C.(Raw_context_intf.T.mem) s_value key_value in
    return? ((C.(Raw_context_intf.T.project) s_value), _exists).

  Definition get_unprojected `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (C.(Raw_context_intf.T.t) × V.(Storage_sigs.VALUE.t)) :=
    let? s_value := consume_read_gas C.(Raw_context_intf.T.get) s_value i_value
      in
    let? b_value := C.(Raw_context_intf.T.get) s_value (data_key i_value) in
    let key_value (function_parameter : unit) : Raw_context.key :=
      let '_ := function_parameter in
      C.(Raw_context_intf.T.absolute_key) s_value (data_key i_value) in
    let? v_value := of_bytes key_value b_value in
    return? (s_value, v_value).

  Definition get `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (Raw_context.root × V.(Storage_sigs.VALUE.t)) :=
    let? '(s_value, v_value) := get_unprojected s_value i_value in
    return? ((C.(Raw_context_intf.T.project) s_value), v_value).

  Definition find `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (Raw_context.root × option V.(Storage_sigs.VALUE.t)) :=
    let key_value := data_key i_value in
    let? s_value := consume_mem_gas s_value key_value in
    let _exists := C.(Raw_context_intf.T.mem) s_value key_value in
    if _exists then
      let? '(s_value, v_value) := get s_value i_value in
      return? (s_value, (Some v_value))
    else
      return? ((C.(Raw_context_intf.T.project) s_value), None).

  Definition update `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    (v_value : V.(Storage_sigs.VALUE.t)) : M? (Raw_context.root × int) :=
    let? '(prev_size, _) := existing_size s_value i_value in
    let? '(s_value, bytes_value) :=
      consume_serialize_write_gas C.(Raw_context_intf.T.update) s_value i_value
        v_value in
    let? t_value :=
      C.(Raw_context_intf.T.update) s_value (data_key i_value) bytes_value in
    let size_diff := (Bytes.length bytes_value) -i prev_size in
    return? ((C.(Raw_context_intf.T.project) t_value), size_diff).

  Definition init_value `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    (v_value : V.(Storage_sigs.VALUE.t)) : M? (Raw_context.root × int) :=
    let? '(s_value, bytes_value) :=
      consume_serialize_write_gas C.(Raw_context_intf.T.init_value) s_value
        i_value v_value in
    let? t_value :=
      C.(Raw_context_intf.T.init_value) s_value (data_key i_value) bytes_value
      in
    let size_value := Bytes.length bytes_value in
    return? ((C.(Raw_context_intf.T.project) t_value), size_value).

  Definition add `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    (v_value : V.(Storage_sigs.VALUE.t)) : M? (Raw_context.root × int × bool) :=
    let add {A : Set}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : Raw_context.key)
      (v_value : Raw_context.value)
      : Pervasives.result C.(Raw_context_intf.T.t) A :=
      Error_monad.op_gtpipeeq
        (C.(Raw_context_intf.T.add) s_value i_value v_value) Error_monad.ok in
    let? '(prev_size, existed) := existing_size s_value i_value in
    let? '(s_value, bytes_value) :=
      consume_serialize_write_gas add s_value i_value v_value in
    let? t_value := add s_value (data_key i_value) bytes_value in
    let size_diff := (Bytes.length bytes_value) -i prev_size in
    return? ((C.(Raw_context_intf.T.project) t_value), size_diff, existed).

  Definition remove `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (Raw_context.root × int × bool) :=
    let remove {A : Set}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : Raw_context.key)
      : Pervasives.result C.(Raw_context_intf.T.t) A :=
      Error_monad.op_gtpipeeq (C.(Raw_context_intf.T.remove) s_value i_value)
        Error_monad.ok in
    let? '(prev_size, existed) := existing_size s_value i_value in
    let? s_value := consume_remove_gas remove s_value i_value in
    let? t_value := remove s_value (data_key i_value) in
    return? ((C.(Raw_context_intf.T.project) t_value), prev_size, existed).

  Definition remove_existing `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (Raw_context.root × int) :=
    let? '(prev_size, _) := existing_size s_value i_value in
    let? s_value :=
      consume_remove_gas C.(Raw_context_intf.T.remove_existing) s_value i_value
      in
    let? t_value :=
      C.(Raw_context_intf.T.remove_existing) s_value (data_key i_value) in
    return? ((C.(Raw_context_intf.T.project) t_value), prev_size).

  Definition add_or_remove `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    (v_value : option V.(Storage_sigs.VALUE.t))
    : M? (Raw_context.root × int × bool) :=
    match v_value with
    | Noneremove s_value i_value
    | Some v_valueadd s_value i_value v_value
    end.

  Definition list_key_values `{FArgs} (op_staroptstar : option int)
    : option int C.(Raw_context_intf.T.t)
    M? (Raw_context.root × list (I.(INDEX.t) × V.(Storage_sigs.VALUE.t))) :=
    let offset :=
      match op_staroptstar with
      | Some op_starsthstarop_starsthstar
      | None ⇒ 0
      end in
    fun (op_staroptstar : option int) ⇒
      let length :=
        match op_staroptstar with
        | Some op_starsthstarop_starsthstar
        | NonePervasives.max_int
        end in
      fun (s_value : C.(Raw_context_intf.T.t)) ⇒
        let root_value {A : Set} : list A :=
          nil in
        let? path_length := I.(INDEX.path_length) in
        let depth := Context.Eq path_length in
        let size_value := C.(Raw_context_intf.T.length) s_value root_value in
        let? s_value :=
          C.(Raw_context_intf.T.consume_gas) s_value
            (Storage_costs.list_key_values_traverse size_value) in
        let? '(s_value, rev_values, _offset, _length) :=
          C.(Raw_context_intf.T.fold) (Some depth) s_value root_value
            (Variant.Build "Sorted" unit tt)
            (return? (s_value, nil, offset, length))
            (fun (file : Raw_context.key) ⇒
              fun (tree_value : Raw_context.tree) ⇒
                fun (acc_value :
                  M?
                    (C.(Raw_context_intf.T.t) ×
                      list (I.(INDEX.t) × V.(Storage_sigs.VALUE.t)) × int × int))
                  ⇒
                  match
                    ((C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.kind_value)
                      tree_value), acc_value) with
                  |
                    (Context.Kind.Tree,
                      Pervasives.Ok (s_value, rev_values, offset, length))
                    if length i 0 then
                      acc_value
                    else
                      if offset >i 0 then
                        let offset := Pervasives.pred offset in
                        Pervasives.Ok (s_value, rev_values, offset, length)
                      else
                        let? of_path := I.(INDEX.of_path) file in
                        match of_path with
                        | Noneacc_value
                        | Some key_value
                          let? '(s_value, value_value) :=
                            get_unprojected s_value key_value in
                          return?
                            (s_value,
                              (cons (key_value, value_value) rev_values), 0,
                              (Pervasives.pred length))
                        end
                  | _acc_value
                  end) in
        return?
          ((C.(Raw_context_intf.T.project) s_value), (List.rev rev_values)).

  Definition fold_keys_unaccounted `{FArgs} {A : Set}
    (s_value : C.(Raw_context_intf.T.t)) (order : Variant.t) (init_value : A)
    (f_value : I.(INDEX.t) A A) : M? A :=
    let? path_length := I.(INDEX.path_length) in
    C.(Raw_context_intf.T.fold) (Some (Context.Eq (1 +i path_length))) s_value
      nil order (return? init_value)
      (fun (file : Raw_context.key) ⇒
        fun (tree_value : Raw_context.tree) ⇒
          fun (acc_value : M? A) ⇒
            match
              C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.kind_value)
                tree_value with
            | Context.Kind.Value
              match
                ((List.rev file),
                  match List.rev file with
                  | cons last _
                    Compare.String.(Compare.S.op_eq) last len_name
                  | _false
                  end,
                  match List.rev file with
                  | cons last rest
                    Compare.String.(Compare.S.op_eq) last data_name
                  | _false
                  end) with
              | (cons last _, true, _)acc_value
              | (cons last rest, _, true)
                let file := List.rev rest in
                let? of_path := I.(INDEX.of_path) file in
                match of_path with
                | Noneacc_value
                | Some path
                  let? acc_value := acc_value in
                  let res := f_value path acc_value in
                  return? res
                end
              | (_, _, _)acc_value
              end
            | Context.Kind.Treeacc_value
            end).

  Definition keys_unaccounted `{FArgs} (s_value : C.(Raw_context_intf.T.t))
    : M? (list I.(INDEX.t)) :=
    fold_keys_unaccounted s_value (Variant.Build "Sorted" unit tt) nil
      (fun (p_value : I.(INDEX.t)) ⇒
        fun (acc_value : list I.(INDEX.t)) ⇒ cons p_value acc_value).

  (* Make_indexed_carbonated_data_storage_INTERNAL *)
  Definition functor `{FArgs} :=
    {|
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.mem := mem;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.get := get;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.find := find;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.update := update;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.init_value :=
        init_value;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.add := add;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.add_or_remove :=
        add_or_remove;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.remove_existing :=
        remove_existing;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.remove := remove;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.keys_unaccounted :=
        keys_unaccounted;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.list_key_values :=
        list_key_values;
      Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.fold_keys_unaccounted
        _ := fold_keys_unaccounted
    |}.
End Make_indexed_carbonated_data_storage_INTERNAL.
Definition Make_indexed_carbonated_data_storage_INTERNAL
  {C_t C_local_context I_t : Set} {I_ipath : Set Set} {V_t : Set}
  (C : Raw_context.T (t := C_t) (local_context := C_local_context))
  (I : INDEX (t := I_t) (ipath := I_ipath)) (V : Storage_sigs.VALUE (t := V_t))
  : Storage_sigs.Indexed_carbonated_data_storage_INTERNAL
    (t := C.(Raw_context_intf.T.t)) (key := I.(INDEX.t))
    (value := V.(Storage_sigs.VALUE.t)) :=
  let '_ := Make_indexed_carbonated_data_storage_INTERNAL.Build_FArgs C I V in
  Make_indexed_carbonated_data_storage_INTERNAL.functor.

Module Make_indexed_carbonated_data_storage.
  Class FArgs {C_t C_local_context I_t : Set} {I_ipath : Set Set} {V_t : Set}
    := {
    C : Raw_context.T (t := C_t) (local_context := C_local_context);
    I : INDEX (t := I_t) (ipath := I_ipath);
    V : Storage_sigs.VALUE (t := V_t);
  }.
  Arguments Build_FArgs {_ _ _ _ _}.

  Definition Make_indexed_carbonated_data_storage_INTERNAL_include `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL C I V.

Inclusion of the module [Make_indexed_carbonated_data_storage_INTERNAL_include]
  Definition t `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.t).

  Definition context `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.context).

  Definition key `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.key).

  Definition value `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.value).

  Definition mem `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.mem).

  Definition get `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.get).

  Definition find `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.find).

  Definition update `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.update).

  Definition init_value `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.init_value).

  Definition add `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.add).

  Definition add_or_remove `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.add_or_remove).

  Definition remove_existing `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.remove_existing).

  Definition remove `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.remove).

  Definition keys_unaccounted `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.keys_unaccounted).

  Definition list_key_values `{FArgs} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.list_key_values).

  Definition fold_keys_unaccounted `{FArgs} {a : Set} :=
    Make_indexed_carbonated_data_storage_INTERNAL_include.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.fold_keys_unaccounted)
      (a := a).

  (* Make_indexed_carbonated_data_storage *)
  Definition functor `{FArgs} :=
    {|
      Storage_sigs.Indexed_carbonated_data_storage.mem := mem;
      Storage_sigs.Indexed_carbonated_data_storage.get := get;
      Storage_sigs.Indexed_carbonated_data_storage.find := find;
      Storage_sigs.Indexed_carbonated_data_storage.update := update;
      Storage_sigs.Indexed_carbonated_data_storage.init_value := init_value;
      Storage_sigs.Indexed_carbonated_data_storage.add := add;
      Storage_sigs.Indexed_carbonated_data_storage.add_or_remove :=
        add_or_remove;
      Storage_sigs.Indexed_carbonated_data_storage.remove_existing :=
        remove_existing;
      Storage_sigs.Indexed_carbonated_data_storage.remove := remove;
      Storage_sigs.Indexed_carbonated_data_storage.keys_unaccounted :=
        keys_unaccounted;
      Storage_sigs.Indexed_carbonated_data_storage.list_key_values :=
        list_key_values
    |}.
End Make_indexed_carbonated_data_storage.
Definition Make_indexed_carbonated_data_storage
  {C_t C_local_context I_t : Set} {I_ipath : Set Set} {V_t : Set}
  (C : Raw_context.T (t := C_t) (local_context := C_local_context))
  (I : INDEX (t := I_t) (ipath := I_ipath)) (V : Storage_sigs.VALUE (t := V_t))
  : Storage_sigs.Indexed_carbonated_data_storage (t := C.(Raw_context_intf.T.t))
    (key := I.(INDEX.t)) (value := V.(Storage_sigs.VALUE.t)) :=
  let '_ := Make_indexed_carbonated_data_storage.Build_FArgs C I V in
  Make_indexed_carbonated_data_storage.functor.

Module Make_carbonated_data_set_storage.
  Class FArgs {C_t C_local_context I_t : Set} {I_ipath : Set Set} := {
    C : Raw_context.T (t := C_t) (local_context := C_local_context);
    I : INDEX (t := I_t) (ipath := I_ipath);
  }.
  Arguments Build_FArgs {_ _ _ _}.

  Module V.
    Definition t `{FArgs} : Set := unit.

    Definition encoding `{FArgs} : Data_encoding.encoding unit :=
      Data_encoding.unit_value.

    (* V *)
    Definition module `{FArgs} :=
      {|
        Storage_sigs.VALUE.encoding := encoding
      |}.
  End V.
  Definition V `{FArgs} := V.module.

  Definition M `{FArgs} := Make_indexed_carbonated_data_storage_INTERNAL C I V.

  Definition t `{FArgs} : Set := C.(Raw_context_intf.T.t).

  Definition context `{FArgs} : Set := t.

  Definition elt `{FArgs} : Set := I.(INDEX.t).

  Definition mem `{FArgs}
    : C.(Raw_context_intf.T.t) I.(INDEX.t) M? (Raw_context.t × bool) :=
    M.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.mem).

  Definition init_value `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (Raw_context.t × int) :=
    M.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.init_value) s_value
      i_value tt.

  Definition add `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (Raw_context.t × int × bool) :=
    M.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.add) s_value
      i_value tt.

  Definition remove `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    : M? (Raw_context.t × int × bool) :=
    M.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.remove) s_value
      i_value.

  Definition fold_keys_unaccounted `{FArgs} {A : Set}
    : C.(Raw_context_intf.T.t) Variant.t A (I.(INDEX.t) A A)
    M? A :=
    M.(Storage_sigs.Indexed_carbonated_data_storage_INTERNAL.fold_keys_unaccounted).

  (* Make_carbonated_data_set_storage *)
  Definition functor `{FArgs} :=
    {|
      Storage_sigs.Carbonated_data_set_storage.mem := mem;
      Storage_sigs.Carbonated_data_set_storage.init_value := init_value;
      Storage_sigs.Carbonated_data_set_storage.add := add;
      Storage_sigs.Carbonated_data_set_storage.remove := remove;
      Storage_sigs.Carbonated_data_set_storage.fold_keys_unaccounted _ :=
        fold_keys_unaccounted
    |}.
End Make_carbonated_data_set_storage.
Definition Make_carbonated_data_set_storage
  {C_t C_local_context I_t : Set} {I_ipath : Set Set}
  (C : Raw_context.T (t := C_t) (local_context := C_local_context))
  (I : INDEX (t := I_t) (ipath := I_ipath))
  : Storage_sigs.Carbonated_data_set_storage (t := C.(Raw_context_intf.T.t))
    (elt := I.(INDEX.t)) :=
  let '_ := Make_carbonated_data_set_storage.Build_FArgs C I in
  Make_carbonated_data_set_storage.functor.

Module Make_indexed_data_snapshotable_storage.
  Class FArgs {C_t C_local_context Snapshot_index_t : Set}
    {Snapshot_index_ipath : Set Set} {I_t : Set} {I_ipath : Set Set}
    {V_t : Set} := {
    C : Raw_context.T (t := C_t) (local_context := C_local_context);
    Snapshot_index :
      INDEX (t := Snapshot_index_t) (ipath := Snapshot_index_ipath);
    I : INDEX (t := I_t) (ipath := I_ipath);
    V : Storage_sigs.VALUE (t := V_t);
  }.
  Arguments Build_FArgs {_ _ _ _ _ _ _}.

  Definition snapshot `{FArgs} : Set := Snapshot_index.(INDEX.t).

  Definition data_name `{FArgs} : list string := [ "current" ].

  Definition snapshot_name `{FArgs} : list string := [ "snapshot" ].

  Definition C_data `{FArgs} :=
    Make_subcontext Registered C
      (let name := data_name in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Definition C_snapshot `{FArgs} :=
    Make_subcontext Registered C
      (let name := snapshot_name in
      {|
        Storage_sigs.NAME.name := name
      |}).

  Definition V_encoder `{FArgs} := Make_encoder V.

  Definition Make_indexed_data_storage_include `{FArgs} :=
    Make_indexed_data_storage C_data I V.

Inclusion of the module [Make_indexed_data_storage_include]
  Definition t `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.t).

  Definition context `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.context).

  Definition key `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.key).

  Definition value `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.value).

  Definition mem `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.mem).

  Definition get `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.get).

  Definition find `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.find).

  Definition update `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.update).

  Definition init_value `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.init_value).

  Definition add `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.add).

  Definition add_or_remove `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.add_or_remove).

  Definition remove_existing `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.remove_existing).

  Definition remove `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.remove).

  Definition clear `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.clear).

  Definition keys `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.keys).

  Definition bindings `{FArgs} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.bindings).

  Definition fold `{FArgs} {a : Set} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.fold)
      (a := a).

  Definition fold_keys `{FArgs} {a : Set} :=
    Make_indexed_data_storage_include.(Storage_sigs.Indexed_data_storage.fold_keys)
      (a := a).

  Definition Snapshot `{FArgs} :=
    Make_indexed_data_storage C_snapshot (Pair Snapshot_index I) V.

  Definition snapshot_path `{FArgs} (id : Snapshot_index.(INDEX.t))
    : list string :=
    Pervasives.op_at snapshot_name (Snapshot_index.(INDEX.to_path) id nil).

  Definition snapshot_exists `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (id : Snapshot_index.(INDEX.t))
    : bool := C.(Raw_context_intf.T.mem_tree) s_value (snapshot_path id).

  Definition err_missing_key `{FArgs} {A : Set} (key_value : list string)
    : M? A :=
    Raw_context.storage_error_value
      (Raw_context.Missing_key key_value Raw_context.Copy).

  Definition snapshot_value `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (id : Snapshot_index.(INDEX.t))
    : M? Raw_context.root :=
    let function_parameter := C.(Raw_context_intf.T.find_tree) s_value data_name
      in
    match function_parameter with
    | Noneerr_missing_key data_name
    | Some tree_value
      Error_monad.op_gtpipeeq
        (let t_value :=
          C.(Raw_context_intf.T.add_tree) s_value (snapshot_path id) tree_value
          in
        C.(Raw_context_intf.T.project) t_value) Error_monad.ok
    end.

  Definition fold_snapshot `{FArgs} {A : Set}
    (s_value : C.(Raw_context_intf.T.t)) (id : Snapshot_index.(INDEX.t))
    (order : Variant.t) (init_value : A)
    (f_value : I.(INDEX.t) V.(Storage_sigs.VALUE.t) A M? A) : M? A :=
    let function_parameter :=
      C.(Raw_context_intf.T.find_tree) s_value (snapshot_path id) in
    match function_parameter with
    | Noneerr_missing_key data_name
    | Some tree_value
      let? path_length := I.(INDEX.path_length) in
      C_data.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.fold)
        (Some (Context.Eq path_length)) tree_value nil order
        (Pervasives.Ok init_value)
        (fun (file : Raw_context.key) ⇒
          fun (tree_value : Raw_context.tree) ⇒
            fun (acc_value : M? A) ⇒
              let? acc_value := acc_value in
              let function_parameter :=
                C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.to_value)
                  tree_value in
              match function_parameter with
              | Some v_value
                let? of_path := I.(INDEX.of_path) file in
                match of_path with
                | Nonereturn? acc_value
                | Some path
                  let key_value (function_parameter : unit) : Raw_context.key :=
                    let '_ := function_parameter in
                    C.(Raw_context_intf.T.absolute_key) s_value file in
                  match V_encoder.(ENCODER.of_bytes) key_value v_value with
                  | Pervasives.Ok v_valuef_value path v_value acc_value
                  | Pervasives.Error _return? acc_value
                  end
                end
              | Nonereturn? acc_value
              end)
    end.

  Definition delete_snapshot `{FArgs}
    (s_value : C.(Raw_context_intf.T.t)) (id : Snapshot_index.(INDEX.t))
    : Raw_context.root :=
    let t_value := C.(Raw_context_intf.T.remove) s_value (snapshot_path id) in
    C.(Raw_context_intf.T.project) t_value.

  (* Make_indexed_data_snapshotable_storage *)
  Definition functor `{FArgs} :=
    {|
      Storage_sigs.Indexed_data_snapshotable_storage.mem := mem;
      Storage_sigs.Indexed_data_snapshotable_storage.get := get;
      Storage_sigs.Indexed_data_snapshotable_storage.find := find;
      Storage_sigs.Indexed_data_snapshotable_storage.update := update;
      Storage_sigs.Indexed_data_snapshotable_storage.init_value := init_value;
      Storage_sigs.Indexed_data_snapshotable_storage.add := add;
      Storage_sigs.Indexed_data_snapshotable_storage.add_or_remove :=
        add_or_remove;
      Storage_sigs.Indexed_data_snapshotable_storage.remove_existing :=
        remove_existing;
      Storage_sigs.Indexed_data_snapshotable_storage.remove := remove;
      Storage_sigs.Indexed_data_snapshotable_storage.clear := clear;
      Storage_sigs.Indexed_data_snapshotable_storage.keys := keys;
      Storage_sigs.Indexed_data_snapshotable_storage.bindings := bindings;
      Storage_sigs.Indexed_data_snapshotable_storage.fold _ := fold;
      Storage_sigs.Indexed_data_snapshotable_storage.fold_keys _ := fold_keys;
      Storage_sigs.Indexed_data_snapshotable_storage.Snapshot := Snapshot;
      Storage_sigs.Indexed_data_snapshotable_storage.snapshot_exists :=
        snapshot_exists;
      Storage_sigs.Indexed_data_snapshotable_storage.snapshot_value :=
        snapshot_value;
      Storage_sigs.Indexed_data_snapshotable_storage.fold_snapshot _ :=
        fold_snapshot;
      Storage_sigs.Indexed_data_snapshotable_storage.delete_snapshot :=
        delete_snapshot
    |}.
End Make_indexed_data_snapshotable_storage.
Definition Make_indexed_data_snapshotable_storage
  {C_t C_local_context Snapshot_index_t : Set}
  {Snapshot_index_ipath : Set Set} {I_t : Set} {I_ipath : Set Set}
  {V_t : Set}
  (C : Raw_context.T (t := C_t) (local_context := C_local_context))
  (Snapshot_index :
    INDEX (t := Snapshot_index_t) (ipath := Snapshot_index_ipath))
  (I : INDEX (t := I_t) (ipath := I_ipath)) (V : Storage_sigs.VALUE (t := V_t))
  : Storage_sigs.Indexed_data_snapshotable_storage
    (snapshot := Snapshot_index.(INDEX.t)) (key := I.(INDEX.t))
    (t := C.(Raw_context_intf.T.t)) (value := V.(Storage_sigs.VALUE.t)) :=
  let '_ :=
    Make_indexed_data_snapshotable_storage.Build_FArgs C Snapshot_index I V in
  Make_indexed_data_snapshotable_storage.functor.

Module Make_indexed_subcontext.
  Class FArgs {C_t C_local_context I_t : Set} {I_ipath : Set Set} := {
    C : Raw_context.T (t := C_t) (local_context := C_local_context);
    I : INDEX (t := I_t) (ipath := I_ipath);
  }.
  Arguments Build_FArgs {_ _ _ _}.

  Definition t `{FArgs} : Set := C.(Raw_context_intf.T.t).

  Definition context `{FArgs} : Set := t.

  Definition key `{FArgs} : Set := I.(INDEX.t).

  Definition ipath `{FArgs} (a : Set) : Set := I.(INDEX.ipath) a.

  Definition local_context `{FArgs} : Set :=
    C.(Raw_context_intf.T.local_context).

  Definition clear `{FArgs} (t_value : C.(Raw_context_intf.T.t))
    : Raw_context.root :=
    let t_value := C.(Raw_context_intf.T.remove) t_value nil in
    C.(Raw_context_intf.T.project) t_value.

  Definition fold_keys `{FArgs} {A : Set}
    (t_value : C.(Raw_context_intf.T.t)) (order : Variant.t) (init_value : A)
    (f_value : I.(INDEX.t) A M? A) : M? A :=
    let? path_length := I.(INDEX.path_length) in
    C.(Raw_context_intf.T.fold) (Some (Context.Eq path_length)) t_value nil
      order (return? init_value)
      (fun (path : Raw_context.key) ⇒
        fun (tree_value : Raw_context.tree) ⇒
          fun (acc_value : M? A) ⇒
            match
              C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.kind_value)
                tree_value with
            | Context.Kind.Tree
              let? of_path := I.(INDEX.of_path) path in
              match of_path with
              | Noneacc_value
              | Some path
                let? acc_value := acc_value in
                let? res := f_value path acc_value in
                return? res
              end
            | Context.Kind.Valueacc_value
            end).

  Definition keys `{FArgs} (t_value : C.(Raw_context_intf.T.t))
    : M? (list I.(INDEX.t)) :=
    fold_keys t_value (Variant.Build "Sorted" unit tt) nil
      (fun (i_value : I.(INDEX.t)) ⇒
        fun (acc_value : list I.(INDEX.t)) ⇒ return? (cons i_value acc_value)).

  Definition err_missing_key `{FArgs} {A : Set} (key_value : list string)
    : M? A :=
    Raw_context.storage_error_value
      (Raw_context.Missing_key key_value Raw_context.Copy).

  Definition copy `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (from : I.(INDEX.t))
    (to_ : I.(INDEX.t)) : M? C.(Raw_context_intf.T.t) :=
    let from := I.(INDEX.to_path) from nil in
    let to_ := I.(INDEX.to_path) to_ nil in
    let function_parameter := C.(Raw_context_intf.T.find_tree) t_value from in
    match function_parameter with
    | Noneerr_missing_key from
    | Some tree_value
      Error_monad.op_gtpipeeq
        (C.(Raw_context_intf.T.add_tree) t_value to_ tree_value) Error_monad.ok
    end.

  Definition remove `{FArgs}
    (t_value : C.(Raw_context_intf.T.t)) (k_value : I.(INDEX.t))
    : C.(Raw_context_intf.T.t) :=
    C.(Raw_context_intf.T.remove) t_value (I.(INDEX.to_path) k_value nil).

  Definition description `{FArgs}
    : Storage_description.t (I.(INDEX.ipath) C.(Raw_context_intf.T.t)) :=
    Storage_description.register_indexed_subcontext
      C.(Raw_context_intf.T.description) keys I.(INDEX.args).

  Definition unpack `{FArgs}
    : I.(INDEX.ipath) C.(Raw_context_intf.T.t)
    C.(Raw_context_intf.T.t) × I.(INDEX.t) :=
    Storage_description.unpack I.(INDEX.args).

  Definition _pack `{FArgs}
    : C.(Raw_context_intf.T.t) I.(INDEX.t)
    I.(INDEX.ipath) C.(Raw_context_intf.T.t) :=
    Storage_description._pack I.(INDEX.args).

  Module Raw_context.
    Definition t `{FArgs} : Set := I.(INDEX.ipath) C.(Raw_context_intf.T.t).

    Definition local_context `{FArgs} : Set :=
      C.(Raw_context_intf.T.local_context).

    Definition to_key `{FArgs} (i_value : I.(INDEX.t)) (k_value : list string)
      : list string := I.(INDEX.to_path) i_value k_value.

    Definition mem `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) : bool :=
      let '(t_value, i_value) := unpack c_value in
      C.(Raw_context_intf.T.mem) t_value (to_key i_value k_value).

    Definition mem_tree `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) : bool :=
      let '(t_value, i_value) := unpack c_value in
      C.(Raw_context_intf.T.mem_tree) t_value (to_key i_value k_value).

    Definition get `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) : M? Raw_context.value :=
      let '(t_value, i_value) := unpack c_value in
      C.(Raw_context_intf.T.get) t_value (to_key i_value k_value).

    Definition get_tree `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) : M? Raw_context.tree :=
      let '(t_value, i_value) := unpack c_value in
      C.(Raw_context_intf.T.get_tree) t_value (to_key i_value k_value).

    Definition find `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) : option Raw_context.value :=
      let '(t_value, i_value) := unpack c_value in
      C.(Raw_context_intf.T.find) t_value (to_key i_value k_value).

    Definition find_tree `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) : option Raw_context.tree :=
      let '(t_value, i_value) := unpack c_value in
      C.(Raw_context_intf.T.find_tree) t_value (to_key i_value k_value).

    Definition list_value `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t)) (offset : option int)
      (length : option int) (k_value : list string)
      : list (string × Raw_context.tree) :=
      let '(t_value, i_value) := unpack c_value in
      C.(Raw_context_intf.T.list_value) t_value offset length
        (to_key i_value k_value).

    Definition init_value `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) (v_value : Raw_context.value)
      : M? (I.(INDEX.ipath) C.(Raw_context_intf.T.t)) :=
      let '(t_value, i_value) := unpack c_value in
      let? t_value :=
        C.(Raw_context_intf.T.init_value) t_value (to_key i_value k_value)
          v_value in
      return? (_pack t_value i_value).

    Definition init_tree `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) (v_value : Raw_context.tree)
      : M? (I.(INDEX.ipath) C.(Raw_context_intf.T.t)) :=
      let '(t_value, i_value) := unpack c_value in
      let? t_value :=
        C.(Raw_context_intf.T.init_tree) t_value (to_key i_value k_value)
          v_value in
      return? (_pack t_value i_value).

    Definition update `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) (v_value : Raw_context.value)
      : M? (I.(INDEX.ipath) C.(Raw_context_intf.T.t)) :=
      let '(t_value, i_value) := unpack c_value in
      let? t_value :=
        C.(Raw_context_intf.T.update) t_value (to_key i_value k_value) v_value
        in
      return? (_pack t_value i_value).

    Definition update_tree `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) (v_value : Raw_context.tree)
      : M? (I.(INDEX.ipath) C.(Raw_context_intf.T.t)) :=
      let '(t_value, i_value) := unpack c_value in
      let? t_value :=
        C.(Raw_context_intf.T.update_tree) t_value (to_key i_value k_value)
          v_value in
      return? (_pack t_value i_value).

    Definition add `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) (v_value : Raw_context.value)
      : I.(INDEX.ipath) C.(Raw_context_intf.T.t) :=
      let '(t_value, i_value) := unpack c_value in
      let t_value :=
        C.(Raw_context_intf.T.add) t_value (to_key i_value k_value) v_value in
      _pack t_value i_value.

    Definition add_tree `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) (v_value : Raw_context.tree)
      : I.(INDEX.ipath) C.(Raw_context_intf.T.t) :=
      let '(t_value, i_value) := unpack c_value in
      let t_value :=
        C.(Raw_context_intf.T.add_tree) t_value (to_key i_value k_value) v_value
        in
      _pack t_value i_value.

    Definition add_or_remove `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) (v_value : option Raw_context.value)
      : I.(INDEX.ipath) C.(Raw_context_intf.T.t) :=
      let '(t_value, i_value) := unpack c_value in
      let t_value :=
        C.(Raw_context_intf.T.add_or_remove) t_value (to_key i_value k_value)
          v_value in
      _pack t_value i_value.

    Definition add_or_remove_tree `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) (v_value : option Raw_context.tree)
      : I.(INDEX.ipath) C.(Raw_context_intf.T.t) :=
      let '(t_value, i_value) := unpack c_value in
      let t_value :=
        C.(Raw_context_intf.T.add_or_remove_tree) t_value
          (to_key i_value k_value) v_value in
      _pack t_value i_value.

    Definition remove_existing `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) : M? (I.(INDEX.ipath) C.(Raw_context_intf.T.t)) :=
      let '(t_value, i_value) := unpack c_value in
      let? t_value :=
        C.(Raw_context_intf.T.remove_existing) t_value (to_key i_value k_value)
        in
      return? (_pack t_value i_value).

    Definition remove_existing_tree `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) : M? (I.(INDEX.ipath) C.(Raw_context_intf.T.t)) :=
      let '(t_value, i_value) := unpack c_value in
      let? t_value :=
        C.(Raw_context_intf.T.remove_existing_tree) t_value
          (to_key i_value k_value) in
      return? (_pack t_value i_value).

    Definition remove `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) : I.(INDEX.ipath) C.(Raw_context_intf.T.t) :=
      let '(t_value, i_value) := unpack c_value in
      let t_value :=
        C.(Raw_context_intf.T.remove) t_value (to_key i_value k_value) in
      _pack t_value i_value.

    Definition fold `{FArgs} {A : Set}
      (depth : option Context.depth)
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) (order : Variant.t) (init_value : A)
      (f_value : Raw_context.key Raw_context.tree A A) : A :=
      let '(t_value, i_value) := unpack c_value in
      C.(Raw_context_intf.T.fold) depth t_value (to_key i_value k_value) order
        init_value f_value.

    Definition config_value `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      : Raw_context_intf.config :=
      let '(t_value, _) := unpack c_value in
      C.(Raw_context_intf.T.config_value) t_value.

    Module Tree.
Inclusion of the module [C.Tree]
      Definition mem `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.mem).

      Definition mem_tree `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.mem_tree).

      Definition get `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.get).

      Definition get_tree `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.get_tree).

      Definition find `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.find).

      Definition find_tree `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.find_tree).

      Definition list_value `{FArgs} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.list_value).

      Definition init_value `{FArgs} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.init_value).

      Definition init_tree `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.init_tree).

      Definition update `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.update).

      Definition update_tree `{FArgs} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.update_tree).

      Definition add `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.add).

      Definition add_tree `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.add_tree).

      Definition remove `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.remove).

      Definition remove_existing `{FArgs} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.remove_existing).

      Definition remove_existing_tree `{FArgs} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.remove_existing_tree).

      Definition add_or_remove `{FArgs} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.add_or_remove).

      Definition add_or_remove_tree `{FArgs} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.add_or_remove_tree).

      Definition fold `{FArgs} {a : Set} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.fold) (a := a).

      Definition config_value `{FArgs} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.config_value).

      Definition length `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.length).

      (* Definition empty `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.empty). *)

      Definition is_empty `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.is_empty).

      Definition kind_value `{FArgs} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.kind_value).

      Definition to_value `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.to_value).

      Definition hash_value `{FArgs} :=
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.hash_value).

      Definition equal `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.equal).

      Definition clear `{FArgs} := C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.clear).

      Definition empty `{FArgs}
        (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
        : Raw_context.tree :=
        let '(t_value, _) := unpack c_value in
        C.(Raw_context_intf.T.Tree).(Raw_context_intf.TREE.empty) t_value.

      (* Tree *)
      Definition module `{FArgs} :=
        {|
          Raw_context_intf.TREE.mem := mem;
          Raw_context_intf.TREE.mem_tree := mem_tree;
          Raw_context_intf.TREE.get := get;
          Raw_context_intf.TREE.get_tree := get_tree;
          Raw_context_intf.TREE.find := find;
          Raw_context_intf.TREE.find_tree := find_tree;
          Raw_context_intf.TREE.list_value := list_value;
          Raw_context_intf.TREE.init_value := init_value;
          Raw_context_intf.TREE.init_tree := init_tree;
          Raw_context_intf.TREE.update := update;
          Raw_context_intf.TREE.update_tree := update_tree;
          Raw_context_intf.TREE.add := add;
          Raw_context_intf.TREE.add_tree := add_tree;
          Raw_context_intf.TREE.remove := remove;
          Raw_context_intf.TREE.remove_existing := remove_existing;
          Raw_context_intf.TREE.remove_existing_tree := remove_existing_tree;
          Raw_context_intf.TREE.add_or_remove := add_or_remove;
          Raw_context_intf.TREE.add_or_remove_tree := add_or_remove_tree;
          Raw_context_intf.TREE.fold _ := fold;
          Raw_context_intf.TREE.config_value := config_value;
          Raw_context_intf.TREE.length := length;
          Raw_context_intf.TREE.is_empty := is_empty;
          Raw_context_intf.TREE.kind_value := kind_value;
          Raw_context_intf.TREE.to_value := to_value;
          Raw_context_intf.TREE.hash_value := hash_value;
          Raw_context_intf.TREE.equal := equal;
          Raw_context_intf.TREE.clear := clear;
          Raw_context_intf.TREE.empty := empty
        |}.
    End Tree.
    Definition Tree `{FArgs} := Tree.module.

    Definition verify_tree_proof `{FArgs} {A : Set}
      : Context.Proof.t Context.Proof.tree
      (Raw_context.tree Raw_context.tree × A)
      Pervasives.result (Raw_context.tree × A) Variant.t :=
      C.(Raw_context_intf.T.verify_tree_proof).

    Definition verify_stream_proof `{FArgs} {A : Set}
      : Context.Proof.t Context.Proof.stream
      (Raw_context.tree Raw_context.tree × A)
      Pervasives.result (Raw_context.tree × A) Variant.t :=
      C.(Raw_context_intf.T.verify_stream_proof).

    Definition equal_config `{FArgs}
      : Raw_context_intf.config Raw_context_intf.config bool :=
      C.(Raw_context_intf.T.equal_config).

    Definition project `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t)) : Raw_context.root :=
      let '(t_value, _) := unpack c_value in
      C.(Raw_context_intf.T.project) t_value.

    Definition absolute_key `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string) : Raw_context.key :=
      let '(t_value, i_value) := unpack c_value in
      C.(Raw_context_intf.T.absolute_key) t_value (to_key i_value k_value).

    Definition consume_gas `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (g_value : Gas_limit_repr.cost)
      : M? (I.(INDEX.ipath) C.(Raw_context_intf.T.t)) :=
      let '(t_value, i_value) := unpack c_value in
      let? t_value := C.(Raw_context_intf.T.consume_gas) t_value g_value in
      return? (_pack t_value i_value).

    Definition check_enough_gas `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (g_value : Gas_limit_repr.cost) : M? unit :=
      let '(t_value, _i) := unpack c_value in
      C.(Raw_context_intf.T.check_enough_gas) t_value g_value.

    Definition description `{FArgs}
      : Storage_description.t (I.(INDEX.ipath) C.(Raw_context_intf.T.t)) :=
      description.

    Definition length `{FArgs}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      : Raw_context.key int :=
      let '(t_value, _i) := unpack c_value in
      C.(Raw_context_intf.T.length) t_value.

    Definition with_local_context `{FArgs} {A : Set}
      (c_value : I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (k_value : list string)
      (f_value :
        C.(Raw_context_intf.T.local_context)
        M? (C.(Raw_context_intf.T.local_context) × A))
      : M? (I.(INDEX.ipath) C.(Raw_context_intf.T.t) × A) :=
      let '(t_value, i_value) := unpack c_value in
      let? '(t_value, res) :=
        C.(Raw_context_intf.T.with_local_context) t_value
          (to_key i_value k_value) f_value in
      return? ((_pack t_value i_value), res).

    Definition Local_context `{FArgs} := C.(Raw_context_intf.T.Local_context).

    (* Raw_context *)
    Definition module `{FArgs} :=
      {|
        Raw_context_intf.T.mem := mem;
        Raw_context_intf.T.mem_tree := mem_tree;
        Raw_context_intf.T.get := get;
        Raw_context_intf.T.get_tree := get_tree;
        Raw_context_intf.T.find := find;
        Raw_context_intf.T.find_tree := find_tree;
        Raw_context_intf.T.list_value := list_value;
        Raw_context_intf.T.init_value := init_value;
        Raw_context_intf.T.init_tree := init_tree;
        Raw_context_intf.T.update := update;
        Raw_context_intf.T.update_tree := update_tree;
        Raw_context_intf.T.add := add;
        Raw_context_intf.T.add_tree := add_tree;
        Raw_context_intf.T.remove := remove;
        Raw_context_intf.T.remove_existing := remove_existing;
        Raw_context_intf.T.remove_existing_tree := remove_existing_tree;
        Raw_context_intf.T.add_or_remove := add_or_remove;
        Raw_context_intf.T.add_or_remove_tree := add_or_remove_tree;
        Raw_context_intf.T.fold _ := fold;
        Raw_context_intf.T.config_value := config_value;
        Raw_context_intf.T.length := length;
        Raw_context_intf.T.Tree := Tree;
        Raw_context_intf.T.verify_tree_proof _ := verify_tree_proof;
        Raw_context_intf.T.verify_stream_proof _ := verify_stream_proof;
        Raw_context_intf.T.equal_config := equal_config;
        Raw_context_intf.T.project := project;
        Raw_context_intf.T.absolute_key := absolute_key;
        Raw_context_intf.T.consume_gas := consume_gas;
        Raw_context_intf.T.check_enough_gas := check_enough_gas;
        Raw_context_intf.T.description := description;
        Raw_context_intf.T.with_local_context _ := with_local_context;
        Raw_context_intf.T.Local_context := Local_context
      |}.
  End Raw_context.
  Definition Raw_context `{FArgs}
    : Raw_context.T (t := I.(INDEX.ipath) C.(Raw_context_intf.T.t))
      (local_context := C.(Raw_context_intf.T.local_context)) :=
    Raw_context.module.

  Definition with_local_context `{FArgs} {A : Set}
    (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
    (f_value :
      C.(Raw_context_intf.T.local_context)
      M? (C.(Raw_context_intf.T.local_context) × A))
    : M? (C.(Raw_context_intf.T.t) × A) :=
    let? '(c_value, x_value) :=
      Raw_context.(Raw_context_intf.T.with_local_context)
        (_pack s_value i_value) nil f_value in
    let '(s_value, _) := unpack c_value in
    return? (s_value, x_value).

  Module Make_set.
    Class FArgs `{FArgs} := {
      R : Storage_sigs.REGISTER;
      N : Storage_sigs.NAME;
    }.
    Arguments Build_FArgs {_ _ _ _ _}.

    Definition t `{FArgs} : Set := C.(Raw_context_intf.T.t).

    Definition context `{FArgs} : Set := t.

    Definition elt `{FArgs} : Set := I.(INDEX.t).

    Definition inited `{FArgs} : bytes := Bytes.of_string "inited".

    Definition mem `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t)) : bool :=
      Raw_context.(Raw_context_intf.T.mem) (_pack s_value i_value)
        N.(Storage_sigs.NAME.name).

    Definition add `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : Raw_context.root :=
      let c_value :=
        Raw_context.(Raw_context_intf.T.add) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) inited in
      let '(s_value, _) := unpack c_value in
      C.(Raw_context_intf.T.project) s_value.

    Definition remove `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : Raw_context.root :=
      let c_value :=
        Raw_context.(Raw_context_intf.T.remove) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) in
      let '(s_value, _) := unpack c_value in
      C.(Raw_context_intf.T.project) s_value.

    Definition clear `{FArgs} (s_value : C.(Raw_context_intf.T.t))
      : M? Raw_context.root :=
      let? t_value :=
        fold_keys s_value (Variant.Build "Sorted" unit tt) s_value
          (fun (i_value : I.(INDEX.t)) ⇒
            fun (s_value : C.(Raw_context_intf.T.t)) ⇒
              let c_value :=
                Raw_context.(Raw_context_intf.T.remove) (_pack s_value i_value)
                  N.(Storage_sigs.NAME.name) in
              let '(s_value, _) := unpack c_value in
              return? s_value) in
      return? (C.(Raw_context_intf.T.project) t_value).

    Definition fold `{FArgs} {A : Set}
      (s_value : C.(Raw_context_intf.T.t)) (order : Variant.t) (init_value : A)
      (f_value : I.(INDEX.t) A M? A) : M? A :=
      fold_keys s_value order init_value
        (fun (i_value : I.(INDEX.t)) ⇒
          fun (acc_value : A) ⇒
            let function_parameter := mem s_value i_value in
            match function_parameter with
            | truef_value i_value acc_value
            | falsereturn? acc_value
            end).

    Definition elements `{FArgs} (s_value : C.(Raw_context_intf.T.t))
      : M? (list I.(INDEX.t)) :=
      fold s_value (Variant.Build "Sorted" unit tt) nil
        (fun (p_value : I.(INDEX.t)) ⇒
          fun (acc_value : list I.(INDEX.t)) ⇒ return? (cons p_value acc_value)).

    (* Make_set *)
    Definition functor `{FArgs} :=
      {|
        Storage_sigs.Data_set_storage.mem := mem;
        Storage_sigs.Data_set_storage.add := add;
        Storage_sigs.Data_set_storage.remove := remove;
        Storage_sigs.Data_set_storage.elements := elements;
        Storage_sigs.Data_set_storage.fold _ := fold;
        Storage_sigs.Data_set_storage.clear := clear
      |}.
  End Make_set.
  Definition Make_set `{FArgs}
    (R : Storage_sigs.REGISTER) (N : Storage_sigs.NAME)
    : Storage_sigs.Data_set_storage (t := t) (elt := key) :=
    let '_ := Make_set.Build_FArgs R N in
    Make_set.functor.

  Module Make_map.
    Class FArgs `{FArgs} {V_t : Set} := {
      R : Storage_sigs.REGISTER;
      N : Storage_sigs.NAME;
      V : Storage_sigs.VALUE (t := V_t);
    }.
    Arguments Build_FArgs {_ _ _ _ _ _}.

    Definition t `{FArgs} : Set := C.(Raw_context_intf.T.t).

    Definition context `{FArgs} : Set := t.

    Definition key `{FArgs} : Set := I.(INDEX.t).

    Definition value `{FArgs} : Set := V.(Storage_sigs.VALUE.t).

    Definition local_context `{FArgs} : Set := local_context.

    Definition Make_encoder_include `{FArgs} := Make_encoder V.

Inclusion of the module [Make_encoder_include]
    Definition of_bytes `{FArgs} := Make_encoder_include.(ENCODER.of_bytes).

    Definition to_bytes `{FArgs} := Make_encoder_include.(ENCODER.to_bytes).

    Definition mem `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t)) : bool :=
      Raw_context.(Raw_context_intf.T.mem) (_pack s_value i_value)
        N.(Storage_sigs.NAME.name).

    Definition get `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : M? V.(Storage_sigs.VALUE.t) :=
      let? b_value :=
        Raw_context.(Raw_context_intf.T.get) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) in
      let key_value (function_parameter : unit) : Raw_context.key :=
        let '_ := function_parameter in
        Raw_context.(Raw_context_intf.T.absolute_key) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) in
      of_bytes key_value b_value.

    Definition find `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : M? (option V.(Storage_sigs.VALUE.t)) :=
      let function_parameter :=
        Raw_context.(Raw_context_intf.T.find) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) in
      match function_parameter with
      | NoneResult.return_none
      | Some b_value
        let key_value (function_parameter : unit) : Raw_context.key :=
          let '_ := function_parameter in
          Raw_context.(Raw_context_intf.T.absolute_key) (_pack s_value i_value)
            N.(Storage_sigs.NAME.name) in
        let? v_value := of_bytes key_value b_value in
        return? (Some v_value)
      end.

    Definition update `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      (v_value : V.(Storage_sigs.VALUE.t)) : M? Raw_context.root :=
      let? c_value :=
        Raw_context.(Raw_context_intf.T.update) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) (to_bytes v_value) in
      let '(s_value, _) := unpack c_value in
      return? (C.(Raw_context_intf.T.project) s_value).

    Definition init_value `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      (v_value : V.(Storage_sigs.VALUE.t)) : M? Raw_context.root :=
      let? c_value :=
        Raw_context.(Raw_context_intf.T.init_value) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) (to_bytes v_value) in
      let '(s_value, _) := unpack c_value in
      return? (C.(Raw_context_intf.T.project) s_value).

    Definition add `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      (v_value : V.(Storage_sigs.VALUE.t)) : Raw_context.root :=
      let c_value :=
        Raw_context.(Raw_context_intf.T.add) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) (to_bytes v_value) in
      let '(s_value, _) := unpack c_value in
      C.(Raw_context_intf.T.project) s_value.

    Definition add_or_remove `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      (v_value : option V.(Storage_sigs.VALUE.t)) : Raw_context.root :=
      let c_value :=
        Raw_context.(Raw_context_intf.T.add_or_remove) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) (Option.map to_bytes v_value) in
      let '(s_value, _) := unpack c_value in
      C.(Raw_context_intf.T.project) s_value.

    Definition remove `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : Raw_context.root :=
      let c_value :=
        Raw_context.(Raw_context_intf.T.remove) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) in
      let '(s_value, _) := unpack c_value in
      C.(Raw_context_intf.T.project) s_value.

    Definition remove_existing `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : M? Raw_context.root :=
      let? c_value :=
        Raw_context.(Raw_context_intf.T.remove_existing) (_pack s_value i_value)
          N.(Storage_sigs.NAME.name) in
      let '(s_value, _) := unpack c_value in
      return? (C.(Raw_context_intf.T.project) s_value).

    Definition clear `{FArgs} (s_value : C.(Raw_context_intf.T.t))
      : M? Raw_context.root :=
      let? t_value :=
        fold_keys s_value (Variant.Build "Sorted" unit tt) s_value
          (fun (i_value : I.(INDEX.t)) ⇒
            fun (s_value : C.(Raw_context_intf.T.t)) ⇒
              let c_value :=
                Raw_context.(Raw_context_intf.T.remove) (_pack s_value i_value)
                  N.(Storage_sigs.NAME.name) in
              let '(s_value, _) := unpack c_value in
              return? s_value) in
      return? (C.(Raw_context_intf.T.project) t_value).

    Definition fold `{FArgs} {A : Set}
      (s_value : C.(Raw_context_intf.T.t)) (order : Variant.t) (init_value : A)
      (f_value : I.(INDEX.t) V.(Storage_sigs.VALUE.t) A M? A) : M? A :=
      fold_keys s_value order init_value
        (fun (i_value : I.(INDEX.t)) ⇒
          fun (acc_value : A) ⇒
            let function_parameter := get s_value i_value in
            match function_parameter with
            | Pervasives.Error _return? acc_value
            | Pervasives.Ok v_valuef_value i_value v_value acc_value
            end).

    Definition bindings `{FArgs} (s_value : C.(Raw_context_intf.T.t))
      : M? (list (I.(INDEX.t) × V.(Storage_sigs.VALUE.t))) :=
      fold s_value (Variant.Build "Sorted" unit tt) nil
        (fun (p_value : I.(INDEX.t)) ⇒
          fun (v_value : V.(Storage_sigs.VALUE.t)) ⇒
            fun (acc_value : list (I.(INDEX.t) × V.(Storage_sigs.VALUE.t))) ⇒
              return? (cons (p_value, v_value) acc_value)).

    Definition fold_keys `{FArgs} {A : Set}
      (s_value : C.(Raw_context_intf.T.t)) (order : Variant.t) (init_value : A)
      (f_value : I.(INDEX.t) A M? A) : M? A :=
      fold_keys s_value order init_value
        (fun (i_value : I.(INDEX.t)) ⇒
          fun (acc_value : A) ⇒
            let function_parameter := mem s_value i_value in
            match function_parameter with
            | falsereturn? acc_value
            | truef_value i_value acc_value
            end).

    Definition keys `{FArgs} (s_value : C.(Raw_context_intf.T.t))
      : M? (list I.(INDEX.t)) :=
      fold_keys s_value (Variant.Build "Sorted" unit tt) nil
        (fun (p_value : I.(INDEX.t)) ⇒
          fun (acc_value : list I.(INDEX.t)) ⇒ return? (cons p_value acc_value)).

    Module Local.
      Definition context `{FArgs} : Set := C.(Raw_context_intf.T.local_context).

      Definition mem `{FArgs} (local : C.(Raw_context_intf.T.local_context))
        : bool :=
        Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.mem)
          local N.(Storage_sigs.NAME.name).

      Definition get `{FArgs} (local : C.(Raw_context_intf.T.local_context))
        : M? V.(Storage_sigs.VALUE.t) :=
        let r_value :=
          Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.get)
            local N.(Storage_sigs.NAME.name) in
        let key_value (function_parameter : unit) : list string :=
          let '_ := function_parameter in
          Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.absolute_key)
            local N.(Storage_sigs.NAME.name) in
        Error_monad.op_gtgtquestion r_value (of_bytes key_value).

      Definition find `{FArgs} (local : C.(Raw_context_intf.T.local_context))
        : M? (option V.(Storage_sigs.VALUE.t)) :=
        let function_parameter :=
          Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.find)
            local N.(Storage_sigs.NAME.name) in
        match function_parameter with
        | NoneResult.return_none
        | Some b_value
          let key_value (function_parameter : unit) : list string :=
            let '_ := function_parameter in
            Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.absolute_key)
              local N.(Storage_sigs.NAME.name) in
          let? v_value := of_bytes key_value b_value in
          return? (Some v_value)
        end.

      Definition init_value `{FArgs}
        (local : C.(Raw_context_intf.T.local_context))
        (v_value : V.(Storage_sigs.VALUE.t))
        : M? C.(Raw_context_intf.T.local_context) :=
        Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.init_value)
          local N.(Storage_sigs.NAME.name) (to_bytes v_value).

      Definition update `{FArgs}
        (local : C.(Raw_context_intf.T.local_context))
        (v_value : V.(Storage_sigs.VALUE.t))
        : M? C.(Raw_context_intf.T.local_context) :=
        Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.update)
          local N.(Storage_sigs.NAME.name) (to_bytes v_value).

      Definition add `{FArgs}
        (local : C.(Raw_context_intf.T.local_context))
        (v_value : V.(Storage_sigs.VALUE.t))
        : C.(Raw_context_intf.T.local_context) :=
        Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.add)
          local N.(Storage_sigs.NAME.name) (to_bytes v_value).

      Definition add_or_remove `{FArgs}
        (local : C.(Raw_context_intf.T.local_context))
        (vo : option V.(Storage_sigs.VALUE.t))
        : C.(Raw_context_intf.T.local_context) :=
        Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.add_or_remove)
          local N.(Storage_sigs.NAME.name) (Option.map to_bytes vo).

      Definition remove_existing `{FArgs}
        (local : C.(Raw_context_intf.T.local_context))
        : M? C.(Raw_context_intf.T.local_context) :=
        Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.remove_existing)
          local N.(Storage_sigs.NAME.name).

      Definition remove `{FArgs} (local : C.(Raw_context_intf.T.local_context))
        : C.(Raw_context_intf.T.local_context) :=
        Raw_context.(Raw_context_intf.T.Local_context).(Raw_context_intf.S_Local_context.remove)
          local N.(Storage_sigs.NAME.name).

      Definition _sig_Local `{FArgs} : unit := tt.

      (* Local *)
      Definition module `{FArgs} :=
        {|
          Storage_sigs.Indexed_data_storage_with_local_context_Local.mem := mem;
          Storage_sigs.Indexed_data_storage_with_local_context_Local.get := get;
          Storage_sigs.Indexed_data_storage_with_local_context_Local.find :=
            find;
          Storage_sigs.Indexed_data_storage_with_local_context_Local.init_value :=
            init_value;
          Storage_sigs.Indexed_data_storage_with_local_context_Local.update :=
            update;
          Storage_sigs.Indexed_data_storage_with_local_context_Local.add := add;
          Storage_sigs.Indexed_data_storage_with_local_context_Local.add_or_remove :=
            add_or_remove;
          Storage_sigs.Indexed_data_storage_with_local_context_Local.remove_existing :=
            remove_existing;
          Storage_sigs.Indexed_data_storage_with_local_context_Local.remove :=
            remove;
          Storage_sigs.Indexed_data_storage_with_local_context_Local._sig_Local :=
            _sig_Local
        |}.
    End Local.
    Definition Local `{FArgs} := Local.module.

    (* Make_map *)
    Definition functor `{FArgs} :=
      {|
        Storage_sigs.Indexed_data_storage_with_local_context.mem := mem;
        Storage_sigs.Indexed_data_storage_with_local_context.get := get;
        Storage_sigs.Indexed_data_storage_with_local_context.find := find;
        Storage_sigs.Indexed_data_storage_with_local_context.update := update;
        Storage_sigs.Indexed_data_storage_with_local_context.init_value :=
          init_value;
        Storage_sigs.Indexed_data_storage_with_local_context.add := add;
        Storage_sigs.Indexed_data_storage_with_local_context.add_or_remove :=
          add_or_remove;
        Storage_sigs.Indexed_data_storage_with_local_context.remove_existing :=
          remove_existing;
        Storage_sigs.Indexed_data_storage_with_local_context.remove := remove;
        Storage_sigs.Indexed_data_storage_with_local_context.clear := clear;
        Storage_sigs.Indexed_data_storage_with_local_context.keys := keys;
        Storage_sigs.Indexed_data_storage_with_local_context.bindings :=
          bindings;
        Storage_sigs.Indexed_data_storage_with_local_context.fold _ := fold;
        Storage_sigs.Indexed_data_storage_with_local_context.fold_keys _ :=
          fold_keys;
        Storage_sigs.Indexed_data_storage_with_local_context.Local := Local
      |}.
  End Make_map.
  Definition Make_map `{FArgs} {V_t : Set}
    (R : Storage_sigs.REGISTER) (N : Storage_sigs.NAME)
    (V : Storage_sigs.VALUE (t := V_t))
    : Storage_sigs.Indexed_data_storage_with_local_context (t := t) (key := key)
      (value := V.(Storage_sigs.VALUE.t)) (local_context := local_context) :=
    let '_ := Make_map.Build_FArgs R N V in
    Make_map.functor.

  Module Make_carbonated_map.
    Class FArgs `{FArgs} {V_t : Set} := {
      R : Storage_sigs.REGISTER;
      N : Storage_sigs.NAME;
      V : Storage_sigs.VALUE (t := V_t);
    }.
    Arguments Build_FArgs {_ _ _ _ _ _}.

    Definition t `{FArgs} : Set := C.(Raw_context_intf.T.t).

    Definition context `{FArgs} : Set := t.

    Definition key `{FArgs} : Set := I.(INDEX.t).

    Definition value `{FArgs} : Set := V.(Storage_sigs.VALUE.t).

    Definition Make_encoder_include `{FArgs} := Make_encoder V.

Inclusion of the module [Make_encoder_include]
    Definition of_bytes `{FArgs} := Make_encoder_include.(ENCODER.of_bytes).

    Definition to_bytes `{FArgs} := Make_encoder_include.(ENCODER.to_bytes).

    Definition len_name `{FArgs} : list string :=
      cons len_name N.(Storage_sigs.NAME.name).

    Definition data_name `{FArgs} : list string :=
      cons data_name N.(Storage_sigs.NAME.name).

    Definition consume_mem_gas `{FArgs}
      (c_value : Raw_context.(Raw_context_intf.T.t))
      : M? Raw_context.(Raw_context_intf.T.t) :=
      let path_length :=
        (List.length
          (Raw_context.(Raw_context_intf.T.absolute_key) c_value
            N.(Storage_sigs.NAME.name))) +i 1 in
      Raw_context.(Raw_context_intf.T.consume_gas) c_value
        (Storage_costs.read_access path_length 0).

    Definition existing_size `{FArgs}
      (c_value : Raw_context.(Raw_context_intf.T.t)) : M? (int × bool) :=
      let function_parameter :=
        Raw_context.(Raw_context_intf.T.find) c_value len_name in
      match function_parameter with
      | Nonereturn? (0, false)
      | Some len
        let? len := decode_len_value len_name len in
        return? (len, true)
      end.

    Definition consume_read_gas `{FArgs}
      (get : Raw_context.(Raw_context_intf.T.t) list string M? bytes)
      (c_value : Raw_context.(Raw_context_intf.T.t))
      : M? Raw_context.(Raw_context_intf.T.t) :=
      let path_length :=
        (List.length
          (Raw_context.(Raw_context_intf.T.absolute_key) c_value
            N.(Storage_sigs.NAME.name))) +i 1 in
      let? len := get c_value len_name in
      let? read_bytes := decode_len_value len_name len in
      Raw_context.(Raw_context_intf.T.consume_gas) c_value
        (Storage_costs.read_access path_length read_bytes).

    Definition consume_write_gas `{FArgs} {A : Set}
      (set : Raw_context.(Raw_context_intf.T.t) list string bytes M? A)
      (c_value : Raw_context.(Raw_context_intf.T.t))
      (v_value : V.(Storage_sigs.VALUE.t)) : M? (A × bytes) :=
      let bytes_value := to_bytes v_value in
      let len := Bytes.length bytes_value in
      let? c_value :=
        Raw_context.(Raw_context_intf.T.consume_gas) c_value
          (Storage_costs.write_access len) in
      let? c_value := set c_value len_name (encode_len_value bytes_value) in
      return? (c_value, bytes_value).

    Definition consume_remove_gas `{FArgs} {A : Set}
      (del : Raw_context.(Raw_context_intf.T.t) list string M? A)
      (c_value : Raw_context.(Raw_context_intf.T.t)) : M? A :=
      let? c_value :=
        Raw_context.(Raw_context_intf.T.consume_gas) c_value
          (Storage_costs.write_access 0) in
      del c_value len_name.

    Definition mem `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : M? (Raw_context.root × bool) :=
      let? c_value := consume_mem_gas (_pack s_value i_value) in
      let res := Raw_context.(Raw_context_intf.T.mem) c_value data_name in
      return? ((Raw_context.(Raw_context_intf.T.project) c_value), res).

    Definition get `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : M? (Raw_context.root × V.(Storage_sigs.VALUE.t)) :=
      let? c_value :=
        consume_read_gas Raw_context.(Raw_context_intf.T.get)
          (_pack s_value i_value) in
      let? b_value := Raw_context.(Raw_context_intf.T.get) c_value data_name in
      let key_value (function_parameter : unit) : Raw_context.key :=
        let '_ := function_parameter in
        Raw_context.(Raw_context_intf.T.absolute_key) c_value data_name in
      let? v_value := of_bytes key_value b_value in
      return? ((Raw_context.(Raw_context_intf.T.project) c_value), v_value).

    Definition find `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : M? (Raw_context.root × option V.(Storage_sigs.VALUE.t)) :=
      let? c_value := consume_mem_gas (_pack s_value i_value) in
      let '(s_value, _) := unpack c_value in
      let _exists :=
        Raw_context.(Raw_context_intf.T.mem) (_pack s_value i_value) data_name
        in
      if _exists then
        let? '(s_value, v_value) := get s_value i_value in
        return? (s_value, (Some v_value))
      else
        return? ((C.(Raw_context_intf.T.project) s_value), None).

    Definition update `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      (v_value : V.(Storage_sigs.VALUE.t)) : M? (Raw_context.root × int) :=
      let? '(prev_size, _) := existing_size (_pack s_value i_value) in
      let? '(c_value, bytes_value) :=
        consume_write_gas Raw_context.(Raw_context_intf.T.update)
          (_pack s_value i_value) v_value in
      let? c_value :=
        Raw_context.(Raw_context_intf.T.update) c_value data_name bytes_value in
      let size_diff := (Bytes.length bytes_value) -i prev_size in
      return? ((Raw_context.(Raw_context_intf.T.project) c_value), size_diff).

    Definition init_value `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      (v_value : V.(Storage_sigs.VALUE.t)) : M? (Raw_context.root × int) :=
      let? '(c_value, bytes_value) :=
        consume_write_gas Raw_context.(Raw_context_intf.T.init_value)
          (_pack s_value i_value) v_value in
      let? c_value :=
        Raw_context.(Raw_context_intf.T.init_value) c_value data_name
          bytes_value in
      let size_value := Bytes.length bytes_value in
      return? ((Raw_context.(Raw_context_intf.T.project) c_value), size_value).

    Definition add `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      (v_value : V.(Storage_sigs.VALUE.t))
      : M? (Raw_context.root × int × bool) :=
      let add {A : Set}
        (c_value : Raw_context.(Raw_context_intf.T.t))
        (k_value : Raw_context.key) (v_value : Raw_context.value)
        : Pervasives.result Raw_context.(Raw_context_intf.T.t) A :=
        Error_monad.op_gtpipeeq
          (Raw_context.(Raw_context_intf.T.add) c_value k_value v_value)
          Error_monad.ok in
      let? '(prev_size, existed) := existing_size (_pack s_value i_value) in
      let? '(c_value, bytes_value) :=
        consume_write_gas add (_pack s_value i_value) v_value in
      let? c_value := add c_value data_name bytes_value in
      let size_diff := (Bytes.length bytes_value) -i prev_size in
      return?
        ((Raw_context.(Raw_context_intf.T.project) c_value), size_diff, existed).

    Definition remove `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : M? (Raw_context.root × int × bool) :=
      let remove {A : Set}
        (c_value : Raw_context.(Raw_context_intf.T.t))
        (k_value : Raw_context.key)
        : Pervasives.result Raw_context.(Raw_context_intf.T.t) A :=
        Error_monad.op_gtpipeeq
          (Raw_context.(Raw_context_intf.T.remove) c_value k_value)
          Error_monad.ok in
      let? '(prev_size, existed) := existing_size (_pack s_value i_value) in
      let? c_value := consume_remove_gas remove (_pack s_value i_value) in
      let? c_value := remove c_value data_name in
      return?
        ((Raw_context.(Raw_context_intf.T.project) c_value), prev_size, existed).

    Definition remove_existing `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      : M? (Raw_context.root × int) :=
      let? '(prev_size, _) := existing_size (_pack s_value i_value) in
      let? c_value :=
        consume_remove_gas Raw_context.(Raw_context_intf.T.remove_existing)
          (_pack s_value i_value) in
      let? c_value :=
        Raw_context.(Raw_context_intf.T.remove_existing) c_value data_name in
      return? ((Raw_context.(Raw_context_intf.T.project) c_value), prev_size).

    Definition add_or_remove `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t))
      (v_value : option V.(Storage_sigs.VALUE.t))
      : M? (Raw_context.root × int × bool) :=
      match v_value with
      | Noneremove s_value i_value
      | Some v_valueadd s_value i_value v_value
      end.

    Definition mem_unaccounted `{FArgs}
      (s_value : C.(Raw_context_intf.T.t)) (i_value : I.(INDEX.t)) : bool :=
      Raw_context.(Raw_context_intf.T.mem) (_pack s_value i_value) data_name.

    Definition fold_keys_unaccounted `{FArgs} {A : Set}
      (s_value : C.(Raw_context_intf.T.t)) (order : Variant.t) (init_value : A)
      (f_value : I.(INDEX.t) A M? A) : M? A :=
      fold_keys s_value order init_value
        (fun (i_value : I.(INDEX.t)) ⇒
          fun (acc_value : A) ⇒
            let function_parameter := mem_unaccounted s_value i_value in
            match function_parameter with
            | falsereturn? acc_value
            | truef_value i_value acc_value
            end).

    Definition keys_unaccounted `{FArgs} (s_value : C.(Raw_context_intf.T.t))
      : M? (list I.(INDEX.t)) :=
      fold_keys_unaccounted s_value (Variant.Build "Sorted" unit tt) nil
        (fun (p_value : I.(INDEX.t)) ⇒
          fun (acc_value : list I.(INDEX.t)) ⇒ return? (cons p_value acc_value)).

    (* Make_carbonated_map *)
    Definition functor `{FArgs} :=
      {|
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem := mem;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get := get;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find := find;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update :=
          update;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value :=
          init_value;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add := add;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add_or_remove :=
          add_or_remove;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove_existing :=
          remove_existing;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove :=
          remove;
        Storage_sigs.Non_iterable_indexed_carbonated_data_storage.keys_unaccounted :=
          keys_unaccounted
      |}.
  End Make_carbonated_map.
  Definition Make_carbonated_map `{FArgs} {V_t : Set}
    (R : Storage_sigs.REGISTER) (N : Storage_sigs.NAME)
    (V : Storage_sigs.VALUE (t := V_t))
    : Storage_sigs.Non_iterable_indexed_carbonated_data_storage (t := t)
      (key := key) (value := V.(Storage_sigs.VALUE.t)) :=
    let '_ := Make_carbonated_map.Build_FArgs R N V in
    Make_carbonated_map.functor.

  (* Make_indexed_subcontext *)
  Definition functor `{FArgs} :=
    {|
      Storage_sigs.Indexed_raw_context.clear := clear;
      Storage_sigs.Indexed_raw_context.fold_keys _ := fold_keys;
      Storage_sigs.Indexed_raw_context.keys := keys;
      Storage_sigs.Indexed_raw_context.remove := remove;
      Storage_sigs.Indexed_raw_context.copy := copy;
      Storage_sigs.Indexed_raw_context.with_local_context _ :=
        with_local_context;
      Storage_sigs.Indexed_raw_context.Make_set := Make_set;
      Storage_sigs.Indexed_raw_context.Make_map _ := Make_map;
      Storage_sigs.Indexed_raw_context.Make_carbonated_map _ :=
        Make_carbonated_map;
      Storage_sigs.Indexed_raw_context.Raw_context := Raw_context
    |}.
End Make_indexed_subcontext.
Definition Make_indexed_subcontext
  {C_t C_local_context I_t : Set} {I_ipath : Set Set}
  (C : Raw_context.T (t := C_t) (local_context := C_local_context))
  (I : INDEX (t := I_t) (ipath := I_ipath))
  : Storage_sigs.Indexed_raw_context (t := C.(Raw_context_intf.T.t))
    (key := I.(INDEX.t)) (ipath := fun (a : Set) ⇒ I.(INDEX.ipath) a)
    (local_context := C.(Raw_context_intf.T.local_context))
    (Raw_context_local_context := _) :=
  let '_ := Make_indexed_subcontext.Build_FArgs C I in
  Make_indexed_subcontext.functor.

Module WRAPPER.
  Record signature {t key : Set} : Set := {
    t := t;
    key := key;
    wrap : t key;
    unwrap : key option t;
  }.
End WRAPPER.
Definition WRAPPER := @WRAPPER.signature.
Arguments WRAPPER {_ _}.

Module Wrap_indexed_data_storage.
  Class FArgs {C_t C_key C_value K_t : Set} := {
    C :
      Storage_sigs.Indexed_data_storage (t := C_t) (key := C_key)
        (value := C_value);
    K : WRAPPER (t := K_t) (key := C.(Storage_sigs.Indexed_data_storage.key));
  }.
  Arguments Build_FArgs {_ _ _ _}.

  Definition t `{FArgs} : Set := C.(Storage_sigs.Indexed_data_storage.t).

  Definition context `{FArgs} : Set := C.(Storage_sigs.Indexed_data_storage.t).

  Definition key `{FArgs} : Set := K.(WRAPPER.t).

  Definition value `{FArgs} : Set :=
    C.(Storage_sigs.Indexed_data_storage.value).

  Definition mem `{FArgs}
    (ctxt : C.(Storage_sigs.Indexed_data_storage.t)) (k_value : K.(WRAPPER.t))
    : bool :=
    C.(Storage_sigs.Indexed_data_storage.mem) ctxt (K.(WRAPPER.wrap) k_value).

  Definition get `{FArgs}
    (ctxt : C.(Storage_sigs.Indexed_data_storage.t)) (k_value : K.(WRAPPER.t))
    : M? C.(Storage_sigs.Indexed_data_storage.value) :=
    C.(Storage_sigs.Indexed_data_storage.get) ctxt (K.(WRAPPER.wrap) k_value).

  Definition find `{FArgs}
    (ctxt : C.(Storage_sigs.Indexed_data_storage.t)) (k_value : K.(WRAPPER.t))
    : M? (option C.(Storage_sigs.Indexed_data_storage.value)) :=
    C.(Storage_sigs.Indexed_data_storage.find) ctxt (K.(WRAPPER.wrap) k_value).

  Definition update `{FArgs}
    (ctxt : C.(Storage_sigs.Indexed_data_storage.t)) (k_value : K.(WRAPPER.t))
    (v_value : C.(Storage_sigs.Indexed_data_storage.value))
    : M? Raw_context.t :=
    C.(Storage_sigs.Indexed_data_storage.update) ctxt (K.(WRAPPER.wrap) k_value)
      v_value.

  Definition init_value `{FArgs}
    (ctxt : C.(Storage_sigs.Indexed_data_storage.t)) (k_value : K.(WRAPPER.t))
    (v_value : C.(Storage_sigs.Indexed_data_storage.value))
    : M? Raw_context.t :=
    C.(Storage_sigs.Indexed_data_storage.init_value) ctxt
      (K.(WRAPPER.wrap) k_value) v_value.

  Definition add `{FArgs}
    (ctxt : C.(Storage_sigs.Indexed_data_storage.t)) (k_value : K.(WRAPPER.t))
    (v_value : C.(Storage_sigs.Indexed_data_storage.value)) : Raw_context.t :=
    C.(Storage_sigs.Indexed_data_storage.add) ctxt (K.(WRAPPER.wrap) k_value)
      v_value.

  Definition add_or_remove `{FArgs}
    (ctxt : C.(Storage_sigs.Indexed_data_storage.t)) (k_value : K.(WRAPPER.t))
    (v_value : option C.(Storage_sigs.Indexed_data_storage.value))
    : Raw_context.t :=
    C.(Storage_sigs.Indexed_data_storage.add_or_remove) ctxt
      (K.(WRAPPER.wrap) k_value) v_value.

  Definition remove_existing `{FArgs}
    (ctxt : C.(Storage_sigs.Indexed_data_storage.t)) (k_value : K.(WRAPPER.t))
    : M? Raw_context.t :=
    C.(Storage_sigs.Indexed_data_storage.remove_existing) ctxt
      (K.(WRAPPER.wrap) k_value).

  Definition remove `{FArgs}
    (ctxt : C.(Storage_sigs.Indexed_data_storage.t)) (k_value : K.(WRAPPER.t))
    : Raw_context.t :=
    C.(Storage_sigs.Indexed_data_storage.remove) ctxt (K.(WRAPPER.wrap) k_value).

  Definition clear `{FArgs} (ctxt : C.(Storage_sigs.Indexed_data_storage.t))
    : M? Raw_context.t := C.(Storage_sigs.Indexed_data_storage.clear) ctxt.

  Definition fold `{FArgs} {A : Set}
    (ctxt : C.(Storage_sigs.Indexed_data_storage.t)) (order : Variant.t)
    (init_value : A)
    (f_value :
      K.(WRAPPER.t) C.(Storage_sigs.Indexed_data_storage.value) A M? A)
    : M? A :=
    C.(Storage_sigs.Indexed_data_storage.fold) ctxt order init_value
      (fun (k_value : C.(Storage_sigs.Indexed_data_storage.key)) ⇒
        fun (v_value : C.(Storage_sigs.Indexed_data_storage.value)) ⇒
          fun (acc_value : A) ⇒
            match K.(WRAPPER.unwrap) k_value with
            | Nonereturn? acc_value
            | Some k_valuef_value k_value v_value acc_value
            end).

  Definition bindings `{FArgs}
    (s_value : C.(Storage_sigs.Indexed_data_storage.t))
    : M? (list (K.(WRAPPER.t) × C.(Storage_sigs.Indexed_data_storage.value))) :=
    fold s_value (Variant.Build "Sorted" unit tt) nil
      (fun (p_value : K.(WRAPPER.t)) ⇒
        fun (v_value : C.(Storage_sigs.Indexed_data_storage.value)) ⇒
          fun (acc_value :
            list (K.(WRAPPER.t) × C.(Storage_sigs.Indexed_data_storage.value)))
            ⇒ return? (cons (p_value, v_value) acc_value)).

  Definition fold_keys `{FArgs} {A : Set}
    (s_value : C.(Storage_sigs.Indexed_data_storage.t)) (order : Variant.t)
    (init_value : A) (f_value : K.(WRAPPER.t) A M? A) : M? A :=
    C.(Storage_sigs.Indexed_data_storage.fold_keys) s_value order init_value
      (fun (k_value : C.(Storage_sigs.Indexed_data_storage.key)) ⇒
        fun (acc_value : A) ⇒
          match K.(WRAPPER.unwrap) k_value with
          | Nonereturn? acc_value
          | Some k_valuef_value k_value acc_value
          end).

  Definition keys `{FArgs} (s_value : C.(Storage_sigs.Indexed_data_storage.t))
    : M? (list K.(WRAPPER.t)) :=
    fold_keys s_value (Variant.Build "Sorted" unit tt) nil
      (fun (p_value : K.(WRAPPER.t)) ⇒
        fun (acc_value : list K.(WRAPPER.t)) ⇒ return? (cons p_value acc_value)).

  (* Wrap_indexed_data_storage *)
  Definition functor `{FArgs} :=
    {|
      Storage_sigs.Indexed_data_storage.mem := mem;
      Storage_sigs.Indexed_data_storage.get := get;
      Storage_sigs.Indexed_data_storage.find := find;
      Storage_sigs.Indexed_data_storage.update := update;
      Storage_sigs.Indexed_data_storage.init_value := init_value;
      Storage_sigs.Indexed_data_storage.add := add;
      Storage_sigs.Indexed_data_storage.add_or_remove := add_or_remove;
      Storage_sigs.Indexed_data_storage.remove_existing := remove_existing;
      Storage_sigs.Indexed_data_storage.remove := remove;
      Storage_sigs.Indexed_data_storage.clear := clear;
      Storage_sigs.Indexed_data_storage.keys := keys;
      Storage_sigs.Indexed_data_storage.bindings := bindings;
      Storage_sigs.Indexed_data_storage.fold _ := fold;
      Storage_sigs.Indexed_data_storage.fold_keys _ := fold_keys
    |}.
End Wrap_indexed_data_storage.
Definition Wrap_indexed_data_storage {C_t C_key C_value K_t : Set}
  (C :
    Storage_sigs.Indexed_data_storage (t := C_t) (key := C_key)
      (value := C_value))
  (K : WRAPPER (t := K_t) (key := C.(Storage_sigs.Indexed_data_storage.key)))
  : Storage_sigs.Indexed_data_storage
    (t := C.(Storage_sigs.Indexed_data_storage.t)) (key := K.(WRAPPER.t))
    (value := C.(Storage_sigs.Indexed_data_storage.value)) :=
  let '_ := Wrap_indexed_data_storage.Build_FArgs C K in
  Wrap_indexed_data_storage.functor.