💾 Storage_functors.v
Proofs
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;
|}.
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 x ⇒ x)
(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.
(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 x ⇒ x)
(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.
(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.
(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 p ⇒ I.(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
| None ⇒ s
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.
(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 p ⇒ I.(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
| None ⇒ s
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.
{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.
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).
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.
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).
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.
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
).
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).
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.
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.
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.
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.
Indexed_data_storage.Valid.t of_to_Simulation.
Proof.
constructor; intros; apply List.fold_right_f_eq; hauto lq: on.
Qed.
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 x ⇒ let× 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 y ⇒ f1 y
| None ⇒ default
end =
match List.find_map g2 l with
| Some y ⇒ f2 y
| None ⇒ default
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 x ⇒ let× 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 y ⇒ y :: acc
| None ⇒ acc
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
].
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 ].
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.
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;
|}.
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.
(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
| None ⇒ None
end
| None ⇒ None
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.
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
| None ⇒ None
end
| None ⇒ None
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 element ⇒ S.(_Set.S.add) element s
| None ⇒ s
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
| None ⇒ false
end =
List.existsb
(fun x ⇒ match f x with Some _ ⇒ true | None ⇒ false 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 x ⇒ match f x with Some y ⇒ eqb v y | None ⇒ false 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 element ⇒ S.(_Set.S.add) element acc
| None ⇒ acc
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 y ⇒ y :: acc
| None ⇒ acc
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.
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 element ⇒ S.(_Set.S.add) element s
| None ⇒ s
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
| None ⇒ false
end =
List.existsb
(fun x ⇒ match f x with Some _ ⇒ true | None ⇒ false 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 x ⇒ match f x with Some y ⇒ eqb v y | None ⇒ false 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 element ⇒ S.(_Set.S.add) element acc
| None ⇒ acc
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 y ⇒ y :: acc
| None ⇒ acc
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.