Library zoo_saturn.ws_bdeque_2
From zoo Require Import
prelude.
From zoo.common Require Import
countable
relations.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.auth_twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option.
From zoo_saturn Require Export
base
ws_bdeque_2__code.
From zoo_saturn Require Import
ws_bdeque_1.
From zoo Require Import
options.
Import ws_bdeque_1.base.
Implicit Types b : bool.
Implicit Types slot : location.
Implicit Types slots : list location.
Implicit Types v : val.
Implicit Types vs ws : list val.
Class WsBdeque2G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] ws_bdeque_2_G_base_G :: WsBdeque1G Σ
; #[local] ws_bdeque_2_G_model_G :: AuthTwinsG Σ (leibnizO (list val)) suffix
}.
Definition ws_bdeque_2_Σ :=
#[ws_bdeque_1_Σ
; auth_twins_Σ (leibnizO (list val)) suffix
].
#[global] Instance subG_ws_bdeque_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG ws_bdeque_2_Σ Σ →
WsBdeque2G Σ .
Module base.
Section ws_bdeque_2_G.
Context `{ws_bdeque_2_G : WsBdeque2G Σ}.
Implicit Types t : location.
Record ws_bdeque_2_name :=
{ ws_bdeque_2_name_capacity : nat
; ws_bdeque_2_name_base : ws_bdeque_1_name
; ws_bdeque_2_name_model : auth_twins_name
}.
Implicit Type γ : ws_bdeque_2_name.
#[global] Instance ws_bdeque_2_name_eq_dec : EqDecision ws_bdeque_2_name :=
ltac:(solve_decision).
#[global] Instance ws_bdeque_2_name_countable :
Countable ws_bdeque_2_name.
#[local] Definition model₁' γ_model vs :=
auth_twins_twin1 _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(ws_bdeque_2_name_model).
#[local] Definition model₂' γ_model vs :=
auth_twins_twin2 _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(ws_bdeque_2_name_model).
#[local] Definition owner' γ_owner ws :=
auth_twins_auth _ γ_owner ws.
#[local] Definition owner γ :=
owner' γ.(ws_bdeque_2_name_model).
#[local] Definition inv_inner γ : iProp Σ :=
∃ vs slots,
ws_bdeque_1_model γ.(ws_bdeque_2_name_base) (#*@{location} slots) ∗
model₂ γ vs ∗
[∗ list] slot; v ∈ slots; vs, slot ↦ᵣ v.
#[local] Instance : CustomIpat "inv_inner" :=
" ( %vs{} & %slots{} & >Hbase_model & >Hmodel₂ & >Hslots ) ".
Definition ws_bdeque_2_inv t γ ι cap : iProp Σ :=
⌜cap = γ.(ws_bdeque_2_name_capacity)⌝ ∗
ws_bdeque_1_inv t γ.(ws_bdeque_2_name_base) (ι.@"base") cap ∗
inv (ι.@"inv") (inv_inner γ).
#[local] Instance : CustomIpat "inv" :=
" ( -> & #Hbase_inv & #Hinv ) ".
Definition ws_bdeque_2_model γ vs : iProp Σ :=
model₁ γ vs ∗
⌜length vs ≤ γ.(ws_bdeque_2_name_capacity)⌝.
#[local] Instance : CustomIpat "model" :=
" ( Hmodel₁{_{}} & %Hvs{} ) ".
Definition ws_bdeque_2_owner t γ ws : iProp Σ :=
∃ slots_owner,
ws_bdeque_1_owner t γ.(ws_bdeque_2_name_base) (#*@{location} slots_owner) ∗
owner γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %slots_owner{_{}} & Hbase_owner{_{}} & Howner{_{}} ) ".
#[global] Instance ws_bdeque_2_model_timeless γ vs :
Timeless (ws_bdeque_2_model γ vs).
#[global] Instance ws_bdeque_2_owner_timeless t γ ws :
Timeless (ws_bdeque_2_owner t γ ws).
#[global] Instance ws_bdeque_2_inv_persistent t γ ι cap :
Persistent (ws_bdeque_2_inv t γ ι cap).
#[local] Lemma model_owner_alloc :
⊢ |==>
∃ γ_model,
model₁' γ_model [] ∗
model₂' γ_model [] ∗
owner' γ_model [].
#[local] Lemma model₁_valid γ ws vs :
owner γ ws -∗
model₁ γ vs -∗
⌜vs `suffix_of` ws⌝.
#[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_owner_agree γ ws vs1 vs2 :
owner γ ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 `suffix_of` ws⌝ ∗
⌜vs1 = vs2⌝.
#[local] Lemma model_push {γ ws vs1 vs2} v :
owner γ ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner γ (vs1 ++ [v]) ∗
model₁ γ (vs1 ++ [v]) ∗
model₂ γ (vs1 ++ [v]).
#[local] Lemma model_steal γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
model₁ γ (tail vs1) ∗
model₂ γ (tail vs1).
#[local] Lemma model_pop γ ws vs1 vs2 :
owner γ ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner γ (removelast vs1) ∗
model₁ γ (removelast vs1) ∗
model₂ γ (removelast vs1).
#[local] Lemma owner_update γ ws vs :
owner γ ws -∗
model₁ γ vs -∗
model₂ γ vs ==∗
owner γ vs ∗
model₁ γ vs ∗
model₂ γ vs.
#[local] Lemma owner_exclusive γ ws1 ws2 :
owner γ ws1 -∗
owner γ ws2 -∗
False.
Lemma ws_bdeque_2_model_valid t γ ι cap vs :
ws_bdeque_2_inv t γ ι cap -∗
ws_bdeque_2_model γ vs -∗
⌜length vs ≤ cap⌝.
Lemma ws_bdeque_2_model_exclusive γ vs1 vs2 :
ws_bdeque_2_model γ vs1 -∗
ws_bdeque_2_model γ vs2 -∗
False.
Lemma ws_bdeque_2_owner_exclusive t γ ws1 ws2 :
ws_bdeque_2_owner t γ ws1 -∗
ws_bdeque_2_owner t γ ws2 -∗
False.
Lemma ws_bdeque_2_owner_model t γ ws vs :
ws_bdeque_2_owner t γ ws -∗
ws_bdeque_2_model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_bdeque_2٠create𑁒spec ι (cap : Z) :
(0 < cap)%Z →
{{{
True
}}}
ws_bdeque_2٠create #cap
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
ws_bdeque_2_inv t γ ι ₊cap ∗
ws_bdeque_2_model γ [] ∗
ws_bdeque_2_owner t γ []
}}}.
Lemma ws_bdeque_2٠size𑁒spec t γ ι cap ws :
<<<
ws_bdeque_2_inv t γ ι cap ∗
ws_bdeque_2_owner t γ ws
| ∀∀ vs,
ws_bdeque_2_model γ vs
>>>
ws_bdeque_2٠size #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model γ vs
| RET #(length vs);
ws_bdeque_2_owner t γ vs
>>>.
Lemma ws_bdeque_2٠is_empty𑁒spec t γ ι cap ws :
<<<
ws_bdeque_2_inv t γ ι cap ∗
ws_bdeque_2_owner t γ ws
| ∀∀ vs,
ws_bdeque_2_model γ vs
>>>
ws_bdeque_2٠is_empty #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model γ vs
| RET #(bool_decide (vs = []%list));
ws_bdeque_2_owner t γ vs
>>>.
Lemma ws_bdeque_2٠push𑁒spec t γ ι cap ws v :
<<<
ws_bdeque_2_inv t γ ι cap ∗
ws_bdeque_2_owner t γ ws
| ∀∀ vs,
ws_bdeque_2_model γ vs
>>>
ws_bdeque_2٠push #t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model γ (if b then vs ++ [v] else vs)
| RET #b;
ws_bdeque_2_owner t γ (if b then vs ++ [v] else ws)
>>>.
Lemma ws_bdeque_2٠steal𑁒spec t γ ι cap :
<<<
ws_bdeque_2_inv t γ ι cap
| ∀∀ vs,
ws_bdeque_2_model γ vs
>>>
ws_bdeque_2٠steal #t @ ↑ι
<<<
ws_bdeque_2_model γ (tail vs)
| RET head vs;
True
>>>.
Lemma ws_bdeque_2٠pop𑁒spec t γ ι cap ws :
<<<
ws_bdeque_2_inv t γ ι cap ∗
ws_bdeque_2_owner t γ ws
| ∀∀ vs,
ws_bdeque_2_model γ vs
>>>
ws_bdeque_2٠pop #t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_bdeque_2_model γ []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_bdeque_2_model γ vs'
end
| RET o;
ws_bdeque_2_owner t γ ws'
>>>.
End ws_bdeque_2_G.
#[global] Opaque ws_bdeque_2_inv.
#[global] Opaque ws_bdeque_2_model.
#[global] Opaque ws_bdeque_2_owner.
End base.
From zoo_saturn Require
ws_bdeque_2__opaque.
Section ws_bdeque_2_G.
Context `{ws_bdeque_2_G : WsBdeque2G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition ws_bdeque_2_inv t ι cap : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_2_inv 𝑡 γ ι cap.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition ws_bdeque_2_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_2_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition ws_bdeque_2_owner t ws : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_2_owner 𝑡 γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Howner{_{}} ) ".
#[global] Instance ws_bdeque_2_model_timeless γ vs :
Timeless (ws_bdeque_2_model γ vs).
#[global] Instance ws_bdeque_2_owner_timeless γ ws :
Timeless (ws_bdeque_2_owner γ ws).
#[global] Instance ws_bdeque_2_inv_persistent t ι cap :
Persistent (ws_bdeque_2_inv t ι cap).
Lemma ws_bdeque_2_model_valid t ι cap vs :
ws_bdeque_2_inv t ι cap -∗
ws_bdeque_2_model t vs -∗
⌜length vs ≤ cap⌝.
Lemma ws_bdeque_2_model_exclusive t vs1 vs2 :
ws_bdeque_2_model t vs1 -∗
ws_bdeque_2_model t vs2 -∗
False.
Lemma ws_bdeque_2_owner_exclusive t ws1 ws2 :
ws_bdeque_2_owner t ws1 -∗
ws_bdeque_2_owner t ws2 -∗
False.
Lemma ws_bdeque_2_owner_model γ ws vs :
ws_bdeque_2_owner γ ws -∗
ws_bdeque_2_model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_bdeque_2٠create𑁒spec ι (cap : Z) :
(0 < cap)%Z →
{{{
True
}}}
ws_bdeque_2٠create #cap
{{{
t
, RET t;
ws_bdeque_2_inv t ι ₊cap ∗
ws_bdeque_2_model t [] ∗
ws_bdeque_2_owner t []
}}}.
Lemma ws_bdeque_2٠size𑁒spec t ι cap ws :
<<<
ws_bdeque_2_inv t ι cap ∗
ws_bdeque_2_owner t ws
| ∀∀ vs,
ws_bdeque_2_model t vs
>>>
ws_bdeque_2٠size t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model t vs
| RET #(length vs);
ws_bdeque_2_owner t vs
>>>.
Lemma ws_bdeque_2٠is_empty𑁒spec t ι cap ws :
<<<
ws_bdeque_2_inv t ι cap ∗
ws_bdeque_2_owner t ws
| ∀∀ vs,
ws_bdeque_2_model t vs
>>>
ws_bdeque_2٠is_empty t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model t vs
| RET #(bool_decide (vs = []%list));
ws_bdeque_2_owner t vs
>>>.
Lemma ws_bdeque_2٠push𑁒spec t ι cap ws v :
<<<
ws_bdeque_2_inv t ι cap ∗
ws_bdeque_2_owner t ws
| ∀∀ vs,
ws_bdeque_2_model t vs
>>>
ws_bdeque_2٠push t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model t (if b then vs ++ [v] else vs)
| RET #b;
ws_bdeque_2_owner t (if b then vs ++ [v] else ws)
>>>.
Lemma ws_bdeque_2٠steal𑁒spec t ι cap :
<<<
ws_bdeque_2_inv t ι cap
| ∀∀ vs,
ws_bdeque_2_model t vs
>>>
ws_bdeque_2٠steal t @ ↑ι
<<<
ws_bdeque_2_model t (tail vs)
| RET head vs;
True
>>>.
Lemma ws_bdeque_2٠pop𑁒spec t ι cap ws :
<<<
ws_bdeque_2_inv t ι cap ∗
ws_bdeque_2_owner t ws
| ∀∀ vs,
ws_bdeque_2_model t vs
>>>
ws_bdeque_2٠pop t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_bdeque_2_model t []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_bdeque_2_model t vs'
end
| RET o;
ws_bdeque_2_owner t ws'
>>>.
End ws_bdeque_2_G.
#[global] Opaque ws_bdeque_2_inv.
#[global] Opaque ws_bdeque_2_model.
#[global] Opaque ws_bdeque_2_owner.
prelude.
From zoo.common Require Import
countable
relations.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.auth_twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option.
From zoo_saturn Require Export
base
ws_bdeque_2__code.
From zoo_saturn Require Import
ws_bdeque_1.
From zoo Require Import
options.
Import ws_bdeque_1.base.
Implicit Types b : bool.
Implicit Types slot : location.
Implicit Types slots : list location.
Implicit Types v : val.
Implicit Types vs ws : list val.
Class WsBdeque2G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] ws_bdeque_2_G_base_G :: WsBdeque1G Σ
; #[local] ws_bdeque_2_G_model_G :: AuthTwinsG Σ (leibnizO (list val)) suffix
}.
Definition ws_bdeque_2_Σ :=
#[ws_bdeque_1_Σ
; auth_twins_Σ (leibnizO (list val)) suffix
].
#[global] Instance subG_ws_bdeque_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG ws_bdeque_2_Σ Σ →
WsBdeque2G Σ .
Module base.
Section ws_bdeque_2_G.
Context `{ws_bdeque_2_G : WsBdeque2G Σ}.
Implicit Types t : location.
Record ws_bdeque_2_name :=
{ ws_bdeque_2_name_capacity : nat
; ws_bdeque_2_name_base : ws_bdeque_1_name
; ws_bdeque_2_name_model : auth_twins_name
}.
Implicit Type γ : ws_bdeque_2_name.
#[global] Instance ws_bdeque_2_name_eq_dec : EqDecision ws_bdeque_2_name :=
ltac:(solve_decision).
#[global] Instance ws_bdeque_2_name_countable :
Countable ws_bdeque_2_name.
#[local] Definition model₁' γ_model vs :=
auth_twins_twin1 _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(ws_bdeque_2_name_model).
#[local] Definition model₂' γ_model vs :=
auth_twins_twin2 _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(ws_bdeque_2_name_model).
#[local] Definition owner' γ_owner ws :=
auth_twins_auth _ γ_owner ws.
#[local] Definition owner γ :=
owner' γ.(ws_bdeque_2_name_model).
#[local] Definition inv_inner γ : iProp Σ :=
∃ vs slots,
ws_bdeque_1_model γ.(ws_bdeque_2_name_base) (#*@{location} slots) ∗
model₂ γ vs ∗
[∗ list] slot; v ∈ slots; vs, slot ↦ᵣ v.
#[local] Instance : CustomIpat "inv_inner" :=
" ( %vs{} & %slots{} & >Hbase_model & >Hmodel₂ & >Hslots ) ".
Definition ws_bdeque_2_inv t γ ι cap : iProp Σ :=
⌜cap = γ.(ws_bdeque_2_name_capacity)⌝ ∗
ws_bdeque_1_inv t γ.(ws_bdeque_2_name_base) (ι.@"base") cap ∗
inv (ι.@"inv") (inv_inner γ).
#[local] Instance : CustomIpat "inv" :=
" ( -> & #Hbase_inv & #Hinv ) ".
Definition ws_bdeque_2_model γ vs : iProp Σ :=
model₁ γ vs ∗
⌜length vs ≤ γ.(ws_bdeque_2_name_capacity)⌝.
#[local] Instance : CustomIpat "model" :=
" ( Hmodel₁{_{}} & %Hvs{} ) ".
Definition ws_bdeque_2_owner t γ ws : iProp Σ :=
∃ slots_owner,
ws_bdeque_1_owner t γ.(ws_bdeque_2_name_base) (#*@{location} slots_owner) ∗
owner γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %slots_owner{_{}} & Hbase_owner{_{}} & Howner{_{}} ) ".
#[global] Instance ws_bdeque_2_model_timeless γ vs :
Timeless (ws_bdeque_2_model γ vs).
#[global] Instance ws_bdeque_2_owner_timeless t γ ws :
Timeless (ws_bdeque_2_owner t γ ws).
#[global] Instance ws_bdeque_2_inv_persistent t γ ι cap :
Persistent (ws_bdeque_2_inv t γ ι cap).
#[local] Lemma model_owner_alloc :
⊢ |==>
∃ γ_model,
model₁' γ_model [] ∗
model₂' γ_model [] ∗
owner' γ_model [].
#[local] Lemma model₁_valid γ ws vs :
owner γ ws -∗
model₁ γ vs -∗
⌜vs `suffix_of` ws⌝.
#[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_owner_agree γ ws vs1 vs2 :
owner γ ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 `suffix_of` ws⌝ ∗
⌜vs1 = vs2⌝.
#[local] Lemma model_push {γ ws vs1 vs2} v :
owner γ ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner γ (vs1 ++ [v]) ∗
model₁ γ (vs1 ++ [v]) ∗
model₂ γ (vs1 ++ [v]).
#[local] Lemma model_steal γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
model₁ γ (tail vs1) ∗
model₂ γ (tail vs1).
#[local] Lemma model_pop γ ws vs1 vs2 :
owner γ ws -∗
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
owner γ (removelast vs1) ∗
model₁ γ (removelast vs1) ∗
model₂ γ (removelast vs1).
#[local] Lemma owner_update γ ws vs :
owner γ ws -∗
model₁ γ vs -∗
model₂ γ vs ==∗
owner γ vs ∗
model₁ γ vs ∗
model₂ γ vs.
#[local] Lemma owner_exclusive γ ws1 ws2 :
owner γ ws1 -∗
owner γ ws2 -∗
False.
Lemma ws_bdeque_2_model_valid t γ ι cap vs :
ws_bdeque_2_inv t γ ι cap -∗
ws_bdeque_2_model γ vs -∗
⌜length vs ≤ cap⌝.
Lemma ws_bdeque_2_model_exclusive γ vs1 vs2 :
ws_bdeque_2_model γ vs1 -∗
ws_bdeque_2_model γ vs2 -∗
False.
Lemma ws_bdeque_2_owner_exclusive t γ ws1 ws2 :
ws_bdeque_2_owner t γ ws1 -∗
ws_bdeque_2_owner t γ ws2 -∗
False.
Lemma ws_bdeque_2_owner_model t γ ws vs :
ws_bdeque_2_owner t γ ws -∗
ws_bdeque_2_model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_bdeque_2٠create𑁒spec ι (cap : Z) :
(0 < cap)%Z →
{{{
True
}}}
ws_bdeque_2٠create #cap
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
ws_bdeque_2_inv t γ ι ₊cap ∗
ws_bdeque_2_model γ [] ∗
ws_bdeque_2_owner t γ []
}}}.
Lemma ws_bdeque_2٠size𑁒spec t γ ι cap ws :
<<<
ws_bdeque_2_inv t γ ι cap ∗
ws_bdeque_2_owner t γ ws
| ∀∀ vs,
ws_bdeque_2_model γ vs
>>>
ws_bdeque_2٠size #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model γ vs
| RET #(length vs);
ws_bdeque_2_owner t γ vs
>>>.
Lemma ws_bdeque_2٠is_empty𑁒spec t γ ι cap ws :
<<<
ws_bdeque_2_inv t γ ι cap ∗
ws_bdeque_2_owner t γ ws
| ∀∀ vs,
ws_bdeque_2_model γ vs
>>>
ws_bdeque_2٠is_empty #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model γ vs
| RET #(bool_decide (vs = []%list));
ws_bdeque_2_owner t γ vs
>>>.
Lemma ws_bdeque_2٠push𑁒spec t γ ι cap ws v :
<<<
ws_bdeque_2_inv t γ ι cap ∗
ws_bdeque_2_owner t γ ws
| ∀∀ vs,
ws_bdeque_2_model γ vs
>>>
ws_bdeque_2٠push #t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model γ (if b then vs ++ [v] else vs)
| RET #b;
ws_bdeque_2_owner t γ (if b then vs ++ [v] else ws)
>>>.
Lemma ws_bdeque_2٠steal𑁒spec t γ ι cap :
<<<
ws_bdeque_2_inv t γ ι cap
| ∀∀ vs,
ws_bdeque_2_model γ vs
>>>
ws_bdeque_2٠steal #t @ ↑ι
<<<
ws_bdeque_2_model γ (tail vs)
| RET head vs;
True
>>>.
Lemma ws_bdeque_2٠pop𑁒spec t γ ι cap ws :
<<<
ws_bdeque_2_inv t γ ι cap ∗
ws_bdeque_2_owner t γ ws
| ∀∀ vs,
ws_bdeque_2_model γ vs
>>>
ws_bdeque_2٠pop #t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_bdeque_2_model γ []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_bdeque_2_model γ vs'
end
| RET o;
ws_bdeque_2_owner t γ ws'
>>>.
End ws_bdeque_2_G.
#[global] Opaque ws_bdeque_2_inv.
#[global] Opaque ws_bdeque_2_model.
#[global] Opaque ws_bdeque_2_owner.
End base.
From zoo_saturn Require
ws_bdeque_2__opaque.
Section ws_bdeque_2_G.
Context `{ws_bdeque_2_G : WsBdeque2G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition ws_bdeque_2_inv t ι cap : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_2_inv 𝑡 γ ι cap.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition ws_bdeque_2_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_2_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition ws_bdeque_2_owner t ws : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.ws_bdeque_2_owner 𝑡 γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Howner{_{}} ) ".
#[global] Instance ws_bdeque_2_model_timeless γ vs :
Timeless (ws_bdeque_2_model γ vs).
#[global] Instance ws_bdeque_2_owner_timeless γ ws :
Timeless (ws_bdeque_2_owner γ ws).
#[global] Instance ws_bdeque_2_inv_persistent t ι cap :
Persistent (ws_bdeque_2_inv t ι cap).
Lemma ws_bdeque_2_model_valid t ι cap vs :
ws_bdeque_2_inv t ι cap -∗
ws_bdeque_2_model t vs -∗
⌜length vs ≤ cap⌝.
Lemma ws_bdeque_2_model_exclusive t vs1 vs2 :
ws_bdeque_2_model t vs1 -∗
ws_bdeque_2_model t vs2 -∗
False.
Lemma ws_bdeque_2_owner_exclusive t ws1 ws2 :
ws_bdeque_2_owner t ws1 -∗
ws_bdeque_2_owner t ws2 -∗
False.
Lemma ws_bdeque_2_owner_model γ ws vs :
ws_bdeque_2_owner γ ws -∗
ws_bdeque_2_model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_bdeque_2٠create𑁒spec ι (cap : Z) :
(0 < cap)%Z →
{{{
True
}}}
ws_bdeque_2٠create #cap
{{{
t
, RET t;
ws_bdeque_2_inv t ι ₊cap ∗
ws_bdeque_2_model t [] ∗
ws_bdeque_2_owner t []
}}}.
Lemma ws_bdeque_2٠size𑁒spec t ι cap ws :
<<<
ws_bdeque_2_inv t ι cap ∗
ws_bdeque_2_owner t ws
| ∀∀ vs,
ws_bdeque_2_model t vs
>>>
ws_bdeque_2٠size t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model t vs
| RET #(length vs);
ws_bdeque_2_owner t vs
>>>.
Lemma ws_bdeque_2٠is_empty𑁒spec t ι cap ws :
<<<
ws_bdeque_2_inv t ι cap ∗
ws_bdeque_2_owner t ws
| ∀∀ vs,
ws_bdeque_2_model t vs
>>>
ws_bdeque_2٠is_empty t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model t vs
| RET #(bool_decide (vs = []%list));
ws_bdeque_2_owner t vs
>>>.
Lemma ws_bdeque_2٠push𑁒spec t ι cap ws v :
<<<
ws_bdeque_2_inv t ι cap ∗
ws_bdeque_2_owner t ws
| ∀∀ vs,
ws_bdeque_2_model t vs
>>>
ws_bdeque_2٠push t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_bdeque_2_model t (if b then vs ++ [v] else vs)
| RET #b;
ws_bdeque_2_owner t (if b then vs ++ [v] else ws)
>>>.
Lemma ws_bdeque_2٠steal𑁒spec t ι cap :
<<<
ws_bdeque_2_inv t ι cap
| ∀∀ vs,
ws_bdeque_2_model t vs
>>>
ws_bdeque_2٠steal t @ ↑ι
<<<
ws_bdeque_2_model t (tail vs)
| RET head vs;
True
>>>.
Lemma ws_bdeque_2٠pop𑁒spec t ι cap ws :
<<<
ws_bdeque_2_inv t ι cap ∗
ws_bdeque_2_owner t ws
| ∀∀ vs,
ws_bdeque_2_model t vs
>>>
ws_bdeque_2٠pop t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_bdeque_2_model t []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_bdeque_2_model t vs'
end
| RET o;
ws_bdeque_2_owner t ws'
>>>.
End ws_bdeque_2_G.
#[global] Opaque ws_bdeque_2_inv.
#[global] Opaque ws_bdeque_2_model.
#[global] Opaque ws_bdeque_2_owner.