proto_channel.v 34.3 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
Export action.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

Robbert Krebbers's avatar
Robbert Krebbers committed
9 10 11 12
Definition start_chan : val := λ: "f",
  let: "cc" := new_chan #() in
  Fork ("f" (Snd "cc"));; Fst "cc".

Robbert Krebbers's avatar
Robbert Krebbers committed
13 14 15 16 17 18 19 20 21 22 23 24 25
(** 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
26
(** Types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28 29 30
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
31 32 33 34 35 36 37 38 39 40 41 42 43 44
(** 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
45
Next Obligation. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
46 47 48 49 50 51
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.

52
Notation "< a > x1 .. xn , 'MSG' v {{ P } } ; p" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54 55 56 57 58 59 60 61 62 63
  (iProto_message
    a
    (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
  (at level 20, a at level 10, x1 binder, xn binder, v at level 20, P, p at level 200) : proto_scope.
Notation "< a > x1 .. xn , 'MSG' v ; p" :=
  (iProto_message
    a
    (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
  (at level 20, a at level 10, x1 binder, xn binder, v at level 20, p at level 200) : proto_scope.
64
Notation "< a > 'MSG' v {{ P } } ; p" :=
65 66 67 68 69 70 71 72 73
  (iProto_message
    a
    (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
  (at level 20, a at level 10, v at level 20, P, p at level 200) : proto_scope.
Notation "< a > 'MSG' v ; p" :=
  (iProto_message
    a
    (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
  (at level 20, a at level 10, v at level 20, p at level 200) : proto_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
74

75
Notation "<!> x1 .. xn , 'MSG' v {{ P } } ; p" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
76 77 78 79 80 81 82 83 84 85 86
  (iProto_message
    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
    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.
87
Notation "<!> 'MSG' v {{ P } } ; p" :=
88 89 90 91 92 93 94 95 96 97 98
  (iProto_message
    (TT:=TeleO)
    Send
    (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
  (at level 20, v at level 20, P, p at level 200) : proto_scope.
Notation "<!> 'MSG' v ; p" :=
  (iProto_message
    (TT:=TeleO)
    Send
    (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
  (at level 20, v at level 20, p at level 200) : proto_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
99

100
Notation "<?> x1 .. xn , 'MSG' v {{ P } } ; p" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
101 102 103 104 105 106 107 108 109 110 111
  (iProto_message
    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
    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.
112
Notation "<?> 'MSG' v {{ P } } ; p" :=
113 114 115 116 117 118 119 120 121
  (iProto_message
    Receive
    (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
  (at level 20, v at level 20, P, p at level 200) : proto_scope.
Notation "<?> 'MSG' v ; p" :=
  (iProto_message
    Receive
    (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
  (at level 20, v at level 20, p at level 200) : proto_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
122 123

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

Robbert Krebbers's avatar
Robbert Krebbers committed
125
(** Dual *)
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
127
  proto_map action_dual cid cid p.
Robbert Krebbers's avatar
Robbert Krebbers committed
128 129 130 131 132 133
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
134

Robbert Krebbers's avatar
Robbert Krebbers committed
135
(** Branching *)
136 137 138
Definition iProto_branch {Σ} (a : action) (P1 P2 : iProp Σ)
    (p1 p2 : iProto Σ) : iProto Σ :=
  (<a> (b : bool), MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Typeclasses Opaque iProto_branch.
140
Arguments iProto_branch {_} _ _%I _%I _%proto _%proto.
141
Instance: Params (@iProto_branch) 2.
142 143 144 145 146 147 148 149
Infix "<{ P1 }+{ P2 }>" := (iProto_branch Send P1 P2) (at level 85) : proto_scope.
Infix "<{ P1 }&{ P2 }>" := (iProto_branch Receive P1 P2) (at level 85) : proto_scope.
Infix "<+{ P2 }>" := (iProto_branch Send True P2) (at level 85) : proto_scope.
Infix "<&{ P2 }>" := (iProto_branch Receive True P2) (at level 85) : proto_scope.
Infix "<{ P1 }+>" := (iProto_branch Send P1 True) (at level 85) : proto_scope.
Infix "<{ P1 }&>" := (iProto_branch Receive P1 True) (at level 85) : proto_scope.
Infix "<+>" := (iProto_branch Send True True) (at level 85) : proto_scope.
Infix "<&>" := (iProto_branch Receive True True) (at level 85) : proto_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
150

Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181
(** 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.

182 183 184
Notation ProtoUnfold p1 p2 := ( d pas q,
  ProtoNormalize d p2 pas q  ProtoNormalize d p1 pas q).

Robbert Krebbers's avatar
Robbert Krebbers committed
185
(** Auxiliary definitions and invariants *)
Robbert Krebbers's avatar
Robbert Krebbers committed
186 187
Fixpoint proto_eval `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
  match vs with
Robbert Krebbers's avatar
Robbert Krebbers committed
188
  | [] => p1  iProto_dual p2
Robbert Krebbers's avatar
Robbert Krebbers committed
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 220 221
  | 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
222
Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ} (N : namespace)
Robbert Krebbers's avatar
Robbert Krebbers committed
223 224 225 226
    (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
227 228 229 230 231
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
232

Robbert Krebbers's avatar
Robbert Krebbers committed
233
Notation "c ↣ p @ N" := (mapsto_proto N c p)
Robbert Krebbers's avatar
Robbert Krebbers committed
234 235 236 237
  (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
238 239 240 241 242 243 244 245 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
  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
274

Robbert Krebbers's avatar
Robbert Krebbers committed
275
  Global Instance iProto_branch_contractive n a :
276 277
    Proper (dist_later n ==> dist_later n ==>
            dist_later n ==> dist_later n ==> dist n) (@iProto_branch Σ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
278
  Proof.
279
    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
Robbert Krebbers's avatar
Robbert Krebbers committed
280 281
    apply iProto_message_contractive=> /= -[] //.
  Qed.
282 283
  Global Instance iProto_branch_ne n a :
    Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (@iProto_branch Σ a).
Robbert Krebbers's avatar
Robbert Krebbers committed
284
  Proof.
285 286
    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
    by apply iProto_message_ne=> /= -[].
Robbert Krebbers's avatar
Robbert Krebbers committed
287 288
  Qed.
  Global Instance iProto_branch_proper a :
289 290 291 292 293
    Proper (() ==> () ==> () ==> () ==> ()) (@iProto_branch Σ a).
  Proof.
    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
    by apply iProto_message_proper=> /= -[].
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
294 295 296

  (** Dual *)
  Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
  Global Instance iProto_dual_proper : Proper (() ==> ()) (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
299
  Proof. apply (ne_proper _). Qed.
300 301 302 303
  Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ d).
  Proof. solve_proper. Qed.
  Global Instance iProto_dual_if_proper d : Proper (() ==> ()) (@iProto_dual_if Σ d).
  Proof. apply (ne_proper _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
304 305

  Global Instance iProto_dual_involutive : Involutive () (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
306
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
    intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
Robbert Krebbers's avatar
Robbert Krebbers committed
308 309
    apply: proto_map_ext=> //. by intros [].
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
310 311 312 313 314 315 316 317 318 319 320

  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.

321 322 323
  Lemma iProto_dual_branch a P1 P2 p1 p2 :
    iProto_dual (iProto_branch a P1 P2 p1 p2)
     iProto_branch (action_dual a) P1 P2 (iProto_dual p1) (iProto_dual p2).
Robbert Krebbers's avatar
Robbert Krebbers committed
324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
  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
343
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
344 345 346
    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
347
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
349
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
350 351 352
  Global Instance iProto_app_assoc : Assoc () (@iProto_app Σ).
  Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.

353 354 355
  Lemma iProto_app_branch a P1 P2 p1 p2 q :
    (iProto_branch a P1 P2 p1 p2 <++> q)%proto
     (iProto_branch a P1 P2 (p1 <++> q) (p2 <++> q))%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
356 357 358 359 360
  Proof.
    rewrite /iProto_branch iProto_app_message.
    by apply iProto_message_proper=> /= -[].
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
361 362 363 364 365
  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 *)
366 367 368
  Lemma proto_unfold_eq p1 p2 : p1  p2  ProtoUnfold p1 p2.
  Proof. rewrite /ProtoNormalize=> Hp d pas q ->. by rewrite Hp. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
369 370 371 372 373
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
374 375 376
  Global Instance proto_normalize_done_dual_end :
    ProtoNormalize (Σ:=Σ) true END [] END | 0.
  Proof. by rewrite /ProtoNormalize /= right_id iProto_dual_end. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392

  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 
393
    ProtoNormalize d' END ((d,p) :: pas) q | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
394
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
395 396
    rewrite /ProtoNormalize=> -> /=.
    destruct d'; by rewrite /= ?iProto_dual_end left_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
397 398
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
399 400
  Global Instance proto_normalize_app_r d p1 p2 pas q :
    ProtoNormalize d p2 pas q 
401
    ProtoNormalize false p1 ((d,p2) :: pas) (p1 <++> q) | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
402 403 404 405
  Proof. by rewrite /ProtoNormalize=> -> /=. Qed.

  Global Instance proto_normalize_app_r_dual d p1 p2 pas q :
    ProtoNormalize d p2 pas q 
406
    ProtoNormalize true p1 ((d,p2) :: pas) (iProto_dual p1 <++> q) | 0.
Robbert Krebbers's avatar
Robbert Krebbers committed
407 408 409 410 411 412 413 414 415 416 417 418
  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
419
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
420 421
    rewrite /ProtoContNormalize=> H. apply tforall_forall=> /= x.
    apply tforall_forall, (H x).
Robbert Krebbers's avatar
Robbert Krebbers committed
422 423
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
424 425 426 427 428 429 430 431 432 433 434 435 436 437 438
  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.

439
  Global Instance proto_normalize_branch d a1 a2 P1 P2 p1 p2 q1 q2 pas :
Robbert Krebbers's avatar
Robbert Krebbers committed
440 441
    ActionDualIf d a1 a2 
    ProtoNormalize d p1 pas q1  ProtoNormalize d p2 pas q2 
442 443
    ProtoNormalize d (iProto_branch a1 P1 P2 p1 p2) pas
                     (iProto_branch a2 P1 P2 q1 q2).
Robbert Krebbers's avatar
Robbert Krebbers committed
444 445 446 447 448
  Proof.
    rewrite /ActionDualIf /ProtoNormalize=> -> -> ->.
    destruct d; by rewrite /= -?iProto_app_branch -?iProto_dual_branch.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
449
  (** Auxiliary definitions and invariants *)
Robbert Krebbers's avatar
Robbert Krebbers committed
450 451 452 453 454 455 456 457 458
  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
459 460 461
  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
462 463 464 465 466 467 468 469 470
  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
471
    assert ( p,
Robbert Krebbers's avatar
Robbert Krebbers committed
472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495
      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
496 497 498
      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
499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523
      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
524
  Lemma proto_eval_nil p1 p2 : proto_eval [] p1 p2 - p1  iProto_dual p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
525 526 527 528
  Proof. done. Qed.

  Arguments proto_eval : simpl never.

Robbert Krebbers's avatar
Robbert Krebbers committed
529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545
  (** Automatically perform normalization of protocols in the proof mode *)
  Global Instance mapsto_proto_from_assumption q c p1 p2 :
    ProtoNormalize false p1 [] p2 
    FromAssumption q (c  p1 @ N) (c  p2 @ N).
  Proof.
    rewrite /FromAssumption /ProtoNormalize=> ->.
    by rewrite /= right_id bi.intuitionistically_if_elim.
  Qed.
  Global Instance mapsto_proto_from_frame q c p1 p2 :
    ProtoNormalize false p1 [] p2 
    Frame q (c  p1 @ N) (c  p2 @ N) True.
  Proof.
    rewrite /Frame /ProtoNormalize=> ->.
    by rewrite /= !right_id bi.intuitionistically_if_elim.
  Qed.

  (** The actual specs *)
Robbert Krebbers's avatar
Robbert Krebbers committed
546 547 548
  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
549
    c1  p @ N  c2  iProto_dual p @ N.
Robbert Krebbers's avatar
Robbert Krebbers committed
550 551 552 553 554
  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
555 556
    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
557 558 559 560
    { 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
561
    iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
Robbert Krebbers's avatar
Robbert Krebbers committed
562 563 564 565
    - iExists Left, c1, c2, pγ; iFrame; auto.
    - iExists Right, c1, c2, pγ; iFrame; auto.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
566 567
  (** Accessor style lemmas *)
  Lemma proto_send_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
568
    N  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
569
    c  iProto_message Send pc @ N -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
570 571 572
       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
573 574 575 576
          (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
577
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
578 579
    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
580 581 582 583 584 585 586 587
    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
588
      iMod (proto_own_auth_update _ _ _ _ (pc x).2
Robbert Krebbers's avatar
Robbert Krebbers committed
589 590 591 592 593 594 595 596 597 598 599 600 601
        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
602
      iModIntro. rewrite mapsto_proto_eq. iExists Left, c1, c2, γ. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
603 604 605 606
    - 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
607
      iMod (proto_own_auth_update _ _ _ _ (pc x).2
Robbert Krebbers's avatar
Robbert Krebbers committed
608 609 610 611 612 613 614 615 616 617 618 619 620
        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
621
      iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
622 623
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
624
  Lemma proto_recv_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
625
    N  E 
Robbert Krebbers's avatar
Robbert Krebbers committed
626
    c  iProto_message Receive pc @ N -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
627 628 629 630
       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
631
             c  iProto_message Receive pc @ N) 
Robbert Krebbers's avatar
Robbert Krebbers committed
632 633
           ( v vs',
              vs = v :: vs'  -
Robbert Krebbers's avatar
Robbert Krebbers committed
634 635
             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
636
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
637 638
    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
639 640 641 642 643 644 645 646 647 648 649 650 651
    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
652 653
        iModIntro. rewrite mapsto_proto_eq.
        iExists Left, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
654 655
      + iIntros (v vs ->) "Hown".
        iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
656 657
        iAssert ( proto_eval (v :: vs) pr (iProto_message_def Receive pc))%I
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
658 659 660 661 662 663
        { 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
664
        set (f lp := ( q, lp  Next q  c1  q @ N)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
665
        assert (NonExpansive f) by solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
666 667 668 669 670
        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
671 672 673 674 675 676 677
    - 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
678 679
        iModIntro. rewrite mapsto_proto_eq.
        iExists Right, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
680 681
      + iIntros (v vs ->) "Hown".
        iDestruct "Hinv'" as "[[>-> Heval]|[>% _]]"; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
682 683
        iAssert ( proto_eval (v :: vs) pl (iProto_message_def Receive pc))%I
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
684 685 686 687 688 689
        { 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
690
        set (f lp := ( q, lp  Next q  c2  q @ N)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
691
        assert (NonExpansive f) by solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
692 693 694 695 696
        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
697 698
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
699 700
  (** Specifications of send and receive *)
  Lemma new_chan_proto_spec p :
Robbert Krebbers's avatar
Robbert Krebbers committed
701 702
    {{{ True }}}
      new_chan #()
Robbert Krebbers's avatar
Robbert Krebbers committed
703
    {{{ c1 c2, RET (c1,c2); c1  p @ N  c2  iProto_dual p @ N }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
704
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
705
    iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
Robbert Krebbers's avatar
Robbert Krebbers committed
706
    iIntros (c1 c2 γ) "(Hc & Hl & Hr)".
Robbert Krebbers's avatar
Robbert Krebbers committed
707 708
    iMod (proto_init  γ c1 c2 p with "Hc Hl Hr") as "[Hp Hdp]".
    iApply "HΨ". by iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
709 710
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
711 712 713 714 715 716 717 718 719 720 721 722
  Lemma start_chan_proto_spec p Ψ (f : val) :
     ( c, c  iProto_dual p @ N - WP f c {{ _, True }}) -
     ( c, c  p @ N - Ψ c) -
    WP start_chan f {{ Ψ }}.
  Proof.
    iIntros "Hfork HΨ". wp_lam.
    wp_apply (new_chan_proto_spec p with "[//]"); iIntros (c1 c2) "[Hc1 Hc2]".
    wp_apply (wp_fork with "[Hfork Hc2]").
    { iNext. wp_apply ("Hfork" with "Hc2"). }
    wp_pures. iApply ("HΨ" with "Hc1").
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
723 724 725 726
  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
727 728 729 730 731 732 733 734 735
  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
736 737
  Lemma send_proto_spec {TT} Ψ c v (pc : TT  val * iProp Σ * iProto Σ) :
    c  iProto_message Send pc @ N -
Robbert Krebbers's avatar
Robbert Krebbers committed
738 739
    (.. x : TT,
       v = (pc x).1.1   (pc x).1.2   (c  (pc x).2 @ N - Ψ #())) -
Robbert Krebbers's avatar
Robbert Krebbers committed
740 741 742 743 744 745
    WP send c v {{ Ψ }}.
  Proof.
    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
746 747
  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
748
      try_recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
749 750
    {{{ 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
751 752 753 754 755 756 757 758
  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
759 760
      iMod ("H" with "[//] Hch") as "H". iIntros "!> !> !>".
      iDestruct "H" as (x ->) "H". iApply "HΨ"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
761 762
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
763 764
  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
765
      recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
766
    {{{ x, RET (pc x).1.1; c  (pc x).2 @ N  (pc x).1.2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
767 768 769 770 771
  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
772 773
    iMod ("H" with "[//] Hvs'") as "H"; iIntros "!> !> !>".
    iDestruct "H" as (x ->) "H". by iApply "HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
774 775
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
776 777
  Lemma recv_proto_spec {TT} Ψ c (pc : TT  val * iProp Σ * iProto Σ) :
    c  iProto_message Receive pc @ N -
Robbert Krebbers's avatar
Robbert Krebbers committed
778
     (.. x : TT, c  (pc x).2 @ N - (pc x).1.2 - Ψ (pc x).1.1) -
Robbert Krebbers's avatar
Robbert Krebbers committed
779 780 781 782 783 784
    WP recv c {{ Ψ }}.
  Proof.
    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
785

Robbert Krebbers's avatar
Robbert Krebbers committed
786
  (** Branching *)
787 788
  Lemma select_spec c (b : bool) P1 P2 p1 p2 :
    {{{ c  p1 <{P1}+{P2}> p2 @ N  if b then P1 else P2 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
789
      send c #b
790
    {{{ RET #(); c  (if b then p1 else p2) @ N }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
791
  Proof.
792
    rewrite /iProto_branch. iIntros (Ψ) "[Hc HP] HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
793 794 795
    iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
  Qed.

796 797
  Lemma branch_spec c P1 P2 p1 p2 :
    {{{ c  p1 <{P1}&{P2}> p2 @ N }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
798
      recv c
799
    {{{ b, RET #b; c  if b : bool then p1 else p2 @ N  if b then P1 else P2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
800 801 802
  Proof.
    rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
    iApply (recv_proto_spec with "Hc"); simpl.
803
    iIntros "!>" (b) "Hc HP". iApply "HΨ". iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
804
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
805
End proto.
806 807 808 809 810 811 812 813 814 815 816 817 818 819

Ltac f_proto_contractive :=
  match goal with
  | _ => apply iProto_branch_contractive
  | _ => apply iProto_message_contractive; simpl; intros; [reflexivity|..]
  | H : _ {?n} _ |- _ {?n'} _ => apply (dist_le n); [apply H|lia]
  end;
  try match goal with
  | |- @dist_later ?A _ ?n ?x ?y =>
         destruct n as [|n]; simpl in *; [exact Logic.I|change (@dist A _ n x y)]
  end.

Ltac solve_proto_contractive :=
  solve_proper_core ltac:(fun _ => first [f_contractive | f_proto_contractive | f_equiv]).