Library zoo_parabs.future
From zoo Require Import
prelude.
From zoo.iris.bi Require Import
big_op.
From zoo.language Require Import
notations.
From zoo.program_logic Require Export
biglater.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
ivar_4
list.
From zoo_parabs Require Export
base
future__code.
From zoo_parabs Require Import
pool.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types depth : nat.
Implicit Types v t pool ctx task waiter : val.
Implicit Types scope : pool_scope.
Implicit Types ω : gname.
Implicit Types ωs : list gname.
Class FutureG Σ `{pool_G : PoolG Σ} :=
{ #[local] future_G_ivar_G :: Ivar4G Σ
}.
Definition future_Σ :=
#[ivar_4_Σ
].
#[global] Instance subG_future_Σ Σ `{pool_G : PoolG Σ} :
subG future_Σ Σ →
FutureG Σ.
Section future_G.
Context `{future_G : FutureG Σ}.
Implicit Types P : iProp Σ.
Implicit Types Ψ Χ Ξ : val → iProp Σ.
#[local] Definition finished t : iProp Σ :=
∃ waiters Ps,
ivar_4_resolved t ∗
ivar_4_waiters t waiters Ps ∗
[∗ list] P ∈ Ps, □ P.
#[local] Instance : CustomIpat "finished" :=
" ( %waiters & %Ps & #Hresolved & #Hwaiters & #HPs ) ".
Definition future_inv pool t Ψ Ξ : iProp Σ :=
∃ depth,
ivar_4_inv t Ψ Ξ (pool_context pool) ∗
⧖ depth ∗
□ (
pool_finished pool -∗
▷^(2 × depth + 1) finished t
).
#[local] Instance : CustomIpat "inv" :=
" ( %depth{} & #Hinv{_{}} & #H⧖{_{}} & #Htermination{_{}} ) ".
Definition future_obligation pool P : iProp Σ :=
∃ depth,
⧖ depth ∗
□ (
pool_finished pool -∗
▷^(2 × depth + 2) □ P
).
#[local] Instance : CustomIpat "obligation" :=
" ( %depth & #H⧖ & #Htermination ) ".
Definition future_consumer :=
ivar_4_consumer.
Definition future_result :=
ivar_4_result.
Definition future_resolved t : iProp Σ :=
∃ v,
future_result t v.
#[global] Instance future_inv_proper pool t :
Proper (
(pointwise_relation _ (≡)) ==>
(pointwise_relation _ (≡)) ==>
(≡)
) (future_inv pool t).
#[global] Instance future_obligation_proper pool :
Proper (
(≡) ==>
(≡)
) (future_obligation pool).
#[global] Instance future_consumer_proper t :
Proper (
(pointwise_relation _ (≡)) ==>
(≡)
) (future_consumer t).
#[global] Instance future_result_timeless t v :
Timeless (future_result t v).
#[global] Instance future_inv_persistent pool t Ψ Ξ :
Persistent (future_inv pool t Ψ Ξ).
#[global] Instance future_obligation_persistent pool P :
Persistent (future_obligation pool P).
#[global] Instance future_result_persistent t v :
Persistent (future_result t v).
#[local] Ltac solve_biglater :=
iFrame "#";
iApply bi.laterN_le;
last iFrame "#∗";
apply Nat.add_le_mono;
[ auto using Nat.mul_le_mono_r
| etrans;
last apply later_constant_lb;
lia
].
Lemma future_inv_finished pool t Ψ Ξ :
future_inv pool t Ψ Ξ -∗
pool_finished pool -∗
▶ future_resolved t.
Lemma future_obligation_finished pool P :
future_obligation pool P -∗
pool_finished pool -∗
▶ □ P.
Lemma future_consumer_wand {pool t Ψ Ξ Χ1} Χ2 :
future_inv pool t Ψ Ξ -∗
future_consumer t Χ1 -∗
(∀ x, Χ1 x -∗ Χ2 x) ={⊤}=∗
future_consumer t Χ2.
Lemma future_consumer_divide {pool t Ψ Ξ} Χs :
future_inv pool t Ψ Ξ -∗
future_consumer t (λ x, [∗ list] Χ ∈ Χs, Χ x) ={⊤}=∗
[∗ list] Χ ∈ Χs, future_consumer t Χ.
Lemma future_consumer_split {pool t Ψ Ξ} Χ1 Χ2 :
future_inv pool t Ψ Ξ -∗
future_consumer t (λ v, Χ1 v ∗ Χ2 v) ={⊤}=∗
future_consumer t Χ1 ∗
future_consumer t Χ2.
Lemma future_result_agree t v1 v2 :
future_result t v1 -∗
future_result t v2 -∗
⌜v1 = v2⌝.
Lemma future_inv_result pool t Ψ Ξ v :
future_inv pool t Ψ Ξ -∗
future_result t v ={⊤}=∗
▷ □ Ξ v.
Lemma future_inv_result' pool t Ψ Ξ v :
£ 1 -∗
future_inv pool t Ψ Ξ -∗
future_result t v ={⊤}=∗
□ Ξ v.
Lemma future_inv_result_consumer pool t Ψ Ξ v Χ :
future_inv pool t Ψ Ξ -∗
future_result t v -∗
future_consumer t Χ ={⊤}=∗
▷^2 Χ v ∗
▷ □ Ξ v.
Lemma future_inv_result_consumer' pool t Ψ Ξ v Χ :
£ 2 -∗
future_inv pool t Ψ Ξ -∗
future_result t v -∗
future_consumer t Χ ={⊤}=∗
Χ v ∗
□ Ξ v.
Lemma future٠return𑁒spec pool Ψ Ξ v :
{{{
Ψ v ∗
□ Ξ v
}}}
future٠return v
{{{
t
, RET t;
future_inv pool t Ψ Ξ ∗
future_consumer t Ψ ∗
future_result t v
}}}.
#[local] Lemma future٠set𑁒spec pool ctx scope t Ψ Ξ v :
{{{
pool_context pool ctx scope ∗
ivar_4_inv t Ψ Ξ (pool_context pool) ∗
ivar_4_producer t ∗
▷ Ψ v ∗
▷ □ Ξ v
}}}
future٠set ctx t v
{{{
RET ();
pool_context pool ctx scope ∗
finished t
}}}.
Lemma future٠async𑁒spec Ψ Ξ pool ctx scope task :
{{{
pool_context pool ctx scope ∗
( ∀ ctx scope,
pool_context pool ctx scope -∗
WP task ctx {{ v,
pool_context pool ctx scope ∗
▷ Ψ v ∗
▷ □ Ξ v
}}
)
}}}
future٠async ctx task
{{{
t
, RET t;
pool_context pool ctx scope ∗
future_inv pool t Ψ Ξ ∗
future_consumer t Ψ
}}}.
Lemma future٠wait𑁒spec pool ctx scope t Ψ Ξ :
{{{
pool_context pool ctx scope ∗
future_inv pool t Ψ Ξ
}}}
future٠wait ctx t
{{{
v
, RET v;
£ 2 ∗
pool_context pool ctx scope ∗
future_result t v
}}}.
Lemma future٠iter𑁒spec P pool ctx scope t Ψ Ξ task :
{{{
pool_context pool ctx scope ∗
future_inv pool t Ψ Ξ ∗
( ∀ ctx scope v,
pool_context pool ctx scope -∗
future_result t v -∗
WP task ctx v {{ res,
⌜res = ()%V⌝ ∗
pool_context pool ctx scope ∗
▷ □ P
}}
)
}}}
future٠iter ctx t task
{{{
RET ();
pool_context pool ctx scope ∗
future_obligation pool P
}}}.
Lemma future٠map𑁒spec {pool ctx scope t1 Ψ1 Ξ1} Ψ2 Ξ2 task :
{{{
pool_context pool ctx scope ∗
future_inv pool t1 Ψ1 Ξ1 ∗
( ∀ ctx scope v1,
pool_context pool ctx scope -∗
future_result t1 v1 -∗
WP task ctx v1 {{ v2,
pool_context pool ctx scope ∗
▷ Ψ2 v2 ∗
▷ □ Ξ2 v2
}}
)
}}}
future٠map ctx t1 task
{{{
t2
, RET t2;
pool_context pool ctx scope ∗
future_inv pool t2 Ψ2 Ξ2 ∗
future_consumer t2 Ψ2
}}}.
End future_G.
From zoo_parabs Require
future__opaque.
#[global] Opaque future_inv.
#[global] Opaque future_obligation.
#[global] Opaque future_consumer.
#[global] Opaque future_result.
prelude.
From zoo.iris.bi Require Import
big_op.
From zoo.language Require Import
notations.
From zoo.program_logic Require Export
biglater.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
ivar_4
list.
From zoo_parabs Require Export
base
future__code.
From zoo_parabs Require Import
pool.
From zoo Require Import
options.
Implicit Types b : bool.
Implicit Types depth : nat.
Implicit Types v t pool ctx task waiter : val.
Implicit Types scope : pool_scope.
Implicit Types ω : gname.
Implicit Types ωs : list gname.
Class FutureG Σ `{pool_G : PoolG Σ} :=
{ #[local] future_G_ivar_G :: Ivar4G Σ
}.
Definition future_Σ :=
#[ivar_4_Σ
].
#[global] Instance subG_future_Σ Σ `{pool_G : PoolG Σ} :
subG future_Σ Σ →
FutureG Σ.
Section future_G.
Context `{future_G : FutureG Σ}.
Implicit Types P : iProp Σ.
Implicit Types Ψ Χ Ξ : val → iProp Σ.
#[local] Definition finished t : iProp Σ :=
∃ waiters Ps,
ivar_4_resolved t ∗
ivar_4_waiters t waiters Ps ∗
[∗ list] P ∈ Ps, □ P.
#[local] Instance : CustomIpat "finished" :=
" ( %waiters & %Ps & #Hresolved & #Hwaiters & #HPs ) ".
Definition future_inv pool t Ψ Ξ : iProp Σ :=
∃ depth,
ivar_4_inv t Ψ Ξ (pool_context pool) ∗
⧖ depth ∗
□ (
pool_finished pool -∗
▷^(2 × depth + 1) finished t
).
#[local] Instance : CustomIpat "inv" :=
" ( %depth{} & #Hinv{_{}} & #H⧖{_{}} & #Htermination{_{}} ) ".
Definition future_obligation pool P : iProp Σ :=
∃ depth,
⧖ depth ∗
□ (
pool_finished pool -∗
▷^(2 × depth + 2) □ P
).
#[local] Instance : CustomIpat "obligation" :=
" ( %depth & #H⧖ & #Htermination ) ".
Definition future_consumer :=
ivar_4_consumer.
Definition future_result :=
ivar_4_result.
Definition future_resolved t : iProp Σ :=
∃ v,
future_result t v.
#[global] Instance future_inv_proper pool t :
Proper (
(pointwise_relation _ (≡)) ==>
(pointwise_relation _ (≡)) ==>
(≡)
) (future_inv pool t).
#[global] Instance future_obligation_proper pool :
Proper (
(≡) ==>
(≡)
) (future_obligation pool).
#[global] Instance future_consumer_proper t :
Proper (
(pointwise_relation _ (≡)) ==>
(≡)
) (future_consumer t).
#[global] Instance future_result_timeless t v :
Timeless (future_result t v).
#[global] Instance future_inv_persistent pool t Ψ Ξ :
Persistent (future_inv pool t Ψ Ξ).
#[global] Instance future_obligation_persistent pool P :
Persistent (future_obligation pool P).
#[global] Instance future_result_persistent t v :
Persistent (future_result t v).
#[local] Ltac solve_biglater :=
iFrame "#";
iApply bi.laterN_le;
last iFrame "#∗";
apply Nat.add_le_mono;
[ auto using Nat.mul_le_mono_r
| etrans;
last apply later_constant_lb;
lia
].
Lemma future_inv_finished pool t Ψ Ξ :
future_inv pool t Ψ Ξ -∗
pool_finished pool -∗
▶ future_resolved t.
Lemma future_obligation_finished pool P :
future_obligation pool P -∗
pool_finished pool -∗
▶ □ P.
Lemma future_consumer_wand {pool t Ψ Ξ Χ1} Χ2 :
future_inv pool t Ψ Ξ -∗
future_consumer t Χ1 -∗
(∀ x, Χ1 x -∗ Χ2 x) ={⊤}=∗
future_consumer t Χ2.
Lemma future_consumer_divide {pool t Ψ Ξ} Χs :
future_inv pool t Ψ Ξ -∗
future_consumer t (λ x, [∗ list] Χ ∈ Χs, Χ x) ={⊤}=∗
[∗ list] Χ ∈ Χs, future_consumer t Χ.
Lemma future_consumer_split {pool t Ψ Ξ} Χ1 Χ2 :
future_inv pool t Ψ Ξ -∗
future_consumer t (λ v, Χ1 v ∗ Χ2 v) ={⊤}=∗
future_consumer t Χ1 ∗
future_consumer t Χ2.
Lemma future_result_agree t v1 v2 :
future_result t v1 -∗
future_result t v2 -∗
⌜v1 = v2⌝.
Lemma future_inv_result pool t Ψ Ξ v :
future_inv pool t Ψ Ξ -∗
future_result t v ={⊤}=∗
▷ □ Ξ v.
Lemma future_inv_result' pool t Ψ Ξ v :
£ 1 -∗
future_inv pool t Ψ Ξ -∗
future_result t v ={⊤}=∗
□ Ξ v.
Lemma future_inv_result_consumer pool t Ψ Ξ v Χ :
future_inv pool t Ψ Ξ -∗
future_result t v -∗
future_consumer t Χ ={⊤}=∗
▷^2 Χ v ∗
▷ □ Ξ v.
Lemma future_inv_result_consumer' pool t Ψ Ξ v Χ :
£ 2 -∗
future_inv pool t Ψ Ξ -∗
future_result t v -∗
future_consumer t Χ ={⊤}=∗
Χ v ∗
□ Ξ v.
Lemma future٠return𑁒spec pool Ψ Ξ v :
{{{
Ψ v ∗
□ Ξ v
}}}
future٠return v
{{{
t
, RET t;
future_inv pool t Ψ Ξ ∗
future_consumer t Ψ ∗
future_result t v
}}}.
#[local] Lemma future٠set𑁒spec pool ctx scope t Ψ Ξ v :
{{{
pool_context pool ctx scope ∗
ivar_4_inv t Ψ Ξ (pool_context pool) ∗
ivar_4_producer t ∗
▷ Ψ v ∗
▷ □ Ξ v
}}}
future٠set ctx t v
{{{
RET ();
pool_context pool ctx scope ∗
finished t
}}}.
Lemma future٠async𑁒spec Ψ Ξ pool ctx scope task :
{{{
pool_context pool ctx scope ∗
( ∀ ctx scope,
pool_context pool ctx scope -∗
WP task ctx {{ v,
pool_context pool ctx scope ∗
▷ Ψ v ∗
▷ □ Ξ v
}}
)
}}}
future٠async ctx task
{{{
t
, RET t;
pool_context pool ctx scope ∗
future_inv pool t Ψ Ξ ∗
future_consumer t Ψ
}}}.
Lemma future٠wait𑁒spec pool ctx scope t Ψ Ξ :
{{{
pool_context pool ctx scope ∗
future_inv pool t Ψ Ξ
}}}
future٠wait ctx t
{{{
v
, RET v;
£ 2 ∗
pool_context pool ctx scope ∗
future_result t v
}}}.
Lemma future٠iter𑁒spec P pool ctx scope t Ψ Ξ task :
{{{
pool_context pool ctx scope ∗
future_inv pool t Ψ Ξ ∗
( ∀ ctx scope v,
pool_context pool ctx scope -∗
future_result t v -∗
WP task ctx v {{ res,
⌜res = ()%V⌝ ∗
pool_context pool ctx scope ∗
▷ □ P
}}
)
}}}
future٠iter ctx t task
{{{
RET ();
pool_context pool ctx scope ∗
future_obligation pool P
}}}.
Lemma future٠map𑁒spec {pool ctx scope t1 Ψ1 Ξ1} Ψ2 Ξ2 task :
{{{
pool_context pool ctx scope ∗
future_inv pool t1 Ψ1 Ξ1 ∗
( ∀ ctx scope v1,
pool_context pool ctx scope -∗
future_result t1 v1 -∗
WP task ctx v1 {{ v2,
pool_context pool ctx scope ∗
▷ Ψ2 v2 ∗
▷ □ Ξ2 v2
}}
)
}}}
future٠map ctx t1 task
{{{
t2
, RET t2;
pool_context pool ctx scope ∗
future_inv pool t2 Ψ2 Ξ2 ∗
future_consumer t2 Ψ2
}}}.
End future_G.
From zoo_parabs Require
future__opaque.
#[global] Opaque future_inv.
#[global] Opaque future_obligation.
#[global] Opaque future_consumer.
#[global] Opaque future_result.