Library zoo_persistent.parray_2
From iris.base_logic Require Import
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
countable.
From zoo.iris.bi Require Import
big_op.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
array.
From zoo_persistent Require Export
base
parray_2__code.
From zoo_persistent Require Import
parray_2__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types l node root : location.
Implicit Types v t s equal : val.
Implicit Types vs : list val.
Implicit Types nodes : gmap location (list val).
Class Parray2G Σ `{zoo_G : !ZooG Σ} :=
{ parray_2_G_nodes_G : ghost_mapG Σ location (list val)
}.
Definition parray_2_Σ :=
#[ghost_mapΣ location (list val)
].
#[global] Instance subG_parray_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG parray_2_Σ Σ →
Parray2G Σ.
Section parray_2_G.
Context `{parray_2_G : Parray2G Σ}.
Context τ `{!iType (iProp Σ) τ}.
Record metadata :=
{ metadata_equal : val
; metadata_size : nat
; metadata_data : val
; metadata_nodes : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition nodes_auth' γ_nodes :=
@ghost_map_auth _ _ _ _ _ parray_2_G_nodes_G γ_nodes 1.
#[local] Definition nodes_auth γ :=
nodes_auth' γ.(metadata_nodes).
#[local] Definition nodes_elem' γ_nodes node :=
@ghost_map_elem _ _ _ _ _ parray_2_G_nodes_G γ_nodes node DfracDiscarded.
#[local] Definition nodes_elem γ :=
nodes_elem' γ.(metadata_nodes).
Definition equal_model equal : iProp Σ :=
□ ∀ v1 v2,
τ v1 -∗
τ v2 -∗
WP equal v1 v2 {{ res,
∃ b,
⌜res = #b⌝ ∗
⌜if b then v1 = v2 else True⌝
}}.
#[local] Definition node_model γ node vs : iProp Σ :=
∃ (i : nat) v node' vs',
node ↦ᵣ ‘Diff( #i, v, #node' ) ∗
τ v ∗
nodes_elem γ node' vs' ∗
⌜length vs = γ.(metadata_size)⌝ ∗
⌜i < γ.(metadata_size)⌝ ∗
⌜vs = <[i := v]> vs'⌝.
#[local] Instance : CustomIpat "node_model" :=
" ( %i_{node} & %v_{node} & %node{;'} & %vs_node{;'} & H{node}{_{!}} & #Hv_{node} & #Hnodes_elem_node{;'} & % & % & %Hvs_{node} ) ".
#[local] Definition model' γ nodes root vs_root : iProp Σ :=
nodes_auth γ nodes ∗
root ↦ᵣ §Root ∗
array_model γ.(metadata_data) (DfracOwn 1) vs_root ∗
nodes_elem γ root vs_root ∗
⌜length vs_root = γ.(metadata_size)⌝ ∗
([∗ list] v ∈ vs_root, τ v) ∗
[∗ map] node ↦ vs ∈ delete root nodes,
node_model γ node vs.
#[local] Instance : CustomIpat "model'" :=
" ( Hnodes_auth{_{}} & H{root}{} & Hdata{_{}} & #Hnodes_elem_{root}{_{}} & % & #Hvs_{root}{_{}} & Hnodes{_{}} ) ".
Definition parray_2_model t vs : iProp Σ :=
∃ l γ nodes root,
⌜t = #l⌝ ∗
meta l nroot γ ∗
l.[equal] ↦□ γ.(metadata_equal) ∗
l.[data] ↦□ γ.(metadata_data) ∗
l.[root] ↦ #root ∗
equal_model γ.(metadata_equal) ∗
model' γ nodes root vs.
#[local] Instance : CustomIpat "model" :=
" ( %l{} & %γ{} & %nodes{} & %root{} & {%Heq{};->} & #Hmeta{_{}} & #Hl_equal{_{}} & #Hl_data{_{}} & Hl_root{_{}} & #Hequal{_{}} & (:model') ) ".
Definition parray_2_snapshot s t vs : iProp Σ :=
∃ node l γ,
⌜s = #node⌝ ∗
⌜t = #l⌝ ∗
meta l nroot γ ∗
nodes_elem γ node vs.
#[local] Instance : CustomIpat "snapshot" :=
" ( %node & %l_ & %γ_ & -> & %Heq & #Hmeta_ & #Hnodes_elem_node ) ".
#[global] Instance parray_2_snapshot_persistent s t vs :
Persistent (parray_2_snapshot s t vs).
#[local] Lemma nodes_alloc root vs :
⊢ |==>
∃ γ_nodes,
nodes_auth' γ_nodes {[root := vs]} ∗
nodes_elem' γ_nodes root vs.
#[local] Lemma nodes_elem_lookup γ nodes node vs :
nodes_auth γ nodes -∗
nodes_elem γ node vs -∗
⌜nodes !! node = Some vs⌝.
#[local] Lemma nodes_elem_agree γ node vs1 vs2 :
nodes_elem γ node vs1 -∗
nodes_elem γ node vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma nodes_insert {γ nodes} node vs :
nodes !! node = None →
nodes_auth γ nodes ⊢ |==>
nodes_auth γ (<[node := vs]> nodes) ∗
nodes_elem γ node vs.
Lemma parray_2_model_exclusive t vs1 vs2 :
parray_2_model t vs1 -∗
parray_2_model t vs2 -∗
False.
Lemma parray_2٠make𑁒spec equal (sz : Z) v :
(0 ≤ sz)%Z →
{{{
equal_model equal ∗
τ v
}}}
parray_2٠make equal #sz v
{{{
t
, RET t;
parray_2_model t (replicate ₊sz v)
}}}.
Lemma parray_2٠get𑁒spec {t vs} i v :
(0 ≤ i)%Z →
vs !! ₊i = Some v →
{{{
parray_2_model t vs
}}}
parray_2٠get t #i
{{{
RET v;
parray_2_model t vs
}}}.
Lemma parray_2٠set𑁒spec t vs i v :
(0 ≤ i < length vs)%Z →
{{{
parray_2_model t vs ∗
τ v
}}}
parray_2٠set t #i v
{{{
RET ();
parray_2_model t (<[₊i := v]> vs)
}}}.
Lemma parray_2٠capture𑁒spec t vs :
{{{
parray_2_model t vs
}}}
parray_2٠capture t
{{{
s
, RET s;
parray_2_model t vs ∗
parray_2_snapshot s t vs
}}}.
#[local] Definition restore_inv γ nodes root vs_root : iProp Σ :=
∃ descr_root,
nodes_auth γ nodes ∗
root ↦ᵣ descr_root ∗
array_model γ.(metadata_data) (DfracOwn 1) vs_root ∗
⌜length vs_root = γ.(metadata_size)⌝ ∗
([∗ list] v ∈ vs_root, τ v) ∗
[∗ map] node ↦ vs ∈ delete root nodes,
node_model γ node vs.
#[local] Instance : CustomIpat "restore_inv" :=
" ( %descr_{root} & Hnodes_auth & H{root} & Hdata & % & #Hvs_{root} & Hnodes ) ".
#[local] Lemma parray_2٠restore₀𑁒spec {γ nodes root vs_root node} vs :
{{{
model' γ nodes root vs_root ∗
nodes_elem γ node vs
}}}
parray_2٠restore₀ γ.(metadata_data) #node
{{{
RET ();
restore_inv γ nodes node vs
}}}.
Lemma parray_2٠restore𑁒spec t vs s vs' :
{{{
parray_2_model t vs ∗
parray_2_snapshot s t vs'
}}}
parray_2٠restore t s
{{{
RET ();
parray_2_model t vs'
}}}.
End parray_2_G.
From zoo_persistent Require
parray_2__opaque.
#[global] Opaque parray_2_model.
#[global] Opaque parray_2_snapshot.
lib.ghost_map.
From zoo Require Import
prelude.
From zoo.common Require Import
countable.
From zoo.iris.bi Require Import
big_op.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
array.
From zoo_persistent Require Export
base
parray_2__code.
From zoo_persistent Require Import
parray_2__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types l node root : location.
Implicit Types v t s equal : val.
Implicit Types vs : list val.
Implicit Types nodes : gmap location (list val).
Class Parray2G Σ `{zoo_G : !ZooG Σ} :=
{ parray_2_G_nodes_G : ghost_mapG Σ location (list val)
}.
Definition parray_2_Σ :=
#[ghost_mapΣ location (list val)
].
#[global] Instance subG_parray_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG parray_2_Σ Σ →
Parray2G Σ.
Section parray_2_G.
Context `{parray_2_G : Parray2G Σ}.
Context τ `{!iType (iProp Σ) τ}.
Record metadata :=
{ metadata_equal : val
; metadata_size : nat
; metadata_data : val
; metadata_nodes : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition nodes_auth' γ_nodes :=
@ghost_map_auth _ _ _ _ _ parray_2_G_nodes_G γ_nodes 1.
#[local] Definition nodes_auth γ :=
nodes_auth' γ.(metadata_nodes).
#[local] Definition nodes_elem' γ_nodes node :=
@ghost_map_elem _ _ _ _ _ parray_2_G_nodes_G γ_nodes node DfracDiscarded.
#[local] Definition nodes_elem γ :=
nodes_elem' γ.(metadata_nodes).
Definition equal_model equal : iProp Σ :=
□ ∀ v1 v2,
τ v1 -∗
τ v2 -∗
WP equal v1 v2 {{ res,
∃ b,
⌜res = #b⌝ ∗
⌜if b then v1 = v2 else True⌝
}}.
#[local] Definition node_model γ node vs : iProp Σ :=
∃ (i : nat) v node' vs',
node ↦ᵣ ‘Diff( #i, v, #node' ) ∗
τ v ∗
nodes_elem γ node' vs' ∗
⌜length vs = γ.(metadata_size)⌝ ∗
⌜i < γ.(metadata_size)⌝ ∗
⌜vs = <[i := v]> vs'⌝.
#[local] Instance : CustomIpat "node_model" :=
" ( %i_{node} & %v_{node} & %node{;'} & %vs_node{;'} & H{node}{_{!}} & #Hv_{node} & #Hnodes_elem_node{;'} & % & % & %Hvs_{node} ) ".
#[local] Definition model' γ nodes root vs_root : iProp Σ :=
nodes_auth γ nodes ∗
root ↦ᵣ §Root ∗
array_model γ.(metadata_data) (DfracOwn 1) vs_root ∗
nodes_elem γ root vs_root ∗
⌜length vs_root = γ.(metadata_size)⌝ ∗
([∗ list] v ∈ vs_root, τ v) ∗
[∗ map] node ↦ vs ∈ delete root nodes,
node_model γ node vs.
#[local] Instance : CustomIpat "model'" :=
" ( Hnodes_auth{_{}} & H{root}{} & Hdata{_{}} & #Hnodes_elem_{root}{_{}} & % & #Hvs_{root}{_{}} & Hnodes{_{}} ) ".
Definition parray_2_model t vs : iProp Σ :=
∃ l γ nodes root,
⌜t = #l⌝ ∗
meta l nroot γ ∗
l.[equal] ↦□ γ.(metadata_equal) ∗
l.[data] ↦□ γ.(metadata_data) ∗
l.[root] ↦ #root ∗
equal_model γ.(metadata_equal) ∗
model' γ nodes root vs.
#[local] Instance : CustomIpat "model" :=
" ( %l{} & %γ{} & %nodes{} & %root{} & {%Heq{};->} & #Hmeta{_{}} & #Hl_equal{_{}} & #Hl_data{_{}} & Hl_root{_{}} & #Hequal{_{}} & (:model') ) ".
Definition parray_2_snapshot s t vs : iProp Σ :=
∃ node l γ,
⌜s = #node⌝ ∗
⌜t = #l⌝ ∗
meta l nroot γ ∗
nodes_elem γ node vs.
#[local] Instance : CustomIpat "snapshot" :=
" ( %node & %l_ & %γ_ & -> & %Heq & #Hmeta_ & #Hnodes_elem_node ) ".
#[global] Instance parray_2_snapshot_persistent s t vs :
Persistent (parray_2_snapshot s t vs).
#[local] Lemma nodes_alloc root vs :
⊢ |==>
∃ γ_nodes,
nodes_auth' γ_nodes {[root := vs]} ∗
nodes_elem' γ_nodes root vs.
#[local] Lemma nodes_elem_lookup γ nodes node vs :
nodes_auth γ nodes -∗
nodes_elem γ node vs -∗
⌜nodes !! node = Some vs⌝.
#[local] Lemma nodes_elem_agree γ node vs1 vs2 :
nodes_elem γ node vs1 -∗
nodes_elem γ node vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma nodes_insert {γ nodes} node vs :
nodes !! node = None →
nodes_auth γ nodes ⊢ |==>
nodes_auth γ (<[node := vs]> nodes) ∗
nodes_elem γ node vs.
Lemma parray_2_model_exclusive t vs1 vs2 :
parray_2_model t vs1 -∗
parray_2_model t vs2 -∗
False.
Lemma parray_2٠make𑁒spec equal (sz : Z) v :
(0 ≤ sz)%Z →
{{{
equal_model equal ∗
τ v
}}}
parray_2٠make equal #sz v
{{{
t
, RET t;
parray_2_model t (replicate ₊sz v)
}}}.
Lemma parray_2٠get𑁒spec {t vs} i v :
(0 ≤ i)%Z →
vs !! ₊i = Some v →
{{{
parray_2_model t vs
}}}
parray_2٠get t #i
{{{
RET v;
parray_2_model t vs
}}}.
Lemma parray_2٠set𑁒spec t vs i v :
(0 ≤ i < length vs)%Z →
{{{
parray_2_model t vs ∗
τ v
}}}
parray_2٠set t #i v
{{{
RET ();
parray_2_model t (<[₊i := v]> vs)
}}}.
Lemma parray_2٠capture𑁒spec t vs :
{{{
parray_2_model t vs
}}}
parray_2٠capture t
{{{
s
, RET s;
parray_2_model t vs ∗
parray_2_snapshot s t vs
}}}.
#[local] Definition restore_inv γ nodes root vs_root : iProp Σ :=
∃ descr_root,
nodes_auth γ nodes ∗
root ↦ᵣ descr_root ∗
array_model γ.(metadata_data) (DfracOwn 1) vs_root ∗
⌜length vs_root = γ.(metadata_size)⌝ ∗
([∗ list] v ∈ vs_root, τ v) ∗
[∗ map] node ↦ vs ∈ delete root nodes,
node_model γ node vs.
#[local] Instance : CustomIpat "restore_inv" :=
" ( %descr_{root} & Hnodes_auth & H{root} & Hdata & % & #Hvs_{root} & Hnodes ) ".
#[local] Lemma parray_2٠restore₀𑁒spec {γ nodes root vs_root node} vs :
{{{
model' γ nodes root vs_root ∗
nodes_elem γ node vs
}}}
parray_2٠restore₀ γ.(metadata_data) #node
{{{
RET ();
restore_inv γ nodes node vs
}}}.
Lemma parray_2٠restore𑁒spec t vs s vs' :
{{{
parray_2_model t vs ∗
parray_2_snapshot s t vs'
}}}
parray_2٠restore t s
{{{
RET ();
parray_2_model t vs'
}}}.
End parray_2_G.
From zoo_persistent Require
parray_2__opaque.
#[global] Opaque parray_2_model.
#[global] Opaque parray_2_snapshot.