Library zoo_saturn.inf_mpmc_queue_1
From zoo Require Import
prelude.
From zoo.common Require Import
countable
function.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.twins
lib.mono_list
lib.saved_pred
lib.oneshot.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
prophet_nat.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
optional
inf_array
int.
From zoo_saturn Require Export
base
inf_mpmc_queue_1__code.
From zoo_saturn Require Import
inf_mpmc_queue_1__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types front back : nat.
Implicit Types v : val.
Implicit Types vs hist : list val.
Implicit Types slot : optional val.
Implicit Types slots : nat → optional val.
Implicit Types η : gname.
Implicit Types ηs : list gname.
Class InfMpmcQueue1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] inf_mpmc_queue_1_G_inf_array_G :: InfArrayG Σ
; #[local] inf_mpmc_queue_1_G_model_G :: TwinsG Σ (leibnizO (list val))
; #[local] inf_mpmc_queue_1_G_history_G :: MonoListG Σ val
; #[local] inf_mpmc_queue_1_G_consumer_G :: SavedPredG Σ val
; #[local] inf_mpmc_queue_1_G_consumers_G :: MonoListG Σ gname
; #[local] inf_mpmc_queue_1_G_token_G :: OneshotG Σ () ()
; #[local] inf_mpmc_queue_1_G_tokens_G :: MonoListG Σ gname
}.
Definition inf_mpmc_queue_1_Σ :=
#[inf_array_Σ
; twins_Σ (leibnizO (list val))
; mono_list_Σ val
; saved_pred_Σ val
; mono_list_Σ gname
; oneshot_Σ () ()
; mono_list_Σ gname
].
#[global] Instance subG_inf_mpmc_queue_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG inf_mpmc_queue_1_Σ Σ →
InfMpmcQueue1G Σ.
Module base.
Section inf_mpmc_queue_1_G.
Context `{inf_mpmc_queue_1_G : InfMpmcQueue1G Σ}.
Implicit Types t : location.
Implicit Types Ψ : val → iProp Σ.
Record inf_mpmc_queue_1_name :=
{ inf_mpmc_queue_1_name_data : val
; inf_mpmc_queue_1_name_inv : namespace
; inf_mpmc_queue_1_name_model : gname
; inf_mpmc_queue_1_name_history : gname
; inf_mpmc_queue_1_name_consumers : gname
; inf_mpmc_queue_1_name_tokens : gname
}.
Implicit Types γ : inf_mpmc_queue_1_name.
#[global] Instance inf_mpmc_queue_1_name_eq_dec : EqDecision inf_mpmc_queue_1_name :=
ltac:(solve_decision).
#[global] Instance inf_mpmc_queue_1_name_countable :
Countable inf_mpmc_queue_1_name.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ :=
model₁' γ.(inf_mpmc_queue_1_name_model).
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(inf_mpmc_queue_1_name_model).
#[local] Definition history_auth' γ_history hist :=
mono_list_auth γ_history (DfracOwn 1) hist.
#[local] Definition history_auth γ :=
history_auth' γ.(inf_mpmc_queue_1_name_history).
#[local] Definition history_at γ i v :=
mono_list_at γ.(inf_mpmc_queue_1_name_history) i v.
#[local] Definition consumers_auth' γ_consumers i : iProp Σ :=
∃ ηs,
mono_list_auth γ_consumers (DfracOwn 1) ηs ∗
⌜length ηs = i⌝.
#[local] Definition consumers_auth γ i :=
consumers_auth' γ.(inf_mpmc_queue_1_name_consumers) i.
#[local] Instance : CustomIpat "consumers_auth" :=
" ( %ηs{} & Hauth{} & %Hηs{} ) ".
#[local] Definition consumers_at γ i Ψ : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_1_name_consumers) i η ∗
saved_pred η Ψ.
#[local] Instance : CustomIpat "consumers_at" :=
" ( %η{} & Hat{} & HΨ{} ) ".
#[local] Definition consumers_lb γ i : iProp Σ :=
∃ ηs,
⌜length ηs = i⌝ ∗
mono_list_lb γ.(inf_mpmc_queue_1_name_consumers) ηs.
#[local] Instance : CustomIpat "consumers_lb" :=
" ( %ηs{} & %Hηs{} & Hlb{} ) ".
#[local] Definition tokens_auth' γ_tokens i : iProp Σ :=
∃ ηs,
mono_list_auth γ_tokens (DfracOwn 1) ηs ∗
⌜length ηs = i⌝.
#[local] Definition tokens_auth γ i :=
tokens_auth' γ.(inf_mpmc_queue_1_name_tokens) i.
#[local] Instance : CustomIpat "tokens_auth" :=
" ( %ηs{} & Hauth{} & %Hηs{} ) ".
#[local] Definition tokens_pending γ i : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_1_name_tokens) i η ∗
oneshot_pending η (DfracOwn 1) ().
#[local] Instance : CustomIpat "tokens_pending" :=
" ( %η{} & Hat{} & Hpending{} ) ".
#[local] Definition tokens_done γ i : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_1_name_tokens) i η ∗
oneshot_shot η ().
#[local] Instance : CustomIpat "tokens_done" :=
" ( %η{} & Hat{} & Hshot{} ) ".
#[local] Definition consumer_au γ Ψ : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(inf_mpmc_queue_1_name_inv), ∅ <{
∀∀ v vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
, COMM
Ψ v
}>.
#[local] Definition slot_model γ i slot : iProp Σ :=
match slot with
| Something v ⇒
history_at γ i v
| Anything ⇒
tokens_done γ i
| Nothing ⇒
True
end.
#[local] Definition inv_inner t γ : iProp Σ :=
∃ front back hist slots,
t.[front] ↦ #front ∗
t.[back] ↦ #back ∗
inf_array_model γ.(inf_mpmc_queue_1_name_data) (optional_to_val ∘ slots) ∗
history_auth γ hist ∗
⌜length hist = back⌝ ∗
model₂ γ (drop front hist) ∗
consumers_auth γ front ∗
tokens_auth γ (front `max` back) ∗
( [∗ list] i ∈ seq 0 back,
tokens_pending γ i
∨ ∃ Ψ,
consumers_at γ i Ψ ∗
( tokens_done γ i
∨ ∃ v,
history_at γ i v ∗
Ψ v
)
) ∗
( [∗ list] i ∈ seq back (front - back),
∃ Ψ,
consumers_at γ i Ψ ∗
consumer_au γ Ψ
) ∗
(∀ i, slot_model γ i (slots i)).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %front{} & %back{} & %hist{} & %slots{} & Ht_front & Ht_back & >Hdata_model & >Hhistory_auth & >%Hhist{} & Hmodel₂ & Hconsumers_auth & Htokens_auth & Hpast & Hwaiters & Hslots ) ".
Definition inv' t γ : iProp Σ :=
t.[data] ↦□ γ.(inf_mpmc_queue_1_name_data) ∗
inf_array_inv γ.(inf_mpmc_queue_1_name_data) ∗
inv γ.(inf_mpmc_queue_1_name_inv) (inv_inner t γ).
#[local] Instance : CustomIpat "inv'" :=
" ( #Ht_data & #Hdata_inv & #Hinv ) ".
Definition inf_mpmc_queue_1_inv t γ ι : iProp Σ :=
⌜ι = γ.(inf_mpmc_queue_1_name_inv)⌝ ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & (:inv') ) ".
Definition inf_mpmc_queue_1_model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
#[local] Instance tokens_pending_timeless γ i :
Timeless (tokens_pending γ i).
#[local] Instance tokens_done_timeless γ i :
Timeless (tokens_done γ i).
#[local] Instance slot_model_timeless γ i slot :
Timeless (slot_model γ i slot).
#[global] Instance inf_mpmc_queue_1_model_timeless γ vs :
Timeless (inf_mpmc_queue_1_model γ vs).
#[local] Instance consumers_at_persistent γ i Ψ :
Persistent (consumers_at γ i Ψ).
#[local] Instance consumers_lb_persistent γ i :
Persistent (consumers_lb γ i).
#[local] Instance tokens_done_persistent γ i :
Persistent (tokens_done γ i).
#[local] Instance slot_model_persistent γ i slot :
Persistent (slot_model γ i slot).
#[global] Instance inf_mpmc_queue_1_inv_persistent t γ ι :
Persistent (inf_mpmc_queue_1_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_valid γ hist i v :
history_auth γ hist -∗
history_at γ i v -∗
⌜hist !! i = Some v⌝.
#[local] Lemma history_at_agree γ i v1 v2 :
history_at γ i v1 -∗
history_at γ i v2 -∗
⌜v1 = v2⌝.
#[local] Lemma history_at_get {γ hist} i v :
hist !! i = Some v →
history_auth γ hist ⊢
history_at γ i v.
#[local] Lemma history_update {γ hist} v :
history_auth γ hist ⊢ |==>
history_auth γ (hist ++ [v]) ∗
history_at γ (length hist) v.
#[local] Lemma consumers_alloc :
⊢ |==>
∃ γ_consumers,
consumers_auth' γ_consumers 0.
#[local] Lemma consumers_at_valid γ i j Ψ :
consumers_auth γ i -∗
consumers_at γ j Ψ -∗
⌜j < i⌝.
#[local] Lemma consumers_at_agree γ i Ψ1 Ψ2 v :
consumers_at γ i Ψ1 -∗
▷ consumers_at γ i Ψ2 -∗
▷ Ψ2 v -∗
▷^2 Ψ1 v.
#[local] Lemma consumers_lb_valid γ i j :
consumers_auth γ i -∗
consumers_lb γ j -∗
⌜j ≤ i⌝.
#[local] Lemma consumers_lb_get γ i :
consumers_auth γ i ⊢
consumers_lb γ i.
#[local] Lemma consumers_update {γ i} Ψ :
consumers_auth γ i ⊢ |==>
consumers_auth γ (S i) ∗
consumers_at γ i Ψ.
Opaque consumers_auth'.
Opaque consumers_at.
Opaque consumers_lb.
#[local] Lemma tokens_alloc :
⊢ |==>
∃ γ_tokens,
tokens_auth' γ_tokens 0.
#[local] Lemma tokens_pending_exclusive γ i :
tokens_pending γ i -∗
tokens_pending γ i -∗
False.
#[local] Lemma tokens_pending_done γ i :
tokens_pending γ i -∗
tokens_done γ i -∗
False.
#[local] Lemma tokens_update {γ} i :
tokens_auth γ i ⊢ |==>
tokens_auth γ (S i) ∗
tokens_pending γ i.
#[local] Lemma tokens_pending_update γ i :
tokens_pending γ i ⊢ |==>
tokens_done γ i.
Opaque tokens_auth'.
Opaque tokens_pending.
Opaque tokens_done.
Lemma inf_mpmc_queue_1_model_exclusive γ vs1 vs2 :
inf_mpmc_queue_1_model γ vs1 -∗
inf_mpmc_queue_1_model γ vs2 -∗
False.
Lemma inf_mpmc_queue_1٠create𑁒spec ι :
{{{
True
}}}
inf_mpmc_queue_1٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
inf_mpmc_queue_1_inv t γ ι ∗
inf_mpmc_queue_1_model γ []
}}}.
Lemma inf_mpmc_queue_1٠size𑁒spec t γ ι :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠size #t @ ↑ι
<<<
inf_mpmc_queue_1_model γ vs
| RET #(length vs);
True
>>>.
Lemma inf_mpmc_queue_1٠is_empty𑁒spec t γ ι :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠is_empty #t @ ↑ι
<<<
inf_mpmc_queue_1_model γ vs
| RET #(bool_decide (vs = []%list));
True
>>>.
Lemma inf_mpmc_queue_1٠is_empty_weak𑁒spec t γ ι :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠is_empty_weak #t @ ↑ι
<<<
∃∃ b,
⌜if b then vs = [] else True⌝ ∗
inf_mpmc_queue_1_model γ vs
| RET #b;
True
>>>.
Lemma inf_mpmc_queue_1٠push𑁒spec t γ ι v :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠push #t v @ ↑ι
<<<
inf_mpmc_queue_1_model γ (vs ++ [v])
| RET ();
True
>>>.
#[local] Lemma inf_mpmc_queue_1٠pop₀𑁒spec t γ front Ψ :
{{{
inv' t γ ∗
consumers_at γ front Ψ ∗
tokens_pending γ front
}}}
inf_mpmc_queue_1٠pop₀ #t #front
{{{
v
, RET v;
Ψ v
}}}.
Lemma inf_mpmc_queue_1٠pop𑁒spec t γ ι :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠pop #t @ ↑ι
<<<
∃∃ v vs',
⌜vs = v :: vs'⌝ ∗
inf_mpmc_queue_1_model γ vs'
| RET v;
True
>>>.
Lemma inf_mpmc_queue_1٠try_pop𑁒spec t γ ι :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠try_pop #t @ ↑ι
<<<
inf_mpmc_queue_1_model γ (tail vs)
| RET head vs;
True
>>>.
End inf_mpmc_queue_1_G.
#[global] Opaque inf_mpmc_queue_1_inv.
#[global] Opaque inf_mpmc_queue_1_model.
End base.
From zoo_saturn Require
inf_mpmc_queue_1__opaque.
Section inf_mpmc_queue_1_G.
Context `{inf_mpmc_queue_1_G : InfMpmcQueue1G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition inf_mpmc_queue_1_inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.inf_mpmc_queue_1_inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition inf_mpmc_queue_1_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.inf_mpmc_queue_1_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hmodel{_{}} ) ".
#[global] Instance inf_mpmc_queue_1_model_timeless t vs :
Timeless (inf_mpmc_queue_1_model t vs).
#[global] Instance inf_mpmc_queue_1_inv_persistent t ι :
Persistent (inf_mpmc_queue_1_inv t ι).
Lemma inf_mpmc_queue_1_model_exclusive t vs1 vs2 :
inf_mpmc_queue_1_model t vs1 -∗
inf_mpmc_queue_1_model t vs2 -∗
False.
Lemma inf_mpmc_queue_1٠create𑁒spec ι :
{{{
True
}}}
inf_mpmc_queue_1٠create ()
{{{
t
, RET t;
inf_mpmc_queue_1_inv t ι ∗
inf_mpmc_queue_1_model t []
}}}.
Lemma inf_mpmc_queue_1٠size𑁒spec t ι :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠size t @ ↑ι
<<<
inf_mpmc_queue_1_model t vs
| RET #(length vs);
True
>>>.
Lemma inf_mpmc_queue_1٠is_empty𑁒spec t ι :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠is_empty t @ ↑ι
<<<
inf_mpmc_queue_1_model t vs
| RET #(bool_decide (vs = []%list));
True
>>>.
Lemma inf_mpmc_queue_1٠is_empty_weak𑁒spec t ι :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠is_empty_weak t @ ↑ι
<<<
∃∃ b,
⌜if b then vs = [] else True⌝ ∗
inf_mpmc_queue_1_model t vs
| RET #b;
True
>>>.
Lemma inf_mpmc_queue_1٠push𑁒spec t ι v :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠push t v @ ↑ι
<<<
inf_mpmc_queue_1_model t (vs ++ [v])
| RET ();
True
>>>.
Lemma inf_mpmc_queue_1٠pop𑁒spec t ι :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠pop t @ ↑ι
<<<
∃∃ v vs',
⌜vs = v :: vs'⌝ ∗
inf_mpmc_queue_1_model t vs'
| RET v;
True
>>>.
Lemma inf_mpmc_queue_1٠try_pop𑁒spec t ι :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠try_pop t @ ↑ι
<<<
inf_mpmc_queue_1_model t (tail vs)
| RET head vs;
True
>>>.
End inf_mpmc_queue_1_G.
#[global] Opaque inf_mpmc_queue_1_inv.
#[global] Opaque inf_mpmc_queue_1_model.
prelude.
From zoo.common Require Import
countable
function.
From zoo.iris.bi Require Import
big_op.
From zoo.iris.base_logic Require Import
lib.twins
lib.mono_list
lib.saved_pred
lib.oneshot.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
prophet_nat.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
optional
inf_array
int.
From zoo_saturn Require Export
base
inf_mpmc_queue_1__code.
From zoo_saturn Require Import
inf_mpmc_queue_1__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types front back : nat.
Implicit Types v : val.
Implicit Types vs hist : list val.
Implicit Types slot : optional val.
Implicit Types slots : nat → optional val.
Implicit Types η : gname.
Implicit Types ηs : list gname.
Class InfMpmcQueue1G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] inf_mpmc_queue_1_G_inf_array_G :: InfArrayG Σ
; #[local] inf_mpmc_queue_1_G_model_G :: TwinsG Σ (leibnizO (list val))
; #[local] inf_mpmc_queue_1_G_history_G :: MonoListG Σ val
; #[local] inf_mpmc_queue_1_G_consumer_G :: SavedPredG Σ val
; #[local] inf_mpmc_queue_1_G_consumers_G :: MonoListG Σ gname
; #[local] inf_mpmc_queue_1_G_token_G :: OneshotG Σ () ()
; #[local] inf_mpmc_queue_1_G_tokens_G :: MonoListG Σ gname
}.
Definition inf_mpmc_queue_1_Σ :=
#[inf_array_Σ
; twins_Σ (leibnizO (list val))
; mono_list_Σ val
; saved_pred_Σ val
; mono_list_Σ gname
; oneshot_Σ () ()
; mono_list_Σ gname
].
#[global] Instance subG_inf_mpmc_queue_1_Σ Σ `{zoo_G : !ZooG Σ} :
subG inf_mpmc_queue_1_Σ Σ →
InfMpmcQueue1G Σ.
Module base.
Section inf_mpmc_queue_1_G.
Context `{inf_mpmc_queue_1_G : InfMpmcQueue1G Σ}.
Implicit Types t : location.
Implicit Types Ψ : val → iProp Σ.
Record inf_mpmc_queue_1_name :=
{ inf_mpmc_queue_1_name_data : val
; inf_mpmc_queue_1_name_inv : namespace
; inf_mpmc_queue_1_name_model : gname
; inf_mpmc_queue_1_name_history : gname
; inf_mpmc_queue_1_name_consumers : gname
; inf_mpmc_queue_1_name_tokens : gname
}.
Implicit Types γ : inf_mpmc_queue_1_name.
#[global] Instance inf_mpmc_queue_1_name_eq_dec : EqDecision inf_mpmc_queue_1_name :=
ltac:(solve_decision).
#[global] Instance inf_mpmc_queue_1_name_countable :
Countable inf_mpmc_queue_1_name.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ :=
model₁' γ.(inf_mpmc_queue_1_name_model).
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(inf_mpmc_queue_1_name_model).
#[local] Definition history_auth' γ_history hist :=
mono_list_auth γ_history (DfracOwn 1) hist.
#[local] Definition history_auth γ :=
history_auth' γ.(inf_mpmc_queue_1_name_history).
#[local] Definition history_at γ i v :=
mono_list_at γ.(inf_mpmc_queue_1_name_history) i v.
#[local] Definition consumers_auth' γ_consumers i : iProp Σ :=
∃ ηs,
mono_list_auth γ_consumers (DfracOwn 1) ηs ∗
⌜length ηs = i⌝.
#[local] Definition consumers_auth γ i :=
consumers_auth' γ.(inf_mpmc_queue_1_name_consumers) i.
#[local] Instance : CustomIpat "consumers_auth" :=
" ( %ηs{} & Hauth{} & %Hηs{} ) ".
#[local] Definition consumers_at γ i Ψ : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_1_name_consumers) i η ∗
saved_pred η Ψ.
#[local] Instance : CustomIpat "consumers_at" :=
" ( %η{} & Hat{} & HΨ{} ) ".
#[local] Definition consumers_lb γ i : iProp Σ :=
∃ ηs,
⌜length ηs = i⌝ ∗
mono_list_lb γ.(inf_mpmc_queue_1_name_consumers) ηs.
#[local] Instance : CustomIpat "consumers_lb" :=
" ( %ηs{} & %Hηs{} & Hlb{} ) ".
#[local] Definition tokens_auth' γ_tokens i : iProp Σ :=
∃ ηs,
mono_list_auth γ_tokens (DfracOwn 1) ηs ∗
⌜length ηs = i⌝.
#[local] Definition tokens_auth γ i :=
tokens_auth' γ.(inf_mpmc_queue_1_name_tokens) i.
#[local] Instance : CustomIpat "tokens_auth" :=
" ( %ηs{} & Hauth{} & %Hηs{} ) ".
#[local] Definition tokens_pending γ i : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_1_name_tokens) i η ∗
oneshot_pending η (DfracOwn 1) ().
#[local] Instance : CustomIpat "tokens_pending" :=
" ( %η{} & Hat{} & Hpending{} ) ".
#[local] Definition tokens_done γ i : iProp Σ :=
∃ η,
mono_list_at γ.(inf_mpmc_queue_1_name_tokens) i η ∗
oneshot_shot η ().
#[local] Instance : CustomIpat "tokens_done" :=
" ( %η{} & Hat{} & Hshot{} ) ".
#[local] Definition consumer_au γ Ψ : iProp Σ :=
AU <{
∃∃ vs,
model₁ γ vs
}> @ ⊤ ∖ ↑γ.(inf_mpmc_queue_1_name_inv), ∅ <{
∀∀ v vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
, COMM
Ψ v
}>.
#[local] Definition slot_model γ i slot : iProp Σ :=
match slot with
| Something v ⇒
history_at γ i v
| Anything ⇒
tokens_done γ i
| Nothing ⇒
True
end.
#[local] Definition inv_inner t γ : iProp Σ :=
∃ front back hist slots,
t.[front] ↦ #front ∗
t.[back] ↦ #back ∗
inf_array_model γ.(inf_mpmc_queue_1_name_data) (optional_to_val ∘ slots) ∗
history_auth γ hist ∗
⌜length hist = back⌝ ∗
model₂ γ (drop front hist) ∗
consumers_auth γ front ∗
tokens_auth γ (front `max` back) ∗
( [∗ list] i ∈ seq 0 back,
tokens_pending γ i
∨ ∃ Ψ,
consumers_at γ i Ψ ∗
( tokens_done γ i
∨ ∃ v,
history_at γ i v ∗
Ψ v
)
) ∗
( [∗ list] i ∈ seq back (front - back),
∃ Ψ,
consumers_at γ i Ψ ∗
consumer_au γ Ψ
) ∗
(∀ i, slot_model γ i (slots i)).
#[local] Instance : CustomIpat "inv_inner" :=
" ( %front{} & %back{} & %hist{} & %slots{} & Ht_front & Ht_back & >Hdata_model & >Hhistory_auth & >%Hhist{} & Hmodel₂ & Hconsumers_auth & Htokens_auth & Hpast & Hwaiters & Hslots ) ".
Definition inv' t γ : iProp Σ :=
t.[data] ↦□ γ.(inf_mpmc_queue_1_name_data) ∗
inf_array_inv γ.(inf_mpmc_queue_1_name_data) ∗
inv γ.(inf_mpmc_queue_1_name_inv) (inv_inner t γ).
#[local] Instance : CustomIpat "inv'" :=
" ( #Ht_data & #Hdata_inv & #Hinv ) ".
Definition inf_mpmc_queue_1_inv t γ ι : iProp Σ :=
⌜ι = γ.(inf_mpmc_queue_1_name_inv)⌝ ∗
inv' t γ.
#[local] Instance : CustomIpat "inv" :=
" ( -> & (:inv') ) ".
Definition inf_mpmc_queue_1_model :=
model₁.
#[local] Instance : CustomIpat "model" :=
" Hmodel₁{_{}} ".
#[local] Instance tokens_pending_timeless γ i :
Timeless (tokens_pending γ i).
#[local] Instance tokens_done_timeless γ i :
Timeless (tokens_done γ i).
#[local] Instance slot_model_timeless γ i slot :
Timeless (slot_model γ i slot).
#[global] Instance inf_mpmc_queue_1_model_timeless γ vs :
Timeless (inf_mpmc_queue_1_model γ vs).
#[local] Instance consumers_at_persistent γ i Ψ :
Persistent (consumers_at γ i Ψ).
#[local] Instance consumers_lb_persistent γ i :
Persistent (consumers_lb γ i).
#[local] Instance tokens_done_persistent γ i :
Persistent (tokens_done γ i).
#[local] Instance slot_model_persistent γ i slot :
Persistent (slot_model γ i slot).
#[global] Instance inf_mpmc_queue_1_inv_persistent t γ ι :
Persistent (inf_mpmc_queue_1_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_valid γ hist i v :
history_auth γ hist -∗
history_at γ i v -∗
⌜hist !! i = Some v⌝.
#[local] Lemma history_at_agree γ i v1 v2 :
history_at γ i v1 -∗
history_at γ i v2 -∗
⌜v1 = v2⌝.
#[local] Lemma history_at_get {γ hist} i v :
hist !! i = Some v →
history_auth γ hist ⊢
history_at γ i v.
#[local] Lemma history_update {γ hist} v :
history_auth γ hist ⊢ |==>
history_auth γ (hist ++ [v]) ∗
history_at γ (length hist) v.
#[local] Lemma consumers_alloc :
⊢ |==>
∃ γ_consumers,
consumers_auth' γ_consumers 0.
#[local] Lemma consumers_at_valid γ i j Ψ :
consumers_auth γ i -∗
consumers_at γ j Ψ -∗
⌜j < i⌝.
#[local] Lemma consumers_at_agree γ i Ψ1 Ψ2 v :
consumers_at γ i Ψ1 -∗
▷ consumers_at γ i Ψ2 -∗
▷ Ψ2 v -∗
▷^2 Ψ1 v.
#[local] Lemma consumers_lb_valid γ i j :
consumers_auth γ i -∗
consumers_lb γ j -∗
⌜j ≤ i⌝.
#[local] Lemma consumers_lb_get γ i :
consumers_auth γ i ⊢
consumers_lb γ i.
#[local] Lemma consumers_update {γ i} Ψ :
consumers_auth γ i ⊢ |==>
consumers_auth γ (S i) ∗
consumers_at γ i Ψ.
Opaque consumers_auth'.
Opaque consumers_at.
Opaque consumers_lb.
#[local] Lemma tokens_alloc :
⊢ |==>
∃ γ_tokens,
tokens_auth' γ_tokens 0.
#[local] Lemma tokens_pending_exclusive γ i :
tokens_pending γ i -∗
tokens_pending γ i -∗
False.
#[local] Lemma tokens_pending_done γ i :
tokens_pending γ i -∗
tokens_done γ i -∗
False.
#[local] Lemma tokens_update {γ} i :
tokens_auth γ i ⊢ |==>
tokens_auth γ (S i) ∗
tokens_pending γ i.
#[local] Lemma tokens_pending_update γ i :
tokens_pending γ i ⊢ |==>
tokens_done γ i.
Opaque tokens_auth'.
Opaque tokens_pending.
Opaque tokens_done.
Lemma inf_mpmc_queue_1_model_exclusive γ vs1 vs2 :
inf_mpmc_queue_1_model γ vs1 -∗
inf_mpmc_queue_1_model γ vs2 -∗
False.
Lemma inf_mpmc_queue_1٠create𑁒spec ι :
{{{
True
}}}
inf_mpmc_queue_1٠create ()
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
inf_mpmc_queue_1_inv t γ ι ∗
inf_mpmc_queue_1_model γ []
}}}.
Lemma inf_mpmc_queue_1٠size𑁒spec t γ ι :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠size #t @ ↑ι
<<<
inf_mpmc_queue_1_model γ vs
| RET #(length vs);
True
>>>.
Lemma inf_mpmc_queue_1٠is_empty𑁒spec t γ ι :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠is_empty #t @ ↑ι
<<<
inf_mpmc_queue_1_model γ vs
| RET #(bool_decide (vs = []%list));
True
>>>.
Lemma inf_mpmc_queue_1٠is_empty_weak𑁒spec t γ ι :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠is_empty_weak #t @ ↑ι
<<<
∃∃ b,
⌜if b then vs = [] else True⌝ ∗
inf_mpmc_queue_1_model γ vs
| RET #b;
True
>>>.
Lemma inf_mpmc_queue_1٠push𑁒spec t γ ι v :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠push #t v @ ↑ι
<<<
inf_mpmc_queue_1_model γ (vs ++ [v])
| RET ();
True
>>>.
#[local] Lemma inf_mpmc_queue_1٠pop₀𑁒spec t γ front Ψ :
{{{
inv' t γ ∗
consumers_at γ front Ψ ∗
tokens_pending γ front
}}}
inf_mpmc_queue_1٠pop₀ #t #front
{{{
v
, RET v;
Ψ v
}}}.
Lemma inf_mpmc_queue_1٠pop𑁒spec t γ ι :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠pop #t @ ↑ι
<<<
∃∃ v vs',
⌜vs = v :: vs'⌝ ∗
inf_mpmc_queue_1_model γ vs'
| RET v;
True
>>>.
Lemma inf_mpmc_queue_1٠try_pop𑁒spec t γ ι :
<<<
inf_mpmc_queue_1_inv t γ ι
| ∀∀ vs,
inf_mpmc_queue_1_model γ vs
>>>
inf_mpmc_queue_1٠try_pop #t @ ↑ι
<<<
inf_mpmc_queue_1_model γ (tail vs)
| RET head vs;
True
>>>.
End inf_mpmc_queue_1_G.
#[global] Opaque inf_mpmc_queue_1_inv.
#[global] Opaque inf_mpmc_queue_1_model.
End base.
From zoo_saturn Require
inf_mpmc_queue_1__opaque.
Section inf_mpmc_queue_1_G.
Context `{inf_mpmc_queue_1_G : InfMpmcQueue1G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition inf_mpmc_queue_1_inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.inf_mpmc_queue_1_inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition inf_mpmc_queue_1_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.inf_mpmc_queue_1_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hmodel{_{}} ) ".
#[global] Instance inf_mpmc_queue_1_model_timeless t vs :
Timeless (inf_mpmc_queue_1_model t vs).
#[global] Instance inf_mpmc_queue_1_inv_persistent t ι :
Persistent (inf_mpmc_queue_1_inv t ι).
Lemma inf_mpmc_queue_1_model_exclusive t vs1 vs2 :
inf_mpmc_queue_1_model t vs1 -∗
inf_mpmc_queue_1_model t vs2 -∗
False.
Lemma inf_mpmc_queue_1٠create𑁒spec ι :
{{{
True
}}}
inf_mpmc_queue_1٠create ()
{{{
t
, RET t;
inf_mpmc_queue_1_inv t ι ∗
inf_mpmc_queue_1_model t []
}}}.
Lemma inf_mpmc_queue_1٠size𑁒spec t ι :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠size t @ ↑ι
<<<
inf_mpmc_queue_1_model t vs
| RET #(length vs);
True
>>>.
Lemma inf_mpmc_queue_1٠is_empty𑁒spec t ι :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠is_empty t @ ↑ι
<<<
inf_mpmc_queue_1_model t vs
| RET #(bool_decide (vs = []%list));
True
>>>.
Lemma inf_mpmc_queue_1٠is_empty_weak𑁒spec t ι :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠is_empty_weak t @ ↑ι
<<<
∃∃ b,
⌜if b then vs = [] else True⌝ ∗
inf_mpmc_queue_1_model t vs
| RET #b;
True
>>>.
Lemma inf_mpmc_queue_1٠push𑁒spec t ι v :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠push t v @ ↑ι
<<<
inf_mpmc_queue_1_model t (vs ++ [v])
| RET ();
True
>>>.
Lemma inf_mpmc_queue_1٠pop𑁒spec t ι :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠pop t @ ↑ι
<<<
∃∃ v vs',
⌜vs = v :: vs'⌝ ∗
inf_mpmc_queue_1_model t vs'
| RET v;
True
>>>.
Lemma inf_mpmc_queue_1٠try_pop𑁒spec t ι :
<<<
inf_mpmc_queue_1_inv t ι
| ∀∀ vs,
inf_mpmc_queue_1_model t vs
>>>
inf_mpmc_queue_1٠try_pop t @ ↑ι
<<<
inf_mpmc_queue_1_model t (tail vs)
| RET head vs;
True
>>>.
End inf_mpmc_queue_1_G.
#[global] Opaque inf_mpmc_queue_1_inv.
#[global] Opaque inf_mpmc_queue_1_model.