Library zoo_parabs.ws_deques_private
From zoo Require Import
prelude.
From zoo.common Require Import
countable.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.ghost_var
lib.ghost_pred
lib.ghost_list
lib.oneshot
lib.twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
array
atomic_array
queue_3
domain
random_round.
From zoo_parabs Require Export
base
ws_deques_private__code.
From zoo_parabs Require Import
ws_deques_private__types.
From zoo Require Import
options.
Implicit Types l : location.
Implicit Types v t queue round : val.
Implicit Types o : option val.
Implicit Types vs ws : list val.
Implicit Types vss wss : list (list val).
Implicit Types status : status.
Implicit Types 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 Types request : request.
Implicit Types 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 Types response : response.
Implicit Types 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 Types Ψ : 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 Types γ : metadata.
Implicit Types γ_owners : list gname.
Implicit Types γ_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_twin1 γ_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_twin2 γ_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)⌝ ∗
meta l nroot γ ∗
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⌝ ∗
meta l nroot γ ∗
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⌝ ∗
meta l nroot γ ∗
⌜γ.(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) →
{{{
meta l nroot γ ∗
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.
From zoo_parabs Require
ws_deques_private__opaque.
prelude.
From zoo.common Require Import
countable.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.ghost_var
lib.ghost_pred
lib.ghost_list
lib.oneshot
lib.twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
array
atomic_array
queue_3
domain
random_round.
From zoo_parabs Require Export
base
ws_deques_private__code.
From zoo_parabs Require Import
ws_deques_private__types.
From zoo Require Import
options.
Implicit Types l : location.
Implicit Types v t queue round : val.
Implicit Types o : option val.
Implicit Types vs ws : list val.
Implicit Types vss wss : list (list val).
Implicit Types status : status.
Implicit Types 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 Types request : request.
Implicit Types 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 Types response : response.
Implicit Types 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 Types Ψ : 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 Types γ : metadata.
Implicit Types γ_owners : list gname.
Implicit Types γ_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_twin1 γ_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_twin2 γ_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)⌝ ∗
meta l nroot γ ∗
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⌝ ∗
meta l nroot γ ∗
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⌝ ∗
meta l nroot γ ∗
⌜γ.(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) →
{{{
meta l nroot γ ∗
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.
From zoo_parabs Require
ws_deques_private__opaque.