Library zoo_eio.rcfd
Require Import zoo.prelude.
Require Import zoo.common.countable.
Require Import zoo.common.gmultiset.
Require Import zoo.common.relations.
Require Import zoo.iris.base_logic.lib.auth_gmultiset.
Require Import zoo.iris.base_logic.lib.auth_mono.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_eio.rcfd__code.
Require Import zoo_eio.rcfd__types.
Require Import zoo.options.
Implicit Type b owned closing : bool.
Implicit Type ops : Z.
Implicit Type q stock : Qp.
Implicit Type qs : gmultiset Qp.
Implicit Type l open : location.
Implicit Type t v v_state fd fn : val.
Implicit Type o : option val.
Record metadata :=
{ metadata۰fd : val
; metadata۰open : block_id
; metadata۰owned : bool
; metadata۰tokens : gname
; metadata۰lstate : gname
}.
Implicit Type γ : metadata.
#[local] Instance metadataｰeq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadataｰcountable :
Countable metadata.
Variant state :=
| Open
| Closing fn.
Implicit Type 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 Type 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 lstepｰrtcｰantisymm :
AntiSymm (=) (rtc lstep).
Class RcfdG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] rcfd۰G۰waiter_spsc۰G :: WaiterSpscG Σ
; #[local] rcfd۰G۰tokens۰G :: AuthGmultisetG Σ Qp
; #[local] rcfd۰G۰lstate۰G :: AuthMonoG Σ (A := leibnizO lstate) lstep
}.
Definition rcfd۰Σ :=
#[waiter_spsc۰Σ
; 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 Type Ψ : 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)⌝ ∗
l ↪ γ ∗
inv' l γ Ψ.
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & -> & -> & -> & #Hmeta & #Hinv ) ".
Definition rcfd۰owner t : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
l ↪ γ ∗
owner γ.
#[local] Instance : CustomIpat "owner" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Howner{_{}} ) ".
Definition rcfd۰closing t : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
l ↪ γ ∗
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ｰ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 γ :
l ↪ γ -∗
rcfd۰owner #l -∗
owner γ.
#[local] Lemma rcfd۰ownerｰelim' l γ b :
l ↪ γ -∗
( 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 γ :
l ↪ γ -∗
rcfd۰closing #l -∗
lstate۰lb γ LClosingUsers.
#[local] Lemma rcfd۰closingｰelim' l γ b P :
l ↪ γ -∗
( 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 Type spec : specification.
#[local] Instance specificationｰeq_dec : EqDecision specification :=
ltac:(solve_decision).
#[local] Definition specification۰pre₁ t spec : iProp Σ :=
match spec with
| SpecOwner ⇒
rcfd۰owner t
| SpecClosing ⇒
rcfd۰closing t
| SpecNormal ⇒
True
end.
#[local] Definition specification۰pre₂ γ spec : iProp Σ :=
match spec with
| SpecOwner ⇒
owner γ
| SpecClosing ⇒
lstate۰lb γ LClosingUsers
| SpecNormal ⇒
True
end.
#[local] Lemma specificationｰpre₁ｰpre₂ l γ spec :
l ↪ γ -∗
specification۰pre₁ #l spec -∗
specification۰pre₂ γ spec.
#[local] Lemma rcfd٠getｰspecｰaux spec l γ Ψ `{HΨ : !Fractional Ψ} :
{{{
inv' l γ Ψ ∗
specification۰pre₂ γ 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₁ 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₁ 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₁ 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.
Require zoo_eio.rcfd__opaque.
#[global] Opaque rcfd۰inv.
#[global] Opaque rcfd۰owner.
#[global] Opaque rcfd۰closing.
Require Import zoo.common.countable.
Require Import zoo.common.gmultiset.
Require Import zoo.common.relations.
Require Import zoo.iris.base_logic.lib.auth_gmultiset.
Require Import zoo.iris.base_logic.lib.auth_mono.
Require Import zoo.base.
Require Import zoo_std.option.
Require Export zoo_eio.rcfd__code.
Require Import zoo_eio.rcfd__types.
Require Import zoo.options.
Implicit Type b owned closing : bool.
Implicit Type ops : Z.
Implicit Type q stock : Qp.
Implicit Type qs : gmultiset Qp.
Implicit Type l open : location.
Implicit Type t v v_state fd fn : val.
Implicit Type o : option val.
Record metadata :=
{ metadata۰fd : val
; metadata۰open : block_id
; metadata۰owned : bool
; metadata۰tokens : gname
; metadata۰lstate : gname
}.
Implicit Type γ : metadata.
#[local] Instance metadataｰeq_dec : EqDecision metadata :=
ltac:(solve_decision).
#[local] Instance metadataｰcountable :
Countable metadata.
Variant state :=
| Open
| Closing fn.
Implicit Type 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 Type 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 lstepｰrtcｰantisymm :
AntiSymm (=) (rtc lstep).
Class RcfdG Σ `{zoo۰G : !ZooG Σ} :=
{ #[local] rcfd۰G۰waiter_spsc۰G :: WaiterSpscG Σ
; #[local] rcfd۰G۰tokens۰G :: AuthGmultisetG Σ Qp
; #[local] rcfd۰G۰lstate۰G :: AuthMonoG Σ (A := leibnizO lstate) lstep
}.
Definition rcfd۰Σ :=
#[waiter_spsc۰Σ
; 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 Type Ψ : 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)⌝ ∗
l ↪ γ ∗
inv' l γ Ψ.
#[local] Instance : CustomIpat "inv" :=
" ( %l & %γ & -> & -> & -> & #Hmeta & #Hinv ) ".
Definition rcfd۰owner t : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
l ↪ γ ∗
owner γ.
#[local] Instance : CustomIpat "owner" :=
" ( %l{;_} & %γ{;_} & %Heq{} & #Hmeta_{} & Howner{_{}} ) ".
Definition rcfd۰closing t : iProp Σ :=
∃ l γ,
⌜t = #l⌝ ∗
l ↪ γ ∗
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ｰ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 γ :
l ↪ γ -∗
rcfd۰owner #l -∗
owner γ.
#[local] Lemma rcfd۰ownerｰelim' l γ b :
l ↪ γ -∗
( 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 γ :
l ↪ γ -∗
rcfd۰closing #l -∗
lstate۰lb γ LClosingUsers.
#[local] Lemma rcfd۰closingｰelim' l γ b P :
l ↪ γ -∗
( 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 Type spec : specification.
#[local] Instance specificationｰeq_dec : EqDecision specification :=
ltac:(solve_decision).
#[local] Definition specification۰pre₁ t spec : iProp Σ :=
match spec with
| SpecOwner ⇒
rcfd۰owner t
| SpecClosing ⇒
rcfd۰closing t
| SpecNormal ⇒
True
end.
#[local] Definition specification۰pre₂ γ spec : iProp Σ :=
match spec with
| SpecOwner ⇒
owner γ
| SpecClosing ⇒
lstate۰lb γ LClosingUsers
| SpecNormal ⇒
True
end.
#[local] Lemma specificationｰpre₁ｰpre₂ l γ spec :
l ↪ γ -∗
specification۰pre₁ #l spec -∗
specification۰pre₂ γ spec.
#[local] Lemma rcfd٠getｰspecｰaux spec l γ Ψ `{HΨ : !Fractional Ψ} :
{{{
inv' l γ Ψ ∗
specification۰pre₂ γ 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₁ 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₁ 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₁ 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.
Require zoo_eio.rcfd__opaque.
#[global] Opaque rcfd۰inv.
#[global] Opaque rcfd۰owner.
#[global] Opaque rcfd۰closing.