Library zoo_persistent.pstore_1
From zoo Require Import
prelude.
From zoo.iris.base_logic Require Import
lib.mono_gset.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
assert
list.
From zoo_persistent Require Export
base
pstore_1__code.
From zoo_persistent Require Import
pstore_1__types.
From zoo Require Import
options.
Implicit Types l : location.
Implicit Types v t s : val.
Implicit Types σ : gmap location val.
Section map.
Context `{Countable K}.
Context {V : Type}.
Lemma gmap_included_insert (σ1 σ2:gmap K V) (l:K) (v:V) :
σ1 ⊆ σ2 →
<[l:=v]>σ1 ⊆ <[l:=v]>σ2.
Lemma gmap_included_insert_notin (σ1 σ2:gmap K V) (l:K) (v:V) :
l ∉ dom σ1 →
σ1 ⊆ σ2 →
σ1 ⊆ <[l:=v]>σ2.
Lemma incl_dom_incl (σ1 σ2:gmap K V) :
σ1 ⊆ σ2 →
dom σ1 ⊆ dom σ2.
End map.
Section list.
Context {A : Type}.
Lemma list_case_r (l:list A) :
l = nil ∨ ∃ (l':list A) x, l = l' ++ [x].
Lemma elem_of_middle (x:A) (xs:list A) :
x ∈ xs →
∃ (l1 l2:list A), xs = l1 ++ x::l2.
End list.
Section graph.
Definition graph (A B : Type) `{Countable A} `{Countable B} :=
gset (A × B × A).
Context `{Countable A} `{Countable B}.
Definition vertices (g:graph A B) : gset A :=
set_fold (fun '(x,_,y) acc ⇒ {[x;y]} ∪ acc) ∅ g.
Lemma vertices_empty :
vertices ∅ = ∅.
Definition proj1 {A B C:Type} (x:(A×B×C)) : A :=
match x with (x,_,_) ⇒ x end.
Definition proj2 {A B C:Type} (x:(A×B×C)) : B :=
match x with (_,x,_) ⇒ x end.
Definition proj3 {A B C:Type} (x:(A×B×C)) : C :=
match x with (_,_,x) ⇒ x end.
Lemma elem_of_vertices x (g:graph A B) :
x ∈ vertices g ↔ ∃ b y, ((x,b,y) ∈ g ∨ (y,b,x) ∈ g).
Lemma vertices_singleton (x:(A×B×A)) :
vertices {[x]} = {[proj1 x; proj3 x]}.
Lemma vertices_union (g1 g2:graph A B) :
vertices (g1 ∪ g2) = vertices g1 ∪ vertices g2.
Definition edge (g:graph A B) x c y :=
(x,c,y) ∈ g.
Inductive path (g:graph A B) : A → list (A×B×A) → A → Prop :=
| path_nil a :
path g a [] a
| path_cons a1 b a2 bs a3 :
(a1,b,a2) ∈ g →
path g a2 bs a3 →
path g a1 ((a1,b,a2)::bs) a3.
Lemma path_app_inv g a1 a2 xs ys :
path g a1 (xs ++ ys) a2 →
∃ a, path g a1 xs a ∧ path g a ys a2.
Lemma path_snoc_inv g a1 a2 a3 a4 b xs :
path g a1 (xs ++ [(a2,b,a3)]) a4 →
path g a1 xs a2 ∧ a3 = a4 ∧ (a2,b,a3) ∈ g.
Definition acyclic g := ∀ a xs, path g a xs a → xs = nil.
Record rooted_dag g (r:A) :=
{ ti1 : ∀ a, a ∈ vertices g → ∃ xs, path g a xs r
; ti2 : acyclic g
}.
Definition unaliased (g:graph A B) :=
∀ r x1 r1 x2 r2,
(r,x1,r1) ∈ g →
(r,x2,r2) ∈ g →
x1 = x2 ∧ r1 = r2.
Lemma path_app (g:graph A B) x3 x1 xs ys x2 :
path g x1 xs x3 →
path g x3 ys x2 →
path g x1 (xs++ys) x2.
Definition all_uniq_path g :=
∀ a1 a2 xs ys, path g a1 xs a2 → path g a1 ys a2 → xs = ys.
Lemma rooted_tree_impl_acyclic_unaliased g r :
(∀ a, a ∈ vertices g → ∃ xs, path g a xs r) →
all_uniq_path g →
acyclic g ∧ unaliased g. Lemma acyclic_unaliased_impl_uniq_path g :
acyclic g →
unaliased g →
all_uniq_path g.
Lemma rooted_dag_empty (r:A) :
rooted_dag (∅ : graph A B) r.
Lemma path_cycle_end_inv_aux g (r r':A) b ds x1 x2 :
r ≠ r' →
x2 ≠ r' →
r' ∉ vertices g →
path ({[(r, b, r')]} ∪ g) x1 ds x2 →
path g x1 ds x2.
Lemma path_cycle_end_inv g (r r':A) b ds x :
r ≠ r' →
r' ∉ vertices g →
path ({[(r, b, r')]} ∪ g) x ds x →
path g x ds x.
Lemma path_snoc g a1 b a2 bs a3 :
path g a1 bs a2 →
(a2,b,a3) ∈ g →
path g a1 (bs++[(a2,b,a3)]) a3.
Lemma path_weak g1 g2 x bs y :
path g1 x bs y →
g1 ⊆ g2 →
path g2 x bs y.
Lemma rooted_dag_add (r r':A) g x:
r ≠ r' →
r' ∉ vertices g →
rooted_dag g r →
rooted_dag ({[(r, x, r')]} ∪ g) r'.
Lemma acyclic_weak (g1 g2:graph A B) :
acyclic g1 →
g2 ⊆ g1 →
acyclic g2.
Lemma path_all_in (g:graph A B) a1 xs a2 :
path g a1 xs a2 →
list_to_set xs ⊆ g.
Lemma path_restrict (g:graph A B) r xs r' :
path g r xs r' →
path (list_to_set xs) r xs r'.
Lemma path_inv_r (g:graph A B) x bs z :
path g x bs z →
(x = z ∧ bs = nil) ∨ ∃ bs' b y, bs = bs' ++ [(y,b,z)] ∧ path g x bs' y ∧ (y,b,z) ∈ g.
Lemma path_add_inv_r (r r':A) b x xs g :
r ≠ r' →
r' ∉ vertices g →
path ({[(r, b, r')]} ∪ g) x xs r' →
(xs = nil ∧ x = r') ∨ (∃ xs', xs = xs' ++ [(r, b, r')] ∧ path g x xs' r).
Inductive mirror : list (A×B×A) → list (A×B×A) → Prop :=
| mirror_nil :
mirror [] []
| mirror_cons r x x' r' xs ys :
mirror xs ys →
mirror (xs++[(r,x,r')]) ((r',x',r)::ys).
Lemma mirror_snoc ys xs a a' x x' :
mirror ys xs →
mirror ((a,x,a') :: ys) (xs ++ [(a',x',a)]).
Lemma mirror_symm xs ys :
mirror xs ys → mirror ys xs.
Lemma use_mirror xs ys (g:graph A B) r y :
mirror xs ys →
path g r xs y →
path (list_to_set ys) y ys r.
Lemma mirror_vertices (xs ys:list (A×B×A)) :
mirror xs ys →
vertices (list_to_set ys) = vertices (list_to_set xs).
Lemma mirror_same_length (xs ys:list (A×B×A)):
mirror xs ys →
length xs = length ys.
Lemma mirror_mirrored_edges xs ys r x r' :
mirror xs ys →
(r,x,r') ∈ xs → ∃ x', (r',x',r) ∈ ys.
Lemma path_middle (g:graph A B) x xs ys z :
path g x (xs ++ ys) z →
∃ y, path g x xs y ∧ path g y ys z.
Lemma use_mirror_subset xs ys xs' g r y :
xs' ⊆ xs →
mirror xs ys →
path g r xs' y →
∃ zs, path (list_to_set ys) y zs r ∧ length xs' = length zs.
Definition pathlike (ys:list (A×B×A)) r :=
∀ a b a', (a,b,a') ∈ ys → a' = r ∨ ∃ b' a'', (a',b',a'') ∈ ys.
Lemma path_pathlike g r ys y :
path g y ys r →
pathlike ys r.
Lemma same_path g (xs:list (A×B×A)) a1 a2 a3 a4 :
path g a1 xs a2 →
path g a3 xs a4 →
xs ≠ nil →
a1 = a3 ∧ a2=a4.
Lemma path_ends_vertices g x1 xs x2 :
path g x1 xs x2 →
(x1 = x2) ∨ (x1 ∈ vertices g ∧ x2 ∈ vertices g).
End graph.
Section adiffl.
Notation diff := (
location×val
)%type.
Definition apply_diffl (ds:list diff) (σ:gmap location val) : gmap location val :=
foldr (fun '(l,v) σ ⇒ <[l:=v]> σ) σ ds.
Lemma dom_apply_diffl ds σ :
dom (apply_diffl ds σ) = dom σ ∪ (list_to_set ds.*1).
Lemma apply_diffl_insert_ne ds l v σ :
l ∉ ds.*1 →
apply_diffl ds (<[l:=v]> σ) = <[l:=v]> (apply_diffl ds σ).
Lemma apply_diffl_app ds ds' σ :
apply_diffl (ds++ds') σ = apply_diffl ds (apply_diffl ds' σ).
Lemma apply_diffl_snoc xs l v σ :
apply_diffl (xs ++ [(l,v)]) σ = apply_diffl xs (<[l:=v]> σ).
Lemma apply_diffl_cons l v xs σ :
apply_diffl ((l,v)::xs) σ = <[l:=v]> (apply_diffl xs σ).
Lemma apply_diffl_included xs σ1 σ2 :
σ1 ⊆ σ2 →
apply_diffl xs σ1 ⊆ apply_diffl xs σ2.
End adiffl.
Class Pstore1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] pstore_1_G_set_G :: MonoGsetG Σ (location × gmap location val)%type
}.
Definition pstore_1_Σ :=
#[mono_gset_Σ (location × gmap location val)%type
].
#[global] Instance subG_pstore_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG pstore_1_Σ Σ →
Pstore1G Σ.
Section pstore_1_G.
Context `{pstore_1_G : Pstore1G Σ}.
Notation diff := (
location×val
)%type.
Notation graph_store := (
graph location diff
).
Notation map_model := (
gmap location (gmap location val)
).
Definition correct_path_diff (M:map_model) (g:graph_store) :=
∀ r1 ds r2 σ1 σ2,
path g r1 ds r2 → M !! r1 = Some σ1 → M !! r2 = Some σ2 →
σ1 = (apply_diffl (proj2 <$> ds) σ2).
Record store_inv (M:map_model) (g:graph_store) (r:location) (σ σ0:gmap location val) :=
{ si1 : dom M = vertices g ∪ {[r]}
; si2 : σ ⊆ σ0
; si3 : M !! r = Some σ0
; si4 : correct_path_diff M g
}.
Definition locations_of_edges_in g (X:gset location) :=
∀ (r:location) l v r', edge g r (l,v) r' → l ∈ X.
Record coherent (M:map_model) (σ0:gmap location val) (g:graph_store) :=
{ coh1 : ∀ r σ, M !! r = Some σ → dom σ = dom σ0
; coh2 : locations_of_edges_in g (dom σ0)
}.
Definition snapshot_inv (M:map_model) (C:gset (location × gmap location val)) :=
∀ l σ, (l,σ) ∈ C → ∃ σ', M !! l = Some σ' ∧ σ ⊆ σ'.
#[local] Definition pstore_1_map_auth (γ:gname) (s:gset (location*(gmap location val))) :=
mono_gset_auth γ (DfracOwn 1) s.
#[local] Definition pstore_1_map_elem γ l σ :=
mono_gset_elem γ (l,σ).
Lemma extract_unaliased (g : graph_store) :
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) -∗
⌜unaliased g⌝.
#[local] Definition snapshosts_model (t0:location) (M:map_model) : iProp Σ :=
∃ (γ:gname) (C:gset (location × gmap location val)),
⌜snapshot_inv M C⌝ ∗ meta t0 nroot γ ∗ pstore_1_map_auth γ C.
#[local] Definition pstore_1 (t:val) (σ:gmap location val) : iProp Σ :=
∃ (t0 r:location)
(σ0:gmap location val)
(g:graph_store)
(M:map_model),
⌜t=#t0 ∧ store_inv M g r σ σ0 ∧ coherent M σ0 g ∧ rooted_dag g r⌝ ∗
t0 ↦ᵣ #r ∗
r ↦ᵣ §Root ∗
snapshosts_model t0 M ∗
([∗ map] l ↦ v ∈ σ0, l ↦ᵣ v) ∗
([∗ set] x ∈ g, let '(r,(l,v),r') := x in r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) .
Definition open_inv : string :=
"[%t0 [%r [%σ0 [%g [%M ((->&%Hinv&%Hcoh&%Hgraph)&Ht0&Hr&HC&Hσ0&Hg)]]]]]".
Definition pstore_1_snapshot t s σ : iProp Σ :=
∃ γ (t0:location) l, ⌜t=#t0 ∧ s=ValTuple [t;#l]⌝ ∗ meta t0 nroot γ ∗ pstore_1_map_elem γ l σ.
#[global] Instance pstore_1_snapshot_timeless t s σ :
Timeless (pstore_1_snapshot t s σ).
#[global] Instance pstore_1_snapshot_persistent t s σ :
Persistent (pstore_1_snapshot t s σ).
Lemma pstore_1٠create𑁒spec :
{{{
True
}}}
pstore_1٠create ()
{{{
t
, RET t;
pstore_1 t ∅
}}}.
Lemma use_locations_of_edges_in g r xs r' X :
locations_of_edges_in g X →
path g r xs r' →
(list_to_set (proj2 <$> xs).*1) ⊆ X.
Lemma pstore_1٠ref𑁒spec t σ v :
{{{
pstore_1 t σ
}}}
pstore_1٠ref t v
{{{
l
, RET #l;
⌜l ∉ dom σ⌝ ∗
pstore_1 t (<[l := v]> σ)
}}}.
Lemma pstore_1٠get𑁒spec {t σ l} v :
σ !! l = Some v →
{{{
pstore_1 t σ
}}}
pstore_1٠get t #l
{{{
RET v;
pstore_1 t σ
}}}.
Lemma pstore_1٠set𑁒spec t σ l v :
l ∈ dom σ →
{{{
pstore_1 t σ
}}}
pstore_1٠set t #l v
{{{
RET ();
pstore_1 t (<[l := v]> σ)
}}}.
Lemma pstore_1٠capture𑁒spec t σ :
{{{
pstore_1 t σ
}}}
pstore_1٠capture t
{{{
s
, RET s;
pstore_1 t σ ∗
pstore_1_snapshot t s σ
}}}.
Definition fsts (ys:list (location*(location×val)*location)) : list val :=
(fun '(x,_,_) ⇒ ValLoc x) <$> ys.
Lemma pstore_1٠collect𑁒spec_aux (r r':location) t' (xs:list val) (ys:list (location*(location×val)*location)) (g:graph_store) :
list_model' t' xs →
path g r ys r' →
{{{
r' ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) ))
}}}
pstore_1٠collect #r t'
{{{
t
, RET (#r',t);
r' ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
list_model t (rev_append (fsts ys) xs)
}}}.
Lemma pstore_1٠collect𑁒spec (r r':location) (ys:list (location*(location×val)*location)) (g:graph_store) :
path g r ys r' →
{{{
r' ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) ))
}}}
pstore_1٠collect #r []
{{{
t
, RET (#r',t);
r' ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
list_model t (rev (fsts ys))
}}}.
Lemma use_path r g (xs:list (location*(location×val)*location)) r0 x r1 r':
list_to_set xs ⊆ g →
path g r (xs ++ [(r0, x, r1)]) r' →
(r0, x, r1) ∈ (list_to_set xs : gset(location*(location×val)*location) ) →
∃ ds, path g r0 ds r0 ∧ ds ≠ nil.
Inductive undo : list (location*(location×val)*location) → list (location*(location×val)*location) → gmap location val → Prop :=
| undo_nil :
∀ σ, undo [] [] σ
| undo_cons σ r l v v' r' xs ys :
σ !! l = Some v' →
undo xs ys (<[l:=v]> σ) →
undo (xs++[(r,(l,v),r')]) ((r',(l,v'),r)::ys) σ.
Lemma use_undo xs ys σ :
undo xs ys σ →
σ = apply_diffl (proj2 <$> ys ++ xs) σ.
Lemma undo_mirror xs ys g :
undo xs ys g →
mirror xs ys.
Lemma pstore_1٠revert𑁒spec_aux g g1 r t g2 xs r' w σ σ0 :
list_model' t (fsts (rev xs)) →
locations_of_edges_in g2 (dom σ) →
g2 = list_to_set xs →
acyclic g →
g2 ⊆ g →
path g r xs r' →
{{{
r' ↦ᵣ w ∗
([∗ map] l0↦v0 ∈ σ, l0 ↦ᵣ v0) ∗
([∗ set] '(r, (l, v), r') ∈ g1, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
([∗ set] '(r, (l, v), r') ∈ g2, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) ))
}}}
pstore_1٠revert #r' t
{{{
RET ();
∃ ys,
⌜undo xs ys σ⌝ ∗
r ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ (g1 ∪ list_to_set ys), r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
([∗ map] l0↦v0 ∈ (apply_diffl (proj2 <$> xs) σ), l0 ↦ᵣ v0)
}}}.
Lemma pstore_1٠revert𑁒spec r t g xs r' w σ σ0 :
list_model' t (fsts (rev xs)) →
locations_of_edges_in g (dom σ) →
g = list_to_set xs →
acyclic g →
path g r xs r' →
{{{
r' ↦ᵣ w ∗
([∗ map] l0↦v0 ∈ σ, l0 ↦ᵣ v0) ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) ))
}}}
pstore_1٠revert #r' t
{{{
RET ();
∃ ys,
⌜undo xs ys σ⌝ ∗
r ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ (list_to_set ys), r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
([∗ map] l0↦v0 ∈ (apply_diffl (proj2 <$> xs) σ), l0 ↦ᵣ v0)
}}}.
Lemma rev_fsts xs :
rev (fsts xs) = fsts (rev xs).
Lemma pstore_1٠reroot𑁒spec r (xs:list (location*(location×val)*location)) r' g σ :
locations_of_edges_in g (dom σ) →
g = list_to_set xs →
acyclic g →
path g r xs r' →
{{{
r' ↦ᵣ §Root ∗
([∗ map] l0↦v0 ∈ σ, l0 ↦ᵣ v0) ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) ))
}}}
pstore_1٠reroot #r
{{{
RET ();
∃ ys,
⌜undo xs ys σ⌝ ∗
r ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ (list_to_set ys), r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
([∗ map] l0↦v0 ∈ (apply_diffl (proj2 <$> xs) σ), l0 ↦ᵣ v0)
}}}.
Lemma locations_of_edges_weak g1 g2 X :
locations_of_edges_in g1 X →
g2 ⊆ g1 →
locations_of_edges_in g2 X.
Lemma undo_same_fst_label xs ys r l v r' σ :
undo xs ys σ →
(r, (l, v), r') ∈ (list_to_set ys : gset (location*(location×val)*location)) →
l ∈ (list_to_set (proj2 <$> xs).*1 : gset location).
Definition diff_last {A:Type} (ys1 ys2:list A) :=
match last ys1, last ys2 with
| Some x, Some y ⇒
x ≠ y
| _, _ ⇒
True
end.
Lemma path_extract_suffix (g:gset (location*(location×val)*location)) a1 a2 xs1 r xs2 :
unaliased g →
path g a1 xs1 r →
path g a2 xs2 r →
∃ ys1 ys2 xs,
xs1 = ys1 ++ xs ∧
xs2 = ys2 ++ xs ∧ diff_last ys1 ys2.
Lemma diff_last_app_middle {A:Type} x (l1' l2' l1 l2:list A) :
diff_last (l1' ++ x :: l2') (l1 ++ x :: l2) →
diff_last (x :: l2') (x :: l2).
Lemma diff_last_irrefl {A:Type} (l:list A) :
l ≠ nil →
¬ (diff_last l l).
Lemma path_use_diff_last (g:gset (location*(location×val)*location)) a1 a2 ys1 ys2 xs r :
acyclic g →
unaliased g →
path g a1 (ys1 ++ xs) r →
path g a2 (ys2 ++ xs) r →
diff_last ys1 ys2 →
∀ x, x ∈ ys2 → x ∉ (ys1 ++ xs).
Lemma diff_last_comm {A:Type} (l1 l2:list A) :
diff_last l1 l2 ↔ diff_last l2 l1.
Lemma path_union_inv (g1: graph location (location×val)) g2 a1 xs a2 :
path (g1 ∪ g2) a1 xs a2 →
path g1 a1 xs a2 ∨ ∃ a' x xs1 xs2, path g1 a1 xs1 a' ∧ x ∈ g2 ∧ path (g1 ∪ g2) a' (x::xs2) a2 ∧ xs=xs1++x::xs2.
Lemma path_cannot_escape (x:(location × diff × location)) (xs ys:list (location × diff × location)) (g1: graph location (location×val)) a a' r :
(∀ x l', ¬ (r,x,l') ∈ (g1 ∪ list_to_set ys)) →
unaliased (g1 ∪ list_to_set ys) →
x ∈ (list_to_set ys : gset _) →
pathlike ys r →
path (g1 ∪ list_to_set ys) a (x :: xs) a' →
path (list_to_set ys) a (x::xs) a'.
Lemma path_in_seg_complete (r a a':location) (x:(location × diff × location)) (xs0 xs1 ys: list (location × diff × location)) (g1:graph location (location×val)) :
(∀ x l', ¬ (r,x,l') ∈ (g1 ∪ list_to_set ys)) →
unaliased (g1 ∪ list_to_set ys) →
pathlike ys r →
path (g1 ∪ list_to_set ys) a xs0 a' →
path (list_to_set ys) a' (x :: xs1) a →
∃ zs, path (list_to_set ys) a zs a'.
Lemma undo_preserves_rooted_dag (g:graph location (location×val)) xs ys rs r :
(∀ x l', ¬ (rs,x,l') ∈ (list_to_set ys ∪ g ∖ list_to_set xs)) →
unaliased g →
unaliased (list_to_set ys ∪ g ∖ list_to_set xs) →
path g rs xs r →
mirror xs ys →
rooted_dag g r →
rooted_dag (list_to_set ys ∪ g ∖ list_to_set xs) rs.
Lemma undo_app_inv xs ys1 ys2 σ :
undo xs (ys1 ++ ys2) σ →
∃ xs1 xs2, xs = xs2 ++ xs1 ∧ undo xs2 ys2 (apply_diffl (proj2 <$> xs1) σ) ∧ undo xs1 ys1 σ.
Lemma construct_middlepoint (g:graph location (location×val)) a1 xs ys a2 a2' :
unaliased g →
(∀ x l', ¬ (a2,x,l') ∈ g) →
path g a1 xs a2 →
path g a1 ys a2' →
∃ zs, xs = ys ++ zs.
Lemma undo_preserves_model g (M:map_model) (xs ys:list (location× (location×val)*location)) rs σ0 r:
dom M = vertices g ∪ {[r]} →
correct_path_diff M g →
(∀ x l', ¬ (rs,x,l') ∈ (list_to_set ys ∪ g ∖ list_to_set xs)) →
unaliased (g ∖ list_to_set xs ∪ list_to_set ys) →
path g rs xs r →
undo xs ys σ0 →
M !! r = Some σ0 →
correct_path_diff M (list_to_set ys ∪ g ∖ list_to_set xs).
Lemma use_snapshots_model γ (t0:location) M r σ :
meta t0 nroot γ -∗
snapshosts_model t0 M -∗
pstore_1_map_elem γ r σ -∗
⌜∃ σ1, M !! r = Some σ1 ∧ σ ⊆ σ1⌝.
Lemma pstore_1٠restore𑁒spec t σ s σ' :
{{{
pstore_1 t σ ∗
pstore_1_snapshot t s σ'
}}}
pstore_1٠restore t s
{{{
RET ();
pstore_1 t σ'
}}}.
End pstore_1_G.
From zoo_persistent Require
pstore_1__opaque.
#[global] Opaque pstore_1.
#[global] Opaque pstore_1_snapshot.
prelude.
From zoo.iris.base_logic Require Import
lib.mono_gset.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
assert
list.
From zoo_persistent Require Export
base
pstore_1__code.
From zoo_persistent Require Import
pstore_1__types.
From zoo Require Import
options.
Implicit Types l : location.
Implicit Types v t s : val.
Implicit Types σ : gmap location val.
Section map.
Context `{Countable K}.
Context {V : Type}.
Lemma gmap_included_insert (σ1 σ2:gmap K V) (l:K) (v:V) :
σ1 ⊆ σ2 →
<[l:=v]>σ1 ⊆ <[l:=v]>σ2.
Lemma gmap_included_insert_notin (σ1 σ2:gmap K V) (l:K) (v:V) :
l ∉ dom σ1 →
σ1 ⊆ σ2 →
σ1 ⊆ <[l:=v]>σ2.
Lemma incl_dom_incl (σ1 σ2:gmap K V) :
σ1 ⊆ σ2 →
dom σ1 ⊆ dom σ2.
End map.
Section list.
Context {A : Type}.
Lemma list_case_r (l:list A) :
l = nil ∨ ∃ (l':list A) x, l = l' ++ [x].
Lemma elem_of_middle (x:A) (xs:list A) :
x ∈ xs →
∃ (l1 l2:list A), xs = l1 ++ x::l2.
End list.
Section graph.
Definition graph (A B : Type) `{Countable A} `{Countable B} :=
gset (A × B × A).
Context `{Countable A} `{Countable B}.
Definition vertices (g:graph A B) : gset A :=
set_fold (fun '(x,_,y) acc ⇒ {[x;y]} ∪ acc) ∅ g.
Lemma vertices_empty :
vertices ∅ = ∅.
Definition proj1 {A B C:Type} (x:(A×B×C)) : A :=
match x with (x,_,_) ⇒ x end.
Definition proj2 {A B C:Type} (x:(A×B×C)) : B :=
match x with (_,x,_) ⇒ x end.
Definition proj3 {A B C:Type} (x:(A×B×C)) : C :=
match x with (_,_,x) ⇒ x end.
Lemma elem_of_vertices x (g:graph A B) :
x ∈ vertices g ↔ ∃ b y, ((x,b,y) ∈ g ∨ (y,b,x) ∈ g).
Lemma vertices_singleton (x:(A×B×A)) :
vertices {[x]} = {[proj1 x; proj3 x]}.
Lemma vertices_union (g1 g2:graph A B) :
vertices (g1 ∪ g2) = vertices g1 ∪ vertices g2.
Definition edge (g:graph A B) x c y :=
(x,c,y) ∈ g.
Inductive path (g:graph A B) : A → list (A×B×A) → A → Prop :=
| path_nil a :
path g a [] a
| path_cons a1 b a2 bs a3 :
(a1,b,a2) ∈ g →
path g a2 bs a3 →
path g a1 ((a1,b,a2)::bs) a3.
Lemma path_app_inv g a1 a2 xs ys :
path g a1 (xs ++ ys) a2 →
∃ a, path g a1 xs a ∧ path g a ys a2.
Lemma path_snoc_inv g a1 a2 a3 a4 b xs :
path g a1 (xs ++ [(a2,b,a3)]) a4 →
path g a1 xs a2 ∧ a3 = a4 ∧ (a2,b,a3) ∈ g.
Definition acyclic g := ∀ a xs, path g a xs a → xs = nil.
Record rooted_dag g (r:A) :=
{ ti1 : ∀ a, a ∈ vertices g → ∃ xs, path g a xs r
; ti2 : acyclic g
}.
Definition unaliased (g:graph A B) :=
∀ r x1 r1 x2 r2,
(r,x1,r1) ∈ g →
(r,x2,r2) ∈ g →
x1 = x2 ∧ r1 = r2.
Lemma path_app (g:graph A B) x3 x1 xs ys x2 :
path g x1 xs x3 →
path g x3 ys x2 →
path g x1 (xs++ys) x2.
Definition all_uniq_path g :=
∀ a1 a2 xs ys, path g a1 xs a2 → path g a1 ys a2 → xs = ys.
Lemma rooted_tree_impl_acyclic_unaliased g r :
(∀ a, a ∈ vertices g → ∃ xs, path g a xs r) →
all_uniq_path g →
acyclic g ∧ unaliased g. Lemma acyclic_unaliased_impl_uniq_path g :
acyclic g →
unaliased g →
all_uniq_path g.
Lemma rooted_dag_empty (r:A) :
rooted_dag (∅ : graph A B) r.
Lemma path_cycle_end_inv_aux g (r r':A) b ds x1 x2 :
r ≠ r' →
x2 ≠ r' →
r' ∉ vertices g →
path ({[(r, b, r')]} ∪ g) x1 ds x2 →
path g x1 ds x2.
Lemma path_cycle_end_inv g (r r':A) b ds x :
r ≠ r' →
r' ∉ vertices g →
path ({[(r, b, r')]} ∪ g) x ds x →
path g x ds x.
Lemma path_snoc g a1 b a2 bs a3 :
path g a1 bs a2 →
(a2,b,a3) ∈ g →
path g a1 (bs++[(a2,b,a3)]) a3.
Lemma path_weak g1 g2 x bs y :
path g1 x bs y →
g1 ⊆ g2 →
path g2 x bs y.
Lemma rooted_dag_add (r r':A) g x:
r ≠ r' →
r' ∉ vertices g →
rooted_dag g r →
rooted_dag ({[(r, x, r')]} ∪ g) r'.
Lemma acyclic_weak (g1 g2:graph A B) :
acyclic g1 →
g2 ⊆ g1 →
acyclic g2.
Lemma path_all_in (g:graph A B) a1 xs a2 :
path g a1 xs a2 →
list_to_set xs ⊆ g.
Lemma path_restrict (g:graph A B) r xs r' :
path g r xs r' →
path (list_to_set xs) r xs r'.
Lemma path_inv_r (g:graph A B) x bs z :
path g x bs z →
(x = z ∧ bs = nil) ∨ ∃ bs' b y, bs = bs' ++ [(y,b,z)] ∧ path g x bs' y ∧ (y,b,z) ∈ g.
Lemma path_add_inv_r (r r':A) b x xs g :
r ≠ r' →
r' ∉ vertices g →
path ({[(r, b, r')]} ∪ g) x xs r' →
(xs = nil ∧ x = r') ∨ (∃ xs', xs = xs' ++ [(r, b, r')] ∧ path g x xs' r).
Inductive mirror : list (A×B×A) → list (A×B×A) → Prop :=
| mirror_nil :
mirror [] []
| mirror_cons r x x' r' xs ys :
mirror xs ys →
mirror (xs++[(r,x,r')]) ((r',x',r)::ys).
Lemma mirror_snoc ys xs a a' x x' :
mirror ys xs →
mirror ((a,x,a') :: ys) (xs ++ [(a',x',a)]).
Lemma mirror_symm xs ys :
mirror xs ys → mirror ys xs.
Lemma use_mirror xs ys (g:graph A B) r y :
mirror xs ys →
path g r xs y →
path (list_to_set ys) y ys r.
Lemma mirror_vertices (xs ys:list (A×B×A)) :
mirror xs ys →
vertices (list_to_set ys) = vertices (list_to_set xs).
Lemma mirror_same_length (xs ys:list (A×B×A)):
mirror xs ys →
length xs = length ys.
Lemma mirror_mirrored_edges xs ys r x r' :
mirror xs ys →
(r,x,r') ∈ xs → ∃ x', (r',x',r) ∈ ys.
Lemma path_middle (g:graph A B) x xs ys z :
path g x (xs ++ ys) z →
∃ y, path g x xs y ∧ path g y ys z.
Lemma use_mirror_subset xs ys xs' g r y :
xs' ⊆ xs →
mirror xs ys →
path g r xs' y →
∃ zs, path (list_to_set ys) y zs r ∧ length xs' = length zs.
Definition pathlike (ys:list (A×B×A)) r :=
∀ a b a', (a,b,a') ∈ ys → a' = r ∨ ∃ b' a'', (a',b',a'') ∈ ys.
Lemma path_pathlike g r ys y :
path g y ys r →
pathlike ys r.
Lemma same_path g (xs:list (A×B×A)) a1 a2 a3 a4 :
path g a1 xs a2 →
path g a3 xs a4 →
xs ≠ nil →
a1 = a3 ∧ a2=a4.
Lemma path_ends_vertices g x1 xs x2 :
path g x1 xs x2 →
(x1 = x2) ∨ (x1 ∈ vertices g ∧ x2 ∈ vertices g).
End graph.
Section adiffl.
Notation diff := (
location×val
)%type.
Definition apply_diffl (ds:list diff) (σ:gmap location val) : gmap location val :=
foldr (fun '(l,v) σ ⇒ <[l:=v]> σ) σ ds.
Lemma dom_apply_diffl ds σ :
dom (apply_diffl ds σ) = dom σ ∪ (list_to_set ds.*1).
Lemma apply_diffl_insert_ne ds l v σ :
l ∉ ds.*1 →
apply_diffl ds (<[l:=v]> σ) = <[l:=v]> (apply_diffl ds σ).
Lemma apply_diffl_app ds ds' σ :
apply_diffl (ds++ds') σ = apply_diffl ds (apply_diffl ds' σ).
Lemma apply_diffl_snoc xs l v σ :
apply_diffl (xs ++ [(l,v)]) σ = apply_diffl xs (<[l:=v]> σ).
Lemma apply_diffl_cons l v xs σ :
apply_diffl ((l,v)::xs) σ = <[l:=v]> (apply_diffl xs σ).
Lemma apply_diffl_included xs σ1 σ2 :
σ1 ⊆ σ2 →
apply_diffl xs σ1 ⊆ apply_diffl xs σ2.
End adiffl.
Class Pstore1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] pstore_1_G_set_G :: MonoGsetG Σ (location × gmap location val)%type
}.
Definition pstore_1_Σ :=
#[mono_gset_Σ (location × gmap location val)%type
].
#[global] Instance subG_pstore_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG pstore_1_Σ Σ →
Pstore1G Σ.
Section pstore_1_G.
Context `{pstore_1_G : Pstore1G Σ}.
Notation diff := (
location×val
)%type.
Notation graph_store := (
graph location diff
).
Notation map_model := (
gmap location (gmap location val)
).
Definition correct_path_diff (M:map_model) (g:graph_store) :=
∀ r1 ds r2 σ1 σ2,
path g r1 ds r2 → M !! r1 = Some σ1 → M !! r2 = Some σ2 →
σ1 = (apply_diffl (proj2 <$> ds) σ2).
Record store_inv (M:map_model) (g:graph_store) (r:location) (σ σ0:gmap location val) :=
{ si1 : dom M = vertices g ∪ {[r]}
; si2 : σ ⊆ σ0
; si3 : M !! r = Some σ0
; si4 : correct_path_diff M g
}.
Definition locations_of_edges_in g (X:gset location) :=
∀ (r:location) l v r', edge g r (l,v) r' → l ∈ X.
Record coherent (M:map_model) (σ0:gmap location val) (g:graph_store) :=
{ coh1 : ∀ r σ, M !! r = Some σ → dom σ = dom σ0
; coh2 : locations_of_edges_in g (dom σ0)
}.
Definition snapshot_inv (M:map_model) (C:gset (location × gmap location val)) :=
∀ l σ, (l,σ) ∈ C → ∃ σ', M !! l = Some σ' ∧ σ ⊆ σ'.
#[local] Definition pstore_1_map_auth (γ:gname) (s:gset (location*(gmap location val))) :=
mono_gset_auth γ (DfracOwn 1) s.
#[local] Definition pstore_1_map_elem γ l σ :=
mono_gset_elem γ (l,σ).
Lemma extract_unaliased (g : graph_store) :
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) -∗
⌜unaliased g⌝.
#[local] Definition snapshosts_model (t0:location) (M:map_model) : iProp Σ :=
∃ (γ:gname) (C:gset (location × gmap location val)),
⌜snapshot_inv M C⌝ ∗ meta t0 nroot γ ∗ pstore_1_map_auth γ C.
#[local] Definition pstore_1 (t:val) (σ:gmap location val) : iProp Σ :=
∃ (t0 r:location)
(σ0:gmap location val)
(g:graph_store)
(M:map_model),
⌜t=#t0 ∧ store_inv M g r σ σ0 ∧ coherent M σ0 g ∧ rooted_dag g r⌝ ∗
t0 ↦ᵣ #r ∗
r ↦ᵣ §Root ∗
snapshosts_model t0 M ∗
([∗ map] l ↦ v ∈ σ0, l ↦ᵣ v) ∗
([∗ set] x ∈ g, let '(r,(l,v),r') := x in r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) .
Definition open_inv : string :=
"[%t0 [%r [%σ0 [%g [%M ((->&%Hinv&%Hcoh&%Hgraph)&Ht0&Hr&HC&Hσ0&Hg)]]]]]".
Definition pstore_1_snapshot t s σ : iProp Σ :=
∃ γ (t0:location) l, ⌜t=#t0 ∧ s=ValTuple [t;#l]⌝ ∗ meta t0 nroot γ ∗ pstore_1_map_elem γ l σ.
#[global] Instance pstore_1_snapshot_timeless t s σ :
Timeless (pstore_1_snapshot t s σ).
#[global] Instance pstore_1_snapshot_persistent t s σ :
Persistent (pstore_1_snapshot t s σ).
Lemma pstore_1٠create𑁒spec :
{{{
True
}}}
pstore_1٠create ()
{{{
t
, RET t;
pstore_1 t ∅
}}}.
Lemma use_locations_of_edges_in g r xs r' X :
locations_of_edges_in g X →
path g r xs r' →
(list_to_set (proj2 <$> xs).*1) ⊆ X.
Lemma pstore_1٠ref𑁒spec t σ v :
{{{
pstore_1 t σ
}}}
pstore_1٠ref t v
{{{
l
, RET #l;
⌜l ∉ dom σ⌝ ∗
pstore_1 t (<[l := v]> σ)
}}}.
Lemma pstore_1٠get𑁒spec {t σ l} v :
σ !! l = Some v →
{{{
pstore_1 t σ
}}}
pstore_1٠get t #l
{{{
RET v;
pstore_1 t σ
}}}.
Lemma pstore_1٠set𑁒spec t σ l v :
l ∈ dom σ →
{{{
pstore_1 t σ
}}}
pstore_1٠set t #l v
{{{
RET ();
pstore_1 t (<[l := v]> σ)
}}}.
Lemma pstore_1٠capture𑁒spec t σ :
{{{
pstore_1 t σ
}}}
pstore_1٠capture t
{{{
s
, RET s;
pstore_1 t σ ∗
pstore_1_snapshot t s σ
}}}.
Definition fsts (ys:list (location*(location×val)*location)) : list val :=
(fun '(x,_,_) ⇒ ValLoc x) <$> ys.
Lemma pstore_1٠collect𑁒spec_aux (r r':location) t' (xs:list val) (ys:list (location*(location×val)*location)) (g:graph_store) :
list_model' t' xs →
path g r ys r' →
{{{
r' ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) ))
}}}
pstore_1٠collect #r t'
{{{
t
, RET (#r',t);
r' ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
list_model t (rev_append (fsts ys) xs)
}}}.
Lemma pstore_1٠collect𑁒spec (r r':location) (ys:list (location*(location×val)*location)) (g:graph_store) :
path g r ys r' →
{{{
r' ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) ))
}}}
pstore_1٠collect #r []
{{{
t
, RET (#r',t);
r' ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
list_model t (rev (fsts ys))
}}}.
Lemma use_path r g (xs:list (location*(location×val)*location)) r0 x r1 r':
list_to_set xs ⊆ g →
path g r (xs ++ [(r0, x, r1)]) r' →
(r0, x, r1) ∈ (list_to_set xs : gset(location*(location×val)*location) ) →
∃ ds, path g r0 ds r0 ∧ ds ≠ nil.
Inductive undo : list (location*(location×val)*location) → list (location*(location×val)*location) → gmap location val → Prop :=
| undo_nil :
∀ σ, undo [] [] σ
| undo_cons σ r l v v' r' xs ys :
σ !! l = Some v' →
undo xs ys (<[l:=v]> σ) →
undo (xs++[(r,(l,v),r')]) ((r',(l,v'),r)::ys) σ.
Lemma use_undo xs ys σ :
undo xs ys σ →
σ = apply_diffl (proj2 <$> ys ++ xs) σ.
Lemma undo_mirror xs ys g :
undo xs ys g →
mirror xs ys.
Lemma pstore_1٠revert𑁒spec_aux g g1 r t g2 xs r' w σ σ0 :
list_model' t (fsts (rev xs)) →
locations_of_edges_in g2 (dom σ) →
g2 = list_to_set xs →
acyclic g →
g2 ⊆ g →
path g r xs r' →
{{{
r' ↦ᵣ w ∗
([∗ map] l0↦v0 ∈ σ, l0 ↦ᵣ v0) ∗
([∗ set] '(r, (l, v), r') ∈ g1, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
([∗ set] '(r, (l, v), r') ∈ g2, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) ))
}}}
pstore_1٠revert #r' t
{{{
RET ();
∃ ys,
⌜undo xs ys σ⌝ ∗
r ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ (g1 ∪ list_to_set ys), r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
([∗ map] l0↦v0 ∈ (apply_diffl (proj2 <$> xs) σ), l0 ↦ᵣ v0)
}}}.
Lemma pstore_1٠revert𑁒spec r t g xs r' w σ σ0 :
list_model' t (fsts (rev xs)) →
locations_of_edges_in g (dom σ) →
g = list_to_set xs →
acyclic g →
path g r xs r' →
{{{
r' ↦ᵣ w ∗
([∗ map] l0↦v0 ∈ σ, l0 ↦ᵣ v0) ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) ))
}}}
pstore_1٠revert #r' t
{{{
RET ();
∃ ys,
⌜undo xs ys σ⌝ ∗
r ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ (list_to_set ys), r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
([∗ map] l0↦v0 ∈ (apply_diffl (proj2 <$> xs) σ), l0 ↦ᵣ v0)
}}}.
Lemma rev_fsts xs :
rev (fsts xs) = fsts (rev xs).
Lemma pstore_1٠reroot𑁒spec r (xs:list (location*(location×val)*location)) r' g σ :
locations_of_edges_in g (dom σ) →
g = list_to_set xs →
acyclic g →
path g r xs r' →
{{{
r' ↦ᵣ §Root ∗
([∗ map] l0↦v0 ∈ σ, l0 ↦ᵣ v0) ∗
([∗ set] '(r, (l, v), r') ∈ g, r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) ))
}}}
pstore_1٠reroot #r
{{{
RET ();
∃ ys,
⌜undo xs ys σ⌝ ∗
r ↦ᵣ §Root ∗
([∗ set] '(r, (l, v), r') ∈ (list_to_set ys), r ↦ᵣ ‘Diff( #(l : location), v, #(r' : location) )) ∗
([∗ map] l0↦v0 ∈ (apply_diffl (proj2 <$> xs) σ), l0 ↦ᵣ v0)
}}}.
Lemma locations_of_edges_weak g1 g2 X :
locations_of_edges_in g1 X →
g2 ⊆ g1 →
locations_of_edges_in g2 X.
Lemma undo_same_fst_label xs ys r l v r' σ :
undo xs ys σ →
(r, (l, v), r') ∈ (list_to_set ys : gset (location*(location×val)*location)) →
l ∈ (list_to_set (proj2 <$> xs).*1 : gset location).
Definition diff_last {A:Type} (ys1 ys2:list A) :=
match last ys1, last ys2 with
| Some x, Some y ⇒
x ≠ y
| _, _ ⇒
True
end.
Lemma path_extract_suffix (g:gset (location*(location×val)*location)) a1 a2 xs1 r xs2 :
unaliased g →
path g a1 xs1 r →
path g a2 xs2 r →
∃ ys1 ys2 xs,
xs1 = ys1 ++ xs ∧
xs2 = ys2 ++ xs ∧ diff_last ys1 ys2.
Lemma diff_last_app_middle {A:Type} x (l1' l2' l1 l2:list A) :
diff_last (l1' ++ x :: l2') (l1 ++ x :: l2) →
diff_last (x :: l2') (x :: l2).
Lemma diff_last_irrefl {A:Type} (l:list A) :
l ≠ nil →
¬ (diff_last l l).
Lemma path_use_diff_last (g:gset (location*(location×val)*location)) a1 a2 ys1 ys2 xs r :
acyclic g →
unaliased g →
path g a1 (ys1 ++ xs) r →
path g a2 (ys2 ++ xs) r →
diff_last ys1 ys2 →
∀ x, x ∈ ys2 → x ∉ (ys1 ++ xs).
Lemma diff_last_comm {A:Type} (l1 l2:list A) :
diff_last l1 l2 ↔ diff_last l2 l1.
Lemma path_union_inv (g1: graph location (location×val)) g2 a1 xs a2 :
path (g1 ∪ g2) a1 xs a2 →
path g1 a1 xs a2 ∨ ∃ a' x xs1 xs2, path g1 a1 xs1 a' ∧ x ∈ g2 ∧ path (g1 ∪ g2) a' (x::xs2) a2 ∧ xs=xs1++x::xs2.
Lemma path_cannot_escape (x:(location × diff × location)) (xs ys:list (location × diff × location)) (g1: graph location (location×val)) a a' r :
(∀ x l', ¬ (r,x,l') ∈ (g1 ∪ list_to_set ys)) →
unaliased (g1 ∪ list_to_set ys) →
x ∈ (list_to_set ys : gset _) →
pathlike ys r →
path (g1 ∪ list_to_set ys) a (x :: xs) a' →
path (list_to_set ys) a (x::xs) a'.
Lemma path_in_seg_complete (r a a':location) (x:(location × diff × location)) (xs0 xs1 ys: list (location × diff × location)) (g1:graph location (location×val)) :
(∀ x l', ¬ (r,x,l') ∈ (g1 ∪ list_to_set ys)) →
unaliased (g1 ∪ list_to_set ys) →
pathlike ys r →
path (g1 ∪ list_to_set ys) a xs0 a' →
path (list_to_set ys) a' (x :: xs1) a →
∃ zs, path (list_to_set ys) a zs a'.
Lemma undo_preserves_rooted_dag (g:graph location (location×val)) xs ys rs r :
(∀ x l', ¬ (rs,x,l') ∈ (list_to_set ys ∪ g ∖ list_to_set xs)) →
unaliased g →
unaliased (list_to_set ys ∪ g ∖ list_to_set xs) →
path g rs xs r →
mirror xs ys →
rooted_dag g r →
rooted_dag (list_to_set ys ∪ g ∖ list_to_set xs) rs.
Lemma undo_app_inv xs ys1 ys2 σ :
undo xs (ys1 ++ ys2) σ →
∃ xs1 xs2, xs = xs2 ++ xs1 ∧ undo xs2 ys2 (apply_diffl (proj2 <$> xs1) σ) ∧ undo xs1 ys1 σ.
Lemma construct_middlepoint (g:graph location (location×val)) a1 xs ys a2 a2' :
unaliased g →
(∀ x l', ¬ (a2,x,l') ∈ g) →
path g a1 xs a2 →
path g a1 ys a2' →
∃ zs, xs = ys ++ zs.
Lemma undo_preserves_model g (M:map_model) (xs ys:list (location× (location×val)*location)) rs σ0 r:
dom M = vertices g ∪ {[r]} →
correct_path_diff M g →
(∀ x l', ¬ (rs,x,l') ∈ (list_to_set ys ∪ g ∖ list_to_set xs)) →
unaliased (g ∖ list_to_set xs ∪ list_to_set ys) →
path g rs xs r →
undo xs ys σ0 →
M !! r = Some σ0 →
correct_path_diff M (list_to_set ys ∪ g ∖ list_to_set xs).
Lemma use_snapshots_model γ (t0:location) M r σ :
meta t0 nroot γ -∗
snapshosts_model t0 M -∗
pstore_1_map_elem γ r σ -∗
⌜∃ σ1, M !! r = Some σ1 ∧ σ ⊆ σ1⌝.
Lemma pstore_1٠restore𑁒spec t σ s σ' :
{{{
pstore_1 t σ ∗
pstore_1_snapshot t s σ'
}}}
pstore_1٠restore t s
{{{
RET ();
pstore_1 t σ'
}}}.
End pstore_1_G.
From zoo_persistent Require
pstore_1__opaque.
#[global] Opaque pstore_1.
#[global] Opaque pstore_1_snapshot.