term_typing_rules.v 22 KB
Newer Older
Jonas Kastberg's avatar
Jonas Kastberg committed
1
From stdpp Require Import pretty.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.bi.lib Require Import core.
3
From iris.base_logic.lib Require Import invariants.
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5
From iris.heap_lang Require Import metatheory.
From iris.heap_lang.lib Require Export spawn par assert.
Robbert Krebbers's avatar
Rename.  
Robbert Krebbers committed
6
From actris.logrel Require Export subtyping term_typing_judgment session_types.
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9
From actris.logrel Require Import environments.
From actris.utils Require Import switch.
From actris.channel Require Import proofmode.
10 11 12

Section properties.
  Context `{heapG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
13 14 15
  Implicit Types A B : ltty Σ.
  Implicit Types S T : lsty Σ.
  Implicit Types Γ : gmap string (ltty Σ).
16

17
  (** Frame rule *)
18
  Lemma ltyped_frame Γ Γ' Γ1 Γ1' Γ2 e A :
19 20 21 22 23 24 25 26 27 28 29 30
    env_split Γ Γ1 Γ2 -
    env_split Γ' Γ1' Γ2 -
    (Γ1  e : A  Γ1') -
    Γ  e : A  Γ'.
  Proof.
    iIntros "#Hsplit #Hsplit' #Htyped !>" (vs) "Henv".
    iDestruct ("Hsplit" with "Henv") as "[Henv1 Henv2]".
    iApply (wp_wand with "(Htyped Henv1)").
    iIntros (v) "[$ Henv1']".
    iApply "Hsplit'". iFrame "Henv1' Henv2".
  Qed.

31 32
  (** Variable properties *)
  Lemma ltyped_var Γ (x : string) A :
Daniël Louwrink's avatar
Daniël Louwrink committed
33
    Γ !! x = Some A   Γ  x : A  <[x := (copy- A)%lty]> Γ.
34
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
    iIntros (HΓx) "!>"; iIntros (vs) "HΓ /=".
Daniël Louwrink's avatar
Daniël Louwrink committed
36 37 38 39 40 41 42 43
    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv.
    iApply wp_value.
    iAssert (ltty_car (copy- A) v)%lty as "#HAm". { iApply coreP_intro. iApply "HA". }
    iFrame "HA".
    iDestruct (env_ltyped_insert _ _ x with "HAm HΓ") as "HΓ".
    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
    iApply "HΓ".
  Qed.
44

Robbert Krebbers's avatar
Robbert Krebbers committed
45 46 47
  (** Subtyping *)
  Theorem ltyped_subsumption Γ Γ2 e τ1 τ2 :
    τ1 <: τ2 - (Γ  e : τ1  Γ2) - (Γ  e : τ2  Γ2).
48
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50 51 52
    iIntros "#Hle #Hltyped" (vs) "!> Henv".
    iDestruct ("Hltyped" with "Henv") as "Hltyped'".
    iApply (wp_wand with "Hltyped' [Hle]").
    iIntros (v) "[H1 $]". by iApply "Hle".
53 54
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
55 56 57 58 59 60 61
  (** Basic properties *)
  Lemma ltyped_unit Γ :  Γ  #() : ().
  Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed.
  Lemma ltyped_bool Γ (b : bool) :  Γ  #b : lty_bool.
  Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed.
  Lemma ltyped_nat Γ (n : Z) :  Γ  #n : lty_int.
  Proof. iIntros "!>" (vs) "Henv /=". iApply wp_value. eauto. Qed.
62

Robbert Krebbers's avatar
Robbert Krebbers committed
63
  (** Arrow properties *)
64 65 66
  Lemma ltyped_app Γ1 Γ2 Γ3 e1 e2 A1 A2 :
    (Γ2  e1 : A1  A2  Γ3) - (Γ1  e2 : A1  Γ2) -
    Γ1  e1 e2 : A2  Γ3.
67
  Proof.
68 69 70 71
    iIntros "#H1 #H2". iIntros (vs) "!> HΓ /=".
    wp_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
    wp_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf HΓ]".
    iApply wp_frame_r. iFrame "HΓ". iApply ("Hf" $! v with "HA1").
72 73
  Qed.

74 75 76
  Lemma ltyped_lam Γ Γ' x e A1 A2 :
    (binder_insert x A1 Γ  e : A2  Γ') -
    Γ  (λ: x, e) : A1  A2  .
77
  Proof.
78 79
    iIntros "#He" (vs) "!> HΓ /=".
    wp_pures.
80
    iSplitL; last by iApply env_ltyped_empty.
81
    iIntros (v) "HA1". wp_pures.
82 83
    iDestruct ("He" $!((binder_insert x v vs)) with "[HA1 HΓ]") as "He'".
    { iApply (env_ltyped_insert with "[HA1 //] HΓ"). }
Robbert Krebbers's avatar
Robbert Krebbers committed
84
    iDestruct (wp_wand _ _ _ _ (ltty_car A2) with "He' []") as "He'".
85
    { iIntros (w) "[$ _]". }
86 87 88
    destruct x as [|x]; rewrite /= -?subst_map_insert //.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
89
  (* Typing rule for introducing copyable functions *)
90
  Lemma ltyped_rec Γ Γ' Γ'' f x e A1 A2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
91
    env_copy Γ Γ' -
92
    (binder_insert f (A1  A2)%lty (binder_insert x A1 Γ')  e : A2  Γ'') -
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113
    Γ  (rec: f x := e) : A1  A2  .
  Proof.
    iIntros "#Hcopy #He". iIntros (vs) "!> HΓ /=". iApply wp_fupd. wp_pures.
    iDestruct ("Hcopy" with "HΓ") as "HΓ".
    iMod (fupd_mask_mono with "HΓ") as "#HΓ"; first done.
    iModIntro. iSplitL; last by iApply env_ltyped_empty.
    iLöb as "IH".
    iIntros (v) "!> HA1". wp_pures. set (r := RecV f x _).
    iDestruct ("He" $!(binder_insert f r (binder_insert x v vs))
                  with "[HΓ HA1]") as "He'".
    { iApply (env_ltyped_insert with "IH").
      iApply (env_ltyped_insert with "HA1 HΓ"). }
    iDestruct (wp_wand _ _ _ _ (ltty_car A2) with "He' []") as "He'".
    { iIntros (w) "[$ _]". }
    destruct x as [|x], f as [|f]; rewrite /= -?subst_map_insert //.
    destruct (decide (x = f)) as [->|].
    - by rewrite subst_subst delete_idemp !insert_insert -subst_map_insert.
    - rewrite subst_subst_ne // -subst_map_insert.
      by rewrite -delete_insert_ne // -subst_map_insert.
  Qed.

114
  Lemma ltyped_let Γ1 Γ2 Γ3 x e1 e2 A1 A2 :
115
    (Γ1  e1 : A1  Γ2) - (binder_insert x A1 Γ2  e2 : A2  Γ3) -
116 117 118 119 120 121 122
    Γ1  (let: x:=e1 in e2) : A2  binder_delete x Γ3.
  Proof.
    iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1"=> /=.
    wp_apply (wp_wand with "(He1 HΓ1)").
    iIntros (v) "[HA1 HΓ2]".
    wp_pures.
    iDestruct (env_ltyped_insert _ _ x with "HA1 HΓ2") as "HΓ2".
123
    iDestruct ("He2" with "HΓ2") as "He2'".
124 125 126 127 128 129
    destruct x as [|x]; rewrite /= -?subst_map_insert //.
    wp_apply (wp_wand with "He2'").
    iIntros (w) "[HA2 HΓ3]".
    iFrame.
    iApply env_ltyped_delete=> //.
  Qed.
130 131

  (** Product properties  *)
132 133 134
  Lemma ltyped_pair Γ1 Γ2 Γ3 e1 e2 A1 A2 :
    (Γ2  e1 : A1  Γ3) - (Γ1  e2 : A2  Γ2) -
    Γ1  (e1,e2) : A1 * A2  Γ3.
135
  Proof.
136 137 138 139
    iIntros "#H1 #H2". iIntros (vs) "!> HΓ /=".
    wp_apply (wp_wand with "(H2 [HΓ //])"); iIntros (w2) "[HA2 HΓ]".
    wp_apply (wp_wand with "(H1 [HΓ //])"); iIntros (w1) "[HA1 HΓ]".
    wp_pures. iFrame "HΓ". iExists w1, w2. by iFrame.
140 141
  Qed.

142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
  Lemma ltyped_fst Γ A1 A2 (x : string) :
    Γ !! x = Some (A1 * A2)%lty 
     Γ  Fst x : A1  <[x := (copy- A1 * A2)%lty]> Γ.
  Proof.
    iIntros (Hx vs) "!> HΓ /=".
    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv.
    iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]".
    wp_pures.
    iAssert (ltty_car (copy- A1) v1)%lty as "#HA1m". { iApply coreP_intro. iApply "HA1". }
    iFrame "HA1".
    iAssert (ltty_car (copy- A1 * A2) (v1, v2))%lty with "[HA2]" as "HA".
    { iExists v1, v2. iSplit=>//. iFrame "HA1m HA2". }
    iDestruct (env_ltyped_insert _ _ x with "HA HΓ") as "HΓ".
    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
    iFrame "HΓ".
  Qed.
158

159 160 161
  Lemma ltyped_snd Γ A1 A2 (x : string) :
    Γ !! x = Some (A1 * A2)%lty 
     Γ  Snd x : A2  <[x := (A1 * copy- A2)%lty]> Γ.
162
  Proof.
163 164 165 166 167 168 169 170 171 172 173
    iIntros (Hx vs) "!> HΓ /=".
    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done; rewrite Hv.
    iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]".
    wp_pures.
    iAssert (ltty_car (copy- A2) v2)%lty as "#HA2m". { iApply coreP_intro. iApply "HA2". }
    iFrame "HA2".
    iAssert (ltty_car (A1 * copy- A2) (v1, v2))%lty with "[HA1]" as "HA".
    { iExists v1, v2. iSplit=>//. iFrame "HA2m HA1". }
    iDestruct (env_ltyped_insert _ _ x with "HA HΓ") as "HΓ".
    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
    iFrame "HΓ".
174 175 176
  Qed.

  (** Sum Properties *)
177
  Lemma ltyped_injl Γ e A1 A2 :
178 179 180 181
    (Γ  e : A1) - Γ  InjL e : A1 + A2.
  Proof.
    iIntros "#HA" (vs) "!> HΓ /=".
    wp_apply (wp_wand with "(HA [HΓ //])").
182
    iIntros (v) "[HA' $]". wp_pures.
183 184 185
    iLeft. iExists v. auto.
  Qed.

186
  Lemma ltyped_injr Γ e A1 A2 :
187 188 189 190
    (Γ  e : A2) - Γ  InjR e : A1 + A2.
  Proof.
    iIntros "#HA" (vs) "!> HΓ /=".
    wp_apply (wp_wand with "(HA [HΓ //])").
191
    iIntros (v) "[HA' $]". wp_pures.
192 193 194
    iRight. iExists v. auto.
  Qed.

Daniël Louwrink's avatar
Daniël Louwrink committed
195 196
  (* TODO: This probably requires there to be a rule that allows dropping arbitrary
  resources from the postcondition. Check if there is such a rule. *)
Daniël Louwrink's avatar
Daniël Louwrink committed
197 198 199 200 201
  Lemma ltyped_case Γ1 Γ2 Γ3 e1 e2 e3 A1 A2 B :
    (Γ1  e1 : A1 + A2  Γ2) -
    (Γ2  e2 : A1  B  Γ3) -
    (Γ2  e3 : A2  B  Γ3) -
    (Γ1  Case e1 e2 e3 : B  Γ3).
202
  Proof.
Daniël Louwrink's avatar
Daniël Louwrink committed
203 204 205 206 207 208 209 210 211 212 213 214 215 216
    iIntros "#H1 #H2 #H3" (vs) "!> HΓ1 /=".
    wp_bind (subst_map vs e1).
    iSpecialize ("H1" with "HΓ1").
    iApply (wp_wand with "H1"). iIntros (s) "[Hs HΓ2]".
    iDestruct "Hs" as "[Hs|Hs]"; iDestruct "Hs" as (w ->) "HA"; wp_case.
    - wp_bind (subst_map vs e2).
      iApply (wp_wand with "(H2 HΓ2)"). iIntros (v) "[Hv HΓ3]".
      iApply (wp_wand with "(Hv HA)"). iIntros (v') "HB".
      iFrame "HΓ3 HB".
    - wp_bind (subst_map vs e3).
      iApply (wp_wand with "(H3 HΓ2)"). iIntros (v) "[Hv HΓ3]".
      iApply (wp_wand with "(Hv HA)"). iIntros (v') "HB".
      iFrame "HΓ3 HB".
  Qed.
217 218

  (** Universal Properties *)
Jonas Kastberg's avatar
Jonas Kastberg committed
219 220
  Lemma ltyped_tlam Γ e k (C : lty Σ k  ltty Σ) :
    ( M, Γ  e : C M  ) - Γ  (λ: <>, e) :  M, C M  .
221
  Proof.
222 223
    iIntros "#He" (vs) "!> HΓ /=". wp_pures.
    iSplitL; last by iApply env_ltyped_empty.
Jonas Kastberg's avatar
Jonas Kastberg committed
224 225
    iIntros (M) "/=". wp_pures.
    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[$ _]".
226 227
  Qed.

Jonas Kastberg's avatar
Jonas Kastberg committed
228 229
  Lemma ltyped_tapp Γ Γ2 e k (C : lty Σ k  ltty Σ) M :
    (Γ  e :  M, C M  Γ2) - Γ  e #() : C M  Γ2.
230
  Proof.
Jonas Kastberg's avatar
Jonas Kastberg committed
231
    iIntros "#He" (vs) "!> HΓ /=".
Robbert Krebbers's avatar
Robbert Krebbers committed
232
    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ] /=".
Jonas Kastberg's avatar
Jonas Kastberg committed
233
    iApply (wp_wand with "HB [HΓ]"). by iIntros (v) "$".
234 235 236
  Qed.

  (** Existential properties *)
Jonas Kastberg's avatar
Jonas Kastberg committed
237 238 239 240 241 242 243
  Lemma ltyped_pack Γ e k (C : lty Σ k  ltty Σ) M :
    (Γ  e : C M) - Γ  e :  M, C M.
  Proof.
    iIntros "#He" (vs) "!> HΓ /=".
    wp_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists M.
  Qed.

Daniël Louwrink's avatar
Daniël Louwrink committed
244 245 246 247
  Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 (x : string) e (C : lty Σ k  ltty Σ) A :
    Γ1 !! x = Some (lty_exist C) 
    ( X, binder_insert x (C X) Γ1  e : A  Γ2) -
    (Γ1  e : A  Γ2).
248
  Proof.
Daniël Louwrink's avatar
Daniël Louwrink committed
249 250 251 252 253 254 255
    iIntros (Hx) "#He". iIntros (vs) "!> HΓ".
    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HB HΓ]"; first done.
    iDestruct ("HB") as (B) "HB".
    iDestruct (env_ltyped_insert _ _ x with "HB HΓ") as "HΓ".
    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
    iApply (wp_wand with "(He HΓ)"). eauto.
  Qed.
256 257

  (** Mutable Reference properties *)
Daniël Louwrink's avatar
Daniël Louwrink committed
258 259 260
  Lemma ltyped_alloc Γ1 Γ2 e A :
    (Γ1  e : A  Γ2) -
    (Γ1  ref e : ref_mut A  Γ2).
261
  Proof.
Daniël Louwrink's avatar
Daniël Louwrink committed
262 263 264 265 266 267 268
    iIntros "#He" (vs) "!> HΓ1 /=".
    wp_bind (subst_map vs e).
    iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv HΓ2]".
    wp_alloc l as "Hl".
    iFrame "HΓ2".
    iExists l, v; iSplit=>//. iFrame "Hv Hl".
  Qed.
269

Daniël Louwrink's avatar
Daniël Louwrink committed
270 271 272
  Lemma ltyped_load Γ (x : string) A :
    Γ !! x = Some (ref_mut A)%lty 
     Γ  ! x : A  <[x := (ref_mut (copy- A))%lty]> Γ.
273
  Proof.
Daniël Louwrink's avatar
Daniël Louwrink committed
274 275 276 277 278 279 280 281 282 283 284 285 286 287
    iIntros (Hx vs) "!> HΓ".
    iDestruct (env_ltyped_lookup with "HΓ") as (v Hv) "[HA HΓ]"; first done.
    simpl. rewrite Hv.
    iDestruct "HA" as (l w ->) "[Hl Hw]".
    wp_load.
    iAssert (ltty_car (copy- A) w)%lty as "#HAm".
    { iApply coreP_intro. iApply "Hw". }
    iFrame "Hw".
    iAssert (ltty_car (ref_mut (copy- A))%lty #l) with "[Hl]" as "HA".
    { iExists l, w. iSplit=>//. iFrame "Hl HAm". }
    iDestruct (env_ltyped_insert _ _ x with "HA HΓ") as "HΓ".
    rewrite /binder_insert insert_delete (insert_id _ _ _ Hv).
    iFrame "HΓ".
  Qed.
288

Daniël Louwrink's avatar
Daniël Louwrink committed
289
  Lemma ltyped_store Γ Γ' (x : string) e A B :
Daniël Louwrink's avatar
Daniël Louwrink committed
290
    Γ' !! x = Some (ref_mut A)%lty 
Daniël Louwrink's avatar
Daniël Louwrink committed
291 292
    (Γ  e : B  Γ') -
    Γ  x <- e : ()  <[x := (ref_mut B)%lty]> Γ'.
293
  Proof.
Daniël Louwrink's avatar
Daniël Louwrink committed
294 295 296 297 298 299 300 301 302 303 304 305 306
    iIntros (Hx) "#He". iIntros (vs) "!> HΓ /=".
    wp_bind (subst_map vs e).
    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
    iDestruct (env_ltyped_lookup with "HΓ'") as (w Hw) "[HA HΓ']"; first done.
    rewrite Hw.
    iDestruct "HA" as (l v' ->) "[Hl HA]".
    wp_store. iSplitR; first done.
    iAssert (ltty_car (ref_mut B)%lty #l) with "[Hl HB]" as "HB".
    { iExists l, v. iSplit=>//. iFrame "Hl HB". }
    iDestruct (env_ltyped_insert _ _ x with "HB HΓ'") as "HΓ'".
    rewrite /binder_insert insert_delete (insert_id _ _ _ Hw).
    iFrame "HΓ'".
  Qed.
307 308

  (** Weak Reference properties *)
309 310 311
  Lemma ltyped_upgrade_shared  Γ Γ' e A :
    (Γ  e : ref_mut A  Γ') -
    Γ  e : ref_shr A  Γ'.
312
  Proof.
313 314 315 316 317 318 319 320 321 322
    iIntros "#He" (vs) "!> HΓ".
    iApply wp_fupd.
    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv HΓ']".
    iDestruct "Hv" as (l w ->) "[Hl HA]".
    iFrame "HΓ'".
    iExists l.
    iMod (inv_alloc (ref_shrN .@ l) _ ( v : val, l  v  ltty_car A v) with "[Hl HA]") as "Href".
    { iExists w. iFrame "Hl HA". }
    iModIntro.
    by iFrame "Href".
323 324
  Qed.

325 326 327
  Lemma ltyped_load_shared Γ Γ' e A :
    (Γ  e : ref_shr A  Γ') -
    Γ  ! e : copy- A  Γ'.
328
  Proof.
329 330 331 332 333 334 335 336 337 338 339
    iIntros "#He" (vs) "!> HΓ /=".
    wp_bind (subst_map vs e).
    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv HΓ]".
    iDestruct "Hv" as (l ->) "#Hv".
    iInv (ref_shrN .@ l) as (v) "[>Hl HA]" "Hclose".
    wp_load.
    iAssert (ltty_car (copy- A) v)%lty as "#HAm". { iApply coreP_intro. iApply "HA". }
    iMod ("Hclose" with "[Hl HA]") as "_".
    { iExists v. iFrame "Hl HA". }
    iModIntro.
    iFrame "HAm HΓ".
340 341
  Qed.

342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358
  Lemma ltyped_store_shared Γ1 Γ2 Γ3 e1 e2 A :
    (Γ1  e2 : A  Γ2) -
    (Γ2  e1 : ref_shr A  Γ3) -
    (Γ1  e1 <- e2 : ()  Γ3).
  Proof.
    iIntros "#H1 #H2" (vs) "!> HΓ1 /=".
    wp_bind (subst_map vs e2).
    iApply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
    wp_bind (subst_map vs e1).
    iApply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw HΓ3]".
    iDestruct "Hw" as (l ->) "#Hw".
    iInv (ref_shrN .@ l) as (?) "[>Hl HA]" "Hclose".
    wp_store.
    iMod ("Hclose" with "[Hl Hv]") as "_".
    { iExists v. iFrame "Hl Hv". }
    iModIntro. iSplit=>//.
  Qed.
359

360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378
  Lemma ltyped_fetch_and_add_shared Γ1 Γ2 Γ3 e1 e2 :
    (Γ1  e2 : lty_int  Γ2) -
    (Γ2  e1 : ref_shr lty_int  Γ3) -
    (Γ1  FAA e1 e2 : lty_int  Γ3).
  Proof.
    iIntros "#H1 #H2" (vs) "!> HΓ1 /=".
    wp_bind (subst_map vs e2).
    iApply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
    wp_bind (subst_map vs e1).
    iApply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw HΓ3]".
    iDestruct "Hw" as (l ->) "#Hw".
    iInv (ref_shrN .@ l) as (w) "[Hl >Hn]" "Hclose".
    iDestruct "Hn" as %[k ->].
    iDestruct "Hv" as %[n ->].
    wp_faa.
    iMod ("Hclose" with "[Hl]") as %_.
    { iExists #(k + n). iFrame "Hl". by iExists (k + n)%Z. }
    iModIntro. iFrame "HΓ3". by iExists k.
  Qed.
379 380 381 382 383

  Section with_spawn.
    Context `{spawnG Σ}.

    (** Parallel composition properties *)
384 385 386 387 388 389
    Lemma ltyped_par Γ Γ' Γ1 Γ1' Γ2 Γ2' e1 e2 A B :
      env_split Γ Γ1 Γ2 -
      env_split Γ' Γ1' Γ2' -
      (Γ1  e1 : A  Γ1') -
      (Γ2  e2 : B  Γ2') -
      Γ  e1 ||| e2 : A * B  Γ'.
390
    Proof.
391 392 393 394 395 396 397 398 399
      iIntros "#Hsplit #Hsplit' #H1 #H2" (vs) "!> HΓ /=".
      iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
      wp_apply (wp_par with "[HΓ1] [HΓ2]").
      - iApply ("H1" with "HΓ1").
      - iApply ("H2" with "HΓ2").
      - iIntros (v1 v2) "[[HA HΓ1'] [HB HΓ2']]".
        iModIntro. iSplitL "HA HB".
        + iExists v1, v2. iSplit=>//. iFrame "HA HB".
        + iApply "Hsplit'". iFrame "HΓ1' HΓ2'".
400 401 402 403 404 405
    Qed.
  End with_spawn.

  Section with_chan.
    Context `{chanG Σ}.

406 407
    Lemma ltyped_new_chan S :
         new_chan : ()  (chan S * chan (lty_dual S)).
408 409
    Proof.
      iIntros (vs) "!> HΓ /=". iApply wp_value.
410
      iSplitL; last by iApply env_ltyped_empty.
411 412 413
      iIntros "!>" (u) ">->".
      iApply (new_chan_spec with "[//]"); iIntros (c1 c2) "!> [Hp1 Hp2]".
      iExists c1, c2. iSplit=>//. iFrame "Hp1 Hp2".
414 415
    Qed.

416
    Lemma ltyped_send Γ Γ' (x : string) e A S :
417 418
      Γ' !! x = Some (chan (<!!> TY A; S))%lty 
      (Γ  e : A  Γ') -
Robbert Krebbers's avatar
Robbert Krebbers committed
419
      Γ  send x e : ()  <[x:=(chan S)%lty]> Γ'.
420
    Proof.
421
      iIntros (Hx) "#He !>". iIntros (vs) "HΓ"=> /=.
422 423 424
      wp_bind (subst_map vs e).
      iApply (wp_wand with "(He HΓ)"); iIntros (v) "[HA HΓ']".
      iDestruct (env_ltyped_lookup with "HΓ'") as (v' Heq) "[Hc HΓ']".
425
      { by apply Hx. }
426 427 428 429 430
      rewrite Heq.
      wp_send with "[HA //]".
      iSplitR; first done.
      iDestruct (env_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ'")
        as "HΓ'"=> /=.
431
      by rewrite insert_delete (insert_id vs).
432 433
    Qed.

Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
434 435
    Lemma iProto_le_lmsg_texist {kt : ktele Σ} (m : ltys Σ kt  iMsg Σ) :
       (<?> (.. Xs : ltys Σ kt, m Xs)%lmsg)  (<? (Xs : ltys Σ kt)> m Xs).
436
    Proof.
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
437 438 439 440 441 442
      iInduction kt as [|k kt] "IH".
      { rewrite /lty_msg_texist /=. by iExists LTysO. }
      rewrite /lty_msg_texist /=. iIntros (X).
      iApply (iProto_le_trans with "IH"). iIntros (Xs). by iExists (LTysS _ _).
    Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
443
    Lemma ltyped_recv_texist {kt} Γ1 Γ2 (xc : string) (x : binder) (e : expr)
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
444 445 446 447
        (A : ltys Σ kt  ltty Σ) (S : ltys Σ kt  lsty Σ) (B : ltty Σ) :
      ( Ys,
        binder_insert x (A Ys) (<[xc:=(chan (S Ys))%lty]> Γ1)  e : B  Γ2) -
      <[xc:=(chan (<??.. Xs> TY A Xs; S Xs))%lty]> Γ1 
Robbert Krebbers's avatar
Robbert Krebbers committed
448
        (let: x := recv xc in e) : B  binder_delete x Γ2.
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
449 450 451
    Proof.
      iIntros "#He !>". iIntros (vs) "HΓ /=".
      iDestruct (env_ltyped_lookup with "HΓ") as (c Hxc) "[Hc HΓ]".
452
      { by apply lookup_insert. }
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
453 454 455 456 457 458
      rewrite Hxc.
      iAssert (c  <? (Xs : ltys Σ kt) (v : val)>
        MSG v {{  ltty_car (A Xs) v }}; lsty_car (S Xs)) with "[Hc]" as "Hc".
      { iApply (iProto_mapsto_le with "Hc"); iIntros "!>".
        iApply iProto_le_lmsg_texist. }
      wp_recv (Xs v) as "HA". wp_pures.
Robbert Krebbers's avatar
Robbert Krebbers committed
459
      rewrite -subst_map_binder_insert.
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
460 461 462 463 464
      wp_apply (wp_wand with "(He [-]) []").
      { iApply (env_ltyped_insert _ _ x with "HA").
        rewrite delete_insert_delete.
        iEval (rewrite -(insert_id vs xc c) // -(insert_delete Γ1)).
        by iApply (env_ltyped_insert _ _ xc with "[Hc] HΓ"). }
Robbert Krebbers's avatar
Robbert Krebbers committed
465
      iIntros (w) "[$ HΓ]". by destruct x; [|by iApply env_ltyped_delete].
Robbert Krebbers's avatar
Tweaks.  
Robbert Krebbers committed
466
    Qed.
467 468

    Lemma ltyped_recv Γ (x : string) A S :
469 470
      Γ !! x = Some (chan (<??> TY A; S))%lty 
       Γ  recv x : A  <[x:=(chan S)%lty]> Γ.
471
    Proof.
472
      iIntros (Hx) "!>". iIntros (vs) "HΓ"=> /=.
473
      iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".
474
      { by apply Hx. }
475 476 477 478
      rewrite Heq.
      wp_recv (v) as "HA".
      iSplitL "HA"; first done.
      iDestruct (env_ltyped_insert _ _ x (chan _) _ with "[Hc //] HΓ") as "HΓ"=> /=.
479
      by rewrite insert_delete (insert_id vs).
480 481
    Qed.

482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501
    Definition select : val := λ: "c" "i", send "c" "i".
    Lemma ltyped_select Γ (c : string) (i : Z) (S : lsty Σ) Ss :
      Ss !! i = Some S 
       <[c := (chan (lty_select Ss))%lty]>Γ  select c #i : () 
        <[c := (chan S)%lty]>Γ.
    Proof.
      iIntros (Hin).
      iIntros "!>" (vs) "HΓ /=".
      iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".
      { by apply lookup_insert. }
      rewrite Heq /select.
      wp_send with "[]".
      { eauto. }
      iSplitR; first done.
      iDestruct (env_ltyped_insert _ _ c (chan _) with "[Hc //] HΓ")
        as "HΓ'"=> /=.
      rewrite insert_delete insert_insert (insert_id vs)=> //.
      by rewrite lookup_total_alt Hin.
    Qed.

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 532 533 534 535 536 537 538 539 540
    Fixpoint lty_arr_list (As : list (ltty Σ)) (B : ltty Σ) : ltty Σ :=
      match As with
      | [] => B
      | A :: As => A  lty_arr_list As B
      end.

    Lemma lty_arr_list_spec_step A As (e : expr) B ws y i :
      ( v, ltty_car A v -
        WP subst_map (<[y+:+pretty i:=v]> ws)
          (switch_lams y (S i) (length As) e) {{ ltty_car (lty_arr_list As B) }}) -
      WP subst_map ws (switch_lams y i (S (length As)) e)
        {{ ltty_car (lty_arr_list (A :: As) B) }}.
    Proof.
      iIntros "H". wp_pures. iIntros (v) "HA".
      iDestruct ("H" with "HA") as "H".
      rewrite subst_map_insert.
      wp_apply "H".
    Qed.

    Lemma lty_arr_list_spec As (e : expr) B ws y i n :
      n = length As 
      ( vs, ([ list] A;v  As;vs, ltty_car A v) -
            WP subst_map (map_string_seq y i vs  ws) e {{ ltty_car B }}) -
      WP subst_map ws (switch_lams y i n e) {{ ltty_car (lty_arr_list As B) }}.
    Proof.
      iIntros (Hlen) "H".
      iInduction As as [|A As] "IH" forall (ws i e n Hlen); simplify_eq/=.
      - iDestruct ("H" $! [] with "[$]") as "H"=> /=.
        by rewrite left_id_L.
      - iApply lty_arr_list_spec_step. iIntros (v) "HA".
        iApply ("IH" with "[//]"). iIntros (vs) "HAs".
        iSpecialize ("H" $! (v::vs)); simpl.
        do 2 rewrite insert_union_singleton_l.
        rewrite (map_union_comm ({[y +:+ pretty i := v]})); last first.
        { apply map_disjoint_singleton_l_2.
          apply lookup_map_string_seq_None_lt. eauto. }
        rewrite assoc_L. iApply ("H" with "[$HA $HAs]").
    Qed.

Jonas Kastberg's avatar
Jonas Kastberg committed
541 542 543 544 545
    Definition chanbranch (xs : list Z) : val := λ: "c",
      switch_lams "f" 0 (length xs) $
      let: "y" := recv "c" in
      switch_body "y" 0 xs (assert: #false) $ λ i, ("f" +:+ pretty i) "c".

546 547
    Lemma ltyped_chanbranch Ss A xs :
      ( x, x  xs  is_Some (Ss !! x)) 
Robbert Krebbers's avatar
Robbert Krebbers committed
548 549
         chanbranch xs : chan (lty_branch Ss) 
        lty_arr_list ((λ x, (chan (Ss !!! x)  A)%lty) <$> xs) A.
Jonas Kastberg's avatar
Jonas Kastberg committed
550
    Proof.
Jonas Kastberg's avatar
Jonas Kastberg committed
551
      iIntros (Hdom) "!>". iIntros (vs) "Hvs".
552 553 554
      iApply wp_value.
      iSplitL; last by iApply env_ltyped_empty.
      iIntros (c) "Hc". wp_lam.
Jonas Kastberg's avatar
Jonas Kastberg committed
555
      rewrite -subst_map_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
556
      iApply lty_arr_list_spec.
Jonas Kastberg's avatar
Jonas Kastberg committed
557 558 559
      { by rewrite fmap_length. }
      iIntros (ws) "H".
      rewrite big_sepL2_fmap_l.
Jonas Kastberg's avatar
Jonas Kastberg committed
560
      iDestruct (big_sepL2_length with "H") as %Heq.
Robbert Krebbers's avatar
Robbert Krebbers committed
561 562 563
      rewrite -insert_union_singleton_r; last by apply lookup_map_string_seq_None.
      rewrite /= lookup_insert.
      wp_recv (x) as "HPsx". iDestruct "HPsx" as %HPs_Some.
Jonas Kastberg's avatar
Jonas Kastberg committed
564 565
      wp_pures.
      rewrite -subst_map_insert.
Robbert Krebbers's avatar
Robbert Krebbers committed
566 567 568 569 570 571
      assert (x  xs) as Hin by naive_solver.
      pose proof (list_find_elem_of (x =.) xs x) as [[n z] Hfind_Some]; [done..|].
      iApply switch_body_spec.
      { apply fmap_Some_2, Hfind_Some. }
      { by rewrite lookup_insert. }
      simplify_map_eq. rewrite lookup_map_string_seq_Some.
Jonas Kastberg's avatar
Jonas Kastberg committed
572
      assert (xs !! n = Some x) as Hxs_Some.
Robbert Krebbers's avatar
Robbert Krebbers committed
573 574 575 576 577
      { by apply list_find_Some in Hfind_Some as [? [-> _]]. }
      assert (is_Some (ws !! n)) as [w Hws_Some].
      { apply lookup_lt_is_Some_2. rewrite -Heq. eauto using lookup_lt_Some. }
      iDestruct (big_sepL2_lookup _ xs ws n with "H") as "HA"; [done..|].
      rewrite Hws_Some. by iApply "HA".
Jonas Kastberg's avatar
Jonas Kastberg committed
578
    Qed.
579 580
  End with_chan.
End properties.