Library zoo_saturn.bqueue_mpmc
Require Import iris.base_logic.lib.ghost_map.
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.list.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.iris.base_logic.lib.auth_nat_max.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.base_logic.lib.saved_pred.
Require Import zoo.base.
Require Import zoo.program_logic.prophet_typed.
Require Import zoo_std.option.
Require Import zoo_std.xtchain.
Require Export zoo_saturn.bqueue_mpmc__code.
Require Import zoo_saturn.bqueue_mpmc__types.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type front node back new_back : location.
Implicit Type hist past nodes : list location.
Implicit Type v : val.
Implicit Type vs : list val.
Implicit Type waiter : gname.
Implicit Type waiters : gmap gname nat.
#[local] Definition prophet :=
{|prophet_typed₁۰type :=
location
; prophet_typed₁۰of_val v _ :=
match v with
| ValLoc l ⇒
Some $ Some l
| _ ⇒
None
end
|}.
Class BqueueMpmcG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] bqueue_mpmc۰G۰history۰G :: MonoListG Σ location
; #[local] bqueue_mpmc۰G۰front۰G :: AuthNatMaxG Σ
; #[local] bqueue_mpmc۰G۰model۰G :: TwinsG Σ (leibnizO (list val))
; #[local] bqueue_mpmc۰G۰waiters۰G :: ghost_mapG Σ gname nat
; #[local] bqueue_mpmc۰G۰saved_pred۰G :: SavedPredG Σ bool;
}.
Definition bqueue_mpmc۰Σ :=
#[mono_list۰Σ location
; auth_nat_max۰Σ
; twins۰Σ (leibnizO (list val))
; ghost_mapΣ gname nat
; saved_pred۰Σ bool
].
#[global] Instance subGｰbqueue_mpmc۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG bqueue_mpmc۰Σ Σ →
BqueueMpmcG Σ.
Module base.
Section bqueue_mpmc۰G.
Context `{bqueue_mpmc۰G : BqueueMpmcG Σ}.
Implicit Type t : location.
Record bqueue_mpmc۰name :=
{ bqueue_mpmc۰name۰inv : namespace
; bqueue_mpmc۰name۰capacity : nat
; bqueue_mpmc۰name۰history : gname
; bqueue_mpmc۰name۰front : gname
; bqueue_mpmc۰name۰model : gname
; bqueue_mpmc۰name۰waiters : gname
}.
Implicit Type γ : bqueue_mpmc۰name.
#[global] Instance bqueue_mpmc۰nameｰeq_dec : EqDecision bqueue_mpmc۰name :=
ltac:(solve_decision).
#[global] Instance bqueue_mpmc۰nameｰcountable :
Countable bqueue_mpmc۰name.
#[local] Definition history۰auth' γ_history :=
mono_list۰auth γ_history (DfracOwn 1).
#[local] Definition history۰auth γ :=
history۰auth' γ.(bqueue_mpmc۰name۰history).
#[local] Definition history۰at γ :=
mono_list۰at γ.(bqueue_mpmc۰name۰history).
#[local] Definition front۰auth' γ_front :=
auth_nat_max۰auth γ_front (DfracOwn 1).
#[local] Definition front۰auth γ :=
front۰auth' γ.(bqueue_mpmc۰name۰front).
#[local] Definition front۰lb γ :=
auth_nat_max۰lb γ.(bqueue_mpmc۰name۰front).
#[local] Definition model₁' γ_model vs :=
twins۰twin₁ γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ :=
model₁' γ.(bqueue_mpmc۰name۰model).
#[local] Definition model₂' γ_model vs :=
twins۰twin₂ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(bqueue_mpmc۰name۰model).
#[local] Definition waiters۰auth' γ_waiters :=
ghost_map_auth γ_waiters 1.
#[local] Definition waiters۰auth γ :=
waiters۰auth' γ.(bqueue_mpmc۰name۰waiters).
#[local] Definition waiters۰at γ waiter :=
ghost_map_elem γ.(bqueue_mpmc۰name۰waiters) waiter (DfracOwn 1).
#[local] Definition node۰model γ node (i : nat) b : iProp Σ :=
node ↦ₕ Header §Node 4 ∗
node.[index] ↦□ #i ∗
history۰at γ i node ∗
if b then front۰lb γ i else True%I.
#[local] Instance : CustomIpat "node۰model" :=
" ( #H{}_header & #H{}_index & #Hhistory_at_{} & {{front}#Hfront_lb_{};_} ) ".
#[local] Definition waiter۰au γ (Ψ : bool → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(bqueue_mpmc۰name۰inv), ∅ <{
model₁ γ vs
, COMM
Ψ (bool_decide (vs = []))
}>.
#[local] Definition waiter۰model γ past waiter i : iProp Σ :=
∃ Ψ,
saved_pred waiter Ψ ∗
if decide (i < length past) then
Ψ false
else
waiter۰au γ Ψ.
#[local] Definition inv۰inner t γ : iProp Σ :=
∃ hist past front nodes back vs waiters,
⌜hist = past ++ front :: nodes⌝ ∗
⌜back ∈ hist⌝ ∗
t.[front] ↦ #front ∗
t.[back] ↦ #back ∗
xtchain (Header §Node 4) (DfracOwn 1) hist §Null ∗
( [∗ list] node; v ∈ nodes; vs,
node.[data] ↦ v
) ∗
( [∗ list] i ↦ node ∈ hist,
node.[index] ↦□ #i
) ∗
( [∗ list] i ↦ node ∈ hist,
∃ cap : nat,
node.[estimated_capacity] ↦ #cap ∗
⌜i + cap ≤ length past + γ.(bqueue_mpmc۰name۰capacity)⌝
) ∗
history۰auth γ hist ∗
front۰auth γ (length past) ∗
model₂ γ vs ∗
waiters۰auth γ waiters ∗
( [∗ map] waiter ↦ i ∈ waiters,
waiter۰model γ past waiter i
).
#[local] Instance : CustomIpat "inv۰inner" :=
" ( %hist{} & %past{} & %front{} & %nodes{} & %back{} & %vs{} & %waiters{} & >%Hhist{} & >%Hback{} & >Ht_front & >Ht_back & >Hhist & >Hnodes & >Hindices & >Hcapacities & >Hhistory_auth & >Hfront_auth & >Hmodel₂ & >Hwaiters_auth & Hwaiters ) ".
#[local] Definition inv' t γ :=
inv γ.(bqueue_mpmc۰name۰inv) (inv۰inner t γ).
Definition bqueue_mpmc۰inv t γ ι cap : iProp Σ :=
⌜ι = γ.(bqueue_mpmc۰name۰inv)⌝ ∗
⌜cap = γ.(bqueue_mpmc۰name۰capacity)⌝ ∗
t.[capacity] ↦□ #cap ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & -> & #Ht_capacity & #Hinv ) ".
Definition bqueue_mpmc۰model γ vs : iProp Σ :=
⌜length vs ≤ γ.(bqueue_mpmc۰name۰capacity)⌝ ∗
model₁ γ vs.
#[local] Instance : CustomIpat "model" :=
" ( % & Hmodel₁{_{}} ) ".
#[global] Instance bqueue_mpmc۰modelｰtimeless γ vs :
Timeless (bqueue_mpmc۰model γ vs).
#[global] Instance bqueue_mpmc۰invｰpersistent t γ ι cap :
Persistent (bqueue_mpmc۰inv t γ ι cap).
#[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ｰagree γ i node1 node2 :
history۰at γ i node1 -∗
history۰at γ i node2 -∗
⌜node1 = node2⌝.
#[local] Lemma history۰atｰlookup γ hist i node :
history۰auth γ hist -∗
history۰at γ i node -∗
⌜hist !! i = Some node⌝.
#[local] Lemma history۰atｰelem_of γ hist i node :
history۰auth γ hist -∗
history۰at γ i node -∗
⌜node ∈ hist⌝.
#[local] Lemma historyｰupdate {γ hist} node :
history۰auth γ hist ⊢ |==>
history۰auth γ (hist ++ [node]) ∗
history۰at γ (length hist) node.
#[local] Lemma frontｰalloc :
⊢ |==>
∃ γ_front,
front۰auth' γ_front 0.
#[local] Lemma front۰lbｰget γ i :
front۰auth γ i ⊢
front۰lb γ i.
#[local] Lemma front۰lbｰvalid γ i1 i2 :
front۰auth γ i1 -∗
front۰lb γ i2 -∗
⌜i2 ≤ i1⌝.
#[local] Lemma frontｰupdate {γ i} i' :
i ≤ i' →
front۰auth γ i ⊢ |==>
front۰auth γ i'.
#[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 waitersｰalloc :
⊢ |==>
∃ γ_waiters,
waiters۰auth' γ_waiters ∅.
#[local] Lemma waitersｰinsert {γ waiters} i Ψ :
waiters۰auth γ waiters ⊢ |==>
∃ waiter,
waiters۰auth γ (<[waiter := i]> waiters) ∗
saved_pred waiter Ψ ∗
waiters۰at γ waiter i.
#[local] Lemma waitersｰdelete γ waiters waiter i :
waiters۰auth γ waiters -∗
waiters۰at γ waiter i ==∗
⌜waiters !! waiter = Some i⌝ ∗
waiters۰auth γ (delete waiter waiters).
Lemma bqueue_mpmc۰modelｰvalid t γ ι cap vs :
bqueue_mpmc۰inv t γ ι cap -∗
bqueue_mpmc۰model γ vs -∗
⌜length vs ≤ cap⌝.
Lemma bqueue_mpmc۰modelｰexclusive γ vs1 vs2 :
bqueue_mpmc۰model γ vs1 -∗
bqueue_mpmc۰model γ vs2 -∗
False.
Lemma bqueue_mpmc٠createｰspec ι cap :
(0 ≤ cap)%Z →
{{{
True
}}}
bqueue_mpmc٠create #cap
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
bqueue_mpmc۰inv t γ ι ₊cap ∗
bqueue_mpmc۰model γ []
}}}.
Lemma bqueue_mpmc٠capacityｰspec t γ ι cap :
{{{
bqueue_mpmc۰inv t γ ι cap
}}}
bqueue_mpmc٠capacity #t
{{{
RET #cap;
True
}}}.
#[local] Lemma frontｰspecｰstrong Ψ t γ :
{{{
inv' t γ ∗
if Ψ is Some Ψ then
waiter۰au γ Ψ
else
True
}}}
(#t).{front}
{{{
front i
, RET #front;
node۰model γ front i true ∗
if Ψ is Some Ψ then
∃ waiter,
saved_pred waiter Ψ ∗
waiters۰at γ waiter i
else
True
}}}.
#[local] Lemma frontｰspec t γ :
{{{
inv' t γ
}}}
(#t).{front}
{{{
front i
, RET #front;
node۰model γ front i true
}}}.
#[local] Lemma backｰspec t γ :
{{{
inv' t γ
}}}
(#t).{back}
{{{
back i
, RET #back;
node۰model γ back i false
}}}.
Variant operation :=
| Size (i_front : nat) (Ψ : val → iProp Σ)
| IsEmpty waiter (Ψ : bool → iProp Σ)
| Pop (Ψ : option val → iProp Σ)
| Other.
Implicit Type op : operation.
Variant operation' :=
| Size'
| IsEmpty'
| Pop'
| Other'.
#[local] Instance operation'ｰeq_dec : EqDecision operation' :=
ltac:(solve_decision).
#[local] Coercion operation۰to_operation' op :=
match op with
| Size _ _ ⇒
Size'
| IsEmpty _ _ ⇒
IsEmpty'
| Pop _ ⇒
Pop'
| Other ⇒
Other'
end.
#[local] Definition size۰au γ Ψ : iProp Σ :=
AU <{
∃∃ vs,
bqueue_mpmc۰model γ vs
}> @ ⊤ ∖ ↑γ.(bqueue_mpmc۰name۰inv), ∅ <{
bqueue_mpmc۰model γ vs
, COMM
True -∗ Ψ #(length vs)
}>.
#[local] Definition pop۰au γ (Ψ : option val → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(bqueue_mpmc۰name۰inv), ∅ <{
model₁ γ (tail vs)
, COMM
True -∗ Ψ (head vs)
}>.
#[local] Lemma nextｰspecｰaux (next : option location) op t γ i node :
{{{
inv' t γ ∗
history۰at γ i node ∗
from_option (history۰at γ ˖i) True next ∗
match op with
| Size i_front Ψ ⇒
front۰lb γ i_front ∗
size۰au γ Ψ
| IsEmpty waiter Ψ ⇒
front۰lb γ i ∗
saved_pred waiter Ψ ∗
waiters۰at γ waiter i ∗
£ 1
| Pop Ψ ⇒
front۰lb γ i ∗
pop۰au γ Ψ
| Other ⇒
True
end
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
from_option (const False) True next ∗
match op with
| Size i_front Ψ ⇒
Ψ #(i - i_front)
∨ ∃ i_front',
front۰lb γ i_front' ∗
⌜i_front < i_front'⌝ ∗
size۰au γ Ψ
| IsEmpty waiter Ψ ⇒
Ψ true
| Pop Ψ ⇒
Ψ None
| _ ⇒
True
end
∨ ∃ node',
⌜res = #node'⌝ ∗
node۰model γ node' ˖i false ∗
⌜from_option (node' =.) True next⌝ ∗
match op with
| Size _ Ψ ⇒
size۰au γ Ψ
| IsEmpty waiter Ψ ⇒
Ψ 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' ˖i false
}}}.
#[local] Lemma nextｰspec' {t γ i} node next :
{{{
inv' t γ ∗
history۰at γ i node ∗
history۰at γ ˖i next
}}}
(#node).{next}
{{{
RET #next;
node۰model γ next ˖i false
}}}.
#[local] Lemma nextｰspecｰsize {t γ i node} i_front Ψ :
{{{
inv' t γ ∗
history۰at γ i node ∗
front۰lb γ i_front ∗
size۰au γ Ψ
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
( Ψ #(i - i_front)
∨ ∃ i_front',
front۰lb γ i_front' ∗
⌜i_front < i_front'⌝ ∗
size۰au γ Ψ
)
∨ ∃ node',
⌜res = #node'⌝ ∗
node۰model γ node' ˖i false ∗
size۰au γ Ψ
}}}.
#[local] Lemma nextｰspecｰis_empty {t γ i node} waiter Ψ :
{{{
inv' t γ ∗
history۰at γ i node ∗
front۰lb γ i ∗
saved_pred waiter Ψ ∗
waiters۰at γ waiter i ∗
£ 1
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
Ψ true
∨ ∃ node',
⌜res = #node'⌝ ∗
node۰model γ node' ˖i false ∗
Ψ false
}}}.
#[local] Lemma nextｰspecｰpop {t γ i node} Ψ :
{{{
inv' t γ ∗
history۰at γ i node ∗
front۰lb γ i ∗
pop۰au γ Ψ
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
Ψ None
∨ ∃ node',
⌜res = #node'⌝ ∗
node۰model γ node' ˖i false ∗
pop۰au γ Ψ
}}}.
Lemma bqueue_mpmc٠sizeｰspec t γ ι cap :
<<<
bqueue_mpmc۰inv t γ ι cap
| ∀∀ vs,
bqueue_mpmc۰model γ vs
>>>
bqueue_mpmc٠size #t @ ↑ι
<<<
bqueue_mpmc۰model γ vs
| RET #(length vs);
True
>>>.
Lemma bqueue_mpmc٠is_emptyｰspec t γ ι cap :
<<<
bqueue_mpmc۰inv t γ ι cap
| ∀∀ vs,
bqueue_mpmc۰model γ vs
>>>
bqueue_mpmc٠is_empty #t @ ↑ι
<<<
bqueue_mpmc۰model γ vs
| RET #(bool_decide (vs = []%list));
True
>>>.
#[local] Lemma bqueue_mpmc٠fix_backｰspec {t γ} i {back} j new_back :
{{{
inv' t γ ∗
history۰at γ i back ∗
node۰model γ new_back j false
}}}
bqueue_mpmc٠fix_back #t #back #new_back
{{{
RET ();
True
}}}.
#[local] Lemma bqueue_mpmc٠push_1_push_2ｰspec t γ new_back v :
⊢ (
∀ back i_back i_front (cap : Z),
<<<
t.[capacity] ↦□ #γ.(bqueue_mpmc۰name۰capacity) ∗
inv' t γ ∗
node۰model γ back i_back false ∗
front۰lb γ i_front ∗
⌜0 ≤ cap⌝%Z ∗
⌜i_back + cap ≤ i_front + γ.(bqueue_mpmc۰name۰capacity)⌝%Z ∗
new_back ↦ₕ Header §Node 4 ∗
new_back.[next] ↦ §Null ∗
new_back.[data] ↦ v ∗
new_back.[index] ↦- ∗
new_back.[estimated_capacity] ↦-
| ∀∀ vs,
⌜length vs ≤ γ.(bqueue_mpmc۰name۰capacity)⌝ ∗
model₁ γ vs
>>>
bqueue_mpmc٠push_1 #t #back #cap #new_back @ ↑γ.(bqueue_mpmc۰name۰inv)
<<<
∃∃ b,
⌜b = bool_decide (length vs < γ.(bqueue_mpmc۰name۰capacity))⌝ ∗
model₁ γ (if b then vs ++ [v] else vs)
| RET #b;
True
>>>
) ∧ (
∀ back i_back,
<<<
t.[capacity] ↦□ #γ.(bqueue_mpmc۰name۰capacity) ∗
inv' t γ ∗
node۰model γ back i_back false ∗
new_back ↦ₕ Header §Node 4 ∗
new_back.[next] ↦ §Null ∗
new_back.[data] ↦ v ∗
new_back.[index] ↦- ∗
new_back.[estimated_capacity] ↦-
| ∀∀ vs,
⌜length vs ≤ γ.(bqueue_mpmc۰name۰capacity)⌝ ∗
model₁ γ vs
>>>
bqueue_mpmc٠push_2 #t #back #new_back @ ↑γ.(bqueue_mpmc۰name۰inv)
<<<
∃∃ b,
⌜b = bool_decide (length vs < γ.(bqueue_mpmc۰name۰capacity))⌝ ∗
model₁ γ (if b then vs ++ [v] else vs)
| RET #b;
True
>>>
).
#[local] Lemma bqueue_mpmc٠push_2ｰspec t γ back i_back new_back v :
<<<
t.[capacity] ↦□ #γ.(bqueue_mpmc۰name۰capacity) ∗
inv' t γ ∗
node۰model γ back i_back false ∗
new_back ↦ₕ Header §Node 4 ∗
new_back.[next] ↦ §Null ∗
new_back.[data] ↦ v ∗
new_back.[index] ↦- ∗
new_back.[estimated_capacity] ↦-
| ∀∀ vs,
⌜length vs ≤ γ.(bqueue_mpmc۰name۰capacity)⌝ ∗
model₁ γ vs
>>>
bqueue_mpmc٠push_2 #t #back #new_back @ ↑γ.(bqueue_mpmc۰name۰inv)
<<<
∃∃ b,
⌜b = bool_decide (length vs < γ.(bqueue_mpmc۰name۰capacity))⌝ ∗
model₁ γ (if b then vs ++ [v] else vs)
| RET #b;
True
>>>.
Lemma bqueue_mpmc٠pushｰspec t γ ι cap v :
<<<
bqueue_mpmc۰inv t γ ι cap
| ∀∀ vs,
bqueue_mpmc۰model γ vs
>>>
bqueue_mpmc٠push #t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
bqueue_mpmc۰model γ (if b then vs ++ [v] else vs)
| RET #b;
True
>>>.
#[local] Lemma bqueue_mpmc٠popｰspecｰaux t γ :
<<<
inv' t γ
| ∀∀ vs,
model₁ γ vs
>>>
bqueue_mpmc٠pop #t @ ↑γ.(bqueue_mpmc۰name۰inv)
<<<
model₁ γ (tail vs)
| RET head vs;
True
>>>.
Lemma bqueue_mpmc٠popｰspec t γ ι cap :
<<<
bqueue_mpmc۰inv t γ ι cap
| ∀∀ vs,
bqueue_mpmc۰model γ vs
>>>
bqueue_mpmc٠pop #t @ ↑ι
<<<
bqueue_mpmc۰model γ (tail vs)
| RET head vs;
True
>>>.
End bqueue_mpmc۰G.
#[global] Opaque bqueue_mpmc۰inv.
#[global] Opaque bqueue_mpmc۰model.
End base.
Require zoo_saturn.bqueue_mpmc__opaque.
Section bqueue_mpmc۰G.
Context `{bqueue_mpmc۰G : BqueueMpmcG Σ}.
Implicit Type 𝑡 : location.
Implicit Type t : val.
Definition bqueue_mpmc۰inv t ι cap : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.bqueue_mpmc۰inv 𝑡 γ ι cap.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition bqueue_mpmc۰model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.bqueue_mpmc۰model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
#[global] Instance bqueue_mpmc۰modelｰtimeless t vs :
Timeless (bqueue_mpmc۰model t vs).
#[global] Instance bqueue_mpmc۰invｰpersistent t ι cap :
Persistent (bqueue_mpmc۰inv t ι cap).
Lemma bqueue_mpmc۰modelｰvalid t ι cap vs :
bqueue_mpmc۰inv t ι cap -∗
bqueue_mpmc۰model t vs -∗
⌜length vs ≤ cap⌝.
Lemma bqueue_mpmc۰modelｰexclusive t vs1 vs2 :
bqueue_mpmc۰model t vs1 -∗
bqueue_mpmc۰model t vs2 -∗
False.
Lemma bqueue_mpmc٠createｰspec ι cap :
(0 ≤ cap)%Z →
{{{
True
}}}
bqueue_mpmc٠create #cap
{{{
t
, RET t;
bqueue_mpmc۰inv t ι ₊cap ∗
bqueue_mpmc۰model t []
}}}.
Lemma bqueue_mpmc٠capacityｰspec t ι cap :
{{{
bqueue_mpmc۰inv t ι cap
}}}
bqueue_mpmc٠capacity t
{{{
RET #cap;
True
}}}.
Lemma bqueue_mpmc٠sizeｰspec t ι cap :
<<<
bqueue_mpmc۰inv t ι cap
| ∀∀ vs,
bqueue_mpmc۰model t vs
>>>
bqueue_mpmc٠size t @ ↑ι
<<<
bqueue_mpmc۰model t vs
| RET #(length vs);
True
>>>.
Lemma bqueue_mpmc٠is_emptyｰspec t ι cap :
<<<
bqueue_mpmc۰inv t ι cap
| ∀∀ vs,
bqueue_mpmc۰model t vs
>>>
bqueue_mpmc٠is_empty t @ ↑ι
<<<
bqueue_mpmc۰model t vs
| RET #(bool_decide (vs = []%list));
True
>>>.
Lemma bqueue_mpmc٠pushｰspec t ι cap v :
<<<
bqueue_mpmc۰inv t ι cap
| ∀∀ vs,
bqueue_mpmc۰model t vs
>>>
bqueue_mpmc٠push t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
bqueue_mpmc۰model t (if b then vs ++ [v] else vs)
| RET #b;
True
>>>.
Lemma bqueue_mpmc٠popｰspec t ι cap :
<<<
bqueue_mpmc۰inv t ι cap
| ∀∀ vs,
bqueue_mpmc۰model t vs
>>>
bqueue_mpmc٠pop t @ ↑ι
<<<
bqueue_mpmc۰model t (tail vs)
| RET head vs;
True
>>>.
End bqueue_mpmc۰G.
#[global] Opaque bqueue_mpmc۰inv.
#[global] Opaque bqueue_mpmc۰model.
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.list.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.mono_list.
Require Import zoo.iris.base_logic.lib.auth_nat_max.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.iris.base_logic.lib.saved_pred.
Require Import zoo.base.
Require Import zoo.program_logic.prophet_typed.
Require Import zoo_std.option.
Require Import zoo_std.xtchain.
Require Export zoo_saturn.bqueue_mpmc__code.
Require Import zoo_saturn.bqueue_mpmc__types.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type front node back new_back : location.
Implicit Type hist past nodes : list location.
Implicit Type v : val.
Implicit Type vs : list val.
Implicit Type waiter : gname.
Implicit Type waiters : gmap gname nat.
#[local] Definition prophet :=
{|prophet_typed₁۰type :=
location
; prophet_typed₁۰of_val v _ :=
match v with
| ValLoc l ⇒
Some $ Some l
| _ ⇒
None
end
|}.
Class BqueueMpmcG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] bqueue_mpmc۰G۰history۰G :: MonoListG Σ location
; #[local] bqueue_mpmc۰G۰front۰G :: AuthNatMaxG Σ
; #[local] bqueue_mpmc۰G۰model۰G :: TwinsG Σ (leibnizO (list val))
; #[local] bqueue_mpmc۰G۰waiters۰G :: ghost_mapG Σ gname nat
; #[local] bqueue_mpmc۰G۰saved_pred۰G :: SavedPredG Σ bool;
}.
Definition bqueue_mpmc۰Σ :=
#[mono_list۰Σ location
; auth_nat_max۰Σ
; twins۰Σ (leibnizO (list val))
; ghost_mapΣ gname nat
; saved_pred۰Σ bool
].
#[global] Instance subGｰbqueue_mpmc۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG bqueue_mpmc۰Σ Σ →
BqueueMpmcG Σ.
Module base.
Section bqueue_mpmc۰G.
Context `{bqueue_mpmc۰G : BqueueMpmcG Σ}.
Implicit Type t : location.
Record bqueue_mpmc۰name :=
{ bqueue_mpmc۰name۰inv : namespace
; bqueue_mpmc۰name۰capacity : nat
; bqueue_mpmc۰name۰history : gname
; bqueue_mpmc۰name۰front : gname
; bqueue_mpmc۰name۰model : gname
; bqueue_mpmc۰name۰waiters : gname
}.
Implicit Type γ : bqueue_mpmc۰name.
#[global] Instance bqueue_mpmc۰nameｰeq_dec : EqDecision bqueue_mpmc۰name :=
ltac:(solve_decision).
#[global] Instance bqueue_mpmc۰nameｰcountable :
Countable bqueue_mpmc۰name.
#[local] Definition history۰auth' γ_history :=
mono_list۰auth γ_history (DfracOwn 1).
#[local] Definition history۰auth γ :=
history۰auth' γ.(bqueue_mpmc۰name۰history).
#[local] Definition history۰at γ :=
mono_list۰at γ.(bqueue_mpmc۰name۰history).
#[local] Definition front۰auth' γ_front :=
auth_nat_max۰auth γ_front (DfracOwn 1).
#[local] Definition front۰auth γ :=
front۰auth' γ.(bqueue_mpmc۰name۰front).
#[local] Definition front۰lb γ :=
auth_nat_max۰lb γ.(bqueue_mpmc۰name۰front).
#[local] Definition model₁' γ_model vs :=
twins۰twin₁ γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ :=
model₁' γ.(bqueue_mpmc۰name۰model).
#[local] Definition model₂' γ_model vs :=
twins۰twin₂ γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(bqueue_mpmc۰name۰model).
#[local] Definition waiters۰auth' γ_waiters :=
ghost_map_auth γ_waiters 1.
#[local] Definition waiters۰auth γ :=
waiters۰auth' γ.(bqueue_mpmc۰name۰waiters).
#[local] Definition waiters۰at γ waiter :=
ghost_map_elem γ.(bqueue_mpmc۰name۰waiters) waiter (DfracOwn 1).
#[local] Definition node۰model γ node (i : nat) b : iProp Σ :=
node ↦ₕ Header §Node 4 ∗
node.[index] ↦□ #i ∗
history۰at γ i node ∗
if b then front۰lb γ i else True%I.
#[local] Instance : CustomIpat "node۰model" :=
" ( #H{}_header & #H{}_index & #Hhistory_at_{} & {{front}#Hfront_lb_{};_} ) ".
#[local] Definition waiter۰au γ (Ψ : bool → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(bqueue_mpmc۰name۰inv), ∅ <{
model₁ γ vs
, COMM
Ψ (bool_decide (vs = []))
}>.
#[local] Definition waiter۰model γ past waiter i : iProp Σ :=
∃ Ψ,
saved_pred waiter Ψ ∗
if decide (i < length past) then
Ψ false
else
waiter۰au γ Ψ.
#[local] Definition inv۰inner t γ : iProp Σ :=
∃ hist past front nodes back vs waiters,
⌜hist = past ++ front :: nodes⌝ ∗
⌜back ∈ hist⌝ ∗
t.[front] ↦ #front ∗
t.[back] ↦ #back ∗
xtchain (Header §Node 4) (DfracOwn 1) hist §Null ∗
( [∗ list] node; v ∈ nodes; vs,
node.[data] ↦ v
) ∗
( [∗ list] i ↦ node ∈ hist,
node.[index] ↦□ #i
) ∗
( [∗ list] i ↦ node ∈ hist,
∃ cap : nat,
node.[estimated_capacity] ↦ #cap ∗
⌜i + cap ≤ length past + γ.(bqueue_mpmc۰name۰capacity)⌝
) ∗
history۰auth γ hist ∗
front۰auth γ (length past) ∗
model₂ γ vs ∗
waiters۰auth γ waiters ∗
( [∗ map] waiter ↦ i ∈ waiters,
waiter۰model γ past waiter i
).
#[local] Instance : CustomIpat "inv۰inner" :=
" ( %hist{} & %past{} & %front{} & %nodes{} & %back{} & %vs{} & %waiters{} & >%Hhist{} & >%Hback{} & >Ht_front & >Ht_back & >Hhist & >Hnodes & >Hindices & >Hcapacities & >Hhistory_auth & >Hfront_auth & >Hmodel₂ & >Hwaiters_auth & Hwaiters ) ".
#[local] Definition inv' t γ :=
inv γ.(bqueue_mpmc۰name۰inv) (inv۰inner t γ).
Definition bqueue_mpmc۰inv t γ ι cap : iProp Σ :=
⌜ι = γ.(bqueue_mpmc۰name۰inv)⌝ ∗
⌜cap = γ.(bqueue_mpmc۰name۰capacity)⌝ ∗
t.[capacity] ↦□ #cap ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & -> & #Ht_capacity & #Hinv ) ".
Definition bqueue_mpmc۰model γ vs : iProp Σ :=
⌜length vs ≤ γ.(bqueue_mpmc۰name۰capacity)⌝ ∗
model₁ γ vs.
#[local] Instance : CustomIpat "model" :=
" ( % & Hmodel₁{_{}} ) ".
#[global] Instance bqueue_mpmc۰modelｰtimeless γ vs :
Timeless (bqueue_mpmc۰model γ vs).
#[global] Instance bqueue_mpmc۰invｰpersistent t γ ι cap :
Persistent (bqueue_mpmc۰inv t γ ι cap).
#[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ｰagree γ i node1 node2 :
history۰at γ i node1 -∗
history۰at γ i node2 -∗
⌜node1 = node2⌝.
#[local] Lemma history۰atｰlookup γ hist i node :
history۰auth γ hist -∗
history۰at γ i node -∗
⌜hist !! i = Some node⌝.
#[local] Lemma history۰atｰelem_of γ hist i node :
history۰auth γ hist -∗
history۰at γ i node -∗
⌜node ∈ hist⌝.
#[local] Lemma historyｰupdate {γ hist} node :
history۰auth γ hist ⊢ |==>
history۰auth γ (hist ++ [node]) ∗
history۰at γ (length hist) node.
#[local] Lemma frontｰalloc :
⊢ |==>
∃ γ_front,
front۰auth' γ_front 0.
#[local] Lemma front۰lbｰget γ i :
front۰auth γ i ⊢
front۰lb γ i.
#[local] Lemma front۰lbｰvalid γ i1 i2 :
front۰auth γ i1 -∗
front۰lb γ i2 -∗
⌜i2 ≤ i1⌝.
#[local] Lemma frontｰupdate {γ i} i' :
i ≤ i' →
front۰auth γ i ⊢ |==>
front۰auth γ i'.
#[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 waitersｰalloc :
⊢ |==>
∃ γ_waiters,
waiters۰auth' γ_waiters ∅.
#[local] Lemma waitersｰinsert {γ waiters} i Ψ :
waiters۰auth γ waiters ⊢ |==>
∃ waiter,
waiters۰auth γ (<[waiter := i]> waiters) ∗
saved_pred waiter Ψ ∗
waiters۰at γ waiter i.
#[local] Lemma waitersｰdelete γ waiters waiter i :
waiters۰auth γ waiters -∗
waiters۰at γ waiter i ==∗
⌜waiters !! waiter = Some i⌝ ∗
waiters۰auth γ (delete waiter waiters).
Lemma bqueue_mpmc۰modelｰvalid t γ ι cap vs :
bqueue_mpmc۰inv t γ ι cap -∗
bqueue_mpmc۰model γ vs -∗
⌜length vs ≤ cap⌝.
Lemma bqueue_mpmc۰modelｰexclusive γ vs1 vs2 :
bqueue_mpmc۰model γ vs1 -∗
bqueue_mpmc۰model γ vs2 -∗
False.
Lemma bqueue_mpmc٠createｰspec ι cap :
(0 ≤ cap)%Z →
{{{
True
}}}
bqueue_mpmc٠create #cap
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
bqueue_mpmc۰inv t γ ι ₊cap ∗
bqueue_mpmc۰model γ []
}}}.
Lemma bqueue_mpmc٠capacityｰspec t γ ι cap :
{{{
bqueue_mpmc۰inv t γ ι cap
}}}
bqueue_mpmc٠capacity #t
{{{
RET #cap;
True
}}}.
#[local] Lemma frontｰspecｰstrong Ψ t γ :
{{{
inv' t γ ∗
if Ψ is Some Ψ then
waiter۰au γ Ψ
else
True
}}}
(#t).{front}
{{{
front i
, RET #front;
node۰model γ front i true ∗
if Ψ is Some Ψ then
∃ waiter,
saved_pred waiter Ψ ∗
waiters۰at γ waiter i
else
True
}}}.
#[local] Lemma frontｰspec t γ :
{{{
inv' t γ
}}}
(#t).{front}
{{{
front i
, RET #front;
node۰model γ front i true
}}}.
#[local] Lemma backｰspec t γ :
{{{
inv' t γ
}}}
(#t).{back}
{{{
back i
, RET #back;
node۰model γ back i false
}}}.
Variant operation :=
| Size (i_front : nat) (Ψ : val → iProp Σ)
| IsEmpty waiter (Ψ : bool → iProp Σ)
| Pop (Ψ : option val → iProp Σ)
| Other.
Implicit Type op : operation.
Variant operation' :=
| Size'
| IsEmpty'
| Pop'
| Other'.
#[local] Instance operation'ｰeq_dec : EqDecision operation' :=
ltac:(solve_decision).
#[local] Coercion operation۰to_operation' op :=
match op with
| Size _ _ ⇒
Size'
| IsEmpty _ _ ⇒
IsEmpty'
| Pop _ ⇒
Pop'
| Other ⇒
Other'
end.
#[local] Definition size۰au γ Ψ : iProp Σ :=
AU <{
∃∃ vs,
bqueue_mpmc۰model γ vs
}> @ ⊤ ∖ ↑γ.(bqueue_mpmc۰name۰inv), ∅ <{
bqueue_mpmc۰model γ vs
, COMM
True -∗ Ψ #(length vs)
}>.
#[local] Definition pop۰au γ (Ψ : option val → iProp Σ) : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(bqueue_mpmc۰name۰inv), ∅ <{
model₁ γ (tail vs)
, COMM
True -∗ Ψ (head vs)
}>.
#[local] Lemma nextｰspecｰaux (next : option location) op t γ i node :
{{{
inv' t γ ∗
history۰at γ i node ∗
from_option (history۰at γ ˖i) True next ∗
match op with
| Size i_front Ψ ⇒
front۰lb γ i_front ∗
size۰au γ Ψ
| IsEmpty waiter Ψ ⇒
front۰lb γ i ∗
saved_pred waiter Ψ ∗
waiters۰at γ waiter i ∗
£ 1
| Pop Ψ ⇒
front۰lb γ i ∗
pop۰au γ Ψ
| Other ⇒
True
end
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
from_option (const False) True next ∗
match op with
| Size i_front Ψ ⇒
Ψ #(i - i_front)
∨ ∃ i_front',
front۰lb γ i_front' ∗
⌜i_front < i_front'⌝ ∗
size۰au γ Ψ
| IsEmpty waiter Ψ ⇒
Ψ true
| Pop Ψ ⇒
Ψ None
| _ ⇒
True
end
∨ ∃ node',
⌜res = #node'⌝ ∗
node۰model γ node' ˖i false ∗
⌜from_option (node' =.) True next⌝ ∗
match op with
| Size _ Ψ ⇒
size۰au γ Ψ
| IsEmpty waiter Ψ ⇒
Ψ 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' ˖i false
}}}.
#[local] Lemma nextｰspec' {t γ i} node next :
{{{
inv' t γ ∗
history۰at γ i node ∗
history۰at γ ˖i next
}}}
(#node).{next}
{{{
RET #next;
node۰model γ next ˖i false
}}}.
#[local] Lemma nextｰspecｰsize {t γ i node} i_front Ψ :
{{{
inv' t γ ∗
history۰at γ i node ∗
front۰lb γ i_front ∗
size۰au γ Ψ
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
( Ψ #(i - i_front)
∨ ∃ i_front',
front۰lb γ i_front' ∗
⌜i_front < i_front'⌝ ∗
size۰au γ Ψ
)
∨ ∃ node',
⌜res = #node'⌝ ∗
node۰model γ node' ˖i false ∗
size۰au γ Ψ
}}}.
#[local] Lemma nextｰspecｰis_empty {t γ i node} waiter Ψ :
{{{
inv' t γ ∗
history۰at γ i node ∗
front۰lb γ i ∗
saved_pred waiter Ψ ∗
waiters۰at γ waiter i ∗
£ 1
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
Ψ true
∨ ∃ node',
⌜res = #node'⌝ ∗
node۰model γ node' ˖i false ∗
Ψ false
}}}.
#[local] Lemma nextｰspecｰpop {t γ i node} Ψ :
{{{
inv' t γ ∗
history۰at γ i node ∗
front۰lb γ i ∗
pop۰au γ Ψ
}}}
(#node).{next}
{{{
res
, RET res;
⌜res = §Null%V⌝ ∗
Ψ None
∨ ∃ node',
⌜res = #node'⌝ ∗
node۰model γ node' ˖i false ∗
pop۰au γ Ψ
}}}.
Lemma bqueue_mpmc٠sizeｰspec t γ ι cap :
<<<
bqueue_mpmc۰inv t γ ι cap
| ∀∀ vs,
bqueue_mpmc۰model γ vs
>>>
bqueue_mpmc٠size #t @ ↑ι
<<<
bqueue_mpmc۰model γ vs
| RET #(length vs);
True
>>>.
Lemma bqueue_mpmc٠is_emptyｰspec t γ ι cap :
<<<
bqueue_mpmc۰inv t γ ι cap
| ∀∀ vs,
bqueue_mpmc۰model γ vs
>>>
bqueue_mpmc٠is_empty #t @ ↑ι
<<<
bqueue_mpmc۰model γ vs
| RET #(bool_decide (vs = []%list));
True
>>>.
#[local] Lemma bqueue_mpmc٠fix_backｰspec {t γ} i {back} j new_back :
{{{
inv' t γ ∗
history۰at γ i back ∗
node۰model γ new_back j false
}}}
bqueue_mpmc٠fix_back #t #back #new_back
{{{
RET ();
True
}}}.
#[local] Lemma bqueue_mpmc٠push_1_push_2ｰspec t γ new_back v :
⊢ (
∀ back i_back i_front (cap : Z),
<<<
t.[capacity] ↦□ #γ.(bqueue_mpmc۰name۰capacity) ∗
inv' t γ ∗
node۰model γ back i_back false ∗
front۰lb γ i_front ∗
⌜0 ≤ cap⌝%Z ∗
⌜i_back + cap ≤ i_front + γ.(bqueue_mpmc۰name۰capacity)⌝%Z ∗
new_back ↦ₕ Header §Node 4 ∗
new_back.[next] ↦ §Null ∗
new_back.[data] ↦ v ∗
new_back.[index] ↦- ∗
new_back.[estimated_capacity] ↦-
| ∀∀ vs,
⌜length vs ≤ γ.(bqueue_mpmc۰name۰capacity)⌝ ∗
model₁ γ vs
>>>
bqueue_mpmc٠push_1 #t #back #cap #new_back @ ↑γ.(bqueue_mpmc۰name۰inv)
<<<
∃∃ b,
⌜b = bool_decide (length vs < γ.(bqueue_mpmc۰name۰capacity))⌝ ∗
model₁ γ (if b then vs ++ [v] else vs)
| RET #b;
True
>>>
) ∧ (
∀ back i_back,
<<<
t.[capacity] ↦□ #γ.(bqueue_mpmc۰name۰capacity) ∗
inv' t γ ∗
node۰model γ back i_back false ∗
new_back ↦ₕ Header §Node 4 ∗
new_back.[next] ↦ §Null ∗
new_back.[data] ↦ v ∗
new_back.[index] ↦- ∗
new_back.[estimated_capacity] ↦-
| ∀∀ vs,
⌜length vs ≤ γ.(bqueue_mpmc۰name۰capacity)⌝ ∗
model₁ γ vs
>>>
bqueue_mpmc٠push_2 #t #back #new_back @ ↑γ.(bqueue_mpmc۰name۰inv)
<<<
∃∃ b,
⌜b = bool_decide (length vs < γ.(bqueue_mpmc۰name۰capacity))⌝ ∗
model₁ γ (if b then vs ++ [v] else vs)
| RET #b;
True
>>>
).
#[local] Lemma bqueue_mpmc٠push_2ｰspec t γ back i_back new_back v :
<<<
t.[capacity] ↦□ #γ.(bqueue_mpmc۰name۰capacity) ∗
inv' t γ ∗
node۰model γ back i_back false ∗
new_back ↦ₕ Header §Node 4 ∗
new_back.[next] ↦ §Null ∗
new_back.[data] ↦ v ∗
new_back.[index] ↦- ∗
new_back.[estimated_capacity] ↦-
| ∀∀ vs,
⌜length vs ≤ γ.(bqueue_mpmc۰name۰capacity)⌝ ∗
model₁ γ vs
>>>
bqueue_mpmc٠push_2 #t #back #new_back @ ↑γ.(bqueue_mpmc۰name۰inv)
<<<
∃∃ b,
⌜b = bool_decide (length vs < γ.(bqueue_mpmc۰name۰capacity))⌝ ∗
model₁ γ (if b then vs ++ [v] else vs)
| RET #b;
True
>>>.
Lemma bqueue_mpmc٠pushｰspec t γ ι cap v :
<<<
bqueue_mpmc۰inv t γ ι cap
| ∀∀ vs,
bqueue_mpmc۰model γ vs
>>>
bqueue_mpmc٠push #t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
bqueue_mpmc۰model γ (if b then vs ++ [v] else vs)
| RET #b;
True
>>>.
#[local] Lemma bqueue_mpmc٠popｰspecｰaux t γ :
<<<
inv' t γ
| ∀∀ vs,
model₁ γ vs
>>>
bqueue_mpmc٠pop #t @ ↑γ.(bqueue_mpmc۰name۰inv)
<<<
model₁ γ (tail vs)
| RET head vs;
True
>>>.
Lemma bqueue_mpmc٠popｰspec t γ ι cap :
<<<
bqueue_mpmc۰inv t γ ι cap
| ∀∀ vs,
bqueue_mpmc۰model γ vs
>>>
bqueue_mpmc٠pop #t @ ↑ι
<<<
bqueue_mpmc۰model γ (tail vs)
| RET head vs;
True
>>>.
End bqueue_mpmc۰G.
#[global] Opaque bqueue_mpmc۰inv.
#[global] Opaque bqueue_mpmc۰model.
End base.
Require zoo_saturn.bqueue_mpmc__opaque.
Section bqueue_mpmc۰G.
Context `{bqueue_mpmc۰G : BqueueMpmcG Σ}.
Implicit Type 𝑡 : location.
Implicit Type t : val.
Definition bqueue_mpmc۰inv t ι cap : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.bqueue_mpmc۰inv 𝑡 γ ι cap.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition bqueue_mpmc۰model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.bqueue_mpmc۰model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hmodel{_{}} ) ".
#[global] Instance bqueue_mpmc۰modelｰtimeless t vs :
Timeless (bqueue_mpmc۰model t vs).
#[global] Instance bqueue_mpmc۰invｰpersistent t ι cap :
Persistent (bqueue_mpmc۰inv t ι cap).
Lemma bqueue_mpmc۰modelｰvalid t ι cap vs :
bqueue_mpmc۰inv t ι cap -∗
bqueue_mpmc۰model t vs -∗
⌜length vs ≤ cap⌝.
Lemma bqueue_mpmc۰modelｰexclusive t vs1 vs2 :
bqueue_mpmc۰model t vs1 -∗
bqueue_mpmc۰model t vs2 -∗
False.
Lemma bqueue_mpmc٠createｰspec ι cap :
(0 ≤ cap)%Z →
{{{
True
}}}
bqueue_mpmc٠create #cap
{{{
t
, RET t;
bqueue_mpmc۰inv t ι ₊cap ∗
bqueue_mpmc۰model t []
}}}.
Lemma bqueue_mpmc٠capacityｰspec t ι cap :
{{{
bqueue_mpmc۰inv t ι cap
}}}
bqueue_mpmc٠capacity t
{{{
RET #cap;
True
}}}.
Lemma bqueue_mpmc٠sizeｰspec t ι cap :
<<<
bqueue_mpmc۰inv t ι cap
| ∀∀ vs,
bqueue_mpmc۰model t vs
>>>
bqueue_mpmc٠size t @ ↑ι
<<<
bqueue_mpmc۰model t vs
| RET #(length vs);
True
>>>.
Lemma bqueue_mpmc٠is_emptyｰspec t ι cap :
<<<
bqueue_mpmc۰inv t ι cap
| ∀∀ vs,
bqueue_mpmc۰model t vs
>>>
bqueue_mpmc٠is_empty t @ ↑ι
<<<
bqueue_mpmc۰model t vs
| RET #(bool_decide (vs = []%list));
True
>>>.
Lemma bqueue_mpmc٠pushｰspec t ι cap v :
<<<
bqueue_mpmc۰inv t ι cap
| ∀∀ vs,
bqueue_mpmc۰model t vs
>>>
bqueue_mpmc٠push t v @ ↑ι
<<<
∃∃ b,
⌜b = bool_decide (length vs < cap)⌝ ∗
bqueue_mpmc۰model t (if b then vs ++ [v] else vs)
| RET #b;
True
>>>.
Lemma bqueue_mpmc٠popｰspec t ι cap :
<<<
bqueue_mpmc۰inv t ι cap
| ∀∀ vs,
bqueue_mpmc۰model t vs
>>>
bqueue_mpmc٠pop t @ ↑ι
<<<
bqueue_mpmc۰model t (tail vs)
| RET head vs;
True
>>>.
End bqueue_mpmc۰G.
#[global] Opaque bqueue_mpmc۰inv.
#[global] Opaque bqueue_mpmc۰model.