Skip to main content

💾 Storage_sigs.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Storage.
Require Import TezosOfOCaml.Proto_alpha.Storage_sigs.
Require Import TezosOfOCaml.Proto_alpha.Storage_functors.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Context.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Error_monad.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.

#[local] Open Scope list.

Module Single_data_storage.
  Module Eq.
    Import Proto_alpha.Storage_sigs.Single_data_storage.

    Record t {t value : Set}
      {S1 S2 : Single_data_storage (t := t) (value := value)}
      : Prop := {
      mem ctxt : S1.(mem) ctxt = S2.(mem) ctxt;
      get ctxt : S1.(get) ctxt = S2.(get) ctxt;
      find ctxt : S1.(find) ctxt = S2.(find) ctxt;
      init_value ctxt value :
        S1.(init_value) ctxt value = S2.(init_value) ctxt value;
      update ctxt value :
        S1.(update) ctxt value = S2.(update) ctxt value;
      add ctxt value :
        S1.(add) ctxt value = S2.(add) ctxt value;
      add_or_remove ctxt value :
        S1.(add_or_remove) ctxt value = S2.(add_or_remove) ctxt value;
      remove_existing ctxt :
        S1.(remove_existing) ctxt = S2.(remove_existing) ctxt;
      remove ctxt : S1.(remove) ctxt = S2.(remove) ctxt;
    }.
    Arguments t {_ _ }.
  End Eq.

The type of a simple store. We add a special case for a state with an invalid encoding. It should not be possible to create such a state, but we may not control what is already in the input store.
  Module State.
    Inductive t (a : Set) : Set :=
    | Empty : t a
    | Invalid_encoding : t a
    | Value : a t a.
    Arguments Empty {_}.
    Arguments Invalid_encoding {_}.
    Arguments Value {_}.

    Definition parse {a : Set} (encoding : Data_encoding.t a)
      (value : option Context.value) : State.t a :=
      match value with
      | Some bytes
        match Data_encoding.Binary.of_bytes_opt encoding bytes with
        | Some valueState.Value value
        | NoneState.Invalid_encoding
        end
      | NoneState.Empty
      end.
  End State.

  Module Change.
    Inductive t (a : Set) : Set :=
    | Empty : t a
    | Value : a t a.
    Arguments Empty {_}.
    Arguments Value {_}.

    Definition apply {a : Set} (ctxt : Raw_context.t) (path : Context.key)
      (encoding : Data_encoding.t a) (change : t a) : Raw_context.t :=
      match change with
      | EmptyRaw_context.remove ctxt path
      | Value value
        let bytes :=
          match Data_encoding.Binary.to_bytes_opt None encoding value with
          | Some bytesbytes
          | NoneBytes.empty
          end in
        Raw_context.add ctxt path bytes
      end.
  End Change.

  Definition reduce {a : Set} (_ : State.t a) (change : Change.t a)
    : State.t a :=
    match change with
    | Change.EmptyState.Empty
    | Change.Value valueState.Value value
    end.

  Module Op.
    Definition mem {a : Set} (state : State.t a) : bool :=
      match state with
      | State.Emptyfalse
      | State.Invalid_encoding | State.Value _true
      end.

    Definition get {a : Set} (absolute_key : key) (state : State.t a) : M? a :=
      match state with
      | State.Empty
        let error := Raw_context.Missing_key absolute_key Raw_context.Get in
        Raw_context.storage_error_value error
      | State.Invalid_encoding
        let error :=
          Build_extensible "Storage_error" Raw_context.storage_error
            (Raw_context.Corrupted_data absolute_key) in
        Error_monad.error_value error
      | State.Value valuereturn? value
      end.

    Definition find {a : Set} (absolute_key : key) (state : State.t a)
      : M? (option a) :=
      match state with
      | State.Emptyreturn? None
      | State.Invalid_encoding
        let error :=
          Build_extensible "Storage_error" Raw_context.storage_error
            (Raw_context.Corrupted_data absolute_key) in
        Error_monad.error_value error
      | State.Value valuereturn? Some value
      end.

    Definition init_value {a : Set} (absolute_key : key) (state : State.t a)
      (value : a) : M? (Change.t a) :=
      match state with
      | State.Emptyreturn? Change.Value value
      | State.Invalid_encoding | State.Value _
        Raw_context.storage_error_value (Raw_context.Existing_key absolute_key)
      end.

    Definition update {a : Set} (absolute_key : key) (state : State.t a)
      (value : a) : M? (Change.t a) :=
      match state with
      | State.Empty
        Raw_context.storage_error_value
          (Raw_context.Missing_key absolute_key Raw_context._Set)
      | State.Invalid_encoding | State.Value _return? Change.Value value
      end.

    Definition add {a : Set} (state : State.t a)
      (value : a) : Change.t a :=
      Change.Value value.

    Definition add_or_remove {a : Set} (state : State.t a) (ovalue : option a)
      : Change.t a :=
      match ovalue with
      | Some valueChange.Value value
      | NoneChange.Empty
      end.

    Definition remove_existing {a : Set} (absolute_key : key) (state : State.t a)
      : M? (Change.t a) :=
      match state with
      | State.Empty
        Raw_context.storage_error_value
          (Raw_context.Missing_key absolute_key Raw_context.Del)
      | State.Invalid_encoding | State.Value _
        return? Change.Empty
      end.

    Definition remove {a : Set} (state : State.t a) : Change.t a :=
      Change.Empty.

    Ltac unfold_all :=
      unfold
        mem, get, find,
        init_value, update, add, add_or_remove, remove_existing.
  End Op.

  Definition Make {C_t V_t : Set}
    (parse : C_t State.t V_t)
    (apply : C_t Change.t V_t Raw_context.t)
    (absolute_key : key)
    : Single_data_storage (t := C_t) (value := V_t) :=
    let apply_e ctxt change :=
      let? change := change in
      return? apply ctxt change in
    {|
      Single_data_storage.mem ctxt :=
        Op.mem (parse ctxt);
      Single_data_storage.get ctxt :=
        Op.get absolute_key (parse ctxt);
      Single_data_storage.find ctxt :=
        Op.find absolute_key (parse ctxt);
      Single_data_storage.init_value ctxt value :=
        apply_e ctxt
          (Op.init_value absolute_key (parse ctxt) value);
      Single_data_storage.update ctxt value :=
        apply_e ctxt
          (Op.update absolute_key (parse ctxt) value);
      Single_data_storage.add ctxt value :=
        let change := Op.add (parse ctxt) value in
        apply ctxt change;
      Single_data_storage.add_or_remove ctxt ovalue :=
        let change := Op.add_or_remove (parse ctxt) ovalue in
        apply ctxt change;
      Single_data_storage.remove_existing ctxt :=
        apply_e ctxt
          (Op.remove_existing absolute_key (parse ctxt));
      Single_data_storage.remove ctxt :=
        apply ctxt (Op.remove (parse ctxt));
    |}.
End Single_data_storage.

Module Non_iterable_indexed_carbonated_data_storage_with_values.
  Module Eq.
    Parameter t : {t key value : Set},
      Non_iterable_indexed_carbonated_data_storage_with_values
        (t := t) (key := key) (value := value)
      Non_iterable_indexed_carbonated_data_storage_with_values
        (t := t) (key := key) (value := value)
      Prop.
  End Eq.

  Module State.
    Parameter t : (key value : Set), Set.
  End State.

  Module Change.
    Parameter t : (key value : Set), Set.
  End Change.

  Parameter reduce : {key value},
    State.t key value Change.t key value State.t key value.

  Parameter Make : {key value : Set}
    (parse : Raw_context.t State.t key value)
    (apply : Raw_context.t Change.t key value Raw_context.t),
    Non_iterable_indexed_carbonated_data_storage_with_values
      (t := Raw_context.t) (key := key) (value := value).
End Non_iterable_indexed_carbonated_data_storage_with_values.

Properties about the [Indexed_data_storage] signature.
The validity predicate states that we can conclude to the equality of the result of folds operations given the equality of the parameters. We consider a pointwise equality for the parameter which is a function. We could also use the "functional extensionality axiom" but we prefer to avoid it.
  Module Valid.
    Import Proto_alpha.Storage_sigs.Indexed_data_storage.

    Record t {C_t I_t V_t : Set}
      {S : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)} :
      Prop := {
      fold {a : Set} ctxt (acc : a) f1 f2 :
        let order := Variant.Build "Sorted" unit tt in
        ( k v acc, f1 k v acc = f2 k v acc)
        S.(fold) ctxt order acc f1 = S.(fold) ctxt order acc f2;
      fold_keys {a : Set} ctxt (acc : a) f1 f2 :
        let order := Variant.Build "Sorted" unit tt in
        ( k acc, f1 k acc = f2 k acc)
        S.(fold_keys) ctxt order acc f1 = S.(fold_keys) ctxt order acc f2;
    }.
    Arguments t {_ _ _}.
  End Valid.

The equality between two [Indexed_data_storage].
  Module Eq.
    Import Proto_alpha.Storage_sigs.Indexed_data_storage.

    Record t {C_t I_t V_t : Set}
      {S1 S2 : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)} :
      Prop := {
      mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
      get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
      find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
      update ctxt path value :
        S1.(update) ctxt path value = S2.(update) ctxt path value;
      init_value ctxt path value :
        S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
      add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
      add_or_remove ctxt path value :
        S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
      remove_existing ctxt path :
        S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
      remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
      clear ctxt : S1.(clear) ctxt = S2.(clear) ctxt;
      keys ctxt : S1.(keys) ctxt = S2.(keys) ctxt;
      bindings ctxt : S1.(bindings) ctxt = S2.(bindings) ctxt;
      (* We only consider the "Sorted" order for the fold operations. *)
      fold {a : Set} ctxt (acc : a) f1 f2 :
        let order := Variant.Build "Sorted" unit tt in
        ( k v acc, f1 k v acc = f2 k v acc)
        S1.(fold) ctxt order acc f1 = S2.(fold) ctxt order acc f2;
      fold_keys {a : Set} ctxt (acc : a) f1 f2 :
        let order := Variant.Build "Sorted" unit tt in
        ( k acc, f1 k acc = f2 k acc)
        S1.(fold_keys) ctxt order acc f1 = S2.(fold_keys) ctxt order acc f2;
    }.
    Arguments t {_ _ _}.

Our equality is reflexive.
    Lemma refl {C_t I_t V_t : Set}
      (S : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)) :
      Valid.t S
      t S S.
    Proof.
      sfirstorder.
    Qed.

Our equality is symmetric.
    Lemma sym {C_t I_t V_t : Set}
      (S1 S2 : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)) :
      Valid.t S1 Valid.t S2
      t S1 S2 t S2 S1.
    Proof.
      intros [] [] []; constructor; intros;
        repeat match goal with
        | H : _ |- _rewrite H
        end;
        try reflexivity;
        sauto dep: on.
    Qed.

Our equality is transitive.
    Lemma trans {C_t I_t V_t : Set}
      (S1 S2 S3 : Indexed_data_storage (t := C_t) (key := I_t) (value := V_t)) :
      Valid.t S1 Valid.t S2 Valid.t S3
      t S1 S2 t S2 S3 t S1 S3.
    Proof.
      intros [] [] [] [] []; constructor; intros;
        repeat match goal with
        | H : _ |- _rewrite H
        end;
        try reflexivity;
        sauto dep: on.
    Qed.
  End Eq.

A [Kernel] from which we can express all the other operations. This is useful to simplify the proofs on the storage simulations.
  Module Kernel.
    Record signature {t key value : Set} : Set := {
      t := t;
      context := t;
      key := key;
      value := value;
      mem : context key bool;
      find : context key M? (option value);
      add_or_remove : context key option value Raw_context.t;
      clear : context Raw_context.t;
      keys : context list key;
      bindings : context list (key × value);
    }.
  End Kernel.
  Definition Kernel := @Kernel.signature.
  Arguments Kernel {_ _ _}.

The equality between two [Kernel].
  Module Kernel_eq.
    Import Kernel.

    Record t {t key value : Set}
      {K1 K2 : Kernel (t := t) (key := key) (value := value)}
      : Prop := {
      mem ctxt path : K1.(mem) ctxt path = K2.(mem) ctxt path;
      find ctxt path : K1.(find) ctxt path = K2.(find) ctxt path;
      add_or_remove ctxt path v :
        K1.(add_or_remove) ctxt path v = K2.(add_or_remove) ctxt path v;
      clear ctxt : K1.(clear) ctxt = K2.(clear) ctxt;
      keys ctxt : K1.(keys) ctxt = K2.(keys) ctxt;
      bindings ctxt : K1.(bindings) ctxt = K2.(bindings) ctxt;
    }.
    Arguments t {_ _ _}.
  End Kernel_eq.

Projection to a [Kernel].
  Definition to_kernel {t key value : Set}
    (S : Indexed_data_storage (t := t) (key := key) (value := value)) :
    Kernel (t := t) (key := key) (value := value) :=
    {|
      Kernel.mem := S.(Indexed_data_storage.mem);
      Kernel.find := S.(Indexed_data_storage.find);
      Kernel.add_or_remove := S.(Indexed_data_storage.add_or_remove);
      Kernel.clear := S.(Indexed_data_storage.clear);
      Kernel.keys := S.(Indexed_data_storage.keys);
      Kernel.bindings := S.(Indexed_data_storage.bindings);
    |}.

Re-definition from a [Kernel].
  Definition of_kernel {t key value : Set}
    (P : Path_encoding.S (t := key))
    (absolute_key : t Context.key) (sub_path : Context.key)
    (K : Kernel (t := t) (key := key) (value := value)) :
    Indexed_data_storage (t := t) (key := key) (value := value) :=
    let to_key (ctxt : t) (i : key) : Context.key :=
      (absolute_key ctxt ++ P.(Path_encoding.S.to_path) i []) ++ sub_path in
    {|
      Indexed_data_storage.mem := K.(Kernel.mem);
      Indexed_data_storage.get ctxt i :=
        let? value := K.(Kernel.find) ctxt i in
        match value with
        | Some valuereturn? value
        | None
          Raw_context.storage_error_value
            (Raw_context.Missing_key (to_key ctxt i) Raw_context.Get)
        end;
      Indexed_data_storage.find := K.(Kernel.find);
      Indexed_data_storage.update ctxt i v :=
        if K.(Kernel.mem) ctxt i then
          return? K.(Kernel.add_or_remove) ctxt i (Some v)
        else
          Raw_context.storage_error_value
            (Raw_context.Missing_key (to_key ctxt i) Raw_context._Set);
      Indexed_data_storage.init_value ctxt i v :=
        if K.(Kernel.mem) ctxt i then
          Raw_context.storage_error_value
            (Raw_context.Existing_key (to_key ctxt i))
        else
          return? K.(Kernel.add_or_remove) ctxt i (Some v);
      Indexed_data_storage.add ctxt i v :=
        K.(Kernel.add_or_remove) ctxt i (Some v);
      Indexed_data_storage.add_or_remove := K.(Kernel.add_or_remove);
      Indexed_data_storage.remove_existing ctxt i :=
        if K.(Kernel.mem) ctxt i then
          return? K.(Kernel.add_or_remove) ctxt i None
        else
          Raw_context.storage_error_value
            (Raw_context.Missing_key (to_key ctxt i) Raw_context.Del);
      Indexed_data_storage.remove ctxt i :=
        K.(Kernel.add_or_remove) ctxt i None;
      Indexed_data_storage.clear := K.(Kernel.clear);
      Indexed_data_storage.keys := K.(Kernel.keys);
      Indexed_data_storage.bindings := K.(Kernel.bindings);
      Indexed_data_storage.fold _ ctxt order acc f :=
        List.fold_right (fun '(k, v) accf k v acc)
          (K.(Kernel.bindings) ctxt) acc;
      Indexed_data_storage.fold_keys _ ctxt order acc f :=
        List.fold_right f (K.(Kernel.keys) ctxt) acc;
    |}.

Going from and then to a kernel does not change anything (this way is not really interesting).
  Lemma to_kernel_of_kernel {t key value : Set}
    (P : Path_encoding.S (t := key))
    (absolute_key : t Context.key) (sub_path : Context.key)
    (K : Kernel (t := t) (key := key) (value := value)) :
    to_kernel (of_kernel P absolute_key sub_path K) = K.
  Proof.
    reflexivity.
  Qed.

From the equality on the kernel we can conclude the equality on the whole definition.
  Lemma of_kernel_implies_eq {t key value : Set}
    (P : Path_encoding.S (t := key))
    (absolute_key : t Context.key) (sub_path : Context.key)
    (K1 K2 : Kernel (t := t) (key := key) (value := value)) :
    Kernel_eq.t K1 K2
    Eq.t
      (of_kernel P absolute_key sub_path K1)
      (of_kernel P absolute_key sub_path K2).
  Proof.
    assert ( {a b : Set} (f1 f2 : a b b) l acc,
      ( x acc, f1 x acc = f2 x acc)
      List.fold_right f1 l acc = List.fold_right f2 l acc
    ) by (induction l; hauto q: on).
    intros []; constructor; hauto l: on.
  Qed.

The simulation state.
  Module State.
    Definition compare {I_t : Set} (P : Path_encoding.S (t := I_t))
      (x1 x2 : I_t) : int :=
      let path1 := P.(Path_encoding.S.to_path) x1 [] in
      let path2 := P.(Path_encoding.S.to_path) x2 [] in
      Context.Key.compare path1 path2.

    Definition Ord {I_t : Set} (P : Path_encoding.S (t := I_t)) :
      Compare.COMPARABLE (t := I_t) :=
      {| Compare.COMPARABLE.compare := compare P |}.

    Definition Map {I_t : Set} (P : Path_encoding.S (t := I_t)) :
      Map.S (key := I_t) (t := _) :=
      Map.Make (Ord P).

The simulation state is a map to optional values. We keep the values optional to represent values with an incorrect encoding.
    Definition t {I_t : Set} (P : Path_encoding.S (t := I_t)) (V_t : Set)
      : Set :=
      (Map P).(Map.S.t) (option V_t).
  End State.

An exmplicit change on the simutation state.
  Module Change.
    Inductive t (I_t V_t : Set) : Set :=
    | Add : I_t V_t t I_t V_t
    | Remove : I_t t I_t V_t
    | Clear : t I_t V_t.
    Arguments Add {_ _}.
    Arguments Remove {_ _}.
    Arguments Clear {_ _}.
  End Change.

How to apply a change on the simulation state.
  Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
    (state : State.t P V_t) (change : Change.t I_t V_t)
    : State.t P V_t :=
    match change with
    | Change.Add key value ⇒ (State.Map P).(Map.S.add) key (Some value) state
    | Change.Remove key ⇒ (State.Map P).(Map.S.remove) key state
    | Change.Clear ⇒ (State.Map P).(Map.S.empty)
    end.

Primitive operations defined on the simulation state.
  Module Op.
    Definition mem {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
      (state : State.t P V_t) (k : I_t) : bool :=
      (State.Map P).(Map.S.mem) k state.

    Definition find {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
      (absolute_key : Context.key)
      (state : State.t P V_t) (k : I_t) : M? (option V_t) :=
      match (State.Map P).(Map.S.find) k state with
      | Some (Some v) ⇒ return? Some v
      | Some None
        let path := P.(Path_encoding.S.to_path) k [] in
        Error_monad.error_value
          (Build_extensible "Storage_error" Raw_context.storage_error
            (Raw_context.Corrupted_data (absolute_key ++ path)))
      | Nonereturn? None
      end.

    Definition get {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
      (absolute_key : Context.key)
      (state : State.t P V_t) (k : I_t)
      : M? V_t :=
      match find absolute_key state k with
      | Pervasives.Error ePervasives.Error e
      | Pervasives.Ok None
        let path := P.(Path_encoding.S.to_path) k [] in
        Error_monad.error_value
          (Build_extensible "Storage_error" Raw_context.storage_error
            (Raw_context.Missing_key (absolute_key ++ path) Raw_context.Get))
      | Pervasives.Ok (Some v) ⇒ return? v
      end.

    Definition add {I_t V_t : Set} (k : I_t) (v : V_t) : Change.t I_t V_t :=
      Change.Add k v.

    Definition add_or_remove {I_t V_t : Set} (k : I_t) (v : option V_t)
      : Change.t I_t V_t :=
      match v with
      | Some vChange.Add k v
      | NoneChange.Remove k
      end.

    Definition update {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
      (absolute_key : Context.key)
      (state : State.t P V_t)
      (k : I_t) (v : V_t) : M? Change.t I_t V_t :=
      if mem state k
      then return? (add k v)
      else let path := P.(Path_encoding.S.to_path) k [] in
        Error_monad.error_value
          (Build_extensible "Storage_error" Raw_context.storage_error
            (Raw_context.Missing_key (absolute_key ++ path) Raw_context._Set)).

    Definition init_value {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
      (absolute_key : Context.key)
      (state : State.t P V_t) (k : I_t) (v : V_t) : M? (Change.t I_t V_t) :=
      if mem state k
      then let path := P.(Path_encoding.S.to_path) k [] in
        Error_monad.error_value
          (Build_extensible "Storage_error" Raw_context.storage_error
            (Raw_context.Existing_key (absolute_key ++ path)))
      else return? (add k v).

    Definition remove {I_t V_t : Set} (k : I_t) : Change.t I_t V_t :=
      Change.Remove k.

    Definition remove_existing {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
      (absolute_key : Context.key) (state : State.t P V_t) (k : I_t) :
      M? Change.t I_t V_t :=
      if Op.mem state k then
        return? Op.remove k
      else
        let path := P.(Path_encoding.S.to_path) k [] in
        Error_monad.error_value
          (Build_extensible "Storage_error" Raw_context.storage_error
            (Raw_context.Missing_key (absolute_key ++ path) Raw_context.Del)).

    Definition clear {I_t V_t : Set} : Change.t I_t V_t :=
      Change.Clear.

    Definition keys {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
      (state : State.t P V_t) : list I_t :=
      List.filter_map
        (fun '(k, v)
          let× '_ := v in
          Some k
        )
        ((State.Map P).(Map.S.bindings) state).

    Definition bindings {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
      (state : State.t P V_t) : list (I_t × V_t) :=
      List.filter_map
        (fun '(k, v)
          let× v := v in
          Some (k, v)
        )
        ((State.Map P).(Map.S.bindings) state).

Helper to unfold all the simulation operators.
    Module Unfold.
      Ltac all :=
        repeat unfold mem, find, get,
          add, add_or_remove, update, init_value,
          remove, remove_existing,
          clear, keys, bindings,
          State.Map.
    End Unfold.
  End Op.

Build a simulation store given two functions [parse] and [apply] to communicate with the actual key-value store.
  Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
    (absolute_key : C_t Context.key)
    (parse : C_t State.t P V_t)
    (apply : C_t Change.t I_t V_t Raw_context.t) :
    Indexed_data_storage (t := C_t) (key := I_t) (value := V_t) :=
    {|
      Indexed_data_storage.mem ctxt k :=
        Op.mem (parse ctxt) k;
      Indexed_data_storage.get ctxt k :=
        Op.get (absolute_key ctxt) (parse ctxt) k;
      Indexed_data_storage.find ctxt k :=
        Op.find (absolute_key ctxt) (parse ctxt) k;
      Indexed_data_storage.update ctxt k v:=
        let? change := Op.update (absolute_key ctxt) (parse ctxt) k v in
        return? apply ctxt change;
      Indexed_data_storage.init_value ctxt k v :=
        let? change := Op.init_value (absolute_key ctxt) (parse ctxt) k v in
        return? apply ctxt change;
      Indexed_data_storage.add ctxt k v :=
        apply ctxt (Op.add k v);
      Indexed_data_storage.add_or_remove ctxt k v :=
        let change := Op.add_or_remove k v in
        apply ctxt change;
      Indexed_data_storage.remove_existing ctxt k :=
        let state := parse ctxt in
        let? change := Op.remove_existing (absolute_key ctxt) state k in
        return? apply ctxt change;
      Indexed_data_storage.remove ctxt k :=
        let change := Op.remove k in
        apply ctxt change;
      Indexed_data_storage.clear ctxt :=
        let change := Op.clear in
        apply ctxt change;
      Indexed_data_storage.keys ctxt := Op.keys (parse ctxt);
      Indexed_data_storage.bindings ctxt := Op.bindings (parse ctxt);
      Indexed_data_storage.fold _ ctxt _ acc f :=
        List.fold_right
          (fun '(k, v) accf k v acc) (Op.bindings (parse ctxt)) acc;
      Indexed_data_storage.fold_keys _ ctxt _ acc f :=
        List.fold_right f (Op.keys (parse ctxt)) acc;
    |}.

The simulation store can be expressed from its kernel. This will be useful to show the equality to other stores.
  Lemma expressed_from_kernel {C_t I_t V_t : Set}
    {P : Path_encoding.S (t := I_t)}
    (absolute_key : C_t Context.key)
    (parse : C_t State.t P V_t)
    (apply : C_t Change.t I_t V_t Raw_context.t) :
    let Store := Make absolute_key parse apply in
    Eq.t Store (of_kernel P absolute_key [] (to_kernel Store)).
  Proof.
    constructor; intros; simpl; try reflexivity;
      repeat Op.Unfold.all;
      try (step; simpl; try rewrite List.app_nil_r; reflexivity);
      try (apply List.fold_right_f_eq; hauto lq: on).
  Qed.
End Indexed_data_storage.

Module Non_iterable_indexed_data_storage.
  Module Eq.
    Import Proto_alpha.Storage_sigs.Non_iterable_indexed_data_storage.

    Record t {t key value : Set}
      {S1 S2 : Non_iterable_indexed_data_storage (t := t) (key := key) (value := value)}
      : Prop := {
      mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
      get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
      find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
      update ctxt path value :
        S1.(update) ctxt path value = S2.(update) ctxt path value;
      init_value ctxt path value :
        S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
      add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
      add_or_remove ctxt path value :
        S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
      remove_existing ctxt path :
        S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
      remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
    }.
    Arguments t {_ _ _}.
  End Eq.

  Module State := Indexed_data_storage.State.
  Module Change := Indexed_data_storage.Change.

  Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)} :=
    @Indexed_data_storage.reduce I_t V_t P.

  Module Op := Indexed_data_storage.Op.

  Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
    (absolute_key : Context.key)
    (parse : C_t State.t P V_t)
    (apply : C_t Change.t I_t V_t Raw_context.t)
    : Non_iterable_indexed_data_storage (t := C_t) (key := I_t) :=
    {|
      Non_iterable_indexed_data_storage.mem ctxt k :=
        Op.mem (parse ctxt) k;
      Non_iterable_indexed_data_storage.get ctxt k :=
        Op.get absolute_key (parse ctxt) k;
      Non_iterable_indexed_data_storage.find ctxt k :=
        Op.find absolute_key (parse ctxt) k;
      Non_iterable_indexed_data_storage.update ctxt k v :=
        let? change := Op.update absolute_key (parse ctxt) k v in
        return? apply ctxt change;
      Non_iterable_indexed_data_storage.init_value ctxt k v :=
        let? change := Op.init_value absolute_key (parse ctxt) k v in
        return? apply ctxt change;
      Non_iterable_indexed_data_storage.add ctxt k v :=
        apply ctxt (Op.add k v);
      Non_iterable_indexed_data_storage.add_or_remove := axiom;
      Non_iterable_indexed_data_storage.remove_existing := axiom;
      Non_iterable_indexed_data_storage.remove := axiom;
    |}.
End Non_iterable_indexed_data_storage.

Module Non_iterable_indexed_carbonated_data_storage_INTERNAL.
  Import Proto_alpha.Storage_sigs.Non_iterable_indexed_carbonated_data_storage_INTERNAL.
  Module Eq.
    Record t {t key value : Set}
      (S1 S2 : Non_iterable_indexed_carbonated_data_storage_INTERNAL (t := t) (key := key) (value := value))
      : Prop := {
      mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
      get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
      find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
      update ctxt path value :
        S1.(update) ctxt path value = S2.(update) ctxt path value;
      init_value ctxt path value :
        S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
      add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
      add_or_remove ctxt path value :
        S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
      remove_existing ctxt path :
        S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
      remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
    }.
    Arguments t {_ _ _}.
  End Eq.

  Module State := Indexed_data_storage.State.
  Module Op := Indexed_data_storage.Op.
  (* Module Change := Indexed_data_storage.Change. *)
  Module Change.
    Inductive t (I_t V_t : Set) : Set :=
    | Add : I_t V_t t I_t V_t
    | Remove : I_t t I_t V_t
    | Clear : t I_t V_t
    | Consume_read_gas : int I_t t I_t V_t.
    Arguments Add {_ _}.
    Arguments Remove {_ _}.
    Arguments Clear {_ _}.
    Arguments Consume_read_gas {_ _}.

    (* Send [Indexed_data_storage.Change.t] to [t] *)
    Definition of_idx {I_t V_t : Set}
               (change : Indexed_data_storage.Change.t I_t V_t)
      : Change.t I_t V_t :=
      match change with
      | Indexed_data_storage.Change.Add k vChange.Add k v
      | Indexed_data_storage.Change.Remove kChange.Remove k
      | Indexed_data_storage.Change.ClearChange.Clear
    end.
  End Change.

  (* @TODO consume changes are identities by now, fix this later *)
  Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
    (state : State.t P V_t) (change : Change.t I_t V_t)
    : State.t P V_t :=
    match change with
    | Change.Add key value ⇒ (State.Map P).(Map.S.add) key (Some value) state
    | Change.Remove key ⇒ (State.Map P).(Map.S.remove) key state
    | Change.Clear ⇒ (State.Map P).(Map.S.empty)
    | Change.Consume_read_gas gas keystate
    end.

Gas consumption functions
  (* @TODO make these functions return a value of gas (int)
     instead of tweaking on the context. The reason is because
     after the generalization of Make function these functions
     will not have access to [Raw_context.t] anymore *)

  Module Gas.
    Definition len_key
               {I_t : Set} {P : Path_encoding.S (t := I_t)}
               (i_value : I_t) : list string :=
      P.(Path_encoding.S.to_path) i_value [Storage_functors.len_name].

    Definition consume_mem_gas
      (c_value : Raw_context.t) (key_value : Context.key)
      : M? Raw_context.t :=
         Raw_context.consume_gas c_value
        (Storage_costs.read_access (List.length key_value) 0).

    Definition consume_read_gas
      {I_t : Set} (P : Path_encoding.S (t := I_t))
      (get : Raw_context.t Context.key M? bytes)
      (c_value : Raw_context.t) (i_value : I_t)
      : M? Raw_context.t :=
      let len_key := len_key (P := P) i_value in
      let? len := get c_value len_key in
      let? read_bytes := decode_len_value len_key len in
      let cost := Storage_costs.read_access (List.length len_key)
                                            read_bytes in
      Raw_context.consume_gas c_value cost.

    (* @TODO This (V : VALUE) dependence is leaking up to Make
       call, maybe we should define this as a [Parameter]? *)

    Definition to_bytes {V_t : Set}
      {V : VALUE (t := V_t)} (v : V.(VALUE.t)) : bytes :=
      (@Storage_functors.Make_encoder V_t V).(
       Storage_functors.ENCODER.to_bytes) v.

    Definition consume_serialize_write_gas
      {A I_t V_t : Set} (P : Path_encoding.S (t := I_t))
      (V : VALUE (t := V_t))
      (set : Raw_context.t list string bytes M? A)
      (c_value : Raw_context.t) (i_value : I_t)
      (v_value : V.(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.consume_gas c_value
          (Gas_limit_repr.alloc_mbytes_cost len) in
      let cost := Storage_costs.write_access len in
      let? c_value := Raw_context.consume_gas c_value cost in
      let? c_value := set c_value (len_key (P := P) i_value)
                          (encode_len_value bytes_value) in
      return? (c_value, bytes_value).

    Definition consume_remove_gas {A I_t : Set} {ipath : Set Set}
      {P : Path_encoding.S (t := I_t)}
      {I : INDEX (t := I_t) (ipath := ipath)}
      (del : Raw_context.t list string M? A)
      (c_value : Raw_context.t) (i_value : I.(INDEX.t)) : M? A :=
      let? c_value :=
        Raw_context.consume_gas c_value (Storage_costs.write_access 0)
        in
      del c_value (len_key (P := P) i_value).

    Definition data_key {I_t : Set} (P : Path_encoding.S (t := I_t))
               (i_value : I_t)
      : list string :=
      P.(Path_encoding.S.to_path) i_value [ data_name].
  End Gas.

  (* @TODO How to take gas in account in these ops *)
  Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
    (absolute_key : C_t Context.key)
    (parse : C_t State.t P V_t)
    (apply : C_t Change.t I_t V_t Raw_context.t)
    : Non_iterable_indexed_carbonated_data_storage_INTERNAL
        (t := C_t) (key := I_t) (value := V_t) :=
    {|
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.mem ctxt k :=
        return? (apply ctxt (Change.Consume_read_gas axiom k),
          Op.mem (parse ctxt) k);
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.get
          ctxt k :=
        let change := (Change.Consume_read_gas axiom k) in
        let? value := Op.get (absolute_key ctxt) (parse ctxt) k in
        return? (apply ctxt change, value);
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.find
           ctxt k :=
        let change := (Change.Consume_read_gas axiom k) in
        let? value := Op.find (absolute_key ctxt) (parse ctxt) k in
        return? (apply ctxt change, value);
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.update ctxt k v :=
        let? change := Op.update (absolute_key ctxt) (parse ctxt) k v in
        return? (apply ctxt (Change.of_idx change), 0);
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.init_value ctxt k v :=
        let? change := Op.init_value (absolute_key ctxt) (parse ctxt) k v in
        return? (apply ctxt (Change.of_idx change), 0);
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.add
        ctxt k v :=
      let change := Change.of_idx (Op.add k v) in
      return? (apply ctxt change, 0, true);
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.add_or_remove := axiom;
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.remove_existing := axiom;
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.remove := axiom;
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.list_values := axiom;
      Non_iterable_indexed_carbonated_data_storage_INTERNAL.fold_keys_unaccounted := axiom;
    |}.
End Non_iterable_indexed_carbonated_data_storage_INTERNAL.

Module Non_iterable_indexed_carbonated_data_storage.
  Import Proto_alpha.Storage_sigs.Non_iterable_indexed_carbonated_data_storage.
  Module Eq.
    Record t {t key value : Set}
      {S1 S2 : Non_iterable_indexed_carbonated_data_storage (t := t) (key := key) (value := value)}
      : Prop := {
      mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
      get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
      find ctxt path : S1.(find) ctxt path = S2.(find) ctxt path;
      update ctxt path value :
        S1.(update) ctxt path value = S2.(update) ctxt path value;
      init_value ctxt path value :
        S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
      add ctxt path value : S1.(add) ctxt path value = S2.(add) ctxt path value;
      add_or_remove ctxt path value :
        S1.(add_or_remove) ctxt path value = S2.(add_or_remove) ctxt path value;
      remove_existing ctxt path :
        S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
      remove ctxt path : S1.(remove) ctxt path = S2.(remove) ctxt path;
    }.
    Arguments t {_ _ _}.
  End Eq.

  Module State := Non_iterable_indexed_carbonated_data_storage_INTERNAL.State.
  Module Change := Non_iterable_indexed_carbonated_data_storage_INTERNAL.Change.
  Definition reduce {I_t V_t : Set} {P : Path_encoding.S (t := I_t)} := @Non_iterable_indexed_carbonated_data_storage_INTERNAL.reduce I_t V_t P.
  Module Op := Non_iterable_indexed_carbonated_data_storage_INTERNAL.Op.

  (* @TODO How to take gas in account in these ops *)
  Definition Make {C_t I_t V_t : Set} {P : Path_encoding.S (t := I_t)}
    (absolute_key : C_t Context.key)
    (parse : C_t State.t P V_t)
    (apply : C_t Change.t I_t V_t Raw_context.t)
    : Non_iterable_indexed_carbonated_data_storage (t := C_t) (key := I_t) :=
    {|
      Non_iterable_indexed_carbonated_data_storage.mem ctxt k :=
        return? (apply ctxt (Change.Consume_read_gas axiom k),
            Op.mem (parse ctxt) k);
      Non_iterable_indexed_carbonated_data_storage.get ctxt k :=
        let change := (Change.Consume_read_gas axiom k) in
        let? value := Op.get (absolute_key ctxt) (parse ctxt) k in
        return? (apply ctxt change, value);
      Non_iterable_indexed_carbonated_data_storage.find ctxt k :=
        let change := (Change.Consume_read_gas axiom k) in
        let? value := Op.find (absolute_key ctxt) (parse ctxt) k in
        return? (apply ctxt change, value);
      Non_iterable_indexed_carbonated_data_storage.update ctxt k v :=
        let? change := Op.update (absolute_key ctxt) (parse ctxt) k v in
        return? (apply ctxt (Change.of_idx change), 0);
      Non_iterable_indexed_carbonated_data_storage.init_value ctxt k v :=
        let? change := Op.init_value (absolute_key ctxt) (parse ctxt) k v in
        return? (apply ctxt (Change.of_idx change), 0);
      Non_iterable_indexed_carbonated_data_storage.add ctxt k v :=
        let change := Change.of_idx (Op.add k v) in
        return? (apply ctxt change, 0, true);
      Non_iterable_indexed_carbonated_data_storage.add_or_remove := axiom;
      Non_iterable_indexed_carbonated_data_storage.remove_existing := axiom;
      Non_iterable_indexed_carbonated_data_storage.remove := axiom;
    |}.
End Non_iterable_indexed_carbonated_data_storage.

Module Indexed_data_snapshotable_storage.
  Module Eq.
    Parameter t : {t snapshot key value : Set},
      Indexed_data_snapshotable_storage
        (t := t) (snapshot := snapshot) (key := key) (value := value)
      Indexed_data_snapshotable_storage
        (t := t) (snapshot := snapshot) (key := key) (value := value)
      Prop.
  End Eq.

  Module State.
    Parameter t : (snapshot key value : Set), Set.
  End State.

  Module Change.
    Parameter t : (snapshot key value : Set), Set.
  End Change.

  Parameter reduce : {snapshot key value},
    State.t snapshot key value
    Change.t snapshot key value
    State.t snapshot key value.

  Parameter Make : {snapshot key value : Set}
    (parse : Raw_context.t State.t snapshot key value)
    (apply : Raw_context.t Change.t snapshot key value Raw_context.t),
    Indexed_data_snapshotable_storage
      (t := Raw_context.t) (snapshot := snapshot) (key := key) (value := value).
End Indexed_data_snapshotable_storage.

Module Data_set_storage.
  Module Eq.
    Import Proto_alpha.Storage_sigs.Data_set_storage.

    Record t {t elt : Set}
      {S1 S2 : Data_set_storage (t := t) (elt := elt)}
      : Prop := {
      mem ctxt value : S1.(mem) ctxt value = S2.(mem) ctxt value;
      add ctxt value : S1.(add) ctxt value = S2.(add) ctxt value;
      remove ctxt value : S1.(remove) ctxt value = S2.(remove) ctxt value;
      elements ctxt : S1.(elements) ctxt = S2.(elements) ctxt;
      clear ctxt : S1.(clear) ctxt = S2.(clear) ctxt;
    }.
    Arguments t {_ _}.
  End Eq.

  Module State.
    Definition compare {elt : Set} (P : Path_encoding.S (t := elt))
      (x1 x2 : elt) : int :=
      let path1 := P.(Path_encoding.S.to_path) x1 [] in
      let path2 := P.(Path_encoding.S.to_path) x2 [] in
      Context.Key.compare path1 path2.

    Definition Ord {elt : Set} (P : Path_encoding.S (t := elt)) :
      Compare.COMPARABLE (t := elt) :=
      {| Compare.COMPARABLE.compare := compare P |}.

    Definition _Set {elt : Set} (P : Path_encoding.S (t := elt))
      : _Set.S (elt := elt) (t := _) :=
      _Set.Make (Ord P).

    Definition t {elt : Set} (P : Path_encoding.S (t := elt)) : Set :=
      (_Set P).(_Set.S.t).
  End State.

  Module Change.
    Inductive t (elt : Set) : Set :=
    | Add : elt t elt
    | Clear : t elt
    | Remove : elt t elt.
    Arguments Add {_}.
    Arguments Clear {_}.
    Arguments Remove {_}.
  End Change.

  Definition reduce {elt : Set} {P : Path_encoding.S (t := elt)}
    (state : State.t P) (change : Change.t elt) : State.t P :=
    match change with
    | Change.Add value ⇒ (State._Set P).(_Set.S.add) value state
    | Change.Clear ⇒ (State._Set P).(_Set.S.empty)
    | Change.Remove value ⇒ (State._Set P).(_Set.S.remove) value state
    end.

  Module Op.
    Definition mem {elt : Set} {P : Path_encoding.S (t := elt)}
      (state : State.t P) (value : elt) : bool :=
      (State._Set P).(_Set.S.mem) value state.

    Definition add {elt : Set} (value : elt) : Change.t elt :=
      Change.Add value.

    Definition remove {elt : Set} (value : elt) : Change.t elt :=
      Change.Remove value.

    Definition elements {elt : Set} {P : Path_encoding.S (t := elt)}
      (state : State.t P) : list elt :=
      (State._Set P).(_Set.S.elements) state.

    Definition clear {elt : Set} : Change.t elt :=
      Change.Clear.

    Definition fold {elt : Set} {P : Path_encoding.S (t := elt)} {a : Set}
      (state : State.t P) (x : a) (f : elt a a) : a :=
      (State._Set P).(_Set.S.fold) f state x.

    Ltac unfold_all :=
      repeat unfold mem, add, remove, elements,
        clear, fold, State._Set.
  End Op.

  Definition Make {elt : Set} {P : Path_encoding.S (t := elt)}
    (parse : Raw_context.t State.t P)
    (apply : Raw_context.t Change.t elt Raw_context.t)
    : Data_set_storage (t := Raw_context.t) (elt := elt) :=
    {|
      Data_set_storage.mem ctxt value :=
        Op.mem (parse ctxt) value;
      Data_set_storage.add ctxt value :=
        apply ctxt (Op.add value);
      Data_set_storage.remove ctxt value :=
        apply ctxt (Op.remove value);
      Data_set_storage.elements ctxt :=
        Op.elements (parse ctxt);
      Data_set_storage.fold a ctxt order x f :=
        Op.fold (parse ctxt) x f;
      Data_set_storage.clear ctxt :=
        apply ctxt Op.clear;
    |}.
End Data_set_storage.

Module Carbonated_data_set_storage.
  Module Eq.
    Parameter t : {t elt : Set},
      Carbonated_data_set_storage (t := t) (elt := elt)
      Carbonated_data_set_storage (t := t) (elt := elt)
      Prop.
  End Eq.

  Module State.
    Parameter t : (elt : Set), Set.
  End State.

  Module Change.
    Parameter t : (elt : Set), Set.
  End Change.

  Parameter reduce : {elt},
    State.t elt Change.t elt State.t elt.

  Parameter Make : {elt : Set}
    (parse : Raw_context.t State.t elt)
    (apply : Raw_context.t Change.t elt Raw_context.t),
    Carbonated_data_set_storage
      (t := Raw_context.t) (elt := elt).
End Carbonated_data_set_storage.

Module Simple_single_data_storage.
  Module Eq.
    Parameter t : {value : Set},
      Storage.Simple_single_data_storage (value := value)
      Storage.Simple_single_data_storage (value := value)
      Prop.
  End Eq.

  Module State.
    Parameter t : (value : Set), Set.
  End State.

  Module Change.
    Parameter t : (value : Set), Set.
  End Change.

  Parameter reduce : {value},
    State.t value Change.t value State.t value.

  Parameter Make : {value : Set}
    (parse : Raw_context.t State.t value)
    (apply : Raw_context.t Change.t value Raw_context.t),
    Storage.Simple_single_data_storage (value := value).
End Simple_single_data_storage.

Module For_cycle.
  Module Eq.
    Import Proto_alpha.Storage.FOR_CYCLE.

    Record t
      {S1 S2 : Storage.FOR_CYCLE}
      : Prop := {
      mem ctxt path : S1.(mem) ctxt path = S2.(mem) ctxt path;
      get ctxt path : S1.(get) ctxt path = S2.(get) ctxt path;
      init_value ctxt path value :
        S1.(init_value) ctxt path value = S2.(init_value) ctxt path value;
      remove_existing ctxt path :
        S1.(remove_existing) ctxt path = S2.(remove_existing) ctxt path;
    }.
  End Eq.

The simulation state.
  Module State.
    Definition compare (P : Path_encoding.S (t := Cycle_repr.t))
      (x1 x2 : Cycle_repr.t) : int :=
      let path1 := P.(Path_encoding.S.to_path) x1 [] in
      let path2 := P.(Path_encoding.S.to_path) x2 [] in
      Context.Key.compare path1 path2.

    Definition Ord (P : Path_encoding.S (t := Cycle_repr.t)) :
      Compare.COMPARABLE :=
      {| Compare.COMPARABLE.compare := compare P |}.

    Definition Map (P : Path_encoding.S (t := Cycle_repr.t)) :
      Map.S (key := Cycle_repr.t) (t := _) :=
      Map.Make (Ord P).

    Definition t (P : Path_encoding.S (t := Cycle_repr.t))
      : Set :=
      (Map P).(Map.S.t) (option Seed_repr.seed).
  End State.

  Module Change.
    Inductive t : Set :=
    | Add : Cycle_repr.t Seed_repr.seed t
    | Remove : Cycle_repr.t t.
  End Change.

  Definition reduce {P : Path_encoding.S (t := Cycle_repr.t)}
    (state : State.t P) (change : Change.t)
    : State.t P :=
    match change with
    | Change.Add key value ⇒ (State.Map P).(Map.S.add) key (Some value) state
    | Change.Remove key ⇒ (State.Map P).(Map.S.remove) key state
    end.

  Module Op.
    Definition mem {P : Path_encoding.S (t := Cycle_repr.t)}
      (state : State.t P) (k : Cycle_repr.t) : bool :=
      (State.Map P).(Map.S.mem) k state.

    Definition init_value {P : Path_encoding.S (t := Cycle_repr.t)}
      (absolute_key : Context.key)
      (state : State.t P) (k : Cycle_repr.t) (v : Seed_repr.seed) : M? (Change.t) :=
      if mem state k
      then let path := P.(Path_encoding.S.to_path) k [] in
        Error_monad.error_value
          (Build_extensible "Storage_error" Raw_context.storage_error
            (Raw_context.Existing_key (absolute_key ++ path)))
      else return? Change.Add k v.

    Definition get {P : Path_encoding.S (t := Cycle_repr.t)}
      (absolute_key : Context.key)
      (state : State.t P) (k : Cycle_repr.t)
      : M? Seed_repr.seed :=
      match (State.Map P).(Map.S.find) k state with
      | Some (Some v) ⇒ return? v
      | Some None
          let path := P.(Path_encoding.S.to_path) k [] in
          Error_monad.error_value
            (Build_extensible "Storage_error" Raw_context.storage_error
              (Raw_context.Corrupted_data (absolute_key ++ path)))
      | None
          let path := P.(Path_encoding.S.to_path) k [] in
          Error_monad.error_value
            (Build_extensible "Storage_error"
              Raw_context.storage_error
              (Raw_context.Missing_key
                 (absolute_key ++ path)
                 Raw_context.Get))
      end.

    Definition remove_existing
               {P : Path_encoding.S (t := Cycle_repr.t)}
              (absolute_key : Context.key)
              (state : State.t P) (k : Cycle_repr.t)
      : M? Change.t :=
        if Op.mem state k
        then return? (Change.Remove k)
        else let path := P.(Path_encoding.S.to_path) k [] in
             Error_monad.error_value
               (Build_extensible "Storage_error"
                                 Raw_context.storage_error
                                 (Raw_context.Missing_key
                                    (absolute_key ++ path)
                                    Raw_context.Del)).

    Module Unfold.
      Ltac all :=
        repeat unfold mem, init_value, get, remove_existing, State.Map.
   End Unfold.
  End Op.

  Definition Make {P : Path_encoding.S (t := Cycle_repr.t)}
    (absolute_key : Context.key)
    (parse : Raw_context.t State.t P)
    (apply : Raw_context.t Change.t Raw_context.t)
    : Storage.FOR_CYCLE :=
    {|
      Storage.FOR_CYCLE.mem ctxt k :=
        Op.mem (parse ctxt) k;
      Storage.FOR_CYCLE.get ctxt k :=
        Op.get absolute_key (parse ctxt) k;
      Storage.FOR_CYCLE.init_value ctxt k v :=
        let? change := Op.init_value absolute_key (parse ctxt) k v in
        return? apply ctxt change;
      Storage.FOR_CYCLE.remove_existing ctxt k :=
        let state := parse ctxt in
        let? change := Op.remove_existing absolute_key state k in
        return? apply ctxt change;
    |}.
End For_cycle.