Library zoo_parabs.vertex
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.gmultiset.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.auth_gmultiset.
Require Import zoo.iris.base_logic.lib.mono_gmultiset.
Require Import zoo.iris.base_logic.lib.subprops.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_parabs.base.
Require Export zoo_parabs.vertex__code.
Require Import zoo_parabs.vertex__types.
Require Import zoo.options.
Implicit Type b finished : bool.
Implicit Type preds : nat.
Implicit Type succ : location.
Implicit Type task ctx : val.
Implicit Type own : ownership.
Variant state :=
| Init
| Released
| Ready
| Finished.
Implicit Type state : state.
#[local] Instance stateｰinhabited : Inhabited state :=
populate Init.
#[local] Instance stateｰeq_dec : EqDecision state :=
ltac:(solve_decision).
Record vertex۰name :=
{ vertex۰name۰successors : val
; vertex۰name۰state : gname
; vertex۰name۰iteration : gname
; vertex۰name۰predecessors : gname
; vertex۰name۰output : gname
}.
Implicit Type γ δ π : vertex۰name.
#[local] Instance vertex۰nameｰeq_dec : EqDecision vertex۰name :=
ltac:(solve_decision).
#[local] Instance vertex۰nameｰcountable :
Countable vertex۰name.
Implicit Type Δ Π : gmultiset vertex۰name.
Definition vertex۰iteration :=
gname.
Implicit Type iter : vertex۰iteration.
Class VertexG Σ `{pool۰G : PoolG Σ} :=
{ #[local] vertex۰G۰stack۰G :: StackMpmc2G Σ
; #[local] vertex۰G۰state۰G :: TwinsG Σ (leibnizO state)
; #[local] vertex۰G۰iteration۰G :: TwinsG Σ (leibnizO vertex۰iteration)
; #[local] vertex۰G۰dependencies۰G :: MonoGmultisetG Σ vertex۰name
; #[local] vertex۰G۰predecessors۰G :: AuthGmultisetG Σ vertex۰name
; #[local] vertex۰G۰output۰G :: SubpropsG Σ
}.
Definition vertex۰Σ :=
#[stack_mpmc_2۰Σ
; twins۰Σ (leibnizO state)
; twins۰Σ (leibnizO vertex۰iteration)
; mono_gmultiset۰Σ vertex۰name
; auth_gmultiset۰Σ vertex۰name
; subprops۰Σ
].
#[global] Instance subGｰvertex۰Σ Σ `{pool۰G : PoolG Σ}:
subG vertex۰Σ Σ →
VertexG Σ.
Module base.
Section vertex۰G.
Context `{vertex۰G : VertexG Σ}.
Implicit Type t : location.
Implicit Type P Q R : iProp Σ.
#[local] Definition state₁' γ_state own state :=
twins۰twin₁ (twins۰G := vertex۰G۰state۰G) γ_state own state.
#[local] Definition state₁ γ :=
state₁' γ.(vertex۰name۰state).
#[local] Definition state₂' γ_state state :=
twins۰twin₂ (twins۰G := vertex۰G۰state۰G) γ_state state.
#[local] Definition state₂ γ :=
state₂' γ.(vertex۰name۰state).
#[local] Definition iteration₁' γ_iteration iter :=
twins۰twin₁ γ_iteration (DfracOwn 1) iter.
#[local] Definition iteration₁ γ :=
iteration₁' γ.(vertex۰name۰iteration).
#[local] Definition iteration₂' γ_iteration iter :=
twins۰twin₂ γ_iteration iter.
#[local] Definition iteration₂ γ :=
iteration₂' γ.(vertex۰name۰iteration).
#[local] Definition dependencies۰auth iter own :=
mono_gmultiset۰auth iter own.
#[local] Definition dependencies۰elem iter :=
mono_gmultiset۰elem iter.
#[local] Definition predecessors۰auth' γ_predecessors Π :=
auth_gmultiset۰auth γ_predecessors (DfracOwn 1) Π.
#[local] Definition predecessors۰auth γ Π :=
predecessors۰auth' γ.(vertex۰name۰predecessors) Π.
#[local] Definition predecessors۰elem γ π :=
auth_gmultiset۰frag γ.(vertex۰name۰predecessors) {[+π+]}.
#[local] Definition output۰auth' γ_output :=
subprops۰auth γ_output.
#[local] Definition output۰auth γ :=
subprops۰auth γ.(vertex۰name۰output).
#[local] Definition output۰frag' γ_output :=
subprops۰frag γ_output.
#[local] Definition output۰frag γ :=
output۰frag' γ.(vertex۰name۰output).
#[local] Definition model' t γ task state iter : iProp Σ :=
t.[task] ↦ task ∗
state₁ γ Own state ∗
iteration₁ γ iter.
#[local] Instance : CustomIpat "model'" :=
" ( Ht{which;}_task{_{}} & Hstate{which;}₁{_{}} & Hiteration{which;}₁{_{}} ) ".
Definition vertex۰model t γ task iter : iProp Σ :=
model' t γ task Init iter.
#[local] Instance : CustomIpat "model" :=
" (:model') ".
Definition vertex۰ready iter : iProp Σ :=
∃ Δ,
dependencies۰auth iter Discard Δ ∗
[∗ mset] δ ∈ Δ, state₁ δ Discard Finished.
#[local] Instance : CustomIpat "ready" :=
" ( %Δ{} & #Hdependencies{which;}_auth{_{}} & #HΔ{} ) ".
Definition vertex۰finished γ :=
state₁ γ Discard Finished.
#[local] Instance : CustomIpat "finished" :=
" #Hstate{which;}₁{_{}} ".
Definition vertex۰wp۰body t γ P R wp task iter : iProp Σ :=
∀ pool ctx scope iter',
pool۰context pool ctx scope -∗
vertex۰ready iter -∗
vertex۰model t γ task iter' -∗
WP task ctx {{ res,
∃ b task,
⌜res = #b⌝ ∗
pool۰context pool ctx scope ∗
vertex۰model t γ task iter' ∗
if b then
▷ P ∗
▷ □ R
else
▷ wp task iter'
}}.
#[local] Definition vertex۰wp۰pre
: location → vertex۰name → iProp Σ → iProp Σ →
(val -d> vertex۰iteration -d> iProp Σ) →
val -d> vertex۰iteration -d> iProp Σ
:=
vertex۰wp۰body.
#[local] Instance vertex۰wp۰preｰcontractive t γ P R :
Contractive (vertex۰wp۰pre t γ P R).
#[local] Instance vertex۰wp۰preｰne t γ P R :
NonExpansive (vertex۰wp۰pre t γ P R).
Definition vertex۰wp t γ P R : val → vertex۰iteration → iProp Σ :=
fixpoint (vertex۰wp۰pre t γ P R).
Lemma vertex۰wpｰunfold t γ P R task iter :
vertex۰wp t γ P R task iter ⊣⊢
vertex۰wp۰body t γ P R (vertex۰wp t γ P R) task iter.
#[global] Instance vertex۰wpｰne n :
Proper (
(=) ==>
(=) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) vertex۰wp.
#[local] Definition inv۰state۰init preds iter Π : iProp Σ :=
∃ Δ,
dependencies۰auth iter Own (Δ ⊎ Π) ∗
⌜preds = ˖(size Π)⌝ ∗
[∗ mset] δ ∈ Δ, vertex۰finished δ.
#[local] Instance : CustomIpat "inv۰state۰init" :=
" ( %Δ & {>;}Hdependencies{which;}_auth & {>;}-> & {>;}HΔ ) ".
#[local] Definition inv۰state۰released t γ P R preds iter Π : iProp Σ :=
∃ task Δ,
model' t γ task Released iter ∗
dependencies۰auth iter Discard (Δ ⊎ Π) ∗
⌜preds = size Π⌝ ∗
([∗ mset] δ ∈ Δ, vertex۰finished δ) ∗
vertex۰wp t γ P R task iter.
#[local] Instance : CustomIpat "inv۰state۰released" :=
" ( %task & %Δ & (:model') & {>;}Hdependencies{which;}_auth & {>;}-> & {>;}HΔ & Htask ) ".
#[local] Definition inv۰state۰ready Π : iProp Σ :=
⌜Π = ∅⌝.
#[local] Instance : CustomIpat "inv۰state۰ready" :=
" {>;}-> ".
#[local] Definition inv۰state۰finished γ R preds Π : iProp Σ :=
vertex۰finished γ ∗
⌜preds = ˖(size Π)⌝ ∗
□ R.
#[local] Instance : CustomIpat "inv۰state۰finished" :=
" ( {>;}#Hstate{which;}₁ & {>;}-> & #HR{which;} ) ".
#[local] Definition inv۰state t γ P R state preds iter Π : iProp Σ :=
match state with
| Init ⇒
inv۰state۰init preds iter Π
| Released ⇒
inv۰state۰released t γ P R preds iter Π
| Ready ⇒
inv۰state۰ready Π
| Finished ⇒
inv۰state۰finished γ R preds Π
end.
#[local] Definition inv۰successor (inv : location → vertex۰name → iProp Σ → iProp Σ → iProp Σ) γ succ : iProp Σ :=
∃ γ_succ P_succ R_succ,
inv succ γ_succ P_succ R_succ ∗
predecessors۰elem γ_succ γ.
#[local] Instance : CustomIpat "inv۰successor" :=
" ( %γ_succ & %P_succ & %R_succ & #Hinv_succ & Hpredecessors_elem ) ".
#[local] Definition inv۰successors inv γ finished :=
if finished then (
stack_mpmc_2۰model γ.(vertex۰name۰successors) None
) else (
∃ succs,
stack_mpmc_2۰model γ.(vertex۰name۰successors) (Some $ #*@{location} succs) ∗
[∗ list] succ ∈ succs, inv۰successor inv γ succ
)%I.
#[local] Instance : CustomIpat "inv۰successors۰finished" :=
" >Hsuccessors{which;}_model ".
#[local] Instance : CustomIpat "inv۰successors" :=
" ( %succs & >Hsuccessors{which;}_model & Hsuccs ) ".
#[local] Definition inv۰inner inv t γ P R : iProp Σ :=
∃ preds state iter Π,
t.[preds] ↦ #preds ∗
state₂ γ state ∗
iteration₂ γ iter ∗
predecessors۰auth γ Π ∗
output۰auth γ P (bool_decide (state = Finished)) ∗
inv۰state t γ P R state preds iter Π ∗
inv۰successors inv γ (bool_decide (state = Finished)).
#[local] Instance : CustomIpat "inv۰inner" :=
" ( %preds{} & %state{} & %iter{} & %Π & Ht{which;}_preds & >Hstate{which;}₂ & >Hiteration{which;}₂ & Hpredecessors{which;}_auth & Houtput{which;}_auth & Hinv_state{which;} & Hinv_successors{which;} ) ".
#[local] Definition inv۰pre
: (location -d> vertex۰name -d> iProp Σ -d> iProp Σ -d> iProp Σ) →
location -d> vertex۰name -d> iProp Σ -d> iProp Σ -d> iProp Σ
:=
λ inv t γ P R, (
t.[succs] ↦□ γ.(vertex۰name۰successors) ∗
stack_mpmc_2۰inv γ.(vertex۰name۰successors) (nroot.@"successors") ∗
invariants.inv (nroot.@"inv") (inv۰inner inv t γ P R)
)%I.
#[local] Instance : CustomIpat "inv۰pre" :=
" ( #Ht{}_succs & #Hsuccessors{}_inv & #Hinv{_{}} ) ".
#[local] Instance inv۰preｰcontractive :
Contractive inv۰pre.
Definition vertex۰inv : location → vertex۰name → iProp Σ → iProp Σ → iProp Σ :=
fixpoint inv۰pre.
#[local] Lemma vertex۰invｰunfold t γ P R :
vertex۰inv t γ P R ⊣⊢
inv۰pre vertex۰inv t γ P R.
#[local] Instance vertex۰invｰcontractive t γ n :
Proper (
dist_later n ==>
dist_later n ==>
(≡{n}≡)
) (vertex۰inv t γ).
#[global] Instance vertex۰invｰne t γ n :
Proper (
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) (vertex۰inv t γ).
#[global] Instance vertex۰invｰproper t γ :
Proper (
(≡) ==>
(≡) ==>
(≡)
) (vertex۰inv t γ).
Definition vertex۰output γ Q :=
output۰frag γ Q.
#[local] Instance : CustomIpat "output" :=
" Houtput{which;}_frag{_{}} ".
#[global] Instance vertex۰outputｰcontractive γ :
Contractive (vertex۰output γ).
#[global] Instance vertex۰outputｰproper γ :
Proper ((≡) ==> (≡)) (vertex۰output γ).
Definition vertex۰predecessor γ iter :=
dependencies۰elem iter γ.
#[local] Instance : CustomIpat "predecessor" :=
" #Hdependencies{which;}_elem{_{}} ".
#[global] Instance vertex۰modelｰtimeless t γ task iter :
Timeless (vertex۰model t γ task iter).
#[global] Instance vertex۰readyｰtimeless iter :
Timeless (vertex۰ready iter).
#[global] Instance vertex۰finishedｰtimeless γ :
Timeless (vertex۰finished γ).
#[global] Instance vertex۰predecessorｰtimeless γ iter :
Timeless (vertex۰predecessor γ iter).
#[global] Instance vertex۰invｰpersistent t γ P R :
Persistent (vertex۰inv t γ P R).
#[global] Instance vertex۰readyｰpersistent iter :
Persistent (vertex۰ready iter).
#[global] Instance vertex۰finishedｰpersistent γ :
Persistent (vertex۰finished γ).
#[global] Instance vertex۰predecessorｰpersistent γ iter :
Persistent (vertex۰predecessor γ iter).
#[local] Lemma stateｰalloc :
⊢ |==>
∃ γ_state,
state₁' γ_state Own Init ∗
state₂' γ_state Init.
#[local] Lemma stateｰagree γ own1 state1 state2 :
state₁ γ own1 state1 -∗
state₂ γ state2 -∗
⌜state1 = state2⌝.
#[local] Lemma state₁ｰexclusive γ state1 own2 state2 :
state₁ γ Own state1 -∗
state₁ γ own2 state2 -∗
False.
#[local] Lemma stateｰupdate {γ state1 state2} state :
state₁ γ Own state1 -∗
state₂ γ state2 ==∗
state₁ γ Own state ∗
state₂ γ state.
#[local] Lemma state₁ｰdiscard γ state :
state₁ γ Own state ⊢ |==>
state₁ γ Discard state.
#[local] Lemma iterationｰalloc iter :
⊢ |==>
∃ γ_iteration,
iteration₁' γ_iteration iter ∗
iteration₂' γ_iteration iter.
#[local] Lemma iterationｰagree γ iteration1 iteration2 :
iteration₁ γ iteration1 -∗
iteration₂ γ iteration2 -∗
⌜iteration1 = iteration2⌝.
#[local] Lemma iteration₁ｰexclusive γ iteration1 iteration2 :
iteration₁ γ iteration1 -∗
iteration₁ γ iteration2 -∗
False.
#[local] Lemma iterationｰupdate {γ iteration1 iteration2} iteration :
iteration₁ γ iteration1 -∗
iteration₂ γ iteration2 ==∗
iteration₁ γ iteration ∗
iteration₂ γ iteration.
#[local] Lemma dependenciesｰalloc :
⊢ |==>
∃ iter,
dependencies۰auth iter Own ∅.
#[local] Lemma dependenciesｰadd {iter Δ} δ :
dependencies۰auth iter Own Δ ⊢ |==>
dependencies۰auth iter Own ({[+δ+]} ⊎ Δ) ∗
dependencies۰elem iter δ.
#[local] Lemma dependenciesｰelem_of iter own Δ δ :
dependencies۰auth iter own Δ -∗
dependencies۰elem iter δ -∗
⌜δ ∈ Δ⌝.
#[local] Lemma dependenciesｰdiscard iter Δ :
dependencies۰auth iter Own Δ ⊢ |==>
dependencies۰auth iter Discard Δ.
#[local] Lemma predecessorsｰalloc :
⊢ |==>
∃ γ_predecessors,
predecessors۰auth' γ_predecessors ∅.
#[local] Lemma predecessorsｰelem_of γ Π π :
predecessors۰auth γ Π -∗
predecessors۰elem γ π -∗
⌜π ∈ Π⌝.
#[local] Lemma predecessorsｰadd {γ Π} π :
predecessors۰auth γ Π ⊢ |==>
predecessors۰auth γ ({[+π+]} ⊎ Π) ∗
predecessors۰elem γ π.
#[local] Lemma predecessorsｰremove γ Π π :
predecessors۰auth γ Π -∗
predecessors۰elem γ π ==∗
predecessors۰auth γ (Π ∖ {[+π+]}).
#[local] Lemma outputｰalloc P :
⊢ |==>
∃ γ_output,
output۰auth' γ_output P false ∗
output۰frag' γ_output P.
#[local] Lemma outputｰwand {γ P finished Q1} Q2 E :
▷ output۰auth γ P finished -∗
output۰frag γ Q1 -∗
(Q1 -∗ Q2) ={E}=∗
▷ output۰auth γ P finished ∗
output۰frag γ Q2.
#[local] Lemma outputｰdivide {γ P finished} Qs E :
▷ output۰auth γ P finished -∗
output۰frag γ ([∗ list] Q ∈ Qs, Q) ={E}=∗
▷ output۰auth γ P finished ∗
[∗ list] Q ∈ Qs, output۰frag γ Q.
#[local] Lemma outputｰproduce γ P :
▷ output۰auth γ P false -∗
P -∗
▷ output۰auth γ P true.
#[local] Lemma outputｰconsume γ P Q E :
▷ output۰auth γ P true -∗
output۰frag γ Q ={E}=∗
▷ output۰auth γ P true ∗
▷^2 Q.
Lemma vertex۰modelｰexclusive t γ task1 iter1 task2 iter2 :
vertex۰model t γ task1 iter1 -∗
vertex۰model t γ task2 iter2 -∗
False.
Lemma vertex۰modelｰfinished t γ task iter :
vertex۰model t γ task iter -∗
vertex۰finished γ -∗
False.
Lemma vertex۰outputｰwand {t γ P R Q1} Q2 :
vertex۰inv t γ P R -∗
vertex۰output γ Q1 -∗
(Q1 -∗ Q2) ={⊤}=∗
vertex۰output γ Q2.
Lemma vertex۰outputｰdivide {t γ P R} Qs :
vertex۰inv t γ P R -∗
vertex۰output γ ([∗ list] Q ∈ Qs, Q) ={⊤}=∗
[∗ list] Q ∈ Qs, vertex۰output γ Q.
Lemma vertexｰpredecessorｰfinished γ iter :
vertex۰predecessor γ iter -∗
vertex۰ready iter -∗
vertex۰finished γ.
Lemma vertexｰinvｰfinished t γ P R :
vertex۰inv t γ P R -∗
vertex۰finished γ ={⊤}=∗
▷ □ R.
Lemma vertexｰinvｰfinishedｰoutput t γ P R Q :
vertex۰inv t γ P R -∗
vertex۰finished γ -∗
vertex۰output γ Q ={⊤}=∗
▷^2 Q.
Lemma vertex٠createｰspec P R (task : option val) :
{{{
True
}}}
vertex٠create task
{{{
t γ iter
, RET #t;
meta_token t ⊤ ∗
vertex۰inv t γ P R ∗
vertex۰model t γ (default (𝗳𝘂𝗻 ⎽ → true)%V task) iter ∗
vertex۰output γ P
}}}.
Lemma vertex٠create'ｰspec P R task :
{{{
True
}}}
vertex٠create' task
{{{
t γ iter
, RET #t;
meta_token t ⊤ ∗
vertex۰inv t γ P R ∗
vertex۰model t γ (𝗳𝘂𝗻 "ctx" → task "ctx" ⍮ true) iter ∗
vertex۰output γ P
}}}.
Lemma vertex٠taskｰspec t γ task iter :
{{{
vertex۰model t γ task iter
}}}
vertex٠task #t
{{{
RET task;
vertex۰model t γ task iter
}}}.
Lemma vertex٠set_taskｰspec t γ task1 iter task2 :
{{{
vertex۰model t γ task1 iter
}}}
vertex٠set_task #t task2
{{{
RET ();
vertex۰model t γ task2 iter
}}}.
Lemma vertex٠precedeｰspec t1 γ1 P1 R1 t2 γ2 P2 R2 task iter :
{{{
vertex۰inv t1 γ1 P1 R1 ∗
vertex۰inv t2 γ2 P2 R2 ∗
vertex۰model t2 γ2 task iter
}}}
vertex٠precede #t1 #t2
{{{
RET ();
vertex۰model t2 γ2 task iter ∗
vertex۰predecessor γ1 iter
}}}.
#[local] Lemma vertex٠release_runｰspec :
⊢ (
∀ pool ctx scope t γ P R task iter,
{{{
pool۰context pool ctx scope ∗
vertex۰inv t γ P R ∗
vertex۰model t γ task iter ∗
vertex۰wp t γ P R task iter
}}}
vertex٠release ctx #t
{{{
RET ();
pool۰context pool ctx scope
}}}
) ∧ (
∀ pool ctx scope t γ P R π,
{{{
pool۰context pool ctx scope ∗
vertex۰inv t γ P R ∗
predecessors۰elem γ π ∗
vertex۰finished π
}}}
vertex٠release ctx #t
{{{
RET ();
pool۰context pool ctx scope
}}}
) ∧ (
∀ pool ctx scope t γ iter P R task,
{{{
pool۰context pool ctx scope ∗
vertex۰inv t γ P R ∗
vertex۰ready iter ∗
model' t γ task Ready iter ∗
vertex۰wp t γ P R task iter
}}}
vertex٠run ctx #t
{{{
RET ();
pool۰context pool ctx scope
}}}
).
Lemma vertex٠releaseｰspec pool ctx scope t γ P R task iter :
{{{
pool۰context pool ctx scope ∗
vertex۰inv t γ P R ∗
vertex۰model t γ task iter ∗
vertex۰wp t γ P R task iter
}}}
vertex٠release ctx #t
{{{
RET ();
pool۰context pool ctx scope
}}}.
Lemma vertex٠yieldｰspec t γ task' iter task :
{{{
vertex۰model t γ task' iter
}}}
vertex٠yield #t task
{{{
RET false;
vertex۰model t γ task iter
}}}.
End vertex۰G.
#[global] Opaque vertex۰inv.
#[global] Opaque vertex۰model.
#[global] Opaque vertex۰output.
#[global] Opaque vertex۰ready.
#[global] Opaque vertex۰finished.
#[global] Opaque vertex۰predecessor.
End base.
Require zoo_parabs.vertex__opaque.
Section vertex۰G.
Context `{vertex۰G : VertexG Σ}.
Implicit Type 𝑡 : location.
Definition vertex۰inv t P R : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.vertex۰inv 𝑡 γ P R.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & #Hinv{_{}} ) ".
#[global] Instance vertex۰invｰne t n :
Proper (
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) (vertex۰inv t).
#[global] Instance vertex۰invｰproper t :
Proper (
(≡) ==>
(≡) ==>
(≡)
) (vertex۰inv t).
Definition vertex۰model t task iter : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.vertex۰model 𝑡 γ task iter.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hmodel{_{}} ) ".
Definition vertex۰output t Q : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.vertex۰output γ Q.
#[local] Instance : CustomIpat "output" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Houtput{_{}} ) ".
Definition vertex۰ready :=
base.vertex۰ready.
Definition vertex۰finished t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.vertex۰finished γ.
#[local] Instance : CustomIpat "finished" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hfinished{_{}} ) ".
Definition vertex۰predecessor t iter : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.vertex۰predecessor γ iter.
#[local] Instance : CustomIpat "predecessor" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hpredecessor{_{}} ) ".
Definition vertex۰wp۰body t P R wp task iter : iProp Σ :=
∀ pool ctx scope iter',
pool۰context pool ctx scope -∗
vertex۰ready iter -∗
vertex۰model t task iter' -∗
WP task ctx {{ res,
∃ b task,
⌜res = #b⌝ ∗
pool۰context pool ctx scope ∗
vertex۰model t task iter' ∗
if b then
▷ P ∗
▷ □ R
else
▷ wp task iter'
}}.
#[local] Definition vertex۰wp۰pre
: val → iProp Σ → iProp Σ →
(val -d> vertex۰iteration -d> iProp Σ) →
val -d> vertex۰iteration -d> iProp Σ
:=
vertex۰wp۰body.
#[local] Instance vertex۰wp۰preｰcontractive t P R :
Contractive (vertex۰wp۰pre t P R).
#[local] Instance vertex۰wp۰preｰne t P R :
NonExpansive (vertex۰wp۰pre t P R).
Definition vertex۰wp t P R : val → vertex۰iteration → iProp Σ :=
fixpoint (vertex۰wp۰pre t P R).
Lemma vertex۰wpｰunfold t P R task iter :
vertex۰wp t P R task iter ⊣⊢
vertex۰wp۰body t P R (vertex۰wp t P R) task iter.
#[global] Instance vertex۰wpｰne n :
Proper (
(=) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) vertex۰wp.
#[local] Lemma vertex۰wpｰtoｰbase 𝑡 γ P R task iter :
𝑡 ↪ γ -∗
vertex۰wp #𝑡 P R task iter -∗
base.vertex۰wp 𝑡 γ P R task iter.
#[global] Instance vertex۰outputｰcontractive t :
Contractive (vertex۰output t).
#[global] Instance vertex۰outputｰproper t :
Proper ((≡) ==> (≡)) (vertex۰output t).
#[global] Instance vertex۰modelｰtimeless t task iter :
Timeless (vertex۰model t task iter).
#[global] Instance vertex۰readyｰtimeless iter :
Timeless (vertex۰ready iter).
#[global] Instance vertex۰finishedｰtimeless t :
Timeless (vertex۰finished t).
#[global] Instance vertex۰predecessorｰtimeless t iter :
Timeless (vertex۰predecessor t iter).
#[global] Instance vertex۰invｰpersistent t P R :
Persistent (vertex۰inv t P R).
#[global] Instance vertex۰readyｰpersistent iter :
Persistent (vertex۰ready iter).
#[global] Instance vertex۰finishedｰpersistent t :
Persistent (vertex۰finished t).
#[global] Instance vertex۰predecessorｰpersistent t iter :
Persistent (vertex۰predecessor t iter).
Lemma vertex۰modelｰexclusive t task1 iter1 task2 iter2 :
vertex۰model t task1 iter1 -∗
vertex۰model t task2 iter2 -∗
False.
Lemma vertex۰modelｰfinished t task iter :
vertex۰model t task iter -∗
vertex۰finished t -∗
False.
Lemma vertex۰outputｰwand {t P R Q1} Q2 :
vertex۰inv t P R -∗
vertex۰output t Q1 -∗
(Q1 -∗ Q2) ={⊤}=∗
vertex۰output t Q2.
Lemma vertex۰outputｰdivide {t P R} Qs :
vertex۰inv t P R -∗
vertex۰output t ([∗ list] Q ∈ Qs, Q) ={⊤}=∗
[∗ list] Q ∈ Qs, vertex۰output t Q.
Lemma vertex۰outputｰsplit {t P R} Q1 Q2 :
vertex۰inv t P R -∗
vertex۰output t (Q1 ∗ Q2) ={⊤}=∗
vertex۰output t Q1 ∗
vertex۰output t Q2.
Lemma vertexｰpredecessorｰfinished t iter :
vertex۰predecessor t iter -∗
vertex۰ready iter -∗
vertex۰finished t.
Lemma vertexｰinvｰfinished t P R :
vertex۰inv t P R -∗
vertex۰finished t ={⊤}=∗
▷ □ R.
Lemma vertexｰinvｰfinished' t P R :
£ 1 -∗
vertex۰inv t P R -∗
vertex۰finished t ={⊤}=∗
□ R.
Lemma vertexｰinvｰfinishedｰoutput t P R Q :
vertex۰inv t P R -∗
vertex۰finished t -∗
vertex۰output t Q ={⊤}=∗
▷^2 Q.
Lemma vertexｰinvｰfinishedｰoutput' t P R Q :
£ 2 -∗
vertex۰inv t P R -∗
vertex۰finished t -∗
vertex۰output t Q ={⊤}=∗
Q.
Lemma vertex٠createｰspec P R (task : option val) :
{{{
True
}}}
vertex٠create task
{{{
t iter
, RET t;
vertex۰inv t P R ∗
vertex۰model t (default (𝗳𝘂𝗻 ⎽ → true)%V task) iter ∗
vertex۰output t P
}}}.
Lemma vertex٠create'ｰspec P R task :
{{{
True
}}}
vertex٠create' task
{{{
t iter
, RET t;
vertex۰inv t P R ∗
vertex۰model t (𝗳𝘂𝗻 "ctx" → task "ctx" ⍮ true) iter ∗
vertex۰output t P
}}}.
Lemma vertex٠taskｰspec t task iter :
{{{
vertex۰model t task iter
}}}
vertex٠task t
{{{
RET task;
vertex۰model t task iter
}}}.
Lemma vertex٠set_taskｰspec t task1 iter task2 :
{{{
vertex۰model t task1 iter
}}}
vertex٠set_task t task2
{{{
RET ();
vertex۰model t task2 iter
}}}.
Lemma vertex٠precedeｰspec t1 P1 R1 t2 P2 R2 task iter :
{{{
vertex۰inv t1 P1 R1 ∗
vertex۰inv t2 P2 R2 ∗
vertex۰model t2 task iter
}}}
vertex٠precede t1 t2
{{{
RET ();
vertex۰model t2 task iter ∗
vertex۰predecessor t1 iter
}}}.
Lemma vertex٠releaseｰspec pool ctx scope t P R task iter :
{{{
pool۰context pool ctx scope ∗
vertex۰inv t P R ∗
vertex۰model t task iter ∗
vertex۰wp t P R task iter
}}}
vertex٠release ctx t
{{{
RET ();
pool۰context pool ctx scope
}}}.
Lemma vertex٠releaseｰspec' pool ctx scope t P R task iter :
{{{
pool۰context pool ctx scope ∗
vertex۰inv t P R ∗
vertex۰model t task iter ∗
( ∀ pool ctx scope,
pool۰context pool ctx scope -∗
vertex۰ready iter -∗
WP task ctx {{ res,
⌜res = true%V⌝ ∗
pool۰context pool ctx scope ∗
▷ P ∗
▷ □ R
}}
)
}}}
vertex٠release ctx t
{{{
RET ();
pool۰context pool ctx scope
}}}.
Lemma vertex٠yieldｰspec t task' iter task :
{{{
vertex۰model t task' iter
}}}
vertex٠yield t task
{{{
RET false;
vertex۰model t task iter
}}}.
End vertex۰G.
#[global] Opaque vertex۰inv.
#[global] Opaque vertex۰model.
#[global] Opaque vertex۰output.
#[global] Opaque vertex۰ready.
#[global] Opaque vertex۰finished.
#[global] Opaque vertex۰predecessor.
Require Import zoo.common.countable.
Require Import zoo.common.gmultiset.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.auth_gmultiset.
Require Import zoo.iris.base_logic.lib.mono_gmultiset.
Require Import zoo.iris.base_logic.lib.subprops.
Require Import zoo.iris.base_logic.lib.twins.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_parabs.base.
Require Export zoo_parabs.vertex__code.
Require Import zoo_parabs.vertex__types.
Require Import zoo.options.
Implicit Type b finished : bool.
Implicit Type preds : nat.
Implicit Type succ : location.
Implicit Type task ctx : val.
Implicit Type own : ownership.
Variant state :=
| Init
| Released
| Ready
| Finished.
Implicit Type state : state.
#[local] Instance stateｰinhabited : Inhabited state :=
populate Init.
#[local] Instance stateｰeq_dec : EqDecision state :=
ltac:(solve_decision).
Record vertex۰name :=
{ vertex۰name۰successors : val
; vertex۰name۰state : gname
; vertex۰name۰iteration : gname
; vertex۰name۰predecessors : gname
; vertex۰name۰output : gname
}.
Implicit Type γ δ π : vertex۰name.
#[local] Instance vertex۰nameｰeq_dec : EqDecision vertex۰name :=
ltac:(solve_decision).
#[local] Instance vertex۰nameｰcountable :
Countable vertex۰name.
Implicit Type Δ Π : gmultiset vertex۰name.
Definition vertex۰iteration :=
gname.
Implicit Type iter : vertex۰iteration.
Class VertexG Σ `{pool۰G : PoolG Σ} :=
{ #[local] vertex۰G۰stack۰G :: StackMpmc2G Σ
; #[local] vertex۰G۰state۰G :: TwinsG Σ (leibnizO state)
; #[local] vertex۰G۰iteration۰G :: TwinsG Σ (leibnizO vertex۰iteration)
; #[local] vertex۰G۰dependencies۰G :: MonoGmultisetG Σ vertex۰name
; #[local] vertex۰G۰predecessors۰G :: AuthGmultisetG Σ vertex۰name
; #[local] vertex۰G۰output۰G :: SubpropsG Σ
}.
Definition vertex۰Σ :=
#[stack_mpmc_2۰Σ
; twins۰Σ (leibnizO state)
; twins۰Σ (leibnizO vertex۰iteration)
; mono_gmultiset۰Σ vertex۰name
; auth_gmultiset۰Σ vertex۰name
; subprops۰Σ
].
#[global] Instance subGｰvertex۰Σ Σ `{pool۰G : PoolG Σ}:
subG vertex۰Σ Σ →
VertexG Σ.
Module base.
Section vertex۰G.
Context `{vertex۰G : VertexG Σ}.
Implicit Type t : location.
Implicit Type P Q R : iProp Σ.
#[local] Definition state₁' γ_state own state :=
twins۰twin₁ (twins۰G := vertex۰G۰state۰G) γ_state own state.
#[local] Definition state₁ γ :=
state₁' γ.(vertex۰name۰state).
#[local] Definition state₂' γ_state state :=
twins۰twin₂ (twins۰G := vertex۰G۰state۰G) γ_state state.
#[local] Definition state₂ γ :=
state₂' γ.(vertex۰name۰state).
#[local] Definition iteration₁' γ_iteration iter :=
twins۰twin₁ γ_iteration (DfracOwn 1) iter.
#[local] Definition iteration₁ γ :=
iteration₁' γ.(vertex۰name۰iteration).
#[local] Definition iteration₂' γ_iteration iter :=
twins۰twin₂ γ_iteration iter.
#[local] Definition iteration₂ γ :=
iteration₂' γ.(vertex۰name۰iteration).
#[local] Definition dependencies۰auth iter own :=
mono_gmultiset۰auth iter own.
#[local] Definition dependencies۰elem iter :=
mono_gmultiset۰elem iter.
#[local] Definition predecessors۰auth' γ_predecessors Π :=
auth_gmultiset۰auth γ_predecessors (DfracOwn 1) Π.
#[local] Definition predecessors۰auth γ Π :=
predecessors۰auth' γ.(vertex۰name۰predecessors) Π.
#[local] Definition predecessors۰elem γ π :=
auth_gmultiset۰frag γ.(vertex۰name۰predecessors) {[+π+]}.
#[local] Definition output۰auth' γ_output :=
subprops۰auth γ_output.
#[local] Definition output۰auth γ :=
subprops۰auth γ.(vertex۰name۰output).
#[local] Definition output۰frag' γ_output :=
subprops۰frag γ_output.
#[local] Definition output۰frag γ :=
output۰frag' γ.(vertex۰name۰output).
#[local] Definition model' t γ task state iter : iProp Σ :=
t.[task] ↦ task ∗
state₁ γ Own state ∗
iteration₁ γ iter.
#[local] Instance : CustomIpat "model'" :=
" ( Ht{which;}_task{_{}} & Hstate{which;}₁{_{}} & Hiteration{which;}₁{_{}} ) ".
Definition vertex۰model t γ task iter : iProp Σ :=
model' t γ task Init iter.
#[local] Instance : CustomIpat "model" :=
" (:model') ".
Definition vertex۰ready iter : iProp Σ :=
∃ Δ,
dependencies۰auth iter Discard Δ ∗
[∗ mset] δ ∈ Δ, state₁ δ Discard Finished.
#[local] Instance : CustomIpat "ready" :=
" ( %Δ{} & #Hdependencies{which;}_auth{_{}} & #HΔ{} ) ".
Definition vertex۰finished γ :=
state₁ γ Discard Finished.
#[local] Instance : CustomIpat "finished" :=
" #Hstate{which;}₁{_{}} ".
Definition vertex۰wp۰body t γ P R wp task iter : iProp Σ :=
∀ pool ctx scope iter',
pool۰context pool ctx scope -∗
vertex۰ready iter -∗
vertex۰model t γ task iter' -∗
WP task ctx {{ res,
∃ b task,
⌜res = #b⌝ ∗
pool۰context pool ctx scope ∗
vertex۰model t γ task iter' ∗
if b then
▷ P ∗
▷ □ R
else
▷ wp task iter'
}}.
#[local] Definition vertex۰wp۰pre
: location → vertex۰name → iProp Σ → iProp Σ →
(val -d> vertex۰iteration -d> iProp Σ) →
val -d> vertex۰iteration -d> iProp Σ
:=
vertex۰wp۰body.
#[local] Instance vertex۰wp۰preｰcontractive t γ P R :
Contractive (vertex۰wp۰pre t γ P R).
#[local] Instance vertex۰wp۰preｰne t γ P R :
NonExpansive (vertex۰wp۰pre t γ P R).
Definition vertex۰wp t γ P R : val → vertex۰iteration → iProp Σ :=
fixpoint (vertex۰wp۰pre t γ P R).
Lemma vertex۰wpｰunfold t γ P R task iter :
vertex۰wp t γ P R task iter ⊣⊢
vertex۰wp۰body t γ P R (vertex۰wp t γ P R) task iter.
#[global] Instance vertex۰wpｰne n :
Proper (
(=) ==>
(=) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) vertex۰wp.
#[local] Definition inv۰state۰init preds iter Π : iProp Σ :=
∃ Δ,
dependencies۰auth iter Own (Δ ⊎ Π) ∗
⌜preds = ˖(size Π)⌝ ∗
[∗ mset] δ ∈ Δ, vertex۰finished δ.
#[local] Instance : CustomIpat "inv۰state۰init" :=
" ( %Δ & {>;}Hdependencies{which;}_auth & {>;}-> & {>;}HΔ ) ".
#[local] Definition inv۰state۰released t γ P R preds iter Π : iProp Σ :=
∃ task Δ,
model' t γ task Released iter ∗
dependencies۰auth iter Discard (Δ ⊎ Π) ∗
⌜preds = size Π⌝ ∗
([∗ mset] δ ∈ Δ, vertex۰finished δ) ∗
vertex۰wp t γ P R task iter.
#[local] Instance : CustomIpat "inv۰state۰released" :=
" ( %task & %Δ & (:model') & {>;}Hdependencies{which;}_auth & {>;}-> & {>;}HΔ & Htask ) ".
#[local] Definition inv۰state۰ready Π : iProp Σ :=
⌜Π = ∅⌝.
#[local] Instance : CustomIpat "inv۰state۰ready" :=
" {>;}-> ".
#[local] Definition inv۰state۰finished γ R preds Π : iProp Σ :=
vertex۰finished γ ∗
⌜preds = ˖(size Π)⌝ ∗
□ R.
#[local] Instance : CustomIpat "inv۰state۰finished" :=
" ( {>;}#Hstate{which;}₁ & {>;}-> & #HR{which;} ) ".
#[local] Definition inv۰state t γ P R state preds iter Π : iProp Σ :=
match state with
| Init ⇒
inv۰state۰init preds iter Π
| Released ⇒
inv۰state۰released t γ P R preds iter Π
| Ready ⇒
inv۰state۰ready Π
| Finished ⇒
inv۰state۰finished γ R preds Π
end.
#[local] Definition inv۰successor (inv : location → vertex۰name → iProp Σ → iProp Σ → iProp Σ) γ succ : iProp Σ :=
∃ γ_succ P_succ R_succ,
inv succ γ_succ P_succ R_succ ∗
predecessors۰elem γ_succ γ.
#[local] Instance : CustomIpat "inv۰successor" :=
" ( %γ_succ & %P_succ & %R_succ & #Hinv_succ & Hpredecessors_elem ) ".
#[local] Definition inv۰successors inv γ finished :=
if finished then (
stack_mpmc_2۰model γ.(vertex۰name۰successors) None
) else (
∃ succs,
stack_mpmc_2۰model γ.(vertex۰name۰successors) (Some $ #*@{location} succs) ∗
[∗ list] succ ∈ succs, inv۰successor inv γ succ
)%I.
#[local] Instance : CustomIpat "inv۰successors۰finished" :=
" >Hsuccessors{which;}_model ".
#[local] Instance : CustomIpat "inv۰successors" :=
" ( %succs & >Hsuccessors{which;}_model & Hsuccs ) ".
#[local] Definition inv۰inner inv t γ P R : iProp Σ :=
∃ preds state iter Π,
t.[preds] ↦ #preds ∗
state₂ γ state ∗
iteration₂ γ iter ∗
predecessors۰auth γ Π ∗
output۰auth γ P (bool_decide (state = Finished)) ∗
inv۰state t γ P R state preds iter Π ∗
inv۰successors inv γ (bool_decide (state = Finished)).
#[local] Instance : CustomIpat "inv۰inner" :=
" ( %preds{} & %state{} & %iter{} & %Π & Ht{which;}_preds & >Hstate{which;}₂ & >Hiteration{which;}₂ & Hpredecessors{which;}_auth & Houtput{which;}_auth & Hinv_state{which;} & Hinv_successors{which;} ) ".
#[local] Definition inv۰pre
: (location -d> vertex۰name -d> iProp Σ -d> iProp Σ -d> iProp Σ) →
location -d> vertex۰name -d> iProp Σ -d> iProp Σ -d> iProp Σ
:=
λ inv t γ P R, (
t.[succs] ↦□ γ.(vertex۰name۰successors) ∗
stack_mpmc_2۰inv γ.(vertex۰name۰successors) (nroot.@"successors") ∗
invariants.inv (nroot.@"inv") (inv۰inner inv t γ P R)
)%I.
#[local] Instance : CustomIpat "inv۰pre" :=
" ( #Ht{}_succs & #Hsuccessors{}_inv & #Hinv{_{}} ) ".
#[local] Instance inv۰preｰcontractive :
Contractive inv۰pre.
Definition vertex۰inv : location → vertex۰name → iProp Σ → iProp Σ → iProp Σ :=
fixpoint inv۰pre.
#[local] Lemma vertex۰invｰunfold t γ P R :
vertex۰inv t γ P R ⊣⊢
inv۰pre vertex۰inv t γ P R.
#[local] Instance vertex۰invｰcontractive t γ n :
Proper (
dist_later n ==>
dist_later n ==>
(≡{n}≡)
) (vertex۰inv t γ).
#[global] Instance vertex۰invｰne t γ n :
Proper (
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) (vertex۰inv t γ).
#[global] Instance vertex۰invｰproper t γ :
Proper (
(≡) ==>
(≡) ==>
(≡)
) (vertex۰inv t γ).
Definition vertex۰output γ Q :=
output۰frag γ Q.
#[local] Instance : CustomIpat "output" :=
" Houtput{which;}_frag{_{}} ".
#[global] Instance vertex۰outputｰcontractive γ :
Contractive (vertex۰output γ).
#[global] Instance vertex۰outputｰproper γ :
Proper ((≡) ==> (≡)) (vertex۰output γ).
Definition vertex۰predecessor γ iter :=
dependencies۰elem iter γ.
#[local] Instance : CustomIpat "predecessor" :=
" #Hdependencies{which;}_elem{_{}} ".
#[global] Instance vertex۰modelｰtimeless t γ task iter :
Timeless (vertex۰model t γ task iter).
#[global] Instance vertex۰readyｰtimeless iter :
Timeless (vertex۰ready iter).
#[global] Instance vertex۰finishedｰtimeless γ :
Timeless (vertex۰finished γ).
#[global] Instance vertex۰predecessorｰtimeless γ iter :
Timeless (vertex۰predecessor γ iter).
#[global] Instance vertex۰invｰpersistent t γ P R :
Persistent (vertex۰inv t γ P R).
#[global] Instance vertex۰readyｰpersistent iter :
Persistent (vertex۰ready iter).
#[global] Instance vertex۰finishedｰpersistent γ :
Persistent (vertex۰finished γ).
#[global] Instance vertex۰predecessorｰpersistent γ iter :
Persistent (vertex۰predecessor γ iter).
#[local] Lemma stateｰalloc :
⊢ |==>
∃ γ_state,
state₁' γ_state Own Init ∗
state₂' γ_state Init.
#[local] Lemma stateｰagree γ own1 state1 state2 :
state₁ γ own1 state1 -∗
state₂ γ state2 -∗
⌜state1 = state2⌝.
#[local] Lemma state₁ｰexclusive γ state1 own2 state2 :
state₁ γ Own state1 -∗
state₁ γ own2 state2 -∗
False.
#[local] Lemma stateｰupdate {γ state1 state2} state :
state₁ γ Own state1 -∗
state₂ γ state2 ==∗
state₁ γ Own state ∗
state₂ γ state.
#[local] Lemma state₁ｰdiscard γ state :
state₁ γ Own state ⊢ |==>
state₁ γ Discard state.
#[local] Lemma iterationｰalloc iter :
⊢ |==>
∃ γ_iteration,
iteration₁' γ_iteration iter ∗
iteration₂' γ_iteration iter.
#[local] Lemma iterationｰagree γ iteration1 iteration2 :
iteration₁ γ iteration1 -∗
iteration₂ γ iteration2 -∗
⌜iteration1 = iteration2⌝.
#[local] Lemma iteration₁ｰexclusive γ iteration1 iteration2 :
iteration₁ γ iteration1 -∗
iteration₁ γ iteration2 -∗
False.
#[local] Lemma iterationｰupdate {γ iteration1 iteration2} iteration :
iteration₁ γ iteration1 -∗
iteration₂ γ iteration2 ==∗
iteration₁ γ iteration ∗
iteration₂ γ iteration.
#[local] Lemma dependenciesｰalloc :
⊢ |==>
∃ iter,
dependencies۰auth iter Own ∅.
#[local] Lemma dependenciesｰadd {iter Δ} δ :
dependencies۰auth iter Own Δ ⊢ |==>
dependencies۰auth iter Own ({[+δ+]} ⊎ Δ) ∗
dependencies۰elem iter δ.
#[local] Lemma dependenciesｰelem_of iter own Δ δ :
dependencies۰auth iter own Δ -∗
dependencies۰elem iter δ -∗
⌜δ ∈ Δ⌝.
#[local] Lemma dependenciesｰdiscard iter Δ :
dependencies۰auth iter Own Δ ⊢ |==>
dependencies۰auth iter Discard Δ.
#[local] Lemma predecessorsｰalloc :
⊢ |==>
∃ γ_predecessors,
predecessors۰auth' γ_predecessors ∅.
#[local] Lemma predecessorsｰelem_of γ Π π :
predecessors۰auth γ Π -∗
predecessors۰elem γ π -∗
⌜π ∈ Π⌝.
#[local] Lemma predecessorsｰadd {γ Π} π :
predecessors۰auth γ Π ⊢ |==>
predecessors۰auth γ ({[+π+]} ⊎ Π) ∗
predecessors۰elem γ π.
#[local] Lemma predecessorsｰremove γ Π π :
predecessors۰auth γ Π -∗
predecessors۰elem γ π ==∗
predecessors۰auth γ (Π ∖ {[+π+]}).
#[local] Lemma outputｰalloc P :
⊢ |==>
∃ γ_output,
output۰auth' γ_output P false ∗
output۰frag' γ_output P.
#[local] Lemma outputｰwand {γ P finished Q1} Q2 E :
▷ output۰auth γ P finished -∗
output۰frag γ Q1 -∗
(Q1 -∗ Q2) ={E}=∗
▷ output۰auth γ P finished ∗
output۰frag γ Q2.
#[local] Lemma outputｰdivide {γ P finished} Qs E :
▷ output۰auth γ P finished -∗
output۰frag γ ([∗ list] Q ∈ Qs, Q) ={E}=∗
▷ output۰auth γ P finished ∗
[∗ list] Q ∈ Qs, output۰frag γ Q.
#[local] Lemma outputｰproduce γ P :
▷ output۰auth γ P false -∗
P -∗
▷ output۰auth γ P true.
#[local] Lemma outputｰconsume γ P Q E :
▷ output۰auth γ P true -∗
output۰frag γ Q ={E}=∗
▷ output۰auth γ P true ∗
▷^2 Q.
Lemma vertex۰modelｰexclusive t γ task1 iter1 task2 iter2 :
vertex۰model t γ task1 iter1 -∗
vertex۰model t γ task2 iter2 -∗
False.
Lemma vertex۰modelｰfinished t γ task iter :
vertex۰model t γ task iter -∗
vertex۰finished γ -∗
False.
Lemma vertex۰outputｰwand {t γ P R Q1} Q2 :
vertex۰inv t γ P R -∗
vertex۰output γ Q1 -∗
(Q1 -∗ Q2) ={⊤}=∗
vertex۰output γ Q2.
Lemma vertex۰outputｰdivide {t γ P R} Qs :
vertex۰inv t γ P R -∗
vertex۰output γ ([∗ list] Q ∈ Qs, Q) ={⊤}=∗
[∗ list] Q ∈ Qs, vertex۰output γ Q.
Lemma vertexｰpredecessorｰfinished γ iter :
vertex۰predecessor γ iter -∗
vertex۰ready iter -∗
vertex۰finished γ.
Lemma vertexｰinvｰfinished t γ P R :
vertex۰inv t γ P R -∗
vertex۰finished γ ={⊤}=∗
▷ □ R.
Lemma vertexｰinvｰfinishedｰoutput t γ P R Q :
vertex۰inv t γ P R -∗
vertex۰finished γ -∗
vertex۰output γ Q ={⊤}=∗
▷^2 Q.
Lemma vertex٠createｰspec P R (task : option val) :
{{{
True
}}}
vertex٠create task
{{{
t γ iter
, RET #t;
meta_token t ⊤ ∗
vertex۰inv t γ P R ∗
vertex۰model t γ (default (𝗳𝘂𝗻 ⎽ → true)%V task) iter ∗
vertex۰output γ P
}}}.
Lemma vertex٠create'ｰspec P R task :
{{{
True
}}}
vertex٠create' task
{{{
t γ iter
, RET #t;
meta_token t ⊤ ∗
vertex۰inv t γ P R ∗
vertex۰model t γ (𝗳𝘂𝗻 "ctx" → task "ctx" ⍮ true) iter ∗
vertex۰output γ P
}}}.
Lemma vertex٠taskｰspec t γ task iter :
{{{
vertex۰model t γ task iter
}}}
vertex٠task #t
{{{
RET task;
vertex۰model t γ task iter
}}}.
Lemma vertex٠set_taskｰspec t γ task1 iter task2 :
{{{
vertex۰model t γ task1 iter
}}}
vertex٠set_task #t task2
{{{
RET ();
vertex۰model t γ task2 iter
}}}.
Lemma vertex٠precedeｰspec t1 γ1 P1 R1 t2 γ2 P2 R2 task iter :
{{{
vertex۰inv t1 γ1 P1 R1 ∗
vertex۰inv t2 γ2 P2 R2 ∗
vertex۰model t2 γ2 task iter
}}}
vertex٠precede #t1 #t2
{{{
RET ();
vertex۰model t2 γ2 task iter ∗
vertex۰predecessor γ1 iter
}}}.
#[local] Lemma vertex٠release_runｰspec :
⊢ (
∀ pool ctx scope t γ P R task iter,
{{{
pool۰context pool ctx scope ∗
vertex۰inv t γ P R ∗
vertex۰model t γ task iter ∗
vertex۰wp t γ P R task iter
}}}
vertex٠release ctx #t
{{{
RET ();
pool۰context pool ctx scope
}}}
) ∧ (
∀ pool ctx scope t γ P R π,
{{{
pool۰context pool ctx scope ∗
vertex۰inv t γ P R ∗
predecessors۰elem γ π ∗
vertex۰finished π
}}}
vertex٠release ctx #t
{{{
RET ();
pool۰context pool ctx scope
}}}
) ∧ (
∀ pool ctx scope t γ iter P R task,
{{{
pool۰context pool ctx scope ∗
vertex۰inv t γ P R ∗
vertex۰ready iter ∗
model' t γ task Ready iter ∗
vertex۰wp t γ P R task iter
}}}
vertex٠run ctx #t
{{{
RET ();
pool۰context pool ctx scope
}}}
).
Lemma vertex٠releaseｰspec pool ctx scope t γ P R task iter :
{{{
pool۰context pool ctx scope ∗
vertex۰inv t γ P R ∗
vertex۰model t γ task iter ∗
vertex۰wp t γ P R task iter
}}}
vertex٠release ctx #t
{{{
RET ();
pool۰context pool ctx scope
}}}.
Lemma vertex٠yieldｰspec t γ task' iter task :
{{{
vertex۰model t γ task' iter
}}}
vertex٠yield #t task
{{{
RET false;
vertex۰model t γ task iter
}}}.
End vertex۰G.
#[global] Opaque vertex۰inv.
#[global] Opaque vertex۰model.
#[global] Opaque vertex۰output.
#[global] Opaque vertex۰ready.
#[global] Opaque vertex۰finished.
#[global] Opaque vertex۰predecessor.
End base.
Require zoo_parabs.vertex__opaque.
Section vertex۰G.
Context `{vertex۰G : VertexG Σ}.
Implicit Type 𝑡 : location.
Definition vertex۰inv t P R : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.vertex۰inv 𝑡 γ P R.
#[local] Instance : CustomIpat "inv" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & #Hinv{_{}} ) ".
#[global] Instance vertex۰invｰne t n :
Proper (
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) (vertex۰inv t).
#[global] Instance vertex۰invｰproper t :
Proper (
(≡) ==>
(≡) ==>
(≡)
) (vertex۰inv t).
Definition vertex۰model t task iter : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.vertex۰model 𝑡 γ task iter.
#[local] Instance : CustomIpat "model" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hmodel{_{}} ) ".
Definition vertex۰output t Q : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.vertex۰output γ Q.
#[local] Instance : CustomIpat "output" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Houtput{_{}} ) ".
Definition vertex۰ready :=
base.vertex۰ready.
Definition vertex۰finished t : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.vertex۰finished γ.
#[local] Instance : CustomIpat "finished" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hfinished{_{}} ) ".
Definition vertex۰predecessor t iter : iProp Σ :=
∃ 𝑡 γ,
⌜t = #𝑡⌝ ∗
𝑡 ↪ γ ∗
base.vertex۰predecessor γ iter.
#[local] Instance : CustomIpat "predecessor" :=
" ( %𝑡{}{_{!}} & %γ{}{_{!}} & {%Heq{};->} & #Hmeta{_{}}{_{!}} & Hpredecessor{_{}} ) ".
Definition vertex۰wp۰body t P R wp task iter : iProp Σ :=
∀ pool ctx scope iter',
pool۰context pool ctx scope -∗
vertex۰ready iter -∗
vertex۰model t task iter' -∗
WP task ctx {{ res,
∃ b task,
⌜res = #b⌝ ∗
pool۰context pool ctx scope ∗
vertex۰model t task iter' ∗
if b then
▷ P ∗
▷ □ R
else
▷ wp task iter'
}}.
#[local] Definition vertex۰wp۰pre
: val → iProp Σ → iProp Σ →
(val -d> vertex۰iteration -d> iProp Σ) →
val -d> vertex۰iteration -d> iProp Σ
:=
vertex۰wp۰body.
#[local] Instance vertex۰wp۰preｰcontractive t P R :
Contractive (vertex۰wp۰pre t P R).
#[local] Instance vertex۰wp۰preｰne t P R :
NonExpansive (vertex۰wp۰pre t P R).
Definition vertex۰wp t P R : val → vertex۰iteration → iProp Σ :=
fixpoint (vertex۰wp۰pre t P R).
Lemma vertex۰wpｰunfold t P R task iter :
vertex۰wp t P R task iter ⊣⊢
vertex۰wp۰body t P R (vertex۰wp t P R) task iter.
#[global] Instance vertex۰wpｰne n :
Proper (
(=) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡) ==>
(≡{n}≡)
) vertex۰wp.
#[local] Lemma vertex۰wpｰtoｰbase 𝑡 γ P R task iter :
𝑡 ↪ γ -∗
vertex۰wp #𝑡 P R task iter -∗
base.vertex۰wp 𝑡 γ P R task iter.
#[global] Instance vertex۰outputｰcontractive t :
Contractive (vertex۰output t).
#[global] Instance vertex۰outputｰproper t :
Proper ((≡) ==> (≡)) (vertex۰output t).
#[global] Instance vertex۰modelｰtimeless t task iter :
Timeless (vertex۰model t task iter).
#[global] Instance vertex۰readyｰtimeless iter :
Timeless (vertex۰ready iter).
#[global] Instance vertex۰finishedｰtimeless t :
Timeless (vertex۰finished t).
#[global] Instance vertex۰predecessorｰtimeless t iter :
Timeless (vertex۰predecessor t iter).
#[global] Instance vertex۰invｰpersistent t P R :
Persistent (vertex۰inv t P R).
#[global] Instance vertex۰readyｰpersistent iter :
Persistent (vertex۰ready iter).
#[global] Instance vertex۰finishedｰpersistent t :
Persistent (vertex۰finished t).
#[global] Instance vertex۰predecessorｰpersistent t iter :
Persistent (vertex۰predecessor t iter).
Lemma vertex۰modelｰexclusive t task1 iter1 task2 iter2 :
vertex۰model t task1 iter1 -∗
vertex۰model t task2 iter2 -∗
False.
Lemma vertex۰modelｰfinished t task iter :
vertex۰model t task iter -∗
vertex۰finished t -∗
False.
Lemma vertex۰outputｰwand {t P R Q1} Q2 :
vertex۰inv t P R -∗
vertex۰output t Q1 -∗
(Q1 -∗ Q2) ={⊤}=∗
vertex۰output t Q2.
Lemma vertex۰outputｰdivide {t P R} Qs :
vertex۰inv t P R -∗
vertex۰output t ([∗ list] Q ∈ Qs, Q) ={⊤}=∗
[∗ list] Q ∈ Qs, vertex۰output t Q.
Lemma vertex۰outputｰsplit {t P R} Q1 Q2 :
vertex۰inv t P R -∗
vertex۰output t (Q1 ∗ Q2) ={⊤}=∗
vertex۰output t Q1 ∗
vertex۰output t Q2.
Lemma vertexｰpredecessorｰfinished t iter :
vertex۰predecessor t iter -∗
vertex۰ready iter -∗
vertex۰finished t.
Lemma vertexｰinvｰfinished t P R :
vertex۰inv t P R -∗
vertex۰finished t ={⊤}=∗
▷ □ R.
Lemma vertexｰinvｰfinished' t P R :
£ 1 -∗
vertex۰inv t P R -∗
vertex۰finished t ={⊤}=∗
□ R.
Lemma vertexｰinvｰfinishedｰoutput t P R Q :
vertex۰inv t P R -∗
vertex۰finished t -∗
vertex۰output t Q ={⊤}=∗
▷^2 Q.
Lemma vertexｰinvｰfinishedｰoutput' t P R Q :
£ 2 -∗
vertex۰inv t P R -∗
vertex۰finished t -∗
vertex۰output t Q ={⊤}=∗
Q.
Lemma vertex٠createｰspec P R (task : option val) :
{{{
True
}}}
vertex٠create task
{{{
t iter
, RET t;
vertex۰inv t P R ∗
vertex۰model t (default (𝗳𝘂𝗻 ⎽ → true)%V task) iter ∗
vertex۰output t P
}}}.
Lemma vertex٠create'ｰspec P R task :
{{{
True
}}}
vertex٠create' task
{{{
t iter
, RET t;
vertex۰inv t P R ∗
vertex۰model t (𝗳𝘂𝗻 "ctx" → task "ctx" ⍮ true) iter ∗
vertex۰output t P
}}}.
Lemma vertex٠taskｰspec t task iter :
{{{
vertex۰model t task iter
}}}
vertex٠task t
{{{
RET task;
vertex۰model t task iter
}}}.
Lemma vertex٠set_taskｰspec t task1 iter task2 :
{{{
vertex۰model t task1 iter
}}}
vertex٠set_task t task2
{{{
RET ();
vertex۰model t task2 iter
}}}.
Lemma vertex٠precedeｰspec t1 P1 R1 t2 P2 R2 task iter :
{{{
vertex۰inv t1 P1 R1 ∗
vertex۰inv t2 P2 R2 ∗
vertex۰model t2 task iter
}}}
vertex٠precede t1 t2
{{{
RET ();
vertex۰model t2 task iter ∗
vertex۰predecessor t1 iter
}}}.
Lemma vertex٠releaseｰspec pool ctx scope t P R task iter :
{{{
pool۰context pool ctx scope ∗
vertex۰inv t P R ∗
vertex۰model t task iter ∗
vertex۰wp t P R task iter
}}}
vertex٠release ctx t
{{{
RET ();
pool۰context pool ctx scope
}}}.
Lemma vertex٠releaseｰspec' pool ctx scope t P R task iter :
{{{
pool۰context pool ctx scope ∗
vertex۰inv t P R ∗
vertex۰model t task iter ∗
( ∀ pool ctx scope,
pool۰context pool ctx scope -∗
vertex۰ready iter -∗
WP task ctx {{ res,
⌜res = true%V⌝ ∗
pool۰context pool ctx scope ∗
▷ P ∗
▷ □ R
}}
)
}}}
vertex٠release ctx t
{{{
RET ();
pool۰context pool ctx scope
}}}.
Lemma vertex٠yieldｰspec t task' iter task :
{{{
vertex۰model t task' iter
}}}
vertex٠yield t task
{{{
RET false;
vertex۰model t task iter
}}}.
End vertex۰G.
#[global] Opaque vertex۰inv.
#[global] Opaque vertex۰model.
#[global] Opaque vertex۰output.
#[global] Opaque vertex۰ready.
#[global] Opaque vertex۰finished.
#[global] Opaque vertex۰predecessor.