Separate file for session typing rules.

_CoqProject

@@ -35,6 +35,7 @@ theories/logrel/operators.v
 theories/logrel/term_typing_judgment.v
 theories/logrel/subtyping_rules.v
 theories/logrel/term_typing_rules.v
+theories/logrel/session_typing_rules.v
 theories/logrel/lib/mutex.v
 theories/logrel/lib/par_start.v
 theories/logrel/examples/double.v

theories/logrel/examples/mapper.v

-From actris.logrel Require Import subtyping_rules term_typing_rules.
+From actris.logrel Require Import term_typing_rules session_typing_rules.
 From actris.channel Require Import proofmode.
 
 Section mapper_example.

theories/logrel/examples/pair.v

@@ -7,7 +7,7 @@ can be assigned the type
   chan (?int.?int.end) ⊸ (int * int)
 
 by exclusively using the semantic typing rules. *)
-From actris.logrel Require Export term_typing_rules.
+From actris.logrel Require Export term_typing_rules session_typing_rules.
 From iris.proofmode Require Import tactics.
 
 Definition prog : expr := λ: "c", (recv "c", recv "c").

theories/logrel/lib/par_start.v

-From actris.logrel Require Export term_typing_rules.
+From actris.logrel Require Export term_typing_rules session_typing_rules.
 From actris.channel Require Import proofmode.
 
 Definition par_start : expr := λ: "e1" "e2",

theories/logrel/term_typing_rules.v

 (** This file defines all of the semantic typing lemmas for term types. Most of
 these lemmas are semantic versions of the syntactic typing judgments typically
 found in a syntactic type system. *)
-From stdpp Require Import pretty.
 From iris.bi.lib Require Import core.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import metatheory.
-From iris.heap_lang.lib Require Export spawn par assert.
+From iris.heap_lang.lib Require Export par.
 From actris.logrel Require Export subtyping_rules term_typing_judgment operators.
-From actris.utils Require Import switch.
 From actris.channel Require Import proofmode.
 
-Section properties.
+Section term_typing_rules.
   Context `{heapG Σ}.
   Implicit Types A B : ltty Σ.
-  Implicit Types S T : lsty Σ.
   Implicit Types Γ : env Σ.
 
   (** Frame rule *)
@@ -406,171 +403,4 @@ Section properties.
     + iExists v1, v2. by iFrame.
     + iApply env_ltyped_app. by iFrame.
   Qed.
-
-  (** Channel properties *)
-  Section with_chan.
-    Context `{chanG Σ}.
-
-    Lemma ltyped_new_chan Γ S :
-      ⊢ Γ ⊨ new_chan : () ⊸ (chan S * chan (lty_dual S)) ⫤ Γ.
-    Proof.
-      iIntros (vs) "!> HΓ /=". iApply wp_value. iFrame "HΓ".
-      iIntros (u) ">->".
-      iApply (new_chan_spec with "[//]"); iIntros (c1 c2) "!> [Hp1 Hp2]".
-      iExists c1, c2. by iFrame "Hp1 Hp2".
-    Qed.
-
-    Lemma ltyped_send Γ Γ' (x : string) e A S :
-      env_filter_eq x Γ' = [EnvItem x (chan (<!!> TY A; S))] →
-      (Γ ⊨ e : A ⫤ Γ') -∗
-      Γ ⊨ send x e : () ⫤ env_cons x (chan S) Γ'.
-    Proof.
-      iIntros (HΓx%env_filter_eq_perm') "#He !>". iIntros (vs) "HΓ /=".
-      wp_apply (wp_wand with "(He HΓ)"); iIntros (v) "[HA HΓ']".
-      rewrite {2}HΓx /=.
-      iDestruct (env_ltyped_cons with "HΓ'") as (c Hvs) "[Hc HΓ']". rewrite Hvs.
-      wp_send with "[HA //]". iSplitR; [done|].
-      iDestruct (env_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ'") as "HΓ' /=".
-      by rewrite  (insert_id vs).
-   Qed.
-
-    Lemma iProto_le_lmsg_texist {kt : ktele Σ} (m : ltys Σ kt → iMsg Σ) :
-      ⊢ (<?> (∃.. Xs : ltys Σ kt, m Xs)%lmsg) ⊑ (<? (Xs : ltys Σ kt)> m Xs).
-    Proof.
-      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.
-
-    Lemma ltyped_recv_texist {kt} Γ1 Γ2 M x (xc : string) (e : expr)
-        (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) (B : ltty Σ) :
-      env_filter_eq xc Γ1 = [EnvItem xc (chan (<??> M))] →
-      LtyMsgTele M A S →
-      (∀ Ys,
-        env_cons x (ktele_app A Ys) (env_cons xc (chan (ktele_app S Ys)) Γ1) ⊨ e : B ⫤ Γ2) -∗
-      Γ1 ⊨ (let: x := recv xc in e) : B ⫤
-            env_filter_eq x (env_filter_ne xc Γ1) ++ env_filter_ne x Γ2.
-    Proof.
-      rewrite /LtyMsgTele.
-      iIntros (HΓxc%env_filter_eq_perm' HM) "#He !>". iIntros (vs) "HΓ1 /=".
-      rewrite {2}HΓxc /=.
-      iDestruct (env_ltyped_cons with "HΓ1") as (c Hvs) "[Hc HΓ1]". rewrite Hvs.
-      rewrite {2}(env_filter_eq_perm (env_filter_ne xc Γ1) x).
-      iDestruct (env_ltyped_app with "HΓ1") as "[HΓ1eq HΓ1neq]".
-      iAssert (c ↣ <? (Xs : ltys Σ kt) (v : val)>
-        MSG v {{ ltty_car (ktele_app A Xs) v }};
-          lsty_car (ktele_app S Xs)) with "[Hc]" as "Hc".
-      { iApply (iProto_mapsto_le with "Hc"); iIntros "!>". rewrite HM.
-        iApply iProto_le_lmsg_texist. }
-      wp_recv (Xs v) as "HA". wp_pures. rewrite -subst_map_binder_insert.
-      wp_apply (wp_wand with "(He [- HΓ1eq])").
-      { iApply (env_ltyped_insert _ _ x with "HA").
-        destruct (decide (x = xc)) as [->|].
-        - by rewrite env_filter_ne_cons.
-        - rewrite env_filter_ne_cons_ne //.
-          iApply env_ltyped_cons. eauto with iFrame. }
-      iIntros (w) "[$ HΓ]".
-      iApply env_ltyped_app. iFrame "HΓ1eq". by iApply env_ltyped_delete.
-    Qed.
-
-    Lemma ltyped_recv Γ (x : string) A S :
-      env_filter_eq x Γ = [EnvItem x (chan (<??> TY A; S))] →
-      ⊢ Γ ⊨ recv x : A ⫤ env_cons x (chan S) Γ.
-    Proof.
-      iIntros (HΓx%env_filter_eq_perm') "!>". iIntros (vs) "HΓ /=".
-      rewrite {1}HΓx /=.
-      iDestruct (env_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs.
-      wp_recv (v) as "HA". iFrame "HA". iApply env_ltyped_cons; eauto with iFrame.
-    Qed.
-
-    Definition select : val := λ: "c" "i", send "c" "i".
-
-    Lemma ltyped_select Γ (x : string) (i : Z) (S : lsty Σ) Ss :
-      Ss !! i = Some S →
-      env_filter_eq x Γ = [EnvItem x (chan (lty_select Ss))] →
-      ⊢ Γ ⊨ select x #i : () ⫤ env_cons x (chan S) Γ.
-    Proof.
-      iIntros (Hin HΓx%env_filter_eq_perm'); iIntros "!>" (vs) "HΓ /=".
-      rewrite {1}HΓx /=.
-      iDestruct (env_ltyped_cons with "HΓ") as (c Hvs) "[Hc HΓ]". rewrite Hvs.
-      rewrite /select. wp_send with "[]"; [by eauto|]. iSplit; [done|].
-      iDestruct (env_ltyped_insert _ _ x (chan _) with "[Hc //] HΓ") as "HΓ' /=".
-      by rewrite insert_id // lookup_total_alt Hin.
-    Qed.
-
-    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.
-
-    Definition branch (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".
-
-    Lemma ltyped_branch Γ Ss A xs :
-      (∀ x, x ∈ xs ↔ is_Some (Ss !! x)) →
-      ⊢ Γ ⊨ branch xs : chan (lty_branch Ss) ⊸
-        lty_arr_list ((λ x, (chan (Ss !!! x) ⊸ A)%lty) <$> xs) A ⫤ Γ.
-    Proof.
-      iIntros (Hdom) "!>". iIntros (vs) "$". iApply wp_value.
-      iIntros (c) "Hc". wp_lam.
-      rewrite -subst_map_singleton.
-      iApply lty_arr_list_spec; [by rewrite fmap_length|].
-      iIntros (ws) "H".
-      rewrite big_sepL2_fmap_l.
-      iDestruct (big_sepL2_length with "H") as %Heq.
-      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.
-      wp_pures. rewrite -subst_map_insert.
-      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.
-      assert (xs !! n = Some x) as Hxs_Some.
-      { 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".
-    Qed.
-  End with_chan.
-End properties.
+End term_typing_rules.