proto_channel.v 38.1 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 *)
196 197 198
Definition proto_eq_next {Σ} (p : iProto Σ) : laterO (iProto Σ) -n> iPropO Σ :=
  OfeMor (sbi_internal_eq (Next p)).

199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
Program Definition iProto_le_aux {Σ} (rec : iProto Σ -n> iProto Σ -n> iPropO Σ) :
    iProto Σ -n> iProto Σ -n> iPropO Σ := λne p1 p2,
  ((p1  proto_end  p2  proto_end) 
   ( pc1 pc2,
     p1  proto_message Send pc1  p2  proto_message Send pc2 
      v p2', pc2 v (proto_eq_next p2') -
        p1',  rec p1' p2'  pc1 v (proto_eq_next p1')) 
   ( pc1 pc2,
     p1  proto_message Receive pc1  p2  proto_message Receive pc2 
      v p1', pc1 v (proto_eq_next p1') -
        p2',  rec p1' p2'  pc2 v (proto_eq_next p2')))%I.
Solve Obligations with solve_proper.
Local Instance iProto_le_aux_contractive {Σ} : Contractive (@iProto_le_aux Σ).
Proof. solve_contractive. Qed.
Definition iProto_le {Σ} (p1 p2 : iProto Σ) : iPropO Σ :=
  fixpoint iProto_le_aux p1 p2.
215
Arguments iProto_le {_} _%proto _%proto.
216 217

Fixpoint proto_interp {Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
218
  match vs with
219
  | [] => iProto_dual p1  p2
Robbert Krebbers's avatar
Robbert Krebbers committed
220
  | v :: vs =>  pc p2',
221 222
     p2  proto_message Receive pc 
     pc v (proto_eq_next p2') 
jihgfee's avatar
jihgfee committed
223
      proto_interp vs p1 p2'
Robbert Krebbers's avatar
Robbert Krebbers committed
224
  end%I.
225
Arguments proto_interp {_} _ _%proto _%proto : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
226 227 228 229 230 231 232

Record proto_name := ProtName {
  proto_c_name : chan_name;
  proto_l_name : gname;
  proto_r_name : gname
}.

233
Definition to_proto_auth_excl {Σ} (p : iProto Σ) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249
  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
250 251
     ((r = []  proto_interp l pl pr) 
       (l = []  proto_interp r pr pl)))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
252

Robbert Krebbers's avatar
Robbert Krebbers committed
253 254
Definition protoN := nroot .@ "proto".

Robbert Krebbers's avatar
Robbert Krebbers committed
255
(** * The connective for ownership of channel ends *)
Robbert Krebbers's avatar
Robbert Krebbers committed
256
Definition mapsto_proto_def `{!proto_chanG Σ, !heapG Σ}
Robbert Krebbers's avatar
Robbert Krebbers committed
257
    (c : val) (p : iProto Σ) : iProp Σ :=
258
  ( s (c1 c2 : val) γ p',
Robbert Krebbers's avatar
Robbert Krebbers committed
259
     c = side_elim s c1 c2  
260 261 262 263
     iProto_le p' p 
    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
264 265 266
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
267 268
Arguments mapsto_proto {_ _ _} _ _%proto.
Instance: Params (@mapsto_proto) 4 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
269

Robbert Krebbers's avatar
Robbert Krebbers committed
270 271
Notation "c ↣ p" := (mapsto_proto c p)
  (at level 20, format "c  ↣  p").
Robbert Krebbers's avatar
Robbert Krebbers committed
272

Robbert Krebbers's avatar
Robbert Krebbers committed
273
(** * Proofs *)
Robbert Krebbers's avatar
Robbert Krebbers committed
274
Section proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
275
  Context `{!proto_chanG Σ, !heapG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
276 277 278
  Implicit Types p : iProto Σ.
  Implicit Types TT : tele.

Robbert Krebbers's avatar
Robbert Krebbers committed
279
  (** ** Non-expansiveness of operators *)
Robbert Krebbers's avatar
Robbert Krebbers committed
280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311
  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
312

Robbert Krebbers's avatar
Robbert Krebbers committed
313
  Global Instance iProto_branch_contractive n a :
314 315
    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
316
  Proof.
317
    intros p1 p1' Hp1 p2 p2' Hp2 P1 P1' HP1 P2 P2' HP2.
Robbert Krebbers's avatar
Robbert Krebbers committed
318 319
    apply iProto_message_contractive=> /= -[] //.
  Qed.
320 321
  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
322
  Proof.
323 324
    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
325 326
  Qed.
  Global Instance iProto_branch_proper a :
327 328 329 330 331
    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
332

Robbert Krebbers's avatar
Robbert Krebbers committed
333
  (** ** Dual *)
Robbert Krebbers's avatar
Robbert Krebbers committed
334
  Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
335
  Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
  Global Instance iProto_dual_proper : Proper (() ==> ()) (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
337
  Proof. apply (ne_proper _). Qed.
338 339 340 341
  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
342 343

  Global Instance iProto_dual_involutive : Involutive () (@iProto_dual Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
344
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
    intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
Robbert Krebbers's avatar
Robbert Krebbers committed
346 347
    apply: proto_map_ext=> //. by intros [].
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
348 349 350 351 352 353 354 355 356 357 358

  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.

359 360 361
  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
362 363 364 365 366
  Proof.
    rewrite /iProto_branch iProto_dual_message /=.
    by apply iProto_message_proper=> /= -[].
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
367
  (** ** Append *)
Robbert Krebbers's avatar
Robbert Krebbers committed
368 369 370 371 372 373 374 375 376 377 378 379 380
  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
381
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
382 383 384
    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
385
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
386
    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
387
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
388 389 390
  Global Instance iProto_app_assoc : Assoc () (@iProto_app Σ).
  Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.

391 392 393
  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
394 395 396 397 398
  Proof.
    rewrite /iProto_branch iProto_app_message.
    by apply iProto_message_proper=> /= -[].
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
399 400 401 402
  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.

403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531
  (** ** Protocol entailment **)
  Global Instance iProto_le_ne : NonExpansive2 (@iProto_le Σ).
  Proof. solve_proper. Qed.
  Global Instance iProto_le_proper : Proper (() ==> () ==> ()) (@iProto_le Σ).
  Proof. solve_proper. Qed.

  Lemma iProto_le_unfold p1 p2 :
    iProto_le p1 p2  iProto_le_aux (fixpoint iProto_le_aux) p1 p2.
  Proof. apply: (fixpoint_unfold iProto_le_aux). Qed.

  Lemma iProto_le_refl p : iProto_le p p.
  Proof.
    iLöb as "IH" forall (p). destruct (proto_case p) as [->|([]&pc&->)].
    - rewrite iProto_le_unfold. iLeft; by auto.
    - rewrite iProto_le_unfold. iRight; iLeft. iExists _, _; do 2 (iSplit; [done|]).
      iIntros (v p') "Hpc". iExists p'. iFrame "Hpc". iNext. iApply "IH".
    - rewrite iProto_le_unfold. iRight; iRight. iExists _, _; do 2 (iSplit; [done|]).
      iIntros (v p') "Hpc". iExists p'. iFrame "Hpc". iNext. iApply "IH".
  Qed.

  Lemma iProto_le_end_inv p : iProto_le p proto_end - p  proto_end.
  Proof.
    rewrite iProto_le_unfold. iIntros "[[Hp _]|H] //".
    iDestruct "H" as "[H|H]"; iDestruct "H" as (pc1 pc2) "(_ & Heq & _)";
      by rewrite proto_end_message_equivI.
  Qed.

  Lemma iProto_le_send_inv p1 pc2 :
    iProto_le p1 (proto_message Send pc2) -  pc1,
      p1  proto_message Send pc1 
       v p2', pc2 v (proto_eq_next p2') -
         p1',  iProto_le p1' p2'  pc1 v (proto_eq_next p1').
  Proof.
    rewrite iProto_le_unfold. iIntros "[[_ Heq]|[H|H]]".
    - by rewrite proto_message_end_equivI.
    - iDestruct "H" as (pc1 pc2') "(Hp1 & Heq & H)".
      iDestruct (proto_message_equivI with "Heq") as "[_ #Heq]".
      iExists pc1. iIntros "{$Hp1}" (v p2') "Hpc".
      iSpecialize ("Heq" $! v). iDestruct (bi.ofe_morO_equivI with "Heq") as "Heq'".
      iRewrite ("Heq'" $! (proto_eq_next p2')) in "Hpc". by iApply "H".
    - iDestruct "H" as (pc1 pc2') "(_ & Heq & _)".
      by iDestruct (proto_message_equivI with "Heq") as "[% ?]".
  Qed.

  Lemma iProto_le_recv_inv p1 pc2 :
    iProto_le p1 (proto_message Receive pc2) -  pc1,
      p1  proto_message Receive pc1 
       v p1', pc1 v (proto_eq_next p1') -
         p2',  iProto_le p1' p2'  pc2 v (proto_eq_next p2').
  Proof.
    rewrite iProto_le_unfold. iIntros "[[_ Heq]|[H|H]]".
    - by rewrite proto_message_end_equivI.
    - iDestruct "H" as (pc1 pc2') "(_ & Heq & _)".
      by iDestruct (proto_message_equivI with "Heq") as "[% ?]".
    - iDestruct "H" as (pc1 pc2') "(Hp1 & Heq & H)".
      iDestruct (proto_message_equivI with "Heq") as "[_ #Heq]".
      iExists pc1. iIntros "{$Hp1}" (v p1') "Hpc".
      iSpecialize ("Heq" $! v). iDestruct (bi.ofe_morO_equivI with "Heq") as "Heq'".
      iDestruct ("H" with "Hpc") as (p2') "[Hle Hpc]".
      iExists p2'. iFrame "Hle". by iRewrite ("Heq'" $! (proto_eq_next p2')).
  Qed.

  Lemma iProto_le_trans p1 p2 p3 :
    iProto_le p1 p2 - iProto_le p2 p3 - iProto_le p1 p3.
  Proof.
    iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3).
    destruct (proto_case p3) as [->|([]&pc3&->)].
    - rewrite iProto_le_end_inv. by iRewrite "H2" in "H1".
    - iDestruct (iProto_le_send_inv with "H2") as (pc2) "[Hp2 H3]".
      iRewrite "Hp2" in "H1".
      iDestruct (iProto_le_send_inv with "H1") as (pc1) "[Hp1 H2]".
      iRewrite "Hp1". rewrite iProto_le_unfold; iRight; iLeft.
      iExists _, _; do 2 (iSplit; [done|]).
      iIntros (v p3') "Hpc".
      iDestruct ("H3" with "Hpc") as (p2') "[Hle Hpc]".
      iDestruct ("H2" with "Hpc") as (p1') "[Hle' Hpc]".
      iExists p1'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle'").
    - iDestruct (iProto_le_recv_inv with "H2") as (pc2) "[Hp2 H3]".
      iRewrite "Hp2" in "H1".
      iDestruct (iProto_le_recv_inv with "H1") as (pc1) "[Hp1 H2]".
      iRewrite "Hp1". rewrite iProto_le_unfold; iRight; iRight.
      iExists _, _; do 2 (iSplit; [done|]).
      iIntros (v p1') "Hpc".
      iDestruct ("H2" with "Hpc") as (p2') "[Hle Hpc]".
      iDestruct ("H3" with "Hpc") as (p3') "[Hle' Hpc]".
      iExists p3'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle").
  Qed.

  Lemma iProto_send_le {TT1 TT2} (pc1 : TT1  val * iProp Σ * iProto Σ)
      (pc2 : TT2  val * iProp Σ * iProto Σ) :
    (.. x2 : TT2, .. x1 : TT1,
      (pc1 x1).1.1 = (pc2 x2).1.1 
       ((pc2 x2).1.2 - (pc1 x1).1.2) 
      iProto_le (pc1 x1).2 (pc2 x2).2) -
    iProto_le (iProto_message Send pc1) (iProto_message Send pc2).
  Proof.
    iIntros "H". rewrite iProto_le_unfold iProto_message_eq. iRight; iLeft.
    iExists _, _; do 2 (iSplit; [done|]).
    iIntros (v p2') "/=". iDestruct 1 as (x2 ->) "[Hpc2 #Heq]".
    iDestruct ("H" $! x2) as (x1 ?) "[Hpc Hle]". iExists (pc1 x1).2. iSplitL "Hle".
    { iNext. change (fixpoint iProto_le_aux ?p1 ?p2) with (iProto_le p1 p2).
      by iRewrite "Heq". }
    iExists x1. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
  Qed.

  Lemma iProto_recv_le {TT1 TT2} (pc1 : TT1  val * iProp Σ * iProto Σ)
      (pc2 : TT2  val * iProp Σ * iProto Σ) :
    (.. x1 : TT1, .. x2 : TT2,
      (pc1 x1).1.1 = (pc2 x2).1.1 
       ((pc1 x1).1.2 - (pc2 x2).1.2) 
      iProto_le (pc1 x1).2 (pc2 x2).2) -
    iProto_le (iProto_message Receive pc1) (iProto_message Receive pc2).
  Proof.
    iIntros "H". rewrite iProto_le_unfold iProto_message_eq. iRight; iRight.
    iExists _, _; do 2 (iSplit; [done|]).
    iIntros (v p1') "/=". iDestruct 1 as (x1 ->) "[Hpc1 #Heq]".
    iDestruct ("H" $! x1) as (x2 ?) "[Hpc Hle]". iExists (pc2 x2).2. iSplitL "Hle".
    { iNext. change (fixpoint iProto_le_aux ?p1 ?p2) with (iProto_le p1 p2).
      by iRewrite "Heq". }
    iExists x2. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
  Qed.

  Lemma iProto_mapsto_le c p1 p2 : c  p1 - iProto_le p1 p2 - c  p2.
  Proof.
    rewrite mapsto_proto_eq. iDestruct 1 as (s c1 c2 γ p1' ->) "[Hle H]".
    iIntros "Hle'". iExists s, c1, c2, γ, p1'. iSplit; first done. iFrame "H".
    by iApply (iProto_le_trans with "Hle").
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
532
  (** ** Auxiliary definitions and invariants *)
533
  Global Instance proto_interp_ne : NonExpansive2 (proto_interp (Σ:=Σ) vs).
Robbert Krebbers's avatar
Robbert Krebbers committed
534
  Proof. induction vs; solve_proper. Qed.
535 536
  Global Instance proto_interp_proper vs :
    Proper (() ==> () ==> ()) (proto_interp (Σ:=Σ) vs).
Robbert Krebbers's avatar
Robbert Krebbers committed
537 538
  Proof. apply (ne_proper_2 _). Qed.

539
  Global Instance to_proto_auth_excl_ne : NonExpansive (to_proto_auth_excl (Σ:=Σ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
540 541 542
  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
543
  Global Instance mapsto_proto_ne c : NonExpansive (mapsto_proto c).
Robbert Krebbers's avatar
Robbert Krebbers committed
544
  Proof. rewrite mapsto_proto_eq. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
  Global Instance mapsto_proto_proper c : Proper (() ==> ()) (mapsto_proto c).
Robbert Krebbers's avatar
Robbert Krebbers committed
546 547 548 549 550 551 552 553 554
  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
555
    assert ( p,
Robbert Krebbers's avatar
Robbert Krebbers committed
556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572
      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.

573 574 575 576 577 578 579 580 581 582 583
  Lemma proto_eq_next_dual p :
    ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid (proto_eq_next (iProto_dual p)) 
    proto_eq_next p.
  Proof.
    intros lp. iSplit; iIntros "Hlp /="; last by iRewrite -"Hlp".
    destruct (Next_uninj lp) as [p' ->].
    rewrite /later_map /= !bi.later_equivI. iNext.
    rewrite -{2}(involutive iProto_dual p) -{2}(involutive iProto_dual p').
    by iRewrite "Hlp".
  Qed.

jihgfee's avatar
jihgfee committed
584 585
  Lemma proto_interp_send v vs pc p1 p2 :
    proto_interp vs (proto_message Send pc) p2 -
586
    pc v (proto_eq_next p1) -
jihgfee's avatar
jihgfee committed
587
    proto_interp (vs ++ [v]) p1 p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
588 589 590
  Proof.
    iIntros "Heval Hc". iInduction vs as [|v' vs] "IH" forall (p2); simpl.
    - iDestruct "Heval" as "#Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
591
      iExists _, (iProto_dual p1). iSplit.
592 593
      { iRewrite -"Heval". by rewrite /iProto_dual proto_map_message. }
      rewrite /= proto_eq_next_dual; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
594 595 596 597
    - 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
598 599
  Lemma proto_interp_recv v vs p1 pc :
     proto_interp (v :: vs) p1 (proto_message Receive pc) -  p2,
600
       pc v (proto_eq_next p2) 
jihgfee's avatar
jihgfee committed
601
        proto_interp vs p1 p2.
Robbert Krebbers's avatar
Robbert Krebbers committed
602 603 604 605
  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.
606
    by iRewrite ("Heq" $! (proto_eq_next p2)).
Robbert Krebbers's avatar
Robbert Krebbers committed
607 608
  Qed.

jihgfee's avatar
jihgfee committed
609 610
  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
611 612 613 614 615
  Proof.
    simpl. iDestruct 1 as (pc' p2') "[Heq _]".
    by iDestruct (@proto_message_equivI with "Heq") as "[% _]".
  Qed.

jihgfee's avatar
jihgfee committed
616
  Lemma proto_interp_nil p1 p2 : proto_interp [] p1 p2 - p1  iProto_dual p2.
617
  Proof. iIntros "#H /=". iRewrite -"H". by rewrite involutive. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
618

jihgfee's avatar
jihgfee committed
619
  Arguments proto_interp : simpl never.
Robbert Krebbers's avatar
Robbert Krebbers committed
620

Robbert Krebbers's avatar
Robbert Krebbers committed
621
  (** ** Initialization of a channel *)
Robbert Krebbers's avatar
Robbert Krebbers committed
622
  Lemma proto_init E cγ c1 c2 p :
Robbert Krebbers's avatar
Robbert Krebbers committed
623
    is_chan protoN cγ c1 c2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
624
    chan_own cγ Left [] - chan_own cγ Right [] ={E}=
Robbert Krebbers's avatar
Robbert Krebbers committed
625
    c1  p  c2  iProto_dual p.
Robbert Krebbers's avatar
Robbert Krebbers committed
626 627 628 629 630
  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
631 632
    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
633 634
    { by apply auth_both_valid_2. }
    pose (ProtName cγ lγ rγ) as pγ.
Robbert Krebbers's avatar
Robbert Krebbers committed
635
    iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
Robbert Krebbers's avatar
Robbert Krebbers committed
636
    { iNext. rewrite /proto_inv. eauto 10 with iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
637
    iModIntro. rewrite mapsto_proto_eq. iSplitL "Hlstf".
638 639 640 641
    - iExists Left, c1, c2, pγ, p.
      iFrame "Hlstf Hinv Hcctx". iSplit; [done|]. iApply iProto_le_refl.
    - iExists Right, c1, c2, pγ, (iProto_dual p).
      iFrame "Hrstf Hinv Hcctx". iSplit; [done|]. iApply iProto_le_refl.
Robbert Krebbers's avatar
Robbert Krebbers committed
642 643
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
644
  (** ** Accessor style lemmas *)
Robbert Krebbers's avatar
Robbert Krebbers committed
645
  Lemma proto_send_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
646 647
    protoN  E 
    c  iProto_message Send pc -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
648
       c = side_elim s c1 c2  
Robbert Krebbers's avatar
Robbert Krebbers committed
649
      is_chan protoN (proto_c_name γ) c1 c2  |={E,E∖↑protoN}=>  vs,
Robbert Krebbers's avatar
Robbert Krebbers committed
650
        chan_own (proto_c_name γ) s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
651 652
          (x : TT),
           (pc x).1.2 -
Robbert Krebbers's avatar
Robbert Krebbers committed
653 654
           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
655
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
656
    iIntros (?). rewrite {1}mapsto_proto_eq iProto_message_eq.
657
    iDestruct 1 as (s c1 c2 γ p ->) "(Hle & Hst & #[Hcctx Hinv])".
Robbert Krebbers's avatar
Robbert Krebbers committed
658
    iExists s, c1, c2, γ. iSplit; first done. iFrame "Hcctx".
659
    iInv protoN as (l r pl pr) "(>Hcl & >Hcr & Hstla & Hstra & Hinv')" "Hclose".
Robbert Krebbers's avatar
Robbert Krebbers committed
660 661 662
    (* TODO: refactor to avoid twice nearly the same proof *)
    iModIntro. destruct s.
    - iExists _.
663 664 665 666 667 668 669 670 671
      iIntros "{$Hcl} !>" (x) "HP Hcl".
      iDestruct (iProto_le_send_inv with "Hle") as (pc') "[Hp H] /=".
      iRewrite "Hp" in "Hst"; clear p.
      iDestruct ("H" with "[HP]") as (p1') "[Hle HP]".
      { iExists _. iFrame "HP". by iSplit. }
      iDestruct (proto_own_auth_agree with "Hstla Hst") as "#Heq".
      iMod (proto_own_auth_update _ _ _ _ p1' with "Hstla Hst") as "[Hstla Hst]".
      iMod ("Hclose" with "[-Hst Hle]") as "_".
      { iNext. iExists _,_,_,_. iFrame "Hcr Hstra Hstla Hcl". iLeft.
Robbert Krebbers's avatar
Robbert Krebbers committed
672 673
        iRewrite "Heq" in "Hinv'".
        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
674
        { iSplit=> //. by iApply (proto_interp_send with "Heval [HP]"). }
Robbert Krebbers's avatar
Robbert Krebbers committed
675
        destruct r as [|vr r]; last first.
jihgfee's avatar
jihgfee committed
676 677
        { iDestruct (proto_interp_False with "Heval") as %[]. }
        iSplit; first done; simpl. iRewrite (proto_interp_nil with "Heval").
678 679 680
        iApply (proto_interp_send _ [] with "[//] HP"). }
      iModIntro. rewrite mapsto_proto_eq. iExists Left, c1, c2, γ, p1'.
      by iFrame "Hcctx Hinv Hst Hle".
Robbert Krebbers's avatar
Robbert Krebbers committed
681
    - iExists _.
682 683 684 685 686 687 688 689 690
      iIntros "{$Hcr} !>" (x) "HP Hcr".
      iDestruct (iProto_le_send_inv with "Hle") as (pc') "[Hp H] /=".
      iRewrite "Hp" in "Hst"; clear p.
      iDestruct ("H" with "[HP]") as (p1') "[Hle HP]".
      { iExists _. iFrame "HP". by iSplit. }
      iDestruct (proto_own_auth_agree with "Hstra Hst") as "#Heq".
      iMod (proto_own_auth_update _ _ _ _ p1' with "Hstra Hst") as "[Hstra Hst]".
      iMod ("Hclose" with "[-Hst Hle]") as "_".
      { iNext. iExists _, _, _, _. iFrame "Hcl Hstra Hstla Hcr". iRight.
Robbert Krebbers's avatar
Robbert Krebbers committed
691 692
        iRewrite "Heq" in "Hinv'".
        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last first.
693
        { iSplit=> //. by iApply (proto_interp_send with "Heval [HP]"). }
Robbert Krebbers's avatar
Robbert Krebbers committed
694
        destruct l as [|vl l]; last first.
jihgfee's avatar
jihgfee committed
695 696
        { iDestruct (proto_interp_False with "Heval") as %[]. }
        iSplit; first done; simpl. iRewrite (proto_interp_nil with "Heval").
697 698 699
        iApply (proto_interp_send _ [] with "[//] HP"). }
      iModIntro. rewrite mapsto_proto_eq. iExists Right, c1, c2, γ, p1'.
      by iFrame "Hcctx Hinv Hst Hle".
Robbert Krebbers's avatar
Robbert Krebbers committed
700 701
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
702
  Lemma proto_recv_acc {TT} E c (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
703 704
    protoN  E 
    c  iProto_message Receive pc -  s c1 c2 γ,
Robbert Krebbers's avatar
Robbert Krebbers committed
705
       c = side_elim s c2 c1  
Robbert Krebbers's avatar
Robbert Krebbers committed
706
      is_chan protoN (proto_c_name γ) c1 c2  |={E,E∖↑protoN}=>  vs,
Robbert Krebbers's avatar
Robbert Krebbers committed
707
        chan_own (proto_c_name γ) s vs 
Robbert Krebbers's avatar
Robbert Krebbers committed
708 709
         ((chan_own (proto_c_name γ) s vs ={E∖↑protoN,E}=
             c  iProto_message Receive pc) 
Robbert Krebbers's avatar
Robbert Krebbers committed
710 711
           ( v vs',
              vs = v :: vs'  -
Robbert Krebbers's avatar
Robbert Krebbers committed
712 713
             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
714
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
715
    iIntros (?). rewrite {1}mapsto_proto_eq iProto_message_eq.
716 717
    iDestruct 1 as (s c1 c2 γ p ->) "(Hle & Hst & #[Hcctx Hinv])".
    iDestruct (iProto_le_recv_inv with "Hle") as (pc') "[Hp Hle]".
Robbert Krebbers's avatar
Robbert Krebbers committed
718 719
    iExists (side_elim s Right Left), c1, c2, γ. iSplit; first by destruct s.
    iFrame "Hcctx".
720
    iInv protoN as (l r pl pr) "(>Hcl & >Hcr & Hstla & Hstra & Hinv')" "Hclose".
Robbert Krebbers's avatar
Robbert Krebbers committed
721 722 723
    iExists (side_elim s r l). iModIntro.
    (* TODO: refactor to avoid twice nearly the same proof *)
    destruct s; simpl.
724 725
    - iIntros "{$Hcr} !>". iRewrite "Hp" in "Hst". clear p.
      iDestruct (proto_own_auth_agree with "Hstla Hst") as "#Heq".
Robbert Krebbers's avatar
Robbert Krebbers committed
726
      iSplit.
727 728
      + iIntros "Hcr".
        iMod ("Hclose" with "[-Hst Hle]") as "_".
Robbert Krebbers's avatar
Robbert Krebbers committed
729
        { iNext. iExists l, r, _, _. iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
730
        iModIntro. rewrite mapsto_proto_eq.
731 732 733 734
        iExists Left, c1, c2, γ, (proto_message Receive pc').
        iFrame "Hcctx Hinv Hst". iSplit; first done.
        rewrite iProto_le_unfold. iModIntro. iRight; auto 10.
      + iIntros (v vs ->) "Hcr".
Robbert Krebbers's avatar
Robbert Krebbers committed
735
        iDestruct "Hinv'" as "[[>% _]|[> -> Heval]]"; first done.
736
        iAssert ( proto_interp (v :: vs) pr (proto_message Receive pc'))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
737
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
738
        { iNext. by iRewrite "Heq" in "Heval". }
739 740 741 742
        iDestruct (proto_interp_recv with "Heval") as (q) "[Hpc Heval]".
        iMod (proto_own_auth_update _ _ _ _ q with "Hstla Hst") as "[Hstla Hst]".
        iMod ("Hclose" with "[-Hst Hpc Hle]") as %_.
        { iExists _, _,_ ,_; iFrame; eauto. }
743
        iIntros "!> !> /=".
744 745
        iDestruct ("Hle" with "Hpc") as (q') "[Hle H]".
        iDestruct "H" as (x) "(Hv & HP & #Hf) /=".
746
        iNext. iExists x. iFrame "Hv HP". iRewrite -"Hf".
747 748 749
        rewrite mapsto_proto_eq. iExists Left, c1, c2, γ, q. iFrame; auto.
    - iIntros "{$Hcl} !>". iRewrite "Hp" in "Hst". clear p.
      iDestruct (proto_own_auth_agree with "Hstra Hst") as "#Heq".
Robbert Krebbers's avatar
Robbert Krebbers committed
750
      iSplit.
751 752
      + iIntros "Hcl".
        iMod ("Hclose" with "[-Hst Hle]") as "_".
Robbert Krebbers's avatar
Robbert Krebbers committed
753
        { iNext. iExists l, r, _, _. iFrame. }
Robbert Krebbers's avatar
Robbert Krebbers committed
754
        iModIntro. rewrite mapsto_proto_eq.
755 756 757 758
        iExists Right, c1, c2, γ, (proto_message Receive pc').
        iFrame "Hcctx Hinv Hst". iSplit; first done.
        rewrite iProto_le_unfold. iModIntro. iRight; auto 10.
      + iIntros (v vs ->) "Hcl".
Robbert Krebbers's avatar
Robbert Krebbers committed
759
        iDestruct "Hinv'" as "[[>-> Heval]|[>% _]]"; last done.
760
        iAssert ( proto_interp (v :: vs) pl (proto_message Receive pc'))%I
Robbert Krebbers's avatar
Robbert Krebbers committed
761
          with "[Heval]" as "Heval".
Robbert Krebbers's avatar
Robbert Krebbers committed
762
        { iNext. by iRewrite "Heq" in "Heval". }
763 764 765
        iDestruct (proto_interp_recv with "Heval") as (q) "[Hpc Heval]".
        iMod (proto_own_auth_update _ _ _ _ q with "Hstra Hst") as "[Hstra Hst]".
        iMod ("Hclose" with "[-Hst Hpc Hle]") as %_.
Robbert Krebbers's avatar
Robbert Krebbers committed
766
        { iExists _, _, _, _. eauto 10 with iFrame. }
767 768 769
        iIntros "!> !> /=".
        iDestruct ("Hle" with "Hpc") as (q') "[Hle H]".
        iDestruct "H" as (x) "(Hv & HP & Hf) /=".
770
        iNext. iExists x. iFrame "Hv HP". iRewrite -"Hf".
771
        rewrite mapsto_proto_eq. iExists Right, c1, c2, γ, q. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
772 773
  Qed.

774
  (** ** Specifications of [send] and [recv] *)
775
  Lemma new_chan_proto_spec :
Robbert Krebbers's avatar
Robbert Krebbers committed
776 777
    {{{ True }}}
      new_chan #()
Robbert Krebbers's avatar
Robbert Krebbers committed
778
    {{{ c1 c2, RET (c1,c2); ( p, |={}=> c1  p  c2  iProto_dual p) }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
779
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
780
    iIntros (Ψ _) "HΨ". iApply wp_fupd. wp_apply new_chan_spec=> //.
781 782
    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
783 784
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
785
  Lemma start_chan_proto_spec p Ψ (f : val) :
Robbert Krebbers's avatar
Robbert Krebbers committed
786 787
     ( c, c  iProto_dual p - WP f c {{ _, True }}) -
     ( c, c  p - Ψ c) -
Robbert Krebbers's avatar
Robbert Krebbers committed
788 789 790
    WP start_chan f {{ Ψ }}.
  Proof.
    iIntros "Hfork HΨ". wp_lam.
791 792
    wp_apply (new_chan_proto_spec with "[//]"); iIntros (c1 c2) "Hc".
    iMod ("Hc" $! p) as "[Hc1 Hc2]".
Robbert Krebbers's avatar
Robbert Krebbers committed
793 794 795 796 797
    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
798
  Lemma send_proto_spec_packed {TT} c (pc : TT  val * iProp Σ * iProto Σ) (x : TT) :
Robbert Krebbers's avatar
Robbert Krebbers committed
799
    {{{ c  iProto_message Send pc  (pc x).1.2 }}}
Robbert Krebbers's avatar
Robbert Krebbers committed
800
      send c (pc x).1.1
Robbert Krebbers's avatar
Robbert Krebbers committed
801
    {{{ RET #(); c  (pc x).2 }}}.
Robbert Krebbers's avatar
Robbert Krebbers committed
802 803 804 805 806 807 808 809 810
  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
811 812
  (** A version written without Texan triples that is more convenient to use
  (via [iApply] in Coq. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
813
  Lemma send_proto_spec {TT} Ψ c v (pc : TT  val * iProp Σ * iProto Σ) :
Robbert Krebbers's avatar
Robbert Krebbers committed
814