Library zoo_saturn.mpmc_queue_2
From zoo Require Import
prelude.
From zoo.common Require Import
countable
relations.
From zoo.iris.base_logic Require Import
lib.twins
lib.auth_mono
lib.auth_nat_max.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
prophet_bool.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
domain
option.
From zoo_saturn Require Export
base
mpmc_queue_2__code.
From zoo_saturn Require Import
mpmc_queue_2__types.
From zoo Require Import
options.
Implicit Types strong : bool.
Implicit Types l back back_prev : location.
Implicit Types backs : gmap location nat.
Implicit Types v w t pref suff 𝑚𝑜𝑣𝑒 : val.
Implicit Types o : option val.
Implicit Types vs vs_front vs_back move : list val.
Variant emptiness :=
| Empty
| Nonempty.
Implicit Types empty : emptiness.
#[local] Instance emptiness_inhabited : Inhabited emptiness :=
populate Empty.
#[local] Instance emptiness_eq_dec : EqDecision emptiness :=
ltac:(solve_decision).
Variant status :=
| Stable empty
| Unstable back move.
Implicit Types status : status.
#[local] Instance status_inhabited : Inhabited status :=
populate (Stable inhabitant).
#[local] Instance status_eq_dec : EqDecision status :=
ltac:(solve_decision).
Record state :=
{ state_backs : gmap location nat
; state_index : nat
; state_status : status
}.
Implicit Types state : state.
#[local] Definition state_with_status state status :=
{|state_backs := state.(state_backs)
; state_index := state.(state_index)
; state_status := status
|}.
Definition state_wf backs i :=
map_Forall (λ _ i_back, i_back ≤ i) backs.
#[local] Definition state_le state1 state2 :=
state1.(state_backs) ⊆ state2.(state_backs) ∧
state1.(state_index) ≤ state2.(state_index).
#[local] Instance state_inhabited : Inhabited state :=
populate
{|state_backs := inhabitant
; state_index := inhabitant
; state_status := inhabitant
|}.
#[local] Instance state_le_reflexive :
Reflexive state_le.
#[local] Instance state_le_transitive :
Transitive state_le.
Variant step : relation state :=
| step_empty state1 state2 :
state1.(state_status) = Stable Nonempty →
state2 = state_with_status state1 (Stable Empty) →
step state1 state2
| step_destabilize state1 state2 back move :
state1.(state_status) = Stable Empty →
state2 = state_with_status state1 (Unstable back move) →
step state1 state2
| step_stabilize state1 state2 back move :
state1.(state_status) = Unstable back move →
state1.(state_backs) !! back = None →
state2 =
{|state_backs := <[back := state1.(state_index) + length move]> state1.(state_backs)
; state_index := state1.(state_index) + length move
; state_status := Stable Nonempty
|} →
step state1 state2.
#[local] Hint Constructors step : core.
#[local] Definition steps :=
rtc step.
#[local] Lemma step_mono state1 state2 :
step state1 state2 →
state_le state1 state2.
#[local] Lemma steps_mono state1 state2 :
steps state1 state2 →
state_le state1 state2.
Class MpmcQueue2G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] mpmc_queue_2_G_model_G :: TwinsG Σ (leibnizO (list val))
; #[local] mpmc_queue_2_G_state_G :: AuthMonoG (A := leibnizO state) Σ step
; #[local] mpmc_queue_2_G_front_G :: AuthNatMaxG Σ
}.
Definition mpmc_queue_2_Σ :=
#[twins_Σ (leibnizO (list val))
; auth_mono_Σ (A := leibnizO state) step
; auth_nat_max_Σ
].
#[global] Instance subG_mpmc_queue_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG mpmc_queue_2_Σ Σ →
MpmcQueue2G Σ.
#[local] Fixpoint suffix_to_val (i : nat) vs : val :=
match vs with
| [] ⇒
‘Front[ #i ]
| v :: vs ⇒
‘Cons[ #i, v, suffix_to_val (S i) vs ]
end.
#[local] Lemma suffix_to_val_generative i1 vs1 i2 vs2 :
suffix_to_val i1 vs1 ≈ suffix_to_val i2 vs2 →
suffix_to_val i1 vs1 = suffix_to_val i2 vs2.
#[local] Instance suffix_to_val_inj2 :
Inj2 (=) (=) (=) suffix_to_val.
#[local] Instance suffix_to_val_inj2' :
Inj2 (=) (=) (≈) suffix_to_val.
#[local] Fixpoint prefix_to_val (i : nat) back vs : val :=
match vs with
| [] ⇒
#back
| v :: vs ⇒
‘Snoc[ #⁺(i + S (length vs)), v, prefix_to_val i back vs ]
end.
#[local] Lemma prefix_to_val_generative i1 back1 vs1 i2 back2 vs2 :
prefix_to_val i1 back1 vs1 ≈ prefix_to_val i2 back2 vs2 →
prefix_to_val i1 back1 vs1 = prefix_to_val i2 back2 vs2.
#[local] Lemma prefix_to_val_inj i1 back1 vs1 i2 back2 vs2 :
prefix_to_val i1 back1 vs1 = prefix_to_val i2 back2 vs2 →
(vs1 ≠ [] → i1 = i2) ∧
back1 = back2 ∧
vs1 = vs2.
#[local] Lemma prefix_to_val_inj' i1 back1 vs1 i2 back2 vs2 :
prefix_to_val i1 back1 vs1 ≈ prefix_to_val i2 back2 vs2 →
(vs1 ≠ [] → i1 = i2) ∧
back1 = back2 ∧
vs1 = vs2.
Section mpmc_queue_2_G.
Context `{mpmc_queue_2_G : MpmcQueue2G Σ}.
Record metadata :=
{ metadata_inv : namespace
; metadata_model : gname
; metadata_state : gname
; metadata_front : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ :=
model₁' γ.(metadata_model).
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(metadata_model).
#[local] Definition state_auth' γ_state backs i status : iProp Σ :=
auth_mono_auth _ γ_state (DfracOwn 1)
{|state_backs := backs
; state_index := i
; state_status := status
|} ∗
⌜state_wf backs i⌝.
#[local] Instance : CustomIpat "state_auth" :=
" ( Hauth & %Hwf ) ".
#[local] Definition state_auth γ backs i status :=
state_auth' γ.(metadata_state) backs i status.
#[local] Definition state_lb γ backs i status :=
auth_mono_lb _ γ.(metadata_state)
{|state_backs := backs
; state_index := i
; state_status := status
|}.
#[local] Definition state_seen γ back i_prev back_prev move : iProp Σ :=
∃ backs,
state_lb γ backs i_prev (Unstable back move) ∗
⌜backs !! back_prev = Some i_prev⌝.
#[local] Instance : CustomIpat "state_seen" :=
" ( %backs{} & #Hstate_lb & %Hbacks{}_lookup ) ".
#[local] Definition state_at γ back i_back : iProp Σ :=
∃ backs i status,
state_lb γ backs i status ∗
⌜backs !! back = Some i_back⌝ ∗
⌜i_back ≤ i⌝.
#[local] Instance : CustomIpat "state_at" :=
" ( %backs{} & %i{} & %status{} & #Hstate_lb{_{}} & %Hbacks{}_lookup & %Hi{} ) ".
#[local] Definition front_auth' γ_front i :=
auth_nat_max_auth γ_front (DfracOwn 1) i.
#[local] Definition front_auth γ i :=
front_auth' γ.(metadata_front) i.
#[local] Definition front_lb γ i :=
auth_nat_max_lb γ.(metadata_front) i.
#[local] Definition move_model_1 𝑚𝑜𝑣𝑒 i_prev back_prev move : iProp Σ :=
⌜𝑚𝑜𝑣𝑒 = §Used%V⌝
∨ ⌜𝑚𝑜𝑣𝑒 = prefix_to_val i_prev back_prev move⌝ ∗
⌜0 < length move⌝ ∗
back_prev ↦ₕ Header §Back 2.
#[local] Instance : CustomIpat "move_model_1" :=
" [ -> | ( -> & % & #Hback{}_prev_header ) ] ".
#[local] Definition move_model_2 γ back 𝑚𝑜𝑣𝑒 : iProp Σ :=
∃ backs_prev i_prev back_prev move,
state_lb γ backs_prev i_prev (Unstable back move) ∗
move_model_1 𝑚𝑜𝑣𝑒 i_prev back_prev move.
#[local] Instance : CustomIpat "move_model_2" :=
" ( %backs{}_prev & %i{}_prev{_{!}} & %back{}_prev{_{!}} & %move{}{_{!}} & #Hstate_lb_unstable{_{}} & H𝑚𝑜𝑣𝑒{} ) ".
#[local] Definition back_model_1 back (i : nat) : iProp Σ :=
back ↦ₕ Header §Back 2 ∗
back.[index] ↦□ #i.
#[local] Instance : CustomIpat "back_model_1" :=
" ( { {!} _ ; #Hback{}_header ; #Hback_header } & #Hback{}_index{_{!}} ) ".
#[local] Definition back_model_2 back (i : nat) 𝑚𝑜𝑣𝑒 : iProp Σ :=
back_model_1 back i ∗
back.[move] ↦ 𝑚𝑜𝑣𝑒.
#[local] Instance : CustomIpat "back_model_2" :=
" ( { {only_move} _ ; (:back_model_1 // /!/) } & Hback{}_move{_{suff}} ) ".
#[local] Definition back_model_3 γ back i : iProp Σ :=
∃ 𝑚𝑜𝑣𝑒,
back_model_2 back i 𝑚𝑜𝑣𝑒 ∗
move_model_2 γ back 𝑚𝑜𝑣𝑒.
#[local] Instance : CustomIpat "back_model_3" :=
" ( %𝑚𝑜𝑣𝑒{} & (:back_model_2) & H𝑚𝑜𝑣𝑒{} ) ".
#[local] Definition inv_status_stable γ i vs_front i_back back vs_back vs empty : iProp Σ :=
⌜i_back = i⌝ ∗
⌜vs = vs_front ++ reverse vs_back⌝ ∗
⌜if empty then vs_front = [] else 0 < length vs_front⌝ ∗
state_at γ back i_back.
#[local] Instance : CustomIpat "inv_status_stable" :=
" ( {>;}-> & {>;}%Hvs{} & {>;}{{empty}->;%Hempty{};%Hempty} & {>;}#Hstate_at{_{}} ) ".
#[local] Definition inv_status_unstable strong γ backs i vs_front i_back back vs_back vs back_ move : iProp Σ :=
∃ back_prev,
⌜back_ = back⌝ ∗
⌜i_back = (i + length move)%nat⌝ ∗
⌜vs_front = []⌝ ∗
⌜vs_back = []⌝ ∗
⌜vs = reverse move⌝ ∗
⌜0 < length move⌝ ∗
state_at γ back_prev i ∗
back_model_2 back i_back (prefix_to_val i back_prev move) ∗
if strong then
⌜backs !! back = None⌝ ∗
back_prev ↦ₕ Header §Back 2
else
True.
#[local] Instance : CustomIpat "inv_status_unstable" :=
" ( %back{}_prev & {>;}-> & {>;}-> & {>;}{{lazy}%Hvs_front{};->} & {>;}{{lazy}%Hvs_back{};->} & {>;}-> & {>;}% & {>;}#Hstate_at_back{}_prev & Hback{} & { {strong} %Hbacks{}_lookup & #Hback{}_prev_header ; _ } ) ".
#[local] Definition inv_status strong γ backs i status vs_front i_back back vs_back vs : iProp Σ :=
match status with
| Stable empty ⇒
inv_status_stable γ i vs_front i_back back vs_back vs empty
| Unstable back_ move ⇒
inv_status_unstable strong γ backs i vs_front i_back back vs_back vs back_ move
end.
#[local] Definition inv_inner strong l γ : iProp Σ :=
∃ backs i status i_front vs_front i_back back vs_back vs,
l.[front] ↦ suffix_to_val i_front vs_front ∗
front_auth γ i_front ∗
l.[back] ↦ prefix_to_val i_back back vs_back ∗
([∗ map] back ↦ i ∈ backs, back_model_3 γ back i) ∗
model₂ γ vs ∗
state_auth γ backs i status ∗
⌜(i_front + length vs_front)%nat = S i⌝ ∗
inv_status strong γ backs i status vs_front i_back back vs_back vs.
#[local] Instance : CustomIpat "inv_inner" :=
" ( %backs{} & %i{} & %status{} & %i_front{} & %vs_front{} & %i_back{} & %back{} & %vs_back{} & %vs{} & Hl_front & {>;}Hfront_auth & Hl_back & Hbacks & Hmodel₂ & {>;}Hstate_auth & {>;}%Hfront{} & Hstatus ) ".
#[local] Definition inv' l γ : iProp Σ :=
inv γ.(metadata_inv) (inv_inner false l γ).
Definition mpmc_queue_2_inv t ι : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
⌜ι = γ.(metadata_inv)⌝ ∗
meta l nroot γ ∗
inv' l γ.
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & -> & -> & #Hmeta & #Hinv ) ".
Definition mpmc_queue_2_model t vs : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
model₁ γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Hmodel₁{_{}} ) ".
#[local] Instance state_auth_timeless γ backs i status :
Timeless (state_auth γ backs i status).
#[local] Instance state_at_timeless γ back i_back :
Timeless (state_at γ back i_back).
#[global] Instance mpmc_queue_2_model_timeless t vs :
Timeless (mpmc_queue_2_model t vs).
#[local] Instance state_at_persistent γ back i_back :
Persistent (state_at γ back i_back).
#[global] Instance mpmc_queue_2_inv_persistent t ι :
Persistent (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 state_alloc back :
⊢ |==>
∃ γ_state,
state_auth' γ_state ∅ 0 (Unstable back []).
#[local] Lemma state_auth_wf γ backs i status :
state_auth γ backs i status ⊢
⌜state_wf backs i⌝.
#[local] Lemma state_lb_get γ backs i status :
state_auth γ backs i status ⊢
state_lb γ backs i status.
#[local] Lemma state_at_get {γ backs i status} back i_back :
backs !! back = Some i_back →
state_auth γ backs i status ⊢
state_at γ back i_back.
#[local] Lemma state_lb_valid γ backs1 i1 status1 backs2 i2 status2 :
state_auth γ backs1 i1 status1 -∗
state_lb γ backs2 i2 status2 -∗
⌜backs2 ⊆ backs1⌝ ∗
⌜i2 ≤ i1⌝.
#[local] Lemma state_lb_valid_Unstable γ backs1 i1 status1 backs2 i2 back2 move2 :
state_auth γ backs1 i1 status1 -∗
state_lb γ backs2 i2 (Unstable back2 move2) -∗
⌜backs1 = backs2⌝ ∗
⌜i1 = i2⌝ ∗
⌜status1 = Unstable back2 move2⌝
∨ ⌜backs1 !! back2 = Some (i2 + length move2)%nat⌝ ∗
⌜i2 + length move2 ≤ i1⌝ ∗
state_at γ back2 (i2 + length move2).
#[local] Lemma state_lb_lookup {γ backs1 i1 status1 backs2 i2 status2} back i_back :
backs2 !! back = Some i_back →
state_auth γ backs1 i1 status1 -∗
state_lb γ backs2 i2 status2 -∗
⌜backs1 !! back = Some i_back⌝.
#[local] Lemma state_seen_valid γ backs i status back i_prev back_prev move :
state_auth γ backs i status -∗
state_seen γ back i_prev back_prev move -∗
⌜backs !! back_prev = Some i_prev⌝ ∗
( ⌜i = i_prev⌝ ∗
⌜status = Unstable back move⌝
∨ ⌜backs !! back = Some (i_prev + length move)%nat⌝ ∗
⌜i_prev + length move ≤ i⌝ ∗
state_at γ back (i_prev + length move)
).
#[local] Lemma state_at_valid γ backs i status back i_back :
state_auth γ backs i status -∗
state_at γ back i_back -∗
⌜backs !! back = Some i_back⌝ ∗
⌜i_back ≤ i⌝.
#[local] Lemma state_lb_stabilized γ backs1 i1 status1 backs2 i2 back2 move2 :
( status1 ≠ Unstable back2 move2
∨ i2 + length move2 ≤ i1 ∧
0 < length move2
) →
state_auth γ backs1 i1 status1 -∗
state_lb γ backs2 i2 (Unstable back2 move2) -∗
⌜backs1 !! back2 = Some (i2 + length move2)%nat⌝ ∗
state_at γ back2 (i2 + length move2).
#[local] Lemma state_lb_unstabilized γ backs1 i1 status1 backs2 i2 back2 move2 :
i1 < i2 + length move2 →
state_auth γ backs1 i1 status1 -∗
state_lb γ backs2 i2 (Unstable back2 move2) -∗
⌜backs1 = backs2⌝ ∗
⌜i1 = i2⌝ ∗
⌜status1 = Unstable back2 move2⌝.
#[local] Lemma state_stabilize γ backs i back move :
backs !! back = None →
state_auth γ backs i (Unstable back move) ⊢ |==>
state_auth γ (<[back := i + length move]> backs) (i + length move) (Stable Nonempty) ∗
state_lb γ (<[back := i + length move]> backs) (i + length move) (Stable Nonempty) ∗
state_at γ back (i + length move).
#[local] Lemma state_empty γ backs i :
state_auth γ backs i (Stable Nonempty) ⊢ |==>
state_auth γ backs i (Stable Empty).
#[local] Lemma state_destabilize {γ backs i} back move :
state_auth γ backs i (Stable Empty) ⊢ |==>
state_auth γ backs i (Unstable back move).
#[local] Lemma front_alloc :
⊢ |==>
∃ γ_front,
front_auth' γ_front 1.
#[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 :
front_auth γ i ⊢ |==>
front_auth γ (S i).
Opaque state_auth.
Opaque state_at.
#[local] Lemma inv_status_weaken γ backs i status vs_front i_back back vs_back vs :
inv_status true γ backs i status vs_front i_back back vs_back vs ⊢
inv_status false γ backs i status vs_front i_back back vs_back vs.
#[local] Lemma inv_status_Stable strong γ backs i status vs_front i_back back vs_back vs :
( strong = true ∧ is_Some (backs !! back)
∨ 0 < length vs_front
∨ 0 < length vs_back
) →
inv_status strong γ backs i status vs_front i_back back vs_back vs ⊢
∃ empty,
⌜status = Stable empty⌝ ∗
inv_status_stable γ i vs_front i_back back vs_back vs empty.
#[local] Lemma inv_inner_strengthen l γ :
inv_inner false l γ ⊢
inv_inner true l γ.
#[local] Lemma inv'_state_at {l γ} back i_back :
inv' l γ -∗
state_at γ back i_back ={⊤}=∗
back_model_1 back i_back.
Lemma mpmc_queue_2_model_exclusive t vs1 vs2 :
mpmc_queue_2_model t vs1 -∗
mpmc_queue_2_model t vs2 -∗
False.
#[local] Lemma mpmc_queue_2٠suffix_index𑁒spec (i : nat) vs :
{{{
True
}}}
mpmc_queue_2٠suffix_index (suffix_to_val i vs)
{{{
RET #i;
True
}}}.
#[local] Lemma mpmc_queue_2٠prefix_index𑁒spec (i : nat) back vs :
{{{
back ↦ₕ Header §Back 2 ∗
back.[index] ↦□ #i
}}}
mpmc_queue_2٠prefix_index (prefix_to_val i back vs)
{{{
RET #⁺(i + length vs);
True
}}}.
#[local] Lemma mpmc_queue_2٠rev₀𑁒spec i vs1 vs2 back :
0 < length vs1 →
{{{
back ↦ₕ Header §Back 2
}}}
mpmc_queue_2٠rev₀ (suffix_to_val (i + S (length vs2)) vs1) (prefix_to_val i back vs2)
{{{
RET suffix_to_val (S i) (reverse vs2 ++ vs1);
True
}}}.
#[local] Lemma mpmc_queue_2٠rev𑁒spec i back vs :
0 < length vs →
{{{
back ↦ₕ Header §Back 2
}}}
mpmc_queue_2٠rev (prefix_to_val i back vs)
{{{
RET suffix_to_val (S i) (reverse vs);
True
}}}.
Lemma mpmc_queue_2٠create𑁒spec ι :
{{{
True
}}}
mpmc_queue_2٠create ()
{{{
t
, RET t;
mpmc_queue_2_inv t ι ∗
mpmc_queue_2_model t []
}}}.
#[local] Lemma front𑁒spec_strong {l γ} i_front i_back :
{{{
inv' l γ ∗
match i_front with
| None ⇒
True
| Some i_front ⇒
front_lb γ i_front
end ∗
match i_back with
| None ⇒
True
| Some i_back ⇒
∃ back,
state_at γ back i_back
end
}}}
(#l).{front}
{{{
i_front' vs_front'
, RET suffix_to_val i_front' vs_front';
front_lb γ i_front' ∗
match i_front with
| None ⇒
True
| Some i_front ⇒
⌜i_front ≤ i_front'⌝
end ∗
match i_back with
| None ⇒
True
| Some i_back ⇒
∃ i',
⌜i_back ≤ i'⌝ ∗
⌜(i_front' + length vs_front')%nat = S i'⌝
end
}}}.
#[local] Lemma front𑁒spec l γ :
{{{
inv' l γ
}}}
(#l).{front}
{{{
i_front' vs_front'
, RET suffix_to_val i_front' vs_front';
front_lb γ i_front'
}}}.
#[local] Lemma move𑁒spec l γ backs back i move :
{{{
inv' l γ ∗
state_lb γ backs i (Unstable back move)
}}}
(#back).{move}
{{{
𝑚𝑜𝑣𝑒
, RET 𝑚𝑜𝑣𝑒;
⌜𝑚𝑜𝑣𝑒 = §Used%V⌝
∨ ∃ backs i back_prev move,
⌜𝑚𝑜𝑣𝑒 = prefix_to_val i back_prev move⌝ ∗
⌜0 < length move⌝ ∗
state_lb γ backs i (Unstable back move)
}}}.
Lemma mpmc_queue_2٠size𑁒spec t ι :
<<<
mpmc_queue_2_inv t ι
| ∀∀ vs,
mpmc_queue_2_model t vs
>>>
mpmc_queue_2٠size t @ ↑ι
<<<
mpmc_queue_2_model t vs
| RET #(length vs);
True
>>>.
Lemma mpmc_queue_2٠is_empty𑁒spec t ι :
<<<
mpmc_queue_2_inv t ι
| ∀∀ vs,
mpmc_queue_2_model t vs
>>>
mpmc_queue_2٠is_empty t @ ↑ι
<<<
mpmc_queue_2_model t vs
| RET #(bool_decide (vs = []%list));
True
>>>.
#[local] Lemma mpmc_queue_2٠finish𑁒spec {l γ} i_back back :
{{{
inv' l γ ∗
state_at γ back i_back
}}}
mpmc_queue_2٠finish #back
{{{
RET ();
True
}}}.
#[local] Lemma mpmc_queue_2٠help𑁒spec {l γ backs i back_prev back} move :
0 < length move →
{{{
inv' l γ ∗
state_lb γ backs i (Unstable back move) ∗
back_prev ↦ₕ Header §Back 2
}}}
mpmc_queue_2٠help #l #back #⁺(i + length move) (prefix_to_val i back_prev move)
{{{
RET ();
True
}}}.
#[local] Lemma mpmc_queue_2٠push𑁒spec_aux l γ v :
⊢ (
∀ back i ws (j : Z),
<<<
⌜j = ⁺(i + length ws)⌝ ∗
inv' l γ ∗
state_at γ back i
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠push_aux #l v #j (prefix_to_val i back ws) @ ↑γ.(metadata_inv)
<<<
model₁ γ (vs ++ [v])
| RET ();
True
>>>
) ∧ (
<<<
inv' l γ
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠push #l v @ ↑γ.(metadata_inv)
<<<
model₁ γ (vs ++ [v])
| RET ();
True
>>>
).
Lemma mpmc_queue_2٠push𑁒spec t v ι :
<<<
mpmc_queue_2_inv t ι
| ∀∀ vs,
mpmc_queue_2_model t vs
>>>
mpmc_queue_2٠push t v @ ↑ι
<<<
mpmc_queue_2_model t (vs ++ [v])
| RET ();
True
>>>.
#[local] Lemma mpmc_queue_2٠pop𑁒spec_aux l γ :
⊢ (
∀ i_front vs_front,
<<<
inv' l γ ∗
front_lb γ i_front
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠pop_1 #l (suffix_to_val i_front vs_front) @ ↑γ.(metadata_inv)
<<<
∃∃ o,
match o with
| None ⇒
model₁ γ vs
| Some v ⇒
∃ vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
end
| RET o;
True
>>>
) ∧ (
∀ (i_front : nat) backs back i back_prev move,
<<<
⌜i_front ≤ S i⌝ ∗
⌜1 < length move⌝ ∗
inv' l γ ∗
state_lb γ backs i (Unstable back move) ∗
back_prev ↦ₕ Header §Back 2
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠pop_2 #l ’Front[ #i_front ] #back (prefix_to_val i back_prev move) @ ↑γ.(metadata_inv)
<<<
∃∃ o,
match o with
| None ⇒
model₁ γ vs
| Some v ⇒
∃ vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
end
| RET o;
True
>>>
) ∧ (
∀ i_front,
<<<
inv' l γ
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠pop_3 #l ’Front[ #i_front ] @ ↑γ.(metadata_inv)
<<<
∃∃ o,
match o with
| None ⇒
model₁ γ vs
| Some v ⇒
∃ vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
end
| RET o;
True
>>>
) ∧ (
<<<
inv' l γ
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠pop #l @ ↑γ.(metadata_inv)
<<<
∃∃ o,
match o with
| None ⇒
model₁ γ vs
| Some v ⇒
∃ vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
end
| RET o;
True
>>>
).
Lemma mpmc_queue_2٠pop𑁒spec t ι :
<<<
mpmc_queue_2_inv t ι
| ∀∀ vs,
mpmc_queue_2_model t vs
>>>
mpmc_queue_2٠pop t @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
mpmc_queue_2_model t vs
| Some v ⇒
∃ vs',
⌜vs = v :: vs'⌝ ∗
mpmc_queue_2_model t vs'
end
| RET o;
True
>>>.
End mpmc_queue_2_G.
From zoo_saturn Require
mpmc_queue_2__opaque.
#[global] Opaque mpmc_queue_2_inv.
#[global] Opaque mpmc_queue_2_model.
prelude.
From zoo.common Require Import
countable
relations.
From zoo.iris.base_logic Require Import
lib.twins
lib.auth_mono
lib.auth_nat_max.
From zoo.language Require Import
notations.
From zoo.program_logic Require Import
prophet_bool.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
domain
option.
From zoo_saturn Require Export
base
mpmc_queue_2__code.
From zoo_saturn Require Import
mpmc_queue_2__types.
From zoo Require Import
options.
Implicit Types strong : bool.
Implicit Types l back back_prev : location.
Implicit Types backs : gmap location nat.
Implicit Types v w t pref suff 𝑚𝑜𝑣𝑒 : val.
Implicit Types o : option val.
Implicit Types vs vs_front vs_back move : list val.
Variant emptiness :=
| Empty
| Nonempty.
Implicit Types empty : emptiness.
#[local] Instance emptiness_inhabited : Inhabited emptiness :=
populate Empty.
#[local] Instance emptiness_eq_dec : EqDecision emptiness :=
ltac:(solve_decision).
Variant status :=
| Stable empty
| Unstable back move.
Implicit Types status : status.
#[local] Instance status_inhabited : Inhabited status :=
populate (Stable inhabitant).
#[local] Instance status_eq_dec : EqDecision status :=
ltac:(solve_decision).
Record state :=
{ state_backs : gmap location nat
; state_index : nat
; state_status : status
}.
Implicit Types state : state.
#[local] Definition state_with_status state status :=
{|state_backs := state.(state_backs)
; state_index := state.(state_index)
; state_status := status
|}.
Definition state_wf backs i :=
map_Forall (λ _ i_back, i_back ≤ i) backs.
#[local] Definition state_le state1 state2 :=
state1.(state_backs) ⊆ state2.(state_backs) ∧
state1.(state_index) ≤ state2.(state_index).
#[local] Instance state_inhabited : Inhabited state :=
populate
{|state_backs := inhabitant
; state_index := inhabitant
; state_status := inhabitant
|}.
#[local] Instance state_le_reflexive :
Reflexive state_le.
#[local] Instance state_le_transitive :
Transitive state_le.
Variant step : relation state :=
| step_empty state1 state2 :
state1.(state_status) = Stable Nonempty →
state2 = state_with_status state1 (Stable Empty) →
step state1 state2
| step_destabilize state1 state2 back move :
state1.(state_status) = Stable Empty →
state2 = state_with_status state1 (Unstable back move) →
step state1 state2
| step_stabilize state1 state2 back move :
state1.(state_status) = Unstable back move →
state1.(state_backs) !! back = None →
state2 =
{|state_backs := <[back := state1.(state_index) + length move]> state1.(state_backs)
; state_index := state1.(state_index) + length move
; state_status := Stable Nonempty
|} →
step state1 state2.
#[local] Hint Constructors step : core.
#[local] Definition steps :=
rtc step.
#[local] Lemma step_mono state1 state2 :
step state1 state2 →
state_le state1 state2.
#[local] Lemma steps_mono state1 state2 :
steps state1 state2 →
state_le state1 state2.
Class MpmcQueue2G Σ `{zoo_G : !ZooG Σ} :=
{ #[local] mpmc_queue_2_G_model_G :: TwinsG Σ (leibnizO (list val))
; #[local] mpmc_queue_2_G_state_G :: AuthMonoG (A := leibnizO state) Σ step
; #[local] mpmc_queue_2_G_front_G :: AuthNatMaxG Σ
}.
Definition mpmc_queue_2_Σ :=
#[twins_Σ (leibnizO (list val))
; auth_mono_Σ (A := leibnizO state) step
; auth_nat_max_Σ
].
#[global] Instance subG_mpmc_queue_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG mpmc_queue_2_Σ Σ →
MpmcQueue2G Σ.
#[local] Fixpoint suffix_to_val (i : nat) vs : val :=
match vs with
| [] ⇒
‘Front[ #i ]
| v :: vs ⇒
‘Cons[ #i, v, suffix_to_val (S i) vs ]
end.
#[local] Lemma suffix_to_val_generative i1 vs1 i2 vs2 :
suffix_to_val i1 vs1 ≈ suffix_to_val i2 vs2 →
suffix_to_val i1 vs1 = suffix_to_val i2 vs2.
#[local] Instance suffix_to_val_inj2 :
Inj2 (=) (=) (=) suffix_to_val.
#[local] Instance suffix_to_val_inj2' :
Inj2 (=) (=) (≈) suffix_to_val.
#[local] Fixpoint prefix_to_val (i : nat) back vs : val :=
match vs with
| [] ⇒
#back
| v :: vs ⇒
‘Snoc[ #⁺(i + S (length vs)), v, prefix_to_val i back vs ]
end.
#[local] Lemma prefix_to_val_generative i1 back1 vs1 i2 back2 vs2 :
prefix_to_val i1 back1 vs1 ≈ prefix_to_val i2 back2 vs2 →
prefix_to_val i1 back1 vs1 = prefix_to_val i2 back2 vs2.
#[local] Lemma prefix_to_val_inj i1 back1 vs1 i2 back2 vs2 :
prefix_to_val i1 back1 vs1 = prefix_to_val i2 back2 vs2 →
(vs1 ≠ [] → i1 = i2) ∧
back1 = back2 ∧
vs1 = vs2.
#[local] Lemma prefix_to_val_inj' i1 back1 vs1 i2 back2 vs2 :
prefix_to_val i1 back1 vs1 ≈ prefix_to_val i2 back2 vs2 →
(vs1 ≠ [] → i1 = i2) ∧
back1 = back2 ∧
vs1 = vs2.
Section mpmc_queue_2_G.
Context `{mpmc_queue_2_G : MpmcQueue2G Σ}.
Record metadata :=
{ metadata_inv : namespace
; metadata_model : gname
; metadata_state : gname
; metadata_front : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
#[local] Definition model₁' γ_model vs :=
twins_twin1 γ_model (DfracOwn 1) vs.
#[local] Definition model₁ γ :=
model₁' γ.(metadata_model).
#[local] Definition model₂' γ_model vs :=
twins_twin2 γ_model vs.
#[local] Definition model₂ γ :=
model₂' γ.(metadata_model).
#[local] Definition state_auth' γ_state backs i status : iProp Σ :=
auth_mono_auth _ γ_state (DfracOwn 1)
{|state_backs := backs
; state_index := i
; state_status := status
|} ∗
⌜state_wf backs i⌝.
#[local] Instance : CustomIpat "state_auth" :=
" ( Hauth & %Hwf ) ".
#[local] Definition state_auth γ backs i status :=
state_auth' γ.(metadata_state) backs i status.
#[local] Definition state_lb γ backs i status :=
auth_mono_lb _ γ.(metadata_state)
{|state_backs := backs
; state_index := i
; state_status := status
|}.
#[local] Definition state_seen γ back i_prev back_prev move : iProp Σ :=
∃ backs,
state_lb γ backs i_prev (Unstable back move) ∗
⌜backs !! back_prev = Some i_prev⌝.
#[local] Instance : CustomIpat "state_seen" :=
" ( %backs{} & #Hstate_lb & %Hbacks{}_lookup ) ".
#[local] Definition state_at γ back i_back : iProp Σ :=
∃ backs i status,
state_lb γ backs i status ∗
⌜backs !! back = Some i_back⌝ ∗
⌜i_back ≤ i⌝.
#[local] Instance : CustomIpat "state_at" :=
" ( %backs{} & %i{} & %status{} & #Hstate_lb{_{}} & %Hbacks{}_lookup & %Hi{} ) ".
#[local] Definition front_auth' γ_front i :=
auth_nat_max_auth γ_front (DfracOwn 1) i.
#[local] Definition front_auth γ i :=
front_auth' γ.(metadata_front) i.
#[local] Definition front_lb γ i :=
auth_nat_max_lb γ.(metadata_front) i.
#[local] Definition move_model_1 𝑚𝑜𝑣𝑒 i_prev back_prev move : iProp Σ :=
⌜𝑚𝑜𝑣𝑒 = §Used%V⌝
∨ ⌜𝑚𝑜𝑣𝑒 = prefix_to_val i_prev back_prev move⌝ ∗
⌜0 < length move⌝ ∗
back_prev ↦ₕ Header §Back 2.
#[local] Instance : CustomIpat "move_model_1" :=
" [ -> | ( -> & % & #Hback{}_prev_header ) ] ".
#[local] Definition move_model_2 γ back 𝑚𝑜𝑣𝑒 : iProp Σ :=
∃ backs_prev i_prev back_prev move,
state_lb γ backs_prev i_prev (Unstable back move) ∗
move_model_1 𝑚𝑜𝑣𝑒 i_prev back_prev move.
#[local] Instance : CustomIpat "move_model_2" :=
" ( %backs{}_prev & %i{}_prev{_{!}} & %back{}_prev{_{!}} & %move{}{_{!}} & #Hstate_lb_unstable{_{}} & H𝑚𝑜𝑣𝑒{} ) ".
#[local] Definition back_model_1 back (i : nat) : iProp Σ :=
back ↦ₕ Header §Back 2 ∗
back.[index] ↦□ #i.
#[local] Instance : CustomIpat "back_model_1" :=
" ( { {!} _ ; #Hback{}_header ; #Hback_header } & #Hback{}_index{_{!}} ) ".
#[local] Definition back_model_2 back (i : nat) 𝑚𝑜𝑣𝑒 : iProp Σ :=
back_model_1 back i ∗
back.[move] ↦ 𝑚𝑜𝑣𝑒.
#[local] Instance : CustomIpat "back_model_2" :=
" ( { {only_move} _ ; (:back_model_1 // /!/) } & Hback{}_move{_{suff}} ) ".
#[local] Definition back_model_3 γ back i : iProp Σ :=
∃ 𝑚𝑜𝑣𝑒,
back_model_2 back i 𝑚𝑜𝑣𝑒 ∗
move_model_2 γ back 𝑚𝑜𝑣𝑒.
#[local] Instance : CustomIpat "back_model_3" :=
" ( %𝑚𝑜𝑣𝑒{} & (:back_model_2) & H𝑚𝑜𝑣𝑒{} ) ".
#[local] Definition inv_status_stable γ i vs_front i_back back vs_back vs empty : iProp Σ :=
⌜i_back = i⌝ ∗
⌜vs = vs_front ++ reverse vs_back⌝ ∗
⌜if empty then vs_front = [] else 0 < length vs_front⌝ ∗
state_at γ back i_back.
#[local] Instance : CustomIpat "inv_status_stable" :=
" ( {>;}-> & {>;}%Hvs{} & {>;}{{empty}->;%Hempty{};%Hempty} & {>;}#Hstate_at{_{}} ) ".
#[local] Definition inv_status_unstable strong γ backs i vs_front i_back back vs_back vs back_ move : iProp Σ :=
∃ back_prev,
⌜back_ = back⌝ ∗
⌜i_back = (i + length move)%nat⌝ ∗
⌜vs_front = []⌝ ∗
⌜vs_back = []⌝ ∗
⌜vs = reverse move⌝ ∗
⌜0 < length move⌝ ∗
state_at γ back_prev i ∗
back_model_2 back i_back (prefix_to_val i back_prev move) ∗
if strong then
⌜backs !! back = None⌝ ∗
back_prev ↦ₕ Header §Back 2
else
True.
#[local] Instance : CustomIpat "inv_status_unstable" :=
" ( %back{}_prev & {>;}-> & {>;}-> & {>;}{{lazy}%Hvs_front{};->} & {>;}{{lazy}%Hvs_back{};->} & {>;}-> & {>;}% & {>;}#Hstate_at_back{}_prev & Hback{} & { {strong} %Hbacks{}_lookup & #Hback{}_prev_header ; _ } ) ".
#[local] Definition inv_status strong γ backs i status vs_front i_back back vs_back vs : iProp Σ :=
match status with
| Stable empty ⇒
inv_status_stable γ i vs_front i_back back vs_back vs empty
| Unstable back_ move ⇒
inv_status_unstable strong γ backs i vs_front i_back back vs_back vs back_ move
end.
#[local] Definition inv_inner strong l γ : iProp Σ :=
∃ backs i status i_front vs_front i_back back vs_back vs,
l.[front] ↦ suffix_to_val i_front vs_front ∗
front_auth γ i_front ∗
l.[back] ↦ prefix_to_val i_back back vs_back ∗
([∗ map] back ↦ i ∈ backs, back_model_3 γ back i) ∗
model₂ γ vs ∗
state_auth γ backs i status ∗
⌜(i_front + length vs_front)%nat = S i⌝ ∗
inv_status strong γ backs i status vs_front i_back back vs_back vs.
#[local] Instance : CustomIpat "inv_inner" :=
" ( %backs{} & %i{} & %status{} & %i_front{} & %vs_front{} & %i_back{} & %back{} & %vs_back{} & %vs{} & Hl_front & {>;}Hfront_auth & Hl_back & Hbacks & Hmodel₂ & {>;}Hstate_auth & {>;}%Hfront{} & Hstatus ) ".
#[local] Definition inv' l γ : iProp Σ :=
inv γ.(metadata_inv) (inv_inner false l γ).
Definition mpmc_queue_2_inv t ι : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
⌜ι = γ.(metadata_inv)⌝ ∗
meta l nroot γ ∗
inv' l γ.
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & -> & -> & #Hmeta & #Hinv ) ".
Definition mpmc_queue_2_model t vs : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
model₁ γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Hmodel₁{_{}} ) ".
#[local] Instance state_auth_timeless γ backs i status :
Timeless (state_auth γ backs i status).
#[local] Instance state_at_timeless γ back i_back :
Timeless (state_at γ back i_back).
#[global] Instance mpmc_queue_2_model_timeless t vs :
Timeless (mpmc_queue_2_model t vs).
#[local] Instance state_at_persistent γ back i_back :
Persistent (state_at γ back i_back).
#[global] Instance mpmc_queue_2_inv_persistent t ι :
Persistent (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 state_alloc back :
⊢ |==>
∃ γ_state,
state_auth' γ_state ∅ 0 (Unstable back []).
#[local] Lemma state_auth_wf γ backs i status :
state_auth γ backs i status ⊢
⌜state_wf backs i⌝.
#[local] Lemma state_lb_get γ backs i status :
state_auth γ backs i status ⊢
state_lb γ backs i status.
#[local] Lemma state_at_get {γ backs i status} back i_back :
backs !! back = Some i_back →
state_auth γ backs i status ⊢
state_at γ back i_back.
#[local] Lemma state_lb_valid γ backs1 i1 status1 backs2 i2 status2 :
state_auth γ backs1 i1 status1 -∗
state_lb γ backs2 i2 status2 -∗
⌜backs2 ⊆ backs1⌝ ∗
⌜i2 ≤ i1⌝.
#[local] Lemma state_lb_valid_Unstable γ backs1 i1 status1 backs2 i2 back2 move2 :
state_auth γ backs1 i1 status1 -∗
state_lb γ backs2 i2 (Unstable back2 move2) -∗
⌜backs1 = backs2⌝ ∗
⌜i1 = i2⌝ ∗
⌜status1 = Unstable back2 move2⌝
∨ ⌜backs1 !! back2 = Some (i2 + length move2)%nat⌝ ∗
⌜i2 + length move2 ≤ i1⌝ ∗
state_at γ back2 (i2 + length move2).
#[local] Lemma state_lb_lookup {γ backs1 i1 status1 backs2 i2 status2} back i_back :
backs2 !! back = Some i_back →
state_auth γ backs1 i1 status1 -∗
state_lb γ backs2 i2 status2 -∗
⌜backs1 !! back = Some i_back⌝.
#[local] Lemma state_seen_valid γ backs i status back i_prev back_prev move :
state_auth γ backs i status -∗
state_seen γ back i_prev back_prev move -∗
⌜backs !! back_prev = Some i_prev⌝ ∗
( ⌜i = i_prev⌝ ∗
⌜status = Unstable back move⌝
∨ ⌜backs !! back = Some (i_prev + length move)%nat⌝ ∗
⌜i_prev + length move ≤ i⌝ ∗
state_at γ back (i_prev + length move)
).
#[local] Lemma state_at_valid γ backs i status back i_back :
state_auth γ backs i status -∗
state_at γ back i_back -∗
⌜backs !! back = Some i_back⌝ ∗
⌜i_back ≤ i⌝.
#[local] Lemma state_lb_stabilized γ backs1 i1 status1 backs2 i2 back2 move2 :
( status1 ≠ Unstable back2 move2
∨ i2 + length move2 ≤ i1 ∧
0 < length move2
) →
state_auth γ backs1 i1 status1 -∗
state_lb γ backs2 i2 (Unstable back2 move2) -∗
⌜backs1 !! back2 = Some (i2 + length move2)%nat⌝ ∗
state_at γ back2 (i2 + length move2).
#[local] Lemma state_lb_unstabilized γ backs1 i1 status1 backs2 i2 back2 move2 :
i1 < i2 + length move2 →
state_auth γ backs1 i1 status1 -∗
state_lb γ backs2 i2 (Unstable back2 move2) -∗
⌜backs1 = backs2⌝ ∗
⌜i1 = i2⌝ ∗
⌜status1 = Unstable back2 move2⌝.
#[local] Lemma state_stabilize γ backs i back move :
backs !! back = None →
state_auth γ backs i (Unstable back move) ⊢ |==>
state_auth γ (<[back := i + length move]> backs) (i + length move) (Stable Nonempty) ∗
state_lb γ (<[back := i + length move]> backs) (i + length move) (Stable Nonempty) ∗
state_at γ back (i + length move).
#[local] Lemma state_empty γ backs i :
state_auth γ backs i (Stable Nonempty) ⊢ |==>
state_auth γ backs i (Stable Empty).
#[local] Lemma state_destabilize {γ backs i} back move :
state_auth γ backs i (Stable Empty) ⊢ |==>
state_auth γ backs i (Unstable back move).
#[local] Lemma front_alloc :
⊢ |==>
∃ γ_front,
front_auth' γ_front 1.
#[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 :
front_auth γ i ⊢ |==>
front_auth γ (S i).
Opaque state_auth.
Opaque state_at.
#[local] Lemma inv_status_weaken γ backs i status vs_front i_back back vs_back vs :
inv_status true γ backs i status vs_front i_back back vs_back vs ⊢
inv_status false γ backs i status vs_front i_back back vs_back vs.
#[local] Lemma inv_status_Stable strong γ backs i status vs_front i_back back vs_back vs :
( strong = true ∧ is_Some (backs !! back)
∨ 0 < length vs_front
∨ 0 < length vs_back
) →
inv_status strong γ backs i status vs_front i_back back vs_back vs ⊢
∃ empty,
⌜status = Stable empty⌝ ∗
inv_status_stable γ i vs_front i_back back vs_back vs empty.
#[local] Lemma inv_inner_strengthen l γ :
inv_inner false l γ ⊢
inv_inner true l γ.
#[local] Lemma inv'_state_at {l γ} back i_back :
inv' l γ -∗
state_at γ back i_back ={⊤}=∗
back_model_1 back i_back.
Lemma mpmc_queue_2_model_exclusive t vs1 vs2 :
mpmc_queue_2_model t vs1 -∗
mpmc_queue_2_model t vs2 -∗
False.
#[local] Lemma mpmc_queue_2٠suffix_index𑁒spec (i : nat) vs :
{{{
True
}}}
mpmc_queue_2٠suffix_index (suffix_to_val i vs)
{{{
RET #i;
True
}}}.
#[local] Lemma mpmc_queue_2٠prefix_index𑁒spec (i : nat) back vs :
{{{
back ↦ₕ Header §Back 2 ∗
back.[index] ↦□ #i
}}}
mpmc_queue_2٠prefix_index (prefix_to_val i back vs)
{{{
RET #⁺(i + length vs);
True
}}}.
#[local] Lemma mpmc_queue_2٠rev₀𑁒spec i vs1 vs2 back :
0 < length vs1 →
{{{
back ↦ₕ Header §Back 2
}}}
mpmc_queue_2٠rev₀ (suffix_to_val (i + S (length vs2)) vs1) (prefix_to_val i back vs2)
{{{
RET suffix_to_val (S i) (reverse vs2 ++ vs1);
True
}}}.
#[local] Lemma mpmc_queue_2٠rev𑁒spec i back vs :
0 < length vs →
{{{
back ↦ₕ Header §Back 2
}}}
mpmc_queue_2٠rev (prefix_to_val i back vs)
{{{
RET suffix_to_val (S i) (reverse vs);
True
}}}.
Lemma mpmc_queue_2٠create𑁒spec ι :
{{{
True
}}}
mpmc_queue_2٠create ()
{{{
t
, RET t;
mpmc_queue_2_inv t ι ∗
mpmc_queue_2_model t []
}}}.
#[local] Lemma front𑁒spec_strong {l γ} i_front i_back :
{{{
inv' l γ ∗
match i_front with
| None ⇒
True
| Some i_front ⇒
front_lb γ i_front
end ∗
match i_back with
| None ⇒
True
| Some i_back ⇒
∃ back,
state_at γ back i_back
end
}}}
(#l).{front}
{{{
i_front' vs_front'
, RET suffix_to_val i_front' vs_front';
front_lb γ i_front' ∗
match i_front with
| None ⇒
True
| Some i_front ⇒
⌜i_front ≤ i_front'⌝
end ∗
match i_back with
| None ⇒
True
| Some i_back ⇒
∃ i',
⌜i_back ≤ i'⌝ ∗
⌜(i_front' + length vs_front')%nat = S i'⌝
end
}}}.
#[local] Lemma front𑁒spec l γ :
{{{
inv' l γ
}}}
(#l).{front}
{{{
i_front' vs_front'
, RET suffix_to_val i_front' vs_front';
front_lb γ i_front'
}}}.
#[local] Lemma move𑁒spec l γ backs back i move :
{{{
inv' l γ ∗
state_lb γ backs i (Unstable back move)
}}}
(#back).{move}
{{{
𝑚𝑜𝑣𝑒
, RET 𝑚𝑜𝑣𝑒;
⌜𝑚𝑜𝑣𝑒 = §Used%V⌝
∨ ∃ backs i back_prev move,
⌜𝑚𝑜𝑣𝑒 = prefix_to_val i back_prev move⌝ ∗
⌜0 < length move⌝ ∗
state_lb γ backs i (Unstable back move)
}}}.
Lemma mpmc_queue_2٠size𑁒spec t ι :
<<<
mpmc_queue_2_inv t ι
| ∀∀ vs,
mpmc_queue_2_model t vs
>>>
mpmc_queue_2٠size t @ ↑ι
<<<
mpmc_queue_2_model t vs
| RET #(length vs);
True
>>>.
Lemma mpmc_queue_2٠is_empty𑁒spec t ι :
<<<
mpmc_queue_2_inv t ι
| ∀∀ vs,
mpmc_queue_2_model t vs
>>>
mpmc_queue_2٠is_empty t @ ↑ι
<<<
mpmc_queue_2_model t vs
| RET #(bool_decide (vs = []%list));
True
>>>.
#[local] Lemma mpmc_queue_2٠finish𑁒spec {l γ} i_back back :
{{{
inv' l γ ∗
state_at γ back i_back
}}}
mpmc_queue_2٠finish #back
{{{
RET ();
True
}}}.
#[local] Lemma mpmc_queue_2٠help𑁒spec {l γ backs i back_prev back} move :
0 < length move →
{{{
inv' l γ ∗
state_lb γ backs i (Unstable back move) ∗
back_prev ↦ₕ Header §Back 2
}}}
mpmc_queue_2٠help #l #back #⁺(i + length move) (prefix_to_val i back_prev move)
{{{
RET ();
True
}}}.
#[local] Lemma mpmc_queue_2٠push𑁒spec_aux l γ v :
⊢ (
∀ back i ws (j : Z),
<<<
⌜j = ⁺(i + length ws)⌝ ∗
inv' l γ ∗
state_at γ back i
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠push_aux #l v #j (prefix_to_val i back ws) @ ↑γ.(metadata_inv)
<<<
model₁ γ (vs ++ [v])
| RET ();
True
>>>
) ∧ (
<<<
inv' l γ
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠push #l v @ ↑γ.(metadata_inv)
<<<
model₁ γ (vs ++ [v])
| RET ();
True
>>>
).
Lemma mpmc_queue_2٠push𑁒spec t v ι :
<<<
mpmc_queue_2_inv t ι
| ∀∀ vs,
mpmc_queue_2_model t vs
>>>
mpmc_queue_2٠push t v @ ↑ι
<<<
mpmc_queue_2_model t (vs ++ [v])
| RET ();
True
>>>.
#[local] Lemma mpmc_queue_2٠pop𑁒spec_aux l γ :
⊢ (
∀ i_front vs_front,
<<<
inv' l γ ∗
front_lb γ i_front
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠pop_1 #l (suffix_to_val i_front vs_front) @ ↑γ.(metadata_inv)
<<<
∃∃ o,
match o with
| None ⇒
model₁ γ vs
| Some v ⇒
∃ vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
end
| RET o;
True
>>>
) ∧ (
∀ (i_front : nat) backs back i back_prev move,
<<<
⌜i_front ≤ S i⌝ ∗
⌜1 < length move⌝ ∗
inv' l γ ∗
state_lb γ backs i (Unstable back move) ∗
back_prev ↦ₕ Header §Back 2
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠pop_2 #l ’Front[ #i_front ] #back (prefix_to_val i back_prev move) @ ↑γ.(metadata_inv)
<<<
∃∃ o,
match o with
| None ⇒
model₁ γ vs
| Some v ⇒
∃ vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
end
| RET o;
True
>>>
) ∧ (
∀ i_front,
<<<
inv' l γ
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠pop_3 #l ’Front[ #i_front ] @ ↑γ.(metadata_inv)
<<<
∃∃ o,
match o with
| None ⇒
model₁ γ vs
| Some v ⇒
∃ vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
end
| RET o;
True
>>>
) ∧ (
<<<
inv' l γ
| ∀∀ vs,
model₁ γ vs
>>>
mpmc_queue_2٠pop #l @ ↑γ.(metadata_inv)
<<<
∃∃ o,
match o with
| None ⇒
model₁ γ vs
| Some v ⇒
∃ vs',
⌜vs = v :: vs'⌝ ∗
model₁ γ vs'
end
| RET o;
True
>>>
).
Lemma mpmc_queue_2٠pop𑁒spec t ι :
<<<
mpmc_queue_2_inv t ι
| ∀∀ vs,
mpmc_queue_2_model t vs
>>>
mpmc_queue_2٠pop t @ ↑ι
<<<
∃∃ o,
match o with
| None ⇒
mpmc_queue_2_model t vs
| Some v ⇒
∃ vs',
⌜vs = v :: vs'⌝ ∗
mpmc_queue_2_model t vs'
end
| RET o;
True
>>>.
End mpmc_queue_2_G.
From zoo_saturn Require
mpmc_queue_2__opaque.
#[global] Opaque mpmc_queue_2_inv.
#[global] Opaque mpmc_queue_2_model.