Commit 19acb9ad authored by Robbert Krebbers's avatar Robbert Krebbers

More renaming, use Φ for predicates as we do in Iris.

parent 8c9c949a
......@@ -22,7 +22,7 @@ Instance proto_inhabited V PROP : Inhabited (proto V PROP) := populate TEnd.
CoFixpoint dual_proto {V PROP} (prot : proto V PROP) : proto V PROP :=
match prot with
| TEnd => TEnd
| TSR a P prot => TSR (dual_action a) P (λ v, dual_proto (prot v))
| TSR a Φ prot => TSR (dual_action a) Φ (λ v, dual_proto (prot v))
end.
Instance: Params (@dual_proto) 2.
......@@ -39,9 +39,9 @@ Notation "<!> x , prot" := (<!> x @ True, prot%proto)%proto
(at level 200, x pattern, prot at level 200) : proto_scope.
Notation "<?> x , prot" := (<?> x @ True, prot%proto)%proto
(at level 200, x pattern, prot at level 200) : proto_scope.
Notation "<!> @ P , prot" := (<!> x @ P x, prot x)%proto
Notation "<!> @ Φ , prot" := (TSR Send Φ prot)%proto
(at level 200, prot at level 200) : proto_scope.
Notation "<?> @ P , prot" := (<?> x @ P x, prot x)%proto
Notation "<?> @ Φ , prot" := (TSR Receive Φ prot)%proto
(at level 200, prot at level 200) : proto_scope.
Section proto_ofe.
......@@ -50,52 +50,52 @@ Section proto_ofe.
CoInductive proto_equiv : Equiv (proto V PROP) :=
| TEnd_equiv : TEnd TEnd
| TSR_equiv a P1 P2 prot1 prot2 :
pointwise_relation V () P1 P2
| TSR_equiv a Φ1 Φ2 prot1 prot2 :
pointwise_relation V () Φ1 Φ2
pointwise_relation V () prot1 prot2
TSR a P1 prot1 TSR a P2 prot2.
TSR a Φ1 prot1 TSR a Φ2 prot2.
Existing Instance proto_equiv.
CoInductive proto_dist : Dist (proto V PROP) :=
| TEnd_dist n : TEnd {n} TEnd
| TSR_dist_0 a P1 P2 prot1 prot2 :
pointwise_relation V (dist 0) P1 P2
TSR a P1 prot1 {0} TSR a P2 prot2
| TSR_dist_S n a P1 P2 prot1 prot2 :
pointwise_relation V (dist (S n)) P1 P2
| TSR_dist_0 a Φ1 Φ2 prot1 prot2 :
pointwise_relation V (dist 0) Φ1 Φ2
TSR a Φ1 prot1 {0} TSR a Φ2 prot2
| TSR_dist_S n a Φ1 Φ2 prot1 prot2 :
pointwise_relation V (dist (S n)) Φ1 Φ2
pointwise_relation V (dist n) prot1 prot2
TSR a P1 prot1 {S n} TSR a P2 prot2.
TSR a Φ1 prot1 {S n} TSR a Φ2 prot2.
Existing Instance proto_dist.
Lemma TSR_dist n a P1 P2 prot1 prot2 :
pointwise_relation V (dist n) P1 P2
Lemma TSR_dist n a Φ1 Φ2 prot1 prot2 :
pointwise_relation V (dist n) Φ1 Φ2
pointwise_relation V (dist_later n) prot1 prot2
TSR a P1 prot1 {n} TSR a P2 prot2.
TSR a Φ1 prot1 {n} TSR a Φ2 prot2.
Proof. destruct n; by constructor. Defined.
Definition proto_ofe_mixin : OfeMixin (proto V PROP).
Proof.
split.
- intros prot1 prot2. split.
+ revert prot1 prot2. cofix IH; destruct 1 as [|a P1 P2 prot1' prot2' HP]=> n.
+ revert prot1 prot2. cofix IH; destruct 1 as [|a Φ1 Φ2 prot1' prot2' HΦ]=> n.
{ constructor. }
destruct n as [|n].
* constructor=> v. apply equiv_dist, HP.
* constructor=> v. apply equiv_dist, HP. by apply IH.
+ revert prot1 prot2. cofix IH=> -[|a1 P1 prot1] -[|a2 P2 prot2] Hprot;
* constructor=> v. apply equiv_dist, HΦ.
* constructor=> v. apply equiv_dist, HΦ. by apply IH.
+ revert prot1 prot2. cofix IH=> -[|a1 Φ1 prot1] -[|a2 Φ2 prot2] Hprot;
feed inversion (Hprot O); subst; constructor=> v.
* apply equiv_dist=> n. feed inversion (Hprot n); auto.
* apply IH=> n. feed inversion (Hprot (S n)); auto.
- intros n. split.
+ revert n. cofix IH=> -[|n] [|a P prot]; constructor=> v; auto.
+ revert n. cofix IH=> -[|n] [|a Φ prot]; constructor=> v; auto.
+ revert n. cofix IH; destruct 1; constructor=> v; symmetry; auto.
+ revert n. cofix IH; destruct 1; inversion 1; constructor=> v; etrans; eauto.
- cofix IH=> -[|n]; inversion 1; constructor=> v; try apply dist_S; auto.
Qed.
Canonical Structure protoC : ofeT := OfeT (proto V PROP) proto_ofe_mixin.
Definition proto_head (d : V -c> PROP) (prot : proto V PROP) : V -c> PROP :=
match prot with TEnd => d | TSR a P prot => P end.
Definition proto_head (dΦ : V -c> PROP) (prot : proto V PROP) : V -c> PROP :=
match prot with TEnd => dΦ | TSR a Φ prot => Φ end.
Definition proto_tail (v : V) (prot : protoC) : later protoC :=
match prot with TEnd => Next TEnd | TSR a P prot => Next (prot v) end.
Global Instance proto_head_ne d : NonExpansive (proto_head d).
......@@ -106,7 +106,7 @@ Section proto_ofe.
Definition proto_force (prot : proto V PROP) : proto V PROP :=
match prot with
| TEnd => TEnd
| TSR a P prot => TSR a P prot
| TSR a Φ prot => TSR a Φ prot
end.
Lemma proto_force_eq prot : proto_force prot = prot.
Proof. by destruct prot. Defined.
......@@ -114,8 +114,8 @@ Section proto_ofe.
CoFixpoint proto_compl_go `{!Cofe PROP} (c : chain protoC) : protoC :=
match c O with
| TEnd => TEnd
| TSR a P prot => TSR a
(compl (chain_map (proto_head P) c) : V PROP)
| TSR a Φ prot => TSR a
(compl (chain_map (proto_head Φ) c) : V PROP)
(λ v, proto_compl_go (later_chain (chain_map (proto_tail v) c)))
end.
......@@ -124,16 +124,16 @@ Section proto_ofe.
Next Obligation.
intros ? n c; rewrite /compl. revert c n. cofix IH=> c n.
rewrite -(proto_force_eq (proto_compl_go c)) /=.
destruct (c O) as [|a P prot'] eqn:Hc0.
destruct (c O) as [|a Φ prot'] eqn:Hc0.
- assert (c n {0} TEnd) as Hcn.
{ rewrite -Hc0 -(chain_cauchy c 0 n) //. lia. }
by inversion Hcn.
- assert (c n {0} TSR a P prot') as Hcn.
- assert (c n {0} TSR a Φ prot') as Hcn.
{ rewrite -Hc0 -(chain_cauchy c 0 n) //. lia. }
inversion Hcn as [|? P' ? prot'' ? HP|]; subst.
inversion Hcn as [|? P' ? prot'' ? HΦ|]; subst.
destruct n as [|n]; constructor.
+ intros v. by rewrite (conv_compl 0 (chain_map (proto_head P) c) v) /= -H.
+ intros v. by rewrite (conv_compl _ (chain_map (proto_head P) c) v) /= -H.
+ intros v. by rewrite (conv_compl 0 (chain_map (proto_head Φ) c) v) /= -H.
+ intros v. by rewrite (conv_compl _ (chain_map (proto_head Φ) c) v) /= -H.
+ intros v. assert (prot'' v = later_car (proto_tail v (c (S n)))) as ->.
{ by rewrite -H /=. }
apply IH.
......@@ -147,7 +147,7 @@ Section proto_ofe.
Proper (pointwise_relation _ (dist n) ==>
pointwise_relation _ (dist n) ==> dist n) (TSR a).
Proof.
intros P1 P2 HP prot1 prot2 Hst. apply TSR_proto_contractive=> //.
intros Φ1 Φ2 HΦ prot1 prot2 Hst. apply TSR_proto_contractive=> //.
destruct n as [|n]=> // v /=. by apply dist_S.
Qed.
Global Instance TSR_proto_proper a :
......@@ -175,8 +175,8 @@ Section proto_ofe.
prot1 prot2 @{uPredI M}
match prot1, prot2 with
| TEnd, TEnd => True
| TSR a1 P1 prot1, TSR a2 P2 prot2 =>
a1 = a2 ( v, P1 v P2 v) ( v, prot1 v prot2 v)
| TSR a1 Φ1 prot1, TSR a2 Φ2 prot2 =>
a1 = a2 ( v, Φ1 v Φ2 v) ( v, prot1 v prot2 v)
| _, _ => False
end.
Proof.
......@@ -185,16 +185,16 @@ Section proto_ofe.
by intros [[= ->] [??]]; destruct n; constructor.
Qed.
Lemma proto_later_equiv M prot a P2 prot2 :
(prot TSR a P2 prot2) -
( P1 prot1, prot TSR a P1 prot1
( v, P1 v P2 v)
Lemma proto_later_equiv M prot a Φ2 prot2 :
(prot TSR a Φ2 prot2) -
( Φ1 prot1, prot TSR a Φ1 prot1
( v, Φ1 v Φ2 v)
( v, prot1 v prot2 v) : uPred M).
Proof.
iIntros "Heq". destruct prot as [|a' P1 prot1].
iIntros "Heq". destruct prot as [|a' Φ1 prot1].
- iDestruct (proto_equivI with "Heq") as ">[]".
- iDestruct (proto_equivI with "Heq") as "(>-> & HPeq & Hsteq)".
iExists P1, prot1. auto.
- iDestruct (proto_equivI with "Heq") as "(>-> & HΦeq & Hsteq)".
iExists Φ1, prot1. auto.
Qed.
Lemma dual_proto_flip {M} prot1 prot2 :
......@@ -212,7 +212,7 @@ CoFixpoint proto_map {V PROP PROP'} (f : PROP → PROP')
(prot : proto V PROP) : proto V PROP' :=
match prot with
| TEnd => TEnd
| TSR a P prot => TSR a (λ v, f (P v)) (λ v, proto_map f (prot v))
| TSR a Φ prot => TSR a (λ v, f (Φ v)) (λ v, proto_map f (prot v))
end.
Lemma proto_map_ext_ne {V PROP} {PROP' : ofeT}
(f g : PROP PROP') (prot : proto V PROP) n :
......@@ -220,7 +220,7 @@ Lemma proto_map_ext_ne {V PROP} {PROP' : ofeT}
Proof.
revert n prot. cofix IH=> n prot Hf.
rewrite -(proto_force_eq (proto_map f prot)) -(proto_force_eq (proto_map g prot)).
destruct prot as [|a P prot], n as [|n]; constructor=> v //. apply IH; auto using dist_S.
destruct prot as [|a Φ prot], n as [|n]; constructor=> v //. apply IH; auto using dist_S.
Qed.
Lemma proto_map_ext {V PROP} {B : ofeT} (f g : PROP B) (prot : proto V PROP) :
( x, f x g x) proto_map f prot proto_map g prot.
......@@ -305,10 +305,10 @@ Section DualProto.
Global Instance is_dual_end : IsDualProto (TEnd : proto V PROP) TEnd.
Proof. by rewrite /IsDualProto -(proto_force_eq (dual_proto _)). Qed.
Global Instance is_dual_tsr a1 a2 P (prot1 prot2 : V proto V PROP) :
Global Instance is_dual_tsr a1 a2 Φ (prot1 prot2 : V proto V PROP) :
IsDualAction a1 a2
( x, IsDualProto (prot1 x) (prot2 x))
IsDualProto (TSR a1 P prot1) (TSR a2 P prot2).
IsDualProto (TSR a1 Φ prot1) (TSR a2 Φ prot2).
Proof.
rewrite /IsDualAction /IsDualProto. intros <- Hst.
rewrite /IsDualProto -(proto_force_eq (dual_proto _)) /=.
......
......@@ -5,16 +5,16 @@ Section DualProtoEnc.
Context `{ValEncDec V} {PROP: bi} .
Definition TSR'
(a : action) (P : V PROP) (prot : V proto val PROP) : proto val PROP :=
(a : action) (Φ : V PROP) (prot : V proto val PROP) : proto val PROP :=
TSR a
(λ v, if val_decode v is Some x then P x else False)%I
(λ v, if val_decode v is Some x then Φ x else False)%I
(λ v, if val_decode v is Some x then prot x else TEnd (* dummy *)).
Global Instance: Params (@TSR') 3.
Global Instance is_dual_tsr' a1 a2 P (st1 st2 : V proto val PROP) :
Global Instance is_dual_tsr' a1 a2 Φ (st1 st2 : V proto val PROP) :
IsDualAction a1 a2
( x, IsDualProto (st1 x) (st2 x))
IsDualProto (TSR' a1 P st1) (TSR' a2 P st2).
IsDualProto (TSR' a1 Φ st1) (TSR' a2 Φ st2).
Proof.
rewrite /IsDualAction /IsDualProto. intros <- Hst.
rewrite -(proto_force_eq (dual_proto _)).
......@@ -33,41 +33,39 @@ Notation "<!> x , prot" := (<!> x @ True, (prot x))%proto
(at level 200, x pattern, prot at level 200) : proto_scope.
Notation "<?> x , prot" := (<?> x @ True, (prot x))%proto
(at level 200, x pattern, prot at level 200) : proto_scope.
Notation "<!> @ P , prot" := (<!> dummy__ @ P dummy__, prot dummy__)%proto
Notation "<!> @ Φ , prot" := (TSR' Send Φ prot)
(at level 200, prot at level 200) : proto_scope.
Notation "<?> @ P , prot" := (<?> dummy__ @ P dummy__, prot dummy__)%proto
Notation "<?> @ Φ , prot" := (TSR' Receive Φ prot)
(at level 200, prot at level 200) : proto_scope.
Section proto_enc_specs.
Context `{!heapG Σ, !logrelG val Σ} `{ValEncDec A} (N : namespace).
Lemma send_st_spec prot γ c s (P : A iProp Σ) w :
{{{ P w c @ s : <!> @ P, prot {N,γ} }}}
Lemma send_st_spec prot γ c s (Φ : A iProp Σ) w :
{{{ Φ w c @ s : <!> @ Φ, prot {N,γ} }}}
send c #s (val_encode w)
{{{ RET #(); c @ s : prot w {N,γ} }}}.
Proof.
iIntros (Φ) "[HP Hsend] HΦ".
iApply (send_st_spec with "[HP $Hsend]").
iIntros (Ψ) "[HΦ Hsend] HΨ".
iApply (send_st_spec with "[HΦ $Hsend]").
{ by rewrite val_encode_decode. }
iNext. rewrite val_encode_decode.
by iApply "HΦ".
by iApply "HΨ".
Qed.
Lemma recv_st_spec prot γ c s (P : A iProp Σ) :
{{{ c @ s : <?> @ P, prot {N,γ} }}}
Lemma recv_st_spec prot γ c s (Φ : A iProp Σ) :
{{{ c @ s : <?> @ Φ, prot {N,γ} }}}
recv c #s
{{{ v, RET (val_encode v); c @ s : prot v {N,γ} P v }}}.
{{{ v, RET (val_encode v); c @ s : prot v {N,γ} Φ v }}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
iIntros (Ψ) "Hrecv HΨ".
iApply (recv_st_spec with "Hrecv").
iNext. iIntros (v).
iIntros "[H HP]".
iAssert ( w, val_decode v = Some w P w)%I with "[HP]" as (w Hw) "HP".
iIntros "!>" (v) "[H HΦ]".
iAssert ( w, val_decode v = Some w Φ w)%I with "[HΦ]" as (w Hw) "HΦ".
{ destruct (val_decode v) as [x|]; last done.
iExists x. by iFrame. }
iSpecialize ("HΦ" $!w).
apply val_decode_encode in Hw as <-.
iApply "HΦ". iFrame "HP".
iApply ("HΨ" $!w). iFrame "HΦ".
by rewrite val_encode_decode.
Qed.
End proto_enc_specs.
......@@ -20,7 +20,7 @@ Fixpoint prot_eval `{!logrelG val Σ} (vs : list val) (prot1 prot2 : proto val (
match vs with
| [] => prot1 dual_proto prot2
| v::vs => match prot2 with
| TSR Receive P prot2 => P v prot_eval vs prot1 (prot2 v)
| TSR Receive Φ prot2 => Φ v prot_eval vs prot1 (prot2 v)
| _ => False
end
end%I.
......@@ -67,7 +67,7 @@ Section proto.
Global Instance prot_eval_ne : NonExpansive2 (prot_eval vs).
Proof.
induction vs as [|v vs IH];
destruct 2 as [n|[] P1 P2 prot1 prot2|n [] P1 P2 prot1 prot2]=> //=.
destruct 2 as [n|[] Φ1 Φ2 prot1 prot2|n [] Φ1 Φ2 prot1 prot2]=> //=.
- by repeat f_equiv.
- f_equiv. done. f_equiv. by constructor.
- f_equiv. done. f_equiv. by constructor.
......@@ -114,24 +114,24 @@ Section proto.
by rewrite own_op.
Qed.
Lemma prot_eval_send (P : val iProp Σ) prot vs v protr :
P v - prot_eval vs (<!> @ P, prot) protr - prot_eval (vs ++ [v]) (prot v) protr.
Lemma prot_eval_send (Φ : val iProp Σ) prot vs v protr :
Φ v - prot_eval vs (<!> @ Φ, prot) protr - prot_eval (vs ++ [v]) (prot v) protr.
Proof.
iIntros "HP".
iIntros "HΦ".
iRevert (protr).
iInduction vs as [|v' vs] "IH"; iIntros (protr) "Heval".
- iDestruct (dual_proto_flip with "Heval") as "Heval".
iRewrite -"Heval"; simpl.
rewrite dual_proto_involutive.
by iFrame.
- destruct protr as [|[] P' protr]=> //=.
- destruct protr as [|[] Φ' protr]=> //=.
iDestruct "Heval" as "[$ Heval]".
by iApply ("IH" with "HP").
by iApply ("IH" with "HΦ").
Qed.
Lemma prot_eval_recv (P : val iProp Σ) prot1 l prot2 v :
prot_eval (v :: l) prot1 (<?> @ P, prot2) - prot_eval l prot1 (prot2 v) P v.
Proof. iDestruct 1 as "[HP Heval]". iFrame. Qed.
Lemma prot_eval_recv (Φ : val iProp Σ) prot1 l prot2 v :
prot_eval (v :: l) prot1 (<?> @ Φ, prot2) - prot_eval l prot1 (prot2 v) Φ v.
Proof. iDestruct 1 as "[HΦ Heval]". iFrame. Qed.
Lemma new_chan_vs prot E c cγ :
is_chan N cγ c
......@@ -175,11 +175,11 @@ Section proto.
by iFrame.
Qed.
Lemma send_vs c γ s (P : val iProp Σ) prot E :
Lemma send_vs c γ s (Φ : val iProp Σ) prot E :
N E
c @ s : TSR Send P prot {N,γ} ={E,E∖↑N}= vs,
c @ s : <!> @ Φ, prot {N,γ} ={E,E∖↑N}= vs,
chan_own (prot_c_name γ) s vs
v, P v -
v, Φ v -
chan_own (prot_c_name γ) s (vs ++ [v]) ={E∖↑N,E}=
c @ s : prot v {N,γ}.
Proof.
......@@ -188,7 +188,7 @@ Section proto.
iModIntro.
destruct s.
- iExists _.
iIntros "{$Hclf} !>" (v) "HP Hclf".
iIntros "{$Hclf} !>" (v) "HΦ Hclf".
iRename "Hstf" into "Hstlf".
iDestruct (prot_excl_eq with "Hstla Hstlf") as "#Heq".
iMod (prot_excl_update _ _ _ _ (prot v) with "Hstla Hstlf") as "[Hstla Hstlf]".
......@@ -198,14 +198,14 @@ Section proto.
iLeft.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- iSplit=> //.
iApply (prot_eval_send with "HP").
iApply (prot_eval_send with "HΦ").
by iRewrite "Heq" in "Heval".
- iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //=.
iSplit; first done.
iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_proto_involutive. }
iRewrite "Heval". simpl. iFrame "HΦ". by rewrite dual_proto_involutive. }
iModIntro. iFrame. auto.
- iExists _.
iIntros "{$Hcrf} !>" (v) "HP Hcrf".
iIntros "{$Hcrf} !>" (v) "HΦ Hcrf".
iRename "Hstf" into "Hstrf".
iDestruct (prot_excl_eq with "Hstra Hstrf") as "#Heq".
iMod (prot_excl_update _ _ _ _ (prot v) with "Hstra Hstrf") as "[Hstra Hstrf]".
......@@ -216,38 +216,38 @@ Section proto.
iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
- iRewrite "Heq" in "Heval". destruct l as [|vl l]=> //.
iSplit; first done. simpl.
iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_proto_involutive.
iRewrite "Heval". simpl. iFrame "HΦ". by rewrite dual_proto_involutive.
- iSplit=> //.
iApply (prot_eval_send with "HP").
iApply (prot_eval_send with "HΦ").
by iRewrite "Heq" in "Heval". }
iModIntro. iFrame. auto.
Qed.
Lemma send_st_spec prot γ c s (P : val iProp Σ) v :
{{{ P v c @ s : <!> @ P , prot {N,γ} }}}
Lemma send_st_spec prot γ c s (Φ : val iProp Σ) v :
{{{ Φ v c @ s : <!> @ Φ, prot {N,γ} }}}
send c #s v
{{{ RET #(); c @ s : prot v {N,γ} }}}.
Proof.
iIntros (Φ) "[HP Hsend] HΦ".
iIntros (Ψ) "[HΦ Hsend] HΨ".
iApply (send_spec with "[#]").
{ iDestruct "Hsend" as "[? [$ ?]]". }
iMod (send_vs with "Hsend") as (vs) "[Hch H]"; first done.
iModIntro. iExists vs. iFrame "Hch".
iIntros "!> Hupd". iApply "HΦ".
iApply ("H" $! v with "HP"). by destruct s.
iIntros "!> Hupd". iApply "HΨ".
iApply ("H" $! v with "HΦ"). by destruct s.
Qed.
Lemma try_recv_vs c γ s (P : val iProp Σ) prot E :
Lemma try_recv_vs c γ s (Φ : val iProp Σ) prot E :
N E
c @ s : TSR Receive P prot {N,γ} ={E,E∖↑N}= vs,
c @ s : TSR Receive Φ prot {N,γ} ={E,E∖↑N}= vs,
chan_own (prot_c_name γ) (dual_side s) vs
((vs = [] -
chan_own (prot_c_name γ) (dual_side s) vs ={E∖↑N,E}=
c @ s : TSR Receive P prot {N,γ})
c @ s : <?> @ Φ, prot {N,γ})
( v vs',
vs = v :: vs' -
chan_own (prot_c_name γ) (dual_side s) vs' ={E∖↑N,E}=
c @ s : (prot v) {N,γ} P v)).
c @ s : prot v {N,γ} Φ v)).
Proof.
iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
iInv N as (l r protl protr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
......@@ -295,13 +295,13 @@ Section proto.
iNext. by iRewrite -("HPeq" $! v).
Qed.
Lemma try_recv_st_spec prot γ c s (P : val iProp Σ) :
{{{ c @ s : <?> @ P , prot {N,γ} }}}
Lemma try_recv_st_spec prot γ c s (Φ : val iProp Σ) :
{{{ c @ s : <?> @ Φ, prot {N,γ} }}}
try_recv c #s
{{{ v, RET v; (v = NONEV c @ s : <?> @ P, prot {N,γ})
( w, v = SOMEV w c @ s : prot w {N,γ} P w)}}}.
{{{ v, RET v; (v = NONEV c @ s : <?> @ Φ, prot {N,γ})
( w, v = SOMEV w c @ s : prot w {N,γ} Φ w)}}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
iIntros (Ψ) "Hrecv HΨ".
iApply (try_recv_spec with "[#]").
{ iDestruct "Hrecv" as "[? [$ ?]]". }
iMod (try_recv_vs with "Hrecv") as (vs) "[Hch H]"; first done.
......@@ -312,27 +312,27 @@ Section proto.
iDestruct "H" as "[H _]".
iMod ("H" $!Hvs with "Hown") as "H".
iModIntro.
iApply "HΦ"=> //.
iApply "HΨ"=> //.
eauto with iFrame.
- iIntros (v vs' Hvs) "Hown".
iDestruct "H" as "[_ H]".
iMod ("H" $!v vs' Hvs with "Hown") as "H".
iModIntro.
iApply "HΦ"; eauto with iFrame.
iApply "HΨ"; eauto with iFrame.
Qed.
Lemma recv_st_spec prot γ c s (P : val iProp Σ) :
{{{ c @ s : <?> @ P , prot {N,γ} }}}
Lemma recv_st_spec prot γ c s (Φ : val iProp Σ) :
{{{ c @ s : <?> @ Φ, prot {N,γ} }}}
recv c #s
{{{ v, RET v; c @ s : prot v {N,γ} P v }}}.
{{{ v, RET v; c @ s : prot v {N,γ} Φ v }}}.
Proof.
iIntros (Φ) "Hrecv HΦ".
iIntros (Ψ) "Hrecv HΨ".
iLöb as "IH". wp_rec.
wp_apply (try_recv_st_spec with "Hrecv").
iIntros (v) "H".
iDestruct "H" as "[[-> H]| H]".
- wp_pures. by iApply ("IH" with "[H]").
- iDestruct "H" as (w ->) "[H HP]".
wp_pures. iApply "HΦ". iFrame.
- iDestruct "H" as (w ->) "[H HΦ]".
wp_pures. iApply "HΨ". iFrame.
Qed.
End proto.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment