Guarantees by Construction (Mechanization)

Jules Jacobs

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
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
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
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
From dlfactris.session_logic Require Export tele_imp.
From iris.proofmode Require Import coq_tactics reduction spec_patterns.
Import TImp TImp.notations.

(** Tactics for proving contractiveness of protocols *)
Ltac f_dist_le :=
  match goal with
  | H : _ {?n} _ |- _ {?n'} _ => apply (dist_le n); [apply H|lia]
  end.

Ltac solve_prot_contractive :=
  solve_proper_core ltac:(fun _ =>
    first [f_contractive; simpl in * | f_equiv | f_dist_le]).

(** Let [auto] use reflexivity of subprot *)
Global Hint Extern 0 (environments.envs_entails _ (?x  ?y)) =>
  first [is_evar x; fail 1 | is_evar y; fail 1|iApply subprot_refl] : core.

(** * Normalization of protocols *)
Class ActionDualIf (d : bool) (a1 a2 : action) :=
  { dual_action_if : a2 = if d then action_dual a1 else a1 }.
Global Hint Mode ActionDualIf ! ! - : typeclass_instances.

Global Instance action_dual_if_false a : ActionDualIf false a a.
Proof. by constructor. Qed.
Global Instance action_dual_if_true_send : ActionDualIf true ASend ARecv.
Proof. by constructor. Qed.
Global Instance action_dual_if_true_recv : ActionDualIf true ARecv ASend.
Proof. by constructor. Qed.

Class ProtNormalize (d : bool) (p q : aMiniProt) :=
  { prot_normalize :  (if d then dual p else p)  q }.
Global Hint Mode ProtNormalize ! ! - : typeclass_instances.

Notation ProtUnfold p1 p2 :=
  (∀ d q, ProtNormalize d p2 q  ProtNormalize d p1 q).

Class MsgNormalize (d : bool) (a : action) (m1 m2 : msg) :=
  { msg_normalize :
      ProtNormalize d (<a> m1) (<(if d then action_dual a else a)> m2) }.
Global Hint Mode MsgNormalize ! ! ! - : typeclass_instances.

Class MsgTele {TT : tele} (m : msg)
    (tv : TT -t> val) (tP : TT -t> aProp) (tp : TT -t> aMiniProt) :=
  { msg_tele :
     m  (∃.. x, MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x)%msg }.
Global Hint Mode MsgTele - ! - - - : typeclass_instances.

Section classes.
  Implicit Types TT : tele.
  Implicit Types p : aMiniProt.
  Implicit Types m : msg.
  Implicit Types P : aProp.

  (** The instances below make it possible to use the tactics [iIntros],
  [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [subprot] goals. *)
  Global Instance from_wand_end_recv P :
    TCIf (TCEq P emp%I) False TCTrue 
    FromWand (END? {{ P }}  END?) P (END?  END?) | 10.
  Proof. intros _. rewrite /FromWand. iApply subprot_end_elim_l. Qed.
  Global Instance from_wand_end_send P :
    TCIf (TCEq P emp%I) False TCTrue 
    FromWand (END!  END! {{ P }}) P (END!  END!) | 11.
  Proof. intros _. rewrite /FromWand. iApply subprot_end_elim_r. Qed.

  Global Instance frame_end_recv q R P Q1 Q2 :
    Frame q R Q1 Q2 
    Frame q R (END? {{ P }}  END? {{ Q1 }}) (END? {{ P }}  END? {{ Q2 }}) | 10.
  Proof.
    rewrite /Frame /=. iIntros (HP) "[HR H]".
    iApply (subprot_trans with "H"). iApply subprot_end_elim_l.
    iIntros "HQ". iApply subprot_end_intro_r. iApply HP; iFrame.
  Qed.
  Global Instance frame_end_send q R P1 P2 Q :
    Frame q R P1 P2 
    Frame q R (END! {{ P1 }}  END! {{ Q }}) (END! {{ P2 }}  END! {{ Q }}) | 10.
  Proof.
    rewrite /Frame /=. iIntros (HP) "[HR H]".
    iApply (subprot_trans with "[HR] H"). iApply subprot_end_elim_r.
    iIntros "HQ". iApply subprot_end_intro_l. iApply HP; iFrame.
  Qed.
  Global Instance from_sep_end_recv P Q :
    FromSep (END? {{ P }}  END? {{ Q }}) Q (END? {{ P }}  END?) | 11.
  Proof. rewrite /FromSep. by iIntros "[$ H]". Qed.
  Global Instance from_sep_end_send P Q :
    FromSep (END! {{ P }}  END! {{ Q }}) P (END!  END! {{ Q }}) | 10.
  Proof. rewrite /FromSep. by iIntros "[$ H]". Qed.

  Global Instance from_forall_recv {A} (m1 : A  msg) m2 name :
    AsIdentName m1 name 
    FromForall (msg_prot ARecv (msg_exist m1)  (<?> m2))
                x, (<?> m1 x)  (<?> m2))%I name | 10.
  Proof. intros _. apply subprot_exist_elim_l. Qed.
  Global Instance rrom_forall_tele_recv {TT : tele} (m1 : TT  msg) m2 name :
    AsIdentName m1 name 
    FromForall (msg_prot ARecv (msg_texist m1)  (<?> m2))
                x, (<?> m1 x)  (<?> m2))%I name | 11.
  Proof. intros _. apply subprot_texist_elim_l. Qed.
  Global Instance from_forall_send {A} m1 (m2 : A  msg) name :
    AsIdentName m2 name 
    FromForall ((<!> m1)  msg_prot ASend (msg_exist m2))
                x, (<!> m1)  (<!> m2 x))%I name | 20.
  Proof. intros _. apply subprot_exist_elim_r. Qed.
  Global Instance from_forall_tele_send {TT : tele} m1 (m2 : TT  msg) name :
    AsIdentName m2 name 
    FromForall ((<!> m1)  msg_prot ASend (msg_texist m2))
                x, (<!> m1)  (<!> m2 x))%I name | 21.
  Proof. intros _. rewrite /FromForall. iApply subprot_texist_elim_r. Qed.

  Global Instance from_wand_recv m v P p :
    TCIf (TCEq P emp%I) False TCTrue 
    FromWand ((<?> MSG v {{ P }}; p)  (<?> m)) P ((<?> MSG v; p)  (<?> m)) | 10.
  Proof. intros _. apply subprot_payload_elim_l. Qed.
  Global Instance from_wand_send m v P p :
    TCIf (TCEq P emp%I) False TCTrue 
    FromWand ((<!> m)  (<!> MSG v {{ P }}; p)) P ((<!> m)  (<!> MSG v; p)) | 11.
  Proof. intros _. apply subprot_payload_elim_r. Qed.

  Global Instance from_exist_send {A} (m : A  msg) p :
    FromExist ((<! x> m x)  p)  a, (<!> m a)  p)%I | 10.
  Proof.
    rewrite /FromExist. iDestruct 1 as (x) "H".
    iApply (subprot_trans with "[] H"). iApply subprot_exist_intro_l.
  Qed.
  Global Instance from_exist_tele_send {TT : tele} (m : TT  msg) p :
    FromExist ((<!.. x> m x)  p)  a, (<!> m a)  p)%I | 11.
  Proof.
    rewrite /FromExist. iDestruct 1 as (x) "H".
    iApply (subprot_trans with "[] H"). iApply subprot_texist_intro_l.
  Qed.
  Global Instance from_exist_recv {A} (m : A  msg) p :
    FromExist (p  <? x> m x)  a, p  (<?> m a))%I | 20.
  Proof.
    rewrite /FromExist. iDestruct 1 as (x) "H".
    iApply (subprot_trans with "H"). iApply subprot_exist_intro_r.
  Qed.
  Global Instance from_exist_tele_recv {TT : tele} (m : TT  msg) p :
    FromExist (p  <?.. x> m x)  a, p  (<?> m a))%I | 21.
  Proof.
    rewrite /FromExist. iDestruct 1 as (x) "H".
    iApply (subprot_trans with "H"). iApply subprot_texist_intro_r.
  Qed.

  Global Instance frame_send q m v R P Q p :
    Frame q R P Q 
    Frame q R ((<!> MSG v {{ P }}; p)  (<!> m))
              ((<!> MSG v {{ Q }}; p)  (<!> m)) | 10.
  Proof.
    rewrite /Frame /=. iIntros (HP) "[HR H]".
    iApply (subprot_trans with "[HR] H"). iApply subprot_payload_elim_r.
    iIntros "HQ". iApply subprot_payload_intro_l. iApply HP; iFrame.
  Qed.
  Global Instance frame_recv q m v R P Q p :
    Frame q R P Q 
    Frame q R ((<?> m)  (<?> MSG v {{ P }}; p))
              ((<?> m)  (<?> MSG v {{ Q }}; p)) | 11.
  Proof.
    rewrite /Frame /=. iIntros (HP) "[HR H]".
    iApply (subprot_trans with "H"). iApply subprot_payload_elim_l.
    iIntros "HQ". iApply subprot_payload_intro_r. iApply HP; iFrame.
  Qed.
  Global Instance from_sep_send m v P p :
    FromSep ((<!> MSG v {{ P }}; p)  (<!> m)) P ((<!> MSG v; p)  (<!> m)) | 10.
  Proof. rewrite /FromSep. by iIntros "[$ H]". Qed.
  Global Instance from_sep_recv m v P p :
    FromSep ((<?> m)  (<?> MSG v {{ P }}; p)) P ((<?> m)  (<?> MSG v; p)) | 11.
  Proof. rewrite /FromSep. by iIntros "[$ H]". Qed.

  Global Instance from_modal_msg a v p1 p2 :
    FromModal True (modality_instances.modality_laterN 1) (p1  p2)
              ((<a> MSG v; p1)  (<a> MSG v; p2)) (p1  p2).
  Proof. intros _. apply subprot_base. Qed.

  (** Session normalize *)
  Lemma prot_unfold_eq p1 p2 : p1  p2  ProtUnfold p1 p2.
  Proof. intros Hp d q [Hq]; constructor. destruct d; by rewrite Hp. Qed.

  Global Instance prot_normalize_done p : ProtNormalize false p p | 0.
  Proof. constructor. iApply subprot_refl. Qed.
  Global Instance prot_normalize_done_dual p : ProtNormalize true p (dual p) | 0.
  Proof. constructor. iApply subprot_refl. Qed.
  Global Instance prot_normalize_done_dual_end d a1 a2 P :
    ActionDualIf d a1 a2 
    ProtNormalize d (END@a1 {{ P }}) (END@a2 {{ P }}) | 0.
  Proof. intros [->]. constructor. destruct d; rewrite ?dual_end; auto. Qed.

  Global Instance prot_normalize_dual d p q :
    ProtNormalize (negb d) p q 
    ProtNormalize d (dual p) q.
  Proof. intros [Hp]; constructor. by destruct d; rewrite /= ?dual_dual. Qed.

  Global Instance msg_normalize_base d a v P p q :
    ProtNormalize d p q 
    MsgNormalize d a (MSG v {{ P }}; p) (MSG v {{ P }}; q).
  Proof.
    intros [Hp]; do 2 split. iApply subprot_trans; [|by iApply subprot_base].
    destruct d; by rewrite /= ?dual_msg ?msg_dual_base.
  Qed.
  Global Instance msg_normalize_exist_base {A} d a (m : A  msg)
      (v : A  val) (P : A  aProp) (q : A  aMiniProt) y v' P' q' :
    ActionDualIf d a ASend 
    (∀ x, MsgNormalize d a (m x) (MSG v x {{ P x }}; q x)) 
    TCEq (v y) v'  TCEq (P y) P'  TCEq (q y) q' 
    MsgNormalize d a (∃ x, m x) (MSG v' {{ P' }}; q').
  Proof.
    intros [Ha] Hpq <-%TCEq_eq <-%TCEq_eq <-%TCEq_eq. do 2 split.
    destruct (Hpq y) as [[Hm]]. destruct a, d; simplify_eq/=.
    - by iExists y.
    - rewrite dual_msg /= msg_dual_exist. iExists y. by rewrite dual_msg in Hm.
  Qed.

  Global Instance msg_normalize_exist {A} d a (m1 m2 : A  msg) :
    (∀ x, MsgNormalize d a (m1 x) (m2 x)) 
    MsgNormalize d a (∃ x, m1 x) (∃ x, m2 x).
  Proof.
    intros Hp; do 2 split.
    destruct d, a; simpl in *; rewrite ?dual_msg ?msg_dual_exist /=;
      iIntros (x); iExists x; destruct (Hp x) as [[Hpx]];
      move: Hpx; rewrite ?dual_msg; auto.
  Qed.

  Global Instance msg_tele_base v P p :
    MsgTele (TT:=TeleO) (MSG v {{ P }}; p) v P p.
  Proof. by constructor. Qed.
  Global Instance msg_tele_exist {A} {TT : A  tele} (m : A  msg) tv tP tp :
    (∀ x, MsgTele (TT:=TT x) (m x) (tv x) (tP x) (tp x)) 
    MsgTele (TT:=TeleS TT) (∃ x, m x) tv tP tp.
  Proof. intros Hm. constructor; simpl; f_equiv=> x. apply Hm. Qed.

  Global Instance msg_normalize_texist {TT : tele} d a m (tv : TT -t> _) tP tp tq :
    MsgTele m tv tP tp 
    (∀.. x, ProtNormalize d (tele_app tp x) (tele_app tq x)) 
    MsgNormalize d a m (∃.. x : TT, MSG tele_app tv x {{ tele_app tP x }}; tele_app tq x).
  Proof.
    rewrite tforall_forall. intros [Hm] Hpq; do 2 split.
    destruct d; rewrite /= Hm ?dual_msg ?msg_dual_base ?msg_dual_texist {Hm};
      destruct a; simpl; iIntros (x); iExists x; rewrite ?msg_dual_base;
      iIntros "$ !>"; destruct (Hpq x); auto.
  Qed.

  Global Instance prot_normalize_message d a1 a2 m1 m2 :
    ActionDualIf d a1 a2 
    MsgNormalize d a1 m1 m2 
    ProtNormalize d (<a1> m1) (<a2> m2).
  Proof. by intros [->] [Hm]. Qed.

  (** Automatically perform normalization of protocols in the proof mode when
  using [iAssumption] and [iFrame]. *)
  Global Instance from_assumption_own_chan q c p1 p2 :
    ProtNormalize false p1 p2 
    FromAssumption q (c  p1) (c  p2).
  Proof.
    intros [Hp]. rewrite /FromAssumption bi.intuitionistically_if_elim.
    iIntros "H". by iApply (own_chan_subprot with "H").
  Qed.
  Global Instance into_wand_own_chan_send q c p1 v P p2 Q :
    ProtNormalize false p1 (<!> MSG v {{ P }}; p2) 
    FromAssumption false Q ( P) 
    IntoWand q false (c  p1) Q (c  <!> MSG v; p2).
  Proof.
    intros [Hp]; rewrite /FromAssumption /IntoWand /= bi.intuitionistically_if_elim /=.
    iIntros (->) "H HP". iApply (own_chan_subprot with "H").
    iApply subprot_trans; first by iApply Hp. iFrame "HP". auto.
  Qed.
  Global Instance into_wand_own_chan_end q c p P Q :
    ProtNormalize false p (END! {{ P }}) 
    FromAssumption false Q ( P) 
    IntoWand q false (c  p) Q (c  END!).
  Proof.
    intros [Hp]; rewrite /FromAssumption /IntoWand /= bi.intuitionistically_if_elim /=.
    iIntros (->) "H HP". iApply (own_chan_subprot with "H").
    iApply subprot_trans; first by iApply Hp. iFrame "HP". auto.
  Qed.
  Global Instance frame_own_chan q c p1 p2 :
    ProtNormalize false p1 p2 
    Frame q (c  p1) (c  p2) emp.
  Proof.
    intros [Hp]. rewrite /Frame bi.intuitionistically_if_elim.
    iIntros "[H _]". by iApply (own_chan_subprot with "H").
  Qed.
End classes.

Lemma tac_wp_recv {TT : tele} {Δ Δ' n k e i c p Φ tv tP tp Q} j :
  DoPureStepsIntoCtx e (TCEq (recv (Val c))) n k 
  MaybeIntoLaterNEnvs n Δ Δ'  (* we should do one more in the part not containing i *)
  envs_lookup i Δ' = Some (false, c  p)%I 
  ProtNormalize false p (<?.. x> MSG tv x {{ tP x }}; tp x) 
  (∀.. x, FinalizeWP (k (Val (tv x))) Φ (tele_app Q x)) 
  let Δ'' := envs_delete false i false Δ' in
  (∀.. x : TT,
    match envs_app false (Esnoc (Esnoc Enil j (tP x)) i (c  tp x)) Δ'' with
    | Some Δ''' => envs_entails Δ''' (tele_app Q x)
    | None => False
    end) 
  envs_entails Δ (WP e {{ Φ }}).
Proof.
  rewrite envs_entails_unseal /= !tforall_forall.
  iIntros ((e'&?&<-%TCEq_eq&Hwp)%do_pure_steps_into_ctx_wp ??? HQ HΔ'') "HΔ".
  rewrite into_laterN_env_sound /=. iApply Hwp; iNext.
  rewrite envs_lookup_sound //=. set (envs_delete true i false Δ') as Δ''.
  iDestruct "HΔ" as "[Hc HΔ]". iApply (wp_recv with "Hc").
  iIntros "!> %w (%x & -> & Hc & HP)". destruct (HQ x) as [HQ']; clear HQ.
  specialize (HΔ'' x). destruct (envs_app _ _ _) as [Δ'''|] eqn:?; last done.
  iApply HQ'. iApply HΔ''.
  iApply (envs_app_sound with "[$]"); first done. by iFrame.
Qed.

Lemma tac_wp_send {TT : tele} {Δ Δ' e n k i c v p tv tP tp Φ} neg js :
  DoPureStepsIntoCtx e (TCEq (send (Val c) (Val v))) n k 
  MaybeIntoLaterNEnvs n Δ Δ' 
  envs_lookup i Δ' = Some (false, c  p)%I 
  ProtNormalize false p (<!.. x> MSG tv x {{ tP x }}; tp x) 
  let Δ'' := envs_delete false i false Δ' in
  (∃.. x : TT,
    match envs_split (if neg is true then base.Right else base.Left) js Δ'' with
    | Some (Δ1,Δ2) =>
       match envs_app false (Esnoc Enil i (c  tp x)) Δ2 with
       | Some Δ2' =>
          v = tv x 
          envs_entails Δ1 (tP x) 
           Q, FinalizeWP (k (Val #())) Φ Q  envs_entails Δ2' Q
       | None => False
       end
    | None => False
    end) 
  envs_entails Δ (WP e {{ Φ }}).
Proof.
  rewrite envs_entails_unseal /= !texist_exist.
  iIntros ((e'&?&<-%TCEq_eq&Hwp)%do_pure_steps_into_ctx_wp ?? [Hp] [x HΔ'']) "HΔ".
  rewrite into_laterN_env_sound /=. iApply Hwp; iNext.
  destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
  destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
  rewrite envs_lookup_sound //= envs_split_sound //=.
  rewrite (envs_app_sound Δ2) //; simpl. destruct HΔ'' as (-> & -> & Q & [HQ] & ->).
  iDestruct "HΔ" as "(Hc & HP & HQ)". iApply (wp_send with "[Hc HP]").
  { iApply (own_chan_subprot with "Hc"); iIntros "!>".
    iApply subprot_trans; [iApply Hp|]. iExists x. iFrame "HP". auto. }
  iIntros "!> Hc". iApply HQ. iApply "HQ"; by iFrame.
Qed.

Lemma tac_wp_wait {Δ Δ' e n k c p i Φ Q} :
  DoPureStepsIntoCtx e (TCEq (wait (Val c))) n k 
  MaybeIntoLaterNEnvs n Δ Δ' 
  envs_lookup i Δ' = Some (false, c  p)%I 
  ProtNormalize false p END? 
  FinalizeWP (k (Val #())) Φ Q 
  envs_entails (envs_delete false i false Δ') Q 
  envs_entails Δ (WP e {{ Φ }}).
Proof.
  rewrite envs_entails_unseal.
  iIntros ((e'&?&<-%TCEq_eq&Hwp)%do_pure_steps_into_ctx_wp ??? [HQ] HΔ') "HΔ".
  rewrite into_laterN_env_sound /= envs_lookup_sound //=.
  set (envs_delete true i false Δ') as Δ''.
  iDestruct "HΔ" as "[Hc HΔ]"; [done..|].
  iApply Hwp. iNext. iApply (wp_wait with "Hc"); iIntros "!> _".
  iApply HQ. by iApply HΔ'.
Qed.

Lemma tac_wp_close {Δ Δ' e n k c p i Φ Q} :
  DoPureStepsIntoCtx e (TCEq (close (Val c))) n k 
  MaybeIntoLaterNEnvs n Δ Δ' 
  envs_lookup i Δ' = Some (false, c  p)%I 
  ProtNormalize false p END! 
  FinalizeWP (k (Val #())) Φ Q 
  envs_entails (envs_delete false i false Δ') Q 
  envs_entails Δ (WP e {{ Φ }}).
Proof.
  rewrite envs_entails_unseal.
  iIntros ((e'&?&<-%TCEq_eq&Hwp)%do_pure_steps_into_ctx_wp ??? [HQ] HΔ') "HΔ".
  rewrite into_laterN_env_sound /= envs_lookup_sound //=.
  set (envs_delete true i false Δ') as Δ''.
  iDestruct "HΔ" as "[Hc HΔ]"; [done..|].
  iApply Hwp. iNext. iApply (wp_close with "Hc"); iNext.
  iApply HQ. by iApply HΔ'.
Qed.

Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
  iStartProof;
  let Htmp := iFresh in
  lazymatch goal with
  | |- environments.envs_entails _ (WP _ {{ _ }}) =>
     notypeclasses refine (tac_wp_recv Htmp _ _ _ _ _ _);
       [tc_solve || fail 1 "wp_recv: cannot find 'recv' subexpression"
       |tc_solve (* into laters *)
       |iAssumptionCore || fail 1 "wp_recv: cannot find ↦"
       |tc_solve || fail 1 "wp_recv: protocol not a recv"
       |try tc_solve (* wp finalize *)
       |pm_reduce; cbn [tforall tele_fold tele_bind tele_app];
        tac_intros; intros; tac Htmp]
  | _ => fail "wp_recv: goal not a 'wp'"
  end.

Tactic Notation "wp_recv" "as" constr(pat) :=
  wp_recv_core (idtac) as (fun H => iDestructHyp H as pat).
Tactic Notation "wp_recv" := wp_recv as "_".
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" constr(pat) :=
  wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat).
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" :=
  wp_recv_core (intros xs) as (fun H => iDestructHyp H as "_").

Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
  let solve_done d :=
    lazymatch d with
    | true =>
       done ||
       let Q := match goal with |- envs_entails _ ?Q => Q end in
       fail "wp_send: cannot solve" Q "using done"
    | false => idtac
    end in
  lazymatch spec_pat.parse pat with
  | [SGoal (SpecGoal GSpatial ?neg ?Hs_frame ?Hs ?d)] =>
     let Hs' := eval cbv in (if neg then Hs else Hs_frame ++ Hs) in
     iStartProof;
     lazymatch goal with
     | |- environments.envs_entails _ (WP _ {{ _ }}) =>
          notypeclasses refine (tac_wp_send neg Hs' _ _ _ _ _);
            [tc_solve || fail 1 "wp_send: cannot find 'send' subexpression"
            |tc_solve (* into laters *)
            |iAssumptionCore || fail 1 "wp_send: cannot find ↦"
            |tc_solve || fail 1 "wp_send: protocol not a send"
            |pm_reduce; simpl; tac_exist;
             repeat lazymatch goal with |-  _, _ => eexists _ end;
             notypeclasses refine (conj _ (conj _ (ex_intro _ _ (conj _ _))));
               [notypeclasses refine (eq_refl _)
                 || fail 1 "wp_send: value does not match protocol"
               |iFrame Hs_frame; solve_done d
               |tc_solve (* simpl *)
               |]]
     | _ => fail "wp_send: not a 'wp'"
     end
  | _ => fail "wp_send: only a single non-framing spec pattern supported"
  end.

(* From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/931 *)
Ltac2 with_ltac1_list f ls :=
  let ls := Option.get (Ltac1.to_list ls) in
  f ls.

Tactic Notation "wp_send" "with" constr(pat) :=
  wp_send_core (idtac) with pat.
Tactic Notation "wp_send" := wp_send with "[//]".
Tactic Notation "wp_send" "(" ne_uconstr_list_sep(xs,",") ")" "with" constr(pat) :=
  wp_send_core (idtac;
    let f := ltac2:(xs |- with_ltac1_list (List.iter ltac1:(x |- eexists x)) xs)
    in f xs) with pat.

Tactic Notation "wp_wait" :=
  iStartProof;
  lazymatch goal with
  | |- environments.envs_entails _ (WP _ {{ _ }}) =>
     notypeclasses refine (tac_wp_wait _ _ _ _ _ _);
       [tc_solve || fail 1 "wp_wait: cannot find 'wait' subexpression"
       |tc_solve (* into laters *)
       |iAssumptionCore || fail 1 "wp_wait: cannot find ↦"
       |tc_solve || fail 1 "wp_wait: protocol not an END?"
       |tc_solve (* simpl *)
       |pm_reduce]
  | _ => fail "wp_wait: goal not a 'wp'"
  end.
Tactic Notation "wp_wait" "!" := wp_wait; wp_pures _.

Tactic Notation "wp_close" :=
  iStartProof;
  lazymatch goal with
  | |- environments.envs_entails _ (WP _ {{ _ }}) =>
     notypeclasses refine (tac_wp_close _ _ _ _ _ _);
       [tc_solve || fail 1 "wp_close: cannot find 'close' subexpression"
       |tc_solve (* into laters *)
       |iAssumptionCore || fail 1 "wp_close: cannot find ↦"
       |tc_solve || fail 1 "wp_close: protocol not an END!"
       |tc_solve (* simpl *)
       |pm_reduce]
  | _ => fail "wp_close: goal not a 'wp'"
  end.
Tactic Notation "wp_close" "!" := wp_close; wp_pures _.