💾 Storage_description.v
Proofs
See code, See simulations, Gitlab , OCaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_arg.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_query.
Require TezosOfOCaml.Proto_alpha.Proofs.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Simulations.Storage_description.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Storage_description.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_arg.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_query.
Require TezosOfOCaml.Proto_alpha.Proofs.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Simulations.Storage_description.
Our dependent veresion of [unpack] is equivalent to the original one.
Fixpoint dep_unpack_eq {a b c : Set}
(v : Storage_description.dep_args a b c) (x : c) {struct v} :
Storage_description.dep_unpack v x =
Storage_description.unpack (Storage_description.to_args v) x.
Proof.
destruct v; simpl.
{ now rewrite cast_eval. }
{ match goal with
| _ : Storage_description.dep_args _ ?a ?inter_key,
_ : Storage_description.dep_args ?inter_key ?b _
|- context[cast_exists (Es := ?Es) ?T ?x] ⇒
match Es with
| [Set ** Set ** Set] ⇒
rewrite (cast_exists_eval_3 (T := T)
(E1 := inter_key) (E2 := b) (E3 := a))
end
end; rewrite cast_eval.
now repeat (rewrite dep_unpack_eq; destruct Storage_description.unpack).
}
Qed.
(v : Storage_description.dep_args a b c) (x : c) {struct v} :
Storage_description.dep_unpack v x =
Storage_description.unpack (Storage_description.to_args v) x.
Proof.
destruct v; simpl.
{ now rewrite cast_eval. }
{ match goal with
| _ : Storage_description.dep_args _ ?a ?inter_key,
_ : Storage_description.dep_args ?inter_key ?b _
|- context[cast_exists (Es := ?Es) ?T ?x] ⇒
match Es with
| [Set ** Set ** Set] ⇒
rewrite (cast_exists_eval_3 (T := T)
(E1 := inter_key) (E2 := b) (E3 := a))
end
end; rewrite cast_eval.
now repeat (rewrite dep_unpack_eq; destruct Storage_description.unpack).
}
Qed.
Our dependent veresion of [_pack] is equivalent to the original one.
Fixpoint dep_pack_eq {a b c : Set}
(v : Storage_description.dep_args a b c) (x : a) (y : b) {struct v} :
Storage_description.dep_pack v x y =
Storage_description._pack (Storage_description.to_args v) x y.
Proof.
destruct v; simpl.
{ now rewrite cast_eval. }
{ match goal with
| _ : Storage_description.dep_args _ ?a ?inter_key,
_ : Storage_description.dep_args ?inter_key ?b _
|- context[cast_exists (Es := ?Es) ?T ?x] ⇒
match Es with
| [Set ** Set ** Set] ⇒
rewrite (cast_exists_eval_3 (T := T)
(E1 := inter_key) (E2 := b) (E3 := a))
end
end; rewrite cast_eval.
destruct y.
now repeat rewrite dep_pack_eq.
}
Qed.
(v : Storage_description.dep_args a b c) (x : a) (y : b) {struct v} :
Storage_description.dep_pack v x y =
Storage_description._pack (Storage_description.to_args v) x y.
Proof.
destruct v; simpl.
{ now rewrite cast_eval. }
{ match goal with
| _ : Storage_description.dep_args _ ?a ?inter_key,
_ : Storage_description.dep_args ?inter_key ?b _
|- context[cast_exists (Es := ?Es) ?T ?x] ⇒
match Es with
| [Set ** Set ** Set] ⇒
rewrite (cast_exists_eval_3 (T := T)
(E1 := inter_key) (E2 := b) (E3 := a))
end
end; rewrite cast_eval.
destruct y.
now repeat rewrite dep_pack_eq.
}
Qed.
[dep_unpack] is the inverse of [dep_pack].
Fixpoint dep_unpack_dep_pack {a b c : Set}
(v : Storage_description.dep_args a b c) (x : a) (y : b) {struct v} :
Storage_description.dep_unpack v (Storage_description.dep_pack v x y) =
(x, y).
Proof.
destruct v; simpl; try reflexivity.
Tactics.destruct_pairs.
now repeat rewrite dep_unpack_dep_pack.
Qed.
(v : Storage_description.dep_args a b c) (x : a) (y : b) {struct v} :
Storage_description.dep_unpack v (Storage_description.dep_pack v x y) =
(x, y).
Proof.
destruct v; simpl; try reflexivity.
Tactics.destruct_pairs.
now repeat rewrite dep_unpack_dep_pack.
Qed.
[dep_pack] is the inverse of [dep_unpack].
Fixpoint dep_pack_dep_unpack {a b c : Set}
(v : Storage_description.dep_args a b c) (z : c) {struct v} :
(let '(x, y) := Storage_description.dep_unpack v z in
Storage_description.dep_pack v x y) =
z.
Proof.
destruct v; Tactics.destruct_pairs; simpl; try reflexivity.
repeat match goal with
| |- context[Storage_description.dep_unpack ?v ?z] ⇒
pose proof (dep_pack_dep_unpack _ _ _ v z);
destruct (Storage_description.dep_unpack v z)
end.
congruence.
Qed.
Module INDEX.
Definition to_Path {t : Set} (I : Storage_description.INDEX (t := t))
: Path_encoding.S (t := t) := {|
Path_encoding.S.to_path := I.(Storage_description.INDEX.to_path);
Path_encoding.S.of_path := I.(Storage_description.INDEX.of_path);
Path_encoding.S.path_length := I.(Storage_description.INDEX.path_length);
|}.
Module Valid.
Record t {t : Set} (domain : t → Prop)
(I : Storage_description.INDEX (t := t)) : Prop := {
Path_is_valid : Path_encoding.S.Valid.t (to_Path I);
rpc_arg : RPC_arg.Valid.t domain I.(Storage_description.INDEX.rpc_arg);
encoding_is_valid :
Data_encoding.Valid.t domain I.(Storage_description.INDEX.encoding);
compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id
I.(Storage_description.INDEX.compare);
}.
End Valid.
End INDEX.
Module Query.
(v : Storage_description.dep_args a b c) (z : c) {struct v} :
(let '(x, y) := Storage_description.dep_unpack v z in
Storage_description.dep_pack v x y) =
z.
Proof.
destruct v; Tactics.destruct_pairs; simpl; try reflexivity.
repeat match goal with
| |- context[Storage_description.dep_unpack ?v ?z] ⇒
pose proof (dep_pack_dep_unpack _ _ _ v z);
destruct (Storage_description.dep_unpack v z)
end.
congruence.
Qed.
Module INDEX.
Definition to_Path {t : Set} (I : Storage_description.INDEX (t := t))
: Path_encoding.S (t := t) := {|
Path_encoding.S.to_path := I.(Storage_description.INDEX.to_path);
Path_encoding.S.of_path := I.(Storage_description.INDEX.of_path);
Path_encoding.S.path_length := I.(Storage_description.INDEX.path_length);
|}.
Module Valid.
Record t {t : Set} (domain : t → Prop)
(I : Storage_description.INDEX (t := t)) : Prop := {
Path_is_valid : Path_encoding.S.Valid.t (to_Path I);
rpc_arg : RPC_arg.Valid.t domain I.(Storage_description.INDEX.rpc_arg);
encoding_is_valid :
Data_encoding.Valid.t domain I.(Storage_description.INDEX.encoding);
compare_is_valid :
Compare.Valid.t (fun _ ⇒ True) id
I.(Storage_description.INDEX.compare);
}.
End Valid.
End INDEX.
Module Query.
Validity predicate for a query.
Module Valid.
Import Storage_description.query.
Record t (q : Storage_description.query) : Prop := {
depth : Pervasives.Int.Valid.non_negative q.(depth);
}.
End Valid.
End Query.
Import Storage_description.query.
Record t (q : Storage_description.query) : Prop := {
depth : Pervasives.Int.Valid.non_negative q.(depth);
}.
End Valid.
End Query.
The query [depth_query] is valid.
Lemma depth_query_is_valid :
RPC_query.Valid.t Query.Valid.t Storage_description.depth_query.
Proof.
RPC_query.valid_auto.
Qed.
RPC_query.Valid.t Query.Valid.t Storage_description.depth_query.
Proof.
RPC_query.valid_auto.
Qed.