Library zoo_persistent.parray_1
From iris.base_logic Require Import
lib.ghost_map.
From zoo Require Import
prelude.
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_1__code.
From zoo_persistent Require Import
parray_1__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types node root : location.
Implicit Types v t equal : val.
Implicit Types vs : list val.
Implicit Types nodes : gmap location (list val).
Class Parray1G Σ `{zoo_G : !ZooG Σ} :=
{ parray_1_G_nodes_G : ghost_mapG Σ location (list val)
}.
Definition parray_1_Σ :=
#[ghost_mapΣ location (list val)
].
#[global] Instance subG_parray_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG parray_1_Σ Σ →
Parray1G Σ.
Section parray_1_G.
Context `{parray_1_G : Parray1G Σ}.
Context τ `{!iType (iProp Σ) τ}.
Record metadata :=
{ metadata_equal : val
; metadata_size : nat
; metadata_data : val
; metadata_nodes : gname
}.
Implicit Types γ : metadata.
#[local] Definition nodes_auth' γ_nodes :=
@ghost_map_auth _ _ _ _ _ parray_1_G_nodes_G γ_nodes 1.
#[local] Definition nodes_auth γ :=
nodes_auth' γ.(metadata_nodes).
#[local] Definition nodes_elem' γ_nodes node :=
@ghost_map_elem _ _ _ _ _ parray_1_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 inv' γ nodes root : iProp Σ :=
∃ vs_root,
equal_model γ.(metadata_equal) ∗
nodes_auth γ nodes ∗
root ↦ᵣ ‘Root( γ.(metadata_equal), γ.(metadata_data) ) ∗
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 "inv'" :=
" ( %vs_{root}{_{}} & #Hequal{_{}} & Hnodes_auth{_{}} & H{root}{} & Hdata{_{}} & #Hnodes_elem_{root}{_{}}{_{!}} & % & #Hvs_{root}{_{}} & Hnodes{_{}} ) ".
Definition parray_1_inv γ : iProp Σ :=
∃ nodes root,
inv' γ nodes root.
#[local] Instance : CustomIpat "inv" :=
" ( %nodes{} & %{root}{} & (:inv') ) ".
Definition parray_1_model t γ vs : iProp Σ :=
∃ node,
⌜t = #node⌝ ∗
nodes_elem γ node vs.
#[local] Instance : CustomIpat "model" :=
" ( %node & -> & #Hnodes_elem_node ) ".
#[global] Instance parray_1_model_persistent t γ vs :
Persistent (parray_1_model t γ vs).
#[local] Lemma nodes_alloc root vs :
⊢ |==>
∃ γ_nodes,
nodes_auth' γ_nodes {[root := vs]} ∗
nodes_elem' γ_nodes root vs.
#[local] Lemma nodes_auth_exclusive γ nodes1 nodes2 :
nodes_auth γ nodes1 -∗
nodes_auth γ nodes2 -∗
False.
#[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_1_inv_exclusive γ :
parray_1_inv γ -∗
parray_1_inv γ -∗
False.
Lemma parray_1٠make𑁒spec equal (sz : Z) v :
(0 ≤ sz)%Z →
{{{
equal_model equal ∗
τ v
}}}
parray_1٠make equal #sz v
{{{
t γ
, RET t;
parray_1_inv γ ∗
parray_1_model t γ (replicate ₊sz v)
}}}.
#[local] Definition reroot_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 "reroot_inv" :=
" ( %descr_{root} & Hnodes_auth & H{root} & Hdata & % & #Hvs_{root} & Hnodes ) ".
#[local] Lemma parray_1٠reroot₀𑁒spec {γ nodes root node} vs :
{{{
inv' γ nodes root ∗
nodes_elem γ node vs
}}}
parray_1٠reroot₀ #node
{{{
RET (γ.(metadata_equal), γ.(metadata_data));
reroot_inv γ nodes node vs
}}}.
#[local] Lemma parray_1٠reroot𑁒spec γ node vs :
{{{
parray_1_inv γ ∗
nodes_elem γ node vs
}}}
parray_1٠reroot #node
{{{
nodes
, RET (γ.(metadata_equal),γ.(metadata_data));
inv' γ nodes node
}}}.
Lemma parray_1٠get𑁒spec {t γ vs} i v :
(0 ≤ i)%Z →
vs !! ₊i = Some v →
{{{
parray_1_inv γ ∗
parray_1_model t γ vs
}}}
parray_1٠get t #i
{{{
RET v;
parray_1_inv γ
}}}.
Lemma parray_1٠set𑁒spec t γ vs i v :
(0 ≤ i < length vs)%Z →
{{{
parray_1_inv γ ∗
parray_1_model t γ vs ∗
τ v
}}}
parray_1٠set t #i v
{{{
t'
, RET t';
parray_1_inv γ ∗
parray_1_model t' γ (<[₊i := v]> vs)
}}}.
End parray_1_G.
From zoo_persistent Require
parray_1__opaque.
#[global] Opaque parray_1_inv.
#[global] Opaque parray_1_model.
lib.ghost_map.
From zoo Require Import
prelude.
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_1__code.
From zoo_persistent Require Import
parray_1__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types node root : location.
Implicit Types v t equal : val.
Implicit Types vs : list val.
Implicit Types nodes : gmap location (list val).
Class Parray1G Σ `{zoo_G : !ZooG Σ} :=
{ parray_1_G_nodes_G : ghost_mapG Σ location (list val)
}.
Definition parray_1_Σ :=
#[ghost_mapΣ location (list val)
].
#[global] Instance subG_parray_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG parray_1_Σ Σ →
Parray1G Σ.
Section parray_1_G.
Context `{parray_1_G : Parray1G Σ}.
Context τ `{!iType (iProp Σ) τ}.
Record metadata :=
{ metadata_equal : val
; metadata_size : nat
; metadata_data : val
; metadata_nodes : gname
}.
Implicit Types γ : metadata.
#[local] Definition nodes_auth' γ_nodes :=
@ghost_map_auth _ _ _ _ _ parray_1_G_nodes_G γ_nodes 1.
#[local] Definition nodes_auth γ :=
nodes_auth' γ.(metadata_nodes).
#[local] Definition nodes_elem' γ_nodes node :=
@ghost_map_elem _ _ _ _ _ parray_1_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 inv' γ nodes root : iProp Σ :=
∃ vs_root,
equal_model γ.(metadata_equal) ∗
nodes_auth γ nodes ∗
root ↦ᵣ ‘Root( γ.(metadata_equal), γ.(metadata_data) ) ∗
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 "inv'" :=
" ( %vs_{root}{_{}} & #Hequal{_{}} & Hnodes_auth{_{}} & H{root}{} & Hdata{_{}} & #Hnodes_elem_{root}{_{}}{_{!}} & % & #Hvs_{root}{_{}} & Hnodes{_{}} ) ".
Definition parray_1_inv γ : iProp Σ :=
∃ nodes root,
inv' γ nodes root.
#[local] Instance : CustomIpat "inv" :=
" ( %nodes{} & %{root}{} & (:inv') ) ".
Definition parray_1_model t γ vs : iProp Σ :=
∃ node,
⌜t = #node⌝ ∗
nodes_elem γ node vs.
#[local] Instance : CustomIpat "model" :=
" ( %node & -> & #Hnodes_elem_node ) ".
#[global] Instance parray_1_model_persistent t γ vs :
Persistent (parray_1_model t γ vs).
#[local] Lemma nodes_alloc root vs :
⊢ |==>
∃ γ_nodes,
nodes_auth' γ_nodes {[root := vs]} ∗
nodes_elem' γ_nodes root vs.
#[local] Lemma nodes_auth_exclusive γ nodes1 nodes2 :
nodes_auth γ nodes1 -∗
nodes_auth γ nodes2 -∗
False.
#[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_1_inv_exclusive γ :
parray_1_inv γ -∗
parray_1_inv γ -∗
False.
Lemma parray_1٠make𑁒spec equal (sz : Z) v :
(0 ≤ sz)%Z →
{{{
equal_model equal ∗
τ v
}}}
parray_1٠make equal #sz v
{{{
t γ
, RET t;
parray_1_inv γ ∗
parray_1_model t γ (replicate ₊sz v)
}}}.
#[local] Definition reroot_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 "reroot_inv" :=
" ( %descr_{root} & Hnodes_auth & H{root} & Hdata & % & #Hvs_{root} & Hnodes ) ".
#[local] Lemma parray_1٠reroot₀𑁒spec {γ nodes root node} vs :
{{{
inv' γ nodes root ∗
nodes_elem γ node vs
}}}
parray_1٠reroot₀ #node
{{{
RET (γ.(metadata_equal), γ.(metadata_data));
reroot_inv γ nodes node vs
}}}.
#[local] Lemma parray_1٠reroot𑁒spec γ node vs :
{{{
parray_1_inv γ ∗
nodes_elem γ node vs
}}}
parray_1٠reroot #node
{{{
nodes
, RET (γ.(metadata_equal),γ.(metadata_data));
inv' γ nodes node
}}}.
Lemma parray_1٠get𑁒spec {t γ vs} i v :
(0 ≤ i)%Z →
vs !! ₊i = Some v →
{{{
parray_1_inv γ ∗
parray_1_model t γ vs
}}}
parray_1٠get t #i
{{{
RET v;
parray_1_inv γ
}}}.
Lemma parray_1٠set𑁒spec t γ vs i v :
(0 ≤ i < length vs)%Z →
{{{
parray_1_inv γ ∗
parray_1_model t γ vs ∗
τ v
}}}
parray_1٠set t #i v
{{{
t'
, RET t';
parray_1_inv γ ∗
parray_1_model t' γ (<[₊i := v]> vs)
}}}.
End parray_1_G.
From zoo_persistent Require
parray_1__opaque.
#[global] Opaque parray_1_inv.
#[global] Opaque parray_1_model.