💾 Storage_functors.v | Coq Tezos of OCaml 💫

  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
    | None ⇒ Result.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
    | None ⇒ return ? 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
              | None ⇒ acc_value
              | Some p_value ⇒
                let ? acc_value := acc_value in
                let ? res := f_value p_value acc_value in
                return ? res
              end
            | Context.Kind.Tree ⇒ 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_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.

  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
    | None ⇒ return ? (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
    | None ⇒ remove s_value i_value
    | Some v_value ⇒ add 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_starsthstar ⇒ op_starsthstar
      | None ⇒ 0
      end in
    fun (op_staroptstar : option int) ⇒
      let length :=
        match op_staroptstar with
        | Some op_starsthstar ⇒ op_starsthstar
        | None ⇒ Pervasives.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
                        | None ⇒ acc_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
                | None ⇒ acc_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.Tree ⇒ 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)) ⇒ 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.

  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
    | None ⇒ err_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
    | None ⇒ err_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
                | None ⇒ return ? 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_value ⇒ f_value path v_value acc_value
                  | Pervasives.Error _ ⇒ return ? acc_value
                  end
                end
              | None ⇒ return ? 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
              | None ⇒ acc_value
              | Some path ⇒
                let ? acc_value := acc_value in
                let ? res := f_value path acc_value in
                return ? res
              end
            | Context.Kind.Value ⇒ acc_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
    | None ⇒ err_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.

    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)