Library zoo_saturn.bag_1
From zoo Require Import
prelude.
From zoo.common Require Import
countable
gmultiset
list.
From zoo.iris.base_logic Require Import
lib.twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
goption
array.
From zoo_saturn Require Export
base
bag_1__code.
From zoo_saturn Require Import
bag_1__types.
From zoo Require Import
options.
Implicit Types front back : nat.
Implicit Types l slot : location.
Implicit Types slots : list location.
Implicit Types v t data : val.
Implicit Types vs : gmultiset val.
Implicit Types o : option val.
Implicit Types os : list (option val).
Class Bag1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] bag_1_G_model_G :: TwinsG Σ (leibnizO (gmultiset val))
}.
Definition bag_1_Σ :=
#[twins_Σ (leibnizO (gmultiset val))
].
#[global] Instance subG_bag_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG bag_1_Σ Σ →
Bag1G Σ.
#[local] Definition consistent vs os :=
vs = ⋃+ (singletonMS <$> oflatten os).
#[local] Lemma consistent_lookup vs os i v :
os !! i = Some $ Some v →
consistent vs os →
v ∈ vs.
#[local] Lemma consistent_insert {vs os i} v :
os !! i = Some None →
consistent vs os →
consistent ({[+v+]} ⊎ vs) (<[i := Some v]> os).
#[local] Lemma consistent_remove vs os i v :
os !! i = Some $ Some v →
consistent vs os →
consistent (vs ∖ {[+v+]}) (<[i := None]> os).
Opaque consistent.
Section bag_1_G.
Context `{bag_1_G : Bag1G Σ}.
Record metadata :=
{ metadata_data : val
; metadata_slots : list location
; metadata_inv : namespace
; metadata_model : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ vs :=
model₁' γ.(metadata_model) vs.
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ vs :=
model₂' γ.(metadata_model) vs.
#[local] Definition inv_inner l γ : iProp Σ :=
∃ front back vs os,
l.[front] ↦ #front ∗
l.[back] ↦ #back ∗
model₂ γ vs ∗
⌜consistent vs os⌝ ∗
[∗ list] slot; o ∈ γ.(metadata_slots); os,
slot ↦ᵣ (o : val).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %front & %back & %vs & %os & Hfront & Hback & Hmodel₂ & >%Hconsistent & Hslots ) ".
#[local] Definition inv' l γ :=
inv γ.(metadata_inv) (inv_inner l γ).
Definition bag_1_inv t ι : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
⌜ι = γ.(metadata_inv)⌝ ∗
⌜0 < length γ.(metadata_slots)⌝ ∗
meta l nroot γ ∗
l.[data] ↦□ γ.(metadata_data) ∗
array_model γ.(metadata_data) DfracDiscarded (#*@{location} γ.(metadata_slots)) ∗
inv' l γ.
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & -> & -> & %Hsz & #Hmeta & #Hdata & #Hdata_model & #Hinv ) ".
Definition bag_1_model t vs : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
model₁ γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Hmodel₁{_{}} ) ".
#[global] Instance bag_1_inv_timeless t vs :
Timeless (bag_1_model t vs).
#[global] Instance bag_1_inv_persistent t ι :
Persistent (bag_1_inv t ι).
#[local] Lemma model_alloc :
⊢ |==>
∃ γ_model,
model₁' γ_model ∅ ∗
model₂' γ_model ∅.
#[local] Lemma model₁_exclusive γ vs1 vs2 :
model₁ γ vs1 -∗
model₁ γ vs2 -∗
False.
#[local] Lemma model_agree γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma model_update {γ vs1 vs2} vs :
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
model₁ γ vs ∗
model₂ γ vs.
Lemma bag_1_model_exclusive t vs1 vs2 :
bag_1_model t vs1 -∗
bag_1_model t vs2 -∗
False.
Lemma bag_1٠create𑁒spec ι (sz : Z) :
(0 < sz)%Z →
{{{
True
}}}
bag_1٠create #sz
{{{
t
, RET t;
bag_1_inv t ι ∗
bag_1_model t ∅
}}}.
#[local] Lemma bag_1٠push₀𑁒spec slot v l γ :
slot ∈ γ.(metadata_slots) →
<<<
meta l nroot γ ∗
inv' l γ
| ∀∀ vs,
bag_1_model #l vs
>>>
bag_1٠push₀ #slot ’Some[ v ] @ ↑γ.(metadata_inv)
<<<
bag_1_model #l ({[+v+]} ⊎ vs)
| RET ();
True
>>>.
Lemma bag_1٠push𑁒spec t ι v :
<<<
bag_1_inv t ι
| ∀∀ vs,
bag_1_model t vs
>>>
bag_1٠push t v @ ↑ι
<<<
bag_1_model t ({[+v+]} ⊎ vs)
| RET ();
True
>>>.
#[local] Lemma bag_1٠pop₀𑁒spec slot l γ :
slot ∈ γ.(metadata_slots) →
<<<
meta l nroot γ ∗
inv' l γ
| ∀∀ vs,
bag_1_model #l vs
>>>
bag_1٠pop₀ #slot @ ↑γ.(metadata_inv)
<<<
∃∃ v vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
bag_1_model #l vs'
| RET v;
True
>>>.
Lemma bag_1٠pop𑁒spec t ι :
<<<
bag_1_inv t ι
| ∀∀ vs,
bag_1_model t vs
>>>
bag_1٠pop t @ ↑ι
<<<
∃∃ v vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
bag_1_model t vs'
| RET v;
True
>>>.
End bag_1_G.
From zoo_saturn Require
bag_1__opaque.
#[global] Opaque bag_1_inv.
#[global] Opaque bag_1_model.
prelude.
From zoo.common Require Import
countable
gmultiset
list.
From zoo.iris.base_logic Require Import
lib.twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
goption
array.
From zoo_saturn Require Export
base
bag_1__code.
From zoo_saturn Require Import
bag_1__types.
From zoo Require Import
options.
Implicit Types front back : nat.
Implicit Types l slot : location.
Implicit Types slots : list location.
Implicit Types v t data : val.
Implicit Types vs : gmultiset val.
Implicit Types o : option val.
Implicit Types os : list (option val).
Class Bag1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] bag_1_G_model_G :: TwinsG Σ (leibnizO (gmultiset val))
}.
Definition bag_1_Σ :=
#[twins_Σ (leibnizO (gmultiset val))
].
#[global] Instance subG_bag_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG bag_1_Σ Σ →
Bag1G Σ.
#[local] Definition consistent vs os :=
vs = ⋃+ (singletonMS <$> oflatten os).
#[local] Lemma consistent_lookup vs os i v :
os !! i = Some $ Some v →
consistent vs os →
v ∈ vs.
#[local] Lemma consistent_insert {vs os i} v :
os !! i = Some None →
consistent vs os →
consistent ({[+v+]} ⊎ vs) (<[i := Some v]> os).
#[local] Lemma consistent_remove vs os i v :
os !! i = Some $ Some v →
consistent vs os →
consistent (vs ∖ {[+v+]}) (<[i := None]> os).
Opaque consistent.
Section bag_1_G.
Context `{bag_1_G : Bag1G Σ}.
Record metadata :=
{ metadata_data : val
; metadata_slots : list location
; metadata_inv : namespace
; metadata_model : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ vs :=
model₁' γ.(metadata_model) vs.
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ vs :=
model₂' γ.(metadata_model) vs.
#[local] Definition inv_inner l γ : iProp Σ :=
∃ front back vs os,
l.[front] ↦ #front ∗
l.[back] ↦ #back ∗
model₂ γ vs ∗
⌜consistent vs os⌝ ∗
[∗ list] slot; o ∈ γ.(metadata_slots); os,
slot ↦ᵣ (o : val).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %front & %back & %vs & %os & Hfront & Hback & Hmodel₂ & >%Hconsistent & Hslots ) ".
#[local] Definition inv' l γ :=
inv γ.(metadata_inv) (inv_inner l γ).
Definition bag_1_inv t ι : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
⌜ι = γ.(metadata_inv)⌝ ∗
⌜0 < length γ.(metadata_slots)⌝ ∗
meta l nroot γ ∗
l.[data] ↦□ γ.(metadata_data) ∗
array_model γ.(metadata_data) DfracDiscarded (#*@{location} γ.(metadata_slots)) ∗
inv' l γ.
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & -> & -> & %Hsz & #Hmeta & #Hdata & #Hdata_model & #Hinv ) ".
Definition bag_1_model t vs : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
model₁ γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Hmodel₁{_{}} ) ".
#[global] Instance bag_1_inv_timeless t vs :
Timeless (bag_1_model t vs).
#[global] Instance bag_1_inv_persistent t ι :
Persistent (bag_1_inv t ι).
#[local] Lemma model_alloc :
⊢ |==>
∃ γ_model,
model₁' γ_model ∅ ∗
model₂' γ_model ∅.
#[local] Lemma model₁_exclusive γ vs1 vs2 :
model₁ γ vs1 -∗
model₁ γ vs2 -∗
False.
#[local] Lemma model_agree γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma model_update {γ vs1 vs2} vs :
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
model₁ γ vs ∗
model₂ γ vs.
Lemma bag_1_model_exclusive t vs1 vs2 :
bag_1_model t vs1 -∗
bag_1_model t vs2 -∗
False.
Lemma bag_1٠create𑁒spec ι (sz : Z) :
(0 < sz)%Z →
{{{
True
}}}
bag_1٠create #sz
{{{
t
, RET t;
bag_1_inv t ι ∗
bag_1_model t ∅
}}}.
#[local] Lemma bag_1٠push₀𑁒spec slot v l γ :
slot ∈ γ.(metadata_slots) →
<<<
meta l nroot γ ∗
inv' l γ
| ∀∀ vs,
bag_1_model #l vs
>>>
bag_1٠push₀ #slot ’Some[ v ] @ ↑γ.(metadata_inv)
<<<
bag_1_model #l ({[+v+]} ⊎ vs)
| RET ();
True
>>>.
Lemma bag_1٠push𑁒spec t ι v :
<<<
bag_1_inv t ι
| ∀∀ vs,
bag_1_model t vs
>>>
bag_1٠push t v @ ↑ι
<<<
bag_1_model t ({[+v+]} ⊎ vs)
| RET ();
True
>>>.
#[local] Lemma bag_1٠pop₀𑁒spec slot l γ :
slot ∈ γ.(metadata_slots) →
<<<
meta l nroot γ ∗
inv' l γ
| ∀∀ vs,
bag_1_model #l vs
>>>
bag_1٠pop₀ #slot @ ↑γ.(metadata_inv)
<<<
∃∃ v vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
bag_1_model #l vs'
| RET v;
True
>>>.
Lemma bag_1٠pop𑁒spec t ι :
<<<
bag_1_inv t ι
| ∀∀ vs,
bag_1_model t vs
>>>
bag_1٠pop t @ ↑ι
<<<
∃∃ v vs',
⌜vs = {[+v+]} ⊎ vs'⌝ ∗
bag_1_model t vs'
| RET v;
True
>>>.
End bag_1_G.
From zoo_saturn Require
bag_1__opaque.
#[global] Opaque bag_1_inv.
#[global] Opaque bag_1_model.