Library zoo_saturn.mpsc_queue_3
From zoo Require Import
prelude.
From zoo.common Require Import
countable
list.
From zoo.iris.base_logic Require Import
lib.twins
lib.oneshot.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
clist.
From zoo_saturn Require Export
base
mpsc_queue_3__code.
From zoo_saturn Require Import
mpsc_queue_3__types.
From zoo Require Import
options.
Implicit Types b closed : bool.
Implicit Types l : location.
Implicit Types v t : val.
Implicit Types vs front back : list val.
Implicit Types ws : option (list val).
Class MpscQueue3G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] mpsc_queue_3_G_twins_G :: TwinsG Σ (leibnizO (list val))
; #[local] mpsc_queue_3_G_lstate_G :: OneshotG Σ () ()
}.
Definition mpsc_queue_3_Σ :=
#[twins_Σ (leibnizO (list val))
; oneshot_Σ () ()
].
#[global] Instance subG_mpsc_queue_3_Σ Σ `{zoo_G : !ZooG Σ} :
subG mpsc_queue_3_Σ Σ →
MpscQueue3G Σ.
Section mpsc_queue_3_G.
Context `{mpsc_queue_3_G : MpscQueue3G Σ}.
Record metadata :=
{ metadata_model : gname
; metadata_front : gname
; metadata_lstate : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ vs :=
model₁' γ.(metadata_model) vs.
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ vs :=
model₂' γ.(metadata_model) vs.
#[local] Definition front₁' γ_front front :=
twins_twin1 γ_front (DfracOwn 1) front.
#[local] Definition front₁ γ front :=
front₁' γ.(metadata_front) front.
#[local] Definition front₂' γ_model front :=
twins_twin2 γ_model front.
#[local] Definition front₂ γ front :=
front₂' γ.(metadata_front) front.
#[local] Definition lstate_open₁' γ_lstate :=
oneshot_pending γ_lstate (DfracOwn (1/2)) ().
#[local] Definition lstate_open₁ γ :=
lstate_open₁' γ.(metadata_lstate).
#[local] Definition lstate_open₂' γ_lstate :=
oneshot_pending γ_lstate (DfracOwn (1/2)) ().
#[local] Definition lstate_open₂ γ :=
lstate_open₂' γ.(metadata_lstate).
#[local] Definition lstate_closed γ :=
oneshot_shot γ.(metadata_lstate) ().
#[local] Definition inv_inner l γ : iProp Σ :=
∃ front v_back,
front₂ γ front ∗
l.[back] ↦ v_back ∗
( ( lstate_open₂ γ ∗
∃ back,
⌜v_back = list_to_clist_open back⌝ ∗
model₂ γ (front ++ reverse back)
) ∨ (
lstate_closed γ ∗
⌜v_back = §ClistClosed%V⌝
)
).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %front{} & %v_back & >Hfront₂ & >Hl_back & [(>Hopen₂ & %back{} & >-> & >Hmodel₂{_{suff}}) | (>Hclosed{_{suff}} & >->)] ) ".
Definition mpsc_queue_3_inv t ι : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
inv ι (inv_inner l γ).
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & -> & #Hmeta & #Hinv ) ".
Definition mpsc_queue_3_model t vs : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
model₁ γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %l{;_} & %γ{;_} & %Heq{} & Hmeta_{} & Hmodel₁{_{}} ) ".
Definition mpsc_queue_3_consumer t ws : iProp Σ :=
∃ l γ v_front front,
⌜t = #l⌝ ∗
meta l nroot γ ∗
l.[front] ↦ v_front ∗
front₁ γ front ∗
match ws with
| None ⇒
⌜v_front = list_to_clist_open front⌝ ∗
lstate_open₁ γ
| Some ws ⇒
⌜ws = front⌝ ∗
⌜v_front = list_to_clist_closed front⌝ ∗
lstate_closed γ ∗
model₂ γ front
end.
#[local] Instance : CustomIpat "consumer" :=
" ( %l_ & %γ_ & %v_front & %front & %Heq & Hmeta_ & Hl_front & Hfront₁ & {{open}(-> & Hopen₁);{closed}(-> & -> & Hclosed & Hmodel₂);Hlstate} ) ".
Definition mpsc_queue_3_closed t : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
lstate_closed γ.
#[local] Instance : CustomIpat "closed" :=
" ( %l_ & %γ_ & %Heq & Hmeta_ & Hclosed ) ".
#[global] Instance mpsc_queue_3_model_timeless t vs :
Timeless (mpsc_queue_3_model t vs).
#[global] Instance mpsc_queue_3_consumer_timeless t ws :
Timeless (mpsc_queue_3_consumer t ws ).
#[global] Instance mpsc_queue_3_inv_persistent t ι :
Persistent (mpsc_queue_3_inv t ι).
#[global] Instance mpsc_queue_3_closed_persistent t :
Persistent (mpsc_queue_3_closed t).
#[local] Lemma model_alloc :
⊢ |==>
∃ γ_model,
model₁' γ_model [] ∗
model₂' γ_model [].
#[local] Lemma model₁_exclusive γ vs1 vs2 :
model₁ γ vs1 -∗
model₁ γ vs2 -∗
False.
#[local] Lemma model_agree γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma model_update {γ vs1 vs2} vs :
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
model₁ γ vs ∗
model₂ γ vs.
#[local] Lemma front_alloc :
⊢ |==>
∃ γ_front,
front₁' γ_front [] ∗
front₂' γ_front [].
#[local] Lemma front_agree γ front1 front2 :
front₁ γ front1 -∗
front₂ γ front2 -∗
⌜front1 = front2⌝.
#[local] Lemma front_update {γ front1 front2} front :
front₁ γ front1 -∗
front₂ γ front2 ==∗
front₁ γ front ∗
front₂ γ front.
#[local] Lemma lstate_alloc :
⊢ |==>
∃ γ_lstate,
lstate_open₁' γ_lstate ∗
lstate_open₂' γ_lstate.
#[local] Lemma lstate_open₁_closed γ :
lstate_open₁ γ -∗
lstate_closed γ -∗
False.
#[local] Lemma lstate_open₂_closed γ :
lstate_open₂ γ -∗
lstate_closed γ -∗
False.
#[local] Lemma lstate_update γ :
lstate_open₁ γ -∗
lstate_open₂ γ ==∗
lstate_closed γ.
Lemma mpsc_queue_3_model_exclusive t vs1 vs2 :
mpsc_queue_3_model t vs1 -∗
mpsc_queue_3_model t vs2 -∗
False.
Lemma mpsc_queue_3_consumer_exclusive t ws1 ws2 :
mpsc_queue_3_consumer t ws1 -∗
mpsc_queue_3_consumer t ws2 -∗
False.
Lemma mpsc_queue_3_consumer_closed t vs :
mpsc_queue_3_consumer t (Some vs) ⊢
mpsc_queue_3_closed t.
Lemma mpsc_queue_3٠create𑁒spec ι :
{{{
True
}}}
mpsc_queue_3٠create ()
{{{
t
, RET t;
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_model t [] ∗
mpsc_queue_3_consumer t None
}}}.
Lemma mpsc_queue_3٠is_empty𑁒spec_open t ι :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t None
| ∀∀ vs,
mpsc_queue_3_model t vs
>>>
mpsc_queue_3٠is_empty t @ ↑ι
<<<
mpsc_queue_3_model t vs
| RET #(bool_decide (vs = []%list));
mpsc_queue_3_consumer t None
>>>.
Lemma mpsc_queue_3٠is_empty𑁒spec_closed t ι vs :
{{{
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t (Some vs)
}}}
mpsc_queue_3٠is_empty t
{{{
RET #(bool_decide (vs = []%list));
mpsc_queue_3_consumer t (Some vs)
}}}.
Lemma mpsc_queue_3٠push_front𑁒spec_open t ι v :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t None
| ∀∀ vs,
mpsc_queue_3_model t vs
>>>
mpsc_queue_3٠push_front t v @ ↑ι
<<<
mpsc_queue_3_model t (v :: vs)
| RET false;
mpsc_queue_3_consumer t None
>>>.
Lemma mpsc_queue_3٠push_front𑁒spec_closed t ι vs v :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t (Some vs)
| ∀∀ vs',
mpsc_queue_3_model t vs'
>>>
mpsc_queue_3٠push_front t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (vs = [])⌝ ∗
⌜vs' = vs⌝ ∗
mpsc_queue_3_model t (if b then [] else v :: vs)
| RET #b;
mpsc_queue_3_consumer t (Some $ if b then [] else v :: vs)
>>>.
Lemma mpsc_queue_3٠push_back𑁒spec_open closed t ι v :
<<<
mpsc_queue_3_inv t ι
| ∀∀ vs,
mpsc_queue_3_model t vs
>>>
mpsc_queue_3٠push_back t v @ ↑ι
<<<
∃∃ closed,
if closed then
mpsc_queue_3_model t vs
else
mpsc_queue_3_model t (vs ++ [v])
| RET #closed;
if closed then
mpsc_queue_3_closed t
else
True
>>>.
Lemma mpsc_queue_3٠push_back𑁒spec_closed closed t ι v :
{{{
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_closed t
}}}
mpsc_queue_3٠push_back t v
{{{
RET true;
True
}}}.
Lemma mpsc_queue_3٠pop𑁒spec_open t ι :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t None
| ∀∀ vs,
mpsc_queue_3_model t vs
>>>
mpsc_queue_3٠pop t @ ↑ι
<<<
mpsc_queue_3_model t (tail vs)
| RET head vs;
mpsc_queue_3_consumer t None
>>>.
Lemma mpsc_queue_3٠pop𑁒spec_closed t ι vs :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t (Some vs)
| ∀∀ vs',
mpsc_queue_3_model t vs'
>>>
mpsc_queue_3٠pop t @ ↑ι
<<<
⌜vs' = vs⌝ ∗
mpsc_queue_3_model t (tail vs)
| RET head vs;
mpsc_queue_3_consumer t (Some $ tail vs)
>>>.
Lemma mpsc_queue_3٠close𑁒spec_open t ι :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t None
| ∀∀ vs,
mpsc_queue_3_model t vs
>>>
mpsc_queue_3٠close t @ ↑ι
<<<
mpsc_queue_3_model t vs
| RET false;
mpsc_queue_3_consumer t (Some vs)
>>>.
Lemma mpsc_queue_3٠close𑁒spec_closed t ι vs :
{{{
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t (Some vs)
}}}
mpsc_queue_3٠close t
{{{
RET true;
mpsc_queue_3_consumer t (Some vs)
}}}.
End mpsc_queue_3_G.
From zoo_saturn Require
mpsc_queue_3__opaque.
#[global] Opaque mpsc_queue_3_inv.
#[global] Opaque mpsc_queue_3_model.
#[global] Opaque mpsc_queue_3_consumer.
#[global] Opaque mpsc_queue_3_closed.
prelude.
From zoo.common Require Import
countable
list.
From zoo.iris.base_logic Require Import
lib.twins
lib.oneshot.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
clist.
From zoo_saturn Require Export
base
mpsc_queue_3__code.
From zoo_saturn Require Import
mpsc_queue_3__types.
From zoo Require Import
options.
Implicit Types b closed : bool.
Implicit Types l : location.
Implicit Types v t : val.
Implicit Types vs front back : list val.
Implicit Types ws : option (list val).
Class MpscQueue3G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] mpsc_queue_3_G_twins_G :: TwinsG Σ (leibnizO (list val))
; #[local] mpsc_queue_3_G_lstate_G :: OneshotG Σ () ()
}.
Definition mpsc_queue_3_Σ :=
#[twins_Σ (leibnizO (list val))
; oneshot_Σ () ()
].
#[global] Instance subG_mpsc_queue_3_Σ Σ `{zoo_G : !ZooG Σ} :
subG mpsc_queue_3_Σ Σ →
MpscQueue3G Σ.
Section mpsc_queue_3_G.
Context `{mpsc_queue_3_G : MpscQueue3G Σ}.
Record metadata :=
{ metadata_model : gname
; metadata_front : gname
; metadata_lstate : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ vs :=
model₁' γ.(metadata_model) vs.
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ vs :=
model₂' γ.(metadata_model) vs.
#[local] Definition front₁' γ_front front :=
twins_twin1 γ_front (DfracOwn 1) front.
#[local] Definition front₁ γ front :=
front₁' γ.(metadata_front) front.
#[local] Definition front₂' γ_model front :=
twins_twin2 γ_model front.
#[local] Definition front₂ γ front :=
front₂' γ.(metadata_front) front.
#[local] Definition lstate_open₁' γ_lstate :=
oneshot_pending γ_lstate (DfracOwn (1/2)) ().
#[local] Definition lstate_open₁ γ :=
lstate_open₁' γ.(metadata_lstate).
#[local] Definition lstate_open₂' γ_lstate :=
oneshot_pending γ_lstate (DfracOwn (1/2)) ().
#[local] Definition lstate_open₂ γ :=
lstate_open₂' γ.(metadata_lstate).
#[local] Definition lstate_closed γ :=
oneshot_shot γ.(metadata_lstate) ().
#[local] Definition inv_inner l γ : iProp Σ :=
∃ front v_back,
front₂ γ front ∗
l.[back] ↦ v_back ∗
( ( lstate_open₂ γ ∗
∃ back,
⌜v_back = list_to_clist_open back⌝ ∗
model₂ γ (front ++ reverse back)
) ∨ (
lstate_closed γ ∗
⌜v_back = §ClistClosed%V⌝
)
).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %front{} & %v_back & >Hfront₂ & >Hl_back & [(>Hopen₂ & %back{} & >-> & >Hmodel₂{_{suff}}) | (>Hclosed{_{suff}} & >->)] ) ".
Definition mpsc_queue_3_inv t ι : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
inv ι (inv_inner l γ).
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & -> & #Hmeta & #Hinv ) ".
Definition mpsc_queue_3_model t vs : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
model₁ γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %l{;_} & %γ{;_} & %Heq{} & Hmeta_{} & Hmodel₁{_{}} ) ".
Definition mpsc_queue_3_consumer t ws : iProp Σ :=
∃ l γ v_front front,
⌜t = #l⌝ ∗
meta l nroot γ ∗
l.[front] ↦ v_front ∗
front₁ γ front ∗
match ws with
| None ⇒
⌜v_front = list_to_clist_open front⌝ ∗
lstate_open₁ γ
| Some ws ⇒
⌜ws = front⌝ ∗
⌜v_front = list_to_clist_closed front⌝ ∗
lstate_closed γ ∗
model₂ γ front
end.
#[local] Instance : CustomIpat "consumer" :=
" ( %l_ & %γ_ & %v_front & %front & %Heq & Hmeta_ & Hl_front & Hfront₁ & {{open}(-> & Hopen₁);{closed}(-> & -> & Hclosed & Hmodel₂);Hlstate} ) ".
Definition mpsc_queue_3_closed t : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
lstate_closed γ.
#[local] Instance : CustomIpat "closed" :=
" ( %l_ & %γ_ & %Heq & Hmeta_ & Hclosed ) ".
#[global] Instance mpsc_queue_3_model_timeless t vs :
Timeless (mpsc_queue_3_model t vs).
#[global] Instance mpsc_queue_3_consumer_timeless t ws :
Timeless (mpsc_queue_3_consumer t ws ).
#[global] Instance mpsc_queue_3_inv_persistent t ι :
Persistent (mpsc_queue_3_inv t ι).
#[global] Instance mpsc_queue_3_closed_persistent t :
Persistent (mpsc_queue_3_closed t).
#[local] Lemma model_alloc :
⊢ |==>
∃ γ_model,
model₁' γ_model [] ∗
model₂' γ_model [].
#[local] Lemma model₁_exclusive γ vs1 vs2 :
model₁ γ vs1 -∗
model₁ γ vs2 -∗
False.
#[local] Lemma model_agree γ vs1 vs2 :
model₁ γ vs1 -∗
model₂ γ vs2 -∗
⌜vs1 = vs2⌝.
#[local] Lemma model_update {γ vs1 vs2} vs :
model₁ γ vs1 -∗
model₂ γ vs2 ==∗
model₁ γ vs ∗
model₂ γ vs.
#[local] Lemma front_alloc :
⊢ |==>
∃ γ_front,
front₁' γ_front [] ∗
front₂' γ_front [].
#[local] Lemma front_agree γ front1 front2 :
front₁ γ front1 -∗
front₂ γ front2 -∗
⌜front1 = front2⌝.
#[local] Lemma front_update {γ front1 front2} front :
front₁ γ front1 -∗
front₂ γ front2 ==∗
front₁ γ front ∗
front₂ γ front.
#[local] Lemma lstate_alloc :
⊢ |==>
∃ γ_lstate,
lstate_open₁' γ_lstate ∗
lstate_open₂' γ_lstate.
#[local] Lemma lstate_open₁_closed γ :
lstate_open₁ γ -∗
lstate_closed γ -∗
False.
#[local] Lemma lstate_open₂_closed γ :
lstate_open₂ γ -∗
lstate_closed γ -∗
False.
#[local] Lemma lstate_update γ :
lstate_open₁ γ -∗
lstate_open₂ γ ==∗
lstate_closed γ.
Lemma mpsc_queue_3_model_exclusive t vs1 vs2 :
mpsc_queue_3_model t vs1 -∗
mpsc_queue_3_model t vs2 -∗
False.
Lemma mpsc_queue_3_consumer_exclusive t ws1 ws2 :
mpsc_queue_3_consumer t ws1 -∗
mpsc_queue_3_consumer t ws2 -∗
False.
Lemma mpsc_queue_3_consumer_closed t vs :
mpsc_queue_3_consumer t (Some vs) ⊢
mpsc_queue_3_closed t.
Lemma mpsc_queue_3٠create𑁒spec ι :
{{{
True
}}}
mpsc_queue_3٠create ()
{{{
t
, RET t;
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_model t [] ∗
mpsc_queue_3_consumer t None
}}}.
Lemma mpsc_queue_3٠is_empty𑁒spec_open t ι :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t None
| ∀∀ vs,
mpsc_queue_3_model t vs
>>>
mpsc_queue_3٠is_empty t @ ↑ι
<<<
mpsc_queue_3_model t vs
| RET #(bool_decide (vs = []%list));
mpsc_queue_3_consumer t None
>>>.
Lemma mpsc_queue_3٠is_empty𑁒spec_closed t ι vs :
{{{
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t (Some vs)
}}}
mpsc_queue_3٠is_empty t
{{{
RET #(bool_decide (vs = []%list));
mpsc_queue_3_consumer t (Some vs)
}}}.
Lemma mpsc_queue_3٠push_front𑁒spec_open t ι v :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t None
| ∀∀ vs,
mpsc_queue_3_model t vs
>>>
mpsc_queue_3٠push_front t v @ ↑ι
<<<
mpsc_queue_3_model t (v :: vs)
| RET false;
mpsc_queue_3_consumer t None
>>>.
Lemma mpsc_queue_3٠push_front𑁒spec_closed t ι vs v :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t (Some vs)
| ∀∀ vs',
mpsc_queue_3_model t vs'
>>>
mpsc_queue_3٠push_front t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (vs = [])⌝ ∗
⌜vs' = vs⌝ ∗
mpsc_queue_3_model t (if b then [] else v :: vs)
| RET #b;
mpsc_queue_3_consumer t (Some $ if b then [] else v :: vs)
>>>.
Lemma mpsc_queue_3٠push_back𑁒spec_open closed t ι v :
<<<
mpsc_queue_3_inv t ι
| ∀∀ vs,
mpsc_queue_3_model t vs
>>>
mpsc_queue_3٠push_back t v @ ↑ι
<<<
∃∃ closed,
if closed then
mpsc_queue_3_model t vs
else
mpsc_queue_3_model t (vs ++ [v])
| RET #closed;
if closed then
mpsc_queue_3_closed t
else
True
>>>.
Lemma mpsc_queue_3٠push_back𑁒spec_closed closed t ι v :
{{{
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_closed t
}}}
mpsc_queue_3٠push_back t v
{{{
RET true;
True
}}}.
Lemma mpsc_queue_3٠pop𑁒spec_open t ι :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t None
| ∀∀ vs,
mpsc_queue_3_model t vs
>>>
mpsc_queue_3٠pop t @ ↑ι
<<<
mpsc_queue_3_model t (tail vs)
| RET head vs;
mpsc_queue_3_consumer t None
>>>.
Lemma mpsc_queue_3٠pop𑁒spec_closed t ι vs :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t (Some vs)
| ∀∀ vs',
mpsc_queue_3_model t vs'
>>>
mpsc_queue_3٠pop t @ ↑ι
<<<
⌜vs' = vs⌝ ∗
mpsc_queue_3_model t (tail vs)
| RET head vs;
mpsc_queue_3_consumer t (Some $ tail vs)
>>>.
Lemma mpsc_queue_3٠close𑁒spec_open t ι :
<<<
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t None
| ∀∀ vs,
mpsc_queue_3_model t vs
>>>
mpsc_queue_3٠close t @ ↑ι
<<<
mpsc_queue_3_model t vs
| RET false;
mpsc_queue_3_consumer t (Some vs)
>>>.
Lemma mpsc_queue_3٠close𑁒spec_closed t ι vs :
{{{
mpsc_queue_3_inv t ι ∗
mpsc_queue_3_consumer t (Some vs)
}}}
mpsc_queue_3٠close t
{{{
RET true;
mpsc_queue_3_consumer t (Some vs)
}}}.
End mpsc_queue_3_G.
From zoo_saturn Require
mpsc_queue_3__opaque.
#[global] Opaque mpsc_queue_3_inv.
#[global] Opaque mpsc_queue_3_model.
#[global] Opaque mpsc_queue_3_consumer.
#[global] Opaque mpsc_queue_3_closed.