Library zoo_parabs.ws_deques_private
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.ghost_var.
Require Import zoo.iris.base_logic.lib.ghost_pred.
Require Import zoo.iris.base_logic.lib.ghost_list.
Require Import zoo.iris.base_logic.lib.oneshot.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_parabs.base.
Require Export zoo_parabs.ws_deques_private__code.
Require Import zoo_parabs.ws_deques_private__types.
Require Import zoo.options.
Implicit Type l : location.
Implicit Type v t queue round : val.
Implicit Type o : option val.
Implicit Type vs ws : list val.
Implicit Type vss wss : list (list val).
Implicit Type status : status.
Implicit Type statuses : list status.
Class WsDequesPrivateG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ws_deques_private۰G۰models۰G :: GhostListG Σ (list val)
; #[local] ws_deques_private۰G۰owner۰G :: TwinsG Σ (leibnizO status)
; #[local] ws_deques_private۰G۰channel۰pred۰G :: GhostPredG Σ (option val)
; #[local] ws_deques_private۰G۰channel۰generation۰G :: GhostVarG Σ (leibnizO gname)
; #[local] ws_deques_private۰G۰channel۰state۰G :: OneshotG Σ () (option val)
}.
Definition ws_deques_private۰Σ :=
#[ghost_list۰Σ (list val)
; twins۰Σ (leibnizO status)
; ghost_pred۰Σ (option val)
; ghost_var۰Σ (leibnizO gname)
; oneshot۰Σ () (option val)
].
#[global] Instance subGｰws_deques_private۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ws_deques_private۰Σ Σ →
WsDequesPrivateG Σ.
#[local] Coercion status۰to_val status : val :=
match status with
| Blocked ⇒
§Blocked
| Nonblocked ⇒
§Nonblocked
end.
Variant request :=
| RequestBlocked
| RequestNone
| RequestSome (i : nat).
Implicit Type request : request.
Implicit Type requests : list request.
#[local] Definition request۰to_val request : val :=
match request with
| RequestBlocked ⇒
§RequestBlocked
| RequestNone ⇒
§RequestNone
| RequestSome i ⇒
‘RequestSome( #i )
end.
Variant response :=
| ResponseWaiting
| ResponseNone
| ResponseSome v.
Implicit Type response : response.
Implicit Type responses : list response.
#[local] Coercion option۰to_response o :=
match o with
| None ⇒
ResponseNone
| Some v ⇒
ResponseSome v
end.
#[local] Definition response۰to_val response : val :=
match response with
| ResponseWaiting ⇒
§ResponseWaiting
| ResponseNone ⇒
§ResponseNone
| ResponseSome v ⇒
‘ResponseSome( v )
end.
Section ws_deques_private۰G.
Context `{ws_deques_private۰G : WsDequesPrivateG Σ}.
Implicit Type Ψ : option val → iProp Σ.
Record metadata :=
{ metadata۰queues۰array : val
; metadata۰queues : list val
; metadata۰statuses۰array : val
; metadata۰requests۰array : val
; metadata۰responses۰array : val
; metadata۰inv : namespace
; metadata۰size : nat
; metadata۰models : gname
; metadata۰owners : list gname
; metadata۰channels : list (gname × gname)
}.
Implicit Type γ : metadata.
Implicit Type γ_owners : list gname.
Implicit Type γ_channels : list (gname × gname).
#[local] Instance metadataｰeq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadataｰcountable :
Countable metadata.
#[local] Definition models۰auth' γ_models sz vss : iProp Σ :=
ghost_list۰auth γ_models vss ∗
⌜length vss = sz⌝.
#[local] Definition models۰auth γ :=
models۰auth' γ.(metadata۰models) γ.(metadata۰size).
#[local] Instance : CustomIpat "models۰auth" :=
" ( Hauth{_{}} & %Hvss{} ) ".
#[local] Definition models۰at' γ_models i :=
ghost_list۰at γ_models i (DfracOwn 1).
#[local] Definition models۰at γ :=
models۰at' γ.(metadata۰models).
#[local] Definition owner₁' γ_owners i status : iProp Σ :=
∃ γ_owner,
⌜γ_owners !! i = Some γ_owner⌝ ∗
twins۰twin₁ γ_owner (DfracOwn 1) status.
#[local] Definition owner₁ γ :=
owner₁' γ.(metadata۰owners).
#[local] Instance : CustomIpat "owner₁" :=
" ( %γ_owner{_{}} & %Hlookup{_{}} & Htwin₁ ) ".
#[local] Definition owner₂' γ_owners i status : iProp Σ :=
∃ γ_owner,
⌜γ_owners !! i = Some γ_owner⌝ ∗
twins۰twin₂ γ_owner status.
#[local] Definition owner₂ γ :=
owner₂' γ.(metadata۰owners).
#[local] Instance : CustomIpat "owner₂" :=
" ( %γ_owner{_{}} & %Hlookup{_{}} & Htwin₂ ) ".
#[local] Definition channels۰waiting' γ_channels i : iProp Σ :=
∃ γ_channel gen,
⌜γ_channels !! i = Some γ_channel⌝ ∗
ghost_var γ_channel.2 (DfracOwn (1/2)) gen ∗
oneshot۰pending gen (DfracOwn 1) ().
#[local] Definition channels۰waiting γ :=
channels۰waiting' γ.(metadata۰channels).
#[local] Instance : CustomIpat "channels۰waiting" :=
" ( %γ_channel_{} & %gen{} & %Hlookup_{} & Hgeneration_{} & Hpending_{} ) ".
#[local] Definition channels۰sender' γ_channels i Ψ state : iProp Σ :=
∃ γ_channel,
⌜γ_channels !! i = Some γ_channel⌝ ∗
ghost_pred γ_channel.1 (DfracOwn (3/4)) Ψ ∗
match state with
| None ⇒
True
| Some o ⇒
∃ gen,
ghost_var γ_channel.2 (DfracOwn (1/2)) gen ∗
oneshot۰shot gen o
end.
#[local] Definition channels۰sender γ :=
channels۰sender' γ.(metadata۰channels).
#[local] Instance : CustomIpat "channels۰sender" :=
" ( %γ_channel_{} & {>;}%Hlookup_{} & Hpred_{} & { {done} ( %gen{} & Hgeneration_{} & #Hshot_{} ) ; _ } ) ".
#[local] Definition channels۰receiver' γ_channels i Ψ state : iProp Σ :=
∃ γ_channel gen,
⌜γ_channels !! i = Some γ_channel⌝ ∗
ghost_pred γ_channel.1 (DfracOwn (1/4)) Ψ ∗
ghost_var γ_channel.2 (DfracOwn (1/2)) gen ∗
match state with
| None ⇒
True
| Some o ⇒
oneshot۰shot gen o
end.
#[local] Definition channels۰receiver γ :=
channels۰receiver' γ.(metadata۰channels).
#[local] Instance : CustomIpat "channels۰receiver" :=
" ( %γ_channel_{} & %gen{} & %Hlookup_{} & Hpred_{} & Hgeneration_{} & {{done}#Hshot_{};_} ) ".
#[local] Definition request۰au γ i Ψ : iProp Σ :=
AU <{
∃∃ vss,
models۰auth γ vss
}> @ ⊤ ∖ ↑γ.(metadata۰inv), ∅ <{
∀∀ o,
match o with
| None ⇒
models۰auth γ vss
| Some v ⇒
∃ vs,
⌜vss !! i = Some (v :: vs)⌝ ∗
models۰auth γ (<[i := vs]> vss)
end
, COMM
Ψ o
}>.
#[local] Definition request۰model۰blocked γ i : iProp Σ :=
owner₂ γ i Blocked.
#[local] Instance : CustomIpat "request۰model۰blocked" :=
" {>;}Howner₂ ".
#[local] Definition request۰model۰nonblocked' γ i j : iProp Σ :=
∃ Ψ,
⌜j < γ.(metadata۰size)⌝ ∗
channels۰sender γ j Ψ None ∗
request۰au γ i Ψ.
#[local] Instance : CustomIpat "request۰model۰nonblocked'" :=
" ( %Χ & {>;}% & Hchannels_sender & HΧ ) ".
#[local] Definition request۰model۰nonblocked γ i j : iProp Σ :=
owner₂ γ i Nonblocked ∗
request۰model۰nonblocked' γ i j.
#[local] Instance : CustomIpat "request۰model۰nonblocked" :=
" ( {>;}Howner₂ & (:request۰model۰nonblocked') ) ".
#[local] Definition request۰model γ i request : iProp Σ :=
match request with
| RequestSome j ⇒
request۰model۰blocked γ i
∨ request۰model۰nonblocked γ i j
| _ ⇒
owner₂ γ i Nonblocked
end.
#[local] Instance : CustomIpat "request۰model" :=
" [ (:request۰model۰blocked) | (:request۰model۰nonblocked) ] ".
#[local] Definition response۰model γ i response : iProp Σ :=
match response with
| ResponseWaiting ⇒
channels۰waiting γ i
| ResponseNone ⇒
∃ Ψ,
channels۰sender γ i Ψ (Some None) ∗
Ψ None
| ResponseSome v ⇒
∃ Ψ,
channels۰sender γ i Ψ (Some $ Some v) ∗
Ψ (Some v)
end.
#[local] Instance : CustomIpat "response۰model" :=
" ( %Ψ{} & Hchannels_sender{_{}} & HΨ{} ) ".
#[local] Definition inv۰inner γ : iProp Σ :=
∃ statuses requests responses,
array۰model γ.(metadata۰statuses۰array) (DfracOwn 1) (status۰to_val <$> statuses) ∗
array۰model γ.(metadata۰requests۰array) (DfracOwn 1) (request۰to_val <$> requests) ∗
array۰model γ.(metadata۰responses۰array) (DfracOwn 1) (response۰to_val <$> responses) ∗
([∗ list] i ↦ request ∈ requests, request۰model γ i request) ∗
([∗ list] i ↦ response ∈ responses, response۰model γ i response).
#[local] Instance : CustomIpat "inv۰inner" :=
" ( %statuses{} & %requests{} & %responses{} & >Hstatuses_model & >Hrequests_model & >Hresponses_model & Hrequests & Hresponses ) ".
Definition ws_deques_private۰inv t ι (sz : nat) : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
⌜ι = γ.(metadata۰inv)⌝ ∗
⌜sz = γ.(metadata۰size)⌝ ∗
l ↪ γ ∗
l.[size] ↦□ #γ.(metadata۰size) ∗
l.[queues] ↦□ γ.(metadata۰queues۰array) ∗
⌜length γ.(metadata۰queues) = γ.(metadata۰size)⌝ ∗
array۰model γ.(metadata۰queues۰array) DfracDiscarded γ.(metadata۰queues) ∗
l.[statuses] ↦□ γ.(metadata۰statuses۰array) ∗
array۰inv γ.(metadata۰statuses۰array) γ.(metadata۰size) ∗
l.[requests] ↦□ γ.(metadata۰requests۰array) ∗
array۰inv γ.(metadata۰requests۰array) γ.(metadata۰size) ∗
l.[responses] ↦□ γ.(metadata۰responses۰array) ∗
array۰inv γ.(metadata۰responses۰array) γ.(metadata۰size) ∗
inv ι (inv۰inner γ).
#[local] Instance : CustomIpat "inv" :=
" ( %l{} & %γ{} & {%Ht_eq{};->} & {%Hι_eq{};->} & {%Hsz_eq{};->} & #Hmeta{_{}} & #Hl{}_size & #Hl{}_queues & %Hqueues{}_length & #Hqueues{}_model & #Hl{}_statuses & #Hstatuses{}_inv & #Hl{}_requests & #Hrequests{}_inv & #Hl{}_responses & #Hresponses{}_inv & #Hinv{} ) ".
Definition ws_deques_private۰model t vss : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
l ↪ γ ∗
models۰auth γ vss.
#[local] Instance : CustomIpat "model" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Hmodels_auth{_{}} ) ".
Definition ws_deques_private۰owner t i status ws : iProp Σ :=
∃ l γ queue vs Ψ_sender Ψ_receiver,
⌜t = #l⌝ ∗
l ↪ γ ∗
⌜γ.(metadata۰queues) !! i = Some queue⌝ ∗
queue_3۰model queue vs ∗
models۰at γ i vs ∗
⌜vs `suffix_of` ws⌝ ∗
owner₁ γ i Nonblocked ∗
channels۰sender γ i Ψ_sender None ∗
channels۰receiver γ i Ψ_receiver None.
#[local] Instance : CustomIpat "owner" :=
" ( %l{;_} & %γ{;_} & %queue{} & %vs{} & %Ψ_sender{_{}} & %Ψ_receiver{_{}} & %Heq{} & #Hmeta_{} & %Hqueues_lookup{_{}} & Hqueue_model{_{}} & Hmodels_at{_{}} & %Hws{} & Howner₁{_{}} & Hchannels_sender{_{}} & Hchannels_receiver{_{}} ) ".
#[local] Instance owner₂ｰtimeless γ i status :
Timeless (owner₂ γ i status).
#[local] Instance channels۰waitingｰtimeless γ i :
Timeless (channels۰waiting γ i).
#[global] Instance ws_deques_private۰modelｰtimeless t vss :
Timeless (ws_deques_private۰model t vss).
#[global] Instance ws_deques_private۰invｰpersistent t ι sz :
Persistent (ws_deques_private۰inv t ι sz).
#[local] Lemma modelsｰalloc sz :
⊢ |==>
∃ γ_models,
models۰auth' γ_models sz (replicate sz []) ∗
[∗ list] i ∈ seq 0 sz,
models۰at' γ_models i [].
#[local] Lemma models۰authｰlength γ vss :
models۰auth γ vss ⊢
⌜length vss = γ.(metadata۰size)⌝.
#[local] Lemma modelsｰlookup γ vss i vs :
models۰auth γ vss -∗
models۰at γ i vs -∗
⌜vss !! i = Some vs⌝.
#[local] Lemma modelsｰupdate {γ vss i vs} vs' :
models۰auth γ vss -∗
models۰at γ i vs ==∗
models۰auth γ (<[i := vs']> vss) ∗
models۰at γ i vs'.
Opaque models۰auth'.
#[local] Lemma ownerｰalloc sz :
⊢ |==>
∃ γ_owners,
( [∗ list] i ∈ seq 0 sz,
owner₁' γ_owners i Nonblocked
) ∗
( [∗ list] i ∈ seq 0 sz,
owner₂' γ_owners i Nonblocked
).
#[local] Lemma ownerｰagree γ i status1 status2 :
owner₁ γ i status1 -∗
owner₂ γ i status2 -∗
⌜status1 = status2⌝.
#[local] Lemma ownerｰupdate {γ i status1 status2} status :
owner₁ γ i status1 -∗
owner₂ γ i status2 ==∗
owner₁ γ i status ∗
owner₂ γ i status.
Opaque owner₁'.
Opaque owner₂'.
#[local] Lemma channelsｰalloc sz :
⊢ |==>
∃ γ_channels,
( [∗ list] i ∈ seq 0 sz,
channels۰waiting' γ_channels i
) ∗
( [∗ list] i ∈ seq 0 sz,
channels۰sender' γ_channels i inhabitant None ∗
channels۰receiver' γ_channels i inhabitant None
).
#[local] Lemma channels۰senderｰexclusive γ i Ψ1 state1 Ψ2 state2 :
channels۰sender γ i Ψ1 state1 -∗
channels۰sender γ i Ψ2 state2 -∗
False.
#[local] Lemma channelsｰwaitingｰreceiver γ i Ψ o :
▷ channels۰waiting γ i -∗
channels۰receiver γ i Ψ (Some o) -∗
◇ False.
#[local] Lemma channelsｰsenderｰreceiverｰagree γ i Ψ1 o1 Ψ2 o2 E :
▷ channels۰sender γ i Ψ1 (Some o1) -∗
channels۰receiver γ i Ψ2 (Some o2) ={E}=∗
▷^2 (Ψ1 o1 ≡ Ψ2 o1) ∗
⌜o1 = o2⌝ ∗
▷ channels۰sender γ i Ψ1 (Some o1) ∗
channels۰receiver γ i Ψ2 (Some o1).
#[local] Lemma channelsｰprepare {γ i Ψ1 Ψ2} Ψ :
channels۰sender γ i Ψ1 None -∗
channels۰receiver γ i Ψ2 None ==∗
channels۰sender γ i Ψ None ∗
channels۰receiver γ i Ψ None.
#[local] Lemma channelsｰsend {γ i Ψ} o :
channels۰waiting γ i -∗
channels۰sender γ i Ψ None ==∗
channels۰sender γ i Ψ (Some o).
#[local] Lemma channelsｰreceive γ i Ψ1 Ψ2 o :
▷ channels۰sender γ i Ψ1 (Some o) -∗
channels۰receiver γ i Ψ2 None -∗
◇ (
▷ channels۰sender γ i Ψ1 (Some o) ∗
channels۰receiver γ i Ψ2 (Some o)
).
#[local] Lemma channelsｰreset γ i Ψ1 o1 Ψ2 o2 E :
▷ channels۰sender γ i Ψ1 (Some o1) -∗
channels۰receiver γ i Ψ2 (Some o2) ={E}=∗
channels۰waiting γ i ∗
▷ channels۰sender γ i Ψ1 None ∗
channels۰receiver γ i Ψ2 None.
Opaque channels۰waiting'.
Opaque channels۰sender'.
Opaque channels۰receiver'.
#[local] Lemma request۰modelｰupdate {γ i request} request' :
(request' = RequestBlocked ∨ request' = RequestNone) →
▷ request۰model γ i request -∗
owner₁ γ i Nonblocked -∗
◇ (
▷ request۰model γ i request' ∗
owner₁ γ i Nonblocked ∗
if request is RequestSome j then
▷ request۰model۰nonblocked' γ i j
else
True
).
#[local] Lemma request۰modelｰrespond γ i request :
▷ request۰model γ i request -∗
owner₁ γ i Nonblocked ==∗
◇ (
▷ request۰model γ i request ∗
if request is RequestSome j then
owner₁ γ i Blocked ∗
▷ request۰model۰nonblocked' γ i j
else
owner₁ γ i Nonblocked
).
#[local] Lemma request۰modelｰunblock γ i request :
▷ request۰model γ i request -∗
owner₁ γ i Blocked ==∗
◇ (
▷ request۰model γ i RequestNone ∗
owner₁ γ i Nonblocked
).
#[local] Lemma response۰modelｰsender γ i response Ψ state :
▷ response۰model γ i response -∗
channels۰sender γ i Ψ state -∗
◇ (
⌜response = ResponseWaiting⌝ ∗
channels۰waiting γ i ∗
channels۰sender γ i Ψ state
).
#[local] Lemma response۰modelｰreceiver γ i response Ψ o E :
▷ response۰model γ i response -∗
channels۰receiver γ i Ψ (Some o) ={E}=∗
∃ Ψ_,
▷^2 (Ψ_ o ≡ Ψ o) ∗
⌜response = o⌝ ∗
▷ channels۰sender γ i Ψ_ (Some o) ∗
channels۰receiver γ i Ψ (Some o) ∗
▷ Ψ_ o.
Lemma ws_deques_private۰invｰagree t ι1 sz1 ι2 sz2 :
ws_deques_private۰inv t ι1 sz1 -∗
ws_deques_private۰inv t ι2 sz2 -∗
⌜sz1 = sz2⌝.
Lemma ws_deques_private۰ownerｰexclusive t i status1 ws1 status2 ws2 :
ws_deques_private۰owner t i status1 ws1 -∗
ws_deques_private۰owner t i status2 ws2 -∗
False.
Lemma ws_deques_privateｰinvｰmodel t ι sz vss :
ws_deques_private۰inv t ι sz -∗
ws_deques_private۰model t vss -∗
⌜length vss = sz⌝.
Lemma ws_deques_privateｰinvｰowner t ι sz i status ws :
ws_deques_private۰inv t ι sz -∗
ws_deques_private۰owner t i status ws -∗
⌜i < sz⌝.
Lemma ws_deques_privateｰmodelｰowner t vss i status ws :
ws_deques_private۰model t vss -∗
ws_deques_private۰owner t i status ws -∗
∃ vs,
⌜vss !! i = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝.
Lemma ws_deques_private٠createｰspec ι sz :
(0 ≤ sz)%Z →
{{{
True
}}}
ws_deques_private٠create #sz
{{{
t
, RET t;
ws_deques_private۰inv t ι ₊sz ∗
ws_deques_private۰model t (replicate ₊sz []) ∗
[∗ list] i ∈ seq 0 ₊sz,
ws_deques_private۰owner t i Nonblocked []
}}}.
Lemma ws_deques_private٠sizeｰspec t ι sz :
{{{
ws_deques_private۰inv t ι sz
}}}
ws_deques_private٠size t
{{{
RET #sz;
True
}}}.
Lemma ws_deques_private٠blockｰspec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Nonblocked ws
}}}
ws_deques_private٠block t #i
{{{
RET ();
ws_deques_private۰owner t i_ Blocked ws
}}}.
Lemma ws_deques_private٠unblockｰspec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Blocked ws
}}}
ws_deques_private٠unblock t #i
{{{
RET ();
ws_deques_private۰owner t i_ Nonblocked ws
}}}.
#[local] Lemma ws_deques_private٠respondｰspec {t ι sz i i_} ws :
i = ⁺i_ →
{{{
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Nonblocked ws
}}}
ws_deques_private٠respond t #i
{{{
RET ();
ws_deques_private۰owner t i_ Nonblocked ws
}}}.
Lemma ws_deques_private٠pushｰspec t ι sz i i_ ws v :
i = ⁺i_ →
<<<
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Nonblocked ws
| ∀∀ vss,
ws_deques_private۰model t vss
>>>
ws_deques_private٠push t #i v @ ↑ι
<<<
∃∃ vs,
⌜vss !! i_ = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_deques_private۰model t (<[i_ := vs ++ [v]]> vss)
| RET ();
ws_deques_private۰owner t i_ Nonblocked (vs ++ [v])
>>>.
Lemma ws_deques_private٠popｰspec t ι sz i i_ ws :
i = ⁺i_ →
<<<
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Nonblocked ws
| ∀∀ vss,
ws_deques_private۰model t vss
>>>
ws_deques_private٠pop t #i @ ↑ι
<<<
∃∃ o ws',
match o with
| None ⇒
⌜vss !! i_ = Some []⌝ ∗
⌜ws' = []⌝ ∗
ws_deques_private۰model t vss
| Some v ⇒
∃ vs,
⌜vss !! i_ = Some (vs ++ [v])⌝ ∗
⌜vs ++ [v] `suffix_of` ws⌝ ∗
⌜ws' = vs⌝ ∗
ws_deques_private۰model t (<[i_ := vs]> vss)
end
| RET o;
ws_deques_private۰owner t i_ Nonblocked ws'
>>>.
#[local] Lemma ws_deques_private٠steal_to₁ｰspec l γ i i_ Ψ :
i = ⁺i_ →
i_ < γ.(metadata۰size) →
{{{
l ↪ γ ∗
l.[responses] ↦□ γ.(metadata۰responses۰array) ∗
array۰inv γ.(metadata۰responses۰array) γ.(metadata۰size) ∗
inv γ.(metadata۰inv) (inv۰inner γ) ∗
channels۰receiver γ i_ Ψ None
}}}
ws_deques_private٠steal_to₁ #l #i
{{{
o Ψ_sender Ψ_receiver
, RET o;
channels۰sender γ i_ Ψ_sender None ∗
channels۰receiver γ i_ Ψ_receiver None ∗
Ψ o
}}}.
Lemma ws_deques_private٠steal_toｰspec t ι (sz : nat) i i_ ws j :
i = ⁺i_ →
(0 ≤ j < sz)%Z →
<<<
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Blocked ws
| ∀∀ vss,
ws_deques_private۰model t vss
>>>
ws_deques_private٠steal_to t #i #j @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_private۰model t vss
| Some v ⇒
∃ vs,
⌜vss !! ₊j = Some (v :: vs)⌝ ∗
ws_deques_private۰model t (<[₊j := vs]> vss)
end
| RET o;
ws_deques_private۰owner t i_ Blocked ws
>>>.
End ws_deques_private۰G.
#[global] Opaque ws_deques_private۰inv.
#[global] Opaque ws_deques_private۰model.
#[global] Opaque ws_deques_private۰owner.
Section ws_deques_private۰G.
Context `{ws_deques_private۰G : WsDequesPrivateG Σ}.
#[local] Lemma ws_deques_private٠steal_as₁ｰspec t ι (sz : nat) i i_ ws round (n : nat) :
i = ⁺i_ →
<<<
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
| ∀∀ vss,
ws_deques_private۰model t vss
>>>
ws_deques_private٠steal_as₁ t #sz #i round #n @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_private۰model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_deques_private۰model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_deques_private۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
>>>.
Lemma ws_deques_private٠steal_asｰspec t ι sz i i_ ws round :
i = ⁺i_ →
0 < sz →
<<<
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) (sz - 1)
| ∀∀ vss,
ws_deques_private۰model t vss
>>>
ws_deques_private٠steal_as t #i round @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_private۰model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_deques_private۰model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_deques_private۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
>>>.
End ws_deques_private۰G.
Require zoo_parabs.ws_deques_private__opaque.
Require Import zoo.common.countable.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.ghost_var.
Require Import zoo.iris.base_logic.lib.ghost_pred.
Require Import zoo.iris.base_logic.lib.ghost_list.
Require Import zoo.iris.base_logic.lib.oneshot.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_parabs.base.
Require Export zoo_parabs.ws_deques_private__code.
Require Import zoo_parabs.ws_deques_private__types.
Require Import zoo.options.
Implicit Type l : location.
Implicit Type v t queue round : val.
Implicit Type o : option val.
Implicit Type vs ws : list val.
Implicit Type vss wss : list (list val).
Implicit Type status : status.
Implicit Type statuses : list status.
Class WsDequesPrivateG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ws_deques_private۰G۰models۰G :: GhostListG Σ (list val)
; #[local] ws_deques_private۰G۰owner۰G :: TwinsG Σ (leibnizO status)
; #[local] ws_deques_private۰G۰channel۰pred۰G :: GhostPredG Σ (option val)
; #[local] ws_deques_private۰G۰channel۰generation۰G :: GhostVarG Σ (leibnizO gname)
; #[local] ws_deques_private۰G۰channel۰state۰G :: OneshotG Σ () (option val)
}.
Definition ws_deques_private۰Σ :=
#[ghost_list۰Σ (list val)
; twins۰Σ (leibnizO status)
; ghost_pred۰Σ (option val)
; ghost_var۰Σ (leibnizO gname)
; oneshot۰Σ () (option val)
].
#[global] Instance subGｰws_deques_private۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ws_deques_private۰Σ Σ →
WsDequesPrivateG Σ.
#[local] Coercion status۰to_val status : val :=
match status with
| Blocked ⇒
§Blocked
| Nonblocked ⇒
§Nonblocked
end.
Variant request :=
| RequestBlocked
| RequestNone
| RequestSome (i : nat).
Implicit Type request : request.
Implicit Type requests : list request.
#[local] Definition request۰to_val request : val :=
match request with
| RequestBlocked ⇒
§RequestBlocked
| RequestNone ⇒
§RequestNone
| RequestSome i ⇒
‘RequestSome( #i )
end.
Variant response :=
| ResponseWaiting
| ResponseNone
| ResponseSome v.
Implicit Type response : response.
Implicit Type responses : list response.
#[local] Coercion option۰to_response o :=
match o with
| None ⇒
ResponseNone
| Some v ⇒
ResponseSome v
end.
#[local] Definition response۰to_val response : val :=
match response with
| ResponseWaiting ⇒
§ResponseWaiting
| ResponseNone ⇒
§ResponseNone
| ResponseSome v ⇒
‘ResponseSome( v )
end.
Section ws_deques_private۰G.
Context `{ws_deques_private۰G : WsDequesPrivateG Σ}.
Implicit Type Ψ : option val → iProp Σ.
Record metadata :=
{ metadata۰queues۰array : val
; metadata۰queues : list val
; metadata۰statuses۰array : val
; metadata۰requests۰array : val
; metadata۰responses۰array : val
; metadata۰inv : namespace
; metadata۰size : nat
; metadata۰models : gname
; metadata۰owners : list gname
; metadata۰channels : list (gname × gname)
}.
Implicit Type γ : metadata.
Implicit Type γ_owners : list gname.
Implicit Type γ_channels : list (gname × gname).
#[local] Instance metadataｰeq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadataｰcountable :
Countable metadata.
#[local] Definition models۰auth' γ_models sz vss : iProp Σ :=
ghost_list۰auth γ_models vss ∗
⌜length vss = sz⌝.
#[local] Definition models۰auth γ :=
models۰auth' γ.(metadata۰models) γ.(metadata۰size).
#[local] Instance : CustomIpat "models۰auth" :=
" ( Hauth{_{}} & %Hvss{} ) ".
#[local] Definition models۰at' γ_models i :=
ghost_list۰at γ_models i (DfracOwn 1).
#[local] Definition models۰at γ :=
models۰at' γ.(metadata۰models).
#[local] Definition owner₁' γ_owners i status : iProp Σ :=
∃ γ_owner,
⌜γ_owners !! i = Some γ_owner⌝ ∗
twins۰twin₁ γ_owner (DfracOwn 1) status.
#[local] Definition owner₁ γ :=
owner₁' γ.(metadata۰owners).
#[local] Instance : CustomIpat "owner₁" :=
" ( %γ_owner{_{}} & %Hlookup{_{}} & Htwin₁ ) ".
#[local] Definition owner₂' γ_owners i status : iProp Σ :=
∃ γ_owner,
⌜γ_owners !! i = Some γ_owner⌝ ∗
twins۰twin₂ γ_owner status.
#[local] Definition owner₂ γ :=
owner₂' γ.(metadata۰owners).
#[local] Instance : CustomIpat "owner₂" :=
" ( %γ_owner{_{}} & %Hlookup{_{}} & Htwin₂ ) ".
#[local] Definition channels۰waiting' γ_channels i : iProp Σ :=
∃ γ_channel gen,
⌜γ_channels !! i = Some γ_channel⌝ ∗
ghost_var γ_channel.2 (DfracOwn (1/2)) gen ∗
oneshot۰pending gen (DfracOwn 1) ().
#[local] Definition channels۰waiting γ :=
channels۰waiting' γ.(metadata۰channels).
#[local] Instance : CustomIpat "channels۰waiting" :=
" ( %γ_channel_{} & %gen{} & %Hlookup_{} & Hgeneration_{} & Hpending_{} ) ".
#[local] Definition channels۰sender' γ_channels i Ψ state : iProp Σ :=
∃ γ_channel,
⌜γ_channels !! i = Some γ_channel⌝ ∗
ghost_pred γ_channel.1 (DfracOwn (3/4)) Ψ ∗
match state with
| None ⇒
True
| Some o ⇒
∃ gen,
ghost_var γ_channel.2 (DfracOwn (1/2)) gen ∗
oneshot۰shot gen o
end.
#[local] Definition channels۰sender γ :=
channels۰sender' γ.(metadata۰channels).
#[local] Instance : CustomIpat "channels۰sender" :=
" ( %γ_channel_{} & {>;}%Hlookup_{} & Hpred_{} & { {done} ( %gen{} & Hgeneration_{} & #Hshot_{} ) ; _ } ) ".
#[local] Definition channels۰receiver' γ_channels i Ψ state : iProp Σ :=
∃ γ_channel gen,
⌜γ_channels !! i = Some γ_channel⌝ ∗
ghost_pred γ_channel.1 (DfracOwn (1/4)) Ψ ∗
ghost_var γ_channel.2 (DfracOwn (1/2)) gen ∗
match state with
| None ⇒
True
| Some o ⇒
oneshot۰shot gen o
end.
#[local] Definition channels۰receiver γ :=
channels۰receiver' γ.(metadata۰channels).
#[local] Instance : CustomIpat "channels۰receiver" :=
" ( %γ_channel_{} & %gen{} & %Hlookup_{} & Hpred_{} & Hgeneration_{} & {{done}#Hshot_{};_} ) ".
#[local] Definition request۰au γ i Ψ : iProp Σ :=
AU <{
∃∃ vss,
models۰auth γ vss
}> @ ⊤ ∖ ↑γ.(metadata۰inv), ∅ <{
∀∀ o,
match o with
| None ⇒
models۰auth γ vss
| Some v ⇒
∃ vs,
⌜vss !! i = Some (v :: vs)⌝ ∗
models۰auth γ (<[i := vs]> vss)
end
, COMM
Ψ o
}>.
#[local] Definition request۰model۰blocked γ i : iProp Σ :=
owner₂ γ i Blocked.
#[local] Instance : CustomIpat "request۰model۰blocked" :=
" {>;}Howner₂ ".
#[local] Definition request۰model۰nonblocked' γ i j : iProp Σ :=
∃ Ψ,
⌜j < γ.(metadata۰size)⌝ ∗
channels۰sender γ j Ψ None ∗
request۰au γ i Ψ.
#[local] Instance : CustomIpat "request۰model۰nonblocked'" :=
" ( %Χ & {>;}% & Hchannels_sender & HΧ ) ".
#[local] Definition request۰model۰nonblocked γ i j : iProp Σ :=
owner₂ γ i Nonblocked ∗
request۰model۰nonblocked' γ i j.
#[local] Instance : CustomIpat "request۰model۰nonblocked" :=
" ( {>;}Howner₂ & (:request۰model۰nonblocked') ) ".
#[local] Definition request۰model γ i request : iProp Σ :=
match request with
| RequestSome j ⇒
request۰model۰blocked γ i
∨ request۰model۰nonblocked γ i j
| _ ⇒
owner₂ γ i Nonblocked
end.
#[local] Instance : CustomIpat "request۰model" :=
" [ (:request۰model۰blocked) | (:request۰model۰nonblocked) ] ".
#[local] Definition response۰model γ i response : iProp Σ :=
match response with
| ResponseWaiting ⇒
channels۰waiting γ i
| ResponseNone ⇒
∃ Ψ,
channels۰sender γ i Ψ (Some None) ∗
Ψ None
| ResponseSome v ⇒
∃ Ψ,
channels۰sender γ i Ψ (Some $ Some v) ∗
Ψ (Some v)
end.
#[local] Instance : CustomIpat "response۰model" :=
" ( %Ψ{} & Hchannels_sender{_{}} & HΨ{} ) ".
#[local] Definition inv۰inner γ : iProp Σ :=
∃ statuses requests responses,
array۰model γ.(metadata۰statuses۰array) (DfracOwn 1) (status۰to_val <$> statuses) ∗
array۰model γ.(metadata۰requests۰array) (DfracOwn 1) (request۰to_val <$> requests) ∗
array۰model γ.(metadata۰responses۰array) (DfracOwn 1) (response۰to_val <$> responses) ∗
([∗ list] i ↦ request ∈ requests, request۰model γ i request) ∗
([∗ list] i ↦ response ∈ responses, response۰model γ i response).
#[local] Instance : CustomIpat "inv۰inner" :=
" ( %statuses{} & %requests{} & %responses{} & >Hstatuses_model & >Hrequests_model & >Hresponses_model & Hrequests & Hresponses ) ".
Definition ws_deques_private۰inv t ι (sz : nat) : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
⌜ι = γ.(metadata۰inv)⌝ ∗
⌜sz = γ.(metadata۰size)⌝ ∗
l ↪ γ ∗
l.[size] ↦□ #γ.(metadata۰size) ∗
l.[queues] ↦□ γ.(metadata۰queues۰array) ∗
⌜length γ.(metadata۰queues) = γ.(metadata۰size)⌝ ∗
array۰model γ.(metadata۰queues۰array) DfracDiscarded γ.(metadata۰queues) ∗
l.[statuses] ↦□ γ.(metadata۰statuses۰array) ∗
array۰inv γ.(metadata۰statuses۰array) γ.(metadata۰size) ∗
l.[requests] ↦□ γ.(metadata۰requests۰array) ∗
array۰inv γ.(metadata۰requests۰array) γ.(metadata۰size) ∗
l.[responses] ↦□ γ.(metadata۰responses۰array) ∗
array۰inv γ.(metadata۰responses۰array) γ.(metadata۰size) ∗
inv ι (inv۰inner γ).
#[local] Instance : CustomIpat "inv" :=
" ( %l{} & %γ{} & {%Ht_eq{};->} & {%Hι_eq{};->} & {%Hsz_eq{};->} & #Hmeta{_{}} & #Hl{}_size & #Hl{}_queues & %Hqueues{}_length & #Hqueues{}_model & #Hl{}_statuses & #Hstatuses{}_inv & #Hl{}_requests & #Hrequests{}_inv & #Hl{}_responses & #Hresponses{}_inv & #Hinv{} ) ".
Definition ws_deques_private۰model t vss : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
l ↪ γ ∗
models۰auth γ vss.
#[local] Instance : CustomIpat "model" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Hmodels_auth{_{}} ) ".
Definition ws_deques_private۰owner t i status ws : iProp Σ :=
∃ l γ queue vs Ψ_sender Ψ_receiver,
⌜t = #l⌝ ∗
l ↪ γ ∗
⌜γ.(metadata۰queues) !! i = Some queue⌝ ∗
queue_3۰model queue vs ∗
models۰at γ i vs ∗
⌜vs `suffix_of` ws⌝ ∗
owner₁ γ i Nonblocked ∗
channels۰sender γ i Ψ_sender None ∗
channels۰receiver γ i Ψ_receiver None.
#[local] Instance : CustomIpat "owner" :=
" ( %l{;_} & %γ{;_} & %queue{} & %vs{} & %Ψ_sender{_{}} & %Ψ_receiver{_{}} & %Heq{} & #Hmeta_{} & %Hqueues_lookup{_{}} & Hqueue_model{_{}} & Hmodels_at{_{}} & %Hws{} & Howner₁{_{}} & Hchannels_sender{_{}} & Hchannels_receiver{_{}} ) ".
#[local] Instance owner₂ｰtimeless γ i status :
Timeless (owner₂ γ i status).
#[local] Instance channels۰waitingｰtimeless γ i :
Timeless (channels۰waiting γ i).
#[global] Instance ws_deques_private۰modelｰtimeless t vss :
Timeless (ws_deques_private۰model t vss).
#[global] Instance ws_deques_private۰invｰpersistent t ι sz :
Persistent (ws_deques_private۰inv t ι sz).
#[local] Lemma modelsｰalloc sz :
⊢ |==>
∃ γ_models,
models۰auth' γ_models sz (replicate sz []) ∗
[∗ list] i ∈ seq 0 sz,
models۰at' γ_models i [].
#[local] Lemma models۰authｰlength γ vss :
models۰auth γ vss ⊢
⌜length vss = γ.(metadata۰size)⌝.
#[local] Lemma modelsｰlookup γ vss i vs :
models۰auth γ vss -∗
models۰at γ i vs -∗
⌜vss !! i = Some vs⌝.
#[local] Lemma modelsｰupdate {γ vss i vs} vs' :
models۰auth γ vss -∗
models۰at γ i vs ==∗
models۰auth γ (<[i := vs']> vss) ∗
models۰at γ i vs'.
Opaque models۰auth'.
#[local] Lemma ownerｰalloc sz :
⊢ |==>
∃ γ_owners,
( [∗ list] i ∈ seq 0 sz,
owner₁' γ_owners i Nonblocked
) ∗
( [∗ list] i ∈ seq 0 sz,
owner₂' γ_owners i Nonblocked
).
#[local] Lemma ownerｰagree γ i status1 status2 :
owner₁ γ i status1 -∗
owner₂ γ i status2 -∗
⌜status1 = status2⌝.
#[local] Lemma ownerｰupdate {γ i status1 status2} status :
owner₁ γ i status1 -∗
owner₂ γ i status2 ==∗
owner₁ γ i status ∗
owner₂ γ i status.
Opaque owner₁'.
Opaque owner₂'.
#[local] Lemma channelsｰalloc sz :
⊢ |==>
∃ γ_channels,
( [∗ list] i ∈ seq 0 sz,
channels۰waiting' γ_channels i
) ∗
( [∗ list] i ∈ seq 0 sz,
channels۰sender' γ_channels i inhabitant None ∗
channels۰receiver' γ_channels i inhabitant None
).
#[local] Lemma channels۰senderｰexclusive γ i Ψ1 state1 Ψ2 state2 :
channels۰sender γ i Ψ1 state1 -∗
channels۰sender γ i Ψ2 state2 -∗
False.
#[local] Lemma channelsｰwaitingｰreceiver γ i Ψ o :
▷ channels۰waiting γ i -∗
channels۰receiver γ i Ψ (Some o) -∗
◇ False.
#[local] Lemma channelsｰsenderｰreceiverｰagree γ i Ψ1 o1 Ψ2 o2 E :
▷ channels۰sender γ i Ψ1 (Some o1) -∗
channels۰receiver γ i Ψ2 (Some o2) ={E}=∗
▷^2 (Ψ1 o1 ≡ Ψ2 o1) ∗
⌜o1 = o2⌝ ∗
▷ channels۰sender γ i Ψ1 (Some o1) ∗
channels۰receiver γ i Ψ2 (Some o1).
#[local] Lemma channelsｰprepare {γ i Ψ1 Ψ2} Ψ :
channels۰sender γ i Ψ1 None -∗
channels۰receiver γ i Ψ2 None ==∗
channels۰sender γ i Ψ None ∗
channels۰receiver γ i Ψ None.
#[local] Lemma channelsｰsend {γ i Ψ} o :
channels۰waiting γ i -∗
channels۰sender γ i Ψ None ==∗
channels۰sender γ i Ψ (Some o).
#[local] Lemma channelsｰreceive γ i Ψ1 Ψ2 o :
▷ channels۰sender γ i Ψ1 (Some o) -∗
channels۰receiver γ i Ψ2 None -∗
◇ (
▷ channels۰sender γ i Ψ1 (Some o) ∗
channels۰receiver γ i Ψ2 (Some o)
).
#[local] Lemma channelsｰreset γ i Ψ1 o1 Ψ2 o2 E :
▷ channels۰sender γ i Ψ1 (Some o1) -∗
channels۰receiver γ i Ψ2 (Some o2) ={E}=∗
channels۰waiting γ i ∗
▷ channels۰sender γ i Ψ1 None ∗
channels۰receiver γ i Ψ2 None.
Opaque channels۰waiting'.
Opaque channels۰sender'.
Opaque channels۰receiver'.
#[local] Lemma request۰modelｰupdate {γ i request} request' :
(request' = RequestBlocked ∨ request' = RequestNone) →
▷ request۰model γ i request -∗
owner₁ γ i Nonblocked -∗
◇ (
▷ request۰model γ i request' ∗
owner₁ γ i Nonblocked ∗
if request is RequestSome j then
▷ request۰model۰nonblocked' γ i j
else
True
).
#[local] Lemma request۰modelｰrespond γ i request :
▷ request۰model γ i request -∗
owner₁ γ i Nonblocked ==∗
◇ (
▷ request۰model γ i request ∗
if request is RequestSome j then
owner₁ γ i Blocked ∗
▷ request۰model۰nonblocked' γ i j
else
owner₁ γ i Nonblocked
).
#[local] Lemma request۰modelｰunblock γ i request :
▷ request۰model γ i request -∗
owner₁ γ i Blocked ==∗
◇ (
▷ request۰model γ i RequestNone ∗
owner₁ γ i Nonblocked
).
#[local] Lemma response۰modelｰsender γ i response Ψ state :
▷ response۰model γ i response -∗
channels۰sender γ i Ψ state -∗
◇ (
⌜response = ResponseWaiting⌝ ∗
channels۰waiting γ i ∗
channels۰sender γ i Ψ state
).
#[local] Lemma response۰modelｰreceiver γ i response Ψ o E :
▷ response۰model γ i response -∗
channels۰receiver γ i Ψ (Some o) ={E}=∗
∃ Ψ_,
▷^2 (Ψ_ o ≡ Ψ o) ∗
⌜response = o⌝ ∗
▷ channels۰sender γ i Ψ_ (Some o) ∗
channels۰receiver γ i Ψ (Some o) ∗
▷ Ψ_ o.
Lemma ws_deques_private۰invｰagree t ι1 sz1 ι2 sz2 :
ws_deques_private۰inv t ι1 sz1 -∗
ws_deques_private۰inv t ι2 sz2 -∗
⌜sz1 = sz2⌝.
Lemma ws_deques_private۰ownerｰexclusive t i status1 ws1 status2 ws2 :
ws_deques_private۰owner t i status1 ws1 -∗
ws_deques_private۰owner t i status2 ws2 -∗
False.
Lemma ws_deques_privateｰinvｰmodel t ι sz vss :
ws_deques_private۰inv t ι sz -∗
ws_deques_private۰model t vss -∗
⌜length vss = sz⌝.
Lemma ws_deques_privateｰinvｰowner t ι sz i status ws :
ws_deques_private۰inv t ι sz -∗
ws_deques_private۰owner t i status ws -∗
⌜i < sz⌝.
Lemma ws_deques_privateｰmodelｰowner t vss i status ws :
ws_deques_private۰model t vss -∗
ws_deques_private۰owner t i status ws -∗
∃ vs,
⌜vss !! i = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝.
Lemma ws_deques_private٠createｰspec ι sz :
(0 ≤ sz)%Z →
{{{
True
}}}
ws_deques_private٠create #sz
{{{
t
, RET t;
ws_deques_private۰inv t ι ₊sz ∗
ws_deques_private۰model t (replicate ₊sz []) ∗
[∗ list] i ∈ seq 0 ₊sz,
ws_deques_private۰owner t i Nonblocked []
}}}.
Lemma ws_deques_private٠sizeｰspec t ι sz :
{{{
ws_deques_private۰inv t ι sz
}}}
ws_deques_private٠size t
{{{
RET #sz;
True
}}}.
Lemma ws_deques_private٠blockｰspec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Nonblocked ws
}}}
ws_deques_private٠block t #i
{{{
RET ();
ws_deques_private۰owner t i_ Blocked ws
}}}.
Lemma ws_deques_private٠unblockｰspec t ι sz i i_ ws :
i = ⁺i_ →
{{{
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Blocked ws
}}}
ws_deques_private٠unblock t #i
{{{
RET ();
ws_deques_private۰owner t i_ Nonblocked ws
}}}.
#[local] Lemma ws_deques_private٠respondｰspec {t ι sz i i_} ws :
i = ⁺i_ →
{{{
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Nonblocked ws
}}}
ws_deques_private٠respond t #i
{{{
RET ();
ws_deques_private۰owner t i_ Nonblocked ws
}}}.
Lemma ws_deques_private٠pushｰspec t ι sz i i_ ws v :
i = ⁺i_ →
<<<
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Nonblocked ws
| ∀∀ vss,
ws_deques_private۰model t vss
>>>
ws_deques_private٠push t #i v @ ↑ι
<<<
∃∃ vs,
⌜vss !! i_ = Some vs⌝ ∗
⌜vs `suffix_of` ws⌝ ∗
ws_deques_private۰model t (<[i_ := vs ++ [v]]> vss)
| RET ();
ws_deques_private۰owner t i_ Nonblocked (vs ++ [v])
>>>.
Lemma ws_deques_private٠popｰspec t ι sz i i_ ws :
i = ⁺i_ →
<<<
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Nonblocked ws
| ∀∀ vss,
ws_deques_private۰model t vss
>>>
ws_deques_private٠pop t #i @ ↑ι
<<<
∃∃ o ws',
match o with
| None ⇒
⌜vss !! i_ = Some []⌝ ∗
⌜ws' = []⌝ ∗
ws_deques_private۰model t vss
| Some v ⇒
∃ vs,
⌜vss !! i_ = Some (vs ++ [v])⌝ ∗
⌜vs ++ [v] `suffix_of` ws⌝ ∗
⌜ws' = vs⌝ ∗
ws_deques_private۰model t (<[i_ := vs]> vss)
end
| RET o;
ws_deques_private۰owner t i_ Nonblocked ws'
>>>.
#[local] Lemma ws_deques_private٠steal_to₁ｰspec l γ i i_ Ψ :
i = ⁺i_ →
i_ < γ.(metadata۰size) →
{{{
l ↪ γ ∗
l.[responses] ↦□ γ.(metadata۰responses۰array) ∗
array۰inv γ.(metadata۰responses۰array) γ.(metadata۰size) ∗
inv γ.(metadata۰inv) (inv۰inner γ) ∗
channels۰receiver γ i_ Ψ None
}}}
ws_deques_private٠steal_to₁ #l #i
{{{
o Ψ_sender Ψ_receiver
, RET o;
channels۰sender γ i_ Ψ_sender None ∗
channels۰receiver γ i_ Ψ_receiver None ∗
Ψ o
}}}.
Lemma ws_deques_private٠steal_toｰspec t ι (sz : nat) i i_ ws j :
i = ⁺i_ →
(0 ≤ j < sz)%Z →
<<<
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Blocked ws
| ∀∀ vss,
ws_deques_private۰model t vss
>>>
ws_deques_private٠steal_to t #i #j @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_private۰model t vss
| Some v ⇒
∃ vs,
⌜vss !! ₊j = Some (v :: vs)⌝ ∗
ws_deques_private۰model t (<[₊j := vs]> vss)
end
| RET o;
ws_deques_private۰owner t i_ Blocked ws
>>>.
End ws_deques_private۰G.
#[global] Opaque ws_deques_private۰inv.
#[global] Opaque ws_deques_private۰model.
#[global] Opaque ws_deques_private۰owner.
Section ws_deques_private۰G.
Context `{ws_deques_private۰G : WsDequesPrivateG Σ}.
#[local] Lemma ws_deques_private٠steal_as₁ｰspec t ι (sz : nat) i i_ ws round (n : nat) :
i = ⁺i_ →
<<<
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
| ∀∀ vss,
ws_deques_private۰model t vss
>>>
ws_deques_private٠steal_as₁ t #sz #i round #n @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_private۰model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_deques_private۰model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_deques_private۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
>>>.
Lemma ws_deques_private٠steal_asｰspec t ι sz i i_ ws round :
i = ⁺i_ →
0 < sz →
<<<
ws_deques_private۰inv t ι sz ∗
ws_deques_private۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) (sz - 1)
| ∀∀ vss,
ws_deques_private۰model t vss
>>>
ws_deques_private٠steal_as t #i round @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
ws_deques_private۰model t vss
| Some v ⇒
∃ j vs,
⌜₊i ≠ j⌝ ∗
⌜vss !! j = Some (v :: vs)⌝ ∗
ws_deques_private۰model t (<[j := vs]> vss)
end
| RET o;
∃ n,
ws_deques_private۰owner t i_ Blocked ws ∗
random_round۰model' round (sz - 1) n
>>>.
End ws_deques_private۰G.
Require zoo_parabs.ws_deques_private__opaque.