Library zoo_parabs.ws_deques_public
From zoo Require Import
prelude.
From zoo.iris.bi Require Import
big_op.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
array
random_round.
From zoo_saturn Require Import
ws_deque_2.
From zoo_parabs Require Export
base
ws_deques_public__code.
From zoo Require Import
options.
Implicit Types v t queue round : val.
Implicit Types vs ws queues : list val.
Implicit Types vss : list (list val).
Implicit Types status : status.
Class WsDequesPublicG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] ws_deques_public_G_ws_deque_G :: WsDeque2G Σ
}.
Definition ws_deques_public_Σ :=
#[ws_deque_2_Σ
].
#[global] Instance subG_ws_deques_public_Σ Σ `{zoo_G : !ZooG Σ} :
subG ws_deques_public_Σ Σ →
WsDequesPublicG Σ.
Section ws_deques_public_G.
Context `{ws_deques_public_G : WsDequesPublicG Σ}.
Definition ws_deques_public_inv t ι sz : iProp Σ :=
∃ queues,
⌜sz = length queues⌝ ∗
array_model t DfracDiscarded queues ∗
[∗ list] queue ∈ queues,
ws_deque_2_inv queue ι.
#[local] Instance : CustomIpat "inv" :=
" ( %queues{} & %Hqueues{}_length & #Hqueues{} & #Hqueues{}_inv ) ".
Definition ws_deques_public_model t vss : iProp Σ :=
∃ queues,
array_model t DfracDiscarded queues ∗
[∗ list] i ↦ queue; vs ∈ queues; vss,
ws_deque_2_model queue vs.
#[local] Instance : CustomIpat "model" :=
" ( %queues{;_} & Hqueues{;_} & Hqueues{}_model ) ".
Definition ws_deques_public_owner t i status ws : iProp Σ :=
∃ queues queue,
⌜queues !! i = Some queue⌝ ∗
array_model t DfracDiscarded queues ∗
ws_deque_2_owner queue ws.
#[local] Instance : CustomIpat "owner" :=
" ( %queues{;_} & %queue{} & %Hqueues{}_lookup & Hqueues{;_} & Hqueue{}_owner ) ".
#[global] Instance ws_deques_public_model_timeless t vss :
Timeless (ws_deques_public_model t vss).
#[global] Instance ws_deques_public_inv_persistent t ι sz :
Persistent (ws_deques_public_inv t ι sz).
Lemma ws_deques_public_inv_agree t ι1 sz1 ι2 sz2 :
ws_deques_public_inv t ι1 sz1 -∗
ws_deques_public_inv t ι2 sz2 -∗
⌜sz1 = sz2⌝.
Lemma ws_deques_public_owner_exclusive t i status1 ws1 status2 ws2 :
ws_deques_public_owner t i status1 ws1 -∗
ws_deques_public_owner t i status2 ws2 -∗
False.
Lemma ws_deques_public_inv_model t ι sz vss :
ws_deques_public_inv t ι sz -∗
ws_deques_public_model t vss -∗
⌜length vss = sz⌝.
Lemma ws_deques_public_inv_owner t ι sz i status ws :
ws_deques_public_inv t ι sz -∗
ws_deques_public_owner t i status ws -∗
⌜i < sz⌝.
Lemma ws_deques_public_model_owner t vss i status ws :
ws_deques_public_model t vss -∗
ws_deques_public_owner t i status ws -∗
∃ vs,
⌜vss !! i = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝.
Lemma ws_deques_public٠create𑁒spec ι sz :
(0 ≤ sz)%Z →
{{{
True
}}}
ws_deques_public٠create #sz
{{{
t
, RET t;
ws_deques_public_inv t ι ₊sz ∗
ws_deques_public_model t (replicate ₊sz []) ∗
[∗ list] i ∈ seq 0 ₊sz,
ws_deques_public_owner t i Nonblocked []
}}}.
Lemma ws_deques_public٠size𑁒spec t ι sz :
{{{
ws_deques_public_inv t ι sz
}}}
ws_deques_public٠size t
{{{
RET #sz;
True
}}}.
Lemma ws_deques_public٠block𑁒spec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Nonblocked ws
}}}
ws_deques_public٠block t #i
{{{
RET ();
ws_deques_public_owner t i_ Blocked ws
}}}.
Lemma ws_deques_public٠unblock𑁒spec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Blocked ws
}}}
ws_deques_public٠unblock t #i
{{{
RET ();
ws_deques_public_owner t i_ Nonblocked ws
}}}.
Lemma ws_deques_public٠push𑁒spec t ι sz i i_ ws v :
i = ⁺i_ →
<<<
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Nonblocked ws
| ∀∀ vss,
ws_deques_public_model t vss
>>>
ws_deques_public٠push t #i v @ ↑ι
<<<
∃∃ vs,
⌜vss !! i_ = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_deques_public_model t (<[i_ := vs ++ [v]]> vss)
| RET ();
ws_deques_public_owner t i_ Nonblocked (vs ++ [v])
>>>.
Lemma ws_deques_public٠pop𑁒spec t ι sz i i_ ws :
i = ⁺i_ →
<<<
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Nonblocked ws
| ∀∀ vss,
ws_deques_public_model t vss
>>>
ws_deques_public٠pop t #i @ ↑ι
<<<
∃∃ o ws',
match o with
| None ⇒
⌜vss !! i_ = Some []⌝ ∗
⌜ws' = []⌝ ∗
ws_deques_public_model t vss
| Some v ⇒
∃ vs,
⌜vss !! i_ = Some (vs ++ [v])⌝ ∗
⌜vs ++ [v] `suffix_of` ws⌝ ∗
⌜ws' = vs⌝ ∗
ws_deques_public_model t (<[i_ := vs]> vss)
end
| RET o;
ws_deques_public_owner t i_ Nonblocked ws'
>>>.
Lemma ws_deques_public٠steal_to𑁒spec t ι (sz : nat) i i_ ws j :
i = ⁺i_ →
(0 ≤ j < sz)%Z →
<<<
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Blocked ws
| ∀∀ vss,
ws_deques_public_model t vss
>>>
ws_deques_public٠steal_to t #i #j @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_public_model t vss
| Some v ⇒
∃ vs,
⌜vss !! ₊j = Some (v :: vs)⌝ ∗
ws_deques_public_model t (<[₊j := vs]> vss)
end
| RET o;
ws_deques_public_owner t i_ Blocked ws
>>>.
End ws_deques_public_G.
#[global] Opaque ws_deques_public_inv.
#[global] Opaque ws_deques_public_model.
#[global] Opaque ws_deques_public_owner.
Section ws_deques_public_G.
Context `{ws_deques_public_G : WsDequesPublicG Σ}.
#[local] Lemma ws_deques_public٠steal_as₀𑁒spec t ι (sz : nat) i i_ ws round (n : nat) :
i = ⁺i_ →
<<<
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Blocked ws ∗
random_round_model' round (sz - 1) n
| ∀∀ vss,
ws_deques_public_model t vss
>>>
ws_deques_public٠steal_as₀ t #sz #i round #n @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_public_model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_deques_public_model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_deques_public_owner t i_ Blocked ws ∗
random_round_model' round (sz - 1) n
>>>.
Lemma ws_deques_public٠steal_as𑁒spec t ι sz i i_ ws round :
i = ⁺i_ →
0 < sz →
<<<
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Blocked ws ∗
random_round_model' round (sz - 1) (sz - 1)
| ∀∀ vss,
ws_deques_public_model t vss
>>>
ws_deques_public٠steal_as t #i round @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_public_model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_deques_public_model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_deques_public_owner t i_ Blocked ws ∗
random_round_model' round (sz - 1) n
>>>.
End ws_deques_public_G.
From zoo_parabs Require
ws_deques_public__opaque.
prelude.
From zoo.iris.bi Require Import
big_op.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
array
random_round.
From zoo_saturn Require Import
ws_deque_2.
From zoo_parabs Require Export
base
ws_deques_public__code.
From zoo Require Import
options.
Implicit Types v t queue round : val.
Implicit Types vs ws queues : list val.
Implicit Types vss : list (list val).
Implicit Types status : status.
Class WsDequesPublicG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] ws_deques_public_G_ws_deque_G :: WsDeque2G Σ
}.
Definition ws_deques_public_Σ :=
#[ws_deque_2_Σ
].
#[global] Instance subG_ws_deques_public_Σ Σ `{zoo_G : !ZooG Σ} :
subG ws_deques_public_Σ Σ →
WsDequesPublicG Σ.
Section ws_deques_public_G.
Context `{ws_deques_public_G : WsDequesPublicG Σ}.
Definition ws_deques_public_inv t ι sz : iProp Σ :=
∃ queues,
⌜sz = length queues⌝ ∗
array_model t DfracDiscarded queues ∗
[∗ list] queue ∈ queues,
ws_deque_2_inv queue ι.
#[local] Instance : CustomIpat "inv" :=
" ( %queues{} & %Hqueues{}_length & #Hqueues{} & #Hqueues{}_inv ) ".
Definition ws_deques_public_model t vss : iProp Σ :=
∃ queues,
array_model t DfracDiscarded queues ∗
[∗ list] i ↦ queue; vs ∈ queues; vss,
ws_deque_2_model queue vs.
#[local] Instance : CustomIpat "model" :=
" ( %queues{;_} & Hqueues{;_} & Hqueues{}_model ) ".
Definition ws_deques_public_owner t i status ws : iProp Σ :=
∃ queues queue,
⌜queues !! i = Some queue⌝ ∗
array_model t DfracDiscarded queues ∗
ws_deque_2_owner queue ws.
#[local] Instance : CustomIpat "owner" :=
" ( %queues{;_} & %queue{} & %Hqueues{}_lookup & Hqueues{;_} & Hqueue{}_owner ) ".
#[global] Instance ws_deques_public_model_timeless t vss :
Timeless (ws_deques_public_model t vss).
#[global] Instance ws_deques_public_inv_persistent t ι sz :
Persistent (ws_deques_public_inv t ι sz).
Lemma ws_deques_public_inv_agree t ι1 sz1 ι2 sz2 :
ws_deques_public_inv t ι1 sz1 -∗
ws_deques_public_inv t ι2 sz2 -∗
⌜sz1 = sz2⌝.
Lemma ws_deques_public_owner_exclusive t i status1 ws1 status2 ws2 :
ws_deques_public_owner t i status1 ws1 -∗
ws_deques_public_owner t i status2 ws2 -∗
False.
Lemma ws_deques_public_inv_model t ι sz vss :
ws_deques_public_inv t ι sz -∗
ws_deques_public_model t vss -∗
⌜length vss = sz⌝.
Lemma ws_deques_public_inv_owner t ι sz i status ws :
ws_deques_public_inv t ι sz -∗
ws_deques_public_owner t i status ws -∗
⌜i < sz⌝.
Lemma ws_deques_public_model_owner t vss i status ws :
ws_deques_public_model t vss -∗
ws_deques_public_owner t i status ws -∗
∃ vs,
⌜vss !! i = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝.
Lemma ws_deques_public٠create𑁒spec ι sz :
(0 ≤ sz)%Z →
{{{
True
}}}
ws_deques_public٠create #sz
{{{
t
, RET t;
ws_deques_public_inv t ι ₊sz ∗
ws_deques_public_model t (replicate ₊sz []) ∗
[∗ list] i ∈ seq 0 ₊sz,
ws_deques_public_owner t i Nonblocked []
}}}.
Lemma ws_deques_public٠size𑁒spec t ι sz :
{{{
ws_deques_public_inv t ι sz
}}}
ws_deques_public٠size t
{{{
RET #sz;
True
}}}.
Lemma ws_deques_public٠block𑁒spec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Nonblocked ws
}}}
ws_deques_public٠block t #i
{{{
RET ();
ws_deques_public_owner t i_ Blocked ws
}}}.
Lemma ws_deques_public٠unblock𑁒spec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Blocked ws
}}}
ws_deques_public٠unblock t #i
{{{
RET ();
ws_deques_public_owner t i_ Nonblocked ws
}}}.
Lemma ws_deques_public٠push𑁒spec t ι sz i i_ ws v :
i = ⁺i_ →
<<<
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Nonblocked ws
| ∀∀ vss,
ws_deques_public_model t vss
>>>
ws_deques_public٠push t #i v @ ↑ι
<<<
∃∃ vs,
⌜vss !! i_ = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_deques_public_model t (<[i_ := vs ++ [v]]> vss)
| RET ();
ws_deques_public_owner t i_ Nonblocked (vs ++ [v])
>>>.
Lemma ws_deques_public٠pop𑁒spec t ι sz i i_ ws :
i = ⁺i_ →
<<<
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Nonblocked ws
| ∀∀ vss,
ws_deques_public_model t vss
>>>
ws_deques_public٠pop t #i @ ↑ι
<<<
∃∃ o ws',
match o with
| None ⇒
⌜vss !! i_ = Some []⌝ ∗
⌜ws' = []⌝ ∗
ws_deques_public_model t vss
| Some v ⇒
∃ vs,
⌜vss !! i_ = Some (vs ++ [v])⌝ ∗
⌜vs ++ [v] `suffix_of` ws⌝ ∗
⌜ws' = vs⌝ ∗
ws_deques_public_model t (<[i_ := vs]> vss)
end
| RET o;
ws_deques_public_owner t i_ Nonblocked ws'
>>>.
Lemma ws_deques_public٠steal_to𑁒spec t ι (sz : nat) i i_ ws j :
i = ⁺i_ →
(0 ≤ j < sz)%Z →
<<<
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Blocked ws
| ∀∀ vss,
ws_deques_public_model t vss
>>>
ws_deques_public٠steal_to t #i #j @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_public_model t vss
| Some v ⇒
∃ vs,
⌜vss !! ₊j = Some (v :: vs)⌝ ∗
ws_deques_public_model t (<[₊j := vs]> vss)
end
| RET o;
ws_deques_public_owner t i_ Blocked ws
>>>.
End ws_deques_public_G.
#[global] Opaque ws_deques_public_inv.
#[global] Opaque ws_deques_public_model.
#[global] Opaque ws_deques_public_owner.
Section ws_deques_public_G.
Context `{ws_deques_public_G : WsDequesPublicG Σ}.
#[local] Lemma ws_deques_public٠steal_as₀𑁒spec t ι (sz : nat) i i_ ws round (n : nat) :
i = ⁺i_ →
<<<
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Blocked ws ∗
random_round_model' round (sz - 1) n
| ∀∀ vss,
ws_deques_public_model t vss
>>>
ws_deques_public٠steal_as₀ t #sz #i round #n @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_public_model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_deques_public_model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_deques_public_owner t i_ Blocked ws ∗
random_round_model' round (sz - 1) n
>>>.
Lemma ws_deques_public٠steal_as𑁒spec t ι sz i i_ ws round :
i = ⁺i_ →
0 < sz →
<<<
ws_deques_public_inv t ι sz ∗
ws_deques_public_owner t i_ Blocked ws ∗
random_round_model' round (sz - 1) (sz - 1)
| ∀∀ vss,
ws_deques_public_model t vss
>>>
ws_deques_public٠steal_as t #i round @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_public_model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_deques_public_model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_deques_public_owner t i_ Blocked ws ∗
random_round_model' round (sz - 1) n
>>>.
End ws_deques_public_G.
From zoo_parabs Require
ws_deques_public__opaque.