proto_channel.v 29.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(** This file contains the instantiation of the
Dependent Separation Protocols with the encoded messages.
For starters this means fixing the types of message to the
language value type [val] and the logic to the iris logic [iProp Σ].

It then defines a convenient way of constructing instances of the type
via [iProto_end] and [iProto_message] with associated notation,
as well as type-specific variants of [dual] and [append].
An encoding of branching behaviour is additionally included, defined
in terms of sending and receiving boolean flags, along with relevant notation.

The logical connectives of protocol ownership [c >-> prot] are then defined.
This is achieved through Iris invariants and ghost state along with the
logical connectives of the channel encodings. 

Lastly, relevant typeclasses are defined for each of the above notions,
such as contractiveness and non-expansiveness, after which the specifications
of the message-passing primitives are defined in terms of the protocol connectives.
*)
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21
From actris.channel Require Export channel.
From actris.channel Require Import proto_model.
Robbert Krebbers's avatar
Robbert Krebbers committed
22 23 24
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
25
From actris.utils Require Import auth_excl.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Export action.
Robbert Krebbers's avatar
Robbert Krebbers committed
27

Robbert Krebbers's avatar
Robbert Krebbers committed
28 29 30 31
Definition start_chan : val := λ: "f",
  let: "cc" := new_chan #() in
  Fork ("f" (Snd "cc"));; Fst "cc".

Robbert Krebbers's avatar
Robbert Krebbers committed
32 33 34
(** Camera setup *)
Class proto_chanG Σ := {
  proto_chanG_chanG :> chanG Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
35
  proto_chanG_authG :> auth_exclG (laterO (proto val (iPrePropO Σ) (iPrePropO Σ))) Σ;
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38 39 40 41 42 43 44
}.

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
45
(** Types *)
Robbert Krebbers's avatar
Robbert Krebbers committed
46
Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48 49
Delimit Scope proto_scope with proto.
Bind Scope proto_scope with iProto.

Robbert Krebbers's avatar
Robbert Krebbers committed
50 51 52 53 54 55 56 57 58 59 60 61 62 63
(** 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
64
Next Obligation. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
65 66 67 68 69 70
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.

71
Notation "< a > x1 .. xn , 'MSG' v {{ P } } ; p" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74 75 76 77 78 79 80 81 82
  (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.
83
Notation "< a > 'MSG' v {{ P } } ; p" :=
84 85 86 87 88 89 90 91 92
  (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
93

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
144
(** Dual *)
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
146
  proto_map action_dual cid cid p.
Robbert Krebbers's avatar
Robbert Krebbers committed
147 148 149 150 151 152
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
153

Robbert Krebbers's avatar
Robbert Krebbers committed
154
(** Branching *)
155 156 157
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
158
Typeclasses Opaque iProto_branch.
159
Arguments iProto_branch {_} _ _%I _%I _%proto _%proto.
160
Instance: Params (@iProto_branch) 2.
161 162 163 164 165 166 167 168
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
169

Robbert Krebbers's avatar
Robbert Krebbers committed
170 171 172 173 174 175 176
(** 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
177
Fixpoint proto_interp `{!proto_chanG Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
178
  match vs with
Robbert Krebbers's avatar
Robbert Krebbers committed
179
  | [] => p1  iProto_dual p2
Robbert Krebbers's avatar
Robbert Krebbers committed
180 181
  | v :: vs =>  pc p2',
     p2  (proto_message Receive pc)%proto 
Robbert Krebbers's avatar
Robbert Krebbers committed
182
     ( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p2') - pc v f) 
jihgfee's avatar
jihgfee committed
183
      proto_interp vs p1 p2'
Robbert Krebbers's avatar
Robbert Krebbers committed
184
  end%I.
jihgfee's avatar
jihgfee committed
185
Arguments proto_interp {_ _} _ _%proto _%proto : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209

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

Robbert Krebbers's avatar
Robbert Krebbers committed
213 214 215
Definition protoN := nroot .@ "proto".

Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
Robbert Krebbers's avatar
Robbert Krebbers committed
216 217 218
    (c : val) (p : iProto Σ) : iProp Σ :=
  ( s (c1 c2 : val) γ,
     c = side_elim s c1 c2  
Robbert Krebbers's avatar
Robbert Krebbers committed
219
    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
220 221 222
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
223 224
Arguments mapsto_proto {_ _ _} _ _%proto.
Instance: Params (@mapsto_proto) 4 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
225

Robbert Krebbers's avatar
Robbert Krebbers committed
226 227
Notation "c ↣ p" := (mapsto_proto c p)
  (at level 20, format "c  ↣  p").
Robbert Krebbers's avatar
Robbert Krebbers committed
228 229

Section proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
230
  Context `{!proto_chanG Σ, !heapG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
231 232 233 234 235 236 237 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
  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
267

Robbert Krebbers's avatar
Robbert Krebbers committed
268
  Global Instance iProto_branch_contractive n a :
269 270
    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
271
  Proof.
272
    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
Robbert Krebbers's avatar
Robbert Krebbers committed
273 274
    apply iProto_message_contractive=> /= -[] //.
  Qed.
275 276
  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
277
  Proof.
278 279
    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
280 281
  Qed.
  Global Instance iProto_branch_proper a :
282 283 284 285 286
    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
287 288 289

  (** Dual *)
  Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
290
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
291
  Global Instance iProto_dual_proper : Proper (() ==> ()) (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
292
  Proof. apply (ne_proper _). Qed.
293 294 295 296
  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
297 298

  Global Instance iProto_dual_involutive : Involutive () (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
299
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
    intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
Robbert Krebbers's avatar
Robbert Krebbers committed
301 302
    apply: proto_map_ext=> //. by intros [].
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
303 304 305 306 307 308 309 310 311 312 313

  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.

314 315 316
  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
317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335
  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
336
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
337 338 339
    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
340
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
343 344 345
  Global Instance iProto_app_assoc : Assoc () (@iProto_app Σ).
  Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.

346 347 348
  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
349 350 351 352 353
  Proof.
    rewrite /iProto_branch iProto_app_message.
    by apply iProto_message_proper=> /= -[].
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
354 355 356 357 358
  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
359
  Global Instance proto_interp_ne : NonExpansive2 (proto_interp vs).
Robbert Krebbers's avatar
Robbert Krebbers committed
360
  Proof. induction vs; solve_proper. Qed.
jihgfee's avatar
jihgfee committed
361
  Global Instance proto_interp_proper vs : Proper (() ==> () ==> ()) (proto_interp vs).
Robbert Krebbers's avatar
Robbert Krebbers committed
362 363 364 365 366 367
  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
368
  Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto c).
Robbert Krebbers's avatar
Robbert Krebbers committed
369
  Proof. rewrite mapsto_proto_eq. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
370
  Global Instance mapsto_proto_proper c : Proper (() ==> ()) (mapsto_proto c).
Robbert Krebbers's avatar
Robbert Krebbers committed
371 372 373 374 375 376 377 378 379
  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
380
    assert ( p,
Robbert Krebbers's avatar
Robbert Krebbers committed
381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397
      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
398 399
  Lemma proto_interp_send v vs pc p1 p2 :
    proto_interp vs (proto_message Send pc) p2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
400
    ( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p1) - pc v f) -
jihgfee's avatar
jihgfee committed
401
    proto_interp (vs ++ [v]) p1 p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
402 403 404
  Proof.
    iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl.
    - iDestruct "Heval" as "#Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
405 406 407
      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
408 409 410 411 412 413 414
      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
415 416
  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
417
       ( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p2) - pc v f) 
jihgfee's avatar
jihgfee committed
418
        proto_interp vs p1 p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
419 420 421 422 423 424 425
  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
426 427
  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
428 429 430 431 432
  Proof.
    simpl. iDestruct 1 as (pc' p2') "[Heq _]".
    by iDestruct (@proto_message_equivI with "Heq") as "[% _]".
  Qed.

jihgfee's avatar
jihgfee committed
433
  Lemma proto_interp_nil p1 p2 : proto_interp [] p1 p2 - p1  iProto_dual p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
434 435
  Proof. done. Qed.

jihgfee's avatar
jihgfee committed
436
  Arguments proto_interp : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
437

Robbert Krebbers's avatar
Robbert Krebbers committed
438
  (** The actual specs *)
Robbert Krebbers's avatar
Robbert Krebbers committed
439
  Lemma proto_init E cγ c1 c2 p :
Robbert Krebbers's avatar
Robbert Krebbers committed
440
    is_chan protoN cγ c1 c2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
441
    chan_own cγ Left [] - chan_own cγ Right [] ={E}=
Robbert Krebbers's avatar
Robbert Krebbers committed
442
    c1  p  c2  iProto_dual p.
Robbert Krebbers's avatar
Robbert Krebbers committed
443 444 445 446 447
  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
448 449
    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
450 451
    { by apply auth_both_valid_2. }
    pose (ProtName cγ lγ rγ) as pγ.
Robbert Krebbers's avatar
Robbert Krebbers committed
452
    iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
453
    { iNext. rewrite /proto_inv. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
454
    iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
Robbert Krebbers's avatar
Robbert Krebbers committed
455 456 457 458
    - iExists Left, c1, c2, pγ; iFrame; auto.
    - iExists Right, c1, c2, pγ; iFrame; auto.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
459 460
  (** Accessor style lemmas *)
  Lemma proto_send_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
461 462
    protoN  E 
    c  iProto_message Send pc -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
463
       c = side_elim s c1 c2  
Robbert Krebbers's avatar
Robbert Krebbers committed
464
      is_chan protoN (proto_c_name γ) c1 c2  |={E,E∖↑protoN}=>  vs,
Robbert Krebbers's avatar
Robbert Krebbers committed
465
        chan_own (proto_c_name γ) s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
466 467
          (x : TT),
           (pc x).1.2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
468 469
           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
470
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
471 472
    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
473
    iExists s, c1, c2, γ. iSplit; first done. iFrame "Hcctx".
Robbert Krebbers's avatar
Robbert Krebbers committed
474
    iInv protoN as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
Robbert Krebbers's avatar
Robbert Krebbers committed
475 476 477 478 479 480
    (* 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
481
      iMod (proto_own_auth_update _ _ _ _ (pc x).2
Robbert Krebbers's avatar
Robbert Krebbers committed
482 483 484 485 486
        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
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 r as [|vr r]; 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 Left, c1, c2, γ. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
496 497 498 499
    - 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
500
      iMod (proto_own_auth_update _ _ _ _ (pc x).2
Robbert Krebbers's avatar
Robbert Krebbers committed
501 502 503 504 505
        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
506
        { iSplit=> //. iApply (proto_interp_send with "Heval [HP]").
Robbert Krebbers's avatar
Robbert Krebbers committed
507 508
          iIntros (f) "Hf /=". iExists x. by iFrame. }
        destruct l as [|vl l]; last first.
jihgfee's avatar
jihgfee committed
509 510 511 512
        { 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
513
        iIntros (f) "Hf /=". iExists x. by iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
514
      iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
515 516
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
517
  Lemma proto_recv_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
518 519
    protoN  E 
    c  iProto_message Receive pc -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
520
       c = side_elim s c2 c1  
Robbert Krebbers's avatar
Robbert Krebbers committed
521
      is_chan protoN (proto_c_name γ) c1 c2  |={E,E∖↑protoN}=>  vs,
Robbert Krebbers's avatar
Robbert Krebbers committed
522
        chan_own (proto_c_name γ) s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
523 524
         ((chan_own (proto_c_name γ) s vs ={E∖↑protoN,E}=
             c  iProto_message Receive pc) 
Robbert Krebbers's avatar
Robbert Krebbers committed
525 526
           ( v vs',
              vs = v :: vs'  -
Robbert Krebbers's avatar
Robbert Krebbers committed
527 528
             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
529
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
530 531
    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
532 533
    iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
    iFrame "Hcctx".
Robbert Krebbers's avatar
Robbert Krebbers committed
534
    iInv protoN as (l r pl pr) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')" "Hclose".
Robbert Krebbers's avatar
Robbert Krebbers committed
535 536 537 538 539 540 541 542 543 544
    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
545 546
        iModIntro. rewrite mapsto_proto_eq.
        iExists Left, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
547 548
      + iIntros (v vs ->) "Hown".
        iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
jihgfee's avatar
jihgfee committed
549
        iAssert ( proto_interp (v :: vs) pr (iProto_message_def Receive pc))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
550
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
551
        { iNext. by iRewrite "Heq" in "Heval". }
jihgfee's avatar
jihgfee committed
552
        iDestruct (proto_interp_recv with "Heval") as (q) "[Hf Heval]".
Robbert Krebbers's avatar
Robbert Krebbers committed
553 554 555 556
        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
557
        set (f lp := ( q, lp  Next q  c1  q)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
558
        assert (NonExpansive f) by solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
559 560 561 562 563
        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
564 565 566 567 568 569 570
    - 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
571 572
        iModIntro. rewrite mapsto_proto_eq.
        iExists Right, c1, c2, γ. by iFrame "Hcctx ∗ Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
573 574
      + iIntros (v vs ->) "Hown".
        iDestruct "Hinv'" as "[[>-> Heval]|[>% _]]"; last done.
jihgfee's avatar
jihgfee committed
575
        iAssert ( proto_interp (v :: vs) pl (iProto_message_def Receive pc))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
576
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
577
        { iNext. by iRewrite "Heq" in "Heval". }
jihgfee's avatar
jihgfee committed
578
        iDestruct (proto_interp_recv with "Heval") as (q) "[Hf Heval]".
Robbert Krebbers's avatar
Robbert Krebbers committed
579 580 581 582
        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
583
        set (f lp := ( q, lp  Next q  c2  q)%I).
Robbert Krebbers's avatar
Robbert Krebbers committed
584
        assert (NonExpansive f) by solve_proper.
Robbert Krebbers's avatar
Robbert Krebbers committed
585 586 587 588 589
        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
590 591
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
592
  (** Specifications of send and receive *)
593
  Lemma new_chan_proto_spec :
Robbert Krebbers's avatar
Robbert Krebbers committed
594 595
    {{{ True }}}
      new_chan #()
Robbert Krebbers's avatar
Robbert Krebbers committed
596
    {{{ c1 c2, RET (c1,c2); ( p, |={}=> c1  p  c2  iProto_dual p) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
597
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
598
    iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
599 600
    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
601 602
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
603
  Lemma start_chan_proto_spec p Ψ (f : val) :
Robbert Krebbers's avatar
Robbert Krebbers committed
604 605
     ( c, c  iProto_dual p - WP f c {{ _, True }}) -
     ( c, c  p - Ψ c) -
Robbert Krebbers's avatar
Robbert Krebbers committed
606 607 608
    WP start_chan f {{ Ψ }}.
  Proof.
    iIntros "Hfork HΨ". wp_lam.
609 610
    wp_apply (new_chan_proto_spec with "[//]"); iIntros (c1 c2) "Hc".
    iMod ("Hc" $! p) as "[Hc1 Hc2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
611 612 613 614 615
    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
616
  Lemma send_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) (x : TT) :
Robbert Krebbers's avatar
Robbert Krebbers committed
617
    {{{ c  iProto_message Send pc  (pc x).1.2 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
618
      send c (pc x).1.1
Robbert Krebbers's avatar
Robbert Krebbers committed
619
    {{{ RET #(); c  (pc x).2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
620 621 622 623 624 625 626 627 628
  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
629
  Lemma send_proto_spec {TT} Ψ c v (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
630
    c  iProto_message Send pc -
Robbert Krebbers's avatar
Robbert Krebbers committed
631
    (.. x : TT,
Robbert Krebbers's avatar
Robbert Krebbers committed
632
       v = (pc x).1.1   (pc x).1.2   (c  (pc x).2 - Ψ #())) -
Robbert Krebbers's avatar
Robbert Krebbers committed
633 634 635 636 637 638
    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
639
  Lemma try_recv_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
640
    {{{ c  iProto_message Receive pc }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
641
      try_recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
642 643
    {{{ 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
644 645 646 647 648 649 650 651
  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
652 653
      iMod ("H" with "[//] Hch") as "H". iIntros "!> !> !>".
      iDestruct "H" as (x ->) "H". iApply "HΨ"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
654 655
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
656
  Lemma recv_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
657
    {{{ c  iProto_message Receive pc }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
658
      recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
659
    {{{ x, RET (pc x).1.1; c  (pc x).2  (pc x).1.2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
660 661 662 663 664
  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
665 666
    iMod ("H" with "[//] Hvs'") as "H"; iIntros "!> !> !>".
    iDestruct "H" as (x ->) "H". by iApply "HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
667 668
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
669
  Lemma recv_proto_spec {TT} Ψ c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
670 671
    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
672 673 674 675 676 677
    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
678

Robbert Krebbers's avatar
Robbert Krebbers committed
679
  (** Branching *)
680
  Lemma select_spec c (b : bool) P1 P2 p1 p2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
681
    {{{ c  (p1 <{P1}+{P2}> p2)  if b then P1 else P2 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
682
      send c #b
Robbert Krebbers's avatar
Robbert Krebbers committed
683
    {{{ RET #(); c  (if b then p1 else p2) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
684
  Proof.
685
    rewrite /iProto_branch. iIntros (Ψ) "[Hc HP] HΨ".
Robbert Krebbers's avatar
Robbert Krebbers committed
686 687 688
    iApply (send_proto_spec with "Hc"); simpl; eauto with iFrame.
  Qed.

689
  Lemma branch_spec c P1 P2 p1 p2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
690
    {{{ c  (p1 <{P1}&{P2}> p2) }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
691
      recv c
Robbert Krebbers's avatar
Robbert Krebbers committed
692
    {{{ b, RET #b; c  (if b : bool then p1 else p2)  if b then P1 else P2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
693 694 695
  Proof.
    rewrite /iProto_branch. iIntros (Ψ) "Hc HΨ".
    iApply (recv_proto_spec with "Hc"); simpl.
696
    iIntros "!>" (b) "Hc HP". iApply "HΨ". iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
697
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
698
End proto.