Library zoo_persistent.sarray
Require Import iris.base_logic.lib.ghost_map.
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Export zoo_persistent.sarray__code.
Require Import zoo_persistent.sarray__types.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type l node root : location.
Implicit Type v t s equal : val.
Implicit Type vs : list val.
Implicit Type nodes : gmap location (list val).
Class SarrayG Σ `{zoo۰G : !ZooG Σ} :=
{ sarray۰G۰nodes۰G : ghost_mapG Σ location (list val)
}.
Definition sarray۰Σ :=
#[ghost_mapΣ location (list val)
].
#[global] Instance subGｰsarray۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG sarray۰Σ Σ →
SarrayG Σ.
Section sarray۰G.
Context `{sarray۰G : SarrayG Σ}.
Context τ `{!iType (iProp Σ) τ}.
Record metadata :=
{ metadata۰equal : val
; metadata۰size : nat
; metadata۰data : val
; metadata۰nodes : gname
}.
Implicit Type γ : 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 _ _ _ _ _ sarray۰G۰nodes۰G γ_nodes 1.
#[local] Definition nodes۰auth γ :=
nodes۰auth' γ.(metadata۰nodes).
#[local] Definition nodes۰elem' γ_nodes node :=
@ghost_map_elem _ _ _ _ _ sarray۰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 sarray۰model t vs : iProp Σ :=
∃ l γ nodes root,
⌜t = #l⌝ ∗
l ↪ γ ∗
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 sarray۰snapshot s t vs : iProp Σ :=
∃ node l γ,
⌜s = #node⌝ ∗
⌜t = #l⌝ ∗
l ↪ γ ∗
nodes۰elem γ node vs.
#[local] Instance : CustomIpat "snapshot" :=
" ( %node & %l_ & %γ_ & -> & %Heq & #Hmeta_ & #Hnodes_elem_node ) ".
#[global] Instance sarray۰snapshotｰpersistent s t vs :
Persistent (sarray۰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 sarray۰modelｰexclusive t vs1 vs2 :
sarray۰model t vs1 -∗
sarray۰model t vs2 -∗
False.
Lemma sarray٠makeｰspec equal (sz : Z) v :
(0 ≤ sz)%Z →
{{{
equal۰model equal ∗
τ v
}}}
sarray٠make equal #sz v
{{{
t
, RET t;
sarray۰model t (replicate ₊sz v)
}}}.
Lemma sarray٠getｰspec {t vs} i v :
(0 ≤ i)%Z →
vs !! ₊i = Some v →
{{{
sarray۰model t vs
}}}
sarray٠get t #i
{{{
RET v;
sarray۰model t vs
}}}.
Lemma sarray٠setｰspec t vs i v :
(0 ≤ i < length vs)%Z →
{{{
sarray۰model t vs ∗
τ v
}}}
sarray٠set t #i v
{{{
RET ();
sarray۰model t (<[₊i := v]> vs)
}}}.
Lemma sarray٠captureｰspec t vs :
{{{
sarray۰model t vs
}}}
sarray٠capture t
{{{
s
, RET s;
sarray۰model t vs ∗
sarray۰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 sarray٠restore₁ｰspec {γ nodes root vs_root node} vs :
{{{
model' γ nodes root vs_root ∗
nodes۰elem γ node vs
}}}
sarray٠restore₁ γ.(metadata۰data) #node
{{{
RET ();
restore۰inv γ nodes node vs
}}}.
Lemma sarray٠restoreｰspec t vs s vs' :
{{{
sarray۰model t vs ∗
sarray۰snapshot s t vs'
}}}
sarray٠restore t s
{{{
RET ();
sarray۰model t vs'
}}}.
End sarray۰G.
Require zoo_persistent.sarray__opaque.
#[global] Opaque sarray۰model.
#[global] Opaque sarray۰snapshot.
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Export zoo_persistent.sarray__code.
Require Import zoo_persistent.sarray__types.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type l node root : location.
Implicit Type v t s equal : val.
Implicit Type vs : list val.
Implicit Type nodes : gmap location (list val).
Class SarrayG Σ `{zoo۰G : !ZooG Σ} :=
{ sarray۰G۰nodes۰G : ghost_mapG Σ location (list val)
}.
Definition sarray۰Σ :=
#[ghost_mapΣ location (list val)
].
#[global] Instance subGｰsarray۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG sarray۰Σ Σ →
SarrayG Σ.
Section sarray۰G.
Context `{sarray۰G : SarrayG Σ}.
Context τ `{!iType (iProp Σ) τ}.
Record metadata :=
{ metadata۰equal : val
; metadata۰size : nat
; metadata۰data : val
; metadata۰nodes : gname
}.
Implicit Type γ : 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 _ _ _ _ _ sarray۰G۰nodes۰G γ_nodes 1.
#[local] Definition nodes۰auth γ :=
nodes۰auth' γ.(metadata۰nodes).
#[local] Definition nodes۰elem' γ_nodes node :=
@ghost_map_elem _ _ _ _ _ sarray۰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 sarray۰model t vs : iProp Σ :=
∃ l γ nodes root,
⌜t = #l⌝ ∗
l ↪ γ ∗
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 sarray۰snapshot s t vs : iProp Σ :=
∃ node l γ,
⌜s = #node⌝ ∗
⌜t = #l⌝ ∗
l ↪ γ ∗
nodes۰elem γ node vs.
#[local] Instance : CustomIpat "snapshot" :=
" ( %node & %l_ & %γ_ & -> & %Heq & #Hmeta_ & #Hnodes_elem_node ) ".
#[global] Instance sarray۰snapshotｰpersistent s t vs :
Persistent (sarray۰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 sarray۰modelｰexclusive t vs1 vs2 :
sarray۰model t vs1 -∗
sarray۰model t vs2 -∗
False.
Lemma sarray٠makeｰspec equal (sz : Z) v :
(0 ≤ sz)%Z →
{{{
equal۰model equal ∗
τ v
}}}
sarray٠make equal #sz v
{{{
t
, RET t;
sarray۰model t (replicate ₊sz v)
}}}.
Lemma sarray٠getｰspec {t vs} i v :
(0 ≤ i)%Z →
vs !! ₊i = Some v →
{{{
sarray۰model t vs
}}}
sarray٠get t #i
{{{
RET v;
sarray۰model t vs
}}}.
Lemma sarray٠setｰspec t vs i v :
(0 ≤ i < length vs)%Z →
{{{
sarray۰model t vs ∗
τ v
}}}
sarray٠set t #i v
{{{
RET ();
sarray۰model t (<[₊i := v]> vs)
}}}.
Lemma sarray٠captureｰspec t vs :
{{{
sarray۰model t vs
}}}
sarray٠capture t
{{{
s
, RET s;
sarray۰model t vs ∗
sarray۰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 sarray٠restore₁ｰspec {γ nodes root vs_root node} vs :
{{{
model' γ nodes root vs_root ∗
nodes۰elem γ node vs
}}}
sarray٠restore₁ γ.(metadata۰data) #node
{{{
RET ();
restore۰inv γ nodes node vs
}}}.
Lemma sarray٠restoreｰspec t vs s vs' :
{{{
sarray۰model t vs ∗
sarray۰snapshot s t vs'
}}}
sarray٠restore t s
{{{
RET ();
sarray۰model t vs'
}}}.
End sarray۰G.
Require zoo_persistent.sarray__opaque.
#[global] Opaque sarray۰model.
#[global] Opaque sarray۰snapshot.