Library zoo_saturn.ws_deque_2
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.relations.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.auth_twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_saturn.ws_deque_2__code.
Require Import zoo_saturn.ws_deque_2__types.
Require Import zoo.options.
Import ws_deque_1.base.
Implicit Type slot : location.
Implicit Type slots : list location.
Implicit Type v : val.
Implicit Type vs ws : list val.
Class WsDeque2G Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ws_deque_2۰G۰base۰G :: WsDeque1G Σ
; #[local] ws_deque_2۰G۰model۰G :: AuthTwinsG Σ (leibnizO (list val)) suffix
}.
Definition ws_deque_2۰Σ :=
#[ws_deque_1۰Σ
; auth_twins۰Σ (leibnizO (list val)) suffix
].
#[global] Instance subGｰws_deque_2۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ws_deque_2۰Σ Σ →
WsDeque2G Σ .
Module base.
Section ws_deque_2۰G.
Context `{ws_deque_2۰G : WsDeque2G Σ}.
Implicit Type t : location.
Record ws_deque_2۰name :=
{ ws_deque_2۰name۰base : ws_deque_1۰name
; ws_deque_2۰name۰model : auth_twins۰name
}.
Implicit Type γ : ws_deque_2۰name.
#[global] Instance ws_deque_2۰nameｰeq_dec : EqDecision ws_deque_2۰name :=
ltac:(solve_decision).
#[global] Instance ws_deque_2۰nameｰcountable :
Countable ws_deque_2۰name.
#[local] Definition model₁' γ_model vs :=
auth_twins۰twin₁ _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(ws_deque_2۰name۰model).
#[local] Definition model₂' γ_model vs :=
auth_twins۰twin₂ _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(ws_deque_2۰name۰model).
#[local] Definition owner' γ_owner ws :=
auth_twins۰auth _ γ_owner ws.
#[local] Definition owner γ :=
owner' γ.(ws_deque_2۰name۰model).
#[local] Definition inv۰inner γ : iProp Σ :=
∃ vs slots,
ws_deque_1۰model γ.(ws_deque_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_deque_2۰inv t γ ι : iProp Σ :=
ws_deque_1۰inv t γ.(ws_deque_2۰name۰base) (ι.@"base") ∗
inv (ι.@"inv") (inv۰inner γ).
#[local] Instance : CustomIpat "inv" :=
" ( #Hbase_inv & #Hinv ) ".
Definition ws_deque_2۰model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
Definition ws_deque_2۰owner γ ws : iProp Σ :=
∃ slots_owner,
ws_deque_1۰owner γ.(ws_deque_2۰name۰base) (#*@{location} slots_owner) ∗
owner γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %slots_owner{_{}} & Hbase_owner{_{}} & Howner{_{}} ) ".
#[global] Instance ws_deque_2۰modelｰtimeless γ vs :
Timeless (ws_deque_2۰model γ vs).
#[global] Instance ws_deque_2۰ownerｰtimeless γ ws :
Timeless (ws_deque_2۰owner γ ws).
#[global] Instance ws_deque_2۰invｰpersistent t γ ι :
Persistent (ws_deque_2۰inv t γ ι).
#[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_deque_2۰modelｰexclusive γ vs1 vs2 :
ws_deque_2۰model γ vs1 -∗
ws_deque_2۰model γ vs2 -∗
False.
Lemma ws_deque_2۰ownerｰexclusive γ ws1 ws2 :
ws_deque_2۰owner γ ws1 -∗
ws_deque_2۰owner γ ws2 -∗
False.
Lemma ws_deque_2ｰownerｰmodel γ ws vs :
ws_deque_2۰owner γ ws -∗
ws_deque_2۰model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_deque_2٠createｰspec ι :
{{{
True
}}}
ws_deque_2٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
ws_deque_2۰inv t γ ι ∗
ws_deque_2۰model γ [] ∗
ws_deque_2۰owner γ []
}}}.
Lemma ws_deque_2٠sizeｰspec t γ ι ws :
<<<
ws_deque_2۰inv t γ ι ∗
ws_deque_2۰owner γ ws
| ∀∀ vs,
ws_deque_2۰model γ vs
>>>
ws_deque_2٠size #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model γ vs
| RET #(length vs);
ws_deque_2۰owner γ vs
>>>.
Lemma ws_deque_2٠is_emptyｰspec t γ ι ws :
<<<
ws_deque_2۰inv t γ ι ∗
ws_deque_2۰owner γ ws
| ∀∀ vs,
ws_deque_2۰model γ vs
>>>
ws_deque_2٠is_empty #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model γ vs
| RET #(bool_decide (vs = []%list));
ws_deque_2۰owner γ vs
>>>.
Lemma ws_deque_2٠pushｰspec t γ ι ws v :
<<<
ws_deque_2۰inv t γ ι ∗
ws_deque_2۰owner γ ws
| ∀∀ vs,
ws_deque_2۰model γ vs
>>>
ws_deque_2٠push #t v @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model γ (vs ++ [v])
| RET ();
ws_deque_2۰owner γ (vs ++ [v])
>>>.
Lemma ws_deque_2٠stealｰspec t γ ι :
<<<
ws_deque_2۰inv t γ ι
| ∀∀ vs,
ws_deque_2۰model γ vs
>>>
ws_deque_2٠steal #t @ ↑ι
<<<
ws_deque_2۰model γ (tail vs)
| RET head vs;
True
>>>.
Lemma ws_deque_2٠popｰspec t γ ι ws :
<<<
ws_deque_2۰inv t γ ι ∗
ws_deque_2۰owner γ ws
| ∀∀ vs,
ws_deque_2۰model γ vs
>>>
ws_deque_2٠pop #t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_deque_2۰model γ []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_deque_2۰model γ vs'
end
| RET o;
ws_deque_2۰owner γ ws'
>>>.
End ws_deque_2۰G.
#[global] Opaque ws_deque_2۰inv.
#[global] Opaque ws_deque_2۰model.
#[global] Opaque ws_deque_2۰owner.
End base.
Require zoo_saturn.ws_deque_2__opaque.
Section ws_deque_2۰G.
Context `{ws_deque_2۰G : WsDeque2G Σ}.
Implicit Type 𝑡 : location.
Implicit Type t : val.
Definition ws_deque_2۰inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_2۰inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition ws_deque_2۰model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_2۰model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition ws_deque_2۰owner t ws : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_2۰owner γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Howner{_{}} ) ".
#[global] Instance ws_deque_2۰modelｰtimeless γ vs :
Timeless (ws_deque_2۰model γ vs).
#[global] Instance ws_deque_2۰ownerｰtimeless γ ws :
Timeless (ws_deque_2۰owner γ ws).
#[global] Instance ws_deque_2۰invｰpersistent t ι :
Persistent (ws_deque_2۰inv t ι).
Lemma ws_deque_2۰modelｰexclusive t vs1 vs2 :
ws_deque_2۰model t vs1 -∗
ws_deque_2۰model t vs2 -∗
False.
Lemma ws_deque_2۰ownerｰexclusive t ws1 ws2 :
ws_deque_2۰owner t ws1 -∗
ws_deque_2۰owner t ws2 -∗
False.
Lemma ws_deque_2ｰownerｰmodel γ ws vs :
ws_deque_2۰owner γ ws -∗
ws_deque_2۰model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_deque_2٠createｰspec ι :
{{{
True
}}}
ws_deque_2٠create ()
{{{
t
, RET t;
ws_deque_2۰inv t ι ∗
ws_deque_2۰model t [] ∗
ws_deque_2۰owner t []
}}}.
Lemma ws_deque_2٠sizeｰspec t ι ws :
<<<
ws_deque_2۰inv t ι ∗
ws_deque_2۰owner t ws
| ∀∀ vs,
ws_deque_2۰model t vs
>>>
ws_deque_2٠size t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model t vs
| RET #(length vs);
ws_deque_2۰owner t vs
>>>.
Lemma ws_deque_2٠is_emptyｰspec t ι ws :
<<<
ws_deque_2۰inv t ι ∗
ws_deque_2۰owner t ws
| ∀∀ vs,
ws_deque_2۰model t vs
>>>
ws_deque_2٠is_empty t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model t vs
| RET #(bool_decide (vs = []%list));
ws_deque_2۰owner t vs
>>>.
Lemma ws_deque_2٠pushｰspec t ι ws v :
<<<
ws_deque_2۰inv t ι ∗
ws_deque_2۰owner t ws
| ∀∀ vs,
ws_deque_2۰model t vs
>>>
ws_deque_2٠push t v @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model t (vs ++ [v])
| RET ();
ws_deque_2۰owner t (vs ++ [v])
>>>.
Lemma ws_deque_2٠stealｰspec t ι :
<<<
ws_deque_2۰inv t ι
| ∀∀ vs,
ws_deque_2۰model t vs
>>>
ws_deque_2٠steal t @ ↑ι
<<<
ws_deque_2۰model t (tail vs)
| RET head vs;
True
>>>.
Lemma ws_deque_2٠popｰspec t ι ws :
<<<
ws_deque_2۰inv t ι ∗
ws_deque_2۰owner t ws
| ∀∀ vs,
ws_deque_2۰model t vs
>>>
ws_deque_2٠pop t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_deque_2۰model t []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_deque_2۰model t vs'
end
| RET o;
ws_deque_2۰owner t ws'
>>>.
End ws_deque_2۰G.
#[global] Opaque ws_deque_2۰inv.
#[global] Opaque ws_deque_2۰model.
#[global] Opaque ws_deque_2۰owner.
Require Import zoo.common.countable.
Require Import zoo.common.relations.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.auth_twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_saturn.ws_deque_2__code.
Require Import zoo_saturn.ws_deque_2__types.
Require Import zoo.options.
Import ws_deque_1.base.
Implicit Type slot : location.
Implicit Type slots : list location.
Implicit Type v : val.
Implicit Type vs ws : list val.
Class WsDeque2G Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ws_deque_2۰G۰base۰G :: WsDeque1G Σ
; #[local] ws_deque_2۰G۰model۰G :: AuthTwinsG Σ (leibnizO (list val)) suffix
}.
Definition ws_deque_2۰Σ :=
#[ws_deque_1۰Σ
; auth_twins۰Σ (leibnizO (list val)) suffix
].
#[global] Instance subGｰws_deque_2۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ws_deque_2۰Σ Σ →
WsDeque2G Σ .
Module base.
Section ws_deque_2۰G.
Context `{ws_deque_2۰G : WsDeque2G Σ}.
Implicit Type t : location.
Record ws_deque_2۰name :=
{ ws_deque_2۰name۰base : ws_deque_1۰name
; ws_deque_2۰name۰model : auth_twins۰name
}.
Implicit Type γ : ws_deque_2۰name.
#[global] Instance ws_deque_2۰nameｰeq_dec : EqDecision ws_deque_2۰name :=
ltac:(solve_decision).
#[global] Instance ws_deque_2۰nameｰcountable :
Countable ws_deque_2۰name.
#[local] Definition model₁' γ_model vs :=
auth_twins۰twin₁ _ γ_model vs.
#[local] Definition model₁ γ :=
model₁' γ.(ws_deque_2۰name۰model).
#[local] Definition model₂' γ_model vs :=
auth_twins۰twin₂ _ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(ws_deque_2۰name۰model).
#[local] Definition owner' γ_owner ws :=
auth_twins۰auth _ γ_owner ws.
#[local] Definition owner γ :=
owner' γ.(ws_deque_2۰name۰model).
#[local] Definition inv۰inner γ : iProp Σ :=
∃ vs slots,
ws_deque_1۰model γ.(ws_deque_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_deque_2۰inv t γ ι : iProp Σ :=
ws_deque_1۰inv t γ.(ws_deque_2۰name۰base) (ι.@"base") ∗
inv (ι.@"inv") (inv۰inner γ).
#[local] Instance : CustomIpat "inv" :=
" ( #Hbase_inv & #Hinv ) ".
Definition ws_deque_2۰model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
Definition ws_deque_2۰owner γ ws : iProp Σ :=
∃ slots_owner,
ws_deque_1۰owner γ.(ws_deque_2۰name۰base) (#*@{location} slots_owner) ∗
owner γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %slots_owner{_{}} & Hbase_owner{_{}} & Howner{_{}} ) ".
#[global] Instance ws_deque_2۰modelｰtimeless γ vs :
Timeless (ws_deque_2۰model γ vs).
#[global] Instance ws_deque_2۰ownerｰtimeless γ ws :
Timeless (ws_deque_2۰owner γ ws).
#[global] Instance ws_deque_2۰invｰpersistent t γ ι :
Persistent (ws_deque_2۰inv t γ ι).
#[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_deque_2۰modelｰexclusive γ vs1 vs2 :
ws_deque_2۰model γ vs1 -∗
ws_deque_2۰model γ vs2 -∗
False.
Lemma ws_deque_2۰ownerｰexclusive γ ws1 ws2 :
ws_deque_2۰owner γ ws1 -∗
ws_deque_2۰owner γ ws2 -∗
False.
Lemma ws_deque_2ｰownerｰmodel γ ws vs :
ws_deque_2۰owner γ ws -∗
ws_deque_2۰model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_deque_2٠createｰspec ι :
{{{
True
}}}
ws_deque_2٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
ws_deque_2۰inv t γ ι ∗
ws_deque_2۰model γ [] ∗
ws_deque_2۰owner γ []
}}}.
Lemma ws_deque_2٠sizeｰspec t γ ι ws :
<<<
ws_deque_2۰inv t γ ι ∗
ws_deque_2۰owner γ ws
| ∀∀ vs,
ws_deque_2۰model γ vs
>>>
ws_deque_2٠size #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model γ vs
| RET #(length vs);
ws_deque_2۰owner γ vs
>>>.
Lemma ws_deque_2٠is_emptyｰspec t γ ι ws :
<<<
ws_deque_2۰inv t γ ι ∗
ws_deque_2۰owner γ ws
| ∀∀ vs,
ws_deque_2۰model γ vs
>>>
ws_deque_2٠is_empty #t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model γ vs
| RET #(bool_decide (vs = []%list));
ws_deque_2۰owner γ vs
>>>.
Lemma ws_deque_2٠pushｰspec t γ ι ws v :
<<<
ws_deque_2۰inv t γ ι ∗
ws_deque_2۰owner γ ws
| ∀∀ vs,
ws_deque_2۰model γ vs
>>>
ws_deque_2٠push #t v @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model γ (vs ++ [v])
| RET ();
ws_deque_2۰owner γ (vs ++ [v])
>>>.
Lemma ws_deque_2٠stealｰspec t γ ι :
<<<
ws_deque_2۰inv t γ ι
| ∀∀ vs,
ws_deque_2۰model γ vs
>>>
ws_deque_2٠steal #t @ ↑ι
<<<
ws_deque_2۰model γ (tail vs)
| RET head vs;
True
>>>.
Lemma ws_deque_2٠popｰspec t γ ι ws :
<<<
ws_deque_2۰inv t γ ι ∗
ws_deque_2۰owner γ ws
| ∀∀ vs,
ws_deque_2۰model γ vs
>>>
ws_deque_2٠pop #t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_deque_2۰model γ []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_deque_2۰model γ vs'
end
| RET o;
ws_deque_2۰owner γ ws'
>>>.
End ws_deque_2۰G.
#[global] Opaque ws_deque_2۰inv.
#[global] Opaque ws_deque_2۰model.
#[global] Opaque ws_deque_2۰owner.
End base.
Require zoo_saturn.ws_deque_2__opaque.
Section ws_deque_2۰G.
Context `{ws_deque_2۰G : WsDeque2G Σ}.
Implicit Type 𝑡 : location.
Implicit Type t : val.
Definition ws_deque_2۰inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_2۰inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition ws_deque_2۰model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_2۰model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition ws_deque_2۰owner t ws : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.ws_deque_2۰owner γ ws.
#[local] Instance : CustomIpat "owner" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Howner{_{}} ) ".
#[global] Instance ws_deque_2۰modelｰtimeless γ vs :
Timeless (ws_deque_2۰model γ vs).
#[global] Instance ws_deque_2۰ownerｰtimeless γ ws :
Timeless (ws_deque_2۰owner γ ws).
#[global] Instance ws_deque_2۰invｰpersistent t ι :
Persistent (ws_deque_2۰inv t ι).
Lemma ws_deque_2۰modelｰexclusive t vs1 vs2 :
ws_deque_2۰model t vs1 -∗
ws_deque_2۰model t vs2 -∗
False.
Lemma ws_deque_2۰ownerｰexclusive t ws1 ws2 :
ws_deque_2۰owner t ws1 -∗
ws_deque_2۰owner t ws2 -∗
False.
Lemma ws_deque_2ｰownerｰmodel γ ws vs :
ws_deque_2۰owner γ ws -∗
ws_deque_2۰model γ vs -∗
⌜vs `suffix_of` ws⌝.
Lemma ws_deque_2٠createｰspec ι :
{{{
True
}}}
ws_deque_2٠create ()
{{{
t
, RET t;
ws_deque_2۰inv t ι ∗
ws_deque_2۰model t [] ∗
ws_deque_2۰owner t []
}}}.
Lemma ws_deque_2٠sizeｰspec t ι ws :
<<<
ws_deque_2۰inv t ι ∗
ws_deque_2۰owner t ws
| ∀∀ vs,
ws_deque_2۰model t vs
>>>
ws_deque_2٠size t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model t vs
| RET #(length vs);
ws_deque_2۰owner t vs
>>>.
Lemma ws_deque_2٠is_emptyｰspec t ι ws :
<<<
ws_deque_2۰inv t ι ∗
ws_deque_2۰owner t ws
| ∀∀ vs,
ws_deque_2۰model t vs
>>>
ws_deque_2٠is_empty t @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model t vs
| RET #(bool_decide (vs = []%list));
ws_deque_2۰owner t vs
>>>.
Lemma ws_deque_2٠pushｰspec t ι ws v :
<<<
ws_deque_2۰inv t ι ∗
ws_deque_2۰owner t ws
| ∀∀ vs,
ws_deque_2۰model t vs
>>>
ws_deque_2٠push t v @ ↑ι
<<<
⌜vs `suffix_of` ws⌝ ∗
ws_deque_2۰model t (vs ++ [v])
| RET ();
ws_deque_2۰owner t (vs ++ [v])
>>>.
Lemma ws_deque_2٠stealｰspec t ι :
<<<
ws_deque_2۰inv t ι
| ∀∀ vs,
ws_deque_2۰model t vs
>>>
ws_deque_2٠steal t @ ↑ι
<<<
ws_deque_2۰model t (tail vs)
| RET head vs;
True
>>>.
Lemma ws_deque_2٠popｰspec t ι ws :
<<<
ws_deque_2۰inv t ι ∗
ws_deque_2۰owner t ws
| ∀∀ vs,
ws_deque_2۰model t vs
>>>
ws_deque_2٠pop t @ ↑ι
<<<
∃∃ o ws',
⌜vs `suffix_of` ws⌝ ∗
match o with
| None ⇒
⌜vs = []⌝ ∗
⌜ws' = []⌝ ∗
ws_deque_2۰model t []
| Some v ⇒
∃ vs',
⌜vs = vs' ++ [v]⌝ ∗
⌜ws' = vs'⌝ ∗
ws_deque_2۰model t vs'
end
| RET o;
ws_deque_2۰owner t ws'
>>>.
End ws_deque_2۰G.
#[global] Opaque ws_deque_2۰inv.
#[global] Opaque ws_deque_2۰model.
#[global] Opaque ws_deque_2۰owner.