Library zoo_saturn.mpsc_queue_1
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.mono_list
lib.twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
xtchain
domain.
From zoo_saturn Require Export
base
mpsc_queue_1__code.
From zoo_saturn Require Import
mpsc_queue_1__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types front node back new_back : location.
Implicit Types hist past nodes : list location.
Implicit Types v : val.
Implicit Types o : option val.
Implicit Types vs : list val.
Class MpscQueue1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] mpsc_queue_1_G_history_G :: MonoListG Σ location
; #[local] mpsc_queue_1_G_model_G :: TwinsG Σ (leibnizO (list val))
}.
Definition mpsc_queue_1_Σ :=
#[mono_list_Σ location
; twins_Σ (leibnizO (list val))
].
#[global] Instance subG_mpsc_queue_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG mpsc_queue_1_Σ Σ →
MpscQueue1G Σ.
Module base.
Section mpsc_queue_1_G.
Context `{mpsc_queue_1_G : MpscQueue1G Σ}.
Implicit Types t : location.
Record mpsc_queue_1_name :=
{ mpsc_queue_1_name_inv : namespace
; mpsc_queue_1_name_history : gname
; mpsc_queue_1_name_model : gname
}.
Implicit Type γ : mpsc_queue_1_name.
#[global] Instance mpsc_queue_1_name_eq_dec : EqDecision mpsc_queue_1_name :=
ltac:(solve_decision).
#[global] Instance mpsc_queue_1_name_countable :
Countable mpsc_queue_1_name.
#[local] Definition history_auth' γ_history hist :=
mono_list_auth γ_history (DfracOwn 1) hist.
#[local] Definition history_auth γ hist :=
history_auth' γ.(mpsc_queue_1_name_history) hist.
#[local] Definition history_at γ i node :=
mono_list_at γ.(mpsc_queue_1_name_history) i node.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ vs :=
model₁' γ.(mpsc_queue_1_name_model) vs.
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ vs :=
model₂' γ.(mpsc_queue_1_name_model) vs.
#[local] Definition node_model γ node i : iProp Σ :=
node ↦ₕ Header §Node 2 ∗
history_at γ i node.
#[local] Instance : CustomIpat "node_model" :=
" ( #H{}_header & #Hhistory_at_{} ) ".
#[local] Definition inv_inner t γ : iProp Σ :=
∃ hist past front nodes back vs,
⌜hist = past ++ front :: nodes⌝ ∗
⌜back ∈ hist⌝ ∗
t.[front] ↦{#1/4} #front ∗
t.[back] ↦ #back ∗
xtchain (Header §Node 2) (DfracOwn 1) hist §Null ∗
([∗ list] node; v ∈ nodes; vs, node.[data] ↦ v) ∗
history_auth γ hist ∗
model₂ γ vs.
#[local] Instance : CustomIpat "inv_inner" :=
" ( %hist{} & %past{} & %front{} & %nodes{} & %back{} & %vs{} & >%Hhist{} & >%Hback{} & >Ht_front & >Ht_back & >Hhist & >Hnodes & >Hhistory_auth & >Hmodel₂ ) ".
#[local] Definition inv' t γ :=
inv γ.(mpsc_queue_1_name_inv) (inv_inner t γ).
Definition mpsc_queue_1_inv t γ ι : iProp Σ :=
⌜ι = γ.(mpsc_queue_1_name_inv)⌝ ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & #Hinv ) ".
Definition mpsc_queue_1_model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
#[local] Definition consumer_1 t front : iProp Σ :=
t.[front] ↦{#3/4} #front.
#[local] Definition consumer_2 t : iProp Σ :=
∃ front,
consumer_1 t front.
#[local] Instance : CustomIpat "consumer_2" :=
" ( %front{} & Hconsumer{_{}} ) ".
Definition mpsc_queue_1_consumer :=
consumer_2.
#[local] Instance : CustomIpat "consumer" :=
" (:consumer_2) ".
#[global] Instance mpsc_queue_1_model_timeless γ vs :
Timeless (mpsc_queue_1_model γ vs).
#[global] Instance mpsc_queue_1_consumer_timeless t :
Timeless (mpsc_queue_1_consumer t).
#[global] Instance mpsc_queue_1_inv_persistent t γ ι :
Persistent (mpsc_queue_1_inv t γ ι).
#[local] Lemma history_alloc front :
⊢ |==>
∃ γ_history,
history_auth' γ_history [front].
#[local] Lemma history_at_get {γ hist} i node :
hist !! i = Some node →
history_auth γ hist ⊢
history_at γ i node.
#[local] Lemma history_at_lookup γ hist i node :
history_auth γ hist -∗
history_at γ i node -∗
⌜hist !! i = Some node⌝.
#[local] Lemma history_update {γ hist} node :
history_auth γ hist ⊢ |==>
history_auth γ (hist ++ [node]) ∗
history_at γ (length hist) node.
#[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 inv_inner_history_at t γ front :
inv' t γ -∗
consumer_1 t front ={⊤}=∗
∃ i,
consumer_1 t front ∗
node_model γ front i.
Lemma mpsc_queue_1_model_exclusive γ vs1 vs2 :
mpsc_queue_1_model γ vs1 -∗
mpsc_queue_1_model γ vs2 -∗
False.
Lemma mpsc_queue_1_consumer_exclusive t :
mpsc_queue_1_consumer t -∗
mpsc_queue_1_consumer t -∗
False.
Lemma mpsc_queue_1٠create𑁒spec ι :
{{{
True
}}}
mpsc_queue_1٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
mpsc_queue_1_inv t γ ι ∗
mpsc_queue_1_model γ [] ∗
mpsc_queue_1_consumer t
}}}.
#[local] Lemma mpsc_queue_1٠front𑁒spec t γ :
{{{
inv' t γ
}}}
(#t).{front}
{{{
front i
, RET #front;
node_model γ front i
}}}.
#[local] Lemma back𑁒spec t γ :
{{{
inv' t γ
}}}
(#t).{back}
{{{
back i
, RET #back;
node_model γ back i
}}}.
Variant operation :=
| IsEmpty (Ψ : bool → iProp Σ)
| Pop (Ψ : option val → iProp Σ)
| Other.
Implicit Types op : operation.
Variant operation' :=
| IsEmpty'
| Pop'
| Other'.
#[local] Instance operation'_eq_dec : EqDecision operation' :=
ltac:(solve_decision).
#[local] Coercion operation_to_operation' op :=
match op with
| IsEmpty _ ⇒
IsEmpty'
| Pop _ ⇒
Pop'
| Other ⇒
Other'
end.
#[local] Definition is_empty_au γ (Ψ : bool → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(mpsc_queue_1_name_inv), ∅ <{
model₁ γ vs
, COMM
Ψ (bool_decide (vs = []))
}>.
#[local] Definition pop_au γ (Ψ : option val → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(mpsc_queue_1_name_inv), ∅ <{
model₁ γ (tail vs)
, COMM
Ψ (head vs)
}>.
#[local] Lemma next𑁒spec_aux op t γ i node :
{{{
inv' t γ ∗
history_at γ i node ∗
( if decide (op = Other' :> operation') then True else
consumer_1 t node
) ∗
match op with
| IsEmpty Ψ ⇒
is_empty_au γ Ψ
| Pop Ψ ⇒
pop_au γ Ψ
| Other ⇒
True
end
}}}
(#node).{next}
{{{
res
, RET res;
( if decide (op = Other' :> operation') then True else
consumer_1 t node
) ∗
( ⌜res = §Null%V⌝ ∗
match op with
| IsEmpty Ψ ⇒
Ψ true
| Pop Ψ ⇒
Ψ None
| Other ⇒
True
end
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) ∗
match op with
| IsEmpty Ψ ⇒
Ψ false
| Pop Ψ ⇒
pop_au γ Ψ
| Other ⇒
True
end
)
}}}.
#[local] Lemma next𑁒spec {t γ i} node :
{{{
inv' t γ ∗
history_at γ i node
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i)
}}}.
#[local] Lemma next𑁒spec_is_empty {t γ i node} Ψ :
{{{
inv' t γ ∗
history_at γ i node ∗
consumer_1 t node ∗
is_empty_au γ Ψ
}}}
(#node).{next}
{{{
res
, RET res;
consumer_1 t node ∗
( ⌜res = §Null%V⌝ ∗
Ψ true
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) ∗
Ψ false
)
}}}.
#[local] Lemma next𑁒spec_pop {t γ i node} Ψ :
{{{
inv' t γ ∗
history_at γ i node ∗
consumer_1 t node ∗
pop_au γ Ψ
}}}
(#node).{next}
{{{
res
, RET res;
consumer_1 t node ∗
( ⌜res = §Null%V⌝ ∗
Ψ None
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) ∗
pop_au γ Ψ
)
}}}.
Lemma mpsc_queue_1٠is_empty𑁒spec t γ ι :
<<<
mpsc_queue_1_inv t γ ι ∗
mpsc_queue_1_consumer t
| ∀∀ vs,
mpsc_queue_1_model γ vs
>>>
mpsc_queue_1٠is_empty #t @ ↑ι
<<<
mpsc_queue_1_model γ vs
| RET #(bool_decide (vs = []%list));
mpsc_queue_1_consumer t
>>>.
#[local] Lemma mpsc_queue_1٠push₀𑁒spec t γ i node new_back v :
<<<
inv' t γ ∗
node_model γ node i ∗
new_back ↦ₕ Header §Node 2 ∗
new_back.[next] ↦ §Null ∗
new_back.[data] ↦ v
| ∀∀ vs,
mpsc_queue_1_model γ vs
>>>
mpsc_queue_1٠push₀ #node #new_back @ ↑γ.(mpsc_queue_1_name_inv)
<<<
mpsc_queue_1_model γ (vs ++ [v])
| RET ();
∃ j,
history_at γ j new_back
>>>.
#[local] Lemma mpsc_queue_1٠fix_back𑁒spec t γ i back j new_back :
{{{
inv' t γ ∗
history_at γ i back ∗
node_model γ new_back j
}}}
mpsc_queue_1٠fix_back #t #back #new_back
{{{
RET ();
True
}}}.
Lemma mpsc_queue_1٠push𑁒spec t γ ι v :
<<<
mpsc_queue_1_inv t γ ι
| ∀∀ vs,
mpsc_queue_1_model γ vs
>>>
mpsc_queue_1٠push #t v @ ↑ι
<<<
mpsc_queue_1_model γ (vs ++ [v])
| RET ();
True
>>>.
#[local] Lemma mpsc_queue_1٠pop𑁒spec_aux t γ :
<<<
inv' t γ ∗
consumer_2 t
| ∀∀ vs,
model₁ γ vs
>>>
mpsc_queue_1٠pop #t @ ↑γ.(mpsc_queue_1_name_inv)
<<<
model₁ γ (tail vs)
| RET head vs;
consumer_2 t
>>>.
Lemma mpsc_queue_1٠pop𑁒spec t γ ι :
<<<
mpsc_queue_1_inv t γ ι ∗
mpsc_queue_1_consumer t
| ∀∀ vs,
mpsc_queue_1_model γ vs
>>>
mpsc_queue_1٠pop #t @ ↑ι
<<<
mpsc_queue_1_model γ (tail vs)
| RET head vs;
mpsc_queue_1_consumer t
>>>.
End mpsc_queue_1_G.
#[global] Opaque mpsc_queue_1_inv.
#[global] Opaque mpsc_queue_1_model.
#[global] Opaque mpsc_queue_1_consumer.
End base.
From zoo_saturn Require
mpsc_queue_1__opaque.
Section mpsc_queue_1_G.
Context `{mpsc_queue_1_G : MpscQueue1G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition mpsc_queue_1_inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpsc_queue_1_inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition mpsc_queue_1_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpsc_queue_1_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition mpsc_queue_1_consumer t : iProp Σ :=
∃ 𝑡,
⌜t = #𝑡⌝ ∗
base.mpsc_queue_1_consumer 𝑡.
#[local] Instance : CustomIpat "consumer" :=
" ( %𝑡{} & {%Heq{};->} & Hconsumer{_{}} ) ".
#[global] Instance mpsc_queue_1_model_timeless t vs :
Timeless (mpsc_queue_1_model t vs).
#[global] Instance mpsc_queue_1_consumer_timeless t :
Timeless (mpsc_queue_1_consumer t ).
#[global] Instance mpsc_queue_1_inv_persistent t ι :
Persistent (mpsc_queue_1_inv t ι).
Lemma mpsc_queue_1_model_exclusive t vs1 vs2 :
mpsc_queue_1_model t vs1 -∗
mpsc_queue_1_model t vs2 -∗
False.
Lemma mpsc_queue_1_consumer_exclusive t :
mpsc_queue_1_consumer t -∗
mpsc_queue_1_consumer t -∗
False.
Lemma mpsc_queue_1٠create𑁒spec ι :
{{{
True
}}}
mpsc_queue_1٠create ()
{{{
t
, RET t;
mpsc_queue_1_inv t ι ∗
mpsc_queue_1_model t [] ∗
mpsc_queue_1_consumer t
}}}.
Lemma mpsc_queue_1٠is_empty𑁒spec t ι :
<<<
mpsc_queue_1_inv t ι ∗
mpsc_queue_1_consumer t
| ∀∀ vs,
mpsc_queue_1_model t vs
>>>
mpsc_queue_1٠is_empty t @ ↑ι
<<<
mpsc_queue_1_model t vs
| RET #(bool_decide (vs = []%list));
mpsc_queue_1_consumer t
>>>.
Lemma mpsc_queue_1٠push𑁒spec t ι v :
<<<
mpsc_queue_1_inv t ι
| ∀∀ vs,
mpsc_queue_1_model t vs
>>>
mpsc_queue_1٠push t v @ ↑ι
<<<
mpsc_queue_1_model t (vs ++ [v])
| RET ();
True
>>>.
Lemma mpsc_queue_1٠pop𑁒spec t ι :
<<<
mpsc_queue_1_inv t ι ∗
mpsc_queue_1_consumer t
| ∀∀ vs,
mpsc_queue_1_model t vs
>>>
mpsc_queue_1٠pop t @ ↑ι
<<<
mpsc_queue_1_model t (tail vs)
| RET head vs;
mpsc_queue_1_consumer t
>>>.
End mpsc_queue_1_G.
#[global] Opaque mpsc_queue_1_inv.
#[global] Opaque mpsc_queue_1_model.
#[global] Opaque mpsc_queue_1_consumer.
prelude.
From zoo.common Require Import
countable.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.mono_list
lib.twins.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
xtchain
domain.
From zoo_saturn Require Export
base
mpsc_queue_1__code.
From zoo_saturn Require Import
mpsc_queue_1__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types front node back new_back : location.
Implicit Types hist past nodes : list location.
Implicit Types v : val.
Implicit Types o : option val.
Implicit Types vs : list val.
Class MpscQueue1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] mpsc_queue_1_G_history_G :: MonoListG Σ location
; #[local] mpsc_queue_1_G_model_G :: TwinsG Σ (leibnizO (list val))
}.
Definition mpsc_queue_1_Σ :=
#[mono_list_Σ location
; twins_Σ (leibnizO (list val))
].
#[global] Instance subG_mpsc_queue_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG mpsc_queue_1_Σ Σ →
MpscQueue1G Σ.
Module base.
Section mpsc_queue_1_G.
Context `{mpsc_queue_1_G : MpscQueue1G Σ}.
Implicit Types t : location.
Record mpsc_queue_1_name :=
{ mpsc_queue_1_name_inv : namespace
; mpsc_queue_1_name_history : gname
; mpsc_queue_1_name_model : gname
}.
Implicit Type γ : mpsc_queue_1_name.
#[global] Instance mpsc_queue_1_name_eq_dec : EqDecision mpsc_queue_1_name :=
ltac:(solve_decision).
#[global] Instance mpsc_queue_1_name_countable :
Countable mpsc_queue_1_name.
#[local] Definition history_auth' γ_history hist :=
mono_list_auth γ_history (DfracOwn 1) hist.
#[local] Definition history_auth γ hist :=
history_auth' γ.(mpsc_queue_1_name_history) hist.
#[local] Definition history_at γ i node :=
mono_list_at γ.(mpsc_queue_1_name_history) i node.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ vs :=
model₁' γ.(mpsc_queue_1_name_model) vs.
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ vs :=
model₂' γ.(mpsc_queue_1_name_model) vs.
#[local] Definition node_model γ node i : iProp Σ :=
node ↦ₕ Header §Node 2 ∗
history_at γ i node.
#[local] Instance : CustomIpat "node_model" :=
" ( #H{}_header & #Hhistory_at_{} ) ".
#[local] Definition inv_inner t γ : iProp Σ :=
∃ hist past front nodes back vs,
⌜hist = past ++ front :: nodes⌝ ∗
⌜back ∈ hist⌝ ∗
t.[front] ↦{#1/4} #front ∗
t.[back] ↦ #back ∗
xtchain (Header §Node 2) (DfracOwn 1) hist §Null ∗
([∗ list] node; v ∈ nodes; vs, node.[data] ↦ v) ∗
history_auth γ hist ∗
model₂ γ vs.
#[local] Instance : CustomIpat "inv_inner" :=
" ( %hist{} & %past{} & %front{} & %nodes{} & %back{} & %vs{} & >%Hhist{} & >%Hback{} & >Ht_front & >Ht_back & >Hhist & >Hnodes & >Hhistory_auth & >Hmodel₂ ) ".
#[local] Definition inv' t γ :=
inv γ.(mpsc_queue_1_name_inv) (inv_inner t γ).
Definition mpsc_queue_1_inv t γ ι : iProp Σ :=
⌜ι = γ.(mpsc_queue_1_name_inv)⌝ ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & #Hinv ) ".
Definition mpsc_queue_1_model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
#[local] Definition consumer_1 t front : iProp Σ :=
t.[front] ↦{#3/4} #front.
#[local] Definition consumer_2 t : iProp Σ :=
∃ front,
consumer_1 t front.
#[local] Instance : CustomIpat "consumer_2" :=
" ( %front{} & Hconsumer{_{}} ) ".
Definition mpsc_queue_1_consumer :=
consumer_2.
#[local] Instance : CustomIpat "consumer" :=
" (:consumer_2) ".
#[global] Instance mpsc_queue_1_model_timeless γ vs :
Timeless (mpsc_queue_1_model γ vs).
#[global] Instance mpsc_queue_1_consumer_timeless t :
Timeless (mpsc_queue_1_consumer t).
#[global] Instance mpsc_queue_1_inv_persistent t γ ι :
Persistent (mpsc_queue_1_inv t γ ι).
#[local] Lemma history_alloc front :
⊢ |==>
∃ γ_history,
history_auth' γ_history [front].
#[local] Lemma history_at_get {γ hist} i node :
hist !! i = Some node →
history_auth γ hist ⊢
history_at γ i node.
#[local] Lemma history_at_lookup γ hist i node :
history_auth γ hist -∗
history_at γ i node -∗
⌜hist !! i = Some node⌝.
#[local] Lemma history_update {γ hist} node :
history_auth γ hist ⊢ |==>
history_auth γ (hist ++ [node]) ∗
history_at γ (length hist) node.
#[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 inv_inner_history_at t γ front :
inv' t γ -∗
consumer_1 t front ={⊤}=∗
∃ i,
consumer_1 t front ∗
node_model γ front i.
Lemma mpsc_queue_1_model_exclusive γ vs1 vs2 :
mpsc_queue_1_model γ vs1 -∗
mpsc_queue_1_model γ vs2 -∗
False.
Lemma mpsc_queue_1_consumer_exclusive t :
mpsc_queue_1_consumer t -∗
mpsc_queue_1_consumer t -∗
False.
Lemma mpsc_queue_1٠create𑁒spec ι :
{{{
True
}}}
mpsc_queue_1٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
mpsc_queue_1_inv t γ ι ∗
mpsc_queue_1_model γ [] ∗
mpsc_queue_1_consumer t
}}}.
#[local] Lemma mpsc_queue_1٠front𑁒spec t γ :
{{{
inv' t γ
}}}
(#t).{front}
{{{
front i
, RET #front;
node_model γ front i
}}}.
#[local] Lemma back𑁒spec t γ :
{{{
inv' t γ
}}}
(#t).{back}
{{{
back i
, RET #back;
node_model γ back i
}}}.
Variant operation :=
| IsEmpty (Ψ : bool → iProp Σ)
| Pop (Ψ : option val → iProp Σ)
| Other.
Implicit Types op : operation.
Variant operation' :=
| IsEmpty'
| Pop'
| Other'.
#[local] Instance operation'_eq_dec : EqDecision operation' :=
ltac:(solve_decision).
#[local] Coercion operation_to_operation' op :=
match op with
| IsEmpty _ ⇒
IsEmpty'
| Pop _ ⇒
Pop'
| Other ⇒
Other'
end.
#[local] Definition is_empty_au γ (Ψ : bool → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(mpsc_queue_1_name_inv), ∅ <{
model₁ γ vs
, COMM
Ψ (bool_decide (vs = []))
}>.
#[local] Definition pop_au γ (Ψ : option val → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(mpsc_queue_1_name_inv), ∅ <{
model₁ γ (tail vs)
, COMM
Ψ (head vs)
}>.
#[local] Lemma next𑁒spec_aux op t γ i node :
{{{
inv' t γ ∗
history_at γ i node ∗
( if decide (op = Other' :> operation') then True else
consumer_1 t node
) ∗
match op with
| IsEmpty Ψ ⇒
is_empty_au γ Ψ
| Pop Ψ ⇒
pop_au γ Ψ
| Other ⇒
True
end
}}}
(#node).{next}
{{{
res
, RET res;
( if decide (op = Other' :> operation') then True else
consumer_1 t node
) ∗
( ⌜res = §Null%V⌝ ∗
match op with
| IsEmpty Ψ ⇒
Ψ true
| Pop Ψ ⇒
Ψ None
| Other ⇒
True
end
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) ∗
match op with
| IsEmpty Ψ ⇒
Ψ false
| Pop Ψ ⇒
pop_au γ Ψ
| Other ⇒
True
end
)
}}}.
#[local] Lemma next𑁒spec {t γ i} node :
{{{
inv' t γ ∗
history_at γ i node
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i)
}}}.
#[local] Lemma next𑁒spec_is_empty {t γ i node} Ψ :
{{{
inv' t γ ∗
history_at γ i node ∗
consumer_1 t node ∗
is_empty_au γ Ψ
}}}
(#node).{next}
{{{
res
, RET res;
consumer_1 t node ∗
( ⌜res = §Null%V⌝ ∗
Ψ true
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) ∗
Ψ false
)
}}}.
#[local] Lemma next𑁒spec_pop {t γ i node} Ψ :
{{{
inv' t γ ∗
history_at γ i node ∗
consumer_1 t node ∗
pop_au γ Ψ
}}}
(#node).{next}
{{{
res
, RET res;
consumer_1 t node ∗
( ⌜res = §Null%V⌝ ∗
Ψ None
∨ ∃ node',
⌜res = #node'⌝ ∗
node_model γ node' (S i) ∗
pop_au γ Ψ
)
}}}.
Lemma mpsc_queue_1٠is_empty𑁒spec t γ ι :
<<<
mpsc_queue_1_inv t γ ι ∗
mpsc_queue_1_consumer t
| ∀∀ vs,
mpsc_queue_1_model γ vs
>>>
mpsc_queue_1٠is_empty #t @ ↑ι
<<<
mpsc_queue_1_model γ vs
| RET #(bool_decide (vs = []%list));
mpsc_queue_1_consumer t
>>>.
#[local] Lemma mpsc_queue_1٠push₀𑁒spec t γ i node new_back v :
<<<
inv' t γ ∗
node_model γ node i ∗
new_back ↦ₕ Header §Node 2 ∗
new_back.[next] ↦ §Null ∗
new_back.[data] ↦ v
| ∀∀ vs,
mpsc_queue_1_model γ vs
>>>
mpsc_queue_1٠push₀ #node #new_back @ ↑γ.(mpsc_queue_1_name_inv)
<<<
mpsc_queue_1_model γ (vs ++ [v])
| RET ();
∃ j,
history_at γ j new_back
>>>.
#[local] Lemma mpsc_queue_1٠fix_back𑁒spec t γ i back j new_back :
{{{
inv' t γ ∗
history_at γ i back ∗
node_model γ new_back j
}}}
mpsc_queue_1٠fix_back #t #back #new_back
{{{
RET ();
True
}}}.
Lemma mpsc_queue_1٠push𑁒spec t γ ι v :
<<<
mpsc_queue_1_inv t γ ι
| ∀∀ vs,
mpsc_queue_1_model γ vs
>>>
mpsc_queue_1٠push #t v @ ↑ι
<<<
mpsc_queue_1_model γ (vs ++ [v])
| RET ();
True
>>>.
#[local] Lemma mpsc_queue_1٠pop𑁒spec_aux t γ :
<<<
inv' t γ ∗
consumer_2 t
| ∀∀ vs,
model₁ γ vs
>>>
mpsc_queue_1٠pop #t @ ↑γ.(mpsc_queue_1_name_inv)
<<<
model₁ γ (tail vs)
| RET head vs;
consumer_2 t
>>>.
Lemma mpsc_queue_1٠pop𑁒spec t γ ι :
<<<
mpsc_queue_1_inv t γ ι ∗
mpsc_queue_1_consumer t
| ∀∀ vs,
mpsc_queue_1_model γ vs
>>>
mpsc_queue_1٠pop #t @ ↑ι
<<<
mpsc_queue_1_model γ (tail vs)
| RET head vs;
mpsc_queue_1_consumer t
>>>.
End mpsc_queue_1_G.
#[global] Opaque mpsc_queue_1_inv.
#[global] Opaque mpsc_queue_1_model.
#[global] Opaque mpsc_queue_1_consumer.
End base.
From zoo_saturn Require
mpsc_queue_1__opaque.
Section mpsc_queue_1_G.
Context `{mpsc_queue_1_G : MpscQueue1G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition mpsc_queue_1_inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpsc_queue_1_inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition mpsc_queue_1_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpsc_queue_1_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
Definition mpsc_queue_1_consumer t : iProp Σ :=
∃ 𝑡,
⌜t = #𝑡⌝ ∗
base.mpsc_queue_1_consumer 𝑡.
#[local] Instance : CustomIpat "consumer" :=
" ( %𝑡{} & {%Heq{};->} & Hconsumer{_{}} ) ".
#[global] Instance mpsc_queue_1_model_timeless t vs :
Timeless (mpsc_queue_1_model t vs).
#[global] Instance mpsc_queue_1_consumer_timeless t :
Timeless (mpsc_queue_1_consumer t ).
#[global] Instance mpsc_queue_1_inv_persistent t ι :
Persistent (mpsc_queue_1_inv t ι).
Lemma mpsc_queue_1_model_exclusive t vs1 vs2 :
mpsc_queue_1_model t vs1 -∗
mpsc_queue_1_model t vs2 -∗
False.
Lemma mpsc_queue_1_consumer_exclusive t :
mpsc_queue_1_consumer t -∗
mpsc_queue_1_consumer t -∗
False.
Lemma mpsc_queue_1٠create𑁒spec ι :
{{{
True
}}}
mpsc_queue_1٠create ()
{{{
t
, RET t;
mpsc_queue_1_inv t ι ∗
mpsc_queue_1_model t [] ∗
mpsc_queue_1_consumer t
}}}.
Lemma mpsc_queue_1٠is_empty𑁒spec t ι :
<<<
mpsc_queue_1_inv t ι ∗
mpsc_queue_1_consumer t
| ∀∀ vs,
mpsc_queue_1_model t vs
>>>
mpsc_queue_1٠is_empty t @ ↑ι
<<<
mpsc_queue_1_model t vs
| RET #(bool_decide (vs = []%list));
mpsc_queue_1_consumer t
>>>.
Lemma mpsc_queue_1٠push𑁒spec t ι v :
<<<
mpsc_queue_1_inv t ι
| ∀∀ vs,
mpsc_queue_1_model t vs
>>>
mpsc_queue_1٠push t v @ ↑ι
<<<
mpsc_queue_1_model t (vs ++ [v])
| RET ();
True
>>>.
Lemma mpsc_queue_1٠pop𑁒spec t ι :
<<<
mpsc_queue_1_inv t ι ∗
mpsc_queue_1_consumer t
| ∀∀ vs,
mpsc_queue_1_model t vs
>>>
mpsc_queue_1٠pop t @ ↑ι
<<<
mpsc_queue_1_model t (tail vs)
| RET head vs;
mpsc_queue_1_consumer t
>>>.
End mpsc_queue_1_G.
#[global] Opaque mpsc_queue_1_inv.
#[global] Opaque mpsc_queue_1_model.
#[global] Opaque mpsc_queue_1_consumer.