proto_channel.v 30.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
(** This file contains an instantiation of the
Dependent Separation Protocols and an integration with the channel encodings.
For starters this means fixing the types of messages to the
value type of the language [val] and the logic to the iris logic [iProp Σ].

In doing so we define way of constructing instances of the instantiated type
via two constructors:
- [iProto_end] which is identical to [proto_end]
- [iProto_message] which takes an action and a continuation to construct
the corresponding message protocols.

For convenience sake the following notation is provided:
- [END] which is simply [iProto_end]
- [<!> x .. y, MSG v; {{ P }}; prot] and
- [<?> x .. y, MSG v; {{ P }}; prot] which constructs an instance of
iProto_message with an appropriate continuation.

Said continuation ultimately establishes the following:
- Existential quantification of variables [x .. y].
- The equivalence [v = w], where [w] is the value that is eventually sent.
- Ownership of the predicate P
- A continuation as [prot]

Futhermore type-specific variants of dual and append are provided:
- [iProto_dual] which turns all [Send] of a protocol into [Recv] and vice-versa
- [iProto_app] which appends two protocols as described in proto_model.v

28
An encoding of branching behaviour is additionally included, defined
29 30 31 32
in terms of sending and receiving boolean flags:
- [prot1 {Q1}<+>{Q2} prot2] and
- [prot1 {Q1}<&>{Q2} prot2] which defines ownership of Q1 or Q2, and continues as
Q1 or Q2, based on the sent or received flag.
33

34
The logical connective of protocol ownership are then defined:
35
- [c ↣  prot] which describes that channel endpoint [c] adheres
36 37
to protocol [prot], achieved through Iris invariants and ghost state along
with the logical connectives of the channel encodings [is_chan] and [chan_own]. 
38 39 40

Lastly, relevant typeclasses are defined for each of the above notions,
such as contractiveness and non-expansiveness, after which the specifications
41
of the message-passing primitives are defined in terms of the protocol connectives.*)
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
From actris.channel Require Export channel.
From actris.channel Require Import proto_model.
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45 46
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
47
From actris.utils Require Import auth_excl.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Export action.
Robbert Krebbers's avatar
Robbert Krebbers committed
49

Robbert Krebbers's avatar
Robbert Krebbers committed
50 51 52 53
Definition start_chan : val := λ: "f",
  let: "cc" := new_chan #() in
  Fork ("f" (Snd "cc"));; Fst "cc".

Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56
(** Camera setup *)
Class proto_chanG Σ := {
  proto_chanG_chanG :> chanG Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  proto_chanG_authG :> auth_exclG (laterO (proto val (iPrePropO Σ) (iPrePropO Σ))) Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59 60 61 62 63 64 65 66
}.

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
67
(** Types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
69 70 71
Delimit Scope proto_scope with proto.
Bind Scope proto_scope with iProto.

Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74 75 76 77 78 79 80 81 82 83 84 85
(** 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
86
Next Obligation. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89 90 91 92
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.

93
Notation "< a > x1 .. xn , 'MSG' v {{ P } } ; p" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
94 95 96 97 98 99 100 101 102 103 104
  (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.
105
Notation "< a > 'MSG' v {{ P } } ; p" :=
106 107 108 109 110 111 112 113 114
  (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
115

116
Notation "<!> x1 .. xn , 'MSG' v {{ P } } ; p" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
117 118 119 120 121 122 123 124 125 126 127
  (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.
128
Notation "<!> 'MSG' v {{ P } } ; p" :=
129 130 131 132 133 134 135 136 137 138 139
  (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
140

141
Notation "<?> x1 .. xn , 'MSG' v {{ P } } ; p" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143 144 145 146 147 148 149 150 151 152
  (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.
153
Notation "<?> 'MSG' v {{ P } } ; p" :=
154 155 156 157 158 159 160 161 162
  (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
163 164

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

Robbert Krebbers's avatar
Robbert Krebbers committed
166
(** Dual *)
Robbert Krebbers's avatar
Robbert Krebbers committed
167
Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
168
  proto_map action_dual cid cid p.
Robbert Krebbers's avatar
Robbert Krebbers committed
169 170 171 172 173 174
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
175

Robbert Krebbers's avatar
Robbert Krebbers committed
176
(** Branching *)
177 178 179
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
180
Typeclasses Opaque iProto_branch.
181
Arguments iProto_branch {_} _ _%I _%I _%proto _%proto.
182
Instance: Params (@iProto_branch) 2.
183 184 185 186 187 188 189 190
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
191

Robbert Krebbers's avatar
Robbert Krebbers committed
192 193 194 195 196 197 198
(** 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
199
Fixpoint proto_interp `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
200
  match vs with
Robbert Krebbers's avatar
Robbert Krebbers committed
201
  | [] => p1  iProto_dual p2
Robbert Krebbers's avatar
Robbert Krebbers committed
202 203
  | v :: vs =>  pc p2',
     p2  (proto_message Receive pc)%proto 
Robbert Krebbers's avatar
Robbert Krebbers committed
204
     ( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p2') - pc v f) 
jihgfee's avatar
jihgfee committed
205
      proto_interp vs p1 p2'
Robbert Krebbers's avatar
Robbert Krebbers committed
206
  end%I.
jihgfee's avatar
jihgfee committed
207
Arguments proto_interp {_ _} _ _%proto _%proto : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231

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
232 233
     ((r = []  proto_interp l pl pr) 
       (l = []  proto_interp r pr pl)))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
234

Robbert Krebbers's avatar
Robbert Krebbers committed
235 236 237
Definition protoN := nroot .@ "proto".

Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
Robbert Krebbers's avatar
Robbert Krebbers committed
238 239 240
    (c : val) (p : iProto Σ) : iProp Σ :=
  ( s (c1 c2 : val) γ,
     c = side_elim s c1 c2  
Robbert Krebbers's avatar
Robbert Krebbers committed
241
    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
242 243 244
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
245 246
Arguments mapsto_proto {_ _ _} _ _%proto.
Instance: Params (@mapsto_proto) 4 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
247

Robbert Krebbers's avatar
Robbert Krebbers committed
248 249
Notation "c ↣ p" := (mapsto_proto c p)
  (at level 20, format "c  ↣  p").
Robbert Krebbers's avatar
Robbert Krebbers committed
250 251

Section proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
252
  Context `{!proto_chanG Σ, !heapG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 279 280 281 282 283 284 285 286 287 288
  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
289

Robbert Krebbers's avatar
Robbert Krebbers committed
290
  Global Instance iProto_branch_contractive n a :
291 292
    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
293
  Proof.
294
    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
Robbert Krebbers's avatar
Robbert Krebbers committed
295 296
    apply iProto_message_contractive=> /= -[] //.
  Qed.
297 298
  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
299
  Proof.
300 301
    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
302 303
  Qed.
  Global Instance iProto_branch_proper a :
304 305 306 307 308
    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
309 310 311

  (** Dual *)
  Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
312
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
313
  Global Instance iProto_dual_proper : Proper (() ==> ()) (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
314
  Proof. apply (ne_proper _). Qed.
315 316 317 318
  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
319 320

  Global Instance iProto_dual_involutive : Involutive () (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
321
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
322
    intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
Robbert Krebbers's avatar
Robbert Krebbers committed
323 324
    apply: proto_map_ext=> //. by intros [].
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
325 326 327 328 329 330 331 332 333 334 335

  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.

336 337 338
  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
339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357
  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
358
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
359 360 361
    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
362
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
363
    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
364
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
365 366 367
  Global Instance iProto_app_assoc : Assoc () (@iProto_app Σ).
  Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.

368 369 370
  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
371 372 373 374 375
  Proof.
    rewrite /iProto_branch iProto_app_message.
    by apply iProto_message_proper=> /= -[].
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
376 377 378 379 380
  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
381
  Global Instance proto_interp_ne : NonExpansive2 (proto_interp vs).
Robbert Krebbers's avatar
Robbert Krebbers committed
382
  Proof. induction vs; solve_proper. Qed.
jihgfee's avatar
jihgfee committed
383
  Global Instance proto_interp_proper vs : Proper (() ==> () ==> ()) (proto_interp vs).
Robbert Krebbers's avatar
Robbert Krebbers committed
384 385 386 387 388 389
  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
390
  Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto c).
Robbert Krebbers's avatar
Robbert Krebbers committed
391
  Proof. rewrite mapsto_proto_eq. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
392
  Global Instance mapsto_proto_proper c : Proper (() ==> ()) (mapsto_proto c).
Robbert Krebbers's avatar
Robbert Krebbers committed
393 394 395 396 397 398 399 400 401
  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
402
    assert ( p,
Robbert Krebbers's avatar
Robbert Krebbers committed
403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419
      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
420 421
  Lemma proto_interp_send v vs pc p1 p2 :
    proto_interp vs (proto_message Send pc) p2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
422
    ( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p1) - pc v f) -
jihgfee's avatar
jihgfee committed
423
    proto_interp (vs ++ [v]) p1 p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
424 425 426
  Proof.
    iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl.
    - iDestruct "Heval" as "#Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
427 428 429
      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
430 431 432 433 434 435 436
      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
437 438
  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
439
       ( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p2) - pc v f) 
jihgfee's avatar
jihgfee committed
440
        proto_interp vs p1 p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
441 442 443 444 445 446 447
  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
448 449
  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
450 451 452 453 454
  Proof.
    simpl. iDestruct 1 as (pc' p2') "[Heq _]".
    by iDestruct (@proto_message_equivI with "Heq") as "[% _]".
  Qed.

jihgfee's avatar
jihgfee committed
455
  Lemma proto_interp_nil p1 p2 : proto_interp [] p1 p2 - p1  iProto_dual p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
456 457
  Proof. done. Qed.

jihgfee's avatar
jihgfee committed
458
  Arguments proto_interp : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
459

Robbert Krebbers's avatar
Robbert Krebbers committed
460
  (** The actual specs *)
Robbert Krebbers's avatar
Robbert Krebbers committed
461
  Lemma proto_init E cγ c1 c2 p :
Robbert Krebbers's avatar
Robbert Krebbers committed
462
    is_chan protoN cγ c1 c2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
463
    chan_own cγ Left [] - chan_own cγ Right [] ={E}=
Robbert Krebbers's avatar
Robbert Krebbers committed
464
    c1  p  c2  iProto_dual p.
Robbert Krebbers's avatar
Robbert Krebbers committed
465 466 467 468 469
  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
470 471
    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
472 473
    { by apply auth_both_valid_2. }
    pose (ProtName cγ lγ rγ) as pγ.
Robbert Krebbers's avatar
Robbert Krebbers committed
474
    iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
475
    { iNext. rewrite /proto_inv. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
476
    iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
Robbert Krebbers's avatar
Robbert Krebbers committed
477 478 479 480
    - iExists Left, c1, c2, pγ; iFrame; auto.
    - iExists Right, c1, c2, pγ; iFrame; auto.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
481 482
  (** Accessor style lemmas *)
  Lemma proto_send_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
483 484
    protoN  E 
    c  iProto_message Send pc -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
485
       c = side_elim s c1 c2  
Robbert Krebbers's avatar
Robbert Krebbers committed
486
      is_chan protoN (proto_c_name γ) c1 c2  |={E,E∖↑protoN}=>  vs,
Robbert Krebbers's avatar
Robbert Krebbers committed
487
        chan_own (proto_c_name γ) s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
488 489
          (x : TT),
           (pc x).1.2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
490 491
           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
492
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
493 494
    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
495
    iExists s, c1, c2, γ. iSplit; first done. iFrame "Hcctx".
Robbert Krebbers's avatar
Robbert Krebbers committed
496
    iInv protoN as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
Robbert Krebbers's avatar
Robbert Krebbers committed
497 498 499 500 501 502
    (* 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
503
      iMod (proto_own_auth_update _ _ _ _ (pc x).2
Robbert Krebbers's avatar
Robbert Krebbers committed
504 505 506 507 508
        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
509
        { iSplit=> //. iApply (proto_interp_send with "Heval [HP]").
Robbert Krebbers's avatar
Robbert Krebbers committed
510 511
          iIntros (f) "Hf /=". iExists x. by iFrame. }
        destruct r as [|vr r]; last first.
jihgfee's avatar
jihgfee committed
512 513 514 515
        { 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
516
        iIntros (f) "Hf /=". iExists x. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
517
      iModIntro. rewrite mapsto_proto_eq. iExists Left, c1, c2, γ. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
518 519 520 521
    - 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
522
      iMod (proto_own_auth_update _ _ _ _ (pc x).2
Robbert Krebbers's avatar
Robbert Krebbers committed
523 524 525 526 527
        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
528
        { iSplit=> //. iApply (proto_interp_send with "Heval [HP]").
Robbert Krebbers's avatar
Robbert Krebbers committed
529 530
          iIntros (f) "Hf /=". iExists x. by iFrame. }
        destruct l as [|vl l]; last first.
jihgfee's avatar
jihgfee committed
531 532 533 534
        { 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
535
        iIntros (f) "Hf /=". iExists x. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
536
      iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
537 538
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
539
  Lemma proto_recv_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
540 541
    protoN  E 
    c  iProto_message Receive pc -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
542
       c = side_elim s c2 c1  
Robbert Krebbers's avatar
Robbert Krebbers committed
543
      is_chan protoN (proto_c_name γ) c1 c2  |={E,E∖↑protoN}=>  vs,
Robbert Krebbers's avatar
Robbert Krebbers committed
544
        chan_own (proto_c_name γ) s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
545 546
         ((chan_own (proto_c_name γ) s vs ={E∖↑protoN,E}=
             c  iProto_message Receive pc) 
Robbert Krebbers's avatar
Robbert Krebbers committed
547 548
           ( v vs',
              vs = v :: vs'  -
Robbert Krebbers's avatar
Robbert Krebbers committed
549 550
             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
551
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
552 553
    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
554 555
    iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
    iFrame "Hcctx".
Robbert Krebbers's avatar
Robbert Krebbers committed
556
    iInv protoN as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
Robbert Krebbers's avatar
Robbert Krebbers committed
557 558 559 560 561 562 563 564 565 566
    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
567 568
        iModIntro. rewrite mapsto_proto_eq.
        iExists Left, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
569 570
      + iIntros (v vs ->) "Hown".
        iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
jihgfee's avatar
jihgfee committed
571
        iAssert ( proto_interp (v :: vs) pr (iProto_message_def Receive pc))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
572
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
573
        { iNext. by iRewrite "Heq" in "Heval". }
jihgfee's avatar
jihgfee committed
574
        iDestruct (proto_interp_recv with "Heval") as (q) "[Hf Heval]".
Robbert Krebbers's avatar
Robbert Krebbers committed
575 576 577 578
        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
579
        set (f lp := ( q, lp  Next q  c1  q)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
580
        assert (NonExpansive f) by solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
581 582 583 584 585
        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
586 587 588 589 590 591 592
    - 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
593 594
        iModIntro. rewrite mapsto_proto_eq.
        iExists Right, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
595 596
      + iIntros (v vs ->) "Hown".
        iDestruct "Hinv'" as "[[>-> Heval]|[>% _]]"; last done.
jihgfee's avatar
jihgfee committed
597
        iAssert ( proto_interp (v :: vs) pl (iProto_message_def Receive pc))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
598
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
599
        { iNext. by iRewrite "Heq" in "Heval". }
jihgfee's avatar
jihgfee committed
600
        iDestruct (proto_interp_recv with "Heval") as (q) "[Hf Heval]".
Robbert Krebbers's avatar
Robbert Krebbers committed
601 602 603 604
        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
605
        set (f lp := ( q, lp  Next q  c2  q)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
606
        assert (NonExpansive f) by solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
607 608 609 610 611
        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
612 613
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
614
  (** Specifications of send and receive *)
615
  Lemma new_chan_proto_spec :
Robbert Krebbers's avatar
Robbert Krebbers committed
616 617
    {{{ True }}}
      new_chan #()
Robbert Krebbers's avatar
Robbert Krebbers committed
618
    {{{ c1 c2, RET (c1,c2); ( p, |={}=> c1  p  c2  iProto_dual p) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
619
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
620
    iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
621 622
    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
623 624
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
625
  Lemma start_chan_proto_spec p Ψ (f : val) :
Robbert Krebbers's avatar
Robbert Krebbers committed
626 627
     ( c, c  iProto_dual p - WP f c {{ _, True }}) -
     ( c, c  p - Ψ c) -
Robbert Krebbers's avatar
Robbert Krebbers committed
628 629 630
    WP start_chan f {{ Ψ }}.
  Proof.
    iIntros "Hfork HΨ". wp_lam.
631 632
    wp_apply (new_chan_proto_spec with "[//]"); iIntros (c1 c2) "Hc".
    iMod ("Hc" $! p) as "[Hc1 Hc2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
633 634 635 636 637
    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
638
  Lemma send_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) (x : TT) :
Robbert Krebbers's avatar
Robbert Krebbers committed
639
    {{{ c  iProto_message Send pc  (pc x).1.2 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
640
      send c (pc x).1.1
Robbert Krebbers's avatar
Robbert Krebbers committed
641
    {{{ RET #(); c  (pc x).2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
642 643 644 645 646 647 648 649 650
  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
651
  Lemma send_proto_spec {TT} Ψ c v (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
652
    c  iProto_message Send pc -
Robbert Krebbers's avatar
Robbert Krebbers committed
653
    (.. x : TT,
Robbert Krebbers's avatar
Robbert Krebbers committed
654
       v = (pc x).1.1   (pc x).1.2   (c  (pc x).2 - Ψ #())) -
Robbert Krebbers's avatar
Robbert Krebbers committed
655 656 657 658 659 660
    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
661
  Lemma try_recv_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
662
    {{{ c  iProto_message Receive pc }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
663
      try_recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
664 665
    {{{ 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
666 667 668 669 670 671 672 673
  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
674 675
      iMod ("H" with "[//] Hch") as "H". iIntros "!> !> !>".
      iDestruct "H" as (x ->) "H". iApply "HΨ"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
676 677
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
678
  Lemma recv_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
679
    {{{ c  iProto_message Receive pc }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
680
      recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
681
    {{{ x, RET (pc x).1.1; c  (pc x).2  (pc x).1.2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
682 683 684 685 686
  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
687 688
    iMod ("H" with "[//] Hvs'") as "H"; iIntros "!> !> !>".
    iDestruct "H" as (x ->) "H". by iApply "HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
689 690
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
691
  Lemma recv_proto_spec {TT} Ψ c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
692 693
    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
694 695 696 697 698 699
    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
700

Robbert Krebbers's avatar
Robbert Krebbers committed
701
  (** Branching *)
702
  Lemma select_spec c (b : bool) P1 P2 p1 p2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
703
    {{{ c  (p1 <{P1}+{P2}> p2)  if b then P1 else P2 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
704
      send c #b
Robbert Krebbers's avatar
Robbert Krebbers committed
705
    {{{ RET #(); c  (if b then p1 else p2) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
706
  Proof.
707
    rewrite /iProto_branch. iIntros (Ψ) "[Hc HP] HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
708 709 710
    iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
  Qed.

711
  Lemma branch_spec c P1 P2 p1 p2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
712
    {{{ c  (p1 <{P1}&{P2}> p2) }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
713
      recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
714
    {{{ b, RET #b; c  (if b : bool then p1 else p2)  if b then P1 else P2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
715 716 717
  Proof.
    rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
    iApply (recv_proto_spec with "Hc"); simpl.
718
    iIntros "!>" (b) "Hc HP". iApply "HΨ". iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
719
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
720
End proto.