Library zoo_std.ivar_4
Require Import zoo.prelude.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.saved_prop.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_std.ivar_4__code.
Require Import zoo_std.ivar_4__types.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type v t ctx waiter : val.
Implicit Type waiters : list val.
Implicit Type ω : gname.
Implicit Type ωs : list gname.
Class Ivar4G Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ivar_4۰G۰ivar_3۰G :: Ivar3G Σ gname
; #[local] ivar_4۰G۰saved_prop۰G :: SavedPropG Σ
}.
Definition ivar_4۰Σ :=
#[ivar_3۰Σ gname
; saved_prop۰Σ
].
#[global] Instance subGｰivar_4۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ivar_4۰Σ Σ →
Ivar4G Σ.
Section ivar_4۰G.
Context `{ivar_4۰G : Ivar4G Σ}.
Context `{context_name : Type}.
Implicit Type 𝑐𝑡𝑥 : context_name.
Implicit Type P : iProp Σ.
Implicit Type Ps : list $ iProp Σ.
Implicit Type Ψ Χ Ξ : val → iProp Σ.
Implicit Type Γ : val → context_name → iProp Σ.
#[local] Definition waiter۰model₁ Γ t waiter P : iProp Σ :=
∀ ctx 𝑐𝑡𝑥 v,
Γ ctx 𝑐𝑡𝑥 -∗
ivar_3۰result t v -∗
WP waiter ctx v {{ res,
⌜res = ()%V⌝ ∗
Γ ctx 𝑐𝑡𝑥 ∗
▷ □ P
}}.
#[local] Definition waiter۰model₂ Γ t waiter ω : iProp Σ :=
∃ P,
saved_prop ω P ∗
waiter۰model₁ Γ t waiter P.
Definition ivar_4۰inv t Ψ Ξ Γ :=
ivar_3۰inv t Ψ Ξ (waiter۰model₂ Γ).
Definition ivar_4۰producer :=
ivar_3۰producer.
Definition ivar_4۰consumer :=
ivar_3۰consumer.
Definition ivar_4۰result :=
ivar_3۰result.
Definition ivar_4۰resolved t : iProp Σ :=
∃ v,
ivar_4۰result t v.
Definition ivar_4۰waiters t waiters Ps : iProp Σ :=
∃ ωs,
ivar_3۰waiters t waiters ωs ∗
[∗ list] ω; P ∈ ωs; Ps, saved_prop ω P.
#[local] Instance : CustomIpat "waiters" :=
" ( %ωs & #Hwaiters & #Hωs ) ".
Definition ivar_4۰waiter t waiter P : iProp Σ :=
∃ ω,
ivar_3۰waiter t waiter ω ∗
saved_prop ω P.
#[local] Instance : CustomIpat "waiter" :=
" ( %ω & #Hwaiter & #Hω ) ".
#[global] Instance ivar_4۰invｰcontractive t n :
Proper (
(pointwise_relation _ $ dist_later n) ==>
(pointwise_relation _ $ dist_later n) ==>
(pointwise_relation _ $ pointwise_relation _ $ (≡{n}≡)) ==>
(≡{n}≡)
) (ivar_4۰inv t).
#[global] Instance ivar_4۰invｰproper t :
Proper (
(pointwise_relation _ (≡)) ==>
(pointwise_relation _ (≡)) ==>
(pointwise_relation _ $ pointwise_relation _ (≡)) ==>
(≡)
) (ivar_4۰inv t).
#[global] Instance ivar_4۰consumerｰcontractive t n :
Proper (
(pointwise_relation _ $ dist_later n) ==>
(≡{n}≡)
) (ivar_4۰consumer t).
#[global] Instance ivar_4۰consumerｰproper t :
Proper (
(pointwise_relation _ (≡)) ==>
(≡)
) (ivar_4۰consumer t).
#[global] Instance ivar_4۰producerｰtimeless t :
Timeless (ivar_4۰producer t).
#[global] Instance ivar_4۰resultｰtimeless t v :
Timeless (ivar_4۰result t v).
#[global] Instance ivar_4۰invｰpersistent t Ψ Ξ Γ :
Persistent (ivar_4۰inv t Ψ Ξ Γ).
#[global] Instance ivar_4۰resultｰpersistent t v :
Persistent (ivar_4۰result t v).
#[global] Instance ivar_4۰waitersｰpersistent t waiters Ps :
Persistent (ivar_4۰waiters t waiters Ps).
#[global] Instance ivar_4۰waiterｰpersistent t waiter P :
Persistent (ivar_4۰waiter t waiter P).
Lemma ivar_4۰producerｰexclusive t :
ivar_4۰producer t -∗
ivar_4۰producer t -∗
False.
Lemma ivar_4۰consumerｰwand {t Ψ Ξ Γ Χ1} Χ2 :
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰consumer t Χ1 -∗
(∀ v, Χ1 v -∗ Χ2 v) ={⊤}=∗
ivar_4۰consumer t Χ2.
Lemma ivar_4۰consumerｰdivide {t Ψ Ξ Γ} Χs :
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰consumer t (λ v, [∗ list] Χ ∈ Χs, Χ v) ={⊤}=∗
[∗ list] Χ ∈ Χs, ivar_4۰consumer t Χ.
Lemma ivar_4۰consumerｰsplit {t Ψ Ξ Γ} Χ1 Χ2 :
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰consumer t (λ v, Χ1 v ∗ Χ2 v) ={⊤}=∗
ivar_4۰consumer t Χ1 ∗
ivar_4۰consumer t Χ2.
Lemma ivar_4۰resultｰagree t v1 v2 :
ivar_4۰result t v1 -∗
ivar_4۰result t v2 -∗
⌜v1 = v2⌝.
Lemma ivar_4ｰproducerｰresult t v :
ivar_4۰producer t -∗
ivar_4۰result t v -∗
False.
Lemma ivar_4ｰinvｰresult t Ψ Ξ Γ v :
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰result t v ={⊤}=∗
▷ □ Ξ v.
Lemma ivar_4ｰinvｰresult' t Ψ Ξ Γ v :
£ 1 -∗
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰result t v ={⊤}=∗
□ Ξ v.
Lemma ivar_4ｰinvｰresultｰconsumer t Ψ Ξ Γ v Χ :
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰result t v -∗
ivar_4۰consumer t Χ ={⊤}=∗
▷^2 Χ v ∗
▷ □ Ξ v.
Lemma ivar_4ｰinvｰresultｰconsumer' t Ψ Ξ Γ v Χ :
£ 2 -∗
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰result t v -∗
ivar_4۰consumer t Χ ={⊤}=∗
Χ v ∗
□ Ξ v.
Lemma ivar_4۰waiterｰvalid t waiters Ps waiter P :
ivar_4۰waiters t waiters Ps -∗
ivar_4۰waiter t waiter P -∗
∃ i P_,
⌜waiters !! i = Some waiter⌝ ∗
⌜Ps !! i = Some P_⌝ ∗
▷ (P ≡ P_).
Lemma ivar_4٠createｰspec Ψ Ξ Γ :
{{{
True
}}}
ivar_4٠create ()
{{{
t
, RET t;
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰producer t ∗
ivar_4۰consumer t Ψ
}}}.
Lemma ivar_4٠makeｰspec Ψ Ξ Γ v :
{{{
▷ Ψ v ∗
▷ □ Ξ v
}}}
ivar_4٠make v
{{{
t
, RET t;
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰consumer t Ψ ∗
ivar_4۰result t v ∗
ivar_4۰waiters t [] []
}}}.
Lemma ivar_4٠is_unsetｰspec t Ψ Ξ Γ :
{{{
ivar_4۰inv t Ψ Ξ Γ
}}}
ivar_4٠is_unset t
{{{
b
, RET #b;
if b then
True
else
£ 2 ∗
ivar_4۰resolved t
}}}.
Lemma ivar_4٠is_unsetｰspecｰresult t Ψ Ξ Γ v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰result t v
}}}
ivar_4٠is_unset t
{{{
RET false;
£ 2
}}}.
Lemma ivar_4٠is_setｰspec t Ψ Ξ Γ :
{{{
ivar_4۰inv t Ψ Ξ Γ
}}}
ivar_4٠is_set t
{{{
b
, RET #b;
if b then
£ 2 ∗
ivar_4۰resolved t
else
True
}}}.
Lemma ivar_4٠is_setｰspecｰresult t Ψ Ξ Γ v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰result t v
}}}
ivar_4٠is_set t
{{{
RET true;
£ 2
}}}.
Lemma ivar_4٠try_getｰspec t Ψ Ξ Γ :
{{{
ivar_4۰inv t Ψ Ξ Γ
}}}
ivar_4٠try_get t
{{{
o
, RET o;
if o is Some v then
£ 2 ∗
ivar_4۰result t v
else
True
}}}.
Lemma ivar_4٠try_getｰspecｰresult t Ψ Ξ Γ v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰result t v
}}}
ivar_4٠try_get t
{{{
RET Some v;
£ 2
}}}.
Lemma ivar_4٠getｰspec t Ψ Ξ Γ v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰result t v
}}}
ivar_4٠get t
{{{
RET v;
£ 2
}}}.
Lemma ivar_4٠waitｰspec P Q t Ψ Ξ Γ waiter :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
Q ∗
( ∀ ctx 𝑐𝑡𝑥 v,
Q -∗
Γ ctx 𝑐𝑡𝑥 -∗
ivar_3۰result t v -∗
WP waiter ctx v {{ res,
⌜res = ()%V⌝ ∗
Γ ctx 𝑐𝑡𝑥 ∗
▷ □ P
}}
)
}}}
ivar_4٠wait t waiter
{{{
o
, RET o;
if o is Some v then
£ 2 ∗
ivar_4۰result t v ∗
Q
else
ivar_4۰waiter t waiter P
}}}.
Lemma ivar_4٠setｰspec t Ψ Ξ Γ v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰producer t ∗
▷ Ψ v ∗
▷ □ Ξ v
}}}
ivar_4٠set t v
{{{
waiters Ps
, RET list۰to_val waiters;
ivar_4۰result t v ∗
ivar_4۰waiters t waiters Ps ∗
[∗ list] waiter; P ∈ waiters; Ps,
∀ ctx 𝑐𝑡𝑥 v,
Γ ctx 𝑐𝑡𝑥 -∗
ivar_3۰result t v -∗
WP waiter ctx v {{ res,
⌜res = ()%V⌝ ∗
Γ ctx 𝑐𝑡𝑥 ∗
▷ □ P
}}
}}}.
Lemma ivar_4٠notifyｰspec {t Ψ Ξ Γ ctx} 𝑐𝑡𝑥 v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰producer t ∗
Γ ctx 𝑐𝑡𝑥 ∗
▷ Ψ v ∗
▷ □ Ξ v
}}}
ivar_4٠notify t ctx v
{{{
waiters Ps
, RET ();
ivar_4۰result t v ∗
ivar_4۰waiters t waiters Ps ∗
Γ ctx 𝑐𝑡𝑥 ∗
[∗ list] P ∈ Ps, □ P
}}}.
End ivar_4۰G.
Require zoo_std.ivar_4__opaque.
#[global] Opaque ivar_4۰inv.
#[global] Opaque ivar_4۰producer.
#[global] Opaque ivar_4۰consumer.
#[global] Opaque ivar_4۰result.
#[global] Opaque ivar_4۰waiter.
#[global] Opaque ivar_4۰waiters.
Require Import zoo.iris.bi.big_op.
Require Import zoo.iris.base_logic.lib.saved_prop.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_std.ivar_4__code.
Require Import zoo_std.ivar_4__types.
Require Import zoo.options.
Implicit Type b : bool.
Implicit Type v t ctx waiter : val.
Implicit Type waiters : list val.
Implicit Type ω : gname.
Implicit Type ωs : list gname.
Class Ivar4G Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] ivar_4۰G۰ivar_3۰G :: Ivar3G Σ gname
; #[local] ivar_4۰G۰saved_prop۰G :: SavedPropG Σ
}.
Definition ivar_4۰Σ :=
#[ivar_3۰Σ gname
; saved_prop۰Σ
].
#[global] Instance subGｰivar_4۰Σ Σ `{zoo۰G : !ZooG Σ} :
subG ivar_4۰Σ Σ →
Ivar4G Σ.
Section ivar_4۰G.
Context `{ivar_4۰G : Ivar4G Σ}.
Context `{context_name : Type}.
Implicit Type 𝑐𝑡𝑥 : context_name.
Implicit Type P : iProp Σ.
Implicit Type Ps : list $ iProp Σ.
Implicit Type Ψ Χ Ξ : val → iProp Σ.
Implicit Type Γ : val → context_name → iProp Σ.
#[local] Definition waiter۰model₁ Γ t waiter P : iProp Σ :=
∀ ctx 𝑐𝑡𝑥 v,
Γ ctx 𝑐𝑡𝑥 -∗
ivar_3۰result t v -∗
WP waiter ctx v {{ res,
⌜res = ()%V⌝ ∗
Γ ctx 𝑐𝑡𝑥 ∗
▷ □ P
}}.
#[local] Definition waiter۰model₂ Γ t waiter ω : iProp Σ :=
∃ P,
saved_prop ω P ∗
waiter۰model₁ Γ t waiter P.
Definition ivar_4۰inv t Ψ Ξ Γ :=
ivar_3۰inv t Ψ Ξ (waiter۰model₂ Γ).
Definition ivar_4۰producer :=
ivar_3۰producer.
Definition ivar_4۰consumer :=
ivar_3۰consumer.
Definition ivar_4۰result :=
ivar_3۰result.
Definition ivar_4۰resolved t : iProp Σ :=
∃ v,
ivar_4۰result t v.
Definition ivar_4۰waiters t waiters Ps : iProp Σ :=
∃ ωs,
ivar_3۰waiters t waiters ωs ∗
[∗ list] ω; P ∈ ωs; Ps, saved_prop ω P.
#[local] Instance : CustomIpat "waiters" :=
" ( %ωs & #Hwaiters & #Hωs ) ".
Definition ivar_4۰waiter t waiter P : iProp Σ :=
∃ ω,
ivar_3۰waiter t waiter ω ∗
saved_prop ω P.
#[local] Instance : CustomIpat "waiter" :=
" ( %ω & #Hwaiter & #Hω ) ".
#[global] Instance ivar_4۰invｰcontractive t n :
Proper (
(pointwise_relation _ $ dist_later n) ==>
(pointwise_relation _ $ dist_later n) ==>
(pointwise_relation _ $ pointwise_relation _ $ (≡{n}≡)) ==>
(≡{n}≡)
) (ivar_4۰inv t).
#[global] Instance ivar_4۰invｰproper t :
Proper (
(pointwise_relation _ (≡)) ==>
(pointwise_relation _ (≡)) ==>
(pointwise_relation _ $ pointwise_relation _ (≡)) ==>
(≡)
) (ivar_4۰inv t).
#[global] Instance ivar_4۰consumerｰcontractive t n :
Proper (
(pointwise_relation _ $ dist_later n) ==>
(≡{n}≡)
) (ivar_4۰consumer t).
#[global] Instance ivar_4۰consumerｰproper t :
Proper (
(pointwise_relation _ (≡)) ==>
(≡)
) (ivar_4۰consumer t).
#[global] Instance ivar_4۰producerｰtimeless t :
Timeless (ivar_4۰producer t).
#[global] Instance ivar_4۰resultｰtimeless t v :
Timeless (ivar_4۰result t v).
#[global] Instance ivar_4۰invｰpersistent t Ψ Ξ Γ :
Persistent (ivar_4۰inv t Ψ Ξ Γ).
#[global] Instance ivar_4۰resultｰpersistent t v :
Persistent (ivar_4۰result t v).
#[global] Instance ivar_4۰waitersｰpersistent t waiters Ps :
Persistent (ivar_4۰waiters t waiters Ps).
#[global] Instance ivar_4۰waiterｰpersistent t waiter P :
Persistent (ivar_4۰waiter t waiter P).
Lemma ivar_4۰producerｰexclusive t :
ivar_4۰producer t -∗
ivar_4۰producer t -∗
False.
Lemma ivar_4۰consumerｰwand {t Ψ Ξ Γ Χ1} Χ2 :
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰consumer t Χ1 -∗
(∀ v, Χ1 v -∗ Χ2 v) ={⊤}=∗
ivar_4۰consumer t Χ2.
Lemma ivar_4۰consumerｰdivide {t Ψ Ξ Γ} Χs :
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰consumer t (λ v, [∗ list] Χ ∈ Χs, Χ v) ={⊤}=∗
[∗ list] Χ ∈ Χs, ivar_4۰consumer t Χ.
Lemma ivar_4۰consumerｰsplit {t Ψ Ξ Γ} Χ1 Χ2 :
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰consumer t (λ v, Χ1 v ∗ Χ2 v) ={⊤}=∗
ivar_4۰consumer t Χ1 ∗
ivar_4۰consumer t Χ2.
Lemma ivar_4۰resultｰagree t v1 v2 :
ivar_4۰result t v1 -∗
ivar_4۰result t v2 -∗
⌜v1 = v2⌝.
Lemma ivar_4ｰproducerｰresult t v :
ivar_4۰producer t -∗
ivar_4۰result t v -∗
False.
Lemma ivar_4ｰinvｰresult t Ψ Ξ Γ v :
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰result t v ={⊤}=∗
▷ □ Ξ v.
Lemma ivar_4ｰinvｰresult' t Ψ Ξ Γ v :
£ 1 -∗
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰result t v ={⊤}=∗
□ Ξ v.
Lemma ivar_4ｰinvｰresultｰconsumer t Ψ Ξ Γ v Χ :
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰result t v -∗
ivar_4۰consumer t Χ ={⊤}=∗
▷^2 Χ v ∗
▷ □ Ξ v.
Lemma ivar_4ｰinvｰresultｰconsumer' t Ψ Ξ Γ v Χ :
£ 2 -∗
ivar_4۰inv t Ψ Ξ Γ -∗
ivar_4۰result t v -∗
ivar_4۰consumer t Χ ={⊤}=∗
Χ v ∗
□ Ξ v.
Lemma ivar_4۰waiterｰvalid t waiters Ps waiter P :
ivar_4۰waiters t waiters Ps -∗
ivar_4۰waiter t waiter P -∗
∃ i P_,
⌜waiters !! i = Some waiter⌝ ∗
⌜Ps !! i = Some P_⌝ ∗
▷ (P ≡ P_).
Lemma ivar_4٠createｰspec Ψ Ξ Γ :
{{{
True
}}}
ivar_4٠create ()
{{{
t
, RET t;
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰producer t ∗
ivar_4۰consumer t Ψ
}}}.
Lemma ivar_4٠makeｰspec Ψ Ξ Γ v :
{{{
▷ Ψ v ∗
▷ □ Ξ v
}}}
ivar_4٠make v
{{{
t
, RET t;
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰consumer t Ψ ∗
ivar_4۰result t v ∗
ivar_4۰waiters t [] []
}}}.
Lemma ivar_4٠is_unsetｰspec t Ψ Ξ Γ :
{{{
ivar_4۰inv t Ψ Ξ Γ
}}}
ivar_4٠is_unset t
{{{
b
, RET #b;
if b then
True
else
£ 2 ∗
ivar_4۰resolved t
}}}.
Lemma ivar_4٠is_unsetｰspecｰresult t Ψ Ξ Γ v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰result t v
}}}
ivar_4٠is_unset t
{{{
RET false;
£ 2
}}}.
Lemma ivar_4٠is_setｰspec t Ψ Ξ Γ :
{{{
ivar_4۰inv t Ψ Ξ Γ
}}}
ivar_4٠is_set t
{{{
b
, RET #b;
if b then
£ 2 ∗
ivar_4۰resolved t
else
True
}}}.
Lemma ivar_4٠is_setｰspecｰresult t Ψ Ξ Γ v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰result t v
}}}
ivar_4٠is_set t
{{{
RET true;
£ 2
}}}.
Lemma ivar_4٠try_getｰspec t Ψ Ξ Γ :
{{{
ivar_4۰inv t Ψ Ξ Γ
}}}
ivar_4٠try_get t
{{{
o
, RET o;
if o is Some v then
£ 2 ∗
ivar_4۰result t v
else
True
}}}.
Lemma ivar_4٠try_getｰspecｰresult t Ψ Ξ Γ v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰result t v
}}}
ivar_4٠try_get t
{{{
RET Some v;
£ 2
}}}.
Lemma ivar_4٠getｰspec t Ψ Ξ Γ v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰result t v
}}}
ivar_4٠get t
{{{
RET v;
£ 2
}}}.
Lemma ivar_4٠waitｰspec P Q t Ψ Ξ Γ waiter :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
Q ∗
( ∀ ctx 𝑐𝑡𝑥 v,
Q -∗
Γ ctx 𝑐𝑡𝑥 -∗
ivar_3۰result t v -∗
WP waiter ctx v {{ res,
⌜res = ()%V⌝ ∗
Γ ctx 𝑐𝑡𝑥 ∗
▷ □ P
}}
)
}}}
ivar_4٠wait t waiter
{{{
o
, RET o;
if o is Some v then
£ 2 ∗
ivar_4۰result t v ∗
Q
else
ivar_4۰waiter t waiter P
}}}.
Lemma ivar_4٠setｰspec t Ψ Ξ Γ v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰producer t ∗
▷ Ψ v ∗
▷ □ Ξ v
}}}
ivar_4٠set t v
{{{
waiters Ps
, RET list۰to_val waiters;
ivar_4۰result t v ∗
ivar_4۰waiters t waiters Ps ∗
[∗ list] waiter; P ∈ waiters; Ps,
∀ ctx 𝑐𝑡𝑥 v,
Γ ctx 𝑐𝑡𝑥 -∗
ivar_3۰result t v -∗
WP waiter ctx v {{ res,
⌜res = ()%V⌝ ∗
Γ ctx 𝑐𝑡𝑥 ∗
▷ □ P
}}
}}}.
Lemma ivar_4٠notifyｰspec {t Ψ Ξ Γ ctx} 𝑐𝑡𝑥 v :
{{{
ivar_4۰inv t Ψ Ξ Γ ∗
ivar_4۰producer t ∗
Γ ctx 𝑐𝑡𝑥 ∗
▷ Ψ v ∗
▷ □ Ξ v
}}}
ivar_4٠notify t ctx v
{{{
waiters Ps
, RET ();
ivar_4۰result t v ∗
ivar_4۰waiters t waiters Ps ∗
Γ ctx 𝑐𝑡𝑥 ∗
[∗ list] P ∈ Ps, □ P
}}}.
End ivar_4۰G.
Require zoo_std.ivar_4__opaque.
#[global] Opaque ivar_4۰inv.
#[global] Opaque ivar_4۰producer.
#[global] Opaque ivar_4۰consumer.
#[global] Opaque ivar_4۰result.
#[global] Opaque ivar_4۰waiter.
#[global] Opaque ivar_4۰waiters.