🍃 Context.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Coq.Sorting.Sorted.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
#[local] Open Scope list.
Module Key.
Definition Compare : Compare.S (t := Context.key) :=
Compare.List {| Compare.COMPARABLE.compare := String.compare |}.
Definition compare : Context.key → Context.key → int :=
Compare.(Compare.S.compare).
Axiom compare_is_valid : Compare.Valid.t (fun _ ⇒ True) id compare.
Definition eqb : Context.key → Context.key → bool :=
Compare.(Compare.S.op_eq).
(* @TODO verify *)
Axiom eqb_implies_eq : ∀ path1 path2,
eqb path1 path2 = true →
path1 = path2.
Axiom eqb_refl : ∀ path,
eqb path path = true.
Definition lt (path1 path2 : Context.key) : Prop :=
Compare.(Compare.S.op_lt) path1 path2 = true.
End Key.
Require Import CoqOfOCaml.Settings.
Require Coq.Sorting.Sorted.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Map.
#[local] Open Scope list.
Module Key.
Definition Compare : Compare.S (t := Context.key) :=
Compare.List {| Compare.COMPARABLE.compare := String.compare |}.
Definition compare : Context.key → Context.key → int :=
Compare.(Compare.S.compare).
Axiom compare_is_valid : Compare.Valid.t (fun _ ⇒ True) id compare.
Definition eqb : Context.key → Context.key → bool :=
Compare.(Compare.S.op_eq).
(* @TODO verify *)
Axiom eqb_implies_eq : ∀ path1 path2,
eqb path1 path2 = true →
path1 = path2.
Axiom eqb_refl : ∀ path,
eqb path path = true.
Definition lt (path1 path2 : Context.key) : Prop :=
Compare.(Compare.S.op_lt) path1 path2 = true.
End Key.
Relate the [find] and [flatten_view] primitives.
Axiom flatten_view_find_In :
∀ (view : Context.t) (root path : key) (depth : int),
List.length path = depth →
(∃ v, Context.find view (op_at root path) = Some v) ↔
∃ t, In (path, t) (Context.flatten_view (Some (Eq depth)) view root).
∀ (view : Context.t) (root path : key) (depth : int),
List.length path = depth →
(∃ v, Context.find view (op_at root path) = Some v) ↔
∃ t, In (path, t) (Context.flatten_view (Some (Eq depth)) view root).
The ordering relation over [flatten_view].
The [flatten_view] is sorted.
Axiom flatten_view_is_sorted : ∀ view root depth,
Sorted.Sorted flatten_view_lt (Context.flatten_view depth view root).
Axiom flatten_view_forall_find : ∀ view root depth,
List.Forall
(fun '(path, tree) ⇒
(Context.Tree.to_value tree =
Context.find view (root ++ path)) ∧
(∀ sub_path,
Context.Tree.find tree sub_path =
Context.find view (root ++ path ++ sub_path))
)
(Context.flatten_view (Some (Context.Eq depth)) view root).
Definition find_value_in_flatten_view
(path : Context.key) (elements : list (Context.key × Context.tree)) :
option Context.value :=
List.find_map
(fun '(current_path, current_tree) ⇒
if Key.eqb path current_path then
Context.Tree.to_value current_tree
else
None
)
elements.
Axiom find_value_flatten_view_eq : ∀ view root path,
let depth := Some (Context.Eq (List.length path)) in
Context.find view (root ++ path) =
find_value_in_flatten_view path (Context.flatten_view depth view root).
Definition find_tree_value_in_flatten_view
(path1 path2 : Context.key) (elements : list (Context.key × Context.tree)) :
option Context.value :=
List.find_map
(fun '(current_path, current_tree) ⇒
if Key.eqb path1 current_path then
Context.Tree.find current_tree path2
else
None
)
elements.
Axiom find_tree_value_flatten_view_eq : ∀ view root path1 path2,
let depth := Some (Context.Eq (List.length path1)) in
Context.find view (root ++ path1 ++ path2) =
find_tree_value_in_flatten_view path1 path2
(Context.flatten_view depth view root).
Fixpoint filter_trees {a} (f : a → Kind.t) (xs : list a) : list a :=
match xs with
| [] ⇒ []
| x::ys ⇒
match f x with
| Kind.Tree ⇒ filter_trees f ys
| Kind.Value ⇒ x :: filter_trees f ys
end
end.
Lemma remove_kind_match : ∀ {a b : Set}
(f : a → Kind.t) (g : a → b → b) (xs : list a) y,
fold_right
(fun x acc ⇒
match f x with
| Kind.Tree ⇒ acc
| Kind.Value ⇒ g x acc
end) xs y =
fold_right g (filter_trees f xs) y.
induction xs; intros.
- reflexivity.
- simpl; destruct (f a0).
+ apply IHxs.
+ simpl; rewrite IHxs; reflexivity.
Qed.
Lemma opt_map_filter_tree : ∀ {a b : Set}
(f : a → Kind.t) (h : a → option b),
(∀ x, f x = Kind.Tree → h x = None) → ∀ xs,
List.filter_map h (filter_trees f xs) = List.filter_map h xs.
induction xs; intros.
- reflexivity.
- simpl.
+ destruct (f a0) eqn:F.
× rewrite (H a0 F); assumption.
× simpl.
destruct (h a0).
** congruence.
** exact IHxs.
Qed.
Sorted.Sorted flatten_view_lt (Context.flatten_view depth view root).
Axiom flatten_view_forall_find : ∀ view root depth,
List.Forall
(fun '(path, tree) ⇒
(Context.Tree.to_value tree =
Context.find view (root ++ path)) ∧
(∀ sub_path,
Context.Tree.find tree sub_path =
Context.find view (root ++ path ++ sub_path))
)
(Context.flatten_view (Some (Context.Eq depth)) view root).
Definition find_value_in_flatten_view
(path : Context.key) (elements : list (Context.key × Context.tree)) :
option Context.value :=
List.find_map
(fun '(current_path, current_tree) ⇒
if Key.eqb path current_path then
Context.Tree.to_value current_tree
else
None
)
elements.
Axiom find_value_flatten_view_eq : ∀ view root path,
let depth := Some (Context.Eq (List.length path)) in
Context.find view (root ++ path) =
find_value_in_flatten_view path (Context.flatten_view depth view root).
Definition find_tree_value_in_flatten_view
(path1 path2 : Context.key) (elements : list (Context.key × Context.tree)) :
option Context.value :=
List.find_map
(fun '(current_path, current_tree) ⇒
if Key.eqb path1 current_path then
Context.Tree.find current_tree path2
else
None
)
elements.
Axiom find_tree_value_flatten_view_eq : ∀ view root path1 path2,
let depth := Some (Context.Eq (List.length path1)) in
Context.find view (root ++ path1 ++ path2) =
find_tree_value_in_flatten_view path1 path2
(Context.flatten_view depth view root).
Fixpoint filter_trees {a} (f : a → Kind.t) (xs : list a) : list a :=
match xs with
| [] ⇒ []
| x::ys ⇒
match f x with
| Kind.Tree ⇒ filter_trees f ys
| Kind.Value ⇒ x :: filter_trees f ys
end
end.
Lemma remove_kind_match : ∀ {a b : Set}
(f : a → Kind.t) (g : a → b → b) (xs : list a) y,
fold_right
(fun x acc ⇒
match f x with
| Kind.Tree ⇒ acc
| Kind.Value ⇒ g x acc
end) xs y =
fold_right g (filter_trees f xs) y.
induction xs; intros.
- reflexivity.
- simpl; destruct (f a0).
+ apply IHxs.
+ simpl; rewrite IHxs; reflexivity.
Qed.
Lemma opt_map_filter_tree : ∀ {a b : Set}
(f : a → Kind.t) (h : a → option b),
(∀ x, f x = Kind.Tree → h x = None) → ∀ xs,
List.filter_map h (filter_trees f xs) = List.filter_map h xs.
induction xs; intros.
- reflexivity.
- simpl.
+ destruct (f a0) eqn:F.
× rewrite (H a0 F); assumption.
× simpl.
destruct (h a0).
** congruence.
** exact IHxs.
Qed.
Reading a value that we just added returns this value.
Axiom find_add_same : ∀ (ctxt : Context.t) (k : key) (v : value),
Context.find (Context.add ctxt k v) k = Some v.
Context.find (Context.add ctxt k v) k = Some v.
Reading a value at a different address is like reading the context before
the insertion.
Axiom find_add_different : ∀ (ctxt : Context.t) (k1 k2 : key) (v : value),
k1 ≠ k2 →
Context.find (Context.add ctxt k1 v) k2 = Context.find ctxt k2.
k1 ≠ k2 →
Context.find (Context.add ctxt k1 v) k2 = Context.find ctxt k2.
Rewrite either [find_add_same] or [find_add_different] depending on which
one fits better.
Ltac rewrite_find_add :=
match goal with
| |- context[Context.find (Context.add _ ?k _) ?k] ⇒
rewrite Context.find_add_same
| |- context[Context.find (Context.add _ ?k1 _) ?k2] ⇒
rewrite Context.find_add_different by now cbv
end.
match goal with
| |- context[Context.find (Context.add _ ?k _) ?k] ⇒
rewrite Context.find_add_same
| |- context[Context.find (Context.add _ ?k1 _) ?k2] ⇒
rewrite Context.find_add_different by now cbv
end.
Module PROOF_ENCODING.
Module Valid.
Import Environment.V8.Context.PROOF_ENCODING.
Record t (x : Context.PROOF_ENCODING) : Prop := {
tree_proof_encoding :
Data_encoding.Valid.t (fun _ ⇒ True) x.(tree_proof_encoding);
stream_proof_encoding :
Data_encoding.Valid.t (fun _ ⇒ True) x.(stream_proof_encoding);
}.
End Valid.
End PROOF_ENCODING.
Module Proof_encoding.
Module V1.
Axiom Tree32_is_valid :
PROOF_ENCODING.Valid.t Context.Proof_encoding.V1.Tree32.
Axiom Tree2_is_valid :
PROOF_ENCODING.Valid.t Context.Proof_encoding.V1.Tree2.
End V1.
Module V2.
Axiom Tree32_is_valid :
PROOF_ENCODING.Valid.t Context.Proof_encoding.V2.Tree32.
Axiom Tree2_is_valid :
PROOF_ENCODING.Valid.t Context.Proof_encoding.V2.Tree2.
End V2.
End Proof_encoding.
Module Cache.
We assume that the sync of the cache is the identity.
Axiom sync_eq : ∀ ctxt cache_nonce,
Context.Cache.(Context.CACHE.sync) ctxt cache_nonce = ctxt.
End Cache.
Context.Cache.(Context.CACHE.sync) ctxt cache_nonce = ctxt.
End Cache.