Library zoo_persistent.pstore_2
From iris.base_logic Require Import
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
fin_maps
list
treemap.
From zoo.iris.base_logic Require Import
lib.mono_gmap.
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_2__code.
From zoo_persistent Require Import
pstore_2__types.
From zoo Require Import
options.
Implicit Types l r node cnode base root dst : location.
Implicit Types nodes : list location.
Implicit Types v t s : val.
Implicit Types σ σ₀ : gmap location val.
Module base.
#[local] Definition generation :=
nat.
Implicit Types g : generation.
#[local] Notation "data '.(gen)'" := (
fst data
)(at level 2,
left associativity,
format "data .(gen)"
) : stdpp_scope.
#[local] Notation "data '.(val)'" := (
snd data
)(at level 2,
left associativity,
format "data .(val)"
) : stdpp_scope.
#[local] Definition store :=
gmap location (generation × val).
Implicit Types ς : store.
Implicit Types data : generation × val.
Record descriptor := Descriptor
{ descriptor_gen : generation
; descriptor_store : store
}.
Add Printing Constructor descriptor.
Implicit Types descr : descriptor.
Implicit Types cnodes : gmap location descriptor.
Class Pstore2G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] pstore_2_G_nodes_G :: ghost_mapG Σ location descriptor
}.
Definition pstore_2_Σ :=
#[ghost_mapΣ location descriptor
].
#[global] Instance subG_pstore_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG pstore_2_Σ Σ →
Pstore2G Σ.
Section pstore_2_G.
Context `{pstore_2_G : Pstore2G Σ}.
#[local] Definition metadata :=
gname.
Implicit Types γ : metadata.
#[local] Definition store_on σ₀ ς :=
ς ∪ (pair 0 <$> σ₀).
#[local] Definition store_generation g ς :=
map_Forall (λ r data, data.(gen) ≤ g) ς.
#[local] Definition descriptor_wf σ₀ descr :=
dom descr.(descriptor_store) ⊆ dom σ₀ ∧
store_generation descr.(descriptor_gen) descr.(descriptor_store).
Record delta := Delta
{ delta_ref : location
; delta_gen : generation
; delta_val : val
; delta_node : location
}.
Add Printing Constructor delta.
Implicit Types δ : delta.
Implicit Types δs : list delta.
Implicit Types path : list (list delta).
#[local] Notation "δ '.(delta_data)'" := (
pair δ.(delta_gen) δ.(delta_val)
)(at level 2,
left associativity,
format "δ .(delta_data)"
) : stdpp_scope.
#[local] Definition delta_patch δ :=
(δ.(delta_ref), δ.(delta_data)).
#[local] Definition deltas_apply δs ς :=
list_to_map (delta_patch <$> δs) ∪ ς.
#[local] Fixpoint deltas_chain node δs dst : iProp Σ :=
match δs with
| [] ⇒
⌜node = dst⌝
| δ :: δs ⇒
node ↦ᵣ ‘Diff( #δ.(delta_ref), #δ.(delta_gen), δ.(delta_val), #δ.(delta_node) ) ∗
deltas_chain δ.(delta_node) δs dst
end.
#[local] Definition edge : Set :=
location × list delta.
Implicit Types ϵ : edge.
Implicit Types ϵs : gmap location edge.
#[local] Definition cnodes_auth γ cnodes :=
ghost_map_auth γ 1 cnodes.
#[local] Definition cnodes_elem γ cnode descr :=
ghost_map_elem γ cnode DfracDiscarded descr.
#[local] Definition cnode_model γ σ₀ cnode descr ϵ ς : iProp Σ :=
let cnode' := ϵ.1 in
let δs := ϵ.2 in
⌜descriptor_wf σ₀ descr⌝ ∗
cnodes_elem γ cnode descr ∗
⌜NoDup $ delta_ref <$> δs⌝ ∗
⌜store_on σ₀ descr.(descriptor_store) = store_on σ₀ $ deltas_apply δs ς⌝ ∗
deltas_chain cnode δs cnode'.
Definition pstore_2_model t σ₀ σ : iProp Σ :=
∃ l γ g root ς,
⌜t = #l⌝ ∗
⌜σ = snd <$> ς⌝ ∗
meta l (nroot.@"impl") γ ∗
l.[gen] ↦ #g ∗
l.[root] ↦ #root ∗
root ↦ᵣ §Root ∗
( [∗ map] r ↦ data ∈ store_on σ₀ ς,
r.[ref_gen] ↦ #data.(gen) ∗
r.[ref_value] ↦ data.(val)
) ∗
⌜descriptor_wf σ₀ (Descriptor g ς)⌝ ∗
if decide (g = 0) then
cnodes_auth γ ∅
else
∃ cnodes ϵs base descr δs,
⌜treemap_rooted ϵs base⌝ ∗
cnodes_auth γ cnodes ∗
⌜cnodes !! base = Some descr⌝ ∗
⌜descr.(descriptor_gen) < g⌝ ∗
cnode_model γ σ₀ base descr (root, δs) ς ∗
⌜δs = [] → ς = descr.(descriptor_store)⌝ ∗
⌜Forall (λ δ, ∃ data, ς !! δ.(delta_ref) = Some data ∧ data.(gen) = g) δs⌝ ∗
[∗ map] cnode ↦ descr; ϵ ∈ delete base cnodes; ϵs,
∃ descr',
⌜cnodes !! ϵ.1 = Some descr'⌝ ∗
cnode_model γ σ₀ cnode descr ϵ descr'.(descriptor_store).
Definition pstore_2_snapshot s t σ : iProp Σ :=
∃ l γ g cnode descr,
⌜t = #l⌝ ∗
⌜s = (t, #g, #cnode)%V⌝ ∗
⌜σ = snd <$> descr.(descriptor_store)⌝ ∗
⌜descr.(descriptor_gen) ≤ g⌝ ∗
meta l (nroot.@"impl") γ ∗
cnodes_elem γ cnode descr.
#[local] Instance deltas_chain_timeless node δs dst :
Timeless (deltas_chain node δs dst).
#[global] Instance pstore_2_model_timeless t σ₀ σ :
Timeless (pstore_2_model t σ₀ σ).
#[global] Instance pstore_2_snapshot_persistent s t σ :
Persistent (pstore_2_snapshot s t σ).
#[local] Lemma store_on_dom σ₀ ς :
dom (store_on σ₀ ς) = dom σ₀ ∪ dom ς.
#[local] Lemma store_on_dom' σ₀ ς :
dom ς ⊆ dom σ₀ →
dom (store_on σ₀ ς) = dom σ₀.
#[local] Lemma store_on_lookup {σ₀ ς} r data :
store_on σ₀ ς !! r = Some data ↔
ς !! r = Some data
∨ ς !! r = None ∧
data.(gen) = 0 ∧
σ₀ !! r = Some data.(val).
#[local] Lemma store_on_lookup' {σ₀ ς} r data :
ς !! r = Some data →
store_on σ₀ ς !! r = Some data.
#[local] Lemma store_on_insert r data σ₀ ς :
store_on σ₀ (<[r := data]> ς) = <[r := data]> (store_on σ₀ ς).
#[local] Lemma store_on_insert_support r v σ₀ ς :
σ₀ !! r = None →
dom ς ⊆ dom σ₀ →
store_on (<[r := v]> σ₀) ς = <[r := (0, v)]> (store_on σ₀ ς).
#[local] Lemma store_on_deltas_apply σ₀ δs ς :
store_on σ₀ (deltas_apply δs ς) = deltas_apply δs (store_on σ₀ ς).
#[local] Lemma store_generation_le {g ς} g' :
g ≤ g' →
store_generation g ς →
store_generation g' ς.
#[local] Lemma store_generation_insert g ς r data :
store_generation g ς →
data.(gen) ≤ g →
store_generation g (<[r := data]> ς).
#[local] Lemma deltas_apply_nil ς :
deltas_apply [] ς = ς.
#[local] Lemma deltas_apply_cons δ δs ς :
deltas_apply (δ :: δs) ς = <[δ.(delta_ref) := δ.(delta_data)]> (deltas_apply δs ς).
#[local] Lemma deltas_apply_singleton δ ς :
deltas_apply [δ] ς = <[δ.(delta_ref) := δ.(delta_data)]> ς.
#[local] Lemma deltas_apply_app δs1 δs2 ς :
deltas_apply (δs1 ++ δs2) ς = deltas_apply δs1 (deltas_apply δs2 ς).
#[local] Lemma deltas_apply_snoc δs δ ς :
deltas_apply (δs ++ [δ]) ς = deltas_apply δs (<[δ.(delta_ref) := δ.(delta_data)]> ς).
#[local] Lemma deltas_apply_snoc' δs r g v node ς :
deltas_apply (δs ++ [Delta r g v node]) ς = deltas_apply δs (<[r := (g, v)]> ς).
#[local] Lemma deltas_apply_dom δs ς :
dom (deltas_apply δs ς) = list_to_set (delta_ref <$> δs) ∪ dom ς.
#[local] Lemma deltas_apply_lookup δs δ r data ς :
NoDup (delta_ref <$> δs) →
δ ∈ δs →
r = δ.(delta_ref) →
data = δ.(delta_data) →
deltas_apply δs ς !! r = Some data.
#[local] Lemma deltas_apply_lookup' δs r data ς :
NoDup (delta_ref <$> δs) →
(r, data) ∈ delta_patch <$> δs →
deltas_apply δs ς !! r = Some data.
#[local] Lemma deltas_apply_lookup_ne r δs ς :
NoDup (delta_ref <$> δs) →
r ∉ (delta_ref <$> δs) →
deltas_apply δs ς !! r = ς !! r.
#[local] Lemma deltas_apply_permutation δs1 δs2 ς :
NoDup (delta_ref <$> δs1) →
δs1 ≡ₚ δs2 →
deltas_apply δs1 ς = deltas_apply δs2 ς.
#[local] Lemma deltas_chain_cons src δ δs dst :
src ↦ᵣ ‘Diff( #δ.(delta_ref), #δ.(delta_gen), δ.(delta_val), #δ.(delta_node) ) -∗
deltas_chain δ.(delta_node) δs dst -∗
deltas_chain src (δ :: δs) dst.
#[local] Lemma deltas_chain_nil_inv src dst :
deltas_chain src [] dst ⊢
⌜src = dst⌝.
#[local] Lemma deltas_chain_cons_inv src δ δs dst :
deltas_chain src (δ :: δs) dst ⊢
src ↦ᵣ ‘Diff( #δ.(delta_ref), #δ.(delta_gen), δ.(delta_val), #δ.(delta_node) ) ∗
deltas_chain δ.(delta_node) δs dst.
#[local] Lemma deltas_chain_snoc {src δs dst} r g v dst' :
deltas_chain src δs dst -∗
dst ↦ᵣ ‘Diff( #r, #g, v, #dst' ) -∗
deltas_chain src (δs ++ [Delta r g v dst']) dst'.
#[local] Lemma deltas_chain_app_1 src δs1 δs2 dst :
deltas_chain src (δs1 ++ δs2) dst ⊢
let node := default src $ delta_node <$> last δs1 in
deltas_chain src δs1 node ∗
deltas_chain node δs2 dst.
#[local] Lemma deltas_chain_app_2 src δs1 node δs2 dst :
deltas_chain src δs1 node -∗
deltas_chain node δs2 dst -∗
deltas_chain src (δs1 ++ δs2) dst.
#[local] Lemma deltas_chain_snoc_inv src δs δ dst :
deltas_chain src (δs ++ [δ]) dst ⊢
let node := default src $ delta_node <$> last δs in
⌜δ.(delta_node) = dst⌝ ∗
deltas_chain src δs node ∗
node ↦ᵣ ‘Diff( #δ.(delta_ref), #δ.(delta_gen), δ.(delta_val), #dst ).
#[local] Lemma deltas_chain_lookup {src δs dst} i δ :
δs !! i = Some δ →
deltas_chain src δs dst ⊢
deltas_chain src (take (S i) δs) δ.(delta_node) ∗
deltas_chain δ.(delta_node) (drop (S i) δs) dst.
#[local] Lemma deltas_chain_lookup' {src δs dst} i δ :
δs !! i = Some δ →
deltas_chain src δs dst ⊢
∃ node,
⌜ if i is 0 then
node = src
else
∃ δ',
δs !! pred i = Some δ' ∧
δ'.(delta_node) = node
⌝ ∗
deltas_chain src (take i δs) node ∗
node ↦ᵣ ‘Diff( #δ.(delta_ref), #δ.(delta_gen), δ.(delta_val), #δ.(delta_node) ) ∗
deltas_chain δ.(delta_node) (drop (S i) δs) dst.
#[local] Definition cnodes_alloc root :
⊢ |==>
∃ γ,
cnodes_auth γ ∅.
#[local] Definition cnodes_lookup γ cnodes cnode descr :
cnodes_auth γ cnodes -∗
cnodes_elem γ cnode descr -∗
⌜cnodes !! cnode = Some descr⌝.
#[local] Lemma cnodes_insert {γ cnodes} cnode descr :
cnodes !! cnode = None →
cnodes_auth γ cnodes ⊢ |==>
cnodes_auth γ (<[cnode := descr]> cnodes) ∗
cnodes_elem γ cnode descr.
Lemma pstore_2_model_valid t σ₀ σ :
pstore_2_model t σ₀ σ ⊢
⌜dom σ ⊆ dom σ₀⌝.
Lemma pstore_2_model_exclusive t σ₀1 σ1 σ₀2 σ2 :
pstore_2_model t σ₀1 σ1 -∗
pstore_2_model t σ₀2 σ2 -∗
False.
Lemma pstore_2٠create𑁒spec :
{{{
True
}}}
pstore_2٠create ()
{{{
t
, RET t;
(∃ l, ⌜t = #l⌝ ∗ meta_token l (↑nroot.@"user")) ∗
pstore_2_model t ∅ ∅
}}}.
Lemma pstore_2٠ref𑁒spec t σ₀ σ v :
{{{
pstore_2_model t σ₀ σ
}}}
pstore_2٠ref t v
{{{
r
, RET #r;
⌜σ₀ !! r = None⌝ ∗
pstore_2_model t (<[r := v]> σ₀) σ
}}}.
Lemma pstore_2٠get𑁒spec {t σ₀ σ r} v :
(σ ∪ σ₀) !! r = Some v →
{{{
pstore_2_model t σ₀ σ
}}}
pstore_2٠get t #r
{{{
RET v;
pstore_2_model t σ₀ σ
}}}.
Lemma pstore_2٠set𑁒spec t σ₀ σ r v :
r ∈ dom σ₀ →
{{{
pstore_2_model t σ₀ σ
}}}
pstore_2٠set t #r v
{{{
RET ();
pstore_2_model t σ₀ (<[r := v]> σ)
}}}.
Lemma pstore_2٠capture𑁒spec t σ₀ σ :
{{{
pstore_2_model t σ₀ σ
}}}
pstore_2٠capture t
{{{
s
, RET s;
pstore_2_model t σ₀ σ ∗
pstore_2_snapshot s t σ
}}}.
#[local] Definition collect_inv γ σ₀ root ς cnodes ϵs base descr δs : iProp Σ :=
root ↦ᵣ §Root ∗
( [∗ map] r ↦ data ∈ store_on σ₀ ς,
r.[ref_gen] ↦ #data.(gen) ∗
r.[ref_value] ↦ data.(val)
) ∗
⌜treemap_rooted ϵs base⌝ ∗
cnodes_auth γ cnodes ∗
⌜cnodes !! base = Some descr⌝ ∗
cnode_model γ σ₀ base descr (root, δs) ς ∗
⌜δs = [] → ς = descr.(descriptor_store)⌝ ∗
[∗ map] cnode ↦ descr; ϵ ∈ delete base cnodes; ϵs,
∃ descr',
⌜cnodes !! ϵ.1 = Some descr'⌝ ∗
cnode_model γ σ₀ cnode descr ϵ descr'.(descriptor_store).
#[local] Lemma pstore_2٠collect𑁒spec_base_chain {γ σ₀ root ς cnodes ϵs base descr δs} i δ node acc :
δs !! i = Some δ →
δ.(delta_node) = node →
{{{
collect_inv γ σ₀ root ς cnodes ϵs base descr δs
}}}
pstore_2٠collect #node acc
{{{
acc'
, RET (#root, acc');
collect_inv γ σ₀ root ς cnodes ϵs base descr δs ∗
plist_model acc' acc $ tail $
(λ δ, #δ.(delta_node)) <$> reverse (drop i δs)
}}}.
#[local] Definition collect𑁒specification γ σ₀ root ς cnodes ϵs base descr δs : iProp Σ :=
∀ cnode descr_cnode path acc,
{{{
⌜cnodes !! cnode = Some descr_cnode⌝ ∗
⌜treemap_path ϵs base cnode path⌝ ∗
collect_inv γ σ₀ root ς cnodes ϵs base descr δs
}}}
pstore_2٠collect #cnode acc
{{{
acc'
, RET (#root, acc');
collect_inv γ σ₀ root ς cnodes ϵs base descr δs ∗
plist_model acc' acc $ tail $
((λ δ, #δ.(delta_node)) <$> reverse δs) ++
((λ δ, #δ.(delta_node)) <$> reverse (concat path)) ++
[ #cnode]
}}}.
#[local] Lemma pstore_2٠collect𑁒spec_chain {γ σ₀ root ς cnodes ϵs base descr δs} cnode ϵ i 𝝳 node path acc :
ϵs !! cnode = Some ϵ →
ϵ.2 !! i = Some 𝝳 →
𝝳.(delta_node) = node →
treemap_path ϵs base ϵ.1 path →
{{{
collect_inv γ σ₀ root ς cnodes ϵs base descr δs ∗
collect𑁒specification γ σ₀ root ς cnodes ϵs base descr δs
}}}
pstore_2٠collect #node acc
{{{
acc'
, RET (#root, acc');
collect_inv γ σ₀ root ς cnodes ϵs base descr δs ∗
plist_model acc' acc $ tail $
((λ δ, #δ.(delta_node)) <$> reverse δs) ++
((λ δ, #δ.(delta_node)) <$> reverse (concat path)) ++
((λ δ, #δ.(delta_node)) <$> reverse (drop i ϵ.2))
}}}.
#[local] Lemma pstore_2٠collect𑁒spec {γ σ₀ root ς cnodes ϵs base descr δs} cnode descr_cnode path acc :
cnodes !! cnode = Some descr_cnode →
treemap_path ϵs base cnode path →
{{{
collect_inv γ σ₀ root ς cnodes ϵs base descr δs
}}}
pstore_2٠collect #cnode acc
{{{
acc'
, RET (#root, acc');
collect_inv γ σ₀ root ς cnodes ϵs base descr δs ∗
plist_model acc' acc $ tail $
((λ δ, #δ.(delta_node)) <$> reverse δs) ++
((λ δ, #δ.(delta_node)) <$> reverse (concat path)) ++
[ #cnode]
}}}.
#[local] Definition revert_pre_1 γ σ₀ root ς cnodes ϵs base descr δs : iProp Σ :=
∃ v_root,
root ↦ᵣ v_root ∗
( [∗ map] r ↦ data ∈ store_on σ₀ ς,
r.[ref_gen] ↦ #data.(gen) ∗
r.[ref_value] ↦ data.(val)
) ∗
⌜treemap_rooted ϵs base⌝ ∗
cnodes_auth γ cnodes ∗
⌜cnodes !! base = Some descr⌝ ∗
cnode_model γ σ₀ base descr (root, δs) ς ∗
⌜δs = [] → ς = descr.(descriptor_store)⌝ ∗
[∗ map] cnode ↦ descr; ϵ ∈ delete base cnodes; ϵs,
∃ descr',
⌜cnodes !! ϵ.1 = Some descr'⌝ ∗
cnode_model γ σ₀ cnode descr ϵ descr'.(descriptor_store).
#[local] Definition revert_pre_2 γ σ₀ ς cnodes ϵs base descr_base δs_base cnode descr_cnode δs_cnode node : iProp Σ :=
∃ v_node,
node ↦ᵣ v_node ∗
( [∗ map] r ↦ data ∈ store_on σ₀ ς,
r.[ref_gen] ↦ #data.(gen) ∗
r.[ref_value] ↦ data.(val)
) ∗
⌜treemap_rooted ϵs base⌝ ∗
cnodes_auth γ cnodes ∗
⌜cnodes !! base = Some descr_base⌝ ∗
cnode_model γ σ₀ base descr_base (node, δs_base) ς ∗
⌜cnodes !! cnode = Some descr_cnode⌝ ∗
cnode_model γ σ₀ cnode descr_cnode (node, δs_cnode) ς ∗
[∗ map] cnode ↦ descr; ϵ ∈ delete base $ delete cnode cnodes; delete cnode ϵs,
∃ descr',
⌜cnodes !! ϵ.1 = Some descr'⌝ ∗
cnode_model γ σ₀ cnode descr ϵ descr'.(descriptor_store).
#[local] Definition revert_post γ σ₀ cnodes ϵs base descr : iProp Σ :=
base ↦ᵣ §Root ∗
( [∗ map] r ↦ data ∈ store_on σ₀ descr.(descriptor_store),
r.[ref_gen] ↦ #data.(gen) ∗
r.[ref_value] ↦ data.(val)
) ∗
⌜treemap_rooted ϵs base⌝ ∗
cnodes_auth γ cnodes ∗
cnode_model γ σ₀ base descr (base, []) descr.(descriptor_store) ∗
[∗ map] cnode ↦ descr; ϵ ∈ delete base cnodes; ϵs,
∃ descr',
⌜cnodes !! ϵ.1 = Some descr'⌝ ∗
cnode_model γ σ₀ cnode descr ϵ descr'.(descriptor_store).
#[local] Lemma pstore_2٠revert𑁒spec_aux {γ σ₀ ς cnodes ϵs base descr_base δs_base cnode descr_cnode δs_cnode node} base' descr_base' path δs acc :
cnodes !! base' = Some descr_base' →
treemap_path ϵs cnode base' path →
ϵs !! cnode = Some (base, δs) →
0 < length δs_cnode →
NoDup (delta_ref <$> δs_cnode ++ δs_base) →
list_model' acc $ tail $
((λ δ, #δ.(delta_node)) <$> reverse δs_cnode) ++
((λ δ, #δ.(delta_node)) <$> reverse (concat path)) ++
[ #base'] →
{{{
revert_pre_2 γ σ₀ ς cnodes ϵs base descr_base δs_base cnode descr_cnode δs_cnode node
}}}
pstore_2٠revert #node acc
{{{
ϵs
, RET ();
revert_post γ σ₀ cnodes ϵs base' descr_base'
}}}.
#[local] Lemma pstore_2٠revert𑁒spec {γ σ₀ root ς cnodes ϵs base descr_base δs} base' descr_base' path acc :
cnodes !! base' = Some descr_base' →
treemap_path ϵs base base' path →
list_model' acc $ tail $
((λ δ, #δ.(delta_node)) <$> reverse δs) ++
((λ δ, #δ.(delta_node)) <$> reverse (concat path)) ++
[ #base'] →
{{{
revert_pre_1 γ σ₀ root ς cnodes ϵs base descr_base δs
}}}
pstore_2٠revert #root acc
{{{
ϵs
, RET ();
revert_post γ σ₀ cnodes ϵs base' descr_base'
}}}.
#[local] Lemma pstore_2٠reroot𑁒spec {γ σ₀ root ς cnodes ϵs base descr δs} base' descr' path :
cnodes !! base' = Some descr' →
treemap_path ϵs base base' path →
{{{
collect_inv γ σ₀ root ς cnodes ϵs base descr δs
}}}
pstore_2٠reroot #base'
{{{
ϵs
, RET ();
revert_post γ σ₀ cnodes ϵs base' descr'
}}}.
Lemma pstore_2٠restore𑁒spec t σ₀ σ s σ' :
{{{
pstore_2_model t σ₀ σ ∗
pstore_2_snapshot s t σ'
}}}
pstore_2٠restore t s
{{{
RET ();
pstore_2_model t σ₀ σ'
}}}.
End pstore_2_G.
#[global] Opaque pstore_2_model.
#[global] Opaque pstore_2_snapshot.
End base.
From zoo_persistent Require
pstore_2__opaque.
Class Pstore2G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] pstore_2_G_raw_G :: base.Pstore2G Σ
; #[local] pstore_2_G_support_G :: MonoGmapG Σ location val
}.
Definition pstore_2_Σ :=
#[base.pstore_2_Σ
; mono_gmap_Σ location val
].
#[global] Instance subG_pstore_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG pstore_2_Σ Σ →
Pstore2G Σ.
Section pstore_2_G.
Context `{pstore_2_G : Pstore2G Σ}.
#[local] Definition metadata :=
gname.
Implicit Types γ : metadata.
Definition pstore_2_model t σ : iProp Σ :=
∃ l γ σ₀ ς,
⌜t = #l⌝ ∗
⌜σ ⊆ ς ∪ σ₀⌝ ∗
meta l (nroot.@"user") γ ∗
mono_gmap_auth γ (DfracOwn 1) σ₀ ∗
base.pstore_2_model t σ₀ ς.
Definition pstore_2_snapshot s t σ : iProp Σ :=
∃ l γ σ₀ ς,
⌜t = #l⌝ ∗
⌜σ ⊆ ς ∪ σ₀⌝ ∗
meta l (nroot.@"user") γ ∗
mono_gmap_lb γ σ₀ ∗
base.pstore_2_snapshot s t ς.
#[global] Instance pstore_2_model_timeless t σ :
Timeless (pstore_2_model t σ).
#[global] Instance pstore_2_snapshot_persistent s t σ :
Persistent (pstore_2_snapshot s t σ).
Lemma pstore_2_model_exclusive t σ1 σ2 :
pstore_2_model t σ1 -∗
pstore_2_model t σ2 -∗
False.
Lemma pstore_2٠create𑁒spec :
{{{
True
}}}
pstore_2٠create ()
{{{
t
, RET t;
pstore_2_model t ∅
}}}.
Lemma pstore_2٠ref𑁒spec t σ v :
{{{
pstore_2_model t σ
}}}
pstore_2٠ref t v
{{{
r
, RET #r;
⌜σ !! r = None⌝ ∗
pstore_2_model t (<[r := v]> σ)
}}}.
Lemma pstore_2٠get𑁒spec {t σ r} v :
σ !! r = Some v →
{{{
pstore_2_model t σ
}}}
pstore_2٠get t #r
{{{
RET v;
pstore_2_model t σ
}}}.
Lemma pstore_2٠set𑁒spec t σ r v :
r ∈ dom σ →
{{{
pstore_2_model t σ
}}}
pstore_2٠set t #r v
{{{
RET ();
pstore_2_model t (<[r := v]> σ)
}}}.
Lemma pstore_2٠capture𑁒spec t σ :
{{{
pstore_2_model t σ
}}}
pstore_2٠capture t
{{{
s
, RET s;
pstore_2_model t σ ∗
pstore_2_snapshot s t σ
}}}.
Lemma pstore_2٠restore𑁒spec t σ s σ' :
{{{
pstore_2_model t σ ∗
pstore_2_snapshot s t σ'
}}}
pstore_2٠restore t s
{{{
RET ();
pstore_2_model t σ'
}}}.
End pstore_2_G.
#[global] Opaque pstore_2_model.
#[global] Opaque pstore_2_snapshot.
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
fin_maps
list
treemap.
From zoo.iris.base_logic Require Import
lib.mono_gmap.
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_2__code.
From zoo_persistent Require Import
pstore_2__types.
From zoo Require Import
options.
Implicit Types l r node cnode base root dst : location.
Implicit Types nodes : list location.
Implicit Types v t s : val.
Implicit Types σ σ₀ : gmap location val.
Module base.
#[local] Definition generation :=
nat.
Implicit Types g : generation.
#[local] Notation "data '.(gen)'" := (
fst data
)(at level 2,
left associativity,
format "data .(gen)"
) : stdpp_scope.
#[local] Notation "data '.(val)'" := (
snd data
)(at level 2,
left associativity,
format "data .(val)"
) : stdpp_scope.
#[local] Definition store :=
gmap location (generation × val).
Implicit Types ς : store.
Implicit Types data : generation × val.
Record descriptor := Descriptor
{ descriptor_gen : generation
; descriptor_store : store
}.
Add Printing Constructor descriptor.
Implicit Types descr : descriptor.
Implicit Types cnodes : gmap location descriptor.
Class Pstore2G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] pstore_2_G_nodes_G :: ghost_mapG Σ location descriptor
}.
Definition pstore_2_Σ :=
#[ghost_mapΣ location descriptor
].
#[global] Instance subG_pstore_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG pstore_2_Σ Σ →
Pstore2G Σ.
Section pstore_2_G.
Context `{pstore_2_G : Pstore2G Σ}.
#[local] Definition metadata :=
gname.
Implicit Types γ : metadata.
#[local] Definition store_on σ₀ ς :=
ς ∪ (pair 0 <$> σ₀).
#[local] Definition store_generation g ς :=
map_Forall (λ r data, data.(gen) ≤ g) ς.
#[local] Definition descriptor_wf σ₀ descr :=
dom descr.(descriptor_store) ⊆ dom σ₀ ∧
store_generation descr.(descriptor_gen) descr.(descriptor_store).
Record delta := Delta
{ delta_ref : location
; delta_gen : generation
; delta_val : val
; delta_node : location
}.
Add Printing Constructor delta.
Implicit Types δ : delta.
Implicit Types δs : list delta.
Implicit Types path : list (list delta).
#[local] Notation "δ '.(delta_data)'" := (
pair δ.(delta_gen) δ.(delta_val)
)(at level 2,
left associativity,
format "δ .(delta_data)"
) : stdpp_scope.
#[local] Definition delta_patch δ :=
(δ.(delta_ref), δ.(delta_data)).
#[local] Definition deltas_apply δs ς :=
list_to_map (delta_patch <$> δs) ∪ ς.
#[local] Fixpoint deltas_chain node δs dst : iProp Σ :=
match δs with
| [] ⇒
⌜node = dst⌝
| δ :: δs ⇒
node ↦ᵣ ‘Diff( #δ.(delta_ref), #δ.(delta_gen), δ.(delta_val), #δ.(delta_node) ) ∗
deltas_chain δ.(delta_node) δs dst
end.
#[local] Definition edge : Set :=
location × list delta.
Implicit Types ϵ : edge.
Implicit Types ϵs : gmap location edge.
#[local] Definition cnodes_auth γ cnodes :=
ghost_map_auth γ 1 cnodes.
#[local] Definition cnodes_elem γ cnode descr :=
ghost_map_elem γ cnode DfracDiscarded descr.
#[local] Definition cnode_model γ σ₀ cnode descr ϵ ς : iProp Σ :=
let cnode' := ϵ.1 in
let δs := ϵ.2 in
⌜descriptor_wf σ₀ descr⌝ ∗
cnodes_elem γ cnode descr ∗
⌜NoDup $ delta_ref <$> δs⌝ ∗
⌜store_on σ₀ descr.(descriptor_store) = store_on σ₀ $ deltas_apply δs ς⌝ ∗
deltas_chain cnode δs cnode'.
Definition pstore_2_model t σ₀ σ : iProp Σ :=
∃ l γ g root ς,
⌜t = #l⌝ ∗
⌜σ = snd <$> ς⌝ ∗
meta l (nroot.@"impl") γ ∗
l.[gen] ↦ #g ∗
l.[root] ↦ #root ∗
root ↦ᵣ §Root ∗
( [∗ map] r ↦ data ∈ store_on σ₀ ς,
r.[ref_gen] ↦ #data.(gen) ∗
r.[ref_value] ↦ data.(val)
) ∗
⌜descriptor_wf σ₀ (Descriptor g ς)⌝ ∗
if decide (g = 0) then
cnodes_auth γ ∅
else
∃ cnodes ϵs base descr δs,
⌜treemap_rooted ϵs base⌝ ∗
cnodes_auth γ cnodes ∗
⌜cnodes !! base = Some descr⌝ ∗
⌜descr.(descriptor_gen) < g⌝ ∗
cnode_model γ σ₀ base descr (root, δs) ς ∗
⌜δs = [] → ς = descr.(descriptor_store)⌝ ∗
⌜Forall (λ δ, ∃ data, ς !! δ.(delta_ref) = Some data ∧ data.(gen) = g) δs⌝ ∗
[∗ map] cnode ↦ descr; ϵ ∈ delete base cnodes; ϵs,
∃ descr',
⌜cnodes !! ϵ.1 = Some descr'⌝ ∗
cnode_model γ σ₀ cnode descr ϵ descr'.(descriptor_store).
Definition pstore_2_snapshot s t σ : iProp Σ :=
∃ l γ g cnode descr,
⌜t = #l⌝ ∗
⌜s = (t, #g, #cnode)%V⌝ ∗
⌜σ = snd <$> descr.(descriptor_store)⌝ ∗
⌜descr.(descriptor_gen) ≤ g⌝ ∗
meta l (nroot.@"impl") γ ∗
cnodes_elem γ cnode descr.
#[local] Instance deltas_chain_timeless node δs dst :
Timeless (deltas_chain node δs dst).
#[global] Instance pstore_2_model_timeless t σ₀ σ :
Timeless (pstore_2_model t σ₀ σ).
#[global] Instance pstore_2_snapshot_persistent s t σ :
Persistent (pstore_2_snapshot s t σ).
#[local] Lemma store_on_dom σ₀ ς :
dom (store_on σ₀ ς) = dom σ₀ ∪ dom ς.
#[local] Lemma store_on_dom' σ₀ ς :
dom ς ⊆ dom σ₀ →
dom (store_on σ₀ ς) = dom σ₀.
#[local] Lemma store_on_lookup {σ₀ ς} r data :
store_on σ₀ ς !! r = Some data ↔
ς !! r = Some data
∨ ς !! r = None ∧
data.(gen) = 0 ∧
σ₀ !! r = Some data.(val).
#[local] Lemma store_on_lookup' {σ₀ ς} r data :
ς !! r = Some data →
store_on σ₀ ς !! r = Some data.
#[local] Lemma store_on_insert r data σ₀ ς :
store_on σ₀ (<[r := data]> ς) = <[r := data]> (store_on σ₀ ς).
#[local] Lemma store_on_insert_support r v σ₀ ς :
σ₀ !! r = None →
dom ς ⊆ dom σ₀ →
store_on (<[r := v]> σ₀) ς = <[r := (0, v)]> (store_on σ₀ ς).
#[local] Lemma store_on_deltas_apply σ₀ δs ς :
store_on σ₀ (deltas_apply δs ς) = deltas_apply δs (store_on σ₀ ς).
#[local] Lemma store_generation_le {g ς} g' :
g ≤ g' →
store_generation g ς →
store_generation g' ς.
#[local] Lemma store_generation_insert g ς r data :
store_generation g ς →
data.(gen) ≤ g →
store_generation g (<[r := data]> ς).
#[local] Lemma deltas_apply_nil ς :
deltas_apply [] ς = ς.
#[local] Lemma deltas_apply_cons δ δs ς :
deltas_apply (δ :: δs) ς = <[δ.(delta_ref) := δ.(delta_data)]> (deltas_apply δs ς).
#[local] Lemma deltas_apply_singleton δ ς :
deltas_apply [δ] ς = <[δ.(delta_ref) := δ.(delta_data)]> ς.
#[local] Lemma deltas_apply_app δs1 δs2 ς :
deltas_apply (δs1 ++ δs2) ς = deltas_apply δs1 (deltas_apply δs2 ς).
#[local] Lemma deltas_apply_snoc δs δ ς :
deltas_apply (δs ++ [δ]) ς = deltas_apply δs (<[δ.(delta_ref) := δ.(delta_data)]> ς).
#[local] Lemma deltas_apply_snoc' δs r g v node ς :
deltas_apply (δs ++ [Delta r g v node]) ς = deltas_apply δs (<[r := (g, v)]> ς).
#[local] Lemma deltas_apply_dom δs ς :
dom (deltas_apply δs ς) = list_to_set (delta_ref <$> δs) ∪ dom ς.
#[local] Lemma deltas_apply_lookup δs δ r data ς :
NoDup (delta_ref <$> δs) →
δ ∈ δs →
r = δ.(delta_ref) →
data = δ.(delta_data) →
deltas_apply δs ς !! r = Some data.
#[local] Lemma deltas_apply_lookup' δs r data ς :
NoDup (delta_ref <$> δs) →
(r, data) ∈ delta_patch <$> δs →
deltas_apply δs ς !! r = Some data.
#[local] Lemma deltas_apply_lookup_ne r δs ς :
NoDup (delta_ref <$> δs) →
r ∉ (delta_ref <$> δs) →
deltas_apply δs ς !! r = ς !! r.
#[local] Lemma deltas_apply_permutation δs1 δs2 ς :
NoDup (delta_ref <$> δs1) →
δs1 ≡ₚ δs2 →
deltas_apply δs1 ς = deltas_apply δs2 ς.
#[local] Lemma deltas_chain_cons src δ δs dst :
src ↦ᵣ ‘Diff( #δ.(delta_ref), #δ.(delta_gen), δ.(delta_val), #δ.(delta_node) ) -∗
deltas_chain δ.(delta_node) δs dst -∗
deltas_chain src (δ :: δs) dst.
#[local] Lemma deltas_chain_nil_inv src dst :
deltas_chain src [] dst ⊢
⌜src = dst⌝.
#[local] Lemma deltas_chain_cons_inv src δ δs dst :
deltas_chain src (δ :: δs) dst ⊢
src ↦ᵣ ‘Diff( #δ.(delta_ref), #δ.(delta_gen), δ.(delta_val), #δ.(delta_node) ) ∗
deltas_chain δ.(delta_node) δs dst.
#[local] Lemma deltas_chain_snoc {src δs dst} r g v dst' :
deltas_chain src δs dst -∗
dst ↦ᵣ ‘Diff( #r, #g, v, #dst' ) -∗
deltas_chain src (δs ++ [Delta r g v dst']) dst'.
#[local] Lemma deltas_chain_app_1 src δs1 δs2 dst :
deltas_chain src (δs1 ++ δs2) dst ⊢
let node := default src $ delta_node <$> last δs1 in
deltas_chain src δs1 node ∗
deltas_chain node δs2 dst.
#[local] Lemma deltas_chain_app_2 src δs1 node δs2 dst :
deltas_chain src δs1 node -∗
deltas_chain node δs2 dst -∗
deltas_chain src (δs1 ++ δs2) dst.
#[local] Lemma deltas_chain_snoc_inv src δs δ dst :
deltas_chain src (δs ++ [δ]) dst ⊢
let node := default src $ delta_node <$> last δs in
⌜δ.(delta_node) = dst⌝ ∗
deltas_chain src δs node ∗
node ↦ᵣ ‘Diff( #δ.(delta_ref), #δ.(delta_gen), δ.(delta_val), #dst ).
#[local] Lemma deltas_chain_lookup {src δs dst} i δ :
δs !! i = Some δ →
deltas_chain src δs dst ⊢
deltas_chain src (take (S i) δs) δ.(delta_node) ∗
deltas_chain δ.(delta_node) (drop (S i) δs) dst.
#[local] Lemma deltas_chain_lookup' {src δs dst} i δ :
δs !! i = Some δ →
deltas_chain src δs dst ⊢
∃ node,
⌜ if i is 0 then
node = src
else
∃ δ',
δs !! pred i = Some δ' ∧
δ'.(delta_node) = node
⌝ ∗
deltas_chain src (take i δs) node ∗
node ↦ᵣ ‘Diff( #δ.(delta_ref), #δ.(delta_gen), δ.(delta_val), #δ.(delta_node) ) ∗
deltas_chain δ.(delta_node) (drop (S i) δs) dst.
#[local] Definition cnodes_alloc root :
⊢ |==>
∃ γ,
cnodes_auth γ ∅.
#[local] Definition cnodes_lookup γ cnodes cnode descr :
cnodes_auth γ cnodes -∗
cnodes_elem γ cnode descr -∗
⌜cnodes !! cnode = Some descr⌝.
#[local] Lemma cnodes_insert {γ cnodes} cnode descr :
cnodes !! cnode = None →
cnodes_auth γ cnodes ⊢ |==>
cnodes_auth γ (<[cnode := descr]> cnodes) ∗
cnodes_elem γ cnode descr.
Lemma pstore_2_model_valid t σ₀ σ :
pstore_2_model t σ₀ σ ⊢
⌜dom σ ⊆ dom σ₀⌝.
Lemma pstore_2_model_exclusive t σ₀1 σ1 σ₀2 σ2 :
pstore_2_model t σ₀1 σ1 -∗
pstore_2_model t σ₀2 σ2 -∗
False.
Lemma pstore_2٠create𑁒spec :
{{{
True
}}}
pstore_2٠create ()
{{{
t
, RET t;
(∃ l, ⌜t = #l⌝ ∗ meta_token l (↑nroot.@"user")) ∗
pstore_2_model t ∅ ∅
}}}.
Lemma pstore_2٠ref𑁒spec t σ₀ σ v :
{{{
pstore_2_model t σ₀ σ
}}}
pstore_2٠ref t v
{{{
r
, RET #r;
⌜σ₀ !! r = None⌝ ∗
pstore_2_model t (<[r := v]> σ₀) σ
}}}.
Lemma pstore_2٠get𑁒spec {t σ₀ σ r} v :
(σ ∪ σ₀) !! r = Some v →
{{{
pstore_2_model t σ₀ σ
}}}
pstore_2٠get t #r
{{{
RET v;
pstore_2_model t σ₀ σ
}}}.
Lemma pstore_2٠set𑁒spec t σ₀ σ r v :
r ∈ dom σ₀ →
{{{
pstore_2_model t σ₀ σ
}}}
pstore_2٠set t #r v
{{{
RET ();
pstore_2_model t σ₀ (<[r := v]> σ)
}}}.
Lemma pstore_2٠capture𑁒spec t σ₀ σ :
{{{
pstore_2_model t σ₀ σ
}}}
pstore_2٠capture t
{{{
s
, RET s;
pstore_2_model t σ₀ σ ∗
pstore_2_snapshot s t σ
}}}.
#[local] Definition collect_inv γ σ₀ root ς cnodes ϵs base descr δs : iProp Σ :=
root ↦ᵣ §Root ∗
( [∗ map] r ↦ data ∈ store_on σ₀ ς,
r.[ref_gen] ↦ #data.(gen) ∗
r.[ref_value] ↦ data.(val)
) ∗
⌜treemap_rooted ϵs base⌝ ∗
cnodes_auth γ cnodes ∗
⌜cnodes !! base = Some descr⌝ ∗
cnode_model γ σ₀ base descr (root, δs) ς ∗
⌜δs = [] → ς = descr.(descriptor_store)⌝ ∗
[∗ map] cnode ↦ descr; ϵ ∈ delete base cnodes; ϵs,
∃ descr',
⌜cnodes !! ϵ.1 = Some descr'⌝ ∗
cnode_model γ σ₀ cnode descr ϵ descr'.(descriptor_store).
#[local] Lemma pstore_2٠collect𑁒spec_base_chain {γ σ₀ root ς cnodes ϵs base descr δs} i δ node acc :
δs !! i = Some δ →
δ.(delta_node) = node →
{{{
collect_inv γ σ₀ root ς cnodes ϵs base descr δs
}}}
pstore_2٠collect #node acc
{{{
acc'
, RET (#root, acc');
collect_inv γ σ₀ root ς cnodes ϵs base descr δs ∗
plist_model acc' acc $ tail $
(λ δ, #δ.(delta_node)) <$> reverse (drop i δs)
}}}.
#[local] Definition collect𑁒specification γ σ₀ root ς cnodes ϵs base descr δs : iProp Σ :=
∀ cnode descr_cnode path acc,
{{{
⌜cnodes !! cnode = Some descr_cnode⌝ ∗
⌜treemap_path ϵs base cnode path⌝ ∗
collect_inv γ σ₀ root ς cnodes ϵs base descr δs
}}}
pstore_2٠collect #cnode acc
{{{
acc'
, RET (#root, acc');
collect_inv γ σ₀ root ς cnodes ϵs base descr δs ∗
plist_model acc' acc $ tail $
((λ δ, #δ.(delta_node)) <$> reverse δs) ++
((λ δ, #δ.(delta_node)) <$> reverse (concat path)) ++
[ #cnode]
}}}.
#[local] Lemma pstore_2٠collect𑁒spec_chain {γ σ₀ root ς cnodes ϵs base descr δs} cnode ϵ i 𝝳 node path acc :
ϵs !! cnode = Some ϵ →
ϵ.2 !! i = Some 𝝳 →
𝝳.(delta_node) = node →
treemap_path ϵs base ϵ.1 path →
{{{
collect_inv γ σ₀ root ς cnodes ϵs base descr δs ∗
collect𑁒specification γ σ₀ root ς cnodes ϵs base descr δs
}}}
pstore_2٠collect #node acc
{{{
acc'
, RET (#root, acc');
collect_inv γ σ₀ root ς cnodes ϵs base descr δs ∗
plist_model acc' acc $ tail $
((λ δ, #δ.(delta_node)) <$> reverse δs) ++
((λ δ, #δ.(delta_node)) <$> reverse (concat path)) ++
((λ δ, #δ.(delta_node)) <$> reverse (drop i ϵ.2))
}}}.
#[local] Lemma pstore_2٠collect𑁒spec {γ σ₀ root ς cnodes ϵs base descr δs} cnode descr_cnode path acc :
cnodes !! cnode = Some descr_cnode →
treemap_path ϵs base cnode path →
{{{
collect_inv γ σ₀ root ς cnodes ϵs base descr δs
}}}
pstore_2٠collect #cnode acc
{{{
acc'
, RET (#root, acc');
collect_inv γ σ₀ root ς cnodes ϵs base descr δs ∗
plist_model acc' acc $ tail $
((λ δ, #δ.(delta_node)) <$> reverse δs) ++
((λ δ, #δ.(delta_node)) <$> reverse (concat path)) ++
[ #cnode]
}}}.
#[local] Definition revert_pre_1 γ σ₀ root ς cnodes ϵs base descr δs : iProp Σ :=
∃ v_root,
root ↦ᵣ v_root ∗
( [∗ map] r ↦ data ∈ store_on σ₀ ς,
r.[ref_gen] ↦ #data.(gen) ∗
r.[ref_value] ↦ data.(val)
) ∗
⌜treemap_rooted ϵs base⌝ ∗
cnodes_auth γ cnodes ∗
⌜cnodes !! base = Some descr⌝ ∗
cnode_model γ σ₀ base descr (root, δs) ς ∗
⌜δs = [] → ς = descr.(descriptor_store)⌝ ∗
[∗ map] cnode ↦ descr; ϵ ∈ delete base cnodes; ϵs,
∃ descr',
⌜cnodes !! ϵ.1 = Some descr'⌝ ∗
cnode_model γ σ₀ cnode descr ϵ descr'.(descriptor_store).
#[local] Definition revert_pre_2 γ σ₀ ς cnodes ϵs base descr_base δs_base cnode descr_cnode δs_cnode node : iProp Σ :=
∃ v_node,
node ↦ᵣ v_node ∗
( [∗ map] r ↦ data ∈ store_on σ₀ ς,
r.[ref_gen] ↦ #data.(gen) ∗
r.[ref_value] ↦ data.(val)
) ∗
⌜treemap_rooted ϵs base⌝ ∗
cnodes_auth γ cnodes ∗
⌜cnodes !! base = Some descr_base⌝ ∗
cnode_model γ σ₀ base descr_base (node, δs_base) ς ∗
⌜cnodes !! cnode = Some descr_cnode⌝ ∗
cnode_model γ σ₀ cnode descr_cnode (node, δs_cnode) ς ∗
[∗ map] cnode ↦ descr; ϵ ∈ delete base $ delete cnode cnodes; delete cnode ϵs,
∃ descr',
⌜cnodes !! ϵ.1 = Some descr'⌝ ∗
cnode_model γ σ₀ cnode descr ϵ descr'.(descriptor_store).
#[local] Definition revert_post γ σ₀ cnodes ϵs base descr : iProp Σ :=
base ↦ᵣ §Root ∗
( [∗ map] r ↦ data ∈ store_on σ₀ descr.(descriptor_store),
r.[ref_gen] ↦ #data.(gen) ∗
r.[ref_value] ↦ data.(val)
) ∗
⌜treemap_rooted ϵs base⌝ ∗
cnodes_auth γ cnodes ∗
cnode_model γ σ₀ base descr (base, []) descr.(descriptor_store) ∗
[∗ map] cnode ↦ descr; ϵ ∈ delete base cnodes; ϵs,
∃ descr',
⌜cnodes !! ϵ.1 = Some descr'⌝ ∗
cnode_model γ σ₀ cnode descr ϵ descr'.(descriptor_store).
#[local] Lemma pstore_2٠revert𑁒spec_aux {γ σ₀ ς cnodes ϵs base descr_base δs_base cnode descr_cnode δs_cnode node} base' descr_base' path δs acc :
cnodes !! base' = Some descr_base' →
treemap_path ϵs cnode base' path →
ϵs !! cnode = Some (base, δs) →
0 < length δs_cnode →
NoDup (delta_ref <$> δs_cnode ++ δs_base) →
list_model' acc $ tail $
((λ δ, #δ.(delta_node)) <$> reverse δs_cnode) ++
((λ δ, #δ.(delta_node)) <$> reverse (concat path)) ++
[ #base'] →
{{{
revert_pre_2 γ σ₀ ς cnodes ϵs base descr_base δs_base cnode descr_cnode δs_cnode node
}}}
pstore_2٠revert #node acc
{{{
ϵs
, RET ();
revert_post γ σ₀ cnodes ϵs base' descr_base'
}}}.
#[local] Lemma pstore_2٠revert𑁒spec {γ σ₀ root ς cnodes ϵs base descr_base δs} base' descr_base' path acc :
cnodes !! base' = Some descr_base' →
treemap_path ϵs base base' path →
list_model' acc $ tail $
((λ δ, #δ.(delta_node)) <$> reverse δs) ++
((λ δ, #δ.(delta_node)) <$> reverse (concat path)) ++
[ #base'] →
{{{
revert_pre_1 γ σ₀ root ς cnodes ϵs base descr_base δs
}}}
pstore_2٠revert #root acc
{{{
ϵs
, RET ();
revert_post γ σ₀ cnodes ϵs base' descr_base'
}}}.
#[local] Lemma pstore_2٠reroot𑁒spec {γ σ₀ root ς cnodes ϵs base descr δs} base' descr' path :
cnodes !! base' = Some descr' →
treemap_path ϵs base base' path →
{{{
collect_inv γ σ₀ root ς cnodes ϵs base descr δs
}}}
pstore_2٠reroot #base'
{{{
ϵs
, RET ();
revert_post γ σ₀ cnodes ϵs base' descr'
}}}.
Lemma pstore_2٠restore𑁒spec t σ₀ σ s σ' :
{{{
pstore_2_model t σ₀ σ ∗
pstore_2_snapshot s t σ'
}}}
pstore_2٠restore t s
{{{
RET ();
pstore_2_model t σ₀ σ'
}}}.
End pstore_2_G.
#[global] Opaque pstore_2_model.
#[global] Opaque pstore_2_snapshot.
End base.
From zoo_persistent Require
pstore_2__opaque.
Class Pstore2G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] pstore_2_G_raw_G :: base.Pstore2G Σ
; #[local] pstore_2_G_support_G :: MonoGmapG Σ location val
}.
Definition pstore_2_Σ :=
#[base.pstore_2_Σ
; mono_gmap_Σ location val
].
#[global] Instance subG_pstore_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG pstore_2_Σ Σ →
Pstore2G Σ.
Section pstore_2_G.
Context `{pstore_2_G : Pstore2G Σ}.
#[local] Definition metadata :=
gname.
Implicit Types γ : metadata.
Definition pstore_2_model t σ : iProp Σ :=
∃ l γ σ₀ ς,
⌜t = #l⌝ ∗
⌜σ ⊆ ς ∪ σ₀⌝ ∗
meta l (nroot.@"user") γ ∗
mono_gmap_auth γ (DfracOwn 1) σ₀ ∗
base.pstore_2_model t σ₀ ς.
Definition pstore_2_snapshot s t σ : iProp Σ :=
∃ l γ σ₀ ς,
⌜t = #l⌝ ∗
⌜σ ⊆ ς ∪ σ₀⌝ ∗
meta l (nroot.@"user") γ ∗
mono_gmap_lb γ σ₀ ∗
base.pstore_2_snapshot s t ς.
#[global] Instance pstore_2_model_timeless t σ :
Timeless (pstore_2_model t σ).
#[global] Instance pstore_2_snapshot_persistent s t σ :
Persistent (pstore_2_snapshot s t σ).
Lemma pstore_2_model_exclusive t σ1 σ2 :
pstore_2_model t σ1 -∗
pstore_2_model t σ2 -∗
False.
Lemma pstore_2٠create𑁒spec :
{{{
True
}}}
pstore_2٠create ()
{{{
t
, RET t;
pstore_2_model t ∅
}}}.
Lemma pstore_2٠ref𑁒spec t σ v :
{{{
pstore_2_model t σ
}}}
pstore_2٠ref t v
{{{
r
, RET #r;
⌜σ !! r = None⌝ ∗
pstore_2_model t (<[r := v]> σ)
}}}.
Lemma pstore_2٠get𑁒spec {t σ r} v :
σ !! r = Some v →
{{{
pstore_2_model t σ
}}}
pstore_2٠get t #r
{{{
RET v;
pstore_2_model t σ
}}}.
Lemma pstore_2٠set𑁒spec t σ r v :
r ∈ dom σ →
{{{
pstore_2_model t σ
}}}
pstore_2٠set t #r v
{{{
RET ();
pstore_2_model t (<[r := v]> σ)
}}}.
Lemma pstore_2٠capture𑁒spec t σ :
{{{
pstore_2_model t σ
}}}
pstore_2٠capture t
{{{
s
, RET s;
pstore_2_model t σ ∗
pstore_2_snapshot s t σ
}}}.
Lemma pstore_2٠restore𑁒spec t σ s σ' :
{{{
pstore_2_model t σ ∗
pstore_2_snapshot s t σ'
}}}
pstore_2٠restore t s
{{{
RET ();
pstore_2_model t σ'
}}}.
End pstore_2_G.
#[global] Opaque pstore_2_model.
#[global] Opaque pstore_2_snapshot.