Skip to main content

💾 Storage_functors.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require Import TezosOfOCaml.Proto_alpha.Storage_functors.
Require Import TezosOfOCaml.Proto_alpha.Storage_sigs.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs._Set.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Context.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.List.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Map.

Require TezosOfOCaml.Proto_alpha.Proofs.Misc.
Require TezosOfOCaml.Proto_alpha.Proofs.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage_description.
Require Import TezosOfOCaml.Proto_alpha.Proofs.Storage_sigs.

(* To have the list concatenation notation [++]. *)
#[local] Open Scope list.

Module ENCODER.
  Module Valid.
    Record property {t : Set} {E : ENCODER (t := t)} : Prop := {
      of_bytes_to_bytes path value :
        E.(ENCODER.of_bytes) path (E.(ENCODER.to_bytes) value) = return? value;
    }.
  End Valid.
End ENCODER.

Module Make_subcontext.
  Module Unfold.
    Import Proto_alpha.Storage_functors.Make_subcontext.

    Ltac all :=
      unfold
        mem, get, find,
        init_value, update, add_or_remove, remove_existing, remove,
        project, to_key.
  End Unfold.

  Definition Make_kernel {t} (N : NAME) (K : Raw_context.T.Kernel (t := t)) :
    Raw_context.T.Kernel (t := t) :=
    {|
      Raw_context.T.Kernel.absolute_key ctxt :=
        K.(Raw_context.T.Kernel.absolute_key) ctxt ++ N.(NAME.name);
      Raw_context.T.Kernel.project ctxt :=
        K.(Raw_context.T.Kernel.project) ctxt;
      Raw_context.T.Kernel.update ctxt root :=
        K.(Raw_context.T.Kernel.update) ctxt root;
    |}.

We can rebuild a sub raw context from the knowledge of its kernel.
  Lemma is_from_kernel {t : Set}
    (R : REGISTER) (C : Raw_context.T (t := t)) (N : NAME)
    (K : Raw_context.T.Kernel (t := t)) :
    Raw_context.T.is_from_kernel C K
    Raw_context.T.is_from_kernel
      (Storage_functors.Make_subcontext R C N) (Make_kernel N K).
  Proof.
    intros []; constructor; intros; simpl in *;
      try rewrite <- List.app_assoc;
      sfirstorder.
  Qed.
End Make_subcontext.

Module Make_single_data_storage.
  Module Unfold.
    Import Proto_alpha.Storage_functors.Make_single_data_storage.

    Ltac all :=
      unfold
        mem, get, find,
        init_value, update, add_or_remove, remove_existing, remove.
  End Unfold.

  Lemma of_nil_sub_context_eq {value : Set}
    (R : REGISTER)
    (N : NAME)
    (V : VALUE (t := value))
    : let N_nil := {| Storage_sigs.NAME.name := [] |} in
      let C := Storage_functors.Make_subcontext R Raw_context.M N_nil in
      Make_single_data_storage R C N V =
      Make_single_data_storage R Raw_context.M N V.
    reflexivity.
  Qed.

  Lemma eq {value : Set}
    (R : REGISTER)
    (N1 N2 : NAME)
    (V : VALUE (t := value))
    : let path := op_at N1.(NAME.name) N2.(NAME.name) in
      Single_data_storage.Eq.t
        (let C := Storage_functors.Make_subcontext R Raw_context.M N1 in
        Make_single_data_storage R C N2 V)
        (Single_data_storage.Make
          (fun ctxt
            let value := Context.find (Raw_context.context_value ctxt) path in
            Single_data_storage.State.parse V.(VALUE.encoding) value
          )
          (fun ctxt change
            Single_data_storage.Change.apply ctxt path V.(VALUE.encoding) change
          )
          path
        ).
    constructor; intros; simpl;
      Unfold.all;
      Single_data_storage.Op.unfold_all;
      simpl;
      Make_subcontext.Unfold.all;
      simpl.
    { unfold Raw_context.M.mem, Raw_context.mem, mem.
      destruct find; simpl; trivial.
      now destruct Binary.of_bytes_opt.
    }
    { unfold Raw_context.M.get, Raw_context.get.
      destruct find; trivial; simpl.
      unfold Make_single_data_storage.of_bytes; simpl.
      unfold Make_encoder.of_bytes; simpl.
      now destruct Binary.of_bytes_opt.
    }
    { unfold Raw_context.M.find, Raw_context.find.
      destruct find; trivial; simpl.
      unfold Make_single_data_storage.of_bytes; simpl.
      unfold Make_encoder.of_bytes; simpl.
      now destruct Binary.of_bytes_opt.
    }
    { unfold Raw_context.M.init_value, Raw_context.init_value, mem.
      destruct find; trivial; simpl.
      now destruct Binary.of_bytes_opt.
    }
    { unfold Raw_context.M.update, Raw_context.update, mem.
      destruct find; trivial; simpl.
      now destruct Binary.of_bytes_opt.
    }
    { reflexivity.
    }
    { match goal with
      | v : _ |- _now destruct v
      end.
    }
    { unfold Raw_context.M.remove_existing, Raw_context.remove_existing, mem.
      destruct find; trivial; simpl.
      now destruct Binary.of_bytes_opt.
    }
    { reflexivity.
    }
  Qed.
End Make_single_data_storage.

Module INDEX.
  Definition to_Path_encoding_S {t ipath}
    (index : INDEX (t := t) (ipath := ipath)) : Path_encoding.S (t := t) := {|
      Path_encoding.S.to_path := index.(Storage_functors.INDEX.to_path);
      Path_encoding.S.of_path := index.(Storage_functors.INDEX.of_path);
      Path_encoding.S.path_length := index.(Storage_functors.INDEX.path_length);
    |}.

  Axiom compare_to_Path_encoding_S_Valid : {t ipath}
    (i : INDEX (t := t) (ipath := ipath)),
    Compare.Valid.t (fun _True) (fun xx)
    (Indexed_data_storage.State.compare (INDEX.to_Path_encoding_S i)).

  Module Valid.
    Record t {u ipath} (index : INDEX (t := u) (ipath := ipath)) : Prop := {
      path_encoding : Path_encoding.S.Valid.t (to_Path_encoding_S index);
      args :
         (a : Set),
         (dep_args : Storage_description.dep_args a u (ipath a)),
        Storage_description.to_args dep_args = index.(INDEX.args)
    }.
  End Valid.

The [unpack] and [_pack] operations are compatible.
  Lemma unpack_pack {a t : Set} {ipath : Set Set}
    (I : INDEX (t := t) (ipath := ipath))
    (ctxt : a) (index : t) :
    Valid.t I
    Storage_description.unpack (c := ipath a) I.(INDEX.args)
      (Storage_description._pack I.(INDEX.args) ctxt index) =
    (ctxt, index).
  Proof.
    intros H.
    destruct (H.(Valid.args _) a) as [? H_args].
    rewrite <- H_args.
    rewrite <- Storage_description.dep_unpack_eq.
    rewrite <- Storage_description.dep_pack_eq.
    apply Storage_description.dep_unpack_dep_pack.
  Qed.

The [_pack] and [unpack] operations are compatible.
  Lemma pack_unpack_match {a t : Set} {ipath : Set Set}
    (I : INDEX (t := t) (ipath := ipath))
    (indexed_ctxt : ipath a) :
    Valid.t I
    let '(ctxt, index) :=
      Storage_description.unpack I.(INDEX.args) indexed_ctxt in
    Storage_description._pack I.(INDEX.args) (ctxt : a) (index : t) =
    indexed_ctxt.
  Proof.
    intros H.
    destruct (H.(Valid.args _) a) as [dep_args H_args].
    rewrite <- H_args.
    rewrite <- Storage_description.dep_unpack_eq.
    epose proof (Storage_description.dep_pack_dep_unpack dep_args indexed_ctxt).
    destruct Storage_description.dep_unpack.
    now rewrite <- Storage_description.dep_pack_eq.
  Qed.

The [_pack] and [unpack] operations are compatible.
  Lemma pack_unpack {a t : Set} {ipath : Set Set}
    (I : INDEX (t := t) (ipath := ipath))
    (indexed_ctxt : ipath a) (ctxt : a) (index : t) :
    Valid.t I
    Storage_description.unpack I.(INDEX.args) indexed_ctxt = (ctxt, index)
    Storage_description._pack I.(INDEX.args) (ctxt : a) (index : t) =
    indexed_ctxt.
  Proof.
    hauto lq: on use: pack_unpack_match.
  Qed.
End INDEX.

Module Make_data_set_storage.
  Lemma of_nil_sub_context_eq {ipath : Set Set} {value : Set}
    (I : INDEX (ipath := ipath) (t := value))
    (R : REGISTER)
    (N : NAME)
    : let N_nil := {| Storage_sigs.NAME.name := [] |} in
      let C := Storage_functors.Make_subcontext R Raw_context.M N_nil in
      Make_data_set_storage C I =
      Make_data_set_storage Raw_context.M I.
    reflexivity.
  Qed.

  (* Should flatten_view have an INDEX as an argument? *)
  Axiom flatten_view_sorted : {ipath : Set Set} {value : Set}
    `{@Make.FArgs value}
    (I : INDEX (ipath := ipath) (t := value))
    (d : option depth) (v : Context.t) (k : key),
    Map.StrictlySorted.t (List.filter_map (fun pI.(INDEX.of_path) (fst p))
    (Context.flatten_view d v k)).

  Lemma eq {ipath : Set Set} {value : Set}
    (I : INDEX (ipath := ipath) (t := value))
    (R : REGISTER)
    (N : NAME)
    : let P := INDEX.to_Path_encoding_S I in
      let C := Storage_functors.Make_subcontext R Raw_context.M N in
      (* this incantation is needed to ensure that
         `args` is used as an implicit argument *)

      let args := Make_data_set_storage.Build_FArgs C I in
      INDEX.Valid.t I
      Data_set_storage.Eq.t
        (Make_data_set_storage C I)
        (Data_set_storage.Make (P := P)
        (fun ctxt
            let view := Raw_context.context_value ctxt in
            Context.fold (Some (Context.Eq I.(INDEX.path_length)))
              view N.(NAME.name) (Variant.Build "Sorted" unit tt)
              (_Set.Make _).(_Set.S.empty)
              (fun k _ s
                match I.(INDEX.of_path) k with
                | Some element ⇒ (_Set.Make _).(_Set.S.add) element s
                | Nones
                end
            ))
          (fun ctxt change
             match change with
             | Data_set_storage.Change.Add val
                 Make_data_set_storage.add ctxt val
             | Data_set_storage.Change.Clear
                 Make_data_set_storage.clear ctxt
             | Data_set_storage.Change.Remove val
                 Make_data_set_storage.remove ctxt val
             end)
        ).
      intros.
      set (compare := Data_set_storage.State.compare P).
      constructor; intros; simpl.
    { unfold Make_data_set_storage.mem; simpl.
      unfold Make_subcontext.mem; simpl.
      unfold Data_set_storage.Op.mem; simpl.
      unfold Make_subcontext.to_key; simpl.
      unfold Raw_context.M.mem; simpl.
      unfold Raw_context.mem.
      unfold Context.mem.
      simpl.
      destruct (find _ _) eqn:G; symmetry; apply axiom.
      (*- unfold Context.fold_sorted.
        rewrite (@Map.mem_In _
          (@Make.Build_FArgs value
        (COMPARABLE.Build_signature value
           compare)) axiom).
        destruct (Context.flatten_view_find_In
          (Raw_context.context_value ctxt)
          (N.(NAME.name))
          (I.(INDEX.to_path) value0 nil)
          (I.(INDEX.path_length))) as [G' _].
        + apply H.
        + destruct G'; [exists v; auto|idtac]. 
          eapply (List.In_to_In_fold_add
            (fun p : key * Context.tree => I.(INDEX.of_path) (fst p))
            (fun v => (v,tt))
            (@_Set.Make.add _ (@_Set.Make.Build_FArgs value
               (COMPARABLE.Build_signature value
                  compare)))).
          * apply _Set.added_In; assumption.
          * intros. apply _Set.In_add_still_In; assumption.
          * exact H0.
          * simpl.
            apply H.
        + rewrite List.fold_right_opt_map.
          rewrite (_Set.sorted_fold_right_add compare);
          apply flatten_view_sorted.
      - unfold Context.fold_sorted.
        rewrite (@Map.mem_not_In _
          (@Make.Build_FArgs value
        (COMPARABLE.Build_signature value
           compare)) lawful). 
        + intro.
          destruct H as [H_path H_args].
          pose proof (List.In_fold_add_to_In
            (fun p : key * Context.tree => I.(INDEX.of_path) (fst p))
            (fun v => (v,tt))
            (@_Set.Make.add _ (@_Set.Make.Build_FArgs value
              (COMPARABLE.Build_signature value compare)))
            (_Set.In_add_destr compare)
            axiom (* inj of to_path, a bit trickier
              because I think we need some local data about
              the list we are inside *)

            (flatten_view
              (Some (Eq I.(INDEX.path_length)))
              (Raw_context.context_value ctxt)
              N.(NAME.name))
            ((I.(INDEX.to_path) value0 nil), axiom)
            value0
            ((Path_encoding.S.Valid.of_path_to_path H_path _))
            H0).
          destruct (Context.flatten_view_find_In
            (Raw_context.context_value ctxt)
            N.(NAME.name)
            (I.(INDEX.to_path) value0 nil)
            I.(INDEX.path_length)
            ) as [_ G1]; [apply H_path|idtac].
          destruct G1 as [v Hv].
          * eexists; exact H.
          * rewrite Hv in G; discriminate.
      + rewrite List.fold_right_opt_map.
        rewrite (_Set.sorted_fold_right_add compare);
        apply flatten_view_sorted.*)

    }
    { reflexivity. }
    { reflexivity. }
    { unfold Make_data_set_storage.elements, Data_set_storage.Op.elements,
        Make_data_set_storage.elements, Make.map, Make.bindings; simpl.
      unfold Make.bindings.
      unfold Make_data_set_storage.fold; simpl.
      unfold Make_subcontext.fold; simpl.
      unfold Raw_context.fold; simpl.
      unfold Make_subcontext.to_key; simpl.
      unfold op_at; rewrite app_nil_r.
      symmetry.
      unfold Raw_context.M.fold.
      unfold Raw_context.fold.
      unfold Context.fold_sorted.
      simpl.
      rewrite List.fold_right_opt_map.
      rewrite Context.remove_kind_match.
      (* rewrite List.fold_right_opt_no_None.
      - rewrite Context.opt_map_filter_tree.
        + unfold nil. rewrite List.fold_right_cons_nil.
          apply (_Set.sorted_fold_right_add compare).
          apply flatten_view_sorted.
        + apply axiom. (*axiomatize this*)
      - apply axiom. kind_value vs of_path *)

      apply axiom.
      }
      { reflexivity. }
Qed.
End Make_data_set_storage.

Module Pair.
We always produce a valid index from a pair of two valid indexes.
  Lemma is_valid {t1 ipath1 t2 ipath2}
    {I1 : INDEX (t := t1) (ipath := ipath1)}
    {I2 : INDEX (t := t2) (ipath := ipath2)}
    : INDEX.Valid.t I1
      INDEX.Valid.t I2
      INDEX.Valid.t (Pair I1 I2).
    intros [H1_path H1_args] [H2_path H2_args].
    econstructor; simpl.
    { constructor; simpl; intros; try destruct v; simpl.
      { rewrite H1_path.(Path_encoding.S.Valid.to_path_postfix).
        simpl.
        rewrite H2_path.(Path_encoding.S.Valid.to_path_postfix).
        simpl.
        rewrite H1_path.(Path_encoding.S.Valid.to_path_postfix)
          with (postfix := I2.(INDEX.to_path) _ []).
        simpl.
        now rewrite List.app_assoc.
      }
      { unfold Pair.of_path; simpl.
        destruct I1, H1_path; simpl in ×.
        erewrite <- to_path_path_length.
        rewrite (to_path_postfix _ (I2.(INDEX.to_path) _ [])).
        rewrite Misc.take_of_length_app.
        rewrite of_path_to_path.
        now rewrite H2_path.(Path_encoding.S.Valid.of_path_to_path).
        apply axiom. (* TODO: check overflow on list lengths *)
      }
      { unfold Pair.of_path.
        match goal with
        | [|- context[Misc.take ?n ?l]] ⇒ assert (H_take := Misc.take_cases n l)
        end.
        destruct (Misc.take _ _) as [[p1 p2]|]; trivial.
        assert (H_p1 := H1_path.(Path_encoding.S.Valid.to_path_of_path) p1).
        assert (H_p2 := H2_path.(Path_encoding.S.Valid.to_path_of_path) p2).
        simpl in ×.
        repeat destruct (_.(INDEX.of_path) _); trivial.
        simpl.
        rewrite H1_path.(Path_encoding.S.Valid.to_path_postfix).
        rewrite H2_path.(Path_encoding.S.Valid.to_path_postfix).
        simpl.
        rewrite H_p1, H_p2.
        rewrite List.app_nil_r.
        symmetry; apply H_take.
        apply axiom.
      }
      { rewrite H1_path.(Path_encoding.S.Valid.to_path_postfix).
        rewrite List.length_app_sum; simpl.
        rewrite H1_path.(Path_encoding.S.Valid.to_path_path_length).
        rewrite H2_path.(Path_encoding.S.Valid.to_path_path_length).
        reflexivity.
      }
    }
    { intros a; unfold Pair.args; simpl.
      destruct (H1_args a) as [args1 ?].
      destruct (H2_args (ipath1 a)) as [args2 ?].
       (Storage_description.Dep_Pair args1 args2).
      scongruence.
    }
  Qed.
End Pair.

Proofs related to the functor [Make_indexed_data_storage].
Module Make_indexed_data_storage.
  Module Unfold.
    Import Proto_alpha.Storage_functors.Make_indexed_data_storage.

Helper to unfold the definition the [Make_indexed_data_storage] functor.
    Ltac all :=
      repeat unfold
        get, mem, find,
        update, init_value, add, add_or_remove,
        remove_existing, remove,
        clear, keys, bindings, fold, fold_keys.
  End Unfold.

  Section Make_indexed_data_storage.
    Context {ipath : Set Set} {C_t I_t V_t : Set}
      (C : Raw_context.T (t := C_t)) (C_K : Raw_context.T.Kernel (t := C_t))
      (I : INDEX (ipath := ipath) (t := I_t))
      (V : Storage_sigs.VALUE (t := V_t))
      (C_is_valid : Raw_context.T.Valid.t C)
      (C_K_is_valid : Raw_context.T.is_from_kernel C C_K)
      (I_is_valid : INDEX.Valid.t I)
      (P := INDEX.to_Path_encoding_S I)
      (M := Indexed_data_storage.State.Map P)
      (Store := Make_indexed_data_storage C I V)
      (Ord := Indexed_data_storage.State.Ord P).

The path-encoding is valid because the index is.
    Lemma P_is_valid : Path_encoding.S.Valid.t P.
    Proof.
      apply I_is_valid.
    Qed.

The [Store] re-created from its kernel.
    Definition of_to_Store :
      Indexed_data_storage (t := C_t) (key := I_t) (value := V_t) :=
      Indexed_data_storage.of_kernel
        P
        (C_K.(Raw_context.T.Kernel.absolute_key))
        []
        (Indexed_data_storage.to_kernel Store).

We show that the [Store] is equivalent to the store created from its kernel. This ensures some consistency of its operations, and make sure that we can compare it by only comparing its kernel.
    Lemma expressed_from_kernel : Indexed_data_storage.Eq.t Store of_to_Store.
    Proof.
      constructor; simpl; intros; try reflexivity;
        Unfold.all;
        cbn;
        destruct C_K_is_valid;
        repeat match goal with
        | H : _ |- _rewrite H
        end;
        simpl;
        Raw_context.T.Unfold.all;
        try rewrite List.app_nil_r.
      { destruct Context.find; simpl; [|reflexivity].
        now destruct Make_encoder.of_bytes.
      }
      { hauto lq: on rew: off. }
      { hauto lq: on rew: off. }
      { scongruence. }
      { hauto lq: on rew: off. }
      { scongruence. }
      { unfold Context.fold_sorted.
        set (l := Context.flatten_view _ _ _).
        induction l; hauto drew: off.
      }
      { unfold Context.fold_sorted.
        set (l := Context.flatten_view _ _ _).
        induction l; sauto.
      }
    Qed.

The definition of a simulation store, where we use high-level OCaml data structures such as maps, instead of the key-value store.
    Definition Simulation :
      Indexed_data_storage (t := C_t) (key := I_t) (value := V_t) :=
      Indexed_data_storage.Make
        C_K.(Raw_context.T.Kernel.absolute_key)
        (fun ctxt
          let depth := Some (Context.Eq P.(Path_encoding.S.path_length)) in
          let view :=
            let root_ctxt := C_K.(Raw_context.T.Kernel.project) ctxt in
            Raw_context.context_value root_ctxt in
          let path := C_K.(Raw_context.T.Kernel.absolute_key) ctxt in
          let bindings := Context.flatten_view depth view path in
          let values :=
            List.filter_map
              (fun '(key, tree)
                let index := P.(Path_encoding.S.of_path) key in
                let bytes := Context.Tree.to_value tree in
                match index, bytes with
                | Some index, Some bytes
                  let value :=
                    Data_encoding.Binary.of_bytes_opt V.(VALUE.encoding) bytes in
                  Some (index, value)
                | _, _None
                end
              )
              bindings in
          Map.of_bindings (Ord := Ord) values
        )
        (fun ctxt change
          match change with
          | Indexed_data_storage.Change.Add k v
            Store.(Indexed_data_storage.add) ctxt k v
          | Indexed_data_storage.Change.Remove k
            Store.(Indexed_data_storage.remove) ctxt k
          | Indexed_data_storage.Change.Clear
            Store.(Indexed_data_storage.clear) ctxt
          end
        ).

The simulation store computed from its kernel.
    Definition of_to_Simulation :
      Indexed_data_storage (t := C_t) (key := I_t) (value := V_t) :=
      Indexed_data_storage.of_kernel
        P
        (C_K.(Raw_context.T.Kernel.absolute_key))
        []
        (Indexed_data_storage.to_kernel Simulation).

The [Store] is valid.
    Lemma Store_is_valid : Indexed_data_storage.Valid.t Store.
    Proof.
      constructor; intros; apply C_is_valid; hauto lq: on rew: off.
    Qed.

The [Simulation] store is valid.
    Lemma Simulation_is_valid : Indexed_data_storage.Valid.t Simulation.
    Proof.
      constructor; intros; apply List.fold_right_f_eq; hauto lq: on.
    Qed.

The [of_to_Store] is valid.
    Lemma of_to_Store_is_valid : Indexed_data_storage.Valid.t of_to_Store.
    Proof.
      constructor; intros; apply List.fold_right_f_eq; hauto lq: on.
    Qed.

The [of_to_Simulation] store is valid.
    Lemma of_to_Simulation_is_valid :
      Indexed_data_storage.Valid.t of_to_Simulation.
    Proof.
      constructor; intros; apply List.fold_right_f_eq; hauto lq: on.
    Qed.

Some auxiliary list lemmas useful for the proof.


    Lemma find_map_filter_map_eq {a b c : Set}
      (f : b option c) g (l : list a) :
      List.find_map f (List.filter_map g l) =
      List.find_map (fun xlet× y := g x in f y) l.
    Proof.
      induction l; hfcrush.
    Qed.

    Lemma find_map_extentionality {a b1 b2 c : Set}
      (f1 : b1 c) (f2 : b2 c) default g1 g2 (l : list a) :
      ( x, (Option.map f1 (g1 x)) = (Option.map f2 (g2 x)))
      match List.find_map g1 l with
      | Some yf1 y
      | Nonedefault
      end =
      match List.find_map g2 l with
      | Some yf2 y
      | Nonedefault
      end.
    Proof.
      unfold Option.map; intros H.
      induction l as [|x l]; simpl; [reflexivity|].
      assert (H_x := H x).
      destruct g1; destruct g2; congruence.
    Qed.

    Lemma filter_map_filter_map_eq {a b c : Set}
      (f : b option c) (g : a option b) (l : list a) :
      List.filter_map f (List.filter_map g l) =
      List.filter_map (fun xlet× y := g x in f y) l.
    Proof.
      induction l; hauto lq: on.
    Qed.

    Lemma fold_right_filter_map_eq {a b : Set}
      (f : a option b) (l : list a) :
      List.filter_map f l =
      List.fold_right
        (fun x acc
          match f x with
          | Some yy :: acc
          | Noneacc
          end
        ) l [].
    Proof.
      induction l; hauto lq: on.
    Qed.

Tactic to help solve the [mem] and [find] cases.
    Ltac eq_on_kernel_mem_find :=
      rewrite Context.find_value_flatten_view_eq;
      rewrite (P_is_valid.(Path_encoding.S.Valid.to_path_path_length));
      set (bindings := Context.flatten_view _ _ _);
      unfold Context.find_value_in_flatten_view;
      unfold Indexed_data_storage.State.Map;
      try rewrite Map.mem_from_find;
      rewrite Map.find_of_bindings;
      cbn;
      rewrite find_map_filter_map_eq;
      apply find_map_extentionality; intros [key tree];
      pose proof (P_is_valid.(Path_encoding.S.Valid.to_path_of_path) key);
      destruct I.(INDEX.of_path) eqn:?; simpl;
      [ subst;
        destruct Tree.to_value; simpl; destruct (_ =? _); try reflexivity
      | set (key' := I.(INDEX.to_path) _ _);
        destruct (_ =? _) eqn:?; simpl; try reflexivity;
        assert (key' = key) by (
          apply Context.Key.compare_is_valid; trivial;
          cbn;
          fold key';
          lia
        );
        eassert (I.(INDEX.of_path) key' = Some _) by apply P_is_valid;
        congruence
      ].

Tactic to help solve the [keys] and [bindings] cases.
    Ltac eq_on_kernel_keys_bindings :=
      unfold Context.fold_sorted;
      rewrite List.app_nil_r;
      set (bindings := Context.flatten_view _ _ _);
      rewrite Map.bindings_of_bindings;
      rewrite filter_map_filter_map_eq;
      rewrite fold_right_filter_map_eq;
      apply List.fold_right_f_eq; intros [key tree] acc;
      repeat match goal with
      | H : _ |- _rewrite H
      end; cbn;
      destruct Tree.to_value; simpl;
      [ destruct I.(INDEX.of_path); simpl; try reflexivity;
        unfold Make_encoder.of_bytes; simpl;
        destruct Binary.of_bytes_opt; reflexivity
      | destruct I.(INDEX.of_path); reflexivity ].

The kernels of [Store] and [Simulation] are equal.
    Lemma eq_on_kernel :
      Indexed_data_storage.Kernel_eq.t
        (Indexed_data_storage.to_kernel Store)
        (Indexed_data_storage.to_kernel Simulation).
    Proof.
      constructor; intros; simpl; Unfold.all; cbn;
        destruct C_K_is_valid; destruct Tree;
        repeat match goal with
        | H : _ |- _rewrite H
        end;
        simpl;
        Raw_context.T.Unfold.all;
        try set (root_ctxt := Raw_context.context_value _).
      { unfold Indexed_data_storage.Op.mem.
        unfold Context.mem.
        rewrite Context.find_value_flatten_view_eq;
        rewrite (P_is_valid.(Path_encoding.S.Valid.to_path_path_length));
        set (bindings := Context.flatten_view _ _ _);
        unfold Context.find_value_in_flatten_view;
        unfold Indexed_data_storage.State.Map;
        try rewrite Map.mem_from_find;
        rewrite Map.find_of_bindings;
        cbn.
        rewrite find_map_filter_map_eq;
        apply find_map_extentionality; intros [key tree];
        pose proof (P_is_valid.(Path_encoding.S.Valid.to_path_of_path) key);
        destruct I.(INDEX.of_path) eqn:?; simpl;
        [ subst;
          destruct Tree.to_value; simpl; destruct (_ =? _); try reflexivity
        | set (key' := I.(INDEX.to_path) _ _);
          destruct (_ =? _) eqn:?; simpl; try reflexivity;
          assert (key' = key) by (
            apply Context.Key.compare_is_valid; trivial;
            cbn;
            fold key';
            lia
          );
          eassert (I.(INDEX.of_path) key' = Some _) by apply P_is_valid;
          congruence
        ].
        apply INDEX.compare_to_Path_encoding_S_Valid.
      }
      { unfold Indexed_data_storage.Op.find.
        rewrite Context.find_value_flatten_view_eq;
        rewrite (P_is_valid.(Path_encoding.S.Valid.to_path_path_length));
        set (bindings := Context.flatten_view _ _ _);
        unfold Context.find_value_in_flatten_view;
        unfold Indexed_data_storage.State.Map;
        try rewrite Map.mem_from_find;
        rewrite Map.find_of_bindings;
        cbn.
        rewrite find_map_filter_map_eq;
        apply find_map_extentionality; intros [key tree];
        pose proof (P_is_valid.(Path_encoding.S.Valid.to_path_of_path) key);
        destruct I.(INDEX.of_path) eqn:?; simpl;
        [ subst;
          destruct Tree.to_value; simpl; destruct (_ =? _); try reflexivity
        | set (key' := I.(INDEX.to_path) _ _);
          destruct (_ =? _) eqn:?; simpl; try reflexivity;
          assert (key' = key) by (
            apply Context.Key.compare_is_valid; trivial;
            cbn;
            fold key';
            lia
          );
          eassert (I.(INDEX.of_path) key' = Some _) by apply P_is_valid;
          congruence
        ].
        unfold Make_encoder.of_bytes; cbn.
        now destruct Binary.of_bytes_opt.
        apply axiom. (* TODO: need compare validity proof *)
      }
      { unfold Indexed_data_storage.Op.add_or_remove.
        hauto drew: off.
      }
      { reflexivity. }
      { unfold Indexed_data_storage.Op.keys.
      unfold Context.fold_sorted;
      rewrite List.app_nil_r;
      set (bindings := Context.flatten_view _ _ _).
      rewrite Map.bindings_of_bindings.
      rewrite filter_map_filter_map_eq.
      rewrite fold_right_filter_map_eq;
      apply List.fold_right_f_eq; intros [key tree] acc;
      repeat match goal with
      | H : _ |- _rewrite H
      end; cbn;
      destruct Tree.to_value; simpl;
      [ destruct I.(INDEX.of_path); simpl; try reflexivity;
        unfold Make_encoder.of_bytes; simpl;
        destruct Binary.of_bytes_opt; reflexivity
      | destruct I.(INDEX.of_path); reflexivity ].
      eapply List.Sorted.filter_map.
      2:{ apply Context.flatten_view_is_sorted. }
      intros.
      destruct x1, x2.
      destruct (I.(INDEX.of_path) l) eqn:Hl; auto.
      destruct (I.(INDEX.of_path) l0) eqn:Hl0; auto.
      destruct (Tree.to_value t); auto.
      destruct (Tree.to_value t0); auto.
      unfold Context.flatten_view_lt.
      simpl.
      unfold Context.Key.lt; simpl.
      apply axiom. (*TODO*)
      destruct (Tree.to_value t); auto.
      }
      { unfold Indexed_data_storage.Op.bindings.
      unfold Context.fold_sorted;
      rewrite List.app_nil_r;
      set (bindings := Context.flatten_view _ _ _).
      rewrite Map.bindings_of_bindings.
      rewrite filter_map_filter_map_eq.
      rewrite fold_right_filter_map_eq;
      apply List.fold_right_f_eq; intros [key tree] acc;
      repeat match goal with
      | H : _ |- _rewrite H
      end; cbn;
      destruct Tree.to_value; simpl;
      [ destruct I.(INDEX.of_path); simpl; try reflexivity;
        unfold Make_encoder.of_bytes; simpl;
        destruct Binary.of_bytes_opt; reflexivity
      | destruct I.(INDEX.of_path); reflexivity ].
      eapply List.Sorted.filter_map.
      2:{ apply Context.flatten_view_is_sorted. }
      intros.
      destruct x1, x2.
      destruct (I.(INDEX.of_path) l) eqn:Hl; auto.
      destruct (I.(INDEX.of_path) l0) eqn:Hl0; auto.
      destruct (Tree.to_value t); auto.
      destruct (Tree.to_value t0); auto.
      unfold Context.flatten_view_lt.
      simpl.
      unfold Context.Key.lt; simpl.
      apply axiom. (*TODO*)
      destruct (Tree.to_value t); auto.
      }
    Qed.

From the equality of the kernels, we conclude that the stores are equal.
    Lemma eq : Indexed_data_storage.Eq.t Store Simulation.
    Proof.
      pose proof Store_is_valid; pose proof Simulation_is_valid.
      eapply Indexed_data_storage.Eq.trans; trivial.
      { apply of_to_Store_is_valid. }
      { apply expressed_from_kernel. }
      { eapply Indexed_data_storage.Eq.trans; trivial.
        { apply of_to_Store_is_valid. }
        { apply of_to_Simulation_is_valid. }
        { apply Indexed_data_storage.of_kernel_implies_eq.
          apply eq_on_kernel.
        }
        { apply Indexed_data_storage.Eq.sym; trivial.
          { apply of_to_Simulation_is_valid. }
          { apply Indexed_data_storage.expressed_from_kernel. }
        }
      }
    Qed.
  End Make_indexed_data_storage.
End Make_indexed_data_storage.

Module Make_indexed_subcontext.
  Module Raw_context.
    Module Unfold.
      Import Proto_alpha.Storage_functors.Make_indexed_subcontext.Raw_context.

      Ltac all :=
        unfold
          mem, mem_tree, get, get_tree, find, find_tree,
          list_value,
          init_value, init_tree,
          update, update_tree,
          add, add_tree,
          remove, remove_existing, remove_existing_tree,
          add_or_remove, add_or_remove_tree,
          fold, project, absolute_key, to_key,
          Tree.empty.
    End Unfold.

    Definition Make_kernel {ipath I_t C_t}
      (I : INDEX (ipath := ipath) (t := I_t))
      (K : Raw_context.T.Kernel (t := C_t)) :
      Raw_context.T.Kernel (t := ipath C_t) :=
      let unpack ctxt :=
        Storage_description.unpack I.(INDEX.args) ctxt in
      let pack ctxt :=
        Storage_description._pack I.(INDEX.args) ctxt in
      {|
        Raw_context.T.Kernel.absolute_key ctxt :=
          let '(ctxt, index) := unpack ctxt in
          K.(Raw_context.T.Kernel.absolute_key) ctxt ++
          I.(INDEX.to_path) index [];
        Raw_context.T.Kernel.project ctxt :=
          let '(ctxt, _) := unpack ctxt in
          K.(Raw_context.T.Kernel.project) ctxt;
        Raw_context.T.Kernel.update ctxt root :=
          let '(ctxt, index) := unpack ctxt in
          pack (K.(Raw_context.T.Kernel.update) ctxt root) index;
      |}.

We can rebuild an indexed raw context from the knowledge of its kernel.
    Lemma is_from_kernel {ipath : Set Set} {I_t C_t : Set}
      (C : Raw_context.T (t := C_t)) (I : INDEX (ipath := ipath) (t := I_t))
      (K : Raw_context.T.Kernel (t := C_t)) :
      INDEX.Valid.t I
      Raw_context.T.is_from_kernel C K
      let IC := Make_indexed_subcontext C I in
      let C' := IC.(Storage_sigs.Indexed_raw_context.Raw_context) in
      Raw_context.T.is_from_kernel C' (Make_kernel I K).
    Proof.
      intros [] [] *; destruct Tree; repeat constructor; intros; simpl in *;
      Unfold.all;
        cbn;
        try destruct Storage_description.unpack;
        try rewrite path_encoding.(Path_encoding.S.Valid.to_path_postfix);
        simpl;
        try rewrite <- List.app_assoc;
        repeat match goal with
        | H : _ |- _rewrite H
        end;
        try match goal with
        | |- _ = let? _ := ?e _ in _destruct e
        end; simpl;
        reflexivity.
    Qed.
  End Raw_context.

  Module Make_set. Section Make_set.
    Context {ipath : Set Set} {value : Set}
      (I : INDEX (ipath := ipath) (t := value))
      (R1 R2 : REGISTER)
      (N1 N2 : NAME)
      (I_is_valid : INDEX.Valid.t I)
      (P := INDEX.to_Path_encoding_S I)
      (S := Data_set_storage.State._Set P)
      (C := Make_subcontext R1 Raw_context.M N1)
      (IC := Make_indexed_subcontext C I)
      (Substore := IC.(Storage_sigs.Indexed_raw_context.Make_set) R2 N2)
      (Ord := Data_set_storage.State.Ord P).

    Lemma P_is_valid : Path_encoding.S.Valid.t P.
    Proof.
      sauto lq: on.
    Qed.

A lemma useful in the [eq] proof.
    Lemma sorted_set_elements view path1 path2 :
      let flat := flatten_view (Some (Eq I.(INDEX.path_length))) view path1 in
      Sorted.Sorted
        (fun x1 x2 : Ord.(COMPARABLE.t) ⇒
          (Compare.Make Ord).(S.op_lt) x1 x2 = true)
        (filter_map
          (fun v : key × tree
            match I.(INDEX.of_path) (Datatypes.fst v) with
            | Some element
                match Tree.find (Datatypes.snd v) path2 with
                | Some _Some element
                | NoneNone
                end
            | NoneNone
            end) flat).
    Proof.
      apply (List.Sorted.filter_map Context.flatten_view_lt);
        [|apply Context.flatten_view_is_sorted].
      intros [] []; simpl.
      repeat destruct I.(INDEX.of_path) eqn:? in |- *;
        repeat destruct Tree.find eqn:? in |- *; trivial.
      repeat match goal with
      | H : I.(INDEX.of_path) ?path = Some _ |- _
        let H_inv := fresh "H_inv" in
        pose proof (P_is_valid.(Path_encoding.S.Valid.to_path_of_path) path)
          as H_inv;
        simpl in H_inv;
        rewrite H in H_inv;
        clear H
      end.
      hauto l: on.
    Qed.

Verification of the simulation for the [Make_set] functor.
    Lemma eq :
      Data_set_storage.Eq.t
        Substore
        (Data_set_storage.Make (P := P)
          (fun ctxt
            let view := Raw_context.context_value ctxt in
            Context.fold (Some (Context.Eq I.(INDEX.path_length)))
              view N1.(NAME.name) (Variant.Build "Sorted" unit tt)
              S.(_Set.S.empty)
              (fun k tree s
                let element :=
                  match
                    I.(INDEX.of_path) k,
                    Context.Tree.find tree N2.(NAME.name)
                  with
                  | Some element, Some _Some element
                  | _, _None
                  end in
                match element with
                | Some elementS.(_Set.S.add) element s
                | Nones
                end
            ))
          (fun ctxt change
            match change with
            | Data_set_storage.Change.Add val
              Substore.(Data_set_storage.add) ctxt val
            | Data_set_storage.Change.Clear
              Substore.(Data_set_storage.clear) ctxt
            | Data_set_storage.Change.Remove val
              Substore.(Data_set_storage.remove) ctxt val
            end)
        ).
    Proof.
      intros.
      constructor; simpl; intros; cbn.
      { unfold Make_indexed_subcontext.Raw_context.mem; cbn.
        rewrite INDEX.unpack_pack by trivial.
        unfold Raw_context.M.mem, Raw_context.mem,
          Make_indexed_subcontext.Raw_context.to_key; simpl.
        match goal with
        | |- context[I.(INDEX.to_path) ?value ?path] ⇒
          replace (I.(INDEX.to_path) value path) with
            (I.(INDEX.to_path) value [] ++ path) by sauto lq: on rew: off
        end.
        unfold Context.fold_sorted.
        erewrite List.fold_right_f_eq.
        erewrite List.fold_right_opt_map.
        2: reflexivity.
        unfold Context.mem.
        rewrite Context.find_tree_value_flatten_view_eq.
        unfold Context.find_tree_value_in_flatten_view.
        unfold Data_set_storage.Op.mem, Data_set_storage.State._Set.
        rewrite (_Set.mem_fold_right_add_eq Ord) by apply sorted_set_elements.
        replace (List.length (I.(INDEX.to_path) _ []))
          with I.(INDEX.path_length)
          by sauto lq: on.
        set (flat := flatten_view _ _ _).
        assert (
          H_match_find_map : {a b : Set} (f : a option b) l,
            match List.find_map f l with
            | Some _true
            | Nonefalse
            end =
            List.existsb
              (fun xmatch f x with Some _true | Nonefalse end)
              l
        ) by (induction l; hauto q: on).
        rewrite H_match_find_map; clear H_match_find_map.
        assert (
          H_mem_opt_map : {a b : Set} eqb (f : a option b) v l,
            List.mem eqb v (List.filter_map f l) =
            List.existsb
              (fun xmatch f x with Some yeqb v y | Nonefalse end)
              l
        ) by (induction l; hauto q: on).
        rewrite H_mem_opt_map; clear H_mem_opt_map.
        assert (
          H_existsb_ext : {a : Set} f1 f2 (l : list a),
            ( x, f1 x = f2 x)
            List.existsb f1 l = List.existsb f2 l
        ) by (induction l; hauto q: on).
        apply H_existsb_ext; clear H_existsb_ext.
        intros [path tree]; simpl.
        set (path_of_value := I.(INDEX.to_path) _ []).
        destruct Context.Key.eqb eqn:?.
        { assert (H_path : path_of_value = path)
            by now apply Context.Key.eqb_implies_eq.
          rewrite <- H_path.
          unfold path_of_value.
          rewrite P_is_valid.(Path_encoding.S.Valid.of_path_to_path).
          destruct Tree.find; trivial.
          unfold Context.Key.eqb, Data_set_storage.State.compare in ×.
          hauto lq: on use: Compare.Valid.refl, Context.Key.compare_is_valid.
        }
        { assert (H_path : path_of_value path)
            by scongruence use: Context.Key.eqb_refl.
          pose proof (P_is_valid.(Path_encoding.S.Valid.to_path_of_path) path).
          destruct I.(INDEX.of_path); trivial; simpl in ×.
          destruct Tree.find; trivial.
          destruct (_ =? _) eqn:?; trivial.
          unfold path_of_value, Data_set_storage.State.compare in ×.
          pose proof (Compare.Valid.zero Context.Key.compare_is_valid).
          match goal with
          | _ : (Context.Key.compare ?x1 ?x2 =? 0) = true |- _
            let H := fresh "H" in
            assert (H : Context.Key.compare x1 x2 = 0) by lia;
            pose proof (
              Compare.Valid.zero Context.Key.compare_is_valid x1 x2
                Logic.I Logic.I H);
            clear H
          end.
          hauto lq: on.
        }
      }
      { reflexivity. }
      { reflexivity. }
      { unfold Data_set_storage.Op.elements; fold S.
        rewrite app_nil_r.
        unfold fold_sorted.
        set (flat := flatten_view _ _ _).
        assert (H_fold_right_match :
           {a : Set} f (l : list a) acc,
          List.fold_right
            (fun v acc
              match f v with
              | Some elementS.(_Set.S.add) element acc
              | Noneacc
              end
            )
            l acc =
          List.fold_right S.(_Set.S.add) (List.filter_map f l) acc
        ) by (induction l; hauto lq: on).
        rewrite H_fold_right_match; clear H_fold_right_match.
        rewrite (_Set.elements_fold_right_add_eq Ord)
          by apply sorted_set_elements.
        assert (H_filter_map_fold_right :
           {a b : Set} (f : a option b) l,
          List.filter_map f l =
          List.fold_right
            (fun x acc
              match f x with
              | Some yy :: acc
              | Noneacc
              end
            )
            l []
        ) by (induction l; hauto lq: on).
        rewrite H_filter_map_fold_right; clear H_filter_map_fold_right.
        assert (H_fold_right_ext :
           {a b : Set} (P : a Prop) (f1 f2 : a b b) l acc,
          ( x acc,
            P x
            f1 x acc = f2 x acc
          )
          List.Forall P l
          List.fold_right f1 l acc =
          List.fold_right f2 l acc
        ) by (induction l; hauto q: on inv: List.Forall).
        eapply H_fold_right_ext; clear H_fold_right_ext;
          [|apply Context.flatten_view_forall_find].
        intros [path tree] acc []; simpl.
        replace (Tree.kind_value tree) with Kind.Tree by apply axiom.
        pose proof (P_is_valid.(Path_encoding.S.Valid.to_path_of_path) path).
        destruct I.(INDEX.of_path); trivial.
        unfold Make_indexed_subcontext.Raw_context.mem; cbn.
        rewrite INDEX.unpack_pack by trivial.
        unfold Raw_context.M.mem, Raw_context.mem, Context.mem,
          Make_indexed_subcontext.Raw_context.to_key; simpl.
        rewrite P_is_valid.(Path_encoding.S.Valid.to_path_postfix).
        qauto l: on.
      }
      { reflexivity. }
    Qed.
  End Make_set. End Make_set.

  Module Make_map.
    Module Unfold.
      Import Proto_alpha.Storage_functors.Make_indexed_subcontext.Make_map.

      Ltac all :=
        unfold
          get, mem, find,
          update, init_value, add, add_or_remove,
          remove_existing, remove,
          clear, keys, bindings, fold, fold_keys.
    End Unfold.

    Section Make_map.
      Context {ipath : Set Set} {C_t I_t V_t : Set}
        (I : INDEX (ipath := ipath) (t := I_t))
        (V : Storage_sigs.VALUE (t := V_t))
        (C : Raw_context.T (t := C_t)) (K : Raw_context.T.Kernel (t := C_t))
        (N : NAME)
        (I_is_valid : INDEX.Valid.t I)
        (K_is_valid : Raw_context.T.is_from_kernel C K)
        (P := INDEX.to_Path_encoding_S I)
        (M := Indexed_data_storage.State.Map P)
        (IC := Make_indexed_subcontext C I)
        (Subcontext := IC.(Storage_sigs.Indexed_raw_context.Raw_context))
        (Subkernel := Raw_context.Make_kernel I K)
        (Substore := IC.(Storage_sigs.Indexed_raw_context.Make_map) N V)
        (Ord := Indexed_data_storage.State.Ord P).

      Lemma expressed_from_kernel :
        Indexed_data_storage.Eq.t
          Substore
          (Indexed_data_storage.of_kernel
            P
            (K.(Raw_context.T.Kernel.absolute_key))
            N.(NAME.name)
            (Indexed_data_storage.to_kernel Substore)).
      Proof.
        assert (Subkernel_is_valid :
          Raw_context.T.is_from_kernel Subcontext Subkernel
        ) by (apply Raw_context.is_from_kernel; trivial).
        destruct Subkernel_is_valid; simpl in ×.
        constructor; simpl; intros; try reflexivity;
          Unfold.all;
          unfold Make_indexed_subcontext.fold_keys;
          cbn;
          repeat match goal with
          | H : _ |- _rewrite H
          end;
          simpl;
          try rewrite INDEX.unpack_pack; trivial;
          unfold
            Raw_context.mem,
            Raw_context.get,
            Raw_context.find,
            Raw_context.update,
            Raw_context.init_value,
            Raw_context.remove_existing;
          try set (full_key := (_ ++ _) ++ _);
          try set (root_ctxt := K.(Raw_context.T.Kernel.project) _).
        { destruct Context.find; simpl; [|reflexivity].
          destruct Make_encoder.of_bytes; reflexivity.
        }
        { rewrite INDEX.unpack_pack; trivial.
          destruct Context.mem; simpl; [|reflexivity].
          rewrite INDEX.unpack_pack; trivial.
        }
        { destruct Context.mem; simpl; [reflexivity|].
          repeat rewrite INDEX.unpack_pack; trivial.
        }
        { destruct Context.mem; simpl; [|reflexivity].
          repeat rewrite INDEX.unpack_pack; trivial.
        }
        all:
          destruct K_is_valid;
          repeat match goal with
          | H : _ |- _rewrite H
          end;
          simpl;
          unfold fold_sorted;
          set (flat := Context.flatten_view _ _ _);
          induction flat; simpl; [reflexivity|];
          rewrite IHflat;
          repeat match goal with
          | |- context[match ?e with __ end] ⇒ destruct e
          end; simpl; try reflexivity;
          scongruence.
      Qed.
    End Make_map.
  End Make_map.
End Make_indexed_subcontext.