proto_channel.v 29.2 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6
From osiris.channel Require Export channel.
From osiris.channel Require Import proto_model.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth excl.
From osiris.utils Require Import auth_excl.
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10 11 12 13 14 15 16 17 18 19 20 21

(** Camera setup *)
Class proto_chanG Σ := {
  proto_chanG_chanG :> chanG Σ;
  proto_chanG_authG :> auth_exclG (laterO (proto val (iPreProp Σ) (iPreProp Σ))) Σ;
}.

Definition proto_chanΣ := #[
  chanΣ;
  GFunctor (authRF(optionURF (exclRF (laterOF (protoOF val idOF idOF)))))
].
Instance subG_chanΣ {Σ} : subG proto_chanΣ Σ  proto_chanG Σ.
Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
22
(** Types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24 25 26
Definition iProto Σ := proto val (iProp Σ) (iProp Σ).
Delimit Scope proto_scope with proto.
Bind Scope proto_scope with iProto.

Robbert Krebbers's avatar
Robbert Krebbers committed
27 28 29 30 31 32 33 34 35 36 37 38 39 40
(** Operators *)
Definition iProto_end_def {Σ} : iProto Σ := proto_end.
Definition iProto_end_aux : seal (@iProto_end_def). by eexists. Qed.
Definition iProto_end := iProto_end_aux.(unseal).
Definition iProto_end_eq : @iProto_end = @iProto_end_def := iProto_end_aux.(seal_eq).
Arguments iProto_end {_}.

Program Definition iProto_message_def {Σ} {TT : tele} (a : action)
    (pc : TT  val * iProp Σ * iProto Σ) : iProto Σ :=
  proto_message a (λ v, λne f,  x : TT,
    (* Need the laters to make [iProto_message] contractive *)
     v = (pc x).1.1  
     (pc x).1.2 
    f (Next (pc x).2))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
Next Obligation. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
Definition iProto_message := iProto_message_aux.(unseal).
Definition iProto_message_eq : @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
Arguments iProto_message {_ _} _ _%proto.
Instance: Params (@iProto_message) 3.

Notation "<!> x1 .. xn , 'MSG' v {{ P }}; p" :=
  (iProto_message
    (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
    Send
    (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
  (at level 20, x1 binder, xn binder, v at level 20, P, p at level 200) : proto_scope.
Notation "<!> x1 .. xn , 'MSG' v ; p" :=
  (iProto_message
    (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
    Send
    (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
  (at level 20, x1 binder, xn binder, v at level 20, p at level 200) : proto_scope.

Notation "<?> x1 .. xn , 'MSG' v {{ P }}; p" :=
  (iProto_message
    (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
    Receive
    (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
  (at level 20, x1 binder, xn binder, v at level 20, P, p at level 200) : proto_scope.
Notation "<?> x1 .. xn , 'MSG' v ; p" :=
  (iProto_message
    (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
    Receive
    (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
  (at level 20, x1 binder, xn binder, v at level 20, p at level 200) : proto_scope.

Notation "'END'" := iProto_end : proto_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
79

Robbert Krebbers's avatar
Robbert Krebbers committed
80
(** Dual *)
Robbert Krebbers's avatar
Robbert Krebbers committed
81
Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  proto_map action_dual cid cid p.
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84 85 86 87 88
Arguments iProto_dual {_} _%proto.
Instance: Params (@iProto_dual) 1.
Definition iProto_dual_if {Σ} (d : bool) (p : iProto Σ) : iProto Σ :=
  if d then iProto_dual p else p.
Arguments iProto_dual_if {_} _ _%proto.
Instance: Params (@iProto_dual_if) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
89

Robbert Krebbers's avatar
Robbert Krebbers committed
90
(** Branching *)
Robbert Krebbers's avatar
Robbert Krebbers committed
91 92 93
Definition iProto_branch {Σ} (a : action) (p1 p2 : iProto Σ) : iProto Σ :=
  iProto_message a (tele_app (TT:=TeleS (λ _: bool, TeleO))
                             (λ b, (#b, True%I, if b then p1 else p2))).
Robbert Krebbers's avatar
Robbert Krebbers committed
94
Typeclasses Opaque iProto_branch.
95 96
Arguments iProto_branch {_} _ _%proto _%proto.
Instance: Params (@iProto_branch) 2.
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98 99
Infix "<+>" := (iProto_branch Send) (at level 85) : proto_scope.
Infix "<&>" := (iProto_branch Receive) (at level 85) : proto_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
(** Append *)
Definition iProto_app {Σ} (p1 p2 : iProto Σ) : iProto Σ := proto_app p1 p2.
Arguments iProto_app {_} _%proto _%proto.
Instance: Params (@iProto_app) 1.
Infix "<++>" := iProto_app (at level 60) : proto_scope.

(** Classes *)
Class ActionDualIf (d : bool) (a1 a2 : action) :=
  dual_action_if : a2 = if d then action_dual a1 else a1.
Hint Mode ActionDualIf ! ! - : typeclass_instances.

Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
Instance action_dual_if_true_send : ActionDualIf true Send Receive := eq_refl.
Instance action_dual_if_true_receive : ActionDualIf true Receive Send := eq_refl.

Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
    (pas : list (bool * iProto Σ)) (q : iProto Σ) :=
  proto_normalize :
    q  (iProto_dual_if d p <++>
         foldr (iProto_app  curry iProto_dual_if) END pas)%proto.
Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
Arguments ProtoNormalize {_} _ _%proto _%proto _%proto.

Class ProtoContNormalize {Σ TT} (d : bool) (pc : TT  val * iProp Σ * iProto Σ)
    (pas : list (bool * iProto Σ)) (qc : TT  val * iProp Σ * iProto Σ) :=
  proto_cont_normalize x :
    (qc x).1.1 = (pc x).1.1 
    (qc x).1.2  (pc x).1.2 
    ProtoNormalize d ((pc x).2) pas ((qc x).2).
Hint Mode ProtoContNormalize ! ! ! ! ! - : typeclass_instances.

(** Auxiliary definitions and invariants *)
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133
Fixpoint proto_eval `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
  match vs with
Robbert Krebbers's avatar
Robbert Krebbers committed
134
  | [] => p1  iProto_dual p2
Robbert Krebbers's avatar
Robbert Krebbers committed
135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167
  | v :: vs =>  pc p2',
     p2  (proto_message Receive pc)%proto 
     ( f : laterO (iProto Σ) -n> iProp Σ, f (Next p2') - pc v f) 
      proto_eval vs p1 p2'
  end%I.
Arguments proto_eval {_ _} _ _%proto _%proto : simpl nomatch.

Record proto_name := ProtName {
  proto_c_name : chan_name;
  proto_l_name : gname;
  proto_r_name : gname
}.

Definition to_proto_auth_excl `{!proto_chanG Σ} (p : iProto Σ) :=
  to_auth_excl (Next (proto_map id iProp_fold iProp_unfold p)).

Definition proto_own_frag `{!proto_chanG Σ} (γ : proto_name) (s : side)
    (p : iProto Σ) : iProp Σ :=
  own (side_elim s proto_l_name proto_r_name γ) ( to_proto_auth_excl p)%I.

Definition proto_own_auth `{!proto_chanG Σ} (γ : proto_name) (s : side)
    (p : iProto Σ) : iProp Σ :=
  own (side_elim s proto_l_name proto_r_name γ) ( to_proto_auth_excl p)%I.

Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ :=
  ( l r pl pr,
    chan_own (proto_c_name γ) Left l 
    chan_own (proto_c_name γ) Right r 
    proto_own_auth γ Left pl 
    proto_own_auth γ Right pr 
     ((r = []  proto_eval l pl pr) 
       (l = []  proto_eval r pr pl)))%I.

Robbert Krebbers's avatar
Robbert Krebbers committed
168
Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ} (N : namespace)
Robbert Krebbers's avatar
Robbert Krebbers committed
169 170 171 172
    (c : val) (p : iProto Σ) : iProp Σ :=
  ( s (c1 c2 : val) γ,
     c = side_elim s c1 c2  
    proto_own_frag γ s p  is_chan N (proto_c_name γ) c1 c2  inv N (proto_inv γ))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174 175 176 177
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_eq : @mapsto_proto = @mapsto_proto_def := mapsto_proto_aux.(seal_eq).
Arguments mapsto_proto {_ _ _} _ _ _%proto.
Instance: Params (@mapsto_proto) 5 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
178

Robbert Krebbers's avatar
Robbert Krebbers committed
179
Notation "c ↣ p @ N" := (mapsto_proto N c p)
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181 182 183
  (at level 20, N at level 50, format "c  ↣  p  @  N").

Section proto.
  Context `{!proto_chanG Σ, !heapG Σ} (N : namespace).
Robbert Krebbers's avatar
Robbert Krebbers committed
184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
  Implicit Types p : iProto Σ.
  Implicit Types TT : tele.

  (** Non-expansiveness of operators *)
  Lemma iProto_message_contractive {TT} a
      (pc1 pc2 : TT  val * iProp Σ * iProto Σ) n :
    (.. x, (pc1 x).1.1 = (pc2 x).1.1) 
    (.. x, dist_later n ((pc1 x).1.2) ((pc2 x).1.2)) 
    (.. x, dist_later n ((pc1 x).2) ((pc2 x).2)) 
    iProto_message a pc1 {n} iProto_message a pc2.
  Proof.
    rewrite !tforall_forall=> Hv HP Hp.
    rewrite iProto_message_eq /iProto_message_def.
    f_equiv=> v f /=. apply bi.exist_ne=> x.
    repeat (apply Hv || apply HP || apply Hp || f_contractive || f_equiv).
  Qed.
  Lemma iProto_message_ne {TT} a
      (pc1 pc2 : TT  val * iProp Σ * iProto Σ) n :
    (.. x, (pc1 x).1.1 = (pc2 x).1.1) 
    (.. x, (pc1 x).1.2 {n} (pc2 x).1.2) 
    (.. x, (pc1 x).2 {n} (pc2 x).2) 
    iProto_message a pc1 {n} iProto_message a pc2.
  Proof.
    rewrite !tforall_forall=> Hv HP Hp.
    apply iProto_message_contractive; apply tforall_forall; eauto using dist_dist_later.
  Qed.
  Lemma iProto_message_proper {TT} a
      (pc1 pc2 : TT  val * iProp Σ * iProto Σ) :
    (.. x, (pc1 x).1.1 = (pc2 x).1.1) 
    (.. x, (pc1 x).1.2  (pc2 x).1.2) 
    (.. x, (pc1 x).2  (pc2 x).2) 
    iProto_message a pc1  iProto_message a pc2.
  Proof.
    rewrite !tforall_forall=> Hv HP Hp. apply equiv_dist => n.
    apply iProto_message_ne; apply tforall_forall=> x; by try apply equiv_dist.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
220

Robbert Krebbers's avatar
Robbert Krebbers committed
221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
  Global Instance iProto_branch_contractive n a :
    Proper (dist_later n ==> dist_later n ==> dist n) (@iProto_branch Σ a).
  Proof.
    intros p1 p1' Hp1 p2 p2' Hp2.
    apply iProto_message_contractive=> /= -[] //.
  Qed.
  Global Instance iProto_branch_ne a : NonExpansive2 (@iProto_branch Σ a).
  Proof.
    intros n p1 p1' Hp1 p2 p2' Hp2. by apply iProto_message_ne=> /= -[].
  Qed.
  Global Instance iProto_branch_proper a :
    Proper (() ==> () ==> ()) (@iProto_branch Σ a).
  Proof. apply (ne_proper_2 _). Qed.

  (** Dual *)
  Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
237
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
238
  Global Instance iProto_dual_proper : Proper (() ==> ()) (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
239
  Proof. apply (ne_proper _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
240 241

  Global Instance iProto_dual_involutive : Involutive () (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
242
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
    intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
Robbert Krebbers's avatar
Robbert Krebbers committed
244 245
    apply: proto_map_ext=> //. by intros [].
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278

  Lemma iProto_dual_end : iProto_dual (Σ:=Σ) END  END%proto.
  Proof. by rewrite iProto_end_eq /iProto_dual proto_map_end. Qed.
  Lemma iProto_dual_message {TT} a (pc : TT  val * iProp Σ * iProto Σ) :
    iProto_dual (iProto_message a pc)
     iProto_message (action_dual a) (prod_map id iProto_dual  pc).
  Proof.
    rewrite /iProto_dual iProto_message_eq /iProto_message_def proto_map_message.
    by f_equiv=> v f /=.
  Qed.

  Lemma iProto_dual_branch a p1 p2 :
    iProto_dual (iProto_branch a p1 p2)
     iProto_branch (action_dual a) (iProto_dual p1) (iProto_dual p2).
  Proof.
    rewrite /iProto_branch iProto_dual_message /=.
    by apply iProto_message_proper=> /= -[].
  Qed.

  (** Append *)
  Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ).
  Proof. apply _. Qed.
  Global Instance iProto_app_proper : Proper (() ==> () ==> ()) (@iProto_app Σ).
  Proof. apply (ne_proper_2 _). Qed.

  Lemma iProto_app_message {TT} a (pc : TT  val * iProp Σ * iProto Σ) p2 :
    (iProto_message a pc <++> p2)%proto  iProto_message a (prod_map id (flip iProto_app p2)  pc).
  Proof.
    rewrite /iProto_app iProto_message_eq /iProto_message_def proto_app_message.
    by f_equiv=> v f /=.
  Qed.

  Global Instance iProto_app_end_l : LeftId () END%proto (@iProto_app Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
279
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
280 281 282
    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_l.
  Qed.
  Global Instance iProto_app_end_r : RightId () END%proto (@iProto_app Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
283
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
284
    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315
  Global Instance iProto_app_assoc : Assoc () (@iProto_app Σ).
  Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.

  Lemma iProto_dual_app p1 p2 :
    iProto_dual (p1 <++> p2)  (iProto_dual p1 <++> iProto_dual p2)%proto.
  Proof. by rewrite /iProto_dual /iProto_app proto_map_app. Qed.

  (** Classes *)
  Global Instance proto_normalize_done p : ProtoNormalize false p [] p | 0.
  Proof. by rewrite /ProtoNormalize /= right_id. Qed. 
  Global Instance proto_normalize_done_dual p :
    ProtoNormalize true p [] (iProto_dual p) | 0.
  Proof. by rewrite /ProtoNormalize /= right_id. Qed.

  Global Instance proto_normalize_dual d p pas q :
    ProtoNormalize (negb d) p pas q 
    ProtoNormalize d (iProto_dual p) pas q.
  Proof. rewrite /ProtoNormalize=> ->. by destruct d; rewrite /= ?involutive. Qed.

  Global Instance proto_normalize_app_l d p1 p2 pas q :
    ProtoNormalize d p1 ((d,p2) :: pas) q 
    ProtoNormalize d (p1 <++> p2) pas q.
  Proof.
    rewrite /ProtoNormalize=> -> /=. rewrite assoc.
    by destruct d; by rewrite /= ?iProto_dual_app.
  Qed.

  Global Instance proto_normalize_end d d' p pas q :
    ProtoNormalize d p pas q 
    ProtoNormalize d' END ((d,p) :: pas) q | 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
316
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
317 318
    rewrite /ProtoNormalize=> -> /=.
    destruct d'; by rewrite /= ?iProto_dual_end left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
319 320
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340
  Global Instance proto_normalize_app_r d p1 p2 pas q :
    ProtoNormalize d p2 pas q 
    ProtoNormalize false p1 ((d,p2) :: pas) (p1 <++> q) | 10.
  Proof. by rewrite /ProtoNormalize=> -> /=. Qed.

  Global Instance proto_normalize_app_r_dual d p1 p2 pas q :
    ProtoNormalize d p2 pas q 
    ProtoNormalize true p1 ((d,p2) :: pas) (iProto_dual p1 <++> q) | 10.
  Proof. by rewrite /ProtoNormalize=> -> /=. Qed.

  Global Instance proto_cont_normalize_O d v P p q pas :
    ProtoNormalize d p pas q 
    ProtoContNormalize d (tele_app (TT:=TeleO) (v,P,p)) pas
                         (tele_app (TT:=TeleO) (v,P,q)).
  Proof. rewrite /ProtoContNormalize=> ?. by apply tforall_forall. Qed.

  Global Instance proto_cont_normalize_S {A} {TT : A  tele} d
      (pc qc :  a, TT a -t> val * iProp Σ * iProto Σ) pas :
    ( a, ProtoContNormalize d (tele_app (pc a)) pas (tele_app (qc a))) 
    ProtoContNormalize d (tele_app (TT:=TeleS TT) pc) pas (tele_app (TT:=TeleS TT) qc).
Robbert Krebbers's avatar
Robbert Krebbers committed
341
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
342 343
    rewrite /ProtoContNormalize=> H. apply tforall_forall=> /= x.
    apply tforall_forall, (H x).
Robbert Krebbers's avatar
Robbert Krebbers committed
344 345
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361
  Global Instance proto_normalize_message {TT} d a1 a2
      (pc qc : TT  val * iProp Σ * iProto Σ) pas :
    ActionDualIf d a1 a2 
    ProtoContNormalize d pc pas qc 
    ProtoNormalize d (iProto_message a1 pc) pas
                     (iProto_message a2 qc).
  Proof.
    rewrite /ActionDualIf /ProtoContNormalize /ProtoNormalize=> -> H.
    destruct d; simpl.
    - rewrite iProto_dual_message iProto_app_message.
      apply iProto_message_proper; apply tforall_forall=> x /=; apply H.
    - rewrite iProto_app_message.
      apply iProto_message_proper; apply tforall_forall=> x /=; apply H.
  Qed.

  (** Auxiliary definitions and invariants *)
Robbert Krebbers's avatar
Robbert Krebbers committed
362 363 364 365 366 367 368 369 370
  Global Instance proto_eval_ne : NonExpansive2 (proto_eval vs).
  Proof. induction vs; solve_proper. Qed.
  Global Instance proto_eval_proper vs : Proper (() ==> () ==> ()) (proto_eval vs).
  Proof. apply (ne_proper_2 _). Qed.

  Global Instance to_proto_auth_excl_ne : NonExpansive to_proto_auth_excl.
  Proof. solve_proper. Qed.
  Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s).
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
371 372 373
  Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto N c).
  Proof. rewrite mapsto_proto_eq. solve_proper. Qed.
  Global Instance mapsto_proto_proper c : Proper (() ==> ()) (mapsto_proto N c).
Robbert Krebbers's avatar
Robbert Krebbers committed
374 375 376 377 378 379 380 381 382
  Proof. apply (ne_proper _). Qed.

  Lemma proto_own_auth_agree γ s p p' :
    proto_own_auth γ s p - proto_own_frag γ s p' -  (p  p').
  Proof.
    iIntros "Hauth Hfrag".
    iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
    iDestruct (to_auth_excl_valid with "Hvalid") as "Hvalid".
    iDestruct (bi.later_eq_1 with "Hvalid") as "Hvalid"; iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
383
    assert ( p,
Robbert Krebbers's avatar
Robbert Krebbers committed
384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407
      proto_map id iProp_unfold iProp_fold (proto_map id iProp_fold iProp_unfold p)  p) as help.
    { intros p''. rewrite -proto_map_compose -{2}(proto_map_id p'').
      apply proto_map_ext=> // pc /=; by rewrite iProp_fold_unfold. }
    rewrite -{2}(help p). iRewrite "Hvalid". by rewrite help.
  Qed.

  Lemma proto_own_auth_update γ s p p' p'' :
    proto_own_auth γ s p - proto_own_frag γ s p' ==
    proto_own_auth γ s p''  proto_own_frag γ s p''.
  Proof.
    iIntros "Hauth Hfrag".
    iDestruct (own_update_2 with "Hauth Hfrag") as "H".
    { eapply (auth_update _ _ (to_proto_auth_excl p'') (to_proto_auth_excl p'')).
      apply option_local_update. by apply exclusive_local_update. }
    by rewrite own_op.
  Qed.

  Lemma proto_eval_send v vs pc p1 p2 :
    proto_eval vs (proto_message Send pc) p2 -
    ( f : laterO (iProto Σ) -n> iProp Σ, f (Next p1) - pc v f) -
    proto_eval (vs ++ [v]) p1 p2.
  Proof.
    iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl.
    - iDestruct "Heval" as "#Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
408 409 410
      iExists _, (iProto_dual p1). iSplit.
      { rewrite -{2}(involutive iProto_dual p2). iRewrite -"Heval".
        rewrite /iProto_dual. by rewrite proto_map_message. }
Robbert Krebbers's avatar
Robbert Krebbers committed
411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435
      iSplit.
      { iIntros (f) "Hf /=". by iApply "Hc". }
      by rewrite involutive.
    - iDestruct "Heval" as (pc' p2') "(Heq & Hc' & Heval)".
      iExists pc', p2'. iFrame "Heq Hc'". iNext. iApply ("IH" with "Heval Hc").
  Qed.

  Lemma proto_eval_recv v vs p1 pc :
     proto_eval (v :: vs) p1 (proto_message Receive pc) -  p2,
       ( f : laterO (iProto Σ) -n> iProp Σ, f (Next p2) - pc v f) 
        proto_eval vs p1 p2.
  Proof.
    simpl. iDestruct 1 as (pc' p2) "(Heq & Hc & Hp2)". iExists p2. iFrame "Hp2".
    iDestruct (@proto_message_equivI with "Heq") as "[_ Heq]".
    iSpecialize ("Heq" $! v). rewrite bi.ofe_morO_equivI.
    iIntros (f) "Hfp2". iRewrite ("Heq" $! f). by iApply "Hc".
  Qed.

  Lemma proto_eval_False p pc v vs :
    proto_eval (v :: vs) p (proto_message Send pc) - False.
  Proof.
    simpl. iDestruct 1 as (pc' p2') "[Heq _]".
    by iDestruct (@proto_message_equivI with "Heq") as "[% _]".
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
436
  Lemma proto_eval_nil p1 p2 : proto_eval [] p1 p2 - p1  iProto_dual p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
437 438 439 440 441 442 443
  Proof. done. Qed.

  Arguments proto_eval : simpl never.

  Lemma proto_init E cγ c1 c2 p :
    is_chan N cγ c1 c2 -
    chan_own cγ Left [] - chan_own cγ Right [] ={E}=
Robbert Krebbers's avatar
Robbert Krebbers committed
444
    c1  p @ N  c2  iProto_dual p @ N.
Robbert Krebbers's avatar
Robbert Krebbers committed
445 446 447 448 449
  Proof.
    iIntros "#Hcctx Hcol Hcor".
    iMod (own_alloc ( (to_proto_auth_excl p) 
                      (to_proto_auth_excl p))) as (lγ) "[Hlsta Hlstf]".
    { by apply auth_both_valid_2. }
Robbert Krebbers's avatar
Robbert Krebbers committed
450 451
    iMod (own_alloc ( (to_proto_auth_excl (iProto_dual p)) 
                      (to_proto_auth_excl (iProto_dual p)))) as (rγ) "[Hrsta Hrstf]".
Robbert Krebbers's avatar
Robbert Krebbers committed
452 453 454 455
    { by apply auth_both_valid_2. }
    pose (ProtName cγ lγ rγ) as pγ.
    iMod (inv_alloc N _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
    { iNext. rewrite /proto_inv. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
456
    iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
Robbert Krebbers's avatar
Robbert Krebbers committed
457 458 459 460
    - iExists Left, c1, c2, pγ; iFrame; auto.
    - iExists Right, c1, c2, pγ; iFrame; auto.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
461 462
  (** Accessor style lemmas *)
  Lemma proto_send_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
463
    N  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
464
    c  iProto_message Send pc @ N -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
465 466 467
       c = side_elim s c1 c2  
      is_chan N (proto_c_name γ) c1 c2  |={E,E∖↑N}=>  vs,
        chan_own (proto_c_name γ) s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
468 469 470 471
          (x : TT),
           (pc x).1.2 -
           chan_own (proto_c_name γ) s (vs ++ [(pc x).1.1]) ={E∖↑N,E}=
           c  (pc x).2 @ N.
Robbert Krebbers's avatar
Robbert Krebbers committed
472
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
473 474
    iIntros (?). rewrite {1}mapsto_proto_eq iProto_message_eq.
    iDestruct 1 as (s c1 c2 γ ->) "[Hstf #[Hcctx Hinv]]".
Robbert Krebbers's avatar
Robbert Krebbers committed
475 476 477 478 479 480 481 482
    iExists s, c1, c2, γ. iSplit; first done. iFrame "Hcctx".
    iInv N as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
    (* TODO: refactor to avoid twice nearly the same proof *)
    iModIntro. destruct s.
    - iExists _.
      iIntros "{$Hclf} !>" (x) "HP Hclf".
      iRename "Hstf" into "Hstlf".
      iDestruct (proto_own_auth_agree with "Hstla Hstlf") as "#Heq".
Robbert Krebbers's avatar
Robbert Krebbers committed
483
      iMod (proto_own_auth_update _ _ _ _ (pc x).2
Robbert Krebbers's avatar
Robbert Krebbers committed
484 485 486 487 488 489 490 491 492 493 494 495 496
        with "Hstla Hstlf") as "[Hstla Hstlf]".
      iMod ("Hclose" with "[-Hstlf]") as "_".
      { iNext. iExists _,_,_,_. iFrame "Hcrf Hstra Hstla Hclf". iLeft.
        iRewrite "Heq" in "Hinv'".
        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
        { iSplit=> //. iApply (proto_eval_send with "Heval [HP]").
          iIntros (f) "Hf /=". iExists x. by iFrame. }
        destruct r as [|vr r]; last first.
        { iDestruct (proto_eval_False with "Heval") as %[]. }
        iSplit; first done; simpl. iRewrite (proto_eval_nil with "Heval").
        iApply (proto_eval_send _ [] with "[] [HP]").
        { by rewrite /proto_eval involutive. }
        iIntros (f) "Hf /=". iExists x. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
497
      iModIntro. rewrite mapsto_proto_eq. iExists Left, c1, c2, γ. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
498 499 500 501
    - iExists _.
      iIntros "{$Hcrf} !>" (x) "HP Hcrf".
      iRename "Hstf" into "Hstrf".
      iDestruct (proto_own_auth_agree with "Hstra Hstrf") as "#Heq".
Robbert Krebbers's avatar
Robbert Krebbers committed
502
      iMod (proto_own_auth_update _ _ _ _ (pc x).2
Robbert Krebbers's avatar
Robbert Krebbers committed
503 504 505 506 507 508 509 510 511 512 513 514 515
        with "Hstra Hstrf") as "[Hstra Hstrf]".
      iMod ("Hclose" with "[-Hstrf]") as "_".
      { iNext. iExists _, _, _, _. iFrame "Hcrf Hstra Hstla Hclf". iRight.
        iRewrite "Heq" in "Hinv'".
        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last first.
        { iSplit=> //. iApply (proto_eval_send with "Heval [HP]").
          iIntros (f) "Hf /=". iExists x. by iFrame. }
        destruct l as [|vl l]; last first.
        { iDestruct (proto_eval_False with "Heval") as %[]. }
        iSplit; first done; simpl. iRewrite (proto_eval_nil with "Heval").
        iApply (proto_eval_send _ [] with "[] [HP]").
        { by rewrite /proto_eval involutive. }
        iIntros (f) "Hf /=". iExists x. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
516
      iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
517 518
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
519
  Lemma proto_recv_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
520
    N  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
521
    c  iProto_message Receive pc @ N -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
522 523 524 525
       c = side_elim s c2 c1  
      is_chan N (proto_c_name γ) c1 c2  |={E,E∖↑N}=>  vs,
        chan_own (proto_c_name γ) s vs 
         ((chan_own (proto_c_name γ) s vs ={E∖↑N,E}=
Robbert Krebbers's avatar
Robbert Krebbers committed
526
             c  iProto_message Receive pc @ N) 
Robbert Krebbers's avatar
Robbert Krebbers committed
527 528
           ( v vs',
              vs = v :: vs'  -
Robbert Krebbers's avatar
Robbert Krebbers committed
529 530
             chan_own (proto_c_name γ) s vs' ={E∖↑N,E}=    x : TT,
              v = (pc x).1.1   c  (pc x).2 @ N  (pc x).1.2)).
Robbert Krebbers's avatar
Robbert Krebbers committed
531
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
532 533
    iIntros (?). rewrite {1}mapsto_proto_eq iProto_message_eq.
    iDestruct 1 as (s c1 c2 γ ->) "[Hstf #[Hcctx Hinv]]".
Robbert Krebbers's avatar
Robbert Krebbers committed
534 535 536 537 538 539 540 541 542 543 544 545 546
    iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
    iFrame "Hcctx".
    iInv N as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
    iExists (side_elim s r l). iModIntro.
    (* TODO: refactor to avoid twice nearly the same proof *)
    destruct s; simpl.
    - iIntros "{$Hcrf} !>".
      iRename "Hstf" into "Hstlf".
      iDestruct (proto_own_auth_agree with "Hstla Hstlf") as "#Heq".
      iSplit.
      + iIntros "Hown".
        iMod ("Hclose" with "[-Hstlf]") as "_".
        { iNext. iExists l, r, _, _. iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
547 548
        iModIntro. rewrite mapsto_proto_eq.
        iExists Left, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
549 550
      + iIntros (v vs ->) "Hown".
        iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
551 552
        iAssert ( proto_eval (v :: vs) pr (iProto_message_def Receive pc))%I
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
553 554 555 556 557 558
        { iNext. by iRewrite "Heq" in "Heval". }
        iDestruct (proto_eval_recv with "Heval") as (q) "[Hf Heval]".
        iMod (proto_own_auth_update _ _ _ _ q with "Hstla Hstlf") as "[Hstla Hstlf]".
        iMod ("Hclose" with "[-Hstlf Hf]") as %_.
        { iExists _, _,_ ,_. eauto 10 with iFrame. }
        iIntros "!> !>".
Robbert Krebbers's avatar
Robbert Krebbers committed
559
        set (f lp := ( q, lp  Next q  c1  q @ N)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
560
        assert (NonExpansive f) by solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
561 562 563 564 565
        iDestruct ("Hf" $! (OfeMor f) with "[Hstlf]") as (x) "(Hv & HP & Hf) /=".
        { iExists q. iSplit; first done. rewrite mapsto_proto_eq.
          iExists Left, c1, c2, γ. iFrame; auto. }
        iDestruct "Hf" as (q') "[#Hq Hc]". iModIntro.
        iExists x. iFrame "Hv HP". by iRewrite "Hq".
Robbert Krebbers's avatar
Robbert Krebbers committed
566 567 568 569 570 571 572
    - iIntros "{$Hclf} !>".
      iRename "Hstf" into "Hstrf".
      iDestruct (proto_own_auth_agree with "Hstra Hstrf") as "#Heq".
      iSplit.
      + iIntros "Hown".
        iMod ("Hclose" with "[-Hstrf]") as "_".
        { iNext. iExists l, r, _, _. iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
573 574
        iModIntro. rewrite mapsto_proto_eq.
        iExists Right, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
575 576
      + iIntros (v vs ->) "Hown".
        iDestruct "Hinv'" as "[[>-> Heval]|[>% _]]"; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
577 578
        iAssert ( proto_eval (v :: vs) pl (iProto_message_def Receive pc))%I
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
579 580 581 582 583 584
        { iNext. by iRewrite "Heq" in "Heval". }
        iDestruct (proto_eval_recv with "Heval") as (q) "[Hf Heval]".
        iMod (proto_own_auth_update _ _ _ _ q with "Hstra Hstrf") as "[Hstra Hstrf]".
        iMod ("Hclose" with "[-Hstrf Hf]") as %_.
        { iExists _, _, _, _. eauto 10 with iFrame. }
        iIntros "!> !>".
Robbert Krebbers's avatar
Robbert Krebbers committed
585
        set (f lp := ( q, lp  Next q  c2  q @ N)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
586
        assert (NonExpansive f) by solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
587 588 589 590 591
        iDestruct ("Hf" $! (OfeMor f) with "[Hstrf]") as (x) "(Hv & HP & Hf) /=".
        { iExists q. iSplit; first done. rewrite mapsto_proto_eq.
          iExists Right, c1, c2, γ. iFrame; auto. }
        iDestruct "Hf" as (q') "[#Hq Hc]". iModIntro.
        iExists x. iFrame "Hv HP". by iRewrite "Hq".
Robbert Krebbers's avatar
Robbert Krebbers committed
592 593
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
594 595
  (** Specifications of send and receive *)
  Lemma new_chan_proto_spec p :
Robbert Krebbers's avatar
Robbert Krebbers committed
596 597
    {{{ True }}}
      new_chan #()
Robbert Krebbers's avatar
Robbert Krebbers committed
598
    {{{ c1 c2, RET (c1,c2); c1  p @ N  c2  iProto_dual p @ N }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
599
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
600
    iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
Robbert Krebbers's avatar
Robbert Krebbers committed
601
    iIntros (c1 c2 γ) "(Hc & Hl & Hr)".
Robbert Krebbers's avatar
Robbert Krebbers committed
602 603
    iMod (proto_init  γ c1 c2 p with "Hc Hl Hr") as "[Hp Hdp]".
    iApply "HΨ". by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
604 605
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
606 607 608 609
  Lemma send_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) (x : TT) :
    {{{ c  iProto_message Send pc @ N  (pc x).1.2 }}}
      send c (pc x).1.1
    {{{ RET #(); c  (pc x).2 @ N }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
610 611 612 613 614 615 616 617 618
  Proof.
    iIntros (Ψ) "[Hp Hf] HΨ".
    iDestruct (proto_send_acc  with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
    iApply (send_spec with "[$]"). iMod "Hvs" as (vs) "[Hch H]".
    iModIntro. iExists vs. iFrame "Hch".
    iIntros "!> Hvs". iApply "HΨ".
    iMod ("H" $! x with "Hf Hvs"); auto.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
619 620 621 622 623
  Lemma send_proto_spec {TT} Ψ c v p (pc : TT  val * iProp Σ * iProto Σ) :
    ProtoNormalize false p [] (iProto_message Send pc) 
    c  p @ N -
    (.. x : TT,
       v = (pc x).1.1   (pc x).1.2   (c  (pc x).2 @ N - Ψ #())) -
Robbert Krebbers's avatar
Robbert Krebbers committed
624 625
    WP send c v {{ Ψ }}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
626
    rewrite /ProtoNormalize /= right_id=> <-.
Robbert Krebbers's avatar
Robbert Krebbers committed
627 628 629 630
    iIntros "Hc H". iDestruct (bi_texist_exist with "H") as (x ->) "[HP HΨ]".
    by iApply (send_proto_spec_packed with "[$]").
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
631 632
  Lemma try_recv_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) :
    {{{ c  iProto_message Receive pc @ N }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
633
      try_recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
634 635
    {{{ v, RET v; (v = NONEV  c  iProto_message Receive pc @ N) 
                  ( x : TT, v = SOMEV ((pc x).1.1)  c  (pc x).2 @ N  (pc x).1.2) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
636 637 638 639 640 641 642 643
  Proof.
    iIntros (Ψ) "Hp HΨ".
    iDestruct (proto_recv_acc  with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
    wp_apply (try_recv_spec with "[$]"). iSplit.
    - iMod "Hvs" as (vs) "[Hch [H _]]".
      iIntros "!> !>". iMod ("H" with "Hch") as "Hch". iApply "HΨ"; auto.
    - iMod "Hvs" as (vs) "[Hch [_ H]]".
      iIntros "!>". iExists vs. iIntros "{$Hch} !>" (v vs' ->) "Hch".
Robbert Krebbers's avatar
Robbert Krebbers committed
644 645
      iMod ("H" with "[//] Hch") as "H". iIntros "!> !> !>".
      iDestruct "H" as (x ->) "H". iApply "HΨ"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
646 647
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
648 649
  Lemma recv_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) :
    {{{ c  iProto_message Receive pc @ N }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
650
      recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
651
    {{{ x, RET (pc x).1.1; c  (pc x).2 @ N  (pc x).1.2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
652 653 654 655 656
  Proof.
    iIntros (Ψ) "Hp HΨ".
    iDestruct (proto_recv_acc  with "Hp") as (γ s c1 c2 ->) "[#Hc Hvs]"; first done.
    wp_apply (recv_spec with "[$]"). iMod "Hvs" as (vs) "[Hch [_ H]]".
    iModIntro. iExists vs. iFrame "Hch". iIntros "!>" (v vs' ->) "Hvs'".
Robbert Krebbers's avatar
Robbert Krebbers committed
657 658
    iMod ("H" with "[//] Hvs'") as "H"; iIntros "!> !> !>".
    iDestruct "H" as (x ->) "H". by iApply "HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
659 660
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
661 662 663 664
  Lemma recv_proto_spec {TT} Ψ p c (pc : TT  val * iProp Σ * iProto Σ) :
    ProtoNormalize false p [] (iProto_message Receive pc) 
    c  p @ N -
     (.. x : TT, c  (pc x).2 @ N - (pc x).1.2 - Ψ (pc x).1.1) -
Robbert Krebbers's avatar
Robbert Krebbers committed
665 666
    WP recv c {{ Ψ }}.
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
667
    rewrite /ProtoNormalize /= right_id=> <-.
Robbert Krebbers's avatar
Robbert Krebbers committed
668 669 670 671
    iIntros "Hc H". iApply (recv_proto_spec_packed with "[$]").
    iIntros "!>" (x) "[Hc HP]". iDestruct (bi_tforall_forall with "H") as "H".
    iApply ("H" with "[$] [$]").
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
672

Robbert Krebbers's avatar
Robbert Krebbers committed
673
  (** Branching *)
Robbert Krebbers's avatar
Robbert Krebbers committed
674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691
  Lemma select_spec c b p1 p2 :
    {{{ c  p1 <+> p2 @ N }}}
      send c #b
    {{{ RET #(); c  (if b : bool then p1 else p2) @ N }}}.
  Proof.
    rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
    iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
  Qed.

  Lemma branch_spec c p1 p2  :
    {{{ c  p1 <&> p2 @ N }}}
      recv c
    {{{ b, RET #b; c  if b : bool then p1 else p2 @ N }}}.
  Proof.
    rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
    iApply (recv_proto_spec with "Hc"); simpl.
    iIntros "!>" (b) "Hc _". by iApply "HΨ".
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
692
End proto.