proto.v 40 KB
Newer Older
1 2 3
(** This file defines the core of the Actris logic: It defines dependent
separation protocols and the various operations on it like dual, append, and
branching.
Robbert Krebbers's avatar
Robbert Krebbers committed
4

Robbert Krebbers's avatar
Robbert Krebbers committed
5
Dependent separation protocols are defined by instantiating the parameterized
6 7
version in [proto_model] with type of propositions [iProp] of Iris. We define
ways of constructing instances of the instantiated type via two constructors:
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10 11 12 13 14 15 16 17 18 19 20 21
- [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

Robbert Krebbers's avatar
Robbert Krebbers committed
22 23 24 25
Lastly, relevant type classes instances 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. *)
26
From iris.algebra Require Import excl_auth.
27 28 29 30 31
From iris.bi Require Import telescopes.
From iris.program_logic Require Import language.
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import lib.own.
From actris.channel Require Import proto_model.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Export action.
Robbert Krebbers's avatar
Robbert Krebbers committed
33

Robbert Krebbers's avatar
Robbert Krebbers committed
34
(** * Setup of Iris's cameras *)
35 36 37 38 39 40
Class protoG Σ V :=
  protoG_authG :>
    inG Σ (excl_authR (laterO (proto (leibnizO V) (iPrePropO Σ) (iPrePropO Σ)))).

Definition protoΣ V := #[
  GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
Robbert Krebbers's avatar
Robbert Krebbers committed
41
].
42 43
Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ  protoG Σ V.
Proof. solve_inG. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
44

Robbert Krebbers's avatar
Robbert Krebbers committed
45
(** * Types *)
46
Definition iProto Σ V := proto V (iPropO Σ) (iPropO Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48 49
Delimit Scope proto_scope with proto.
Bind Scope proto_scope with iProto.

Robbert Krebbers's avatar
Robbert Krebbers committed
50
(** * Operators *)
51
Definition iProto_end_def {Σ V} : iProto Σ V := proto_end.
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53 54
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).
55
Arguments iProto_end {_ _}.
Robbert Krebbers's avatar
Robbert Krebbers committed
56

57 58
Program Definition iProto_message_def {Σ V} {TT : tele} (a : action)
    (pc : TT  V * iProp Σ * iProto Σ V) : iProto Σ V :=
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  proto_message a (λ v, λne f,  x : TT,
Robbert Krebbers's avatar
Robbert Krebbers committed
60
    (** We need the later to make [iProto_message] contractive *)
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62 63
     v = (pc x).1.1  
     (pc x).1.2 
    f (Next (pc x).2))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Next Obligation. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
65 66
Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
Definition iProto_message := iProto_message_aux.(unseal).
Robbert Krebbers's avatar
Robbert Krebbers committed
67 68
Definition iProto_message_eq :
  @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
69 70
Arguments iProto_message {_ _ _} _ _%proto.
Instance: Params (@iProto_message) 4 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
71

72
Notation "< a > x1 .. xn , 'MSG' v {{ P } } ; p" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
73 74 75 76
  (iProto_message
    a
    (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                       λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78
  (at level 20, a at level 10, x1 binder, xn binder,
   v at level 20, P, p at level 200) : proto_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80 81 82 83
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)) ..))
Robbert Krebbers's avatar
Robbert Krebbers committed
84 85
  (at level 20, a at level 10, x1 binder, xn binder,
   v at level 20, p at level 200) : proto_scope.
86
Notation "< a > 'MSG' v {{ P } } ; p" :=
87 88 89 90 91 92 93 94 95
  (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
96

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
147
(** * Operations *)
148
Definition iProto_dual {Σ V} (p : iProto Σ V) : iProto Σ V :=
Robbert Krebbers's avatar
Robbert Krebbers committed
149
  proto_map action_dual cid cid p.
150 151 152
Arguments iProto_dual {_ _} _%proto.
Instance: Params (@iProto_dual) 2 := {}.
Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
Robbert Krebbers's avatar
Robbert Krebbers committed
153
  if d then iProto_dual p else p.
154 155 156 157 158 159
Arguments iProto_dual_if {_ _} _ _%proto.
Instance: Params (@iProto_dual_if) 3 := {}.

Definition iProto_app {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V := proto_app p1 p2.
Arguments iProto_app {_ _} _%proto _%proto.
Instance: Params (@iProto_app) 2 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
160 161
Infix "<++>" := iProto_app (at level 60) : proto_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
162
(** * Auxiliary definitions and invariants *)
163
Definition proto_eq_next {Σ V} (p : iProto Σ V) : laterO (iProto Σ V) -n> iPropO Σ :=
164 165
  OfeMor (sbi_internal_eq (Next p)).

Robbert Krebbers's avatar
Robbert Krebbers committed
166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185
(*
The definition [iProto_le] generalizes the following inductive definition
for subtyping on session types:

                 p1 <: p2           p1 <: p2
----------   ----------------   ----------------
end <: end    !A.p1 <: !A.p2     ?A.p1 <: ?A.p2

 p1 <: !B.p3    ?A.p3 <: p2
----------------------------
       ?A.p1 <: !B.p2

Example:

!R <: !R  ?Q <: ?Q      ?Q <: ?Q
-------------------  --------------
?Q.!R <: !R.?Q       ?P.?Q <: ?P.?Q
------------------------------------
   ?P.?Q.!R <: !R.?P.?Q
*)
186 187
Definition iProto_le_pre {Σ V}
    (rec : iProto Σ V  iProto Σ V iProp Σ) (p1 p2 : iProto Σ V) : iProp Σ :=
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
188 189 190 191 192 193 194
  (p1  proto_end  p2  proto_end) 
   a1 a2 pc1 pc2,
    p1  proto_message a1 pc1 
    p2  proto_message a2 pc2 
    match a1, a2 with
    | Receive, Receive =>
        v p1', pc1 v (proto_eq_next p1') -
195
           p2',  rec p1' p2'  pc2 v (proto_eq_next p2')
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
196 197
    | Send, Send =>
        v p2', pc2 v (proto_eq_next p2') -
198
           p1',  rec p1' p2'  pc1 v (proto_eq_next p1')
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
199 200 201
    | Receive, Send =>
        v1 v2 p1' p2',
         pc1 v1 (proto_eq_next p1') - pc2 v2 (proto_eq_next p2') -
202
           pc1' pc2' pt,
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
203 204 205 206 207 208
            rec p1' (proto_message Send pc1') 
            rec (proto_message Receive pc2') p2' 
           pc1' v2 (proto_eq_next pt) 
           pc2' v1 (proto_eq_next pt)
    | Send, Receive => False
    end.
209
Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V  iProto Σ V  iProp Σ) :
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
210 211 212
  NonExpansive2 (iProto_le_pre rec).
Proof. solve_proper. Qed.

213 214 215
Program Definition iProto_le_pre' {Σ V}
    (rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) :
    iProto Σ V -n> iProto Σ V -n> iPropO Σ :=
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
216
  λne p1 p2, iProto_le_pre (λ p1' p2', rec p1' p2') p1 p2.
217
Solve Obligations with solve_proper.
218
Local Instance iProto_le_pre_contractive {Σ V} : Contractive (@iProto_le_pre' Σ V).
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
219 220 221 222
Proof.
  intros n rec1 rec2 Hrec p1 p2. rewrite /iProto_le_pre' /iProto_le_pre /=.
  by repeat (f_contractive || f_equiv).
Qed.
223 224 225
Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ := fixpoint iProto_le_pre' p1 p2.
Arguments iProto_le {_ _} _%proto _%proto.
Instance: Params (@iProto_le) 2 := {}.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
226

227 228
Fixpoint iProto_interp_aux {Σ V} (n : nat)
    (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
229 230 231 232 233 234 235 236 237 238 239
  match n with
  | 0 =>  p,
      vsl = []  
      vsr = []  
     iProto_le p pl 
     iProto_le (iProto_dual p) pr
  | S n =>
     ( vl vsl' pc p2',
        vsl = vl :: vsl'  
       iProto_le (proto_message Receive pc) pr 
       pc vl (proto_eq_next p2') 
240
       iProto_interp_aux n vsl' vsr pl p2') 
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
241 242 243 244
     ( vr vsr' pc p1',
        vsr = vr :: vsr'  
       iProto_le (proto_message Receive pc) pl 
       pc vr (proto_eq_next p1') 
245
       iProto_interp_aux n vsl vsr' p1' pr)
246
  end.
247 248 249
Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
  iProto_interp_aux (length vsl + length vsr) vsl vsr pl pr.
Arguments iProto_interp {_ _} _ _ _%proto _%proto : simpl nomatch.
Robbert Krebbers's avatar
Robbert Krebbers committed
250

251
Record proto_name := ProtName { proto_l_name : gname; proto_r_name : gname }.
Robbert Krebbers's avatar
Robbert Krebbers committed
252

253 254 255 256
Inductive side := Left | Right.
Instance side_inhabited : Inhabited side := populate Left.
Definition side_elim {A} (s : side) (l r : A) : A :=
  match s with Left => l | Right => r end.
Robbert Krebbers's avatar
Robbert Krebbers committed
257

258 259 260 261 262 263 264 265 266 267 268 269 270 271 272
Definition iProto_unfold {Σ V} (p : iProto Σ V) : proto V (iPrePropO Σ) (iPrePropO Σ) :=
  proto_map id iProp_fold iProp_unfold p.
Definition iProto_own_frag `{!protoG Σ V} (γ : proto_name) (s : side)
    (p : iProto Σ V) : iProp Σ :=
  own (side_elim s proto_l_name proto_r_name γ) (E (Next (iProto_unfold p))).
Definition iProto_own_auth `{!protoG Σ V} (γ : proto_name) (s : side)
    (p : iProto Σ V) : iProp Σ :=
  own (side_elim s proto_l_name proto_r_name γ) (E (Next (iProto_unfold p))).

Definition iProto_ctx `{protoG Σ V}
    (γ : proto_name) (vsl vsr : list V) : iProp Σ :=
   pl pr,
    iProto_own_auth γ Left pl 
    iProto_own_auth γ Right pr 
     iProto_interp vsl vsr pl pr.
Robbert Krebbers's avatar
Robbert Krebbers committed
273

Robbert Krebbers's avatar
Robbert Krebbers committed
274
(** * The connective for ownership of channel ends *)
275 276 277 278 279
Definition iProto_own `{!protoG Σ V}
    (γ : proto_name) (s : side) (p : iProto Σ V) : iProp Σ :=
   p', iProto_le p' p  iProto_own_frag γ s p'.
Arguments iProto_own {_ _ _} _ _%proto.
Instance: Params (@iProto_own) 3 := {}.
Robbert Krebbers's avatar
Robbert Krebbers committed
280

Robbert Krebbers's avatar
Robbert Krebbers committed
281
(** * Proofs *)
Robbert Krebbers's avatar
Robbert Krebbers committed
282
Section proto.
283 284
  Context `{!protoG Σ V}.
  Implicit Types p pl pr : iProto Σ V.
Robbert Krebbers's avatar
Robbert Krebbers committed
285 286
  Implicit Types TT : tele.

Robbert Krebbers's avatar
Robbert Krebbers committed
287
  (** ** Non-expansiveness of operators *)
Robbert Krebbers's avatar
Robbert Krebbers committed
288
  Lemma iProto_message_contractive {TT} a
289
      (pc1 pc2 : TT  V * iProp Σ * iProto Σ V) n :
Robbert Krebbers's avatar
Robbert Krebbers committed
290 291 292 293 294 295 296 297 298 299
    (.. 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.
300
  Lemma iProto_message_ne {TT} a (pc1 pc2 : TT  V * iProp Σ * iProto Σ V) n :
Robbert Krebbers's avatar
Robbert Krebbers committed
301 302 303 304 305 306 307 308
    (.. 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.
309
  Lemma iProto_message_proper {TT} a (pc1 pc2 : TT  V * iProp Σ * iProto Σ V) :
Robbert Krebbers's avatar
Robbert Krebbers committed
310 311 312 313 314 315 316 317
    (.. 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
318

Robbert Krebbers's avatar
Robbert Krebbers committed
319
  (** ** Dual *)
320
  Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
Robbert Krebbers's avatar
Robbert Krebbers committed
321
  Proof. solve_proper. Qed.
322
  Global Instance iProto_dual_proper : Proper (() ==> ()) (@iProto_dual Σ V).
Robbert Krebbers's avatar
Robbert Krebbers committed
323
  Proof. apply (ne_proper _). Qed.
324
  Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ V d).
325
  Proof. solve_proper. Qed.
326
  Global Instance iProto_dual_if_proper d : Proper (() ==> ()) (@iProto_dual_if Σ V d).
327
  Proof. apply (ne_proper _). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
328

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

335
  Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END  END%proto.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
  Proof. by rewrite iProto_end_eq /iProto_dual proto_map_end. Qed.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
337

338
  Lemma iProto_dual_message {TT} a (pc : TT  V * iProp Σ * iProto Σ V) :
Robbert Krebbers's avatar
Robbert Krebbers committed
339 340 341 342 343 344 345
    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.

Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
346
  (** Helpers for duals *)
347
  Global Instance proto_eq_next_ne : NonExpansive (proto_eq_next (Σ:=Σ) (V:=V)).
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
348
  Proof. solve_proper. Qed.
349 350
  Global Instance proto_eq_next_proper :
    Proper (() ==> ()) (proto_eq_next (Σ:=Σ) (V:=V)).
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
351 352 353
  Proof. solve_proper. Qed.

  Lemma proto_eq_next_dual p :
354 355
    ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid
      (proto_eq_next (iProto_dual p))  proto_eq_next p.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371
  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.

  Lemma proto_eq_next_dual' p :
    ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid (proto_eq_next p) 
    proto_eq_next (iProto_dual p).
  Proof.
    rewrite -(proto_eq_next_dual (iProto_dual p))=> lp /=.
    by rewrite involutive.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
372
  (** ** Append *)
373
  Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
Robbert Krebbers's avatar
Robbert Krebbers committed
374
  Proof. apply _. Qed.
375
  Global Instance iProto_app_proper : Proper (() ==> () ==> ()) (@iProto_app Σ V).
Robbert Krebbers's avatar
Robbert Krebbers committed
376 377
  Proof. apply (ne_proper_2 _). Qed.

378
  Lemma iProto_app_message {TT} a (pc : TT  V * iProp Σ * iProto Σ V) p2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
379 380
    (iProto_message a pc <++> p2)%proto
     iProto_message a (prod_map id (flip iProto_app p2)  pc).
Robbert Krebbers's avatar
Robbert Krebbers committed
381 382 383 384 385
  Proof.
    rewrite /iProto_app iProto_message_eq /iProto_message_def proto_app_message.
    by f_equiv=> v f /=.
  Qed.

386
  Global Instance iProto_app_end_l : LeftId () END%proto (@iProto_app Σ V).
Robbert Krebbers's avatar
Robbert Krebbers committed
387
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
388 389
    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_l.
  Qed.
390
  Global Instance iProto_app_end_r : RightId () END%proto (@iProto_app Σ V).
Robbert Krebbers's avatar
Robbert Krebbers committed
391
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
392
    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
393
  Qed.
394
  Global Instance iProto_app_assoc : Assoc () (@iProto_app Σ V).
Robbert Krebbers's avatar
Robbert Krebbers committed
395 396 397 398 399 400
  Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.

  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.

401
  (** ** Protocol entailment **)
402
  Global Instance iProto_le_ne : NonExpansive2 (@iProto_le Σ V).
403
  Proof. solve_proper. Qed.
404
  Global Instance iProto_le_proper : Proper (() ==> () ==> ()) (@iProto_le Σ V).
405 406
  Proof. solve_proper. Qed.

Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
407 408
  Lemma iProto_le_unfold p1 p2 : iProto_le p1 p2  iProto_le_pre iProto_le p1 p2.
  Proof. apply: (fixpoint_unfold iProto_le_pre'). Qed.
409

Robbert Krebbers's avatar
Robbert Krebbers committed
410
  Lemma iProto_le_refl p :  iProto_le p p.
411 412 413
  Proof.
    iLöb as "IH" forall (p). destruct (proto_case p) as [->|([]&pc&->)].
    - rewrite iProto_le_unfold. iLeft; by auto.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
414
    - rewrite iProto_le_unfold. iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
415
      iIntros (v p') "Hpc". iExists p'. iIntros "{$Hpc} !> !>". iApply "IH".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
416
    - rewrite iProto_le_unfold. iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
417
      iIntros (v p') "Hpc". iExists p'. iIntros "{$Hpc} !> !>". iApply "IH".
418 419 420 421 422
  Qed.

  Lemma iProto_le_end_inv p : iProto_le p proto_end - p  proto_end.
  Proof.
    rewrite iProto_le_unfold. iIntros "[[Hp _]|H] //".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
423 424
    iDestruct "H" as (a1 a2 pc1 pc2) "(_ & Heq & _)".
    by iDestruct (proto_end_message_equivI with "Heq") as %[].
425 426 427
  Qed.

  Lemma iProto_le_send_inv p1 pc2 :
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
428 429 430 431 432
    iProto_le p1 (proto_message Send pc2) -  a1 pc1,
      p1  proto_message a1 pc1 
      match a1 with
      | Send =>
          v p2', pc2 v (proto_eq_next p2') -
433
             p1',  iProto_le p1' p2'  pc1 v (proto_eq_next p1')
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
434 435 436
      | Receive =>
          v1 v2 p1' p2',
           pc1 v1 (proto_eq_next p1') - pc2 v2 (proto_eq_next p2') -
437
             pc1' pc2' pt,
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
438 439 440 441 442 443 444 445 446 447 448 449 450
              iProto_le p1' (proto_message Send pc1') 
              iProto_le (proto_message Receive pc2') p2' 
             pc1' v2 (proto_eq_next pt) 
             pc2' v1 (proto_eq_next pt)
      end.
  Proof.
    rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
    { by iDestruct (proto_message_end_equivI with "Heq") as %[]. }
    iDestruct "H" as (a1 a2 pc1 pc2') "(Hp1 & Hp2 & H)".
    iDestruct (proto_message_equivI with "Hp2") as (<-) "{Hp2} #Hpc".
    iExists _, _; iSplit; [done|]. destruct a1. 
    - iIntros (v p2'). by iRewrite ("Hpc" $! v (proto_eq_next p2')).
    - iIntros (v1 v2 p1' p2'). by iRewrite ("Hpc" $! v2 (proto_eq_next p2')).
451 452 453 454 455
  Qed.

  Lemma iProto_le_recv_inv p1 pc2 :
    iProto_le p1 (proto_message Receive pc2) -  pc1,
      p1  proto_message Receive pc1 
456
       v p1', pc1 v (proto_eq_next p1') -
457
          p2',  iProto_le p1' p2'  pc2 v (proto_eq_next p2').
458
  Proof.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
459 460 461 462 463
    rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
    { by iDestruct (proto_message_end_equivI with "Heq") as %[]. }
    iDestruct "H" as (a1 a2 pc1 pc2') "(Hp1 & Hp2 & H)".
    iDestruct (proto_message_equivI with "Hp2") as (<-) "{Hp2} #Hpc2".
    destruct a1; [done|]. iExists _; iSplit; [done|].
464
    iIntros (v p1') "Hpc". iDestruct ("H" with "Hpc") as (p2') ">[Hle Hpc]".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
465
    iExists p2'. iFrame "Hle". by iRewrite ("Hpc2" $! v (proto_eq_next p2')).
466 467 468 469 470 471 472
  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&->)].
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
473 474 475 476 477 478 479
    - by iRewrite (iProto_le_end_inv with "H2") in "H1".
    - iDestruct (iProto_le_send_inv with "H2") as (a2 pc2) "[Hp2 H2]".
      iRewrite "Hp2" in "H1"; clear p2. destruct a2.
      + iDestruct (iProto_le_send_inv with "H1") as (a1 pc1) "[Hp1 H1]".
        iRewrite "Hp1"; clear p1. rewrite iProto_le_unfold; iRight.
        iExists _, _, _, _; do 2 (iSplit; [done|]). destruct a1.
        * iIntros (v p3') "Hpc".
480 481
          iMod ("H2" with "Hpc") as (p2') "[Hle Hpc]".
          iMod ("H1" with "Hpc") as (p1') "[Hle' Hpc]".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
482 483
          iExists p1'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle'").
        * iIntros (v1 v3 p1' p3') "Hpc1 Hpc3".
484 485 486 487
          iMod ("H2" with "Hpc3") as (p2') "[Hle Hpc2]".
          iMod ("H1" with "Hpc1 Hpc2") as (pc1' pc2' pt) "(Hp1' & Hp2' & Hpc)".
          iModIntro. iExists pc1', pc2', pt. iFrame "Hp1' Hpc".
          by iApply ("IH" with "Hp2'").
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
488 489 490 491
      + iDestruct (iProto_le_recv_inv with "H1") as (pc1) "[Hp1 H1]".
        iRewrite "Hp1"; clear p1. rewrite iProto_le_unfold; iRight.
        iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
        iIntros (v1 v3 p1' p3') "Hpc1 Hpc3".
492 493 494 495
        iMod ("H1" with "Hpc1") as (p2') "[Hle Hpc2]".
        iMod ("H2" with "Hpc2 Hpc3") as (pc2' pc3' pt) "(Hp2' & Hp3' & Hpc)".
        iModIntro. iExists pc2', pc3', pt. iFrame "Hp3' Hpc".
        by iApply ("IH" with "Hle").
496 497 498
    - 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]".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
499 500
      iRewrite "Hp1". rewrite iProto_le_unfold. iRight.
      iExists _, _, _, _; do 2 (iSplit; [done|]).
501
      iIntros (v p1') "Hpc".
502 503 504
      iMod ("H2" with "Hpc") as (p2') "[Hle Hpc]".
      iMod ("H3" with "Hpc") as (p3') "[Hle' Hpc]".
      iModIntro. iExists p3'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle").
505 506
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
507
  Lemma iProto_le_send {TT1 TT2} (pc1 : TT1  V * iProp Σ * iProto Σ V)
508
      (pc2 : TT2  V * iProp Σ * iProto Σ V) :
509
    (.. x2 : TT2,  (pc2 x2).1.2 -  .. x1 : TT1,
510
      (pc1 x1).1.1 = (pc2 x2).1.1 
511 512
       (pc1 x1).1.2 
       iProto_le (pc1 x1).2 (pc2 x2).2) -
513 514
    iProto_le (iProto_message Send pc1) (iProto_message Send pc2).
  Proof.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
515 516
    iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
    iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
517
    iIntros (v p2') "/=". iDestruct 1 as (x2 ->) "[Hpc #Heq]".
518 519
    iMod ("H" with "Hpc") as (x1 ?) "[Hpc Hle]".
    iModIntro. iExists (pc1 x1).2. iSplitL "Hle".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
520
    { iIntros "!>". by iRewrite "Heq". }
521
    iExists x1. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
522 523
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
524
  Lemma iProto_le_recv {TT1 TT2} (pc1 : TT1  V * iProp Σ * iProto Σ V)
525
      (pc2 : TT2  V * iProp Σ * iProto Σ V) :
526
    (.. x1 : TT1,  (pc1 x1).1.2 -  .. x2 : TT2,
527
      (pc1 x1).1.1 = (pc2 x2).1.1 
528 529
       (pc2 x2).1.2 
       iProto_le (pc1 x1).2 (pc2 x2).2) -
530 531
    iProto_le (iProto_message Receive pc1) (iProto_message Receive pc2).
  Proof.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
532 533
    iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
    iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
534
    iIntros (v p1') "/=". iDestruct 1 as (x1 ->) "[Hpc #Heq]".
535 536 537
    iMod ("H" with "Hpc") as (x2 ?) "[Hpc Hle]". iExists (pc2 x2).2. iSplitL "Hle".
    { iIntros "!> !>". by iRewrite "Heq". }
    iModIntro. iExists x2. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
538 539
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
540 541 542 543
  Lemma iProto_le_swap {TT1 TT2} (pc1 : TT1  V * iProp Σ * iProto Σ V)
      (pc2 : TT2  V * iProp Σ * iProto Σ V) :
    (.. (x1 : TT1) (x2 : TT2),
       (pc1 x1).1.2 -  (pc2 x2).1.2 -
544
        {TT3 TT4} (pc3 : TT3  V * iProp Σ * iProto Σ V)
Robbert Krebbers's avatar
Robbert Krebbers committed
545 546 547 548 549 550 551 552
          (pc4 : TT4  V * iProp Σ * iProto Σ V), .. (x3 : TT3) (x4 : TT4),
        (pc1 x1).1.1 = (pc4 x4).1.1 
        (pc2 x2).1.1 = (pc3 x3).1.1 
         iProto_le (pc1 x1).2 (iProto_message Send pc3) 
         iProto_le (iProto_message Receive pc4) (pc2 x2).2 
         (pc3 x3).1.2   (pc4 x4).1.2 
         ((pc3 x3).2  (pc4 x4).2)) -
    iProto_le (iProto_message Receive pc1) (iProto_message Send pc2).
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
553
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
    iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
555
    iRight. iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
556 557
    iIntros (v1 v2 p1 p2).
    iDestruct 1 as (x1 ->) "[Hpc1 #Heq1]"; iDestruct 1 as (x2 ->) "[Hpc2 #Heq2]".
558
    iMod ("H" with "Hpc1 Hpc2")
Robbert Krebbers's avatar
Robbert Krebbers committed
559
      as (TT3 TT4 pc3 pc4 x3 x4 ??) "(H1 & H2 & Hpc1 & Hpc2 & #H)".
560
    iModIntro. iExists _, _, (pc3 x3).2. iSplitL "H1"; [iNext; by iRewrite "Heq1"|].
Robbert Krebbers's avatar
Robbert Krebbers committed
561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576
    iSplitL "H2"; [iNext; by iRewrite "Heq2"|]. simpl.
    iSplitL "Hpc1"; [by auto|]. iExists x4. rewrite !bi.later_equivI. auto.
  Qed.

  Lemma iProto_le_swap_simple {TT1 TT2} (v1 : TT1  V) (v2 : TT2  V)
      (P1 : TT1  iProp Σ) (P2 : TT2  iProp Σ) (p : TT1  TT2  iProto Σ V) :
     iProto_le
        (iProto_message Receive (λ x1,
          (v1 x1, P1 x1, iProto_message Send (λ x2, (v2 x2, P2 x2, p x1 x2)))))
        (iProto_message Send (λ x2,
          (v2 x2, P2 x2, iProto_message Receive (λ x1, (v1 x1, P1 x1, p x1 x2))))).
  Proof.
    iApply iProto_le_swap. iIntros (x1 x2) "/= HP1 HP2".
    iExists TT2, TT1, (λ x2, (v2 x2, P2 x2, p x1 x2)),
      (λ x1, (v1 x1, P1 x1, p x1 x2)), x2, x1; simpl.
    do 2 (iSplit; [done|]). do 2 (iSplitR; [iApply iProto_le_refl|]). by iFrame.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
577 578
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
579
  Lemma iProto_le_dual p1 p2 :
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
580 581 582 583 584 585 586 587 588 589
    iProto_le p2 p1 - iProto_le (iProto_dual p1) (iProto_dual p2).
  Proof.
    iIntros "H". iLöb as "IH" forall (p1 p2).
    destruct (proto_case p1) as [->|([]&pc1&->)].
    - iRewrite (iProto_le_end_inv with "H"). iApply iProto_le_refl.
    - iDestruct (iProto_le_send_inv with "H") as (a2 pc2) "[Hp2 H]".
      iRewrite "Hp2"; clear p2. iEval (rewrite /iProto_dual !proto_map_message /=).
      rewrite iProto_le_unfold; iRight.
      iExists _, _, _, _; do 2 (iSplit; [done|]); simpl. destruct a2; simpl.
      + iIntros (v p1') "Hpc". rewrite proto_eq_next_dual'.
590
        iMod ("H" with "Hpc") as (p2'') "[H Hpc]".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
591 592 593
        iDestruct ("IH" with "H") as "H". rewrite involutive.
        iExists (iProto_dual p2''). rewrite proto_eq_next_dual. iFrame.
      + iIntros (v1 v2 p1' p2') "Hpc1 Hpc2". rewrite !proto_eq_next_dual'.
594
        iMod ("H" with "Hpc2 Hpc1") as (pc1' pc2' pt) "(H1 & H2 & Hpc1 & Hpc2)".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
595 596 597 598 599 600 601 602
        iDestruct ("IH" with "H1") as "H1". iDestruct ("IH" with "H2") as "H2 {IH}".
        rewrite !involutive /iProto_dual !proto_map_message.
        iExists _, _, (iProto_dual pt). iFrame. rewrite /= proto_eq_next_dual. iFrame.
    - iDestruct (iProto_le_recv_inv with "H") as (pc2) "[Hp2 H]".
      iRewrite "Hp2"; clear p2. iEval (rewrite /iProto_dual !proto_map_message /=).
      rewrite iProto_le_unfold; iRight.
      iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
      iIntros (v p2') "Hpc". rewrite proto_eq_next_dual'.
603
      iMod ("H" with "Hpc") as (p2'') "[H Hpc]".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
604 605 606 607
      iDestruct ("IH" with "H") as "H". rewrite involutive.
      iExists (iProto_dual p2''). rewrite proto_eq_next_dual. iFrame.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
608
  (** ** Lemmas about the auxiliary definitions and invariants *)
609 610
  Global Instance iProto_interp_aux_ne n vsl vsr :
    NonExpansive2 (iProto_interp_aux (Σ:=Σ) (V:=V) n vsl vsr).
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
611
  Proof. revert vsl vsr. induction n; solve_proper. Qed.
612 613
  Global Instance iProto_interp_aux_proper n vsl vsr :
    Proper (() ==> () ==> ()) (iProto_interp_aux (Σ:=Σ) (V:=V) n vsl vsr).
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
614
  Proof. apply (ne_proper_2 _). Qed.
615 616
  Global Instance iProto_interp_ne vsl vsr :
    NonExpansive2 (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
617
  Proof. solve_proper. Qed.
618 619
  Global Instance iProto_interp_proper vsl vsr :
    Proper (() ==> () ==> ()) (iProto_interp (Σ:=Σ) (V:=V) vsl vsr).
Robbert Krebbers's avatar
Robbert Krebbers committed
620 621
  Proof. apply (ne_proper_2 _). Qed.

622
  Global Instance iProto_unfold_ne : NonExpansive (iProto_unfold (Σ:=Σ) (V:=V)).
Robbert Krebbers's avatar
Robbert Krebbers committed
623
  Proof. solve_proper. Qed.
624
  Global Instance iProto_own_frag_ne γ s : NonExpansive (iProto_own_frag γ s).
Robbert Krebbers's avatar
Robbert Krebbers committed
625 626
  Proof. solve_proper. Qed.

627 628
  Lemma iProto_own_auth_agree γ s p p' :
    iProto_own_auth γ s p - iProto_own_frag γ s p' -  (p  p').
Robbert Krebbers's avatar
Robbert Krebbers committed
629
  Proof.
630 631 632 633
    iIntros "H● H◯". iDestruct (own_valid_2 with "H● H◯") as "H✓".
    iDestruct (excl_auth_agreeI with "H✓") as "H✓".
    iDestruct (bi.later_eq_1 with "H✓") as "H✓"; iNext.
    rewrite /iProto_unfold. assert ( p,
Robbert Krebbers's avatar
Robbert Krebbers committed
634 635 636
      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. }
637
    rewrite -{2}(help p). iRewrite "H✓". by rewrite help.
Robbert Krebbers's avatar
Robbert Krebbers committed
638 639
  Qed.

640 641 642
  Lemma iProto_own_auth_update γ s p p' p'' :
    iProto_own_auth γ s p - iProto_own_frag γ s p' ==
    iProto_own_auth γ s p''  iProto_own_frag γ s p''.
Robbert Krebbers's avatar
Robbert Krebbers committed
643
  Proof.
644 645
    iIntros "H● H◯". iDestruct (own_update_2 with "H● H◯") as "H".
    { eapply (excl_auth_update _ _ (Next (iProto_unfold p''))). }
Robbert Krebbers's avatar
Robbert Krebbers committed
646 647 648
    by rewrite own_op.
  Qed.

Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
649 650 651 652 653 654 655 656 657
  (* TODO: Move somewhere else *)
  Lemma false_disj_cong (P Q Q' : iProp Σ) :
    (P  False)  (Q  Q')  (P  Q  Q').
  Proof. intros HP ->. apply (anti_symm _). by rewrite HP left_id. auto. Qed.

  Lemma pure_sep_cong (φ1 φ2 : Prop) (P1 P2 : iProp Σ) :
    (φ1  φ2)  (φ1  φ2  P1  P2)  (⌜φ1  P1)  (⌜φ2  P2).
  Proof. intros -> HP. iSplit; iDestruct 1 as (Hϕ) "H"; rewrite HP; auto. Qed.

658 659
  Lemma iProto_interp_unfold vsl vsr pl pr :
    iProto_interp vsl vsr pl pr 
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
660 661 662 663 664 665 666 667 668
      ( p,
         vsl = []  
         vsr = []  
        iProto_le p pl 
        iProto_le (iProto_dual p) pr) 
      ( vl vsl' pc pr',
         vsl = vl :: vsl'  
        iProto_le (proto_message Receive pc) pr 
        pc vl (proto_eq_next pr') 
669
        iProto_interp vsl' vsr pl pr') 
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
670 671 672 673
      ( vr vsr' pc pl',
         vsr = vr :: vsr'  
        iProto_le (proto_message Receive pc) pl 
        pc vr (proto_eq_next pl') 
674
        iProto_interp vsl vsr' pl' pr).
675
  Proof.
676
    rewrite {1}/iProto_interp. destruct vsl as [|vl vsl]; simpl.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
677 678 679 680 681 682 683 684 685 686 687 688 689
    - destruct vsr as [|vr vsr]; simpl.
      + iSplit; first by auto.
        iDestruct 1 as "[H | [H | H]]"; first by auto.
        * iDestruct "H" as (? ? ? ? [=]) "_".
        * iDestruct "H" as (? ? ? ? [=]) "_".
      + symmetry. apply false_disj_cong.
        { iDestruct 1 as (? _ [=]) "_". }
        repeat first [apply pure_sep_cong; intros; simplify_eq/= | f_equiv];
          by rewrite ?Nat.add_succ_r.
    - symmetry. apply false_disj_cong.
      { iDestruct 1 as (? [=]) "_". }
      repeat first [apply pure_sep_cong; intros; simplify_eq/= | f_equiv];
        by rewrite ?Nat.add_succ_r.
690 691
  Qed.

692
  Lemma iProto_interp_nil p :  iProto_interp [] [] p (iProto_dual p).
Robbert Krebbers's avatar
Robbert Krebbers committed
693
  Proof.
694
    rewrite iProto_interp_unfold. iLeft. iExists p. do 2 (iSplit; [done|]).
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
695
    iSplitL; iApply iProto_le_refl.
Robbert Krebbers's avatar
Robbert Krebbers committed
696 697
  Qed.

698 699
  Lemma iProto_interp_flip vsl vsr pl pr :
    iProto_interp vsl vsr pl pr - iProto_interp vsr vsl pr pl.
Robbert Krebbers's avatar
Robbert Krebbers committed
700
  Proof.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
701 702
    remember (length vsl + length vsr) as n eqn:Hn.
    iInduction (lt_wf n) as [n _] "IH" forall (vsl vsr pl pr Hn); subst.
703
    rewrite !iProto_interp_unfold. iIntros "[H|[H|H]]".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
704 705
    - iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
      iLeft. iExists (iProto_dual p). rewrite involutive. iFrame; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
706
    - iDestruct "H" as (vl vsl' pc' pr' ->) "(Hpr & Hpc' & H)".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
707
      iRight; iRight. iExists vl, vsl', pc', pr'. iSplit; [done|]; iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
708 709
      iApply ("IH" with "[%] [//] H"); simpl; lia.
    - iDestruct "H" as (vr vsr' pc' pl' ->) "(Hpl & Hpc' & H)".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
710
      iRight; iLeft. iExists vr, vsr', pc', pl'. iSplit; [done|]; iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
711
      iApply ("IH" with "[%] [//] H"); simpl; lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
712 713
  Qed.

714 715
  Lemma iProto_interp_le_l vsl vsr pl pl' pr :
    iProto_interp vsl vsr pl pr - iProto_le pl pl' - iProto_interp vsl vsr pl' pr.
Robbert Krebbers's avatar
Robbert Krebbers committed
716
  Proof.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
717 718
    remember (length vsl + length vsr) as n eqn:Hn.
    iInduction (lt_wf n) as [n _] "IH" forall (vsl vsr pl pr Hn); subst.
719
    rewrite !iProto_interp_unfold. iIntros "[H|[H|H]] Hle".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
720 721 722
    - iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
      iLeft. iExists p. do 2 (iSplit; [done|]). iFrame "Hp'".
      by iApply (iProto_le_trans with "Hp").
Robbert Krebbers's avatar
Robbert Krebbers committed
723
    - iDestruct "H" as (vl vsl' pc' pr' ->) "(Hpr & Hpc' & H)".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
724
      iRight; iLeft. iExists vl, vsl', pc', pr'. iSplit; [done|]; iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
725 726
      iApply ("IH" with "[%] [//] H Hle"); simpl; lia.
    - iClear "IH". iDestruct "H" as (vr vsr' pc' pl'' ->) "(Hpl & Hpc' & H)".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
727 728 729
      iRight; iRight. iExists vr, vsr', pc', pl''. iSplit; [done|]; iFrame.
      by iApply (iProto_le_trans with "Hpl").
  Qed.
730 731
  Lemma iProto_interp_le_r vsl vsr pl pr pr' :
    iProto_interp vsl vsr pl pr - iProto_le pr pr' - iProto_interp vsl vsr pl pr'.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
732
  Proof.
733 734
    iIntros "H Hle". iApply iProto_interp_flip.
    iApply (iProto_interp_le_l with "[H] Hle"). by iApply iProto_interp_flip.
Robbert Krebbers's avatar
Robbert Krebbers committed
735 736
  Qed.

737 738
  Lemma iProto_interp_send vl pcl vsl vsr pl pr pl' :
    iProto_interp vsl vsr pl pr -
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
739 740
    iProto_le pl (proto_message Send pcl) -
    pcl vl (proto_eq_next pl') -
741
    ^(length vsr) iProto_interp (vsl ++ [vl]) vsr pl' pr.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
742
  Proof.
743
    iIntros "H Hle". iDestruct (iProto_interp_le_l with "H Hle") as "H".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
744 745
    clear pl. iIntros "Hpcl". remember (length vsl + length vsr) as n eqn:Hn.
    iInduction (lt_wf n) as [n _] "IH" forall (pcl vsl vsr pr pl' Hn); subst.
746
    rewrite {1}iProto_interp_unfold. iDestruct "H" as "[H|[H|H]]".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
747
    - iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
748
      iDestruct (iProto_le_dual with "Hp") as "Hp".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
749 750
      iDestruct (iProto_le_trans with "Hp Hp'") as "Hp".
      rewrite /iProto_dual proto_map_message /=.
751
      iApply iProto_interp_unfold. iRight; iLeft.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
752
      iExists vl, [], _, (iProto_dual pl'). iSplit; [done|]. iFrame "Hp"; simpl.
753
      rewrite proto_eq_next_dual. iFrame "Hpcl". iApply iProto_interp_nil.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
754 755
    - iDestruct "H" as (vl' vsl' pc' pr' ->) "(Hpr & Hpc' & H)".
      iDestruct ("IH" with "[%] [//] H Hpcl") as "H"; [simpl; lia|].
756 757
      iNext. iApply (iProto_interp_le_r with "[-Hpr] Hpr"); clear pr.
      iApply iProto_interp_unfold. iRight; iLeft.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
758 759
      iExists vl', (vsl' ++ [vl]), pc', pr'. iFrame.
      iSplit; [done|]. iApply iProto_le_refl.
Robbert Krebbers's avatar
Robbert Krebbers committed
760
    - iDestruct "H" as (vr' vsr' pc' pl'' ->) "(Hle & Hpcl' & H) /=".
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
761 762 763
      iDestruct (iProto_le_send_inv with "Hle") as (a pcl') "[Hpc Hle]".
      iDestruct (proto_message_equivI with "Hpc") as (<-) "Hpc".
      iRewrite ("Hpc" $! vr' (proto_eq_next pl'')) in "Hpcl'"; clear pc'.
764
      iMod ("Hle" with "Hpcl' Hpcl")
Robbert Krebbers's avatar
Robbert Krebbers committed
765
        as (pc1 pc2 pt) "(Hpl'' & Hpl' & Hpc1 & Hpc2)".
766
      iNext. iDestruct (iProto_interp_le_l with "H Hpl''") as "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
767
      iDestruct ("IH" with "[%] [//] H Hpc1") as "H"; [simpl; lia|..].
768
      iNext. iApply iProto_interp_unfold. iRight; iRight.
Robbert Krebbers's avatar
Robbert Krebbers committed
769 770
      iExists vr', vsr', _, pt. iSplit; [done|]. by iFrame.
  Qed.
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
771

772 773
  Lemma iProto_interp_recv vl vsl vsr pl pr pcr :
    iProto_interp (vl :: vsl) vsr pl pr -
Robbert Krebbers's avatar
WIP.  
Robbert Krebbers committed
774
    iProto_le pr (proto_message Receive pcr) -