Reverted definition of LTyCopy to simply be the Persistent property.

Added LTyCopy typeclasses for products and sums
Removed mutable ref to weak ref subtyping as a consequence.

_CoqProject

@@ -16,3 +16,9 @@ theories/examples/sort_br_del.v
 theories/examples/sort_fg.v
 theories/examples/map.v
 theories/examples/map_reduce.v
+theories/logrel/ltyping.v
+theories/logrel/lsty.v
+theories/logrel/session_types.v
+theories/logrel/types.v
+theories/logrel/subtyping.v
+theories/logrel/examples/double.v

theories/logrel/examples/double.v

+From iris.heap_lang Require Export lifting metatheory.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Import notation proofmode lib.par lib.spin_lock.
+From iris.algebra Require Import agree frac csum excl frac_auth.
+From actris.channel Require Import channel proto proofmode.
+From actris.logrel Require Export types subtyping.
+
+Definition prog : val := λ: "c",
+  let: "lock" := newlock #() in
+  let: "p" := (
+    acquire "lock";;
+    let: "x1" := recv "c" in
+    release "lock";;
+    "x1"
+  ) ||| (
+    acquire "lock";;
+    let: "x2" := recv "c" in
+    release "lock";;
+    "x2"
+  ) in "p".
+
+Section GhostState.
+  Class fracG Σ := { frac_inG :> inG Σ fracR }.
+  Definition fracΣ : gFunctors := #[GFunctor fracR].
+  Instance subG_fracΣ {Σ} : subG fracΣ Σ → fracG Σ.
+  Proof. solve_inG. Qed.
+End GhostState.
+
+Section Double.
+  Context `{heapG Σ, chanG Σ, fracG Σ, spawnG Σ}.
+
+  Definition prog_prot : iProto Σ :=
+    (<?> (x : Z), MSG #x; <?> (y : Z), MSG #y; END)%proto.
+
+  Definition chan_inv (c : val) (γ : gname) : iProp Σ :=
+    ((c ↣ prog_prot) ∨
+     (own γ (1/2)%Qp ∗ c ↣ (<?> (x : Z), MSG #x; END)%proto) ∨
+     (own γ 1%Qp ∗ c ↣ END))%I.
+
+  Lemma wp_prog (c : val):
+    {{{ ▷ (c ↣ prog_prot) }}}
+      prog c
+    {{{ v, RET v; ∃ k1 k2 : Z, ⌜v = (#k1, #k2)%V⌝ }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ".
+    rewrite /prog.
+    iMod (own_alloc 1%Qp) as (γ) "[Hcredit1 Hcredit2]".
+    { done. }
+    (* Create lock *)
+    wp_apply (newlock_spec (chan_inv c γ) with "[Hc]").
+    { iLeft. iFrame "Hc". }
+    iIntros (lk γlk) "#Hlock".
+    wp_pures.
+    (* Fork into two threads *)
+    wp_bind (par _ _).
+    wp_apply (wp_par (λ v, ∃ k : Z, ⌜v = #k⌝)%I (λ v, ∃ k : Z, ⌜v = #k⌝)%I
+                with "[Hcredit1] [Hcredit2]").
+    - (* Acquire lock *)
+      wp_apply (acquire_spec with "Hlock").
+      iIntros "[Hlocked Hc]". wp_pures.
+      iDestruct "Hc" as "[Hc|[Hc|Hc]]".
+      + wp_recv (x1) as "_". wp_pures.
+        wp_apply (release_spec with "[Hlocked Hcredit1 Hc]").
+        { iFrame "Hlock Hlocked". iRight. iLeft. iFrame "Hcredit1 Hc". }
+        iIntros "_". wp_pures.
+        eauto.
+      + iDestruct "Hc" as "[Hcredit2 Hc]".
+        wp_recv (x1) as "_". wp_pures.
+        iCombine "Hcredit1 Hcredit2" as "Hcredit".
+        wp_apply (release_spec with "[Hlocked Hcredit Hc]").
+        { iFrame "Hlock Hlocked". iRight. iRight. iFrame "Hcredit Hc". }
+        iIntros "_". wp_pures.
+        eauto.
+      + iDestruct "Hc" as "[Hcredit2 Hc]".
+        iExFalso. iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as "%".
+        done.
+    - (* Acquire lock *)
+      wp_apply (acquire_spec with "Hlock").
+      iIntros "[Hlocked Hc]". wp_pures.
+      iDestruct "Hc" as "[Hc|[Hc|Hc]]".
+      + wp_recv (x1) as "_". wp_pures.
+        wp_apply (release_spec with "[Hlocked Hcredit2 Hc]").
+        { iFrame "Hlock Hlocked". iRight. iLeft. iFrame "Hcredit2 Hc". }
+        iIntros "_". wp_pures.
+        eauto.
+      + iDestruct "Hc" as "[Hcredit1 Hc]".
+        wp_recv (x1) as "Hx1". wp_pures.
+        iCombine "Hcredit1 Hcredit2" as "Hcredit".
+        wp_apply (release_spec with "[Hlocked Hcredit Hc]").
+        { iFrame "Hlock Hlocked". iRight. iRight. iFrame "Hcredit Hc". }
+        iIntros "_". wp_pures.
+        eauto.
+      + iDestruct "Hc" as "[Hcredit1 Hc]".
+        iExFalso. iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as "%".
+        done.
+    - iIntros (x1 x2) "[Hx1 Hx2]".
+      iModIntro. wp_pures.
+      iApply "HΦ".
+      iDestruct "Hx1" as (k1) "->".
+      iDestruct "Hx2" as (k2) "->".
+      by iExists k1, k2.
+  Qed.
+
+  Lemma prog_typed :
+    ⊢ (∅ ⊨ prog : chan (<??> lty_int; <??> lty_int; END) ⊸ (lty_int * lty_int))%I.
+  Proof.
+    iIntros (vs) "!> HΓ /=".
+    iApply wp_value.
+    iIntros (c) "Hc".
+    iApply (wp_prog with "[Hc]")=> //=.
+    {
+      iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%lsty with "Hc").
+      iApply iProto_le_recv.
+      iIntros "!> !>" (v) ">H !>".
+      iDestruct "H" as (x) "->"=> /=.
+      iExists _. do 2 iSplit=> //.
+      iApply iProto_le_recv.
+      iIntros "!>" (v) ">H !>".
+      iDestruct "H" as (y) "->"=> /=.
+      iExists _. do 2 iSplit=> //.
+      iApply iProto_le_refl.
+    }
+    iIntros "!>" (v) "H".
+    iDestruct "H" as (k1 k2) "->".
+    iExists _, _. iSplit=> //. eauto.
+  Qed.
+
+End Double.

theories/logrel/lsty.v

+From actris.logrel Require Export ltyping.
+From iris.heap_lang Require Export lifting metatheory.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Import notation proofmode.
+From actris.channel Require Import proto proofmode.
+
+Record lsty Σ := Lsty {
+  lsty_car :> iProto Σ;
+}.
+Arguments Lsty {_} _%proto.
+Arguments lsty_car {_} _ : simpl never.
+Bind Scope lsty_scope with lsty.
+Delimit Scope lsty_scope with lsty.
+
+Section lsty_ofe.
+  Context `{Σ : gFunctors}.
+
+  Instance lsty_equiv : Equiv (lsty Σ) :=
+    λ P Q, lsty_car P ≡ lsty_car Q.
+  Instance lsty_dist : Dist (lsty Σ) :=
+    λ n P Q, lsty_car P ≡{n}≡ lsty_car Q.
+
+  Lemma lsty_ofe_mixin : OfeMixin (lsty Σ).
+  Proof. by apply (iso_ofe_mixin (lsty_car : _ → iProto _)). Qed.
+  Canonical Structure lstyO := OfeT (lsty Σ) lsty_ofe_mixin.
+
+  Global Instance lsty_cofe : Cofe lstyO.
+  Proof. by apply (iso_cofe (@Lsty _ : _ → lstyO) lsty_car). Qed.
+
+  Global Instance lsty_inhabited : Inhabited (lsty Σ) :=
+    populate (Lsty inhabitant).
+
+  Global Instance lsty_car_ne : NonExpansive lsty_car.
+  Proof. intros n A A' H. exact H. Qed.
+
+  Global Instance lsty_car_proper : Proper ((≡) ==> (≡)) lsty_car.
+  Proof. intros A A' H. exact H. Qed.
+
+  Global Instance Lsty_ne : NonExpansive Lsty.
+  Proof. solve_proper. Qed.
+
+  Global Instance Lsty_proper : Proper ((≡) ==> (≡)) Lsty.
+  Proof. solve_proper. Qed.
+End lsty_ofe.
+
+Arguments lstyO : clear implicits.

theories/logrel/ltyping.v

+From iris.heap_lang Require Export lifting metatheory.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Import adequacy notation proofmode.
+
+(* The domain of semantic types: Iris predicates over values *)
+Record lty Σ := Lty {
+  lty_car :> val → iProp Σ;
+}.
+Arguments Lty {_} _%I.
+Arguments lty_car {_} _ _ : simpl never.
+Bind Scope lty_scope with lty.
+Delimit Scope lty_scope with lty.
+
+(* The COFE structure on semantic types *)
+Section lty_ofe.
+  Context `{Σ : gFunctors}.
+
+  (* Equality of semantic types is extensional equality *)
+  Instance lty_equiv : Equiv (lty Σ) := λ A B, ∀ w, A w ≡ B w.
+  Instance lty_dist : Dist (lty Σ) := λ n A B, ∀ w, A w ≡{n}≡ B w.
+
+  (* OFE and COFE structure is taken from isomorphism with val -d> iProp Σ *)
+  Lemma lty_ofe_mixin : OfeMixin (lty Σ).
+  Proof. by apply (iso_ofe_mixin (lty_car : _ → val -d> _)). Qed.
+  Canonical Structure ltyO := OfeT (lty Σ) lty_ofe_mixin.
+
+  Global Instance lty_cofe : Cofe ltyO.
+  Proof. by apply (iso_cofe (@Lty _ : (val -d> _) → ltyO) lty_car). Qed.
+
+  Global Instance lty_inhabited : Inhabited (lty Σ) := populate (Lty inhabitant).
+
+  Global Instance lty_car_ne n : Proper (dist n ==> (=) ==> dist n) lty_car.
+  Proof. by intros A A' ? w ? <-. Qed.
+  Global Instance lty_car_proper : Proper ((≡) ==> (=) ==> (≡)) lty_car.
+  Proof. by intros A A' ? w ? <-. Qed.
+
+  Global Instance lty_ne n : Proper (pointwise_relation _ (dist n) ==> dist n) Lty.
+  Proof. by intros ???. Qed.
+  Global Instance lty_proper : Proper (pointwise_relation _ (≡) ==> (≡)) Lty.
+  Proof. by intros ???. Qed.
+End lty_ofe.
+
+Arguments ltyO : clear implicits.
+
+(* Typing for operators *)
+Class LTyUnboxed {Σ} (A : lty Σ) :=
+  lty_unboxed v : A v -∗ ⌜ val_is_unboxed v ⌝.
+
+Class LTyUnOp {Σ} (op : un_op) (A B : lty Σ) :=
+  lty_un_op v : A v -∗ ∃ w, ⌜ un_op_eval op v = Some w ⌝ ∗ B w.
+
+Class LTyBinOp {Σ} (op : bin_op) (A1 A2 B : lty Σ) :=
+  lty_bin_op v1 v2 : A1 v1 -∗ A2 v2 -∗ ∃ w, ⌜ bin_op_eval op v1 v2 = Some w ⌝ ∗ B w.
+
+(* Copy types *)
+Class LTyCopy `{invG Σ} (A : lty Σ) :=
+  lty_copy_pers v :> Persistent (A v).
+
+Section Environment.
+  Context `{invG Σ}.
+  Implicit Types A : lty Σ.
+
+  Definition env_ltyped (Γ : gmap string (lty Σ))
+             (vs : gmap string val) : iProp Σ :=
+    ([∗ map] i ↦ A ∈ Γ, ∃ v, ⌜vs !! i = Some v⌝ ∗ lty_car A v)%I.
+
+  Lemma env_ltyped_lookup Γ vs x A :
+    Γ !! x = Some A →
+    env_ltyped Γ vs -∗ ∃ v, ⌜ vs !! x = Some v ⌝ ∗ A v.
+  Proof.
+    iIntros (HΓx) "HΓ".
+    iPoseProof (big_sepM_lookup with "HΓ") as "H"; eauto.
+  Qed.
+
+  Lemma env_ltyped_insert Γ vs x A v :
+    A v -∗ env_ltyped Γ vs -∗
+    env_ltyped (binder_insert x A Γ) (binder_insert x v vs).
+  Proof.
+    destruct x as [|x]=> /=; first by auto.
+    iIntros "HA HΓ".
+    rewrite /env_ltyped.
+    set Γ' := <[x:=A]> Γ.
+    assert (Hx: Γ' !! x = Some A).
+    { apply lookup_insert. }
+    iApply (big_sepM_delete _ _ _ _ Hx).
+    iSplitL "HA".
+    { iExists v. rewrite lookup_insert. auto. }
+    assert (Hsub: delete x Γ' ⊆ Γ).
+    { rewrite delete_insert_delete. apply delete_subseteq. }
+    iPoseProof (big_sepM_subseteq _ _ _ Hsub with "HΓ") as "HΓ".
+    iApply (big_sepM_mono with "HΓ"). simpl.
+    iIntros (y B Hy) "HB".
+    iDestruct "HB" as (w Hw) "HB".
+    iExists w. iFrame. iPureIntro.
+    apply lookup_delete_Some in Hy.
+    destruct Hy as [Hxy _].
+    by rewrite -Hw lookup_insert_ne.
+  Qed.
+
+  Definition env_split (Γ Γ1 Γ2 : gmap string (lty Σ)) : iProp Σ :=
+    □ ∀ vs, env_ltyped Γ vs -∗ env_ltyped Γ1 vs ∗ env_ltyped Γ2 vs.
+
+  Lemma env_split_empty : ⊢ env_split ∅ ∅ ∅.
+  Proof. iIntros (vs) "!> HΓ". rewrite /env_ltyped. auto. Qed.
+
+  Lemma env_split_left Γ Γ1 Γ2 x A:
+    Γ !! x = None →
+    env_split Γ Γ1 Γ2 -∗
+    env_split (<[x := A]> Γ) (<[x := A]> Γ1) Γ2.
+  Proof.
+    iIntros (HΓx) "#Hsplit". iIntros (v) "!> HΓ".
+    iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption.
+    iDestruct ("Hsplit" with "HΓ") as "[HΓ1 $]".
+    iApply (big_sepM_insert_2 with "[Hv]"); simpl; eauto.
+  Qed.
+
+  Lemma env_split_comm Γ Γ1 Γ2:
+    env_split Γ Γ1 Γ2 -∗ env_split Γ Γ2 Γ1.
+  Proof.
+    iIntros "#Hsplit" (vs) "!> HΓ".
+    by iDestruct ("Hsplit" with "HΓ") as "[$ $]".
+  Qed.
+
+  Lemma env_split_right Γ Γ1 Γ2 x A:
+    Γ !! x = None →
+    env_split Γ Γ1 Γ2 -∗
+    env_split (<[x := A]> Γ) Γ1 (<[x := A]> Γ2).
+  Proof.
+    iIntros (HΓx) "Hsplit".
+    iApply env_split_comm. iApply env_split_left; first by assumption.
+    by iApply env_split_comm.
+  Qed.
+
+  (* TODO: Get rid of side condition that x does not appear in Γ *)
+  Lemma env_split_copy Γ Γ1 Γ2 (x : string) A:
+    Γ !! x = None →
+    LTyCopy A →
+    env_split Γ Γ1 Γ2 -∗
+    env_split (<[x:=A]> Γ) (<[x:=A]> Γ1) (<[x:=A]> Γ2).
+  Proof.
+    iIntros (Hcopy HΓx) "#Hsplit". iIntros (vs) "!> HΓ".
+    iPoseProof (big_sepM_insert with "HΓ") as "[Hv HΓ]"; first by assumption.
+    iDestruct "Hv" as (v ?) "#HAv".
+    iDestruct ("Hsplit" with "HΓ") as "[HΓ1 HΓ2]".
+    iSplitL "HΓ1"; iApply big_sepM_insert_2; simpl; eauto.
+  Qed.
+
+  (* TODO: Prove lemmas about this *)
+  Definition env_copy (Γ Γ' : gmap string (lty Σ)) : iProp Σ :=
+    □ ∀ vs, env_ltyped Γ vs -∗ □ env_ltyped Γ' vs.
+
+  Lemma env_copy_empty : ⊢ env_copy ∅ ∅.
+  Proof. iIntros (vs) "!> _ !> ". by rewrite /env_ltyped. Qed.
+
+  Lemma env_copy_extend x A Γ Γ' :
+    Γ !! x = None →
+    env_copy Γ Γ' -∗
+    env_copy (<[x:=A]> Γ) Γ'.
+  Proof.
+    iIntros (HΓ) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
+    iDestruct (big_sepM_insert with "Hvs") as "[_ Hvs]"; first by assumption.
+    iApply ("Hcopy" with "Hvs").
+  Qed.
+
+  Lemma env_copy_extend_copy x A Γ Γ' :
+    Γ !! x = None →
+    Γ' !! x = None →
+    LTyCopy A →
+    env_copy Γ Γ' -∗
+    env_copy (<[x:=A]> Γ) (<[x:=A]> Γ').
+  Proof.
+    iIntros (HΓx HΓ'x HcopyA) "#Hcopy". iIntros (vs) "!> Hvs". rewrite /env_ltyped.
+    iDestruct (big_sepM_insert with "Hvs") as "[HA Hvs]"; first done.
+    iDestruct ("Hcopy" with "Hvs") as "#Hvs'".
+    iDestruct "HA" as (v ?) "#HA".
+    iIntros "!>". iApply big_sepM_insert; first done. iSplitL; eauto.
+  Qed.
+End Environment.
+
+(* The semantic typing judgement *)
+Definition ltyped `{!heapG Σ}
+    (Γ : gmap string (lty Σ)) (e : expr) (A : lty Σ) : iProp Σ :=
+  □ ∀ vs, env_ltyped Γ vs -∗ WP subst_map vs e {{ A }}.
+
+Notation "Γ ⊨ e : A" := (ltyped Γ e A)
+  (at level 100, e at next level, A at level 200).
+
+Lemma ltyped_safety `{heapPreG Σ} e σ es σ' e' :
+  (∀ `{heapG Σ}, ∃ A, ⊢ ∅ ⊨ e : A) →
+  rtc erased_step ([e], σ) (es, σ') → e' ∈ es →
+  is_Some (to_val e') ∨ reducible e' σ'.
+Proof.
+  intros Hty. apply (heap_adequacy Σ NotStuck e σ (λ _, True))=> // ?.
+  destruct (Hty _) as [A He]. iStartProof.
+  iDestruct (He) as "He".
+  iSpecialize ("He" $!∅).
+  iSpecialize ("He" with "[]"); first by rewrite /env_ltyped.
+  iEval (rewrite -(subst_map_empty e)). iApply (wp_wand with "He"); auto.
+Qed.

theories/logrel/session_types.v

+From actris.logrel Require Export ltyping lsty.
+From iris.heap_lang Require Export lifting metatheory.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Import notation proofmode.
+From actris.channel Require Import proto proofmode.
+
+Section protocols.
+  Context `{heapG Σ, protoG Σ}.
+
+  Definition lsty_end : lsty Σ := Lsty END.
+
+  Definition lsty_send (A : lty Σ) (P : lsty Σ) : lsty Σ :=
+    Lsty (<!> v, MSG v {{ A v }}; lsty_car P).
+  Definition lsty_recv (A : lty Σ) (P : lsty Σ) : lsty Σ :=
+    Lsty (<?> v, MSG v {{ A v }}; lsty_car P).
+
+  Definition lsty_branch (P1 P2 : lsty Σ) : lsty Σ :=
+    Lsty (P1 <&> P2).
+  Definition lsty_select (P1 P2 : lsty Σ) : lsty Σ :=
+    Lsty (P1 <+> P2).
+
+  Definition lsty_rec1 (C : lsty Σ → lsty Σ)
+             `{!Contractive C}
+             (rec : lsty Σ) : lsty Σ :=
+    Lsty (C rec).
+
+  Instance lsty_rec1_contractive C `{!Contractive C} : Contractive (lsty_rec1 C).
+  Proof. solve_contractive. Qed.
+
+  Definition lsty_rec (C : lsty Σ → lsty Σ) `{!Contractive C} : lsty Σ :=
+    fixpoint (lsty_rec1 C).
+
+  Definition lsty_dual (P : lsty Σ) : lsty Σ :=
+    Lsty (iProto_dual P).
+
+  Definition lsty_app (P1 P2 : lsty Σ) : lsty Σ :=
+    Lsty (iProto_app P1 P2).
+
+End protocols.
+
+Section Propers.
+  Context `{heapG Σ, protoG Σ}.
+
+  Global Instance lsty_send_ne : NonExpansive2 (@lsty_send Σ).
+  Proof.
+    intros n A A' H1 P P' H2.
+    rewrite /lsty_send.
+    apply Lsty_ne.
+    apply iProto_message_ne; simpl; try done.
+  Qed.
+
+  Global Instance lsty_send_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_send Σ).
+  Proof.
+    intros A A' H1 P P' H2.
+    rewrite /lsty_send.
+    apply Lsty_ne.
+    apply iProto_message_contractive; simpl; try done.
+    intros v.
+    destruct n as [|n]; try done.
+    apply H1.
+  Qed.
+
+  Global Instance lsty_recv_ne : NonExpansive2 (@lsty_recv Σ).
+  Proof.
+    intros n A A' H1 P P' H2.
+    rewrite /lsty_recv.
+    apply Lsty_ne.
+    apply iProto_message_ne; simpl; try done.
+  Qed.
+
+  Global Instance lsty_recv_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_recv Σ).
+  Proof.
+    intros A A' H1 P P' H2.
+    rewrite /lsty_recv.
+    apply Lsty_ne.
+    apply iProto_message_contractive; simpl; try done.
+    intros v.
+    destruct n as [|n]; try done.
+    apply H1.
+  Qed.
+
+  Global Instance lsty_branch_ne : NonExpansive2 (@lsty_branch Σ).
+  Proof.
+    intros n A A' H1 P P' H2.
+    rewrite /lsty_branch.
+    apply Lsty_ne.
+    apply iProto_message_ne; simpl; try done.
+    intros v. destruct v; done.
+  Qed.
+
+  Global Instance lsty_branch_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_branch Σ).
+  Proof.
+    intros A A' H1 P P' H2.
+    rewrite /lsty_branch.
+    apply Lsty_ne.
+    apply iProto_message_contractive; simpl; try done.
+    intros v.
+    destruct v; destruct n as [|n]; try done.
+  Qed.
+
+  Global Instance lsty_select_ne : NonExpansive2 (@lsty_select Σ).
+  Proof.
+    intros n A A' H1 P P' H2.
+    rewrite /lsty_select.
+    apply Lsty_ne.
+    apply iProto_message_ne; simpl; try done.
+    intros v. destruct v; done.
+  Qed.
+
+  Global Instance lsty_select_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lsty_select Σ).
+  Proof.
+    intros A A' H1 P P' H2.
+    rewrite /lsty_select.
+    apply Lsty_ne.
+    apply iProto_message_contractive; simpl; try done.
+    intros v.
+    destruct v; destruct n as [|n]; try done.
+  Qed.
+
+  Global Instance lsty_dual_ne : NonExpansive (@lsty_dual Σ).
+  Proof.
+    intros n P P' HP.
+    rewrite /lsty_dual.
+    apply Lsty_ne.
+    by apply iProto_dual_ne.
+  Qed.
+
+  Global Instance lsty_app_ne : NonExpansive2 (@lsty_app Σ).
+  Proof.
+    intros n P1 P1' H1 P2 P2' H2.
+    rewrite /lsty_app.
+    apply Lsty_ne.
+    by apply iProto_app_ne.
+  Qed.
+
+End Propers.
+
+Notation "'END'" := lsty_end : lsty_scope.
+Notation "<!!> A ; P" :=
+  (lsty_send A P) (at level 20, A, P at level 200) : lsty_scope.
+Notation "<??> A ; P" :=
+  (lsty_recv A P) (at level 20, A, P at level 200) : lsty_scope.
+Infix "<+++>" := lsty_select (at level 60) : lsty_scope.
+Infix "<&&&>" := lsty_branch (at level 85) : lsty_scope.
+Infix "<++++>" := lsty_app (at level 60) : lsty_scope.

theories/logrel/subtyping.v

+From actris.logrel Require Import types.
+From actris.channel Require Import channel.
+From iris.base_logic.lib Require Import invariants.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode.
+
+Definition lty_le {Σ} (A1 A2 : lty Σ) : iProp Σ :=
+  □ ∀ v, (A1 v -∗ A2 v).
+
+Arguments lty_le {_} _%lty _%lty.
+Infix "<:" := lty_le (at level 70).
+Instance: Params (@lty_le) 1 := {}.
+
+Instance lty_le_ne {Σ} : NonExpansive2 (@lty_le Σ).
+Proof. solve_proper. Qed.
+Instance lty_le_proper {Σ} :
+  Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ).
+Proof. solve_proper. Qed.
+
+Definition lsty_le {Σ} (P1 P2 : lsty Σ) : iProp Σ :=
+  □ (iProto_le P1 P2).
+
+Arguments lsty_le {_} _%lsty _%lsty.
+Infix "<p:" := lsty_le (at level 70).
+Instance: Params (@lsty_le) 1 := {}.
+
+Instance lsty_le_ne {Σ} : NonExpansive2 (@lsty_le Σ).
+Proof. solve_proper_prepare. f_equiv. solve_proper. Qed.
+Instance lsty_le_proper {Σ} :
+  Proper ((≡) ==> (≡) ==> (≡)) (@lsty_le Σ).
+Proof. apply ne_proper_2. apply _. Qed.
+
+Section subtype.
+  Context `{heapG Σ, chanG Σ}.
+  Implicit Types A : lty Σ.
+  Implicit Types P : lsty Σ.
+
+  Lemma lty_le_refl A : ⊢ A <: A.
+  Proof. by iIntros (v) "!> H". Qed.
+
+  Lemma lty_le_trans A1 A2 A3 : A1 <: A2 -∗ A2 <: A3 -∗ A1 <: A3.
+  Proof. iIntros "#H1 #H2" (v) "!> H". iApply "H2". by iApply "H1". Qed.
+
+  Lemma lty_le_copy A : ⊢ copy A <: A.
+  Proof. by iIntros (v) "!> #H". Qed.
+
+  Lemma lty_le_copyable A `{LTyCopy Σ A} : ⊢ A <: copy A.
+  Proof. by iIntros (v) "!> #H". Qed.
+
+  Lemma lty_arr_le A11 A12 A21 A22 :
+    ▷ (A21 <: A11) -∗ ▷ (A12 <: A22) -∗
+    (A11 ⊸ A12) <: (A21 ⊸ A22).
+  Proof.
+    iIntros "#H1 #H2" (v) "!> H". iIntros (w) "H'".
+    iApply (wp_step_fupd); first done.
+    { iIntros "!>!>!>". iExact "H2". }
+    iApply (wp_wand with "(H (H1 H'))"). iIntros (v') "H Hle !>".
+    by iApply "Hle".
+  Qed.
+
+  Lemma lty_arr_copy_le A11 A12 A21 A22 :
+    ▷ (A21 <: A11) -∗ ▷ (A12 <: A22) -∗
+    (A11 → A12) <: (A21 → A22).
+  Proof. iIntros "#H1 #H2" (v) "!> #H !>". by iApply lty_arr_le. Qed.
+
+  Lemma lty_prod_le A11 A12 A21 A22 :
+    ▷ (A11 <: A21) -∗ ▷ (A12 <: A22) -∗
+    A11 * A12 <: A21 * A22.
+  Proof.
+    iIntros "#H1 #H2" (v) "!>". iDestruct 1 as (w1 w2 ->) "[H1' H2']".
+    iExists _, _.
+    iDestruct ("H1" with "H1'") as "$".
+    by iDestruct ("H2" with "H2'") as "$".
+  Qed.
+
+  Lemma lty_sum_le A11 A12 A21 A22 :
+    ▷ (A11 <: A21) -∗ ▷ (A12 <: A22) -∗
+    A11 + A12 <: A21 + A22.
+  Proof.
+    iIntros "#H1 #H2" (v) "!> [H | H]"; iDestruct "H" as (w ->) "H".
+    - iDestruct ("H1" with "H") as "H1'". iLeft; eauto.
+    - iDestruct ("H2" with "H") as "H2'". iRight; eauto.
+  Qed.
+
+  Lemma lty_any_le A : ⊢ A <: lty_any.
+  Proof. by iIntros (v) "!> H". Qed.
+
+  Lemma lty_forall_le C1 C2 :
+    ▷ (∀ A, C1 A <: C2 A) -∗
+    (∀ A, C1 A) <: (∀ A, C2 A).
+  Proof.
+    iIntros "#Hle" (v) "!> H". iIntros (w).
+    iApply (wp_step_fupd); first done.
+    { iIntros "!>!>!>". iExact "Hle". }
+    iApply (wp_wand with "H"). iIntros (v') "H Hle' !>".
+    by iApply "Hle'".
+  Qed.
+
+  Lemma lty_exist_le C1 C2 :
+    ▷ (∀ A, C1 A <: C2 A) -∗
+    (∃ A, C1 A) <: (∃ A, C2 A).
+  Proof.
+    iIntros "#Hle" (v) "!>". iDestruct 1 as (A) "H". iExists A. by iApply "Hle".
+  Qed.
+
+  Lemma lty_rec_le_1 (C : lty Σ → lty Σ) `{!Contractive C} :
+    ⊢ lty_rec C <: C (lty_rec C).
+  Proof.
+    rewrite {1}/lty_rec {1}fixpoint_unfold {1}/lty_rec_aux. iApply lty_le_refl.
+  Qed.
+  Lemma lty_rec_le_2 (C : lty Σ → lty Σ) `{!Contractive C} :
+    ⊢ C (lty_rec C) <: lty_rec C.
+  Proof.
+    rewrite {2}/lty_rec {1}fixpoint_unfold {1}/lty_rec_aux. iApply lty_le_refl.
+  Qed.
+
+  Lemma lty_rec_le `{Contractive C1, Contractive C2} :
+    (□ ∀ A B, ▷ (A <: B) -∗ C1 A <: C2 B) -∗
+    lty_rec C1 <: lty_rec C2.
+  Proof.
+    iIntros "#Hle".
+    iLöb as "IH".
+    iIntros (v) "!> H".
+    rewrite /lty_rec {2}fixpoint_unfold.
+    iEval (rewrite fixpoint_unfold).
+    rewrite {3}/lty_rec_aux {4}/lty_rec_aux.
+    iApply ("Hle" with "[] H").
+    iNext. iApply "IH".
+  Qed.
+
+  Lemma lty_ref_mut_le A1 A2 :
+    ▷ (A1 <: A2) -∗
+    ref_mut A1 <: ref_mut A2.
+  Proof.
+    iIntros "#H1" (v) "!>". iDestruct 1 as (l w ->) "[Hl HA]".
+    iDestruct ("H1" with "HA") as "HA".
+    iExists l, w. by iFrame.
+  Qed.
+
+  Lemma lty_weak_ref_le A1 A2 :
+    ▷ (A1 <: A2) -∗ ▷ (A2 <: A1) -∗
+    ref_shr A1 <: ref_shr A2.
+  Proof.
+    iIntros "#Hle1 #Hle2" (v) "!>". iDestruct 1 as (l ->) "Hinv".
+    iExists l. iSplit; first done.
+    iApply (inv_iff with "Hinv"). iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle1".
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl". by iApply "Hle2".
+  Qed.
+
+  Lemma lty_mutex_le A1 A2 :
+    ▷ (A1 <: A2) -∗ ▷ (A2 <: A1) -∗
+    mutex A1 <: mutex A2.
+  Proof.
+    iIntros "#Hle1 #Hle2" (v) "!>". iDestruct 1 as (N γ l lk ->) "Hinv".
+    rewrite /spin_lock.is_lock.
+    iExists N, γ, l, lk. iSplit; first done.
+    rewrite /spin_lock.is_lock.
+    iDestruct "Hinv" as (l' ->) "Hinv".
+    iExists l'.
+    iSplit; first done.
+    iApply (inv_iff with "Hinv"); iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
+      destruct v; first done.
+      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
+      iDestruct ("Hle1" with "HA") as "HA". eauto with iFrame.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
+      destruct v; first done.
+      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
+      iDestruct ("Hle2" with "HA") as "HA". eauto with iFrame.
+  Qed.
+
+  Lemma lty_mutexguard_le A1 A2 :
+    ▷ (A1 <: A2) -∗ ▷ (A2 <: A1) -∗
+    mutexguard A1 <: mutexguard A2.
+  Proof.
+    iIntros "#Hle1 #Hle2" (v) "!>".
+    iDestruct 1 as (N γ l lk w ->) "[Hinv [Hlock Hinner]]".
+    rewrite /spin_lock.is_lock.
+    iExists N, γ, l, lk, w. iSplit; first done.
+    rewrite /spin_lock.is_lock.
+    iFrame "Hlock Hinner".
+    iDestruct "Hinv" as (l' ->) "Hinv".
+    iExists l'.
+    iSplit; first done.
+    iApply (inv_iff with "Hinv"); iIntros "!> !>". iSplit.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
+      destruct v; first done.
+      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
+      iDestruct ("Hle1" with "HA") as "HA". eauto with iFrame.
+    - iDestruct 1 as (v) "[Hl HA]". iExists v. iFrame "Hl".
+      destruct v; first done.
+      iDestruct "HA" as "[Hown HA]". iDestruct "HA" as (inner) "[Hinner HA]".
+      iDestruct ("Hle2" with "HA") as "HA". eauto with iFrame.
+  Qed.
+
+  Lemma lsty_le_refl P : ⊢ P <p: P.
+  Proof. iApply iProto_le_refl. Qed.
+
+  Lemma lsty_send_le A1 A2 P1 P2 :
+    ▷ (A2 <: A1) -∗ ▷ (P1 <p: P2) -∗
+    (<!!> A1 ; P1) <p: (<!!> A2 ; P2).
+  Proof.
+    iIntros "#HAle #HPle !>".
+    iApply iProto_le_send=> /=.
+    iIntros (x) "H !>".
+    iDestruct ("HAle" with "H") as "H".
+    eauto with iFrame.
+  Qed.
+
+  Lemma lsty_recv_le A1 A2 P1 P2 :
+    ▷ (A1 <: A2) -∗ ▷ (P1 <p: P2) -∗
+    (<??> A1 ; P1) <p: (<??> A2 ; P2).
+  Proof.
+    iIntros "#HAle #HPle !>".
+    iApply iProto_le_recv=> /=.
+    iIntros (x) "H !>".
+    iDestruct ("HAle" with "H") as "H".
+    eauto with iFrame.
+  Qed.
+
+  Lemma lsty_swap_le (A1 A2 : lty Σ) (P : lsty Σ) :
+    ⊢ (<??> A1 ; <!!> A2 ; P) <p: (<!!> A2 ; <??> A1 ; P).
+  Proof.
+    iIntros "!>".
+    iApply iProto_le_swap. iIntros (x1 x2) "/= HP1 HP2".
+    iExists _, _,
+      (tele_app (TT:=[tele _]) (λ x2, (x2, A2 x2, (P:iProto Σ)))),
+      (tele_app (TT:=[tele _]) (λ x1, (x1, A1 x1, (P:iProto Σ)))),
+    x2, x1.
+    simpl.
+    do 2 (iSplit; [done|]).
+    iFrame "HP1 HP2".
+    iModIntro.
+    do 2 (iSplitR; [iApply iProto_le_refl|]). by iFrame.
+  Qed.
+
+  Lemma lsty_select_le P11 P12 P21 P22 :
+    ▷ (P11 <p: P21) -∗ ▷ (P12 <p: P22) -∗
+    (P11 <+++> P12) <p: (P21 <+++> P22).
+  Proof.
+    iIntros "#H1 #H2 !>".
+    rewrite /lsty_select /iProto_branch=> /=.
+    iApply iProto_le_send=> /=.
+    iIntros (x) "_ !>".
+    destruct x; eauto with iFrame.
+  Qed.
+
+  Lemma lsty_branch_le P11 P12 P21 P22 :
+    ▷ (P11 <p: P21) -∗ ▷ (P12 <p: P22) -∗
+    (P11 <&&&> P12) <p: (P21 <&&&> P22).
+  Proof.
+    iIntros "#H1 #H2 !>".
+    rewrite /lsty_branch /iProto_branch=> /=.
+    iApply iProto_le_recv=> /=.
+    iIntros (x) "_ !>".
+    destruct x; eauto with iFrame.
+  Qed.
+
+  Lemma lsty_app_le P11 P12 P21 P22 :
+    (P11 <p: P21) -∗ (P12 <p: P22) -∗
+    (P11 <++++> P12) <p: (P21 <++++> P22).
+  Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
+
+  Lemma lsty_dual_le P1 P2 : P2 <p: P1 -∗ lsty_dual P1 <p: lsty_dual P2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
+
+  Lemma lsty_rec_le_1 (C : lsty Σ → lsty Σ) `{!Contractive C} :
+    ⊢ lsty_rec C <p: C (lsty_rec C).
+  Proof.
+    rewrite {1}/lsty_rec {1}fixpoint_unfold {1}/lsty_rec1.
+    iApply lsty_le_refl.
+  Qed.
+  Lemma lsty_rec_le_2 (C : lsty Σ → lsty Σ) `{!Contractive C} :
+    ⊢ C (lsty_rec C) <p: lsty_rec C.
+  Proof.
+    rewrite {2}/lsty_rec {1}fixpoint_unfold {1}/lsty_rec1.
+    iApply lsty_le_refl.
+  Qed.
+
+  Lemma lsty_rec_le `{Contractive C1, Contractive C2} :
+    (□ ∀ P P', ▷ (P <p: P') -∗ C1 P <p: C2 P') -∗
+    lsty_rec C1 <p: lsty_rec C2.
+  Proof.
+    iIntros "#Hle".
+    iLöb as "IH".
+    iIntros "!>".
+    rewrite /lsty_rec.
+    iEval (rewrite fixpoint_unfold).
+    iEval (rewrite (fixpoint_unfold (lsty_rec1 C2))).
+    rewrite {1 3}/lsty_rec1.
+    iApply ("Hle" with "[]").
+    iNext. iApply "IH".
+  Qed.
+
+  Lemma lty_chan_le P1 P2 :
+    ▷ (P1 <p: P2) -∗ chan P1 <: chan P2.
+  Proof.
+    iIntros "#Hle" (v) "!> H".
+    iApply (iProto_mapsto_le with "H [Hle]"). eauto.
+  Qed.
+
+  Theorem ltyped_subsumption Γ e τ1 τ2 :
+    τ1 <: τ2 -∗ (Γ ⊨ e : τ1) -∗ (Γ ⊨ e : τ2).
+  Proof.
+    iIntros "#Hle #Hltyped" (vs) "!> Henv".
+    iDestruct ("Hltyped" with "Henv") as "Hltyped'".
+    iApply (wp_wand with "Hltyped' [Hle]").
+    by iIntros (v).
+  Qed.
+
+End subtype.