proto_channel.v 28.6 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
From actris.channel Require Export channel.
From actris.channel Require Import proto_model.
Robbert Krebbers's avatar
Robbert Krebbers committed
3 4 5
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth excl.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
From actris.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
(** 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.

(** Auxiliary definitions and invariants *)
jihgfee's avatar
jihgfee committed
158
Fixpoint proto_interp `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
159
  match vs with
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  | [] => p1  iProto_dual p2
Robbert Krebbers's avatar
Robbert Krebbers committed
161 162 163
  | v :: vs =>  pc p2',
     p2  (proto_message Receive pc)%proto 
     ( f : laterO (iProto Σ) -n> iProp Σ, f (Next p2') - pc v f) 
jihgfee's avatar
jihgfee committed
164
      proto_interp vs p1 p2'
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  end%I.
jihgfee's avatar
jihgfee committed
166
Arguments proto_interp {_ _} _ _%proto _%proto : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190

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 
jihgfee's avatar
jihgfee committed
191 192
     ((r = []  proto_interp l pl pr) 
       (l = []  proto_interp r pr pl)))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
193

Robbert Krebbers's avatar
Robbert Krebbers committed
194 195 196
Definition protoN := nroot .@ "proto".

Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
Robbert Krebbers's avatar
Robbert Krebbers committed
197 198 199
    (c : val) (p : iProto Σ) : iProp Σ :=
  ( s (c1 c2 : val) γ,
     c = side_elim s c1 c2  
Robbert Krebbers's avatar
Robbert Krebbers committed
200
    proto_own_frag γ s p  is_chan protoN (proto_c_name γ) c1 c2  inv protoN (proto_inv γ))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
201 202 203
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
204 205
Arguments mapsto_proto {_ _ _} _ _%proto.
Instance: Params (@mapsto_proto) 4 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
206

Robbert Krebbers's avatar
Robbert Krebbers committed
207 208
Notation "c ↣ p" := (mapsto_proto c p)
  (at level 20, format "c  ↣  p").
Robbert Krebbers's avatar
Robbert Krebbers committed
209 210

Section proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
  Context `{!proto_chanG Σ, !heapG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247
  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
248

Robbert Krebbers's avatar
Robbert Krebbers committed
249
  Global Instance iProto_branch_contractive n a :
250 251
    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
252
  Proof.
253
    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
Robbert Krebbers's avatar
Robbert Krebbers committed
254 255
    apply iProto_message_contractive=> /= -[] //.
  Qed.
256 257
  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
258
  Proof.
259 260
    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
261 262
  Qed.
  Global Instance iProto_branch_proper a :
263 264 265 266 267
    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
268 269 270

  (** Dual *)
  Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
271
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
272
  Global Instance iProto_dual_proper : Proper (() ==> ()) (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
273
  Proof. apply (ne_proper _). Qed.
274 275 276 277
  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
278 279

  Global Instance iProto_dual_involutive : Involutive () (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
280
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
281
    intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
Robbert Krebbers's avatar
Robbert Krebbers committed
282 283
    apply: proto_map_ext=> //. by intros [].
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
284 285 286 287 288 289 290 291 292 293 294

  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.

295 296 297
  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
298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316
  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
317
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
318 319 320
    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
321
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
322
    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
324 325 326
  Global Instance iProto_app_assoc : Assoc () (@iProto_app Σ).
  Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.

327 328 329
  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
330 331 332 333 334
  Proof.
    rewrite /iProto_branch iProto_app_message.
    by apply iProto_message_proper=> /= -[].
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
335 336 337 338 339
  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.

  (** Auxiliary definitions and invariants *)
jihgfee's avatar
jihgfee committed
340
  Global Instance proto_interp_ne : NonExpansive2 (proto_interp vs).
Robbert Krebbers's avatar
Robbert Krebbers committed
341
  Proof. induction vs; solve_proper. Qed.
jihgfee's avatar
jihgfee committed
342
  Global Instance proto_interp_proper vs : Proper (() ==> () ==> ()) (proto_interp vs).
Robbert Krebbers's avatar
Robbert Krebbers committed
343 344 345 346 347 348
  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
349
  Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto c).
Robbert Krebbers's avatar
Robbert Krebbers committed
350
  Proof. rewrite mapsto_proto_eq. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
351
  Global Instance mapsto_proto_proper c : Proper (() ==> ()) (mapsto_proto c).
Robbert Krebbers's avatar
Robbert Krebbers committed
352 353 354 355 356 357 358 359 360
  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
361
    assert ( p,
Robbert Krebbers's avatar
Robbert Krebbers committed
362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378
      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.

jihgfee's avatar
jihgfee committed
379 380
  Lemma proto_interp_send v vs pc p1 p2 :
    proto_interp vs (proto_message Send pc) p2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
381
    ( f : laterO (iProto Σ) -n> iProp Σ, f (Next p1) - pc v f) -
jihgfee's avatar
jihgfee committed
382
    proto_interp (vs ++ [v]) p1 p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
383 384 385
  Proof.
    iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl.
    - iDestruct "Heval" as "#Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
386 387 388
      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
389 390 391 392 393 394 395
      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.

jihgfee's avatar
jihgfee committed
396 397
  Lemma proto_interp_recv v vs p1 pc :
     proto_interp (v :: vs) p1 (proto_message Receive pc) -  p2,
Robbert Krebbers's avatar
Robbert Krebbers committed
398
       ( f : laterO (iProto Σ) -n> iProp Σ, f (Next p2) - pc v f) 
jihgfee's avatar
jihgfee committed
399
        proto_interp vs p1 p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
400 401 402 403 404 405 406
  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.

jihgfee's avatar
jihgfee committed
407 408
  Lemma proto_interp_False p pc v vs :
    proto_interp (v :: vs) p (proto_message Send pc) - False.
Robbert Krebbers's avatar
Robbert Krebbers committed
409 410 411 412 413
  Proof.
    simpl. iDestruct 1 as (pc' p2') "[Heq _]".
    by iDestruct (@proto_message_equivI with "Heq") as "[% _]".
  Qed.

jihgfee's avatar
jihgfee committed
414
  Lemma proto_interp_nil p1 p2 : proto_interp [] p1 p2 - p1  iProto_dual p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
415 416
  Proof. done. Qed.

jihgfee's avatar
jihgfee committed
417
  Arguments proto_interp : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
418

Robbert Krebbers's avatar
Robbert Krebbers committed
419
  (** The actual specs *)
Robbert Krebbers's avatar
Robbert Krebbers committed
420
  Lemma proto_init E cγ c1 c2 p :
Robbert Krebbers's avatar
Robbert Krebbers committed
421
    is_chan protoN cγ c1 c2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
422
    chan_own cγ Left [] - chan_own cγ Right [] ={E}=
Robbert Krebbers's avatar
Robbert Krebbers committed
423
    c1  p  c2  iProto_dual p.
Robbert Krebbers's avatar
Robbert Krebbers committed
424 425 426 427 428
  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
429 430
    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
431 432
    { by apply auth_both_valid_2. }
    pose (ProtName cγ lγ rγ) as pγ.
Robbert Krebbers's avatar
Robbert Krebbers committed
433
    iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
434
    { iNext. rewrite /proto_inv. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
435
    iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
Robbert Krebbers's avatar
Robbert Krebbers committed
436 437 438 439
    - iExists Left, c1, c2, pγ; iFrame; auto.
    - iExists Right, c1, c2, pγ; iFrame; auto.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
440 441
  (** Accessor style lemmas *)
  Lemma proto_send_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
442 443
    protoN  E 
    c  iProto_message Send pc -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
444
       c = side_elim s c1 c2  
Robbert Krebbers's avatar
Robbert Krebbers committed
445
      is_chan protoN (proto_c_name γ) c1 c2  |={E,E∖↑protoN}=>  vs,
Robbert Krebbers's avatar
Robbert Krebbers committed
446
        chan_own (proto_c_name γ) s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
447 448
          (x : TT),
           (pc x).1.2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
449 450
           chan_own (proto_c_name γ) s (vs ++ [(pc x).1.1]) ={E∖↑protoN,E}=
           c  (pc x).2.
Robbert Krebbers's avatar
Robbert Krebbers committed
451
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
452 453
    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
454
    iExists s, c1, c2, γ. iSplit; first done. iFrame "Hcctx".
Robbert Krebbers's avatar
Robbert Krebbers committed
455
    iInv protoN as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
Robbert Krebbers's avatar
Robbert Krebbers committed
456 457 458 459 460 461
    (* 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
462
      iMod (proto_own_auth_update _ _ _ _ (pc x).2
Robbert Krebbers's avatar
Robbert Krebbers committed
463 464 465 466 467
        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]]".
jihgfee's avatar
jihgfee committed
468
        { iSplit=> //. iApply (proto_interp_send with "Heval [HP]").
Robbert Krebbers's avatar
Robbert Krebbers committed
469 470
          iIntros (f) "Hf /=". iExists x. by iFrame. }
        destruct r as [|vr r]; last first.
jihgfee's avatar
jihgfee committed
471 472 473 474
        { iDestruct (proto_interp_False with "Heval") as %[]. }
        iSplit; first done; simpl. iRewrite (proto_interp_nil with "Heval").
        iApply (proto_interp_send _ [] with "[] [HP]").
        { by rewrite /proto_interp involutive. }
Robbert Krebbers's avatar
Robbert Krebbers committed
475
        iIntros (f) "Hf /=". iExists x. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
476
      iModIntro. rewrite mapsto_proto_eq. iExists Left, c1, c2, γ. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
477 478 479 480
    - 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
481
      iMod (proto_own_auth_update _ _ _ _ (pc x).2
Robbert Krebbers's avatar
Robbert Krebbers committed
482 483 484 485 486
        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.
jihgfee's avatar
jihgfee committed
487
        { iSplit=> //. iApply (proto_interp_send with "Heval [HP]").
Robbert Krebbers's avatar
Robbert Krebbers committed
488 489
          iIntros (f) "Hf /=". iExists x. by iFrame. }
        destruct l as [|vl l]; last first.
jihgfee's avatar
jihgfee committed
490 491 492 493
        { iDestruct (proto_interp_False with "Heval") as %[]. }
        iSplit; first done; simpl. iRewrite (proto_interp_nil with "Heval").
        iApply (proto_interp_send _ [] with "[] [HP]").
        { by rewrite /proto_interp involutive. }
Robbert Krebbers's avatar
Robbert Krebbers committed
494
        iIntros (f) "Hf /=". iExists x. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
495
      iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
496 497
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
498
  Lemma proto_recv_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
499 500
    protoN  E 
    c  iProto_message Receive pc -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
501
       c = side_elim s c2 c1  
Robbert Krebbers's avatar
Robbert Krebbers committed
502
      is_chan protoN (proto_c_name γ) c1 c2  |={E,E∖↑protoN}=>  vs,
Robbert Krebbers's avatar
Robbert Krebbers committed
503
        chan_own (proto_c_name γ) s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
504 505
         ((chan_own (proto_c_name γ) s vs ={E∖↑protoN,E}=
             c  iProto_message Receive pc) 
Robbert Krebbers's avatar
Robbert Krebbers committed
506 507
           ( v vs',
              vs = v :: vs'  -
Robbert Krebbers's avatar
Robbert Krebbers committed
508 509
             chan_own (proto_c_name γ) s vs' ={E∖↑protoN,E}=    x : TT,
              v = (pc x).1.1   c  (pc x).2  (pc x).1.2)).
Robbert Krebbers's avatar
Robbert Krebbers committed
510
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
511 512
    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
513 514
    iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
    iFrame "Hcctx".
Robbert Krebbers's avatar
Robbert Krebbers committed
515
    iInv protoN as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
Robbert Krebbers's avatar
Robbert Krebbers committed
516 517 518 519 520 521 522 523 524 525
    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
526 527
        iModIntro. rewrite mapsto_proto_eq.
        iExists Left, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
528 529
      + iIntros (v vs ->) "Hown".
        iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
jihgfee's avatar
jihgfee committed
530
        iAssert ( proto_interp (v :: vs) pr (iProto_message_def Receive pc))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
531
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
532
        { iNext. by iRewrite "Heq" in "Heval". }
jihgfee's avatar
jihgfee committed
533
        iDestruct (proto_interp_recv with "Heval") as (q) "[Hf Heval]".
Robbert Krebbers's avatar
Robbert Krebbers committed
534 535 536 537
        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
538
        set (f lp := ( q, lp  Next q  c1  q)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
539
        assert (NonExpansive f) by solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
540 541 542 543 544
        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
545 546 547 548 549 550 551
    - 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
552 553
        iModIntro. rewrite mapsto_proto_eq.
        iExists Right, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
554 555
      + iIntros (v vs ->) "Hown".
        iDestruct "Hinv'" as "[[>-> Heval]|[>% _]]"; last done.
jihgfee's avatar
jihgfee committed
556
        iAssert ( proto_interp (v :: vs) pl (iProto_message_def Receive pc))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
557
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
558
        { iNext. by iRewrite "Heq" in "Heval". }
jihgfee's avatar
jihgfee committed
559
        iDestruct (proto_interp_recv with "Heval") as (q) "[Hf Heval]".
Robbert Krebbers's avatar
Robbert Krebbers committed
560 561 562 563
        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
564
        set (f lp := ( q, lp  Next q  c2  q)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
565
        assert (NonExpansive f) by solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
566 567 568 569 570
        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
571 572
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
573
  (** Specifications of send and receive *)
574
  Lemma new_chan_proto_spec :
Robbert Krebbers's avatar
Robbert Krebbers committed
575 576
    {{{ True }}}
      new_chan #()
Robbert Krebbers's avatar
Robbert Krebbers committed
577
    {{{ c1 c2, RET (c1,c2); ( p, |={}=> c1  p  c2  iProto_dual p) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
578
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
579
    iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
580 581
    iIntros (c1 c2 γ) "(Hc & Hl & Hr)". iApply "HΨ"; iIntros "!>" (p).
    iApply (proto_init  γ c1 c2 p with "Hc Hl Hr").
Robbert Krebbers's avatar
Robbert Krebbers committed
582 583
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
584
  Lemma start_chan_proto_spec p Ψ (f : val) :
Robbert Krebbers's avatar
Robbert Krebbers committed
585 586
     ( c, c  iProto_dual p - WP f c {{ _, True }}) -
     ( c, c  p - Ψ c) -
Robbert Krebbers's avatar
Robbert Krebbers committed
587 588 589
    WP start_chan f {{ Ψ }}.
  Proof.
    iIntros "Hfork HΨ". wp_lam.
590 591
    wp_apply (new_chan_proto_spec with "[//]"); iIntros (c1 c2) "Hc".
    iMod ("Hc" $! p) as "[Hc1 Hc2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
592 593 594 595 596
    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
597
  Lemma send_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) (x : TT) :
Robbert Krebbers's avatar
Robbert Krebbers committed
598
    {{{ c  iProto_message Send pc  (pc x).1.2 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
599
      send c (pc x).1.1
Robbert Krebbers's avatar
Robbert Krebbers committed
600
    {{{ RET #(); c  (pc x).2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
601 602 603 604 605 606 607 608 609
  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
610
  Lemma send_proto_spec {TT} Ψ c v (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
611
    c  iProto_message Send pc -
Robbert Krebbers's avatar
Robbert Krebbers committed
612
    (.. x : TT,
Robbert Krebbers's avatar
Robbert Krebbers committed
613
       v = (pc x).1.1   (pc x).1.2   (c  (pc x).2 - Ψ #())) -
Robbert Krebbers's avatar
Robbert Krebbers committed
614 615 616 617 618 619
    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
620
  Lemma try_recv_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
621
    {{{ c  iProto_message Receive pc }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
622
      try_recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
623 624
    {{{ v, RET v; (v = NONEV  c  iProto_message Receive pc) 
                  ( x : TT, v = SOMEV ((pc x).1.1)  c  (pc x).2  (pc x).1.2) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
625 626 627 628 629 630 631 632
  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
633 634
      iMod ("H" with "[//] Hch") as "H". iIntros "!> !> !>".
      iDestruct "H" as (x ->) "H". iApply "HΨ"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
635 636
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
637
  Lemma recv_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
638
    {{{ c  iProto_message Receive pc }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
639
      recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
640
    {{{ x, RET (pc x).1.1; c  (pc x).2  (pc x).1.2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
641 642 643 644 645
  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
646 647
    iMod ("H" with "[//] Hvs'") as "H"; iIntros "!> !> !>".
    iDestruct "H" as (x ->) "H". by iApply "HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
648 649
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
650
  Lemma recv_proto_spec {TT} Ψ c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
651 652
    c  iProto_message Receive pc -
     (.. x : TT, c  (pc x).2 - (pc x).1.2 - Ψ (pc x).1.1) -
Robbert Krebbers's avatar
Robbert Krebbers committed
653 654 655 656 657 658
    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
659

Robbert Krebbers's avatar
Robbert Krebbers committed
660
  (** Branching *)
661
  Lemma select_spec c (b : bool) P1 P2 p1 p2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
662
    {{{ c  (p1 <{P1}+{P2}> p2)  if b then P1 else P2 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
663
      send c #b
Robbert Krebbers's avatar
Robbert Krebbers committed
664
    {{{ RET #(); c  (if b then p1 else p2) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
665
  Proof.
666
    rewrite /iProto_branch. iIntros (Ψ) "[Hc HP] HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
667 668 669
    iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
  Qed.

670
  Lemma branch_spec c P1 P2 p1 p2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
671
    {{{ c  (p1 <{P1}&{P2}> p2) }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
672
      recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
673
    {{{ b, RET #b; c  (if b : bool then p1 else p2)  if b then P1 else P2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
674 675 676
  Proof.
    rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
    iApply (recv_proto_spec with "Hc"); simpl.
677
    iIntros "!>" (b) "Hc HP". iApply "HΨ". iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
678
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
679
End proto.