proto_channel.v 30.9 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10 11
(** This file defines the core of the Actris logic:

- It defines dependent separation protocols and the various operations on it
  dual, append, branching
- It defines the connective [c ↣ prot] for ownership of channel endpoints.
- It proves Actris's specifications of [send] and [receive] w.r.t. dependent
  separation protocols.

Dependent separation protocols are defined by instanting the parametrized
version in [proto_model] with type of values [val] of HeapLang and the
propositions [iProp] of Iris.
12

Jonas Kastberg's avatar
Jonas Kastberg committed
13
In doing so we define ways of constructing instances of the instantiated type
14
via two constructors:
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40
- [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, we provide the following notations:
- [END], which is simply [iProto_end].
- [<!> x1 .. xn, MSG v; {{ P }}; prot] and [<?> x1 .. xn, MSG v; {{ P }}; prot],
  which construct an instance of [iProto_message] with the appropriate
  continuation.

Futhermore, we define the following operations:
- [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

An encoding of the usual branching connectives [prot1 {Q1}<+>{Q2} prot2] and
[prot1 {Q1}<&>{Q2} prot2], inspired by session types, is also included in this
file.

The logical connective for protocol ownership is denoted as [c ↣ prot]. It
describes that channel endpoint [c] adheres to protocol [prot]. This connective
is modeled using Iris invariants and ghost state along with the logical
connectives of the channel encodings [is_chan] and [chan_own].

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
41 42
From actris.channel Require Export channel.
From actris.channel Require Import proto_model.
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45
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
46
From actris.utils Require Import auth_excl.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
Export action.
Robbert Krebbers's avatar
Robbert Krebbers committed
48

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
71
(** * Operators *)
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74 75 76 77 78 79 80
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,
Robbert Krebbers's avatar
Robbert Krebbers committed
81
    (** We need the later to make [iProto_message] contractive *)
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83 84
     v = (pc x).1.1  
     (pc x).1.2 
    f (Next (pc x).2))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Next Obligation. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
86 87 88 89
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.
Jonas Kastberg's avatar
Jonas Kastberg committed
90
Instance: Params (@iProto_message) 3 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
91

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
165
(** * Operations *)
Robbert Krebbers's avatar
Robbert Krebbers committed
166
Definition iProto_dual {Σ} (p : iProto Σ) : iProto Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
167
  proto_map action_dual cid cid p.
Robbert Krebbers's avatar
Robbert Krebbers committed
168
Arguments iProto_dual {_} _%proto.
Jonas Kastberg's avatar
Jonas Kastberg committed
169
Instance: Params (@iProto_dual) 1 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
170 171 172
Definition iProto_dual_if {Σ} (d : bool) (p : iProto Σ) : iProto Σ :=
  if d then iProto_dual p else p.
Arguments iProto_dual_if {_} _ _%proto.
Jonas Kastberg's avatar
Jonas Kastberg committed
173
Instance: Params (@iProto_dual_if) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
174

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

Robbert Krebbers's avatar
Robbert Krebbers committed
190 191
Definition iProto_app {Σ} (p1 p2 : iProto Σ) : iProto Σ := proto_app p1 p2.
Arguments iProto_app {_} _%proto _%proto.
Jonas Kastberg's avatar
Jonas Kastberg committed
192
Instance: Params (@iProto_app) 1 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
193 194
Infix "<++>" := iProto_app (at level 60) : proto_scope.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
232 233
Definition protoN := nroot .@ "proto".

Robbert Krebbers's avatar
Robbert Krebbers committed
234
(** * The connective for ownership of channel ends *)
Robbert Krebbers's avatar
Robbert Krebbers committed
235
Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
Robbert Krebbers's avatar
Robbert Krebbers committed
236 237 238
    (c : val) (p : iProto Σ) : iProp Σ :=
  ( s (c1 c2 : val) γ,
     c = side_elim s c1 c2  
Robbert Krebbers's avatar
Robbert Krebbers committed
239
    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
240 241 242
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
243 244
Arguments mapsto_proto {_ _ _} _ _%proto.
Instance: Params (@mapsto_proto) 4 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
245

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

Robbert Krebbers's avatar
Robbert Krebbers committed
249
(** * Proofs *)
Robbert Krebbers's avatar
Robbert Krebbers committed
250
Section proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
251
  Context `{!proto_chanG Σ, !heapG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
252 253 254
  Implicit Types p : iProto Σ.
  Implicit Types TT : tele.

Robbert Krebbers's avatar
Robbert Krebbers committed
255
  (** ** Non-expansiveness of operators *)
Robbert Krebbers's avatar
Robbert Krebbers committed
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
  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
288

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

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

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

  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.

335 336 337
  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
338 339 340 341 342
  Proof.
    rewrite /iProto_branch iProto_dual_message /=.
    by apply iProto_message_proper=> /= -[].
  Qed.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
375 376 377 378
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
379
  (** ** Auxiliary definitions and invariants *)
jihgfee's avatar
jihgfee committed
380
  Global Instance proto_interp_ne : NonExpansive2 (proto_interp vs).
Robbert Krebbers's avatar
Robbert Krebbers committed
381
  Proof. induction vs; solve_proper. Qed.
jihgfee's avatar
jihgfee committed
382
  Global Instance proto_interp_proper vs : Proper (() ==> () ==> ()) (proto_interp vs).
Robbert Krebbers's avatar
Robbert Krebbers committed
383 384 385 386 387 388
  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
389
  Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto c).
Robbert Krebbers's avatar
Robbert Krebbers committed
390
  Proof. rewrite mapsto_proto_eq. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
391
  Global Instance mapsto_proto_proper c : Proper (() ==> ()) (mapsto_proto c).
Robbert Krebbers's avatar
Robbert Krebbers committed
392 393 394 395 396 397 398 399 400
  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
401
    assert ( p,
Robbert Krebbers's avatar
Robbert Krebbers committed
402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418
      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
419 420
  Lemma proto_interp_send v vs pc p1 p2 :
    proto_interp vs (proto_message Send pc) p2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
421
    ( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p1) - pc v f) -
jihgfee's avatar
jihgfee committed
422
    proto_interp (vs ++ [v]) p1 p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
423 424 425
  Proof.
    iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl.
    - iDestruct "Heval" as "#Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
426 427 428
      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
429 430 431 432 433 434 435
      iSplit.
      { iIntros (f) "Hf /=". by iApply "Hc". }
      by rewrite involutive.
    - iDestruct "Heval" as (pc' p2') "(Heq & Hc' & Heval)".
      iExists pc', p2'. iFrame "Heq Hc'". iNext. iApply ("IH" with "Heval Hc").
  Qed.

jihgfee's avatar
jihgfee committed
436 437
  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
438
       ( f : laterO (iProto Σ) -n> iPropO Σ, f (Next p2) - pc v f) 
jihgfee's avatar
jihgfee committed
439
        proto_interp vs p1 p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
440 441 442 443 444 445 446
  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
447 448
  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
449 450 451 452 453
  Proof.
    simpl. iDestruct 1 as (pc' p2') "[Heq _]".
    by iDestruct (@proto_message_equivI with "Heq") as "[% _]".
  Qed.

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

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
692 693
  (** A version written without Texan triples that is more convenient to use
  (via [iApply] in Coq. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
694
  Lemma recv_proto_spec {TT} Ψ c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
695 696
    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
697 698 699 700 701 702
    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
703

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

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