Library zoo_saturn.inf_mpmc_queue_2
From zoo Require Import
prelude.
From zoo.common Require Import
countable
function
list
relations.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.twins
lib.auth_mono
lib.mono_list
lib.saved_pred
lib.oneshot.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
identifier
prophet_identifier
prophet_multi
prophet_nat.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
domain
inf_array
int
optional.
From zoo_saturn Require Export
base
inf_mpmc_queue_2__code.
From zoo_saturn Require Import
inf_mpmc_queue_2__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types front back : nat.
Implicit Types v : val.
Implicit Types o : option val.
Implicit Types vs : list val.
Implicit Types hist : list (option val).
Implicit Types slot : optional val.
Implicit Types slots : nat → optional val.
Implicit Types η : gname.
Implicit Types ηs : list gname.
Implicit Types past prophs : list prophet_identifier.(prophet_typed_type).
Implicit Types pasts prophss : nat → list prophet_identifier.(prophet_typed_type).
Variant lstate :=
| Producer
| ProducerProducer
| ProducerConsumer
| Consumer
| ConsumerProducer η
| ConsumerConsumer.
#[local] Canonical lstate_O {SI : sidx} :=
leibnizO lstate.
Implicit Types lstate : lstate.
Implicit Types lstates : list lstate.
#[local] Definition lstate_winner lstate :=
match lstate with
| Producer ⇒
Producer
| ProducerProducer ⇒
Producer
| ProducerConsumer ⇒
Consumer
| Consumer ⇒
Consumer
| ConsumerProducer η ⇒
Producer
| ConsumerConsumer ⇒
Consumer
end.
#[local] Definition lstate_measure lstate :=
match lstate with
| Producer
| Consumer ⇒
0
| ProducerProducer
| ProducerConsumer
| ConsumerProducer _
| ConsumerConsumer ⇒
1
end.
Variant lstep : lstate → lstate → Prop :=
| lstep_producer_producer :
lstep Producer ProducerProducer
| lstep_producer_consumer :
lstep Consumer ProducerConsumer
| lstep_consumer_producer η :
lstep Producer (ConsumerProducer η)
| lstep_consumer_consumer :
lstep Consumer ConsumerConsumer.
#[local] Lemma lstep_measure lstate1 lstate2 :
lstep lstate1 lstate2 →
lstate_measure lstate1 < lstate_measure lstate2.
#[local] Lemma lstep_tc_measure lstate1 lstate2 :
tc lstep lstate1 lstate2 →
lstate_measure lstate1 < lstate_measure lstate2.
#[local] Lemma lstep_rtc_measure lstate1 lstate2 :
rtc lstep lstate1 lstate2 →
lstate_measure lstate1 ≤ lstate_measure lstate2.
#[local] Instance lsteps_antisymm :
AntiSymm (=) (rtc lstep).
#[local] Lemma lstate_winner_lb lstate :
rtc lstep (lstate_winner lstate) lstate.
#[local] Lemma lstep_winner lstate1 lstate2 :
lstep lstate1 lstate2 →
lstate_winner lstate1 = lstate_winner lstate2.
#[local] Lemma lsteps_winner lstate1 lstate2 :
rtc lstep lstate1 lstate2 →
lstate_winner lstate1 = lstate_winner lstate2.
Class InfMpmcQueue2G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] inf_mpmc_queue_2_G_inf_array_G :: InfArrayG Σ
; #[local] inf_mpmc_queue_2_G_prophet_G :: ProphetMultiG Σ prophet_identifier
; #[local] inf_mpmc_queue_2_G_model_G :: TwinsG Σ (leibnizO (list val))
; #[local] inf_mpmc_queue_2_G_history_G :: MonoListG Σ (option val)
; #[local] inf_mpmc_queue_2_G_lstate_G :: AuthMonoG Σ lstep
; #[local] inf_mpmc_queue_2_G_lstates_G :: MonoListG Σ gname
; #[local] inf_mpmc_queue_2_G_saved_pred_G :: SavedPredG Σ val
; #[local] inf_mpmc_queue_2_G_producer_G :: OneshotG Σ () ()
; #[local] inf_mpmc_queue_2_G_producers_G :: MonoListG Σ gname
; #[local] inf_mpmc_queue_2_G_consumer_G :: OneshotG Σ () ()
; #[local] inf_mpmc_queue_2_G_consumers_G :: MonoListG Σ gname
}.
Definition inf_mpmc_queue_2_Σ :=
#[inf_array_Σ
; prophet_multi_Σ prophet_identifier
; twins_Σ (leibnizO (list val))
; mono_list_Σ (option val)
; mono_list_Σ gname
; auth_mono_Σ lstep
; saved_pred_Σ val
; oneshot_Σ () ()
; mono_list_Σ gname
; oneshot_Σ () ()
; mono_list_Σ gname
].
#[global] Instance subG_inf_mpmc_queue_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG inf_mpmc_queue_2_Σ Σ →
InfMpmcQueue2G Σ.
Module base.
Section inf_mpmc_queue_2_G.
Context `{inf_mpmc_queue_2_G : InfMpmcQueue2G Σ}.
Implicit Types t : location.
Implicit Types Ψ : val → iProp Σ.
Record inf_mpmc_queue_2_name :=
{ inf_mpmc_queue_2_name_data : val
; inf_mpmc_queue_2_name_inv : namespace
; inf_mpmc_queue_2_name_prophet : prophet_id
; inf_mpmc_queue_2_name_prophet_name : prophet_multi_name
; inf_mpmc_queue_2_name_model : gname
; inf_mpmc_queue_2_name_history : gname
; inf_mpmc_queue_2_name_lstates : gname
; inf_mpmc_queue_2_name_producers : gname
; inf_mpmc_queue_2_name_consumers : gname
}.
Implicit Type γ : inf_mpmc_queue_2_name.
#[global] Instance inf_mpmc_queue_2_name_eq_dec : EqDecision inf_mpmc_queue_2_name :=
ltac:(solve_decision).
#[global] Instance inf_mpmc_queue_2_name_countable :
Countable inf_mpmc_queue_2_name.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ vs :=
model₁' γ.(inf_mpmc_queue_2_name_model) vs.
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ vs :=
model₂' γ.(inf_mpmc_queue_2_name_model) vs.
#[local] Definition history_auth' γ_history hist :=
mono_list_auth γ_history (DfracOwn 1) hist.
#[local] Definition history_auth γ :=
history_auth' γ.(inf_mpmc_queue_2_name_history).
#[local] Definition history_at γ i o :=
mono_list_at γ.(inf_mpmc_queue_2_name_history) i o.
#[local] Definition lstates_auth' γ_lstates lstates : iProp Σ :=
∃ ηs,
mono_list_auth γ_lstates (DfracOwn 1) ηs ∗
[∗ list] η; lstate ∈ ηs; lstates,
auth_mono_auth _ η DfracDiscarded lstate.
#[local] Definition lstates_auth γ :=
lstates_auth' γ.(inf_mpmc_queue_2_name_lstates).
#[local] Instance : CustomIpat "lstates_auth" :=
" ( %ηs & Hauth & Hηs ) ".
#[local] Definition lstates_at γ i lstate : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_2_name_lstates) i η ∗
auth_mono_auth _ η DfracDiscarded lstate.
#[local] Instance : CustomIpat "lstates_at" :=
" ( %η{} & #Hat{_{}} & #Hη_auth{_{}} ) ".
#[local] Definition lstates_lb γ i lstate : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_2_name_lstates) i η ∗
auth_mono_lb _ η lstate.
#[local] Instance : CustomIpat "lstates_lb" :=
" ( %η{} & #Hat{_{}} & #Hη_lb{_{}} ) ".
#[local] Definition producers_auth' γ_producers i : iProp Σ :=
∃ ηs,
mono_list_auth γ_producers (DfracOwn 1) ηs ∗
⌜length ηs = i⌝.
#[local] Definition producers_auth γ :=
producers_auth' γ.(inf_mpmc_queue_2_name_producers).
#[local] Instance : CustomIpat "producers_auth" :=
" ( %ηs & Hauth & %Hηs ) ".
#[local] Definition producers_at γ i own : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_2_name_producers) i η ∗
match own with
| Own ⇒
oneshot_pending η (DfracOwn 1) ()
| Discard ⇒
oneshot_shot η ()
end.
#[local] Instance : CustomIpat "producers_at" :=
" ( %η{} & Hat{_{}} & Hη{} ) ".
#[local] Definition consumers_auth' γ_consumers i : iProp Σ :=
∃ ηs,
mono_list_auth γ_consumers (DfracOwn 1) ηs ∗
⌜length ηs = i⌝.
#[local] Definition consumers_auth γ :=
consumers_auth' γ.(inf_mpmc_queue_2_name_consumers).
#[local] Instance : CustomIpat "consumers_auth" :=
" ( %ηs{} & Hauth{} & %Hηs{} ) ".
#[local] Definition consumers_at γ i own : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_2_name_consumers) i η ∗
match own with
| Own ⇒
oneshot_pending η (DfracOwn 1) ()
| Discard ⇒
oneshot_shot η ()
end.
#[local] Instance : CustomIpat "consumers_at" :=
" ( %η{} & Hat{_{}} & Hη{} ) ".
#[local] Definition consumers_lb γ i : iProp Σ :=
∃ ηs,
mono_list_lb γ.(inf_mpmc_queue_2_name_consumers) ηs ∗
⌜length ηs = i⌝.
#[local] Instance : CustomIpat "consumers_lb" :=
" ( %ηs{} & Hlb{} & %Hηs{} ) ".
#[local] Definition winner γ i : iProp Σ :=
∃ id prophs,
prophet_multi_full prophet_identifier γ.(inf_mpmc_queue_2_name_prophet_name) i prophs ∗
⌜head prophs = Some id⌝ ∗
identifier_model' id.
#[local] Instance : CustomIpat "winner" :=
" ( %id{} & %prophs{} & Hprophet_full{_{}} & %Hprophs{} & Hid{} ) ".
#[local] Definition consumer_au γ Ψ : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(inf_mpmc_queue_2_name_inv), ∅ <{
∀∀ v vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
, COMM
Ψ v
}>.
#[local] Definition inv_lstate_left γ back i lstate : iProp Σ :=
match lstate with
| ProducerProducer ⇒
∃ v,
history_at γ i (Some v) ∗
winner γ i
| ProducerConsumer ⇒
history_at γ i None
| ConsumerProducer η ⇒
∃ Ψ v,
consumers_lb γ (S i) ∗
saved_pred η Ψ ∗
history_at γ i (Some v) ∗
( Ψ v
∨ consumers_at γ i Discard
)
| ConsumerConsumer ⇒
consumers_lb γ (S i)
| _ ⇒
False
end.
#[local] Instance : CustomIpat "inv_lstate_left_producer" :=
" ( %v & #Hhistory_at & Hwinner ) ".
#[local] Instance : CustomIpat "inv_lstate_left_consumer" :=
" ( %Ψ & %v_ & #Hconsumers_lb & #Hη_ & #Hhistory_at_ & HΨ ) ".
#[local] Definition inv_lstate_right γ i lstate : iProp Σ :=
match lstate with
| ConsumerProducer η ⇒
∃ Ψ,
saved_pred η Ψ ∗
consumer_au γ Ψ
| ConsumerConsumer ⇒
winner γ i
| _ ⇒
False
end.
#[local] Instance : CustomIpat "inv_lstate_right" :=
" ( %Ψ & #Hη & Hconsumer_au ) ".
#[local] Definition inv_slot γ i slot past : iProp Σ :=
match slot with
| Nothing ⇒
⌜past = []⌝
| Something v ⇒
history_at γ i (Some v) ∗
producers_at γ i Discard ∗
lstates_lb γ i Producer
| Anything ⇒
consumers_at γ i Discard ∗
( lstates_lb γ i Consumer
∨ producers_at γ i Discard
)
end.
#[local] Instance : CustomIpat "inv_slot_nothing" :=
" %Hpast ".
#[local] Instance : CustomIpat "inv_slot_something" :=
" ( #Hhistory_at{_{suff}} & #Hproducers_at{_{suff}} & #Hlstates_lb_producer ) ".
#[local] Instance : CustomIpat "inv_slot_anything" :=
" ( #Hconsumers_at{_{suff}} & { _{suff} ; [ #Hlstates_lb_consumer | #Hproducers_at_ ] } ) ".
#[local] Definition inv_inner t γ : iProp Σ :=
∃ front back hist slots vs lstates pasts prophss,
t.[front] ↦ #front ∗
t.[back] ↦ #back ∗
inf_array_model γ.(inf_mpmc_queue_2_name_data) slots ∗
model₂ γ vs ∗
⌜vs = oflatten (drop front hist)⌝ ∗
history_auth γ hist ∗
⌜length hist = back⌝ ∗
lstates_auth γ lstates ∗
⌜length lstates = front `max` back⌝ ∗
prophet_multi_model prophet_identifier γ.(inf_mpmc_queue_2_name_prophet) γ.(inf_mpmc_queue_2_name_prophet_name) pasts prophss ∗
producers_auth γ back ∗
consumers_auth γ front ∗
( [∗ list] i ↦ lstate ∈ take back lstates,
inv_lstate_left γ back i lstate
) ∗
( [∗ list] k ↦ lstate ∈ drop back lstates,
inv_lstate_right γ (back + k) lstate
) ∗
( ∀ i,
inv_slot γ i (slots i) (pasts i)
).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %front{} & %back{} & %hist{} & %slots{} & %vs{} & %lstates{} & %pasts{} & %prophss{} & Ht_front & Ht_back & >Hdata_model & Hmodel₂ & >%Hvs{} & Hhistory_auth & >%Hhist{} & Hlstates_auth & >%Hlstates{} & >Hprophet_model & Hproducers_auth & Hconsumers_auth & Hlstates_left & Hlstates_right & Hslots ) ".
Definition inf_mpmc_queue_2_inv t γ ι : iProp Σ :=
⌜ι = γ.(inf_mpmc_queue_2_name_inv)⌝ ∗
t.[data] ↦□ γ.(inf_mpmc_queue_2_name_data) ∗
t.[proph] ↦□ #γ.(inf_mpmc_queue_2_name_prophet) ∗
inf_array_inv γ.(inf_mpmc_queue_2_name_data) ∗
inv γ.(inf_mpmc_queue_2_name_inv) (inv_inner t γ).
#[local] Instance : CustomIpat "inv" :=
" ( -> & #Ht_data & #Ht_proph & #Hdata_inv & #Hinv ) ".
Definition inf_mpmc_queue_2_model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
#[global] Instance inf_mpmc_queue_2_model_timeless γ vs :
Timeless (inf_mpmc_queue_2_model γ vs).
#[local] Instance lstates_at_persistent γ i lstate :
Persistent (lstates_at γ i lstate).
#[local] Instance lstates_lb_persistent γ i lstate :
Persistent (lstates_lb γ i lstate).
#[local] Instance producers_at_persistent γ i :
Persistent (producers_at γ i Discard).
#[local] Instance consumers_at_persistent γ i :
Persistent (consumers_at γ i Discard).
#[local] Instance consumers_lb_persistent γ i :
Persistent (consumers_lb γ i).
#[local] Instance inv_slot_persistent γ i slot past :
Persistent (inv_slot γ i slot past).
#[global] Instance inf_mpmc_queue_2_inv_persistent t γ ι :
Persistent (inf_mpmc_queue_2_inv 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 history_alloc :
⊢ |==>
∃ γ_history,
history_auth' γ_history [].
#[local] Lemma history_at_lookup γ hist i o :
history_auth γ hist -∗
history_at γ i o -∗
⌜hist !! i = Some o⌝.
#[local] Lemma history_at_agree γ i o1 o2 :
history_at γ i o1 -∗
history_at γ i o2 -∗
⌜o1 = o2⌝.
#[local] Lemma history_at_get {γ hist} i o :
hist !! i = Some o →
history_auth γ hist ⊢
history_at γ i o.
#[local] Lemma history_update {γ hist} o :
history_auth γ hist ⊢ |==>
history_auth γ (hist ++ [o]) ∗
history_at γ (length hist) o.
#[local] Lemma lstates_alloc :
⊢ |==>
∃ γ_lstates,
lstates_auth' γ_lstates [].
#[local] Lemma lstates_at_lookup γ lstates i lstate :
lstates_auth γ lstates -∗
lstates_at γ i lstate -∗
⌜lstates !! i = Some lstate⌝.
#[local] Lemma lstates_lb_get {γ lstates} i lstate :
lstates !! i = Some lstate →
lstates_auth γ lstates -∗
lstates_lb γ i (lstate_winner lstate).
#[local] Lemma lstates_lb_agree γ i lstate1 lstate2 :
lstates_lb γ i lstate1 -∗
lstates_lb γ i lstate2 -∗
⌜lstate_winner lstate1 = lstate_winner lstate2⌝.
#[local] Lemma lstates_update {γ lstates} lstate :
lstates_auth γ lstates ⊢ |==>
lstates_auth γ (lstates ++ [lstate]) ∗
lstates_lb γ (length lstates) (lstate_winner lstate) ∗
lstates_at γ (length lstates) lstate.
Opaque lstates_auth'.
Opaque lstates_at.
Opaque lstates_lb.
#[local] Lemma producers_alloc :
⊢ |==>
∃ γ_producers,
producers_auth' γ_producers 0.
#[local] Lemma producers_at_exclusive γ i own :
producers_at γ i Own -∗
producers_at γ i own -∗
False.
#[local] Lemma producers_at_discard γ i :
producers_at γ i Own ⊢ |==>
producers_at γ i Discard.
#[local] Lemma producers_update γ i :
producers_auth γ i ⊢ |==>
producers_auth γ (S i) ∗
producers_at γ i Own.
Opaque producers_auth'.
Opaque producers_at.
#[local] Lemma consumers_alloc :
⊢ |==>
∃ γ_consumers,
consumers_auth' γ_consumers 0.
#[local] Lemma consumers_at_exclusive γ i own :
consumers_at γ i Own -∗
consumers_at γ i own -∗
False.
#[local] Lemma consumers_at_discard γ i :
consumers_at γ i Own ⊢ |==>
consumers_at γ i Discard.
#[local] Lemma consumers_lb_valid γ i j :
consumers_auth γ i -∗
consumers_lb γ j -∗
⌜j ≤ i⌝.
#[local] Lemma consumers_lb_le {γ i1} i2 :
i2 ≤ i1 →
consumers_lb γ i1 ⊢
consumers_lb γ i2.
#[local] Lemma consumers_lb_get γ i :
consumers_auth γ i ⊢
consumers_lb γ i.
#[local] Lemma consumers_lb_get' {γ i} i' :
i' ≤ i →
consumers_auth γ i ⊢
consumers_lb γ i'.
#[local] Lemma consumers_update γ i :
consumers_auth γ i ⊢ |==>
consumers_auth γ (S i) ∗
consumers_at γ i Own.
Opaque consumers_auth'.
Opaque consumers_at.
Opaque consumers_lb.
#[local] Lemma winner_exclusive γ i :
winner γ i -∗
winner γ i -∗
False.
#[local] Lemma inv_slot_not_nothing_past {γ i slot past1} past2 :
slot ≠ Nothing →
inv_slot γ i slot past1 ⊣⊢
inv_slot γ i slot past2.
Lemma inf_mpmc_queue_2_model_exclusive γ vs1 vs2 :
inf_mpmc_queue_2_model γ vs1 -∗
inf_mpmc_queue_2_model γ vs2 -∗
False.
Lemma inf_mpmc_queue_2٠create𑁒spec ι :
{{{
True
}}}
inf_mpmc_queue_2٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
inf_mpmc_queue_2_inv t γ ι ∗
inf_mpmc_queue_2_model γ []
}}}.
Lemma inf_mpmc_queue_2٠size𑁒spec t γ ι :
<<<
inf_mpmc_queue_2_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_2_model γ vs
>>>
inf_mpmc_queue_2٠size #t @ ↑ι
<<<
inf_mpmc_queue_2_model γ vs
| sz,
RET #sz;
⌜length vs ≤ sz⌝
>>>.
Lemma inf_mpmc_queue_2٠is_empty𑁒spec t γ ι :
<<<
inf_mpmc_queue_2_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_2_model γ vs
>>>
inf_mpmc_queue_2٠is_empty #t @ ↑ι
<<<
inf_mpmc_queue_2_model γ vs
| b,
RET #b;
⌜if b then vs = [] else True⌝
>>>.
Lemma inf_mpmc_queue_2٠push𑁒spec t γ ι v :
<<<
inf_mpmc_queue_2_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_2_model γ vs
>>>
inf_mpmc_queue_2٠push #t v @ ↑ι
<<<
inf_mpmc_queue_2_model γ (vs ++ [v])
| RET ();
True
>>>.
Lemma inf_mpmc_queue_2٠pop𑁒spec t γ ι :
<<<
inf_mpmc_queue_2_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_2_model γ vs
>>>
inf_mpmc_queue_2٠pop #t @ ↑ι
<<<
∃∃ v vs',
⌜vs = v :: vs'⌝ ∗
inf_mpmc_queue_2_model γ vs'
| RET v;
True
>>>.
End inf_mpmc_queue_2_G.
#[global] Opaque inf_mpmc_queue_2_inv.
#[global] Opaque inf_mpmc_queue_2_model.
End base.
From zoo_saturn Require
inf_mpmc_queue_2__opaque.
Section inf_mpmc_queue_2_G.
Context `{inf_mpmc_queue_2_G : InfMpmcQueue2G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition inf_mpmc_queue_2_inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.inf_mpmc_queue_2_inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition inf_mpmc_queue_2_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.inf_mpmc_queue_2_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hmodel{_{}} ) ".
#[global] Instance inf_mpmc_queue_2_model_timeless t vs :
Timeless (inf_mpmc_queue_2_model t vs).
#[global] Instance inf_mpmc_queue_2_inv_persistent t ι :
Persistent (inf_mpmc_queue_2_inv t ι).
Lemma inf_mpmc_queue_2_model_exclusive t vs1 vs2 :
inf_mpmc_queue_2_model t vs1 -∗
inf_mpmc_queue_2_model t vs2 -∗
False.
Lemma inf_mpmc_queue_2٠create𑁒spec ι :
{{{
True
}}}
inf_mpmc_queue_2٠create ()
{{{
t
, RET t;
inf_mpmc_queue_2_inv t ι ∗
inf_mpmc_queue_2_model t []
}}}.
Lemma inf_mpmc_queue_2٠size𑁒spec t ι :
<<<
inf_mpmc_queue_2_inv t ι
| ∀∀ vs,
inf_mpmc_queue_2_model t vs
>>>
inf_mpmc_queue_2٠size t @ ↑ι
<<<
inf_mpmc_queue_2_model t vs
| sz,
RET #sz;
⌜length vs ≤ sz⌝
>>>.
Lemma inf_mpmc_queue_2٠is_empty𑁒spec t ι :
<<<
inf_mpmc_queue_2_inv t ι
| ∀∀ vs,
inf_mpmc_queue_2_model t vs
>>>
inf_mpmc_queue_2٠is_empty t @ ↑ι
<<<
inf_mpmc_queue_2_model t vs
| b,
RET #b;
⌜if b then vs = [] else True⌝
>>>.
Lemma inf_mpmc_queue_2٠push𑁒spec t ι v :
<<<
inf_mpmc_queue_2_inv t ι
| ∀∀ vs,
inf_mpmc_queue_2_model t vs
>>>
inf_mpmc_queue_2٠push t v @ ↑ι
<<<
inf_mpmc_queue_2_model t (vs ++ [v])
| RET ();
True
>>>.
Lemma inf_mpmc_queue_2٠pop𑁒spec t ι :
<<<
inf_mpmc_queue_2_inv t ι
| ∀∀ vs,
inf_mpmc_queue_2_model t vs
>>>
inf_mpmc_queue_2٠pop t @ ↑ι
<<<
∃∃ v vs',
⌜vs = v :: vs'⌝ ∗
inf_mpmc_queue_2_model t vs'
| RET v;
True
>>>.
End inf_mpmc_queue_2_G.
#[global] Opaque inf_mpmc_queue_2_inv.
#[global] Opaque inf_mpmc_queue_2_model.
prelude.
From zoo.common Require Import
countable
function
list
relations.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.twins
lib.auth_mono
lib.mono_list
lib.saved_pred
lib.oneshot.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
identifier
prophet_identifier
prophet_multi
prophet_nat.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
domain
inf_array
int
optional.
From zoo_saturn Require Export
base
inf_mpmc_queue_2__code.
From zoo_saturn Require Import
inf_mpmc_queue_2__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types front back : nat.
Implicit Types v : val.
Implicit Types o : option val.
Implicit Types vs : list val.
Implicit Types hist : list (option val).
Implicit Types slot : optional val.
Implicit Types slots : nat → optional val.
Implicit Types η : gname.
Implicit Types ηs : list gname.
Implicit Types past prophs : list prophet_identifier.(prophet_typed_type).
Implicit Types pasts prophss : nat → list prophet_identifier.(prophet_typed_type).
Variant lstate :=
| Producer
| ProducerProducer
| ProducerConsumer
| Consumer
| ConsumerProducer η
| ConsumerConsumer.
#[local] Canonical lstate_O {SI : sidx} :=
leibnizO lstate.
Implicit Types lstate : lstate.
Implicit Types lstates : list lstate.
#[local] Definition lstate_winner lstate :=
match lstate with
| Producer ⇒
Producer
| ProducerProducer ⇒
Producer
| ProducerConsumer ⇒
Consumer
| Consumer ⇒
Consumer
| ConsumerProducer η ⇒
Producer
| ConsumerConsumer ⇒
Consumer
end.
#[local] Definition lstate_measure lstate :=
match lstate with
| Producer
| Consumer ⇒
0
| ProducerProducer
| ProducerConsumer
| ConsumerProducer _
| ConsumerConsumer ⇒
1
end.
Variant lstep : lstate → lstate → Prop :=
| lstep_producer_producer :
lstep Producer ProducerProducer
| lstep_producer_consumer :
lstep Consumer ProducerConsumer
| lstep_consumer_producer η :
lstep Producer (ConsumerProducer η)
| lstep_consumer_consumer :
lstep Consumer ConsumerConsumer.
#[local] Lemma lstep_measure lstate1 lstate2 :
lstep lstate1 lstate2 →
lstate_measure lstate1 < lstate_measure lstate2.
#[local] Lemma lstep_tc_measure lstate1 lstate2 :
tc lstep lstate1 lstate2 →
lstate_measure lstate1 < lstate_measure lstate2.
#[local] Lemma lstep_rtc_measure lstate1 lstate2 :
rtc lstep lstate1 lstate2 →
lstate_measure lstate1 ≤ lstate_measure lstate2.
#[local] Instance lsteps_antisymm :
AntiSymm (=) (rtc lstep).
#[local] Lemma lstate_winner_lb lstate :
rtc lstep (lstate_winner lstate) lstate.
#[local] Lemma lstep_winner lstate1 lstate2 :
lstep lstate1 lstate2 →
lstate_winner lstate1 = lstate_winner lstate2.
#[local] Lemma lsteps_winner lstate1 lstate2 :
rtc lstep lstate1 lstate2 →
lstate_winner lstate1 = lstate_winner lstate2.
Class InfMpmcQueue2G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] inf_mpmc_queue_2_G_inf_array_G :: InfArrayG Σ
; #[local] inf_mpmc_queue_2_G_prophet_G :: ProphetMultiG Σ prophet_identifier
; #[local] inf_mpmc_queue_2_G_model_G :: TwinsG Σ (leibnizO (list val))
; #[local] inf_mpmc_queue_2_G_history_G :: MonoListG Σ (option val)
; #[local] inf_mpmc_queue_2_G_lstate_G :: AuthMonoG Σ lstep
; #[local] inf_mpmc_queue_2_G_lstates_G :: MonoListG Σ gname
; #[local] inf_mpmc_queue_2_G_saved_pred_G :: SavedPredG Σ val
; #[local] inf_mpmc_queue_2_G_producer_G :: OneshotG Σ () ()
; #[local] inf_mpmc_queue_2_G_producers_G :: MonoListG Σ gname
; #[local] inf_mpmc_queue_2_G_consumer_G :: OneshotG Σ () ()
; #[local] inf_mpmc_queue_2_G_consumers_G :: MonoListG Σ gname
}.
Definition inf_mpmc_queue_2_Σ :=
#[inf_array_Σ
; prophet_multi_Σ prophet_identifier
; twins_Σ (leibnizO (list val))
; mono_list_Σ (option val)
; mono_list_Σ gname
; auth_mono_Σ lstep
; saved_pred_Σ val
; oneshot_Σ () ()
; mono_list_Σ gname
; oneshot_Σ () ()
; mono_list_Σ gname
].
#[global] Instance subG_inf_mpmc_queue_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG inf_mpmc_queue_2_Σ Σ →
InfMpmcQueue2G Σ.
Module base.
Section inf_mpmc_queue_2_G.
Context `{inf_mpmc_queue_2_G : InfMpmcQueue2G Σ}.
Implicit Types t : location.
Implicit Types Ψ : val → iProp Σ.
Record inf_mpmc_queue_2_name :=
{ inf_mpmc_queue_2_name_data : val
; inf_mpmc_queue_2_name_inv : namespace
; inf_mpmc_queue_2_name_prophet : prophet_id
; inf_mpmc_queue_2_name_prophet_name : prophet_multi_name
; inf_mpmc_queue_2_name_model : gname
; inf_mpmc_queue_2_name_history : gname
; inf_mpmc_queue_2_name_lstates : gname
; inf_mpmc_queue_2_name_producers : gname
; inf_mpmc_queue_2_name_consumers : gname
}.
Implicit Type γ : inf_mpmc_queue_2_name.
#[global] Instance inf_mpmc_queue_2_name_eq_dec : EqDecision inf_mpmc_queue_2_name :=
ltac:(solve_decision).
#[global] Instance inf_mpmc_queue_2_name_countable :
Countable inf_mpmc_queue_2_name.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ vs :=
model₁' γ.(inf_mpmc_queue_2_name_model) vs.
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ vs :=
model₂' γ.(inf_mpmc_queue_2_name_model) vs.
#[local] Definition history_auth' γ_history hist :=
mono_list_auth γ_history (DfracOwn 1) hist.
#[local] Definition history_auth γ :=
history_auth' γ.(inf_mpmc_queue_2_name_history).
#[local] Definition history_at γ i o :=
mono_list_at γ.(inf_mpmc_queue_2_name_history) i o.
#[local] Definition lstates_auth' γ_lstates lstates : iProp Σ :=
∃ ηs,
mono_list_auth γ_lstates (DfracOwn 1) ηs ∗
[∗ list] η; lstate ∈ ηs; lstates,
auth_mono_auth _ η DfracDiscarded lstate.
#[local] Definition lstates_auth γ :=
lstates_auth' γ.(inf_mpmc_queue_2_name_lstates).
#[local] Instance : CustomIpat "lstates_auth" :=
" ( %ηs & Hauth & Hηs ) ".
#[local] Definition lstates_at γ i lstate : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_2_name_lstates) i η ∗
auth_mono_auth _ η DfracDiscarded lstate.
#[local] Instance : CustomIpat "lstates_at" :=
" ( %η{} & #Hat{_{}} & #Hη_auth{_{}} ) ".
#[local] Definition lstates_lb γ i lstate : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_2_name_lstates) i η ∗
auth_mono_lb _ η lstate.
#[local] Instance : CustomIpat "lstates_lb" :=
" ( %η{} & #Hat{_{}} & #Hη_lb{_{}} ) ".
#[local] Definition producers_auth' γ_producers i : iProp Σ :=
∃ ηs,
mono_list_auth γ_producers (DfracOwn 1) ηs ∗
⌜length ηs = i⌝.
#[local] Definition producers_auth γ :=
producers_auth' γ.(inf_mpmc_queue_2_name_producers).
#[local] Instance : CustomIpat "producers_auth" :=
" ( %ηs & Hauth & %Hηs ) ".
#[local] Definition producers_at γ i own : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_2_name_producers) i η ∗
match own with
| Own ⇒
oneshot_pending η (DfracOwn 1) ()
| Discard ⇒
oneshot_shot η ()
end.
#[local] Instance : CustomIpat "producers_at" :=
" ( %η{} & Hat{_{}} & Hη{} ) ".
#[local] Definition consumers_auth' γ_consumers i : iProp Σ :=
∃ ηs,
mono_list_auth γ_consumers (DfracOwn 1) ηs ∗
⌜length ηs = i⌝.
#[local] Definition consumers_auth γ :=
consumers_auth' γ.(inf_mpmc_queue_2_name_consumers).
#[local] Instance : CustomIpat "consumers_auth" :=
" ( %ηs{} & Hauth{} & %Hηs{} ) ".
#[local] Definition consumers_at γ i own : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_2_name_consumers) i η ∗
match own with
| Own ⇒
oneshot_pending η (DfracOwn 1) ()
| Discard ⇒
oneshot_shot η ()
end.
#[local] Instance : CustomIpat "consumers_at" :=
" ( %η{} & Hat{_{}} & Hη{} ) ".
#[local] Definition consumers_lb γ i : iProp Σ :=
∃ ηs,
mono_list_lb γ.(inf_mpmc_queue_2_name_consumers) ηs ∗
⌜length ηs = i⌝.
#[local] Instance : CustomIpat "consumers_lb" :=
" ( %ηs{} & Hlb{} & %Hηs{} ) ".
#[local] Definition winner γ i : iProp Σ :=
∃ id prophs,
prophet_multi_full prophet_identifier γ.(inf_mpmc_queue_2_name_prophet_name) i prophs ∗
⌜head prophs = Some id⌝ ∗
identifier_model' id.
#[local] Instance : CustomIpat "winner" :=
" ( %id{} & %prophs{} & Hprophet_full{_{}} & %Hprophs{} & Hid{} ) ".
#[local] Definition consumer_au γ Ψ : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(inf_mpmc_queue_2_name_inv), ∅ <{
∀∀ v vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
, COMM
Ψ v
}>.
#[local] Definition inv_lstate_left γ back i lstate : iProp Σ :=
match lstate with
| ProducerProducer ⇒
∃ v,
history_at γ i (Some v) ∗
winner γ i
| ProducerConsumer ⇒
history_at γ i None
| ConsumerProducer η ⇒
∃ Ψ v,
consumers_lb γ (S i) ∗
saved_pred η Ψ ∗
history_at γ i (Some v) ∗
( Ψ v
∨ consumers_at γ i Discard
)
| ConsumerConsumer ⇒
consumers_lb γ (S i)
| _ ⇒
False
end.
#[local] Instance : CustomIpat "inv_lstate_left_producer" :=
" ( %v & #Hhistory_at & Hwinner ) ".
#[local] Instance : CustomIpat "inv_lstate_left_consumer" :=
" ( %Ψ & %v_ & #Hconsumers_lb & #Hη_ & #Hhistory_at_ & HΨ ) ".
#[local] Definition inv_lstate_right γ i lstate : iProp Σ :=
match lstate with
| ConsumerProducer η ⇒
∃ Ψ,
saved_pred η Ψ ∗
consumer_au γ Ψ
| ConsumerConsumer ⇒
winner γ i
| _ ⇒
False
end.
#[local] Instance : CustomIpat "inv_lstate_right" :=
" ( %Ψ & #Hη & Hconsumer_au ) ".
#[local] Definition inv_slot γ i slot past : iProp Σ :=
match slot with
| Nothing ⇒
⌜past = []⌝
| Something v ⇒
history_at γ i (Some v) ∗
producers_at γ i Discard ∗
lstates_lb γ i Producer
| Anything ⇒
consumers_at γ i Discard ∗
( lstates_lb γ i Consumer
∨ producers_at γ i Discard
)
end.
#[local] Instance : CustomIpat "inv_slot_nothing" :=
" %Hpast ".
#[local] Instance : CustomIpat "inv_slot_something" :=
" ( #Hhistory_at{_{suff}} & #Hproducers_at{_{suff}} & #Hlstates_lb_producer ) ".
#[local] Instance : CustomIpat "inv_slot_anything" :=
" ( #Hconsumers_at{_{suff}} & { _{suff} ; [ #Hlstates_lb_consumer | #Hproducers_at_ ] } ) ".
#[local] Definition inv_inner t γ : iProp Σ :=
∃ front back hist slots vs lstates pasts prophss,
t.[front] ↦ #front ∗
t.[back] ↦ #back ∗
inf_array_model γ.(inf_mpmc_queue_2_name_data) slots ∗
model₂ γ vs ∗
⌜vs = oflatten (drop front hist)⌝ ∗
history_auth γ hist ∗
⌜length hist = back⌝ ∗
lstates_auth γ lstates ∗
⌜length lstates = front `max` back⌝ ∗
prophet_multi_model prophet_identifier γ.(inf_mpmc_queue_2_name_prophet) γ.(inf_mpmc_queue_2_name_prophet_name) pasts prophss ∗
producers_auth γ back ∗
consumers_auth γ front ∗
( [∗ list] i ↦ lstate ∈ take back lstates,
inv_lstate_left γ back i lstate
) ∗
( [∗ list] k ↦ lstate ∈ drop back lstates,
inv_lstate_right γ (back + k) lstate
) ∗
( ∀ i,
inv_slot γ i (slots i) (pasts i)
).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %front{} & %back{} & %hist{} & %slots{} & %vs{} & %lstates{} & %pasts{} & %prophss{} & Ht_front & Ht_back & >Hdata_model & Hmodel₂ & >%Hvs{} & Hhistory_auth & >%Hhist{} & Hlstates_auth & >%Hlstates{} & >Hprophet_model & Hproducers_auth & Hconsumers_auth & Hlstates_left & Hlstates_right & Hslots ) ".
Definition inf_mpmc_queue_2_inv t γ ι : iProp Σ :=
⌜ι = γ.(inf_mpmc_queue_2_name_inv)⌝ ∗
t.[data] ↦□ γ.(inf_mpmc_queue_2_name_data) ∗
t.[proph] ↦□ #γ.(inf_mpmc_queue_2_name_prophet) ∗
inf_array_inv γ.(inf_mpmc_queue_2_name_data) ∗
inv γ.(inf_mpmc_queue_2_name_inv) (inv_inner t γ).
#[local] Instance : CustomIpat "inv" :=
" ( -> & #Ht_data & #Ht_proph & #Hdata_inv & #Hinv ) ".
Definition inf_mpmc_queue_2_model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
#[global] Instance inf_mpmc_queue_2_model_timeless γ vs :
Timeless (inf_mpmc_queue_2_model γ vs).
#[local] Instance lstates_at_persistent γ i lstate :
Persistent (lstates_at γ i lstate).
#[local] Instance lstates_lb_persistent γ i lstate :
Persistent (lstates_lb γ i lstate).
#[local] Instance producers_at_persistent γ i :
Persistent (producers_at γ i Discard).
#[local] Instance consumers_at_persistent γ i :
Persistent (consumers_at γ i Discard).
#[local] Instance consumers_lb_persistent γ i :
Persistent (consumers_lb γ i).
#[local] Instance inv_slot_persistent γ i slot past :
Persistent (inv_slot γ i slot past).
#[global] Instance inf_mpmc_queue_2_inv_persistent t γ ι :
Persistent (inf_mpmc_queue_2_inv 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 history_alloc :
⊢ |==>
∃ γ_history,
history_auth' γ_history [].
#[local] Lemma history_at_lookup γ hist i o :
history_auth γ hist -∗
history_at γ i o -∗
⌜hist !! i = Some o⌝.
#[local] Lemma history_at_agree γ i o1 o2 :
history_at γ i o1 -∗
history_at γ i o2 -∗
⌜o1 = o2⌝.
#[local] Lemma history_at_get {γ hist} i o :
hist !! i = Some o →
history_auth γ hist ⊢
history_at γ i o.
#[local] Lemma history_update {γ hist} o :
history_auth γ hist ⊢ |==>
history_auth γ (hist ++ [o]) ∗
history_at γ (length hist) o.
#[local] Lemma lstates_alloc :
⊢ |==>
∃ γ_lstates,
lstates_auth' γ_lstates [].
#[local] Lemma lstates_at_lookup γ lstates i lstate :
lstates_auth γ lstates -∗
lstates_at γ i lstate -∗
⌜lstates !! i = Some lstate⌝.
#[local] Lemma lstates_lb_get {γ lstates} i lstate :
lstates !! i = Some lstate →
lstates_auth γ lstates -∗
lstates_lb γ i (lstate_winner lstate).
#[local] Lemma lstates_lb_agree γ i lstate1 lstate2 :
lstates_lb γ i lstate1 -∗
lstates_lb γ i lstate2 -∗
⌜lstate_winner lstate1 = lstate_winner lstate2⌝.
#[local] Lemma lstates_update {γ lstates} lstate :
lstates_auth γ lstates ⊢ |==>
lstates_auth γ (lstates ++ [lstate]) ∗
lstates_lb γ (length lstates) (lstate_winner lstate) ∗
lstates_at γ (length lstates) lstate.
Opaque lstates_auth'.
Opaque lstates_at.
Opaque lstates_lb.
#[local] Lemma producers_alloc :
⊢ |==>
∃ γ_producers,
producers_auth' γ_producers 0.
#[local] Lemma producers_at_exclusive γ i own :
producers_at γ i Own -∗
producers_at γ i own -∗
False.
#[local] Lemma producers_at_discard γ i :
producers_at γ i Own ⊢ |==>
producers_at γ i Discard.
#[local] Lemma producers_update γ i :
producers_auth γ i ⊢ |==>
producers_auth γ (S i) ∗
producers_at γ i Own.
Opaque producers_auth'.
Opaque producers_at.
#[local] Lemma consumers_alloc :
⊢ |==>
∃ γ_consumers,
consumers_auth' γ_consumers 0.
#[local] Lemma consumers_at_exclusive γ i own :
consumers_at γ i Own -∗
consumers_at γ i own -∗
False.
#[local] Lemma consumers_at_discard γ i :
consumers_at γ i Own ⊢ |==>
consumers_at γ i Discard.
#[local] Lemma consumers_lb_valid γ i j :
consumers_auth γ i -∗
consumers_lb γ j -∗
⌜j ≤ i⌝.
#[local] Lemma consumers_lb_le {γ i1} i2 :
i2 ≤ i1 →
consumers_lb γ i1 ⊢
consumers_lb γ i2.
#[local] Lemma consumers_lb_get γ i :
consumers_auth γ i ⊢
consumers_lb γ i.
#[local] Lemma consumers_lb_get' {γ i} i' :
i' ≤ i →
consumers_auth γ i ⊢
consumers_lb γ i'.
#[local] Lemma consumers_update γ i :
consumers_auth γ i ⊢ |==>
consumers_auth γ (S i) ∗
consumers_at γ i Own.
Opaque consumers_auth'.
Opaque consumers_at.
Opaque consumers_lb.
#[local] Lemma winner_exclusive γ i :
winner γ i -∗
winner γ i -∗
False.
#[local] Lemma inv_slot_not_nothing_past {γ i slot past1} past2 :
slot ≠ Nothing →
inv_slot γ i slot past1 ⊣⊢
inv_slot γ i slot past2.
Lemma inf_mpmc_queue_2_model_exclusive γ vs1 vs2 :
inf_mpmc_queue_2_model γ vs1 -∗
inf_mpmc_queue_2_model γ vs2 -∗
False.
Lemma inf_mpmc_queue_2٠create𑁒spec ι :
{{{
True
}}}
inf_mpmc_queue_2٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
inf_mpmc_queue_2_inv t γ ι ∗
inf_mpmc_queue_2_model γ []
}}}.
Lemma inf_mpmc_queue_2٠size𑁒spec t γ ι :
<<<
inf_mpmc_queue_2_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_2_model γ vs
>>>
inf_mpmc_queue_2٠size #t @ ↑ι
<<<
inf_mpmc_queue_2_model γ vs
| sz,
RET #sz;
⌜length vs ≤ sz⌝
>>>.
Lemma inf_mpmc_queue_2٠is_empty𑁒spec t γ ι :
<<<
inf_mpmc_queue_2_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_2_model γ vs
>>>
inf_mpmc_queue_2٠is_empty #t @ ↑ι
<<<
inf_mpmc_queue_2_model γ vs
| b,
RET #b;
⌜if b then vs = [] else True⌝
>>>.
Lemma inf_mpmc_queue_2٠push𑁒spec t γ ι v :
<<<
inf_mpmc_queue_2_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_2_model γ vs
>>>
inf_mpmc_queue_2٠push #t v @ ↑ι
<<<
inf_mpmc_queue_2_model γ (vs ++ [v])
| RET ();
True
>>>.
Lemma inf_mpmc_queue_2٠pop𑁒spec t γ ι :
<<<
inf_mpmc_queue_2_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_2_model γ vs
>>>
inf_mpmc_queue_2٠pop #t @ ↑ι
<<<
∃∃ v vs',
⌜vs = v :: vs'⌝ ∗
inf_mpmc_queue_2_model γ vs'
| RET v;
True
>>>.
End inf_mpmc_queue_2_G.
#[global] Opaque inf_mpmc_queue_2_inv.
#[global] Opaque inf_mpmc_queue_2_model.
End base.
From zoo_saturn Require
inf_mpmc_queue_2__opaque.
Section inf_mpmc_queue_2_G.
Context `{inf_mpmc_queue_2_G : InfMpmcQueue2G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition inf_mpmc_queue_2_inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.inf_mpmc_queue_2_inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition inf_mpmc_queue_2_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.inf_mpmc_queue_2_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hmodel{_{}} ) ".
#[global] Instance inf_mpmc_queue_2_model_timeless t vs :
Timeless (inf_mpmc_queue_2_model t vs).
#[global] Instance inf_mpmc_queue_2_inv_persistent t ι :
Persistent (inf_mpmc_queue_2_inv t ι).
Lemma inf_mpmc_queue_2_model_exclusive t vs1 vs2 :
inf_mpmc_queue_2_model t vs1 -∗
inf_mpmc_queue_2_model t vs2 -∗
False.
Lemma inf_mpmc_queue_2٠create𑁒spec ι :
{{{
True
}}}
inf_mpmc_queue_2٠create ()
{{{
t
, RET t;
inf_mpmc_queue_2_inv t ι ∗
inf_mpmc_queue_2_model t []
}}}.
Lemma inf_mpmc_queue_2٠size𑁒spec t ι :
<<<
inf_mpmc_queue_2_inv t ι
| ∀∀ vs,
inf_mpmc_queue_2_model t vs
>>>
inf_mpmc_queue_2٠size t @ ↑ι
<<<
inf_mpmc_queue_2_model t vs
| sz,
RET #sz;
⌜length vs ≤ sz⌝
>>>.
Lemma inf_mpmc_queue_2٠is_empty𑁒spec t ι :
<<<
inf_mpmc_queue_2_inv t ι
| ∀∀ vs,
inf_mpmc_queue_2_model t vs
>>>
inf_mpmc_queue_2٠is_empty t @ ↑ι
<<<
inf_mpmc_queue_2_model t vs
| b,
RET #b;
⌜if b then vs = [] else True⌝
>>>.
Lemma inf_mpmc_queue_2٠push𑁒spec t ι v :
<<<
inf_mpmc_queue_2_inv t ι
| ∀∀ vs,
inf_mpmc_queue_2_model t vs
>>>
inf_mpmc_queue_2٠push t v @ ↑ι
<<<
inf_mpmc_queue_2_model t (vs ++ [v])
| RET ();
True
>>>.
Lemma inf_mpmc_queue_2٠pop𑁒spec t ι :
<<<
inf_mpmc_queue_2_inv t ι
| ∀∀ vs,
inf_mpmc_queue_2_model t vs
>>>
inf_mpmc_queue_2٠pop t @ ↑ι
<<<
∃∃ v vs',
⌜vs = v :: vs'⌝ ∗
inf_mpmc_queue_2_model t vs'
| RET v;
True
>>>.
End inf_mpmc_queue_2_G.
#[global] Opaque inf_mpmc_queue_2_inv.
#[global] Opaque inf_mpmc_queue_2_model.