Commit 16e1b090 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix namespace for proto.

parent fbdbf1e6
...@@ -48,7 +48,7 @@ Notation ProtoUnfold p1 p2 := (∀ d pas q, ...@@ -48,7 +48,7 @@ Notation ProtoUnfold p1 p2 := (∀ d pas q,
ProtoNormalize d p2 pas q ProtoNormalize d p1 pas q). ProtoNormalize d p2 pas q ProtoNormalize d p1 pas q).
Section classes. Section classes.
Context `{!proto_chanG Σ, !heapG Σ} (N : namespace). Context `{!proto_chanG Σ, !heapG Σ}.
Implicit Types p : iProto Σ. Implicit Types p : iProto Σ.
Implicit Types TT : tele. Implicit Types TT : tele.
...@@ -139,14 +139,14 @@ Section classes. ...@@ -139,14 +139,14 @@ Section classes.
(** Automatically perform normalization of protocols in the proof mode *) (** Automatically perform normalization of protocols in the proof mode *)
Global Instance mapsto_proto_from_assumption q c p1 p2 : Global Instance mapsto_proto_from_assumption q c p1 p2 :
ProtoNormalize false p1 [] p2 ProtoNormalize false p1 [] p2
FromAssumption q (c p1 @ N) (c p2 @ N). FromAssumption q (c p1) (c p2).
Proof. Proof.
rewrite /FromAssumption /ProtoNormalize=> ->. rewrite /FromAssumption /ProtoNormalize=> ->.
by rewrite /= right_id bi.intuitionistically_if_elim. by rewrite /= right_id bi.intuitionistically_if_elim.
Qed. Qed.
Global Instance mapsto_proto_from_frame q c p1 p2 : Global Instance mapsto_proto_from_frame q c p1 p2 :
ProtoNormalize false p1 [] p2 ProtoNormalize false p1 [] p2
Frame q (c p1 @ N) (c p2 @ N) True. Frame q (c p1) (c p2) True.
Proof. Proof.
rewrite /Frame /ProtoNormalize=> ->. rewrite /Frame /ProtoNormalize=> ->.
by rewrite /= !right_id bi.intuitionistically_if_elim. by rewrite /= !right_id bi.intuitionistically_if_elim.
...@@ -155,14 +155,14 @@ End classes. ...@@ -155,14 +155,14 @@ End classes.
(** Symbolic execution tactics *) (** Symbolic execution tactics *)
(* TODO: strip laters *) (* TODO: strip laters *)
Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K N Lemma tac_wp_recv `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ i j K
c p (pc : TT val * iProp Σ * iProto Σ) Φ : c p (pc : TT val * iProp Σ * iProto Σ) Φ :
envs_lookup i Δ = Some (false, c p @ N)%I envs_lookup i Δ = Some (false, c p)%I
ProtoNormalize false p [] (iProto_message Receive pc) ProtoNormalize false p [] (iProto_message Receive pc)
let Δ' := envs_delete false i false Δ in let Δ' := envs_delete false i false Δ in
(.. x : TT, (.. x : TT,
match envs_app false match envs_app false
(Esnoc (Esnoc Enil j ((pc x).1.2)) i (c (pc x).2 @ N)) Δ' with (Esnoc (Esnoc Enil j ((pc x).1.2)) i (c (pc x).2)) Δ' with
| Some Δ'' => envs_entails Δ'' (WP fill K (of_val (pc x).1.1) {{ Φ }}) | Some Δ'' => envs_entails Δ'' (WP fill K (of_val (pc x).1.1) {{ Φ }})
| None => False | None => False
end) end)
...@@ -179,7 +179,7 @@ Qed. ...@@ -179,7 +179,7 @@ Qed.
Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) := Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
let solve_mapsto _ := let solve_mapsto _ :=
let c := match goal with |- _ = Some (_, (?c _ @ _)%I) => c end in let c := match goal with |- _ = Some (_, (?c _)%I) => c end in
iAssumptionCore || fail "wp_recv: cannot find" c "↣ ? @ ?" in iAssumptionCore || fail "wp_recv: cannot find" c "↣ ? @ ?" in
wp_pures; wp_pures;
let Hnew := iFresh in let Hnew := iFresh in
...@@ -233,15 +233,15 @@ Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropat ...@@ -233,15 +233,15 @@ Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropat
simple_intropattern(x8) ")" constr(pat) := simple_intropattern(x8) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat). wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K N Lemma tac_wp_send `{!proto_chanG Σ, !heapG Σ} {TT : tele} Δ neg i js K
c v p (pc : TT val * iProp Σ * iProto Σ) Φ : c v p (pc : TT val * iProp Σ * iProto Σ) Φ :
envs_lookup i Δ = Some (false, c p @ N)%I envs_lookup i Δ = Some (false, c p)%I
ProtoNormalize false p [] (iProto_message Send pc) ProtoNormalize false p [] (iProto_message Send pc)
let Δ' := envs_delete false i false Δ in let Δ' := envs_delete false i false Δ in
(.. x : TT, (.. x : TT,
match envs_split (if neg is true then Right else Left) js Δ' with match envs_split (if neg is true then Right else Left) js Δ' with
| Some (Δ1,Δ2) => | Some (Δ1,Δ2) =>
match envs_app false (Esnoc Enil i (c (pc x).2 @ N)) Δ2 with match envs_app false (Esnoc Enil i (c (pc x).2)) Δ2 with
| Some Δ2' => | Some Δ2' =>
v = (pc x).1.1 v = (pc x).1.1
envs_entails Δ1 (pc x).1.2 envs_entails Δ1 (pc x).1.2
...@@ -265,7 +265,7 @@ Qed. ...@@ -265,7 +265,7 @@ Qed.
Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) := Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
let solve_mapsto _ := let solve_mapsto _ :=
let c := match goal with |- _ = Some (_, (?c _ @ _)%I) => c end in let c := match goal with |- _ = Some (_, (?c _)%I) => c end in
iAssumptionCore || fail "wp_send: cannot find" c "↣ ? @ ?" in iAssumptionCore || fail "wp_send: cannot find" c "↣ ? @ ?" in
let solve_done d := let solve_done d :=
lazymatch d with lazymatch d with
...@@ -327,14 +327,14 @@ Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ") ...@@ -327,14 +327,14 @@ Tactic Notation "wp_send" "(" uconstr(x1) uconstr(x2) uconstr(x3) uconstr(x4) ")
wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5; wp_send_core (eexists x1; eexists x2; eexists x3; eexists x4; eexists x5;
eexists x6; eexists x7; eexists x8) with pat. eexists x6; eexists x7; eexists x8) with pat.
Lemma tac_wp_branch `{!proto_chanG Σ, !heapG Σ} Δ i j K N Lemma tac_wp_branch `{!proto_chanG Σ, !heapG Σ} Δ i j K
c p P1 P2 (p1 p2 : iProto Σ) Φ : c p P1 P2 (p1 p2 : iProto Σ) Φ :
envs_lookup i Δ = Some (false, c p @ N)%I envs_lookup i Δ = Some (false, c p)%I
ProtoNormalize false p [] (p1 <{P1}&{P2}> p2) ProtoNormalize false p [] (p1 <{P1}&{P2}> p2)
let Δ' := envs_delete false i false Δ in let Δ' := envs_delete false i false Δ in
( b : bool, ( b : bool,
match envs_app false match envs_app false
(Esnoc (Esnoc Enil j (if b then P1 else P2)) i (c (if b then p1 else p2) @ N)) Δ' with (Esnoc (Esnoc Enil j (if b then P1 else P2)) i (c (if b then p1 else p2))) Δ' with
| Some Δ'' => envs_entails Δ'' (WP fill K (of_val #b) {{ Φ }}) | Some Δ'' => envs_entails Δ'' (WP fill K (of_val #b) {{ Φ }})
| None => False | None => False
end) end)
...@@ -350,7 +350,7 @@ Qed. ...@@ -350,7 +350,7 @@ Qed.
Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) := Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) :=
let solve_mapsto _ := let solve_mapsto _ :=
let c := match goal with |- _ = Some (_, (?c _ @ _)%I) => c end in let c := match goal with |- _ = Some (_, (?c _)%I) => c end in
iAssumptionCore || fail "wp_branch: cannot find" c "↣ ? @ ?" in iAssumptionCore || fail "wp_branch: cannot find" c "↣ ? @ ?" in
wp_pures; wp_pures;
let Hnew := iFresh in let Hnew := iFresh in
...@@ -375,14 +375,14 @@ Tactic Notation "wp_branch" "as" "%" intropattern(pat1) "|" "%" intropattern(pat ...@@ -375,14 +375,14 @@ Tactic Notation "wp_branch" "as" "%" intropattern(pat1) "|" "%" intropattern(pat
wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2). wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2).
Tactic Notation "wp_branch" := wp_branch as %_ | %_. Tactic Notation "wp_branch" := wp_branch as %_ | %_.
Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K N Lemma tac_wp_select `{!proto_chanG Σ, !heapG Σ} Δ neg i js K
c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ : c (b : bool) p P1 P2 (p1 p2 : iProto Σ) Φ :
envs_lookup i Δ = Some (false, c p @ N)%I envs_lookup i Δ = Some (false, c p)%I
ProtoNormalize false p [] (p1 <{P1}+{P2}> p2) ProtoNormalize false p [] (p1 <{P1}+{P2}> p2)
let Δ' := envs_delete false i false Δ in let Δ' := envs_delete false i false Δ in
match envs_split (if neg is true then Right else Left) js Δ' with match envs_split (if neg is true then Right else Left) js Δ' with
| Some (Δ1,Δ2) => | Some (Δ1,Δ2) =>
match envs_app false (Esnoc Enil i (c if b then p1 else p2 @ N)) Δ2 with match envs_app false (Esnoc Enil i (c if b then p1 else p2)) Δ2 with
| Some Δ2' => | Some Δ2' =>
envs_entails Δ1 (if b then P1 else P2) envs_entails Δ1 (if b then P1 else P2)
envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }}) envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }})
...@@ -404,7 +404,7 @@ Qed. ...@@ -404,7 +404,7 @@ Qed.
Tactic Notation "wp_select" "with" constr(pat) := Tactic Notation "wp_select" "with" constr(pat) :=
let solve_mapsto _ := let solve_mapsto _ :=
let c := match goal with |- _ = Some (_, (?c _ @ _)%I) => c end in let c := match goal with |- _ = Some (_, (?c _)%I) => c end in
iAssumptionCore || fail "wp_select: cannot find" c "↣ ? @ ?" in iAssumptionCore || fail "wp_select: cannot find" c "↣ ? @ ?" in
let solve_done d := let solve_done d :=
lazymatch d with lazymatch d with
......
...@@ -191,22 +191,24 @@ Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ := ...@@ -191,22 +191,24 @@ Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ :=
((r = [] proto_eval l pl pr) ((r = [] proto_eval l pl pr)
(l = [] proto_eval r pr pl)))%I. (l = [] proto_eval r pr pl)))%I.
Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ} (N : namespace) Definition protoN := nroot .@ "proto".
Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
(c : val) (p : iProto Σ) : iProp Σ := (c : val) (p : iProto Σ) : iProp Σ :=
( s (c1 c2 : val) γ, ( s (c1 c2 : val) γ,
c = side_elim s c1 c2 c = side_elim s c1 c2
proto_own_frag γ s p is_chan N (proto_c_name γ) c1 c2 inv N (proto_inv γ))%I. proto_own_frag γ s p is_chan protoN (proto_c_name γ) c1 c2 inv protoN (proto_inv γ))%I.
Definition mapsto_proto_aux : seal (@mapsto_proto_def). by eexists. Qed. Definition mapsto_proto_aux : seal (@mapsto_proto_def). by eexists. Qed.
Definition mapsto_proto {Σ pΣ hΣ} := mapsto_proto_aux.(unseal) Σ pΣ hΣ. Definition mapsto_proto {Σ pΣ hΣ} := mapsto_proto_aux.(unseal) Σ pΣ hΣ.
Definition mapsto_proto_eq : @mapsto_proto = @mapsto_proto_def := mapsto_proto_aux.(seal_eq). Definition mapsto_proto_eq : @mapsto_proto = @mapsto_proto_def := mapsto_proto_aux.(seal_eq).
Arguments mapsto_proto {_ _ _} _ _ _%proto. Arguments mapsto_proto {_ _ _} _ _%proto.
Instance: Params (@mapsto_proto) 5 := {}. Instance: Params (@mapsto_proto) 4 := {}.
Notation "c ↣ p @ N" := (mapsto_proto N c p) Notation "c ↣ p" := (mapsto_proto c p)
(at level 20, N at level 50, format "c ↣ p @ N"). (at level 20, format "c ↣ p").
Section proto. Section proto.
Context `{!proto_chanG Σ, !heapG Σ} (N : namespace). Context `{!proto_chanG Σ, !heapG Σ}.
Implicit Types p : iProto Σ. Implicit Types p : iProto Σ.
Implicit Types TT : tele. Implicit Types TT : tele.
...@@ -344,9 +346,9 @@ Section proto. ...@@ -344,9 +346,9 @@ Section proto.
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s). Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto N c). Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto c).
Proof. rewrite mapsto_proto_eq. solve_proper. Qed. Proof. rewrite mapsto_proto_eq. solve_proper. Qed.
Global Instance mapsto_proto_proper c : Proper (() ==> ()) (mapsto_proto N c). Global Instance mapsto_proto_proper c : Proper (() ==> ()) (mapsto_proto c).
Proof. apply (ne_proper _). Qed. Proof. apply (ne_proper _). Qed.
Lemma proto_own_auth_agree γ s p p' : Lemma proto_own_auth_agree γ s p p' :
...@@ -416,9 +418,9 @@ Section proto. ...@@ -416,9 +418,9 @@ Section proto.
(** The actual specs *) (** The actual specs *)
Lemma proto_init E cγ c1 c2 p : Lemma proto_init E cγ c1 c2 p :
is_chan N cγ c1 c2 - is_chan protoN cγ c1 c2 -
chan_own cγ Left [] - chan_own cγ Right [] ={E}= chan_own cγ Left [] - chan_own cγ Right [] ={E}=
c1 p @ N c2 iProto_dual p @ N. c1 p c2 iProto_dual p.
Proof. Proof.
iIntros "#Hcctx Hcol Hcor". iIntros "#Hcctx Hcol Hcor".
iMod (own_alloc ( (to_proto_auth_excl p) iMod (own_alloc ( (to_proto_auth_excl p)
...@@ -428,7 +430,7 @@ Section proto. ...@@ -428,7 +430,7 @@ Section proto.
(to_proto_auth_excl (iProto_dual p)))) as (rγ) "[Hrsta Hrstf]". (to_proto_auth_excl (iProto_dual p)))) as (rγ) "[Hrsta Hrstf]".
{ by apply auth_both_valid_2. } { by apply auth_both_valid_2. }
pose (ProtName cγ lγ rγ) as pγ. pose (ProtName cγ lγ rγ) as pγ.
iMod (inv_alloc N _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv". iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
{ iNext. rewrite /proto_inv. eauto 10 with iFrame. } { iNext. rewrite /proto_inv. eauto 10 with iFrame. }
iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf". iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
- iExists Left, c1, c2, pγ; iFrame; auto. - iExists Left, c1, c2, pγ; iFrame; auto.
...@@ -437,20 +439,20 @@ Section proto. ...@@ -437,20 +439,20 @@ Section proto.
(** Accessor style lemmas *) (** Accessor style lemmas *)
Lemma proto_send_acc {TT} E c (pc : TT val * iProp Σ * iProto Σ) : Lemma proto_send_acc {TT} E c (pc : TT val * iProp Σ * iProto Σ) :
N E protoN E
c iProto_message Send pc @ N - s c1 c2 γ, c iProto_message Send pc - s c1 c2 γ,
c = side_elim s c1 c2 c = side_elim s c1 c2
is_chan N (proto_c_name γ) c1 c2 |={E,E∖↑N}=> vs, is_chan protoN (proto_c_name γ) c1 c2 |={E,E∖↑protoN}=> vs,
chan_own (proto_c_name γ) s vs chan_own (proto_c_name γ) s vs
(x : TT), (x : TT),
(pc x).1.2 - (pc x).1.2 -
chan_own (proto_c_name γ) s (vs ++ [(pc x).1.1]) ={E∖↑N,E}= chan_own (proto_c_name γ) s (vs ++ [(pc x).1.1]) ={E∖↑protoN,E}=
c (pc x).2 @ N. c (pc x).2.
Proof. Proof.
iIntros (?). rewrite {1}mapsto_proto_eq iProto_message_eq. iIntros (?). rewrite {1}mapsto_proto_eq iProto_message_eq.
iDestruct 1 as (s c1 c2 γ ->) "[Hstf #[Hcctx Hinv]]". iDestruct 1 as (s c1 c2 γ ->) "[Hstf #[Hcctx Hinv]]".
iExists s, c1, c2, γ. iSplit; first done. iFrame "Hcctx". iExists s, c1, c2, γ. iSplit; first done. iFrame "Hcctx".
iInv N as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose". iInv protoN as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
(* TODO: refactor to avoid twice nearly the same proof *) (* TODO: refactor to avoid twice nearly the same proof *)
iModIntro. destruct s. iModIntro. destruct s.
- iExists _. - iExists _.
...@@ -494,23 +496,23 @@ Section proto. ...@@ -494,23 +496,23 @@ Section proto.
Qed. Qed.
Lemma proto_recv_acc {TT} E c (pc : TT val * iProp Σ * iProto Σ) : Lemma proto_recv_acc {TT} E c (pc : TT val * iProp Σ * iProto Σ) :
N E protoN E
c iProto_message Receive pc @ N - s c1 c2 γ, c iProto_message Receive pc - s c1 c2 γ,
c = side_elim s c2 c1 c = side_elim s c2 c1
is_chan N (proto_c_name γ) c1 c2 |={E,E∖↑N}=> vs, is_chan protoN (proto_c_name γ) c1 c2 |={E,E∖↑protoN}=> vs,
chan_own (proto_c_name γ) s vs chan_own (proto_c_name γ) s vs
((chan_own (proto_c_name γ) s vs ={E∖↑N,E}= ((chan_own (proto_c_name γ) s vs ={E∖↑protoN,E}=
c iProto_message Receive pc @ N) c iProto_message Receive pc)
( v vs', ( v vs',
vs = v :: vs' - vs = v :: vs' -
chan_own (proto_c_name γ) s vs' ={E∖↑N,E}= x : TT, chan_own (proto_c_name γ) s vs' ={E∖↑protoN,E}= x : TT,
v = (pc x).1.1 c (pc x).2 @ N (pc x).1.2)). v = (pc x).1.1 c (pc x).2 (pc x).1.2)).
Proof. Proof.
iIntros (?). rewrite {1}mapsto_proto_eq iProto_message_eq. iIntros (?). rewrite {1}mapsto_proto_eq iProto_message_eq.
iDestruct 1 as (s c1 c2 γ ->) "[Hstf #[Hcctx Hinv]]". iDestruct 1 as (s c1 c2 γ ->) "[Hstf #[Hcctx Hinv]]".
iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s. iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
iFrame "Hcctx". iFrame "Hcctx".
iInv N as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose". iInv protoN as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
iExists (side_elim s r l). iModIntro. iExists (side_elim s r l). iModIntro.
(* TODO: refactor to avoid twice nearly the same proof *) (* TODO: refactor to avoid twice nearly the same proof *)
destruct s; simpl. destruct s; simpl.
...@@ -533,7 +535,7 @@ Section proto. ...@@ -533,7 +535,7 @@ Section proto.
iMod ("Hclose" with "[-Hstlf Hf]") as %_. iMod ("Hclose" with "[-Hstlf Hf]") as %_.
{ iExists _, _,_ ,_. eauto 10 with iFrame. } { iExists _, _,_ ,_. eauto 10 with iFrame. }
iIntros "!> !>". iIntros "!> !>".
set (f lp := ( q, lp Next q c1 q @ N)%I). set (f lp := ( q, lp Next q c1 q)%I).
assert (NonExpansive f) by solve_proper. assert (NonExpansive f) by solve_proper.
iDestruct ("Hf" $! (OfeMor f) with "[Hstlf]") as (x) "(Hv & HP & Hf) /=". iDestruct ("Hf" $! (OfeMor f) with "[Hstlf]") as (x) "(Hv & HP & Hf) /=".
{ iExists q. iSplit; first done. rewrite mapsto_proto_eq. { iExists q. iSplit; first done. rewrite mapsto_proto_eq.
...@@ -559,7 +561,7 @@ Section proto. ...@@ -559,7 +561,7 @@ Section proto.
iMod ("Hclose" with "[-Hstrf Hf]") as %_. iMod ("Hclose" with "[-Hstrf Hf]") as %_.
{ iExists _, _, _, _. eauto 10 with iFrame. } { iExists _, _, _, _. eauto 10 with iFrame. }
iIntros "!> !>". iIntros "!> !>".
set (f lp := ( q, lp Next q c2 q @ N)%I). set (f lp := ( q, lp Next q c2 q)%I).
assert (NonExpansive f) by solve_proper. assert (NonExpansive f) by solve_proper.
iDestruct ("Hf" $! (OfeMor f) with "[Hstrf]") as (x) "(Hv & HP & Hf) /=". iDestruct ("Hf" $! (OfeMor f) with "[Hstrf]") as (x) "(Hv & HP & Hf) /=".
{ iExists q. iSplit; first done. rewrite mapsto_proto_eq. { iExists q. iSplit; first done. rewrite mapsto_proto_eq.
...@@ -572,7 +574,7 @@ Section proto. ...@@ -572,7 +574,7 @@ Section proto.
Lemma new_chan_proto_spec : Lemma new_chan_proto_spec :
{{{ True }}} {{{ True }}}
new_chan #() new_chan #()
{{{ c1 c2, RET (c1,c2); ( p, |={}=> c1 p @ N c2 iProto_dual p @ N) }}}. {{{ c1 c2, RET (c1,c2); ( p, |={}=> c1 p c2 iProto_dual p) }}}.
Proof. Proof.
iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //. iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
iIntros (c1 c2 γ) "(Hc & Hl & Hr)". iApply "HΨ"; iIntros "!>" (p). iIntros (c1 c2 γ) "(Hc & Hl & Hr)". iApply "HΨ"; iIntros "!>" (p).
...@@ -580,8 +582,8 @@ Section proto. ...@@ -580,8 +582,8 @@ Section proto.
Qed. Qed.
Lemma start_chan_proto_spec p Ψ (f : val) : Lemma start_chan_proto_spec p Ψ (f : val) :
( c, c iProto_dual p @ N - WP f c {{ _, True }}) - ( c, c iProto_dual p - WP f c {{ _, True }}) -
( c, c p @ N - Ψ c) - ( c, c p - Ψ c) -
WP start_chan f {{ Ψ }}. WP start_chan f {{ Ψ }}.
Proof. Proof.
iIntros "Hfork HΨ". wp_lam. iIntros "Hfork HΨ". wp_lam.
...@@ -593,9 +595,9 @@ Section proto. ...@@ -593,9 +595,9 @@ Section proto.
Qed. Qed.
Lemma send_proto_spec_packed {TT} c (pc : TT val * iProp Σ * iProto Σ) (x : TT) : Lemma send_proto_spec_packed {TT} c (pc : TT val * iProp Σ * iProto Σ) (x : TT) :
{{{ c iProto_message Send pc @ N (pc x).1.2 }}} {{{ c iProto_message Send pc (pc x).1.2 }}}
send c (pc x).1.1 send c (pc x).1.1
{{{ RET #(); c (pc x).2 @ N }}}. {{{ RET #(); c (pc x).2 }}}.
Proof. Proof.
iIntros (Ψ) "[Hp Hf] HΨ". iIntros (Ψ) "[Hp Hf] HΨ".
iDestruct (proto_send_acc with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done. iDestruct (proto_send_acc with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
...@@ -606,9 +608,9 @@ Section proto. ...@@ -606,9 +608,9 @@ Section proto.
Qed. Qed.
Lemma send_proto_spec {TT} Ψ c v (pc : TT val * iProp Σ * iProto Σ) : Lemma send_proto_spec {TT} Ψ c v (pc : TT val * iProp Σ * iProto Σ) :
c iProto_message Send pc @ N - c iProto_message Send pc -
(.. x : TT, (.. x : TT,
v = (pc x).1.1 (pc x).1.2 (c (pc x).2 @ N - Ψ #())) - v = (pc x).1.1 (pc x).1.2 (c (pc x).2 - Ψ #())) -
WP send c v {{ Ψ }}. WP send c v {{ Ψ }}.
Proof. Proof.
iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΨ]". iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΨ]".
...@@ -616,10 +618,10 @@ Section proto. ...@@ -616,10 +618,10 @@ Section proto.
Qed. Qed.
Lemma try_recv_proto_spec_packed {TT} c (pc : TT val * iProp Σ * iProto Σ) : Lemma try_recv_proto_spec_packed {TT} c (pc : TT val * iProp Σ * iProto Σ) :
{{{ c iProto_message Receive pc @ N }}} {{{ c iProto_message Receive pc }}}
try_recv c try_recv c
{{{ v, RET v; (v = NONEV c iProto_message Receive pc @ N) {{{ v, RET v; (v = NONEV c iProto_message Receive pc)
( x : TT, v = SOMEV ((pc x).1.1) c (pc x).2 @ N (pc x).1.2) }}}. ( x : TT, v = SOMEV ((pc x).1.1) c (pc x).2 (pc x).1.2) }}}.
Proof. Proof.
iIntros (Ψ) "Hp HΨ". iIntros (Ψ) "Hp HΨ".
iDestruct (proto_recv_acc with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done. iDestruct (proto_recv_acc with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
...@@ -633,9 +635,9 @@ Section proto. ...@@ -633,9 +635,9 @@ Section proto.
Qed. Qed.
Lemma recv_proto_spec_packed {TT} c (pc : TT val * iProp Σ * iProto Σ) : Lemma recv_proto_spec_packed {TT} c (pc : TT val * iProp Σ * iProto Σ) :
{{{ c iProto_message Receive pc @ N }}} {{{ c iProto_message Receive pc }}}
recv c recv c
{{{ x, RET (pc x).1.1; c (pc x).2 @ N (pc x).1.2 }}}. {{{ x, RET (pc x).1.1; c (pc x).2 (pc x).1.2 }}}.
Proof. Proof.
iIntros (Ψ) "Hp HΨ". iIntros (Ψ) "Hp HΨ".
iDestruct (proto_recv_acc with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done. iDestruct (proto_recv_acc with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
...@@ -646,8 +648,8 @@ Section proto. ...@@ -646,8 +648,8 @@ Section proto.
Qed. Qed.
Lemma recv_proto_spec {TT} Ψ c (pc : TT val * iProp Σ * iProto Σ) : Lemma recv_proto_spec {TT} Ψ c (pc : TT val * iProp Σ * iProto Σ) :
c iProto_message Receive pc @ N - c iProto_message Receive pc -
(.. x : TT, c (pc x).2 @ N - (pc x).1.2 - Ψ (pc x).1.1) - (.. x : TT, c (pc x).2 - (pc x).1.2 - Ψ (pc x).1.1) -
WP recv c {{ Ψ }}. WP recv c {{ Ψ }}.
Proof. Proof.
iIntros "Hc H". iApply (recv_proto_spec_packed with "[$]"). iIntros "Hc H". iApply (recv_proto_spec_packed with "[$]").
...@@ -657,18 +659,18 @@ Section proto. ...@@ -657,18 +659,18 @@ Section proto.