Library zoo_parabs.ws_bdeques_public
Require Import zoo.prelude.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_parabs.base.
Require Export zoo_parabs.ws_bdeques_public__code.
Require Import zoo_parabs.ws_bdeques_public__types.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type v t queue round : val.
Implicit Type vs ws queues : list val.
Implicit Type vss : list (list val).
Implicit Type status : status.
#[local] Definition capacity :=
val۰to_nat' ws_bdeques_public٠capacity.
#[local] Lemma ws_bdeques_public٠capacityｰunfold :
ws_bdeques_public٠capacity = #capacity.
Opaque ws_bdeques_public٠capacity.
Opaque capacity.
Class WsBdequesPublicG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ws_bdeques_public۰G۰ws_bdeque۰G :: WsBdeque2G Σ
}.
Definition ws_bdeques_public۰Σ :=
#[ws_bdeque_2۰Σ
].
#[global] Instance subGｰws_bdeques_public۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ws_bdeques_public۰Σ Σ →
WsBdequesPublicG Σ.
Section ws_bdeques_public۰G.
Context `{ws_bdeques_public۰G : WsBdequesPublicG Σ}.
Definition ws_bdeques_public۰inv t ι sz : iProp Σ :=
∃ queues,
⌜sz = length queues⌝ ∗
array۰model t DfracDiscarded queues ∗
[∗ list] queue ∈ queues,
ws_bdeque_2۰inv queue ι capacity.
#[local] Instance : CustomIpat "inv" :=
" ( %queues{} & %Hqueues{}_length & #Hqueues{} & #Hqueues{}_inv ) ".
Definition ws_bdeques_public۰model t vss : iProp Σ :=
∃ queues,
array۰model t DfracDiscarded queues ∗
[∗ list] i ↦ queue; vs ∈ queues; vss,
ws_bdeque_2۰model queue vs.
#[local] Instance : CustomIpat "model" :=
" ( %queues{;_} & Hqueues{;_} & Hqueues{}_model ) ".
Definition ws_bdeques_public۰owner t i status ws : iProp Σ :=
∃ queues queue,
⌜queues !! i = Some queue⌝ ∗
array۰model t DfracDiscarded queues ∗
ws_bdeque_2۰owner queue ws.
#[local] Instance : CustomIpat "owner" :=
" ( %queues{;_} & %queue{} & %Hqueues{}_lookup & Hqueues{;_} & Hqueue{}_owner ) ".
#[global] Instance ws_bdeques_public۰modelｰtimeless t vss :
Timeless (ws_bdeques_public۰model t vss).
#[global] Instance ws_bdeques_public۰invｰpersistent t ι sz :
Persistent (ws_bdeques_public۰inv t ι sz).
Lemma ws_bdeques_public۰invｰagree t ι1 sz1 ι2 sz2 :
ws_bdeques_public۰inv t ι1 sz1 -∗
ws_bdeques_public۰inv t ι2 sz2 -∗
⌜sz1 = sz2⌝.
Lemma ws_bdeques_public۰ownerｰexclusive t i status1 ws1 status2 ws2 :
ws_bdeques_public۰owner t i status1 ws1 -∗
ws_bdeques_public۰owner t i status2 ws2 -∗
False.
Lemma ws_bdeques_publicｰinvｰmodel t ι sz vss :
ws_bdeques_public۰inv t ι sz -∗
ws_bdeques_public۰model t vss -∗
⌜length vss = sz⌝.
Lemma ws_bdeques_publicｰinvｰowner t ι sz i status ws :
ws_bdeques_public۰inv t ι sz -∗
ws_bdeques_public۰owner t i status ws -∗
⌜i < sz⌝.
Lemma ws_bdeques_publicｰmodelｰowner t vss i status ws :
ws_bdeques_public۰model t vss -∗
ws_bdeques_public۰owner t i status ws -∗
∃ vs,
⌜vss !! i = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝.
Lemma ws_bdeques_public٠createｰspec ι sz :
(0 ≤ sz)%Z →
{{{
True
}}}
ws_bdeques_public٠create #sz
{{{
t
, RET t;
ws_bdeques_public۰inv t ι ₊sz ∗
ws_bdeques_public۰model t (replicate ₊sz []) ∗
[∗ list] i ∈ seq 0 ₊sz,
ws_bdeques_public۰owner t i Nonblocked []
}}}.
Lemma ws_bdeques_public٠sizeｰspec t ι sz :
{{{
ws_bdeques_public۰inv t ι sz
}}}
ws_bdeques_public٠size t
{{{
RET #sz;
True
}}}.
Lemma ws_bdeques_public٠blockｰspec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Nonblocked ws
}}}
ws_bdeques_public٠block t #i
{{{
RET ();
ws_bdeques_public۰owner t i_ Blocked ws
}}}.
Lemma ws_bdeques_public٠unblockｰspec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Blocked ws
}}}
ws_bdeques_public٠unblock t #i
{{{
RET ();
ws_bdeques_public۰owner t i_ Nonblocked ws
}}}.
Lemma ws_bdeques_public٠pushｰspec t ι sz i i_ ws v :
i = ⁺i_ →
<<<
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Nonblocked ws
| ∀∀ vss,
ws_bdeques_public۰model t vss
>>>
ws_bdeques_public٠push t #i v @ ↑ι
<<<
∃∃ b vs,
⌜vss !! i_ = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
if b then
ws_bdeques_public۰model t (<[i_ := vs ++ [v]]> vss)
else
ws_bdeques_public۰model t vss
| RET #b;
if b then
ws_bdeques_public۰owner t i_ Nonblocked (vs ++ [v])
else
ws_bdeques_public۰owner t i_ Nonblocked ws
>>>.
Lemma ws_bdeques_public٠popｰspec t ι sz i i_ ws :
i = ⁺i_ →
<<<
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Nonblocked ws
| ∀∀ vss,
ws_bdeques_public۰model t vss
>>>
ws_bdeques_public٠pop t #i @ ↑ι
<<<
∃∃ o ws',
match o with
| None ⇒
⌜vss !! i_ = Some []⌝ ∗
⌜ws' = []⌝ ∗
ws_bdeques_public۰model t vss
| Some v ⇒
∃ vs,
⌜vss !! i_ = Some (vs ++ [v])⌝ ∗
⌜vs ++ [v] `suffix_of` ws⌝ ∗
⌜ws' = vs⌝ ∗
ws_bdeques_public۰model t (<[i_ := vs]> vss)
end
| RET o;
ws_bdeques_public۰owner t i_ Nonblocked ws'
>>>.
Lemma ws_bdeques_public٠steal_toｰspec t ι (sz : nat) i i_ ws j :
i = ⁺i_ →
(0 ≤ j < sz)%Z →
<<<
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Blocked ws
| ∀∀ vss,
ws_bdeques_public۰model t vss
>>>
ws_bdeques_public٠steal_to t #i #j @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_bdeques_public۰model t vss
| Some v ⇒
∃ vs,
⌜vss !! ₊j = Some (v :: vs)⌝ ∗
ws_bdeques_public۰model t (<[₊j := vs]> vss)
end
| RET o;
ws_bdeques_public۰owner t i_ Blocked ws
>>>.
End ws_bdeques_public۰G.
#[global] Opaque ws_bdeques_public۰inv.
#[global] Opaque ws_bdeques_public۰model.
#[global] Opaque ws_bdeques_public۰owner.
Section ws_bdeques_public۰G.
Context `{ws_bdeques_public۰G : WsBdequesPublicG Σ}.
#[local] Lemma ws_bdeques_public٠steal_as₁ｰspec t ι (sz : nat) i i_ ws round (n : nat) :
i = ⁺i_ →
<<<
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
| ∀∀ vss,
ws_bdeques_public۰model t vss
>>>
ws_bdeques_public٠steal_as₁ t #sz #i round #n @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_bdeques_public۰model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_bdeques_public۰model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_bdeques_public۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
>>>.
Lemma ws_bdeques_public٠steal_asｰspec t ι sz i i_ ws round :
i = ⁺i_ →
0 < sz →
<<<
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) (sz - 1)
| ∀∀ vss,
ws_bdeques_public۰model t vss
>>>
ws_bdeques_public٠steal_as t #i round @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_bdeques_public۰model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_bdeques_public۰model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_bdeques_public۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
>>>.
End ws_bdeques_public۰G.
Require zoo_parabs.ws_bdeques_public__opaque.
Require Import zoo.iris.bi.big_op.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_parabs.base.
Require Export zoo_parabs.ws_bdeques_public__code.
Require Import zoo_parabs.ws_bdeques_public__types.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type v t queue round : val.
Implicit Type vs ws queues : list val.
Implicit Type vss : list (list val).
Implicit Type status : status.
#[local] Definition capacity :=
val۰to_nat' ws_bdeques_public٠capacity.
#[local] Lemma ws_bdeques_public٠capacityｰunfold :
ws_bdeques_public٠capacity = #capacity.
Opaque ws_bdeques_public٠capacity.
Opaque capacity.
Class WsBdequesPublicG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ws_bdeques_public۰G۰ws_bdeque۰G :: WsBdeque2G Σ
}.
Definition ws_bdeques_public۰Σ :=
#[ws_bdeque_2۰Σ
].
#[global] Instance subGｰws_bdeques_public۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ws_bdeques_public۰Σ Σ →
WsBdequesPublicG Σ.
Section ws_bdeques_public۰G.
Context `{ws_bdeques_public۰G : WsBdequesPublicG Σ}.
Definition ws_bdeques_public۰inv t ι sz : iProp Σ :=
∃ queues,
⌜sz = length queues⌝ ∗
array۰model t DfracDiscarded queues ∗
[∗ list] queue ∈ queues,
ws_bdeque_2۰inv queue ι capacity.
#[local] Instance : CustomIpat "inv" :=
" ( %queues{} & %Hqueues{}_length & #Hqueues{} & #Hqueues{}_inv ) ".
Definition ws_bdeques_public۰model t vss : iProp Σ :=
∃ queues,
array۰model t DfracDiscarded queues ∗
[∗ list] i ↦ queue; vs ∈ queues; vss,
ws_bdeque_2۰model queue vs.
#[local] Instance : CustomIpat "model" :=
" ( %queues{;_} & Hqueues{;_} & Hqueues{}_model ) ".
Definition ws_bdeques_public۰owner t i status ws : iProp Σ :=
∃ queues queue,
⌜queues !! i = Some queue⌝ ∗
array۰model t DfracDiscarded queues ∗
ws_bdeque_2۰owner queue ws.
#[local] Instance : CustomIpat "owner" :=
" ( %queues{;_} & %queue{} & %Hqueues{}_lookup & Hqueues{;_} & Hqueue{}_owner ) ".
#[global] Instance ws_bdeques_public۰modelｰtimeless t vss :
Timeless (ws_bdeques_public۰model t vss).
#[global] Instance ws_bdeques_public۰invｰpersistent t ι sz :
Persistent (ws_bdeques_public۰inv t ι sz).
Lemma ws_bdeques_public۰invｰagree t ι1 sz1 ι2 sz2 :
ws_bdeques_public۰inv t ι1 sz1 -∗
ws_bdeques_public۰inv t ι2 sz2 -∗
⌜sz1 = sz2⌝.
Lemma ws_bdeques_public۰ownerｰexclusive t i status1 ws1 status2 ws2 :
ws_bdeques_public۰owner t i status1 ws1 -∗
ws_bdeques_public۰owner t i status2 ws2 -∗
False.
Lemma ws_bdeques_publicｰinvｰmodel t ι sz vss :
ws_bdeques_public۰inv t ι sz -∗
ws_bdeques_public۰model t vss -∗
⌜length vss = sz⌝.
Lemma ws_bdeques_publicｰinvｰowner t ι sz i status ws :
ws_bdeques_public۰inv t ι sz -∗
ws_bdeques_public۰owner t i status ws -∗
⌜i < sz⌝.
Lemma ws_bdeques_publicｰmodelｰowner t vss i status ws :
ws_bdeques_public۰model t vss -∗
ws_bdeques_public۰owner t i status ws -∗
∃ vs,
⌜vss !! i = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝.
Lemma ws_bdeques_public٠createｰspec ι sz :
(0 ≤ sz)%Z →
{{{
True
}}}
ws_bdeques_public٠create #sz
{{{
t
, RET t;
ws_bdeques_public۰inv t ι ₊sz ∗
ws_bdeques_public۰model t (replicate ₊sz []) ∗
[∗ list] i ∈ seq 0 ₊sz,
ws_bdeques_public۰owner t i Nonblocked []
}}}.
Lemma ws_bdeques_public٠sizeｰspec t ι sz :
{{{
ws_bdeques_public۰inv t ι sz
}}}
ws_bdeques_public٠size t
{{{
RET #sz;
True
}}}.
Lemma ws_bdeques_public٠blockｰspec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Nonblocked ws
}}}
ws_bdeques_public٠block t #i
{{{
RET ();
ws_bdeques_public۰owner t i_ Blocked ws
}}}.
Lemma ws_bdeques_public٠unblockｰspec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Blocked ws
}}}
ws_bdeques_public٠unblock t #i
{{{
RET ();
ws_bdeques_public۰owner t i_ Nonblocked ws
}}}.
Lemma ws_bdeques_public٠pushｰspec t ι sz i i_ ws v :
i = ⁺i_ →
<<<
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Nonblocked ws
| ∀∀ vss,
ws_bdeques_public۰model t vss
>>>
ws_bdeques_public٠push t #i v @ ↑ι
<<<
∃∃ b vs,
⌜vss !! i_ = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
if b then
ws_bdeques_public۰model t (<[i_ := vs ++ [v]]> vss)
else
ws_bdeques_public۰model t vss
| RET #b;
if b then
ws_bdeques_public۰owner t i_ Nonblocked (vs ++ [v])
else
ws_bdeques_public۰owner t i_ Nonblocked ws
>>>.
Lemma ws_bdeques_public٠popｰspec t ι sz i i_ ws :
i = ⁺i_ →
<<<
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Nonblocked ws
| ∀∀ vss,
ws_bdeques_public۰model t vss
>>>
ws_bdeques_public٠pop t #i @ ↑ι
<<<
∃∃ o ws',
match o with
| None ⇒
⌜vss !! i_ = Some []⌝ ∗
⌜ws' = []⌝ ∗
ws_bdeques_public۰model t vss
| Some v ⇒
∃ vs,
⌜vss !! i_ = Some (vs ++ [v])⌝ ∗
⌜vs ++ [v] `suffix_of` ws⌝ ∗
⌜ws' = vs⌝ ∗
ws_bdeques_public۰model t (<[i_ := vs]> vss)
end
| RET o;
ws_bdeques_public۰owner t i_ Nonblocked ws'
>>>.
Lemma ws_bdeques_public٠steal_toｰspec t ι (sz : nat) i i_ ws j :
i = ⁺i_ →
(0 ≤ j < sz)%Z →
<<<
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Blocked ws
| ∀∀ vss,
ws_bdeques_public۰model t vss
>>>
ws_bdeques_public٠steal_to t #i #j @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_bdeques_public۰model t vss
| Some v ⇒
∃ vs,
⌜vss !! ₊j = Some (v :: vs)⌝ ∗
ws_bdeques_public۰model t (<[₊j := vs]> vss)
end
| RET o;
ws_bdeques_public۰owner t i_ Blocked ws
>>>.
End ws_bdeques_public۰G.
#[global] Opaque ws_bdeques_public۰inv.
#[global] Opaque ws_bdeques_public۰model.
#[global] Opaque ws_bdeques_public۰owner.
Section ws_bdeques_public۰G.
Context `{ws_bdeques_public۰G : WsBdequesPublicG Σ}.
#[local] Lemma ws_bdeques_public٠steal_as₁ｰspec t ι (sz : nat) i i_ ws round (n : nat) :
i = ⁺i_ →
<<<
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
| ∀∀ vss,
ws_bdeques_public۰model t vss
>>>
ws_bdeques_public٠steal_as₁ t #sz #i round #n @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_bdeques_public۰model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_bdeques_public۰model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_bdeques_public۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
>>>.
Lemma ws_bdeques_public٠steal_asｰspec t ι sz i i_ ws round :
i = ⁺i_ →
0 < sz →
<<<
ws_bdeques_public۰inv t ι sz ∗
ws_bdeques_public۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) (sz - 1)
| ∀∀ vss,
ws_bdeques_public۰model t vss
>>>
ws_bdeques_public٠steal_as t #i round @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_bdeques_public۰model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_bdeques_public۰model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_bdeques_public۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
>>>.
End ws_bdeques_public۰G.
Require zoo_parabs.ws_bdeques_public__opaque.