Library zoo_saturn.mpmc_tqueue_2
From zoo Require Import
prelude.
From zoo.common Require Import
countable.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
optional.
From zoo_saturn Require Export
base
mpmc_tqueue_2__code.
From zoo_saturn Require Import
mpmc_tqueue_2__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types v : val.
Implicit Types vs : list val.
Class MpmcTqueue2G Σ `{zoo_G : !ZooG Σ} :=
{
}.
Definition mpmc_tqueue_2_Σ :=
#[
].
#[global] Instance subG_mpmc_tqueue_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG mpmc_tqueue_2_Σ Σ →
MpmcTqueue2G Σ.
Module base.
Section mpmc_tqueue_2_G.
Context `{mpmc_tqueue_2_G : MpmcTqueue2G Σ}.
Implicit Types t : location.
Record mpmc_tqueue_2_name :=
{
}.
Implicit Type γ : mpmc_tqueue_2_name.
#[global] Instance mpmc_tqueue_2_name_eq_dec : EqDecision mpmc_tqueue_2_name :=
ltac:(solve_decision).
#[global] Instance mpmc_tqueue_2_name_countable :
Countable mpmc_tqueue_2_name.
Definition mpmc_tqueue_2_inv t γ (ι : namespace) : iProp Σ.
Admitted.
Definition mpmc_tqueue_2_model γ vs : iProp Σ.
Admitted.
Definition mpmc_tqueue_2_full γ : iProp Σ.
Admitted.
Definition mpmc_tqueue_2_nonfull γ : iProp Σ.
Admitted.
Definition mpmc_tqueue_2_finished γ : iProp Σ.
Admitted.
#[global] Instance mpmc_tqueue_2_model_timeless γ vs :
Timeless (mpmc_tqueue_2_model γ vs).
#[global] Instance mpmc_tqueue_2_inv_persistent t γ ι :
Persistent (mpmc_tqueue_2_inv t γ ι).
#[global] Instance mpmc_tqueue_2_full_persistent γ :
Persistent (mpmc_tqueue_2_full γ).
#[global] Instance mpmc_tqueue_2_finished_persistent γ :
Persistent (mpmc_tqueue_2_finished γ).
Lemma mpmc_tqueue_2_model_exclusive γ vs1 vs2 :
mpmc_tqueue_2_model γ vs1 -∗
mpmc_tqueue_2_model γ vs2 -∗
False.
Lemma mpmc_tqueue_2_full_nonfull γ :
mpmc_tqueue_2_full γ -∗
mpmc_tqueue_2_nonfull γ -∗
False.
Lemma mpmc_tqueue_2_model_finished t γ ι vs E :
↑ι ⊆ E →
mpmc_tqueue_2_inv t γ ι -∗
mpmc_tqueue_2_model γ vs -∗
mpmc_tqueue_2_finished γ ={E}=∗
⌜vs = []⌝ ∗
mpmc_tqueue_2_model γ vs.
Lemma mpmc_tqueue_2٠create𑁒spec ι cap :
(0 ≤ cap)%Z →
{{{
True
}}}
mpmc_tqueue_2٠create #cap
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
mpmc_tqueue_2_inv t γ ι ∗
mpmc_tqueue_2_model γ []
}}}.
Lemma mpmc_tqueue_2٠make𑁒spec ι cap v :
(0 ≤ cap)%Z →
{{{
True
}}}
mpmc_tqueue_2٠make #cap v
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
mpmc_tqueue_2_inv t γ ι ∗
mpmc_tqueue_2_model γ [v]
}}}.
Lemma mpmc_tqueue_2٠is_empty𑁒spec t γ ι :
<<<
mpmc_tqueue_2_inv t γ ι
| ∀∀ vs,
mpmc_tqueue_2_model γ vs
>>>
mpmc_tqueue_2٠is_empty #t @ ↑ι
<<<
mpmc_tqueue_2_model γ vs
| b,
RET #b;
⌜if b then vs = [] else True⌝
>>>.
Lemma mpmc_tqueue_2٠push𑁒spec t γ ι v E Φ :
mpmc_tqueue_2_inv t γ ι -∗
▷ (
|={⊤ ∖ ↑ι, E}=>
∃ vs,
mpmc_tqueue_2_model γ vs ∗
∀ b,
( if b then
mpmc_tqueue_2_model γ (vs ++ [v]) ∗
mpmc_tqueue_2_nonfull γ
else
mpmc_tqueue_2_model γ vs ∗
mpmc_tqueue_2_full γ
) ={E}=∗
( if b then
mpmc_tqueue_2_nonfull γ
else
True
) ∗
|={E, ⊤ ∖ ↑ι}=>
Φ #b
) -∗
WP mpmc_tqueue_2٠push #t v {{ Φ }}.
Lemma mpmc_tqueue_2٠pop𑁒spec t γ ι :
<<<
mpmc_tqueue_2_inv t γ ι
| ∀∀ vs,
mpmc_tqueue_2_model γ vs
>>>
mpmc_tqueue_2٠pop #t @ ↑ι
<<<
∃∃ o vs',
mpmc_tqueue_2_model γ vs' ∗
⌜ match o with
| Something v ⇒
vs = v :: vs'
| Nothing ⇒
vs' = vs
| Anything ⇒
vs = [] ∧
vs' = vs
end
⌝
| RET o;
if o is Anything then
mpmc_tqueue_2_finished γ
else
True
>>>.
End mpmc_tqueue_2_G.
#[global] Opaque mpmc_tqueue_2_inv.
#[global] Opaque mpmc_tqueue_2_model.
#[global] Opaque mpmc_tqueue_2_full.
#[global] Opaque mpmc_tqueue_2_nonfull.
#[global] Opaque mpmc_tqueue_2_finished.
End base.
From zoo_saturn Require
mpmc_tqueue_2__opaque.
Section mpmc_tqueue_2_G.
Context `{mpmc_tqueue_2_G : MpmcTqueue2G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition mpmc_tqueue_2_inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpmc_tqueue_2_inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition mpmc_tqueue_2_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpmc_tqueue_2_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hmodel{_{}} ) ".
Definition mpmc_tqueue_2_full t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpmc_tqueue_2_full γ.
#[local] Instance : CustomIpat "full" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hfull{_{}} ) ".
Definition mpmc_tqueue_2_nonfull t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpmc_tqueue_2_nonfull γ.
#[local] Instance : CustomIpat "nonfull" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hnonfull{_{}} ) ".
Definition mpmc_tqueue_2_finished t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpmc_tqueue_2_finished γ.
#[local] Instance : CustomIpat "finished" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hfinished{_{}} ) ".
#[global] Instance mpmc_tqueue_2_model_timeless t vs :
Timeless (mpmc_tqueue_2_model t vs).
#[global] Instance mpmc_tqueue_2_inv_persistent t ι :
Persistent (mpmc_tqueue_2_inv t ι).
#[global] Instance mpmc_tqueue_2_full_persistent t :
Persistent (mpmc_tqueue_2_full t).
#[global] Instance mpmc_tqueue_2_finished_persistent t :
Persistent (mpmc_tqueue_2_finished t).
Lemma mpmc_tqueue_2_model_exclusive t vs1 vs2 :
mpmc_tqueue_2_model t vs1 -∗
mpmc_tqueue_2_model t vs2 -∗
False.
Lemma mpmc_tqueue_2_full_nonfull t :
mpmc_tqueue_2_full t -∗
mpmc_tqueue_2_nonfull t -∗
False.
Lemma mpmc_tqueue_2_model_finished t ι vs E :
↑ι ⊆ E →
mpmc_tqueue_2_inv t ι -∗
mpmc_tqueue_2_model t vs -∗
mpmc_tqueue_2_finished t ={E}=∗
⌜vs = []⌝ ∗
mpmc_tqueue_2_model t vs.
Lemma mpmc_tqueue_2٠create𑁒spec ι cap :
(0 ≤ cap)%Z →
{{{
True
}}}
mpmc_tqueue_2٠create #cap
{{{
t
, RET t;
mpmc_tqueue_2_inv t ι ∗
mpmc_tqueue_2_model t []
}}}.
Lemma mpmc_tqueue_2٠make𑁒spec ι cap v :
(0 ≤ cap)%Z →
{{{
True
}}}
mpmc_tqueue_2٠make #cap v
{{{
t
, RET t;
mpmc_tqueue_2_inv t ι ∗
mpmc_tqueue_2_model t [v]
}}}.
Lemma mpmc_tqueue_2٠is_empty𑁒spec t ι :
<<<
mpmc_tqueue_2_inv t ι
| ∀∀ vs,
mpmc_tqueue_2_model t vs
>>>
mpmc_tqueue_2٠is_empty t @ ↑ι
<<<
mpmc_tqueue_2_model t vs
| b,
RET #b;
⌜if b then vs = [] else True⌝
>>>.
Lemma mpmc_tqueue_2٠push𑁒spec t ι v E Φ :
mpmc_tqueue_2_inv t ι -∗
▷ (
|={⊤ ∖ ↑ι, E}=>
∃ vs,
mpmc_tqueue_2_model t vs ∗
∀ b,
( if b then
mpmc_tqueue_2_model t (vs ++ [v]) ∗
mpmc_tqueue_2_nonfull t
else
mpmc_tqueue_2_model t vs ∗
mpmc_tqueue_2_full t
) ={E}=∗
( if b then
mpmc_tqueue_2_nonfull t
else
True
) ∗
|={E, ⊤ ∖ ↑ι}=>
Φ #b
) -∗
WP mpmc_tqueue_2٠push t v {{ Φ }}.
Lemma mpmc_tqueue_2٠pop𑁒spec t ι :
<<<
mpmc_tqueue_2_inv t ι
| ∀∀ vs,
mpmc_tqueue_2_model t vs
>>>
mpmc_tqueue_2٠pop t @ ↑ι
<<<
∃∃ o vs',
mpmc_tqueue_2_model t vs' ∗
⌜ match o with
| Something v ⇒
vs = v :: vs'
| Nothing ⇒
vs' = vs
| Anything ⇒
vs = [] ∧
vs' = vs
end
⌝
| RET o;
if o is Anything then
mpmc_tqueue_2_finished t
else
True
>>>.
End mpmc_tqueue_2_G.
#[global] Opaque mpmc_tqueue_2_inv.
#[global] Opaque mpmc_tqueue_2_model.
#[global] Opaque mpmc_tqueue_2_full.
#[global] Opaque mpmc_tqueue_2_nonfull.
#[global] Opaque mpmc_tqueue_2_finished.
prelude.
From zoo.common Require Import
countable.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
optional.
From zoo_saturn Require Export
base
mpmc_tqueue_2__code.
From zoo_saturn Require Import
mpmc_tqueue_2__types.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types v : val.
Implicit Types vs : list val.
Class MpmcTqueue2G Σ `{zoo_G : !ZooG Σ} :=
{
}.
Definition mpmc_tqueue_2_Σ :=
#[
].
#[global] Instance subG_mpmc_tqueue_2_Σ Σ `{zoo_G : !ZooG Σ} :
subG mpmc_tqueue_2_Σ Σ →
MpmcTqueue2G Σ.
Module base.
Section mpmc_tqueue_2_G.
Context `{mpmc_tqueue_2_G : MpmcTqueue2G Σ}.
Implicit Types t : location.
Record mpmc_tqueue_2_name :=
{
}.
Implicit Type γ : mpmc_tqueue_2_name.
#[global] Instance mpmc_tqueue_2_name_eq_dec : EqDecision mpmc_tqueue_2_name :=
ltac:(solve_decision).
#[global] Instance mpmc_tqueue_2_name_countable :
Countable mpmc_tqueue_2_name.
Definition mpmc_tqueue_2_inv t γ (ι : namespace) : iProp Σ.
Admitted.
Definition mpmc_tqueue_2_model γ vs : iProp Σ.
Admitted.
Definition mpmc_tqueue_2_full γ : iProp Σ.
Admitted.
Definition mpmc_tqueue_2_nonfull γ : iProp Σ.
Admitted.
Definition mpmc_tqueue_2_finished γ : iProp Σ.
Admitted.
#[global] Instance mpmc_tqueue_2_model_timeless γ vs :
Timeless (mpmc_tqueue_2_model γ vs).
#[global] Instance mpmc_tqueue_2_inv_persistent t γ ι :
Persistent (mpmc_tqueue_2_inv t γ ι).
#[global] Instance mpmc_tqueue_2_full_persistent γ :
Persistent (mpmc_tqueue_2_full γ).
#[global] Instance mpmc_tqueue_2_finished_persistent γ :
Persistent (mpmc_tqueue_2_finished γ).
Lemma mpmc_tqueue_2_model_exclusive γ vs1 vs2 :
mpmc_tqueue_2_model γ vs1 -∗
mpmc_tqueue_2_model γ vs2 -∗
False.
Lemma mpmc_tqueue_2_full_nonfull γ :
mpmc_tqueue_2_full γ -∗
mpmc_tqueue_2_nonfull γ -∗
False.
Lemma mpmc_tqueue_2_model_finished t γ ι vs E :
↑ι ⊆ E →
mpmc_tqueue_2_inv t γ ι -∗
mpmc_tqueue_2_model γ vs -∗
mpmc_tqueue_2_finished γ ={E}=∗
⌜vs = []⌝ ∗
mpmc_tqueue_2_model γ vs.
Lemma mpmc_tqueue_2٠create𑁒spec ι cap :
(0 ≤ cap)%Z →
{{{
True
}}}
mpmc_tqueue_2٠create #cap
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
mpmc_tqueue_2_inv t γ ι ∗
mpmc_tqueue_2_model γ []
}}}.
Lemma mpmc_tqueue_2٠make𑁒spec ι cap v :
(0 ≤ cap)%Z →
{{{
True
}}}
mpmc_tqueue_2٠make #cap v
{{{
t γ
, RET #t;
meta_token t ⊤ ∗
mpmc_tqueue_2_inv t γ ι ∗
mpmc_tqueue_2_model γ [v]
}}}.
Lemma mpmc_tqueue_2٠is_empty𑁒spec t γ ι :
<<<
mpmc_tqueue_2_inv t γ ι
| ∀∀ vs,
mpmc_tqueue_2_model γ vs
>>>
mpmc_tqueue_2٠is_empty #t @ ↑ι
<<<
mpmc_tqueue_2_model γ vs
| b,
RET #b;
⌜if b then vs = [] else True⌝
>>>.
Lemma mpmc_tqueue_2٠push𑁒spec t γ ι v E Φ :
mpmc_tqueue_2_inv t γ ι -∗
▷ (
|={⊤ ∖ ↑ι, E}=>
∃ vs,
mpmc_tqueue_2_model γ vs ∗
∀ b,
( if b then
mpmc_tqueue_2_model γ (vs ++ [v]) ∗
mpmc_tqueue_2_nonfull γ
else
mpmc_tqueue_2_model γ vs ∗
mpmc_tqueue_2_full γ
) ={E}=∗
( if b then
mpmc_tqueue_2_nonfull γ
else
True
) ∗
|={E, ⊤ ∖ ↑ι}=>
Φ #b
) -∗
WP mpmc_tqueue_2٠push #t v {{ Φ }}.
Lemma mpmc_tqueue_2٠pop𑁒spec t γ ι :
<<<
mpmc_tqueue_2_inv t γ ι
| ∀∀ vs,
mpmc_tqueue_2_model γ vs
>>>
mpmc_tqueue_2٠pop #t @ ↑ι
<<<
∃∃ o vs',
mpmc_tqueue_2_model γ vs' ∗
⌜ match o with
| Something v ⇒
vs = v :: vs'
| Nothing ⇒
vs' = vs
| Anything ⇒
vs = [] ∧
vs' = vs
end
⌝
| RET o;
if o is Anything then
mpmc_tqueue_2_finished γ
else
True
>>>.
End mpmc_tqueue_2_G.
#[global] Opaque mpmc_tqueue_2_inv.
#[global] Opaque mpmc_tqueue_2_model.
#[global] Opaque mpmc_tqueue_2_full.
#[global] Opaque mpmc_tqueue_2_nonfull.
#[global] Opaque mpmc_tqueue_2_finished.
End base.
From zoo_saturn Require
mpmc_tqueue_2__opaque.
Section mpmc_tqueue_2_G.
Context `{mpmc_tqueue_2_G : MpmcTqueue2G Σ}.
Implicit Types 𝑡 : location.
Implicit Types t : val.
Definition mpmc_tqueue_2_inv t ι : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpmc_tqueue_2_inv 𝑡 γ ι.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & #Hmeta{_{}} & Hinv{_{}} ) ".
Definition mpmc_tqueue_2_model t vs : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpmc_tqueue_2_model γ vs.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hmodel{_{}} ) ".
Definition mpmc_tqueue_2_full t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpmc_tqueue_2_full γ.
#[local] Instance : CustomIpat "full" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hfull{_{}} ) ".
Definition mpmc_tqueue_2_nonfull t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpmc_tqueue_2_nonfull γ.
#[local] Instance : CustomIpat "nonfull" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hnonfull{_{}} ) ".
Definition mpmc_tqueue_2_finished t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
meta 𝑡 nroot γ ∗
base.mpmc_tqueue_2_finished γ.
#[local] Instance : CustomIpat "finished" :=
" ( %𝑡{} & %γ{} & {%Heq{};->} & Hmeta{_{}} & Hfinished{_{}} ) ".
#[global] Instance mpmc_tqueue_2_model_timeless t vs :
Timeless (mpmc_tqueue_2_model t vs).
#[global] Instance mpmc_tqueue_2_inv_persistent t ι :
Persistent (mpmc_tqueue_2_inv t ι).
#[global] Instance mpmc_tqueue_2_full_persistent t :
Persistent (mpmc_tqueue_2_full t).
#[global] Instance mpmc_tqueue_2_finished_persistent t :
Persistent (mpmc_tqueue_2_finished t).
Lemma mpmc_tqueue_2_model_exclusive t vs1 vs2 :
mpmc_tqueue_2_model t vs1 -∗
mpmc_tqueue_2_model t vs2 -∗
False.
Lemma mpmc_tqueue_2_full_nonfull t :
mpmc_tqueue_2_full t -∗
mpmc_tqueue_2_nonfull t -∗
False.
Lemma mpmc_tqueue_2_model_finished t ι vs E :
↑ι ⊆ E →
mpmc_tqueue_2_inv t ι -∗
mpmc_tqueue_2_model t vs -∗
mpmc_tqueue_2_finished t ={E}=∗
⌜vs = []⌝ ∗
mpmc_tqueue_2_model t vs.
Lemma mpmc_tqueue_2٠create𑁒spec ι cap :
(0 ≤ cap)%Z →
{{{
True
}}}
mpmc_tqueue_2٠create #cap
{{{
t
, RET t;
mpmc_tqueue_2_inv t ι ∗
mpmc_tqueue_2_model t []
}}}.
Lemma mpmc_tqueue_2٠make𑁒spec ι cap v :
(0 ≤ cap)%Z →
{{{
True
}}}
mpmc_tqueue_2٠make #cap v
{{{
t
, RET t;
mpmc_tqueue_2_inv t ι ∗
mpmc_tqueue_2_model t [v]
}}}.
Lemma mpmc_tqueue_2٠is_empty𑁒spec t ι :
<<<
mpmc_tqueue_2_inv t ι
| ∀∀ vs,
mpmc_tqueue_2_model t vs
>>>
mpmc_tqueue_2٠is_empty t @ ↑ι
<<<
mpmc_tqueue_2_model t vs
| b,
RET #b;
⌜if b then vs = [] else True⌝
>>>.
Lemma mpmc_tqueue_2٠push𑁒spec t ι v E Φ :
mpmc_tqueue_2_inv t ι -∗
▷ (
|={⊤ ∖ ↑ι, E}=>
∃ vs,
mpmc_tqueue_2_model t vs ∗
∀ b,
( if b then
mpmc_tqueue_2_model t (vs ++ [v]) ∗
mpmc_tqueue_2_nonfull t
else
mpmc_tqueue_2_model t vs ∗
mpmc_tqueue_2_full t
) ={E}=∗
( if b then
mpmc_tqueue_2_nonfull t
else
True
) ∗
|={E, ⊤ ∖ ↑ι}=>
Φ #b
) -∗
WP mpmc_tqueue_2٠push t v {{ Φ }}.
Lemma mpmc_tqueue_2٠pop𑁒spec t ι :
<<<
mpmc_tqueue_2_inv t ι
| ∀∀ vs,
mpmc_tqueue_2_model t vs
>>>
mpmc_tqueue_2٠pop t @ ↑ι
<<<
∃∃ o vs',
mpmc_tqueue_2_model t vs' ∗
⌜ match o with
| Something v ⇒
vs = v :: vs'
| Nothing ⇒
vs' = vs
| Anything ⇒
vs = [] ∧
vs' = vs
end
⌝
| RET o;
if o is Anything then
mpmc_tqueue_2_finished t
else
True
>>>.
End mpmc_tqueue_2_G.
#[global] Opaque mpmc_tqueue_2_inv.
#[global] Opaque mpmc_tqueue_2_model.
#[global] Opaque mpmc_tqueue_2_full.
#[global] Opaque mpmc_tqueue_2_nonfull.
#[global] Opaque mpmc_tqueue_2_finished.