Library zoo_eio.rcfd
From zoo Require Import
prelude.
From zoo.common Require Import
countable
gmultiset
relations.
From zoo.iris.base_logic Require Import
lib.auth_gmultiset
lib.auth_mono.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
spsc_waiter.
From unix Require Import
unix.
From zoo_eio Require Export
base
rcfd__code.
From zoo_eio Require Import
rcfd__types.
From zoo Require Import
options.
Implicit Types b owned closing : bool.
Implicit Types ops : Z.
Implicit Types q stock : Qp.
Implicit Types qs : gmultiset Qp.
Implicit Types l open : location.
Implicit Types t v v_state fd fn : val.
Implicit Types o : option val.
Record metadata :=
{ metadata_fd : val
; metadata_open : block_id
; metadata_owned : bool
; metadata_tokens : gname
; metadata_lstate : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
Variant state :=
| Open
| Closing fn.
Implicit Types state : state.
#[local] Instance state_inhabited : Inhabited state :=
populate Open.
#[local] Instance state_eq_dec : EqDecision state :=
ltac:(solve_decision).
#[local] Definition state_to_val γ state :=
match state with
| Open ⇒
‘Open@γ.(metadata_open)[ γ.(metadata_fd) ]
| Closing fn ⇒
‘Closing[ fn ]
end%V.
#[local] Arguments state_to_val _ !_ / : assert.
Variant lstate :=
| LOpen
| LClosingUsers
| LClosingNoUsers.
Implicit Types lstate : lstate.
#[local] Definition lstate_measure lstate :=
match lstate with
| LOpen ⇒
0
| LClosingUsers ⇒
1
| LClosingNoUsers ⇒
2
end.
#[global] Instance lstate_inhabited : Inhabited lstate :=
populate LOpen.
#[global] Instance lstate_eq_dec : EqDecision lstate :=
ltac:(solve_decision).
Variant lstep : relation lstate :=
| lstep_close_users :
lstep LOpen LClosingUsers
| lstep_close_no_users :
lstep LClosingUsers LClosingNoUsers.
#[local] Hint Constructors lstep : core.
#[local] Lemma lstep_measure lstate1 lstate2 :
lstep lstate1 lstate2 →
lstate_measure lstate1 < lstate_measure lstate2.
#[local] Lemma lstep_tc_measure lstate1 lstate2 :
tc lstep lstate1 lstate2 →
lstate_measure lstate1 < lstate_measure lstate2.
#[local] Lemma lstep_rtc_measure lstate1 lstate2 :
rtc lstep lstate1 lstate2 →
lstate_measure lstate1 ≤ lstate_measure lstate2.
#[local] Instance lsteps_antisymm :
AntiSymm (=) (rtc lstep).
Class RcfdG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] rcfd_G_spsc_waiter_G :: SpscWaiterG Σ
; #[local] rcfd_G_tokens_G :: AuthGmultisetG Σ Qp
; #[local] rcfd_G_lstate_G :: AuthMonoG Σ (A := leibnizO lstate) lstep
}.
Definition rcfd_Σ :=
#[spsc_waiter_Σ
; auth_gmultiset_Σ Qp
; auth_mono_Σ (A := leibnizO lstate) lstep
].
#[global] Instance subG_rcfd_Σ `{zoo_G : !ZooG Σ} :
subG rcfd_Σ Σ →
RcfdG Σ.
Section rcfd_G.
Context `{rcfd_G : RcfdG Σ}.
Implicit Types Ψ : frac → iProp Σ.
#[local] Definition tokens_auth' γ_tokens Ψ ops : iProp Σ :=
∃ stock qs,
⌜ops = size qs⌝ ∗
⌜set_fold Qp.add stock qs = 1%Qp⌝ ∗
auth_gmultiset_auth γ_tokens (DfracOwn 1) qs ∗
Ψ stock.
#[local] Definition tokens_auth γ :=
tokens_auth' γ.(metadata_tokens).
#[local] Instance : CustomIpat "tokens_auth" :=
" ( %stock & %qs & {{lazy}%Hops;->} & %Hqs & Hauth & HΨ_stock ) ".
#[local] Definition tokens_frag γ q :=
auth_gmultiset_frag γ.(metadata_tokens) {[+q+]}.
#[local] Definition lstate_auth_frac owned lstate :=
match lstate with
| LOpen ⇒
if owned then 1/4 else 1
| _ ⇒
1
end%Qp.
#[local] Definition lstate_auth' γ_lstate owned lstate :=
auth_mono_auth _ γ_lstate (DfracOwn $ lstate_auth_frac owned lstate) lstate.
#[local] Definition lstate_auth γ :=
lstate_auth' γ.(metadata_lstate) γ.(metadata_owned).
#[local] Definition lstate_lb γ lstate :=
auth_mono_lb _ γ.(metadata_lstate) lstate.
#[local] Definition owner' γ_lstate :=
auth_mono_auth _ γ_lstate (DfracOwn (3/4)%Qp) LOpen.
#[local] Definition owner γ :=
owner' γ.(metadata_lstate).
#[local] Definition inv_lstate_open γ Ψ state ops : iProp Σ :=
tokens_auth γ Ψ ops ∗
⌜state = Open⌝.
#[local] Instance : CustomIpat "inv_lstate_open" :=
" ( Htokens_auth & {%H{eq};->} ) ".
#[local] Definition inv_lstate_closing_users γ Ψ state ops : iProp Σ :=
∃ fn,
tokens_auth γ Ψ ops ∗
⌜state = Closing fn⌝ ∗
⌜0 < ops⌝%Z ∗
(Ψ 1%Qp -∗ WP fn () {{ itype_unit }}).
#[local] Instance : CustomIpat "inv_lstate_closing_users" :=
" ( %fn{} & Htokens_auth & {%H{eq};->} & %Hops{} & Hfn{} ) ".
#[local] Definition inv_lstate_closing_no_users state : iProp Σ :=
∃ fn,
⌜state = Closing fn⌝ ∗
WP fn () {{ itype_unit }}.
#[local] Instance : CustomIpat "inv_lstate_closing_no_users" :=
" ( %fn{} & {%H{eq};->} & Hfn{} ) ".
#[local] Definition inv_lstate γ Ψ state lstate ops :=
match lstate with
| LOpen ⇒
inv_lstate_open γ Ψ state ops
| LClosingUsers ⇒
inv_lstate_closing_users γ Ψ state ops
| LClosingNoUsers ⇒
inv_lstate_closing_no_users state
end.
#[local] Definition inv_inner l γ Ψ : iProp Σ :=
∃ state lstate ops,
l.[ops] ↦ #ops ∗
l.[state] ↦ state_to_val γ state ∗
lstate_auth γ lstate ∗
inv_lstate γ Ψ state lstate ops.
#[local] Instance : CustomIpat "inv_inner" :=
" ( %state{} & %lstate{} & %ops{} & Hl_ops & Hl_state & Hlstate_auth & Hlstate ) ".
#[local] Definition inv' l γ Ψ :=
inv nroot (inv_inner l γ Ψ).
Definition rcfd_inv t owned fd Ψ : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
⌜owned = γ.(metadata_owned)⌝ ∗
⌜fd = γ.(metadata_fd)⌝ ∗
meta l nroot γ ∗
inv' l γ Ψ.
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & -> & -> & -> & #Hmeta & #Hinv ) ".
Definition rcfd_owner t : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
owner γ.
#[local] Instance : CustomIpat "owner" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Howner{_{}} ) ".
Definition rcfd_closing t : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
lstate_lb γ LClosingUsers.
#[local] Instance : CustomIpat "closing" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & #Hlstate_lb{_{}} ) ".
#[local] Instance tokens_auth'_ne γ_tokens n :
Proper (
(pointwise_relation _ (≡{n}≡)) ==>
(=) ==>
(≡{n}≡)
) (tokens_auth' γ_tokens).
#[local] Instance tokens_auth'_proper γ_tokens :
Proper (
(pointwise_relation _ (≡)) ==>
(=) ==>
(≡)
) (tokens_auth' γ_tokens).
#[global] Instance rcfd_inv_contractive t owned fd n :
Proper (
(pointwise_relation _ (dist_later n)) ==>
(≡{n}≡)
) (rcfd_inv t owned fd).
#[global] Instance rcfd_inv_proper t owned fd :
Proper (
(pointwise_relation _ (≡)) ==>
(≡)
) (rcfd_inv t owned fd).
#[global] Instance rcfd_owner_timeless t :
Timeless (rcfd_owner t).
#[global] Instance rcfd_closing_timeless t :
Timeless (rcfd_closing t).
#[global] Instance rcfd_inv_persistent t owned fd Ψ :
Persistent (rcfd_inv t owned fd Ψ).
#[global] Instance rcfd_closing_persistent t :
Persistent (rcfd_closing t).
#[local] Lemma tokens_alloc Ψ :
Ψ 1%Qp ⊢ |==>
∃ γ_tokens,
tokens_auth' γ_tokens Ψ 0.
#[local] Lemma tokens_auth_valid γ Ψ ops :
tokens_auth γ Ψ ops ⊢
⌜(0 ≤ ops)%Z⌝.
#[local] Lemma tokens_auth_consume γ Ψ :
tokens_auth γ Ψ 0 ⊢
Ψ 1%Qp.
#[local] Lemma tokens_update_alloc γ Ψ `{!Fractional Ψ} ops :
tokens_auth γ Ψ ops ⊢ |==>
∃ q,
tokens_auth γ Ψ (ops + 1) ∗
tokens_frag γ q ∗
Ψ q.
#[local] Lemma tokens_update_dealloc γ Ψ `{!Fractional Ψ} ops q :
tokens_auth γ Ψ ops -∗
tokens_frag γ q -∗
Ψ q ==∗
tokens_auth γ Ψ (ops - 1).
#[local] Lemma lstate_owner_alloc owned :
⊢ |==>
∃ γ_lstate,
lstate_auth' γ_lstate owned LOpen ∗
if owned then
owner' γ_lstate
else
True.
#[local] Lemma lstate_lb_get γ lstate :
lstate_auth γ lstate ⊢
lstate_lb γ lstate.
#[local] Lemma lstate_lb_mono {γ lstate} lstate' :
lstep lstate' lstate →
lstate_lb γ lstate ⊢
lstate_lb γ lstate'.
#[local] Lemma lstate_valid γ lstate lstate' :
lstate_auth γ lstate -∗
lstate_lb γ lstate' -∗
⌜rtc lstep lstate' lstate⌝.
#[local] Lemma lstate_valid_closing_users γ lstate :
lstate_auth γ lstate -∗
lstate_lb γ LClosingUsers -∗
⌜lstate ≠ LOpen⌝.
#[local] Lemma lstate_valid_closing_users' γ lstate :
lstate_auth γ lstate -∗
lstate_lb γ LClosingUsers -∗
⌜lstate = LClosingUsers ∨ lstate = LClosingNoUsers⌝.
#[local] Lemma lstate_valid_closing_no_users γ lstate :
lstate_auth γ lstate -∗
lstate_lb γ LClosingNoUsers -∗
⌜lstate = LClosingNoUsers⌝.
#[local] Lemma lstate_update_close_users γ :
lstate_auth γ LOpen -∗
(if γ.(metadata_owned) then owner γ else True) ==∗
lstate_auth γ LClosingUsers.
#[local] Lemma lstate_update_close_no_users γ :
lstate_auth γ LClosingUsers ⊢ |==>
lstate_auth γ LClosingNoUsers.
#[local] Lemma owner_exclusive γ :
owner γ -∗
owner γ -∗
False.
#[local] Lemma owner_lstate_auth γ lstate :
owner γ -∗
lstate_auth γ lstate -∗
⌜lstate = LOpen⌝.
#[local] Lemma owner_lstate_lb γ :
owner γ -∗
lstate_lb γ LClosingUsers -∗
False.
Opaque tokens_auth'.
#[local] Lemma rcfd_owner_elim l γ :
meta l nroot γ -∗
rcfd_owner #l -∗
owner γ.
#[local] Lemma rcfd_owner_elim' l γ b :
meta l nroot γ -∗
( if b then
rcfd_owner #l
else
True
) -∗
if b then
owner γ
else
True.
Lemma rcfd_owner_exclusive t :
rcfd_owner t -∗
rcfd_owner t -∗
False.
Lemma rcfd_owner_closing t :
rcfd_owner t -∗
rcfd_closing t -∗
False.
#[local] Lemma rcfd_closing_elim l γ :
meta l nroot γ -∗
rcfd_closing #l -∗
lstate_lb γ LClosingUsers.
#[local] Lemma rcfd_closing_elim' l γ b P :
meta l nroot γ -∗
( if b then
rcfd_closing #l
else
P
) -∗
if b then
lstate_lb γ LClosingUsers
else
P.
#[local] Lemma inv_lstate_Open γ Ψ lstate ops :
inv_lstate γ Ψ Open lstate ops ⊢
⌜lstate = LOpen⌝.
#[local] Lemma inv_lstate_Closing γ Ψ state lstate ops :
state ≠ Open →
inv_lstate γ Ψ state lstate ops -∗
lstate_auth γ lstate -∗
∃ fn,
⌜state = Closing fn⌝ ∗
⌜lstate ≠ LOpen ⌝ ∗
lstate_lb γ LClosingUsers.
#[local] Lemma inv_lstate_LClosing γ Ψ state lstate ops :
lstate ≠ LOpen →
inv_lstate γ Ψ state lstate ops -∗
lstate_auth γ lstate -∗
∃ fn,
⌜state = Closing fn⌝ ∗
lstate_lb γ LClosingUsers.
Lemma rcfd٠make𑁒spec owned Ψ fd :
{{{
Ψ 1%Qp
}}}
rcfd٠make fd
{{{
t
, RET t;
rcfd_inv t owned fd Ψ ∗
if owned then
rcfd_owner t
else
True
}}}.
#[local] Lemma rcfd٠finish𑁒spec l γ Ψ (close : val) :
{{{
inv' l γ Ψ ∗
lstate_lb γ LClosingUsers
}}}
rcfd٠finish #l close ’Closing[ close ]
{{{
RET ();
True
}}}.
#[local] Lemma rcfd٠put𑁒spec l γ Ψ `{!Fractional Ψ} :
{{{
inv' l γ Ψ ∗
( lstate_lb γ LClosingNoUsers
∨ ∃ q,
tokens_frag γ q ∗
Ψ q
)
}}}
rcfd٠put #l
{{{
RET ();
True
}}}.
Variant specification :=
| SpecOwner
| SpecClosing
| SpecNormal.
Implicit Types spec : specification.
#[local] Instance specification_eq_dec : EqDecision specification :=
ltac:(solve_decision).
#[local] Definition specification_pre_1 t spec : iProp Σ :=
match spec with
| SpecOwner ⇒
rcfd_owner t
| SpecClosing ⇒
rcfd_closing t
| SpecNormal ⇒
True
end.
#[local] Definition specification_pre_2 γ spec : iProp Σ :=
match spec with
| SpecOwner ⇒
owner γ
| SpecClosing ⇒
lstate_lb γ LClosingUsers
| SpecNormal ⇒
True
end.
#[local] Lemma specification_pre_1_2 l γ spec :
meta l nroot γ -∗
specification_pre_1 #l spec -∗
specification_pre_2 γ spec.
#[local] Lemma rcfd٠get𑁒spec_aux spec l γ Ψ `{HΨ : !Fractional Ψ} :
{{{
inv' l γ Ψ ∗
specification_pre_2 γ spec
}}}
rcfd٠get #l
{{{
o
, RET o;
match spec with
| SpecOwner ⇒
⌜o ≠ None⌝ ∗
owner γ
| SpecClosing ⇒
⌜o = None⌝
| SpecNormal ⇒
True
end ∗
match o with
| None ⇒
True
| Some fd_ ⇒
∃ q,
⌜fd_ = γ.(metadata_fd)⌝ ∗
tokens_frag γ q ∗
Ψ q
end
}}}.
#[local] Lemma rcfd٠get𑁒spec l γ Ψ `{HΨ : !Fractional Ψ} :
{{{
inv' l γ Ψ
}}}
rcfd٠get #l
{{{
o
, RET o;
match o with
| None ⇒
True
| Some fd_ ⇒
∃ q,
⌜fd_ = γ.(metadata_fd)⌝ ∗
tokens_frag γ q ∗
Ψ q
end
}}}.
#[local] Lemma rcfd٠get𑁒spec_owner l γ Ψ `{HΨ : !Fractional Ψ} :
{{{
inv' l γ Ψ ∗
owner γ
}}}
rcfd٠get #l
{{{
RET Some γ.(metadata_fd);
∃ q,
owner γ ∗
tokens_frag γ q ∗
Ψ q
}}}.
#[local] Lemma rcfd٠get𑁒spec_closing l γ Ψ `{HΨ : !Fractional Ψ} :
{{{
inv' l γ Ψ ∗
lstate_lb γ LClosingUsers
}}}
rcfd٠get #l
{{{
RET None;
True
}}}.
#[local] Lemma rcfd٠use𑁒spec_aux spec Χ t owned fd Ψ `{!Fractional Ψ} (closed open : val) :
{{{
rcfd_inv t owned fd Ψ ∗
specification_pre_1 t spec ∗
( if decide (spec ≠ SpecOwner) then
WP closed () {{ Χ false }}
else
True
) ∗
( if decide (spec ≠ SpecClosing) then
∀ q,
Ψ q -∗
WP open fd {{ res,
Ψ q ∗
Χ true res
}}
else
True
)
}}}
rcfd٠use t closed open
{{{
b res
, RET res;
Χ b res ∗
match spec with
| SpecOwner ⇒
⌜b = true⌝ ∗
rcfd_owner t
| SpecClosing ⇒
⌜b = false⌝
| SpecNormal ⇒
True
end
}}}.
Lemma rcfd٠use𑁒spec Χ t owned fd Ψ `{!Fractional Ψ} (closed open : val) :
{{{
rcfd_inv t owned fd Ψ ∗
WP closed () {{ Χ false }} ∗
( ∀ q,
Ψ q -∗
WP open fd {{ res,
Ψ q ∗
Χ true res
}}
)
}}}
rcfd٠use t closed open
{{{
b res
, RET res;
Χ b res
}}}.
Lemma rcfd٠use𑁒spec_owner Χ t owned fd Ψ `{!Fractional Ψ} (closed open : val) :
{{{
rcfd_inv t owned fd Ψ ∗
rcfd_owner t ∗
( ∀ q,
Ψ q -∗
WP open fd {{ res,
Ψ q ∗
Χ res
}}
)
}}}
rcfd٠use t closed open
{{{
res
, RET res;
Χ res
}}}.
Lemma rcfd٠use𑁒spec_closing Χ t owned fd Ψ `{!Fractional Ψ} (closed open : val) :
{{{
rcfd_inv t owned fd Ψ ∗
rcfd_closing t ∗
WP closed () {{ Χ }}
}}}
rcfd٠use t closed open
{{{
res
, RET res;
Χ res
}}}.
#[local] Lemma rcfd٠close𑁒spec_aux closing t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
( if owned then
rcfd_owner t
else
True
) ∗
( if closing then
rcfd_closing t
else
Ψ 1%Qp -∗
∃ chars,
unix_fd_model fd (DfracOwn 1) chars
)
}}}
rcfd٠close t
{{{
b
, RET #b;
rcfd_closing t ∗
( if owned then
⌜b = true⌝
else
True
) ∗
( if closing then
⌜b = false⌝
else
True
)
}}}.
Lemma rcfd٠close𑁒spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
( if owned then
rcfd_owner t
else
True
) ∗
( Ψ 1%Qp -∗
∃ chars,
unix_fd_model fd (DfracOwn 1) chars
)
}}}
rcfd٠close t
{{{
b
, RET #b;
rcfd_closing t ∗
if owned then
⌜b = true⌝
else
True
}}}.
Lemma rcfd٠close𑁒spec_closing t fd Ψ :
{{{
rcfd_inv t false fd Ψ ∗
rcfd_closing t
}}}
rcfd٠close t
{{{
RET false;
True
}}}.
#[local] Lemma rcfd٠remove𑁒spec_aux closing t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
( if owned then
rcfd_owner t
else
True
) ∗
( if closing then
rcfd_closing t
else
True
)
}}}
rcfd٠remove t
{{{
o
, RET o;
rcfd_closing t ∗
( if owned then
⌜o = Some fd⌝ ∗
Ψ 1%Qp
else
match o with
| None ⇒
True
| Some fd_ ⇒
⌜fd_ = fd⌝ ∗
Ψ 1%Qp
end
) ∗
( if closing then
⌜o = None⌝
else
True
)
}}}.
Lemma rcfd٠remove𑁒spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
if owned then
rcfd_owner t
else
True
}}}
rcfd٠remove t
{{{
o
, RET o;
rcfd_closing t ∗
if owned then
⌜o = Some fd⌝ ∗
Ψ 1%Qp
else
match o with
| None ⇒
True
| Some fd_ ⇒
⌜fd_ = fd⌝ ∗
Ψ 1%Qp
end
}}}.
Lemma rcfd٠remove𑁒spec_closing t fd Ψ :
{{{
rcfd_inv t false fd Ψ ∗
rcfd_closing t
}}}
rcfd٠remove t
{{{
RET §None;
True
}}}.
#[local] Lemma rcfd٠is_open𑁒spec_aux spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
specification_pre_1 t spec
}}}
rcfd٠is_open t
{{{
b
, RET #b;
match spec with
| SpecOwner ⇒
⌜b = true⌝ ∗
rcfd_owner t
| SpecClosing ⇒
⌜b = false⌝
| SpecNormal ⇒
if b then
True
else
rcfd_closing t
end
}}}.
Lemma rcfd٠is_open𑁒spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ
}}}
rcfd٠is_open t
{{{
b
, RET #b;
if b then
True
else
rcfd_closing t
}}}.
Lemma rcfd٠is_open𑁒spec_owner t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
rcfd_owner t
}}}
rcfd٠is_open t
{{{
RET true;
rcfd_owner t
}}}.
Lemma rcfd٠is_open𑁒spec_closing t owned fd Ψ :
{{{
rcfd_inv t false fd Ψ ∗
rcfd_closing t
}}}
rcfd٠is_open t
{{{
RET false;
True
}}}.
#[local] Lemma rcfd٠peek𑁒spec_aux spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
specification_pre_1 t spec
}}}
rcfd٠peek t
{{{
o
, RET o;
match spec with
| SpecOwner ⇒
⌜o = Some fd⌝ ∗
rcfd_owner t
| SpecClosing ⇒
⌜o = None⌝
| SpecNormal ⇒
match o with
| None ⇒
rcfd_closing t
| Some fd_ ⇒
⌜fd_ = fd⌝
end
end
}}}.
Lemma rcfd٠peek𑁒spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ
}}}
rcfd٠peek t
{{{
o
, RET o;
match o with
| None ⇒
rcfd_closing t
| Some fd_ ⇒
⌜fd_ = fd⌝
end
}}}.
Lemma rcfd٠peek𑁒spec_owner t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
rcfd_owner t
}}}
rcfd٠peek t
{{{
RET Some fd;
rcfd_owner t
}}}.
Lemma rcfd٠peek𑁒spec_closing t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
rcfd_closing t
}}}
rcfd٠peek t
{{{
RET §None;
True
}}}.
End rcfd_G.
From zoo_eio Require
rcfd__opaque.
#[global] Opaque rcfd_inv.
#[global] Opaque rcfd_owner.
#[global] Opaque rcfd_closing.
prelude.
From zoo.common Require Import
countable
gmultiset
relations.
From zoo.iris.base_logic Require Import
lib.auth_gmultiset
lib.auth_mono.
From zoo.language Require Import
notations.
From zoo.diaframe Require Import
diaframe.
From zoo_std Require Import
option
spsc_waiter.
From unix Require Import
unix.
From zoo_eio Require Export
base
rcfd__code.
From zoo_eio Require Import
rcfd__types.
From zoo Require Import
options.
Implicit Types b owned closing : bool.
Implicit Types ops : Z.
Implicit Types q stock : Qp.
Implicit Types qs : gmultiset Qp.
Implicit Types l open : location.
Implicit Types t v v_state fd fn : val.
Implicit Types o : option val.
Record metadata :=
{ metadata_fd : val
; metadata_open : block_id
; metadata_owned : bool
; metadata_tokens : gname
; metadata_lstate : gname
}.
Implicit Types γ : metadata.
#[local] Instance metadata_eq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadata_countable :
Countable metadata.
Variant state :=
| Open
| Closing fn.
Implicit Types state : state.
#[local] Instance state_inhabited : Inhabited state :=
populate Open.
#[local] Instance state_eq_dec : EqDecision state :=
ltac:(solve_decision).
#[local] Definition state_to_val γ state :=
match state with
| Open ⇒
‘Open@γ.(metadata_open)[ γ.(metadata_fd) ]
| Closing fn ⇒
‘Closing[ fn ]
end%V.
#[local] Arguments state_to_val _ !_ / : assert.
Variant lstate :=
| LOpen
| LClosingUsers
| LClosingNoUsers.
Implicit Types lstate : lstate.
#[local] Definition lstate_measure lstate :=
match lstate with
| LOpen ⇒
0
| LClosingUsers ⇒
1
| LClosingNoUsers ⇒
2
end.
#[global] Instance lstate_inhabited : Inhabited lstate :=
populate LOpen.
#[global] Instance lstate_eq_dec : EqDecision lstate :=
ltac:(solve_decision).
Variant lstep : relation lstate :=
| lstep_close_users :
lstep LOpen LClosingUsers
| lstep_close_no_users :
lstep LClosingUsers LClosingNoUsers.
#[local] Hint Constructors lstep : core.
#[local] Lemma lstep_measure lstate1 lstate2 :
lstep lstate1 lstate2 →
lstate_measure lstate1 < lstate_measure lstate2.
#[local] Lemma lstep_tc_measure lstate1 lstate2 :
tc lstep lstate1 lstate2 →
lstate_measure lstate1 < lstate_measure lstate2.
#[local] Lemma lstep_rtc_measure lstate1 lstate2 :
rtc lstep lstate1 lstate2 →
lstate_measure lstate1 ≤ lstate_measure lstate2.
#[local] Instance lsteps_antisymm :
AntiSymm (=) (rtc lstep).
Class RcfdG Σ `{zoo_G : !ZooG Σ} :=
{ #[local] rcfd_G_spsc_waiter_G :: SpscWaiterG Σ
; #[local] rcfd_G_tokens_G :: AuthGmultisetG Σ Qp
; #[local] rcfd_G_lstate_G :: AuthMonoG Σ (A := leibnizO lstate) lstep
}.
Definition rcfd_Σ :=
#[spsc_waiter_Σ
; auth_gmultiset_Σ Qp
; auth_mono_Σ (A := leibnizO lstate) lstep
].
#[global] Instance subG_rcfd_Σ `{zoo_G : !ZooG Σ} :
subG rcfd_Σ Σ →
RcfdG Σ.
Section rcfd_G.
Context `{rcfd_G : RcfdG Σ}.
Implicit Types Ψ : frac → iProp Σ.
#[local] Definition tokens_auth' γ_tokens Ψ ops : iProp Σ :=
∃ stock qs,
⌜ops = size qs⌝ ∗
⌜set_fold Qp.add stock qs = 1%Qp⌝ ∗
auth_gmultiset_auth γ_tokens (DfracOwn 1) qs ∗
Ψ stock.
#[local] Definition tokens_auth γ :=
tokens_auth' γ.(metadata_tokens).
#[local] Instance : CustomIpat "tokens_auth" :=
" ( %stock & %qs & {{lazy}%Hops;->} & %Hqs & Hauth & HΨ_stock ) ".
#[local] Definition tokens_frag γ q :=
auth_gmultiset_frag γ.(metadata_tokens) {[+q+]}.
#[local] Definition lstate_auth_frac owned lstate :=
match lstate with
| LOpen ⇒
if owned then 1/4 else 1
| _ ⇒
1
end%Qp.
#[local] Definition lstate_auth' γ_lstate owned lstate :=
auth_mono_auth _ γ_lstate (DfracOwn $ lstate_auth_frac owned lstate) lstate.
#[local] Definition lstate_auth γ :=
lstate_auth' γ.(metadata_lstate) γ.(metadata_owned).
#[local] Definition lstate_lb γ lstate :=
auth_mono_lb _ γ.(metadata_lstate) lstate.
#[local] Definition owner' γ_lstate :=
auth_mono_auth _ γ_lstate (DfracOwn (3/4)%Qp) LOpen.
#[local] Definition owner γ :=
owner' γ.(metadata_lstate).
#[local] Definition inv_lstate_open γ Ψ state ops : iProp Σ :=
tokens_auth γ Ψ ops ∗
⌜state = Open⌝.
#[local] Instance : CustomIpat "inv_lstate_open" :=
" ( Htokens_auth & {%H{eq};->} ) ".
#[local] Definition inv_lstate_closing_users γ Ψ state ops : iProp Σ :=
∃ fn,
tokens_auth γ Ψ ops ∗
⌜state = Closing fn⌝ ∗
⌜0 < ops⌝%Z ∗
(Ψ 1%Qp -∗ WP fn () {{ itype_unit }}).
#[local] Instance : CustomIpat "inv_lstate_closing_users" :=
" ( %fn{} & Htokens_auth & {%H{eq};->} & %Hops{} & Hfn{} ) ".
#[local] Definition inv_lstate_closing_no_users state : iProp Σ :=
∃ fn,
⌜state = Closing fn⌝ ∗
WP fn () {{ itype_unit }}.
#[local] Instance : CustomIpat "inv_lstate_closing_no_users" :=
" ( %fn{} & {%H{eq};->} & Hfn{} ) ".
#[local] Definition inv_lstate γ Ψ state lstate ops :=
match lstate with
| LOpen ⇒
inv_lstate_open γ Ψ state ops
| LClosingUsers ⇒
inv_lstate_closing_users γ Ψ state ops
| LClosingNoUsers ⇒
inv_lstate_closing_no_users state
end.
#[local] Definition inv_inner l γ Ψ : iProp Σ :=
∃ state lstate ops,
l.[ops] ↦ #ops ∗
l.[state] ↦ state_to_val γ state ∗
lstate_auth γ lstate ∗
inv_lstate γ Ψ state lstate ops.
#[local] Instance : CustomIpat "inv_inner" :=
" ( %state{} & %lstate{} & %ops{} & Hl_ops & Hl_state & Hlstate_auth & Hlstate ) ".
#[local] Definition inv' l γ Ψ :=
inv nroot (inv_inner l γ Ψ).
Definition rcfd_inv t owned fd Ψ : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
⌜owned = γ.(metadata_owned)⌝ ∗
⌜fd = γ.(metadata_fd)⌝ ∗
meta l nroot γ ∗
inv' l γ Ψ.
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & -> & -> & -> & #Hmeta & #Hinv ) ".
Definition rcfd_owner t : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
owner γ.
#[local] Instance : CustomIpat "owner" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Howner{_{}} ) ".
Definition rcfd_closing t : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
meta l nroot γ ∗
lstate_lb γ LClosingUsers.
#[local] Instance : CustomIpat "closing" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & #Hlstate_lb{_{}} ) ".
#[local] Instance tokens_auth'_ne γ_tokens n :
Proper (
(pointwise_relation _ (≡{n}≡)) ==>
(=) ==>
(≡{n}≡)
) (tokens_auth' γ_tokens).
#[local] Instance tokens_auth'_proper γ_tokens :
Proper (
(pointwise_relation _ (≡)) ==>
(=) ==>
(≡)
) (tokens_auth' γ_tokens).
#[global] Instance rcfd_inv_contractive t owned fd n :
Proper (
(pointwise_relation _ (dist_later n)) ==>
(≡{n}≡)
) (rcfd_inv t owned fd).
#[global] Instance rcfd_inv_proper t owned fd :
Proper (
(pointwise_relation _ (≡)) ==>
(≡)
) (rcfd_inv t owned fd).
#[global] Instance rcfd_owner_timeless t :
Timeless (rcfd_owner t).
#[global] Instance rcfd_closing_timeless t :
Timeless (rcfd_closing t).
#[global] Instance rcfd_inv_persistent t owned fd Ψ :
Persistent (rcfd_inv t owned fd Ψ).
#[global] Instance rcfd_closing_persistent t :
Persistent (rcfd_closing t).
#[local] Lemma tokens_alloc Ψ :
Ψ 1%Qp ⊢ |==>
∃ γ_tokens,
tokens_auth' γ_tokens Ψ 0.
#[local] Lemma tokens_auth_valid γ Ψ ops :
tokens_auth γ Ψ ops ⊢
⌜(0 ≤ ops)%Z⌝.
#[local] Lemma tokens_auth_consume γ Ψ :
tokens_auth γ Ψ 0 ⊢
Ψ 1%Qp.
#[local] Lemma tokens_update_alloc γ Ψ `{!Fractional Ψ} ops :
tokens_auth γ Ψ ops ⊢ |==>
∃ q,
tokens_auth γ Ψ (ops + 1) ∗
tokens_frag γ q ∗
Ψ q.
#[local] Lemma tokens_update_dealloc γ Ψ `{!Fractional Ψ} ops q :
tokens_auth γ Ψ ops -∗
tokens_frag γ q -∗
Ψ q ==∗
tokens_auth γ Ψ (ops - 1).
#[local] Lemma lstate_owner_alloc owned :
⊢ |==>
∃ γ_lstate,
lstate_auth' γ_lstate owned LOpen ∗
if owned then
owner' γ_lstate
else
True.
#[local] Lemma lstate_lb_get γ lstate :
lstate_auth γ lstate ⊢
lstate_lb γ lstate.
#[local] Lemma lstate_lb_mono {γ lstate} lstate' :
lstep lstate' lstate →
lstate_lb γ lstate ⊢
lstate_lb γ lstate'.
#[local] Lemma lstate_valid γ lstate lstate' :
lstate_auth γ lstate -∗
lstate_lb γ lstate' -∗
⌜rtc lstep lstate' lstate⌝.
#[local] Lemma lstate_valid_closing_users γ lstate :
lstate_auth γ lstate -∗
lstate_lb γ LClosingUsers -∗
⌜lstate ≠ LOpen⌝.
#[local] Lemma lstate_valid_closing_users' γ lstate :
lstate_auth γ lstate -∗
lstate_lb γ LClosingUsers -∗
⌜lstate = LClosingUsers ∨ lstate = LClosingNoUsers⌝.
#[local] Lemma lstate_valid_closing_no_users γ lstate :
lstate_auth γ lstate -∗
lstate_lb γ LClosingNoUsers -∗
⌜lstate = LClosingNoUsers⌝.
#[local] Lemma lstate_update_close_users γ :
lstate_auth γ LOpen -∗
(if γ.(metadata_owned) then owner γ else True) ==∗
lstate_auth γ LClosingUsers.
#[local] Lemma lstate_update_close_no_users γ :
lstate_auth γ LClosingUsers ⊢ |==>
lstate_auth γ LClosingNoUsers.
#[local] Lemma owner_exclusive γ :
owner γ -∗
owner γ -∗
False.
#[local] Lemma owner_lstate_auth γ lstate :
owner γ -∗
lstate_auth γ lstate -∗
⌜lstate = LOpen⌝.
#[local] Lemma owner_lstate_lb γ :
owner γ -∗
lstate_lb γ LClosingUsers -∗
False.
Opaque tokens_auth'.
#[local] Lemma rcfd_owner_elim l γ :
meta l nroot γ -∗
rcfd_owner #l -∗
owner γ.
#[local] Lemma rcfd_owner_elim' l γ b :
meta l nroot γ -∗
( if b then
rcfd_owner #l
else
True
) -∗
if b then
owner γ
else
True.
Lemma rcfd_owner_exclusive t :
rcfd_owner t -∗
rcfd_owner t -∗
False.
Lemma rcfd_owner_closing t :
rcfd_owner t -∗
rcfd_closing t -∗
False.
#[local] Lemma rcfd_closing_elim l γ :
meta l nroot γ -∗
rcfd_closing #l -∗
lstate_lb γ LClosingUsers.
#[local] Lemma rcfd_closing_elim' l γ b P :
meta l nroot γ -∗
( if b then
rcfd_closing #l
else
P
) -∗
if b then
lstate_lb γ LClosingUsers
else
P.
#[local] Lemma inv_lstate_Open γ Ψ lstate ops :
inv_lstate γ Ψ Open lstate ops ⊢
⌜lstate = LOpen⌝.
#[local] Lemma inv_lstate_Closing γ Ψ state lstate ops :
state ≠ Open →
inv_lstate γ Ψ state lstate ops -∗
lstate_auth γ lstate -∗
∃ fn,
⌜state = Closing fn⌝ ∗
⌜lstate ≠ LOpen ⌝ ∗
lstate_lb γ LClosingUsers.
#[local] Lemma inv_lstate_LClosing γ Ψ state lstate ops :
lstate ≠ LOpen →
inv_lstate γ Ψ state lstate ops -∗
lstate_auth γ lstate -∗
∃ fn,
⌜state = Closing fn⌝ ∗
lstate_lb γ LClosingUsers.
Lemma rcfd٠make𑁒spec owned Ψ fd :
{{{
Ψ 1%Qp
}}}
rcfd٠make fd
{{{
t
, RET t;
rcfd_inv t owned fd Ψ ∗
if owned then
rcfd_owner t
else
True
}}}.
#[local] Lemma rcfd٠finish𑁒spec l γ Ψ (close : val) :
{{{
inv' l γ Ψ ∗
lstate_lb γ LClosingUsers
}}}
rcfd٠finish #l close ’Closing[ close ]
{{{
RET ();
True
}}}.
#[local] Lemma rcfd٠put𑁒spec l γ Ψ `{!Fractional Ψ} :
{{{
inv' l γ Ψ ∗
( lstate_lb γ LClosingNoUsers
∨ ∃ q,
tokens_frag γ q ∗
Ψ q
)
}}}
rcfd٠put #l
{{{
RET ();
True
}}}.
Variant specification :=
| SpecOwner
| SpecClosing
| SpecNormal.
Implicit Types spec : specification.
#[local] Instance specification_eq_dec : EqDecision specification :=
ltac:(solve_decision).
#[local] Definition specification_pre_1 t spec : iProp Σ :=
match spec with
| SpecOwner ⇒
rcfd_owner t
| SpecClosing ⇒
rcfd_closing t
| SpecNormal ⇒
True
end.
#[local] Definition specification_pre_2 γ spec : iProp Σ :=
match spec with
| SpecOwner ⇒
owner γ
| SpecClosing ⇒
lstate_lb γ LClosingUsers
| SpecNormal ⇒
True
end.
#[local] Lemma specification_pre_1_2 l γ spec :
meta l nroot γ -∗
specification_pre_1 #l spec -∗
specification_pre_2 γ spec.
#[local] Lemma rcfd٠get𑁒spec_aux spec l γ Ψ `{HΨ : !Fractional Ψ} :
{{{
inv' l γ Ψ ∗
specification_pre_2 γ spec
}}}
rcfd٠get #l
{{{
o
, RET o;
match spec with
| SpecOwner ⇒
⌜o ≠ None⌝ ∗
owner γ
| SpecClosing ⇒
⌜o = None⌝
| SpecNormal ⇒
True
end ∗
match o with
| None ⇒
True
| Some fd_ ⇒
∃ q,
⌜fd_ = γ.(metadata_fd)⌝ ∗
tokens_frag γ q ∗
Ψ q
end
}}}.
#[local] Lemma rcfd٠get𑁒spec l γ Ψ `{HΨ : !Fractional Ψ} :
{{{
inv' l γ Ψ
}}}
rcfd٠get #l
{{{
o
, RET o;
match o with
| None ⇒
True
| Some fd_ ⇒
∃ q,
⌜fd_ = γ.(metadata_fd)⌝ ∗
tokens_frag γ q ∗
Ψ q
end
}}}.
#[local] Lemma rcfd٠get𑁒spec_owner l γ Ψ `{HΨ : !Fractional Ψ} :
{{{
inv' l γ Ψ ∗
owner γ
}}}
rcfd٠get #l
{{{
RET Some γ.(metadata_fd);
∃ q,
owner γ ∗
tokens_frag γ q ∗
Ψ q
}}}.
#[local] Lemma rcfd٠get𑁒spec_closing l γ Ψ `{HΨ : !Fractional Ψ} :
{{{
inv' l γ Ψ ∗
lstate_lb γ LClosingUsers
}}}
rcfd٠get #l
{{{
RET None;
True
}}}.
#[local] Lemma rcfd٠use𑁒spec_aux spec Χ t owned fd Ψ `{!Fractional Ψ} (closed open : val) :
{{{
rcfd_inv t owned fd Ψ ∗
specification_pre_1 t spec ∗
( if decide (spec ≠ SpecOwner) then
WP closed () {{ Χ false }}
else
True
) ∗
( if decide (spec ≠ SpecClosing) then
∀ q,
Ψ q -∗
WP open fd {{ res,
Ψ q ∗
Χ true res
}}
else
True
)
}}}
rcfd٠use t closed open
{{{
b res
, RET res;
Χ b res ∗
match spec with
| SpecOwner ⇒
⌜b = true⌝ ∗
rcfd_owner t
| SpecClosing ⇒
⌜b = false⌝
| SpecNormal ⇒
True
end
}}}.
Lemma rcfd٠use𑁒spec Χ t owned fd Ψ `{!Fractional Ψ} (closed open : val) :
{{{
rcfd_inv t owned fd Ψ ∗
WP closed () {{ Χ false }} ∗
( ∀ q,
Ψ q -∗
WP open fd {{ res,
Ψ q ∗
Χ true res
}}
)
}}}
rcfd٠use t closed open
{{{
b res
, RET res;
Χ b res
}}}.
Lemma rcfd٠use𑁒spec_owner Χ t owned fd Ψ `{!Fractional Ψ} (closed open : val) :
{{{
rcfd_inv t owned fd Ψ ∗
rcfd_owner t ∗
( ∀ q,
Ψ q -∗
WP open fd {{ res,
Ψ q ∗
Χ res
}}
)
}}}
rcfd٠use t closed open
{{{
res
, RET res;
Χ res
}}}.
Lemma rcfd٠use𑁒spec_closing Χ t owned fd Ψ `{!Fractional Ψ} (closed open : val) :
{{{
rcfd_inv t owned fd Ψ ∗
rcfd_closing t ∗
WP closed () {{ Χ }}
}}}
rcfd٠use t closed open
{{{
res
, RET res;
Χ res
}}}.
#[local] Lemma rcfd٠close𑁒spec_aux closing t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
( if owned then
rcfd_owner t
else
True
) ∗
( if closing then
rcfd_closing t
else
Ψ 1%Qp -∗
∃ chars,
unix_fd_model fd (DfracOwn 1) chars
)
}}}
rcfd٠close t
{{{
b
, RET #b;
rcfd_closing t ∗
( if owned then
⌜b = true⌝
else
True
) ∗
( if closing then
⌜b = false⌝
else
True
)
}}}.
Lemma rcfd٠close𑁒spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
( if owned then
rcfd_owner t
else
True
) ∗
( Ψ 1%Qp -∗
∃ chars,
unix_fd_model fd (DfracOwn 1) chars
)
}}}
rcfd٠close t
{{{
b
, RET #b;
rcfd_closing t ∗
if owned then
⌜b = true⌝
else
True
}}}.
Lemma rcfd٠close𑁒spec_closing t fd Ψ :
{{{
rcfd_inv t false fd Ψ ∗
rcfd_closing t
}}}
rcfd٠close t
{{{
RET false;
True
}}}.
#[local] Lemma rcfd٠remove𑁒spec_aux closing t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
( if owned then
rcfd_owner t
else
True
) ∗
( if closing then
rcfd_closing t
else
True
)
}}}
rcfd٠remove t
{{{
o
, RET o;
rcfd_closing t ∗
( if owned then
⌜o = Some fd⌝ ∗
Ψ 1%Qp
else
match o with
| None ⇒
True
| Some fd_ ⇒
⌜fd_ = fd⌝ ∗
Ψ 1%Qp
end
) ∗
( if closing then
⌜o = None⌝
else
True
)
}}}.
Lemma rcfd٠remove𑁒spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
if owned then
rcfd_owner t
else
True
}}}
rcfd٠remove t
{{{
o
, RET o;
rcfd_closing t ∗
if owned then
⌜o = Some fd⌝ ∗
Ψ 1%Qp
else
match o with
| None ⇒
True
| Some fd_ ⇒
⌜fd_ = fd⌝ ∗
Ψ 1%Qp
end
}}}.
Lemma rcfd٠remove𑁒spec_closing t fd Ψ :
{{{
rcfd_inv t false fd Ψ ∗
rcfd_closing t
}}}
rcfd٠remove t
{{{
RET §None;
True
}}}.
#[local] Lemma rcfd٠is_open𑁒spec_aux spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
specification_pre_1 t spec
}}}
rcfd٠is_open t
{{{
b
, RET #b;
match spec with
| SpecOwner ⇒
⌜b = true⌝ ∗
rcfd_owner t
| SpecClosing ⇒
⌜b = false⌝
| SpecNormal ⇒
if b then
True
else
rcfd_closing t
end
}}}.
Lemma rcfd٠is_open𑁒spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ
}}}
rcfd٠is_open t
{{{
b
, RET #b;
if b then
True
else
rcfd_closing t
}}}.
Lemma rcfd٠is_open𑁒spec_owner t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
rcfd_owner t
}}}
rcfd٠is_open t
{{{
RET true;
rcfd_owner t
}}}.
Lemma rcfd٠is_open𑁒spec_closing t owned fd Ψ :
{{{
rcfd_inv t false fd Ψ ∗
rcfd_closing t
}}}
rcfd٠is_open t
{{{
RET false;
True
}}}.
#[local] Lemma rcfd٠peek𑁒spec_aux spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
specification_pre_1 t spec
}}}
rcfd٠peek t
{{{
o
, RET o;
match spec with
| SpecOwner ⇒
⌜o = Some fd⌝ ∗
rcfd_owner t
| SpecClosing ⇒
⌜o = None⌝
| SpecNormal ⇒
match o with
| None ⇒
rcfd_closing t
| Some fd_ ⇒
⌜fd_ = fd⌝
end
end
}}}.
Lemma rcfd٠peek𑁒spec t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ
}}}
rcfd٠peek t
{{{
o
, RET o;
match o with
| None ⇒
rcfd_closing t
| Some fd_ ⇒
⌜fd_ = fd⌝
end
}}}.
Lemma rcfd٠peek𑁒spec_owner t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
rcfd_owner t
}}}
rcfd٠peek t
{{{
RET Some fd;
rcfd_owner t
}}}.
Lemma rcfd٠peek𑁒spec_closing t owned fd Ψ :
{{{
rcfd_inv t owned fd Ψ ∗
rcfd_closing t
}}}
rcfd٠peek t
{{{
RET §None;
True
}}}.
End rcfd_G.
From zoo_eio Require
rcfd__opaque.
#[global] Opaque rcfd_inv.
#[global] Opaque rcfd_owner.
#[global] Opaque rcfd_closing.