actris/logrel/subtyping.v

+(** This file contains the definition of the semantic subtyping relation
+[A <: B], where [A] and [B] can be either term types or session types, as
+well as a semantic type equivalence relation [A <:> B], which is equivalent to
+having both [A <: B] and [B <: A]. Finally, the notion of a *copyable type* is
+defined in terms of subtyping: a type [A] is copyable when [A <: copy A]. *)
+From actris.logrel Require Export model term_types.
+
+Definition lty_le {Σ k} : lty Σ k → lty Σ k → iProp Σ :=
+  match k with
+  | tty_kind => λ A1 A2, ■ ∀ v, ltty_car A1 v -∗ ltty_car A2 v
+  | sty_kind => λ P1 P2, ■ iProto_le (lsty_car P1) (lsty_car P2)
+  end%I.
+Arguments lty_le : simpl never.
+Infix "<:" := lty_le (at level 70) : bi_scope.
+Notation "K1 <: K2" := (⊢ K1 <: K2) (at level 70) : type_scope.
+Global Instance: Params (@lty_le) 2 := {}.
+
+Definition lty_bi_le {Σ k} (M1 M2 : lty Σ k) : iProp Σ :=
+  tc_opaque (M1 <: M2 ∧ M2 <: M1)%I.
+Arguments lty_bi_le : simpl never.
+Infix "<:>" := lty_bi_le (at level 70) : bi_scope.
+Notation "K1 <:> K2" := (⊢ K1 <:> K2) (at level 70) : type_scope.
+Global Instance: Params (@lty_bi_le) 2 := {}.
+
+Definition lty_copyable {Σ} (A : ltty Σ) : iProp Σ :=
+  tc_opaque (A <: lty_copy A)%I.
+Global Instance: Params (@lty_copyable) 1 := {}.
+
+Section subtyping.
+  Context {Σ : gFunctors}.
+
+  Global Instance lty_le_plain {k} (M1 M2 : lty Σ k) : Plain (M1 <: M2).
+  Proof. destruct k; apply _. Qed.
+  Global Instance lty_bi_le_plain {k} (M1 M2 : lty Σ k) : Plain (M1 <:> M2).
+  Proof. rewrite /lty_bi_le /=. apply _. Qed.
+
+  Global Instance lty_le_ne k : NonExpansive2 (@lty_le Σ k).
+  Proof. destruct k; solve_proper. Qed.
+  Global Instance lty_le_proper {k} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ k).
+  Proof. apply (ne_proper_2 _). Qed.
+  Global Instance lty_bi_le_ne {k} : NonExpansive2 (@lty_bi_le Σ k).
+  Proof. solve_proper. Qed.
+  Global Instance lty_bi_le_proper {k} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_bi_le Σ k).
+  Proof. solve_proper. Qed.
+
+  Global Instance lty_copyable_plain A : Plain (@lty_copyable Σ A).
+  Proof. rewrite /lty_copyable /=. apply _. Qed.
+  Global Instance lty_copyable_ne : NonExpansive (@lty_copyable Σ).
+  Proof. rewrite /lty_copyable /=. solve_proper. Qed.
+
+  Lemma lsty_car_mono (S T : lsty Σ) :
+    (S <: T) -∗ lsty_car S ⊑ lsty_car T.
+  Proof. eauto. Qed.
+
+End subtyping.

actris/logrel/subtyping_rules.v

+(** This file defines all of the semantic subtyping rules for term types and
+session types. *)
+From iris.bi.lib Require Import core.
+From iris.base_logic.lib Require Import invariants.
+From iris.proofmode Require Import proofmode.
+From actris.logrel Require Export subtyping term_types session_types.
+
+Section subtyping_rules.
+  Context `{heapGS Σ, chanG Σ}.
+  Implicit Types A : ltty Σ.
+  Implicit Types S : lsty Σ.
+
+  (** Generic rules *)
+  Lemma lty_le_refl {k} (K : lty Σ k) : K <: K.
+  Proof. destruct k. by iIntros (v) "!> H". by iModIntro. Qed.
+  Lemma lty_le_trans {k} (K1 K2 K3 : lty Σ k) : K1 <: K2 -∗ K2 <: K3 -∗ K1 <: K3.
+  Proof.
+    destruct k.
+    - iIntros "#H1 #H2" (v) "!> H". iApply "H2". by iApply "H1".
+    - iIntros "#H1 #H2 !>". by iApply iProto_le_trans.
+  Qed.
+
+  Lemma lty_bi_le_refl {k} (K : lty Σ k) : K <:> K.
+  Proof. iSplit; iApply lty_le_refl. Qed.
+  Lemma lty_bi_le_trans {k} (K1 K2 K3 : lty Σ k) :
+    K1 <:> K2 -∗ K2 <:> K3 -∗ K1 <:> K3.
+  Proof. iIntros "#[H11 H12] #[H21 H22]". iSplit; by iApply lty_le_trans. Qed.
+  Lemma lty_bi_le_sym {k} (K1 K2 : lty Σ k) : K1 <:> K2 -∗ K2 <:> K1.
+  Proof. iIntros "#[??]"; by iSplit. Qed.
+
+  Lemma lty_le_l {k} (K1 K2 K3 : lty Σ k) : K1 <:> K2 -∗ K2 <: K3 -∗ K1 <: K3.
+  Proof. iIntros "#[H1 _] #H2". by iApply lty_le_trans. Qed.
+  Lemma lty_le_r {k} (K1 K2 K3 : lty Σ k) : K1 <: K2 -∗ K2 <:> K3 -∗ K1 <: K3.
+  Proof. iIntros "#H1 #[H2 _]". by iApply lty_le_trans. Qed.
+
+  Lemma lty_le_rec_unfold {k} (C : lty Σ k → lty Σ k) `{!Contractive C} :
+    lty_rec C <:> C (lty_rec C).
+  Proof.
+    iSplit.
+    - rewrite {1}/lty_rec fixpoint_unfold. iApply lty_le_refl.
+    - rewrite {2}/lty_rec fixpoint_unfold. iApply lty_le_refl.
+  Qed.
+
+  Lemma lty_le_rec_internal {k} (C1 C2 : lty Σ k → lty Σ k)
+      `{Contractive C1, Contractive C2} :
+    (∀ K1 K2, ▷ (K1 <: K2) -∗ C1 K1 <: C2 K2) -∗
+    lty_rec C1 <: lty_rec C2.
+  Proof.
+    iIntros "#Hle". iLöb as "IH".
+    iApply lty_le_l; [iApply lty_le_rec_unfold|].
+    iApply lty_le_r; [|iApply lty_bi_le_sym; iApply lty_le_rec_unfold].
+    by iApply "Hle".
+  Qed.
+  Lemma lty_le_rec_external {k} (C1 C2 : lty Σ k → lty Σ k)
+      `{Contractive C1, Contractive C2} :
+    (∀ K1 K2, (K1 <: K2) → C1 K1 <: C2 K2) →
+    lty_rec C1 <: lty_rec C2.
+  Proof.
+    intros IH. rewrite /lty_rec. apply fixpoint_ind.
+    - by intros K1' K2' -> ?.
+    - exists (fixpoint C2). iApply lty_le_refl.
+    - intros K' ?. rewrite (fixpoint_unfold C2). by apply IH.
+    - apply bi.limit_preserving_entails; [done|solve_proper].
+  Qed.
+
+  (** Term subtyping *)
+  Lemma lty_le_any A : A <: any.
+  Proof. by iIntros (v) "!> H". Qed.
+  Lemma lty_copyable_any : ⊢@{iPropI Σ} lty_copyable any.
+  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+  Lemma lty_le_copy A B : A <: B -∗ copy A <: copy B.
+  Proof. iIntros "#Hle". iIntros (v) "!> #HA !>". by iApply "Hle". Qed.
+  Lemma lty_le_copy_elim A : copy A <: A.
+  Proof. by iIntros (v) "!> #H". Qed.
+  Lemma lty_copyable_copy A : ⊢@{iPropI Σ} lty_copyable (copy A).
+  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+  Lemma lty_le_copy_inv_mono A B : A <: B -∗ copy- A <: copy- B.
+  Proof.
+    iIntros "#Hle !>" (v) "#HA". iApply (coreP_wand (ltty_car A v) with "[] HA").
+    iIntros "{HA} !> !>". iApply "Hle".
+  Qed.
+  Lemma lty_le_copy_inv_intro A : A <: copy- A.
+  Proof. iIntros "!>" (v). iApply coreP_intro. Qed.
+  Lemma lty_le_copy_inv_elim A : copy- (copy A) <: A.
+  Proof. iIntros (v) "!> #H". iApply (coreP_elim with "H"). Qed.
+  Lemma lty_copyable_copy_inv A : ⊢ lty_copyable (copy- A).
+  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+  Lemma lty_le_copy_inv_elim_copyable A : lty_copyable A -∗ copy- A <: A.
+  Proof.
+    iIntros "#Hcp".
+    iApply lty_le_trans.
+    - iApply lty_le_copy_inv_mono. iApply "Hcp".
+    - iApply lty_le_copy_inv_elim.
+  Qed.
+
+  Lemma lty_copyable_unit : ⊢@{iPropI Σ} lty_copyable ().
+  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+  Lemma lty_copyable_bool : ⊢@{iPropI Σ} lty_copyable lty_bool.
+  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+  Lemma lty_copyable_int : ⊢@{iPropI Σ} lty_copyable lty_int.
+  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+  Lemma lty_le_arr 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_le_arr_copy A11 A12 A21 A22 :
+    ▷ (A21 <: A11) -∗ ▷ (A12 <: A22) -∗
+    (A11 → A12) <: (A21 → A22).
+  Proof. iIntros "#H1 #H2" (v) "!> #H !>". by iApply lty_le_arr. Qed.
+  (** This rule is really trivial, since [A → B] is syntactic sugar for
+  [copy (A ⊸ B)], but we include it anyway for completeness' sake. *)
+  Lemma lty_copyable_arr_copy A B : ⊢@{iPropI Σ} lty_copyable (A → B).
+  Proof. iApply lty_copyable_copy. Qed.
+
+  Lemma lty_le_prod 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_le_prod_copy A B :
+    copy A * copy B <:> copy (A * B).
+  Proof.
+    iSplit; iModIntro; iIntros (v) "#Hv"; iDestruct "Hv" as (v1 v2 ->) "[Hv1 Hv2]".
+    - iModIntro. iExists v1, v2. iSplit; [done|]. iSplitL; auto.
+    - iExists v1, v2. iSplit; [done|]. auto.
+  Qed.
+
+  Lemma lty_copyable_prod A B :
+    lty_copyable A -∗ lty_copyable B -∗ lty_copyable (A * B).
+  Proof.
+    iIntros "#HcpA #HcpB". rewrite /lty_copyable /=.
+    iApply lty_le_r; last by iApply lty_le_prod_copy.
+    iApply lty_le_prod. iApply "HcpA". iApply "HcpB".
+  Qed.
+
+  Lemma lty_le_sum 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_le_sum_copy A B :
+    copy A + copy B <:> copy (A + B).
+  Proof.
+    iSplit; iModIntro; iIntros (v);
+      iDestruct 1 as "#[Hv|Hv]"; iDestruct "Hv" as (w ?) "Hw";
+      try iModIntro; first [iLeft; by auto|iRight; by auto].
+  Qed.
+  Lemma lty_copyable_sum A B :
+    lty_copyable A -∗ lty_copyable B -∗ lty_copyable (A + B).
+  Proof.
+    iIntros "#HcpA #HcpB". rewrite /lty_copyable /=.
+    iApply lty_le_r; last by iApply lty_le_sum_copy.
+    iApply lty_le_sum. iApply "HcpA". iApply "HcpB".
+  Qed.
+
+  Lemma lty_le_forall 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_le_exist 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_le_exist_elim C B :
+    C B <: ∃ A, C A.
+  Proof. iIntros "!>" (v) "Hle". by iExists B. Qed.
+  Lemma lty_le_exist_copy F :
+    (∃ A, copy (F A)) <:> copy (∃ A, F A).
+  Proof.
+    iSplit; iIntros "!>" (v); iDestruct 1 as (A) "#Hv";
+      iExists A; repeat iModIntro; iApply "Hv".
+  Qed.
+
+  Lemma lty_copyable_exist (C : ltty Σ → ltty Σ) :
+    (∀ M, lty_copyable (C M)) -∗ lty_copyable (lty_exist C).
+  Proof.
+    iIntros "#Hle". rewrite /lty_copyable /tc_opaque.
+    iApply lty_le_r; last by iApply lty_le_exist_copy.
+    iApply lty_le_exist. iApply "Hle".
+  Qed.
+
+  (* TODO(COPY): Commuting rule for recursive types, allowing [copy] to move
+  outside the recursive type. This rule should be derivable using Löb
+  induction. *)
+  Lemma lty_copyable_rec C `{!Contractive C} :
+    (∀ A, ▷ lty_copyable A -∗ lty_copyable (C A)) -∗ lty_copyable (lty_rec C).
+  Proof.
+    iIntros "#Hcopy".
+    iLöb as "IH".
+    iIntros (v) "!> Hv".
+    rewrite /lty_rec {2}fixpoint_unfold.
+    iDestruct ("Hcopy" with "IH Hv") as "{Hcopy} #Hcopy".
+    iModIntro.
+    iEval (rewrite fixpoint_unfold).
+    iApply "Hcopy".
+  Qed.
+
+  Lemma lty_le_ref_uniq A1 A2 :
+    ▷ (A1 <: A2) -∗
+    ref_uniq A1 <: ref_uniq 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_le_shr_ref A1 A2 :
+    ▷ (A1 <:> A2) -∗
+    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. iIntros "{$Hl} !>". by iApply "Hle1".
+    - iDestruct 1 as (v) "[Hl #HA]". iExists v. iIntros "{$Hl} !>". by iApply "Hle2".
+  Qed.
+  Lemma lty_copyable_shr_ref A :
+    ⊢ lty_copyable (ref_shr A).
+  Proof. iIntros (v) "!> #Hv !>". iFrame "Hv". Qed.
+
+  Lemma lty_le_chan S1 S2 :
+    ▷ (S1 <: S2) ⊢ chan S1 <: chan S2.
+  Proof.
+    iIntros "#Hle" (v) "!> H".
+    iApply (iProto_pointsto_le with "H [Hle]"). eauto.
+  Qed.
+
+  (** Session subtyping *)
+  Lemma lty_le_send A1 A2 S1 S2 :
+    (A2 <: A1) -∗ ▷ (S1 <: S2) -∗
+    (<!!> TY A1 ; S1) <: (<!!> TY A2 ; S2).
+  Proof.
+    iIntros "#HAle #HSle !>" (v) "H". iExists v.
+    iDestruct ("HAle" with "H") as "$". by iModIntro.
+  Qed.
+
+  Lemma lty_le_recv A1 A2 S1 S2 :
+    (A1 <: A2) -∗ ▷ (S1 <: S2) -∗
+    (<??> TY A1 ; S1) <: (<??> TY A2 ; S2).
+  Proof.
+    iIntros "#HAle #HSle !>" (v) "H". iExists v.
+    iDestruct ("HAle" with "H") as "$". by iModIntro.
+  Qed.
+
+  Lemma lty_le_exist_elim_l k (M : lty Σ k → lmsg Σ) S :
+    (∀ (A : lty Σ k), (<??> M A) <: S) ⊢
+    (<?? (A : lty Σ k)> M A) <: S.
+  Proof.
+    iIntros "#Hle !>". iApply (iProto_le_exist_elim_l_inhabited M). auto.
+  Qed.
+
+  Lemma lty_le_exist_elim_r k (M : lty Σ k → lmsg Σ) S :
+    (∀ (A : lty Σ k), S <: (<!!> M A)) ⊢
+    S <: (<!! (A : lty Σ k)> M A).
+  Proof.
+    iIntros "#Hle !>". iApply (iProto_le_exist_elim_r_inhabited _ M). auto.
+  Qed.
+
+  Lemma lty_le_exist_intro_l k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
+    (<!! X> M X) <: (<!!> M A).
+  Proof. iIntros "!>". iApply (iProto_le_exist_intro_l). Qed.
+
+  Lemma lty_le_exist_intro_r k (M : lty Σ k → lmsg Σ) (A : lty Σ k) :
+    (<??> M A) <: (<?? X> M X).
+  Proof. iIntros "!>". iApply (iProto_le_exist_intro_r). Qed.
+
+  Lemma lty_le_texist_elim_l {kt} (M : ltys Σ kt → lmsg Σ) S :
+    (∀ Xs, (<??> M Xs) <: S) ⊢
+    (<??.. Xs> M Xs) <: S.
+  Proof.
+    iIntros "H". iInduction kt as [|k kt] "IH"; simpl; [done|].
+    iApply lty_le_exist_elim_l; iIntros (X).
+    iApply "IH". iIntros (Xs). iApply "H".
+  Qed.
+
+  Lemma lty_le_texist_elim_r {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) S :
+    (∀ Xs, S <: (<!!> M Xs)) ⊢
+    S <: (<!!.. Xs> M Xs).
+  Proof.
+    iIntros "H". iInduction kt as [|k kt] "IH"; simpl; [done|].
+    iApply lty_le_exist_elim_r; iIntros (X).
+    iApply "IH". iIntros (Xs). iApply "H".
+  Qed.
+
+  Lemma lty_le_texist_intro_l {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) Ks :
+    (<!!.. Xs> M Xs) <: (<!!> M Ks).
+  Proof.
+    induction Ks as [|k kT X Xs IH]; simpl; [iApply lty_le_refl|].
+    iApply lty_le_trans; [by iApply lty_le_exist_intro_l|]. iApply IH.
+  Qed.
+
+  Lemma lty_le_texist_intro_r {kt : ktele Σ} (M : ltys Σ kt → lmsg Σ) Ks :
+    (<??> M Ks) <: (<??.. Xs> M Xs).
+  Proof.
+    induction Ks as [|k kt X Xs IH]; simpl; [iApply lty_le_refl|].
+    iApply lty_le_trans; [|by iApply lty_le_exist_intro_r]. iApply IH.
+  Qed.
+
+  Lemma lty_le_swap_recv_send A1 A2 S :
+    (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
+  Proof.
+    iIntros "!>" (v1 v2).
+    iApply iProto_le_trans;
+      [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ v2)|].
+    iApply iProto_le_trans;
+      [|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ v1)]; simpl.
+    iApply iProto_le_base_swap.
+  Qed.
+
+  Lemma lty_le_swap_recv_select A Ss :
+    (<??> TY A; lty_select Ss) <: lty_select ((λ S, <??> TY A; S) <$> Ss)%lty.
+  Proof.
+    iIntros "!>" (v1 x2).
+    iApply iProto_le_trans;
+      [iApply iProto_le_base; iApply (iProto_le_exist_intro_l _ x2)|]; simpl.
+    iApply iProto_le_payload_elim_r.
+    iDestruct 1 as %HSs. revert HSs.
+    rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
+    iApply iProto_le_trans; [iApply iProto_le_base_swap|]. iSplitL; [by eauto|].
+    iModIntro. by iExists v1.
+  Qed.
+
+  Lemma lty_le_swap_branch_send A Ss :
+    lty_branch ((λ S, <!!> TY A; S) <$> Ss)%lty <: (<!!> TY A; lty_branch Ss).
+  Proof.
+    iIntros "!>" (x1 v2).
+    iApply iProto_le_trans;
+      [|iApply iProto_le_base; iApply (iProto_le_exist_intro_r _ x1)]; simpl.
+    iApply iProto_le_payload_elim_l.
+    iDestruct 1 as %HSs. revert HSs.
+    rewrite !lookup_total_alt !lookup_fmap fmap_is_Some; iIntros ([S ->]) "/=".
+    iApply iProto_le_trans; [|iApply iProto_le_base_swap]. iSplitL; [by eauto|].
+    iModIntro. by iExists v2.
+  Qed.
+
+  Lemma lty_le_swap_branch_select (Ss1 Ss2 : (gmap Z (gmap Z (lsty Σ)))) :
+    (∀ i j Ss1' Ss2',
+        Ss1 !! i = Some Ss1' → Ss2 !! j = Some Ss2' →
+        is_Some (Ss1' !! j) ∧ is_Some (Ss2' !! i) ∧
+        Ss1' !! j = Ss2' !! i) →
+    lty_branch (lty_select <$> Ss1) <: lty_select (lty_branch <$> Ss2).
+  Proof.
+    intros Hin.
+    iIntros "!>" (v1 v2).
+    rewrite !lookup_fmap !fmap_is_Some !lookup_total_alt !lookup_fmap.
+    iIntros "H1 H2". iDestruct "H1" as %H1. iDestruct "H2" as %H2.
+    destruct H1 as [Ss1' Heq1]. destruct H2 as [Ss2' Heq2].
+    rewrite Heq1 Heq2 /=.
+    destruct (Hin v1 v2 Ss1' Ss2' Heq1 Heq2) as (Hin1 & Hin2 & Heq).
+    iApply iProto_le_trans.
+    { iModIntro. iExists v2. by iApply iProto_le_payload_intro_l. }
+    iApply iProto_le_trans; [ iApply iProto_le_base_swap |].
+    iModIntro. iExists v1.
+    iApply iProto_le_trans; [|by iApply iProto_le_payload_intro_r].
+    iModIntro. rewrite !lookup_total_alt. by rewrite Heq.
+  Qed.
+
+  Lemma lty_le_select (Ss1 Ss2 : gmap Z (lsty Σ)) :
+    ([∗ map] S1;S2 ∈ Ss1; Ss2, ▷ (S1 <: S2)) -∗
+    lty_select Ss1 <: lty_select Ss2.
+  Proof.
+    iIntros "#H !>" (x); iDestruct 1 as %[S2 HSs2]. iExists x.
+    iDestruct (big_sepM2_forall with "H") as (?) "{H} H".
+    assert (is_Some (Ss1 !! x)) as [S1 HSs1] by naive_solver.
+    iSpecialize ("H" with "[//] [//]").
+    rewrite HSs1. iSplitR; [by eauto|].
+    iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
+  Qed.
+  Lemma lty_le_select_subseteq (Ss1 Ss2 : gmap Z (lsty Σ)) :
+    Ss2 ⊆ Ss1 →
+    lty_select Ss1 <: lty_select Ss2.
+  Proof.
+    intros; iIntros "!>" (x); iDestruct 1 as %[S HSs2]. iExists x.
+    assert (Ss1 !! x = Some S) as HSs1 by eauto using lookup_weaken.
+    rewrite HSs1. iSplitR; [by eauto|].
+    iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
+  Qed.
+
+  Lemma lty_le_branch (Ss1 Ss2 : gmap Z (lsty Σ)) :
+    ([∗ map] S1;S2 ∈ Ss1; Ss2, ▷ (S1 <: S2)) ⊢
+    lty_branch Ss1 <: lty_branch Ss2.
+  Proof.
+    iIntros "#H !>" (x); iDestruct 1 as %[S1 HSs1]. iExists x.
+    iDestruct (big_sepM2_forall with "H") as (?) "{H} H".
+    assert (is_Some (Ss2 !! x)) as [S2 HSs2] by naive_solver.
+    iSpecialize ("H" with "[//] [//]").
+    rewrite HSs2. iSplitR; [by eauto|].
+    iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
+  Qed.
+  Lemma lty_le_branch_subseteq (Ss1 Ss2 : gmap Z (lsty Σ)) :
+    Ss1 ⊆ Ss2 →
+    lty_branch Ss1 <: lty_branch Ss2.
+  Proof.
+    intros; iIntros "!>" (x); iDestruct 1 as %[S HSs1]. iExists x.
+    assert (Ss2 !! x = Some S) as HSs2 by eauto using lookup_weaken.
+    rewrite HSs2. iSplitR; [by eauto|].
+    iIntros "!>". by rewrite !lookup_total_alt HSs1 HSs2 /=.
+  Qed.
+
+  (** The instances below make it possible to use the tactics [iIntros],
+  [iExist], [iSplitL]/[iSplitR], [iFrame] and [iModIntro] on [lty_le] goals.
+  These instances have higher precedence than the ones in [proto.v] to avoid
+  needless unfolding of the subtyping relation. *)
+  Global Instance lty_le_from_forall_l k (M : lty Σ k → lmsg Σ) (S : lsty Σ) name :
+    AsIdentName M name →
+    FromForall (lty_message Recv (lty_msg_exist M) <: S) (λ X, (<??> M X) <: S)%I name | 0.
+  Proof. intros _. apply lty_le_exist_elim_l. Qed.
+  Global Instance lty_le_from_forall_r k (S : lsty Σ) (M : lty Σ k → lmsg Σ) name :
+    AsIdentName M name →
+    FromForall (S <: lty_message Send (lty_msg_exist M)) (λ X, S <: (<!!> M X))%I name | 1.
+  Proof. intros _. apply lty_le_exist_elim_r. Qed.
+
+  Global Instance lty_le_from_exist_l k (M : lty Σ k → lmsg Σ) S :
+    FromExist ((<!! X> M X) <: S) (λ X, (<!!> M X) <: S)%I | 0.
+  Proof.
+    rewrite /FromExist. iDestruct 1 as (x) "H".
+    iApply (lty_le_trans with "[] H"). iApply lty_le_exist_intro_l.
+  Qed.
+  Global Instance lty_le_from_exist_r k (M : lty Σ k → lmsg Σ) S :
+    FromExist (S <: <?? X> M X) (λ X, S <: (<??> M X))%I | 1.
+  Proof.
+    rewrite /FromExist. iDestruct 1 as (x) "H".
+    iApply (lty_le_trans with "H"). iApply lty_le_exist_intro_r.
+  Qed.
+
+  Global Instance lty_le_from_modal_send A (S1 S2 : lsty Σ) :
+    FromModal True (modality_instances.modality_laterN 1) (S1 <: S2)
+              ((<!!> TY A; S1) <: (<!!> TY A; S2)) (S1 <: S2) | 0.
+  Proof.
+    rewrite /FromModal. iIntros (_) "H". iApply lty_le_send. iApply lty_le_refl. done.
+  Qed.
+
+  Global Instance lty_le_from_modal_recv A (S1 S2 : lsty Σ) :
+    FromModal True (modality_instances.modality_laterN 1) (S1 <: S2)
+              ((<??> TY A; S1) <: (<??> TY A; S2)) (S1 <: S2) | 0.
+  Proof.
+    rewrite /FromModal. iIntros (_) "H". iApply lty_le_recv. iApply lty_le_refl. done.
+  Qed.
+
+  (** Algebraic laws *)
+  Lemma lty_le_app S11 S12 S21 S22 :
+    (S11 <: S21) -∗ (S12 <: S22) -∗
+    (S11 <++> S12) <: (S21 <++> S22).
+  Proof. iIntros "#H1 #H2 !>". by iApply iProto_le_app. Qed.
+
+  Lemma lty_le_app_id_l S : (END <++> S) <:> S.
+  Proof. rewrite left_id. iSplit; by iModIntro. Qed.
+  Lemma lty_le_app_id_r S : (S <++> END) <:> S.
+  Proof. rewrite right_id. iSplit; by iModIntro. Qed.
+  Lemma lty_le_app_assoc S1 S2 S3 :
+    (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
+  Proof. rewrite assoc. iSplit; by iModIntro. Qed.
+
+  Lemma lty_le_app_send_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) S2 :
+    LtyMsgTele M A S →
+    (<!!> M) <++> S2 <:>
+        <!!.. As> TY (ktele_app A As) ; (ktele_app S As) <++> S2.
+  Proof.
+    rewrite /LtyMsgTele. intros ->.
+    rewrite /lty_app /lty_message iProto_app_message /=.
+    induction kt as [|k kt IH]; rewrite /= iMsg_app_exist.
+    - iSplit; iIntros (v); iExists v; rewrite iMsg_app_base; eauto.
+    - iSplit.
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply IH | iApply lty_le_refl ].
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply lty_bi_le_sym; iApply IH | iApply lty_le_refl ].
+  Qed.
+
+  Lemma lty_le_app_recv_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) S2 :
+    LtyMsgTele M A S →
+    (<??> M) <++> S2 <:>
+        <??.. As> TY (ktele_app A As) ; (ktele_app S As) <++> S2.
+  Proof.
+    rewrite /LtyMsgTele. intros ->.
+    rewrite /lty_app /lty_message iProto_app_message /=.
+    induction kt as [|k kt IH]; rewrite /= iMsg_app_exist.
+    - iSplit; iIntros (v); iExists v; rewrite iMsg_app_base; eauto.
+    - iSplit.
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply IH | iApply lty_le_refl ].
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply lty_bi_le_sym; iApply IH | iApply lty_le_refl ].
+  Qed.
+
+  Lemma lty_le_app_send A S1 S2 :
+    (<!!> TY A; S1) <++> S2 <:> (<!!> TY A; S1 <++> S2).
+  Proof. by apply (lty_le_app_send_exist (kt:=KTeleO)). Qed.
+  Lemma lty_le_app_recv A S1 S2 :
+    (<??> TY A; S1) <++> S2 <:> (<??> TY A; S1 <++> S2).
+  Proof. by apply (lty_le_app_recv_exist (kt:=KTeleO)). Qed.
+
+  Lemma lty_le_app_choice a (Ss : gmap Z (lsty Σ)) S2 :
+    lty_choice a Ss <++> S2 <:> lty_choice a ((.<++> S2) <$> Ss)%lty.
+  Proof.
+    rewrite /lty_app /lty_choice iProto_app_message iMsg_app_exist;
+      setoid_rewrite iMsg_app_base; setoid_rewrite lookup_total_alt;
+      setoid_rewrite lookup_fmap; setoid_rewrite fmap_is_Some.
+    iSplit; iIntros "!> /="; destruct a;
+      iIntros (x); iExists x; iDestruct 1 as %[S ->]; iSplitR; eauto.
+  Qed.
+  Lemma lty_le_app_select Ss S2 :
+    lty_select Ss <++> S2 <:> lty_select ((.<++> S2) <$> Ss)%lty.
+  Proof. apply lty_le_app_choice. Qed.
+  Lemma lty_le_app_branch Ss S2 :
+    lty_branch Ss <++> S2 <:> lty_branch ((.<++> S2) <$> Ss)%lty.
+  Proof. apply lty_le_app_choice. Qed.
+
+  Lemma lty_le_dual S1 S2 : S2 <: S1 -∗ lty_dual S1 <: lty_dual S2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual. Qed.
+  Lemma lty_le_dual_l S1 S2 : lty_dual S2 <: S1 -∗ lty_dual S1 <: S2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual_l. Qed.
+  Lemma lty_le_dual_r S1 S2 : S2 <: lty_dual S1 -∗ S1 <: lty_dual S2.
+  Proof. iIntros "#H !>". by iApply iProto_le_dual_r. Qed.
+
+  Lemma lty_le_dual_end : lty_dual (Σ:=Σ) END <:> END.
+  Proof. rewrite /lty_dual iProto_dual_end=> /=. apply lty_bi_le_refl. Qed.
+
+  Lemma lty_le_dual_message a A S :
+    lty_dual (lty_message a (TY A; S)) <:>
+      lty_message (action_dual a) (TY A; (lty_dual S)).
+  Proof.
+    rewrite /lty_dual iProto_dual_message iMsg_dual_exist.
+    setoid_rewrite iMsg_dual_base. iSplit; by iIntros "!> /=".
+  Qed.
+
+  Lemma lty_le_dual_send_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) :
+    LtyMsgTele M A S →
+    lty_dual (<!!> M) <:>
+        <??.. As> TY (ktele_app A As) ; lty_dual (ktele_app S As).
+  Proof.
+    rewrite /LtyMsgTele. intros ->.
+    rewrite /lty_dual /lty_message iProto_dual_message /=.
+    induction kt as [|k kt IH]; rewrite /= iMsg_dual_exist.
+    - iSplit; iIntros (v); iExists v; rewrite iMsg_dual_base; eauto.
+    - iSplit.
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply IH | iApply lty_le_refl ].
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply lty_bi_le_sym; iApply IH | iApply lty_le_refl ].
+  Qed.
+
+  Lemma lty_le_dual_recv_exist {kt} M (A : kt -k> ltty Σ) (S : kt -k> lsty Σ) :
+    LtyMsgTele M A S →
+    lty_dual (<??> M) <:>
+      <!!.. As> TY (ktele_app A As) ; lty_dual (ktele_app S As).
+  Proof.
+    rewrite /LtyMsgTele. intros ->.
+    rewrite /lty_dual /lty_message iProto_dual_message /=.
+    induction kt as [|k kt IH]; rewrite /= iMsg_dual_exist.
+    - iSplit; iIntros (v); iExists v; rewrite iMsg_dual_base; eauto.
+    - iSplit.
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply IH | iApply lty_le_refl ].
+      + iIntros (v). iExists v.
+        iApply lty_le_l; [ iApply lty_bi_le_sym; iApply IH | iApply lty_le_refl ].
+  Qed.
+
+  Lemma lty_le_dual_send A S : lty_dual (<!!> TY A; S) <:> (<??> TY A; lty_dual S).
+  Proof. by apply (lty_le_dual_send_exist (kt:=KTeleO)). Qed.
+  Lemma lty_le_dual_recv A S : lty_dual (<??> TY A; S) <:> (<!!> TY A; lty_dual S).
+  Proof. by apply (lty_le_dual_recv_exist (kt:=KTeleO)). Qed.
+
+  Lemma lty_le_dual_choice a (Ss : gmap Z (lsty Σ)) :
+    lty_dual (lty_choice a Ss) <:> lty_choice (action_dual a) (lty_dual <$> Ss).
+  Proof.
+    rewrite /lty_dual /lty_choice iProto_dual_message iMsg_dual_exist;
+      setoid_rewrite iMsg_dual_base.
+    iSplit; iIntros "!> /="; destruct a; iIntros (x); iExists x;
+      rewrite !lookup_total_alt lookup_fmap fmap_is_Some;
+      iDestruct 1 as %[S ->]; iSplitR; eauto.
+  Qed.
+
+  Lemma lty_le_dual_select (Ss : gmap Z (lsty Σ)) :
+    lty_dual (lty_select Ss) <:> lty_branch (lty_dual <$> Ss).
+  Proof. iApply lty_le_dual_choice. Qed.
+  Lemma lty_le_dual_branch (Ss : gmap Z (lsty Σ)) :
+    lty_dual (lty_branch Ss) <:> lty_select (lty_dual <$> Ss).
+  Proof. iApply lty_le_dual_choice. Qed.
+
+End subtyping_rules.
+
+Global Hint Extern 0 (environments.envs_entails _ (?x <: ?y)) =>
+  first [is_evar x; fail 1 | is_evar y; fail 1|iApply lty_le_refl] : core.

actris/logrel/telescopes.v

+(** This file defines kinded telescopes, which are used for representing binders
+in session types. *)
+From stdpp Require Import base tactics telescopes.
+From actris.logrel Require Import model.
+Set Default Proof Using "Type".
+
+(** NB: This is overkill for the current setting, as there are no
+dependencies between binders, hence we might have just used a list of [kind]
+but might be needed for future extensions, such as for bounded polymorphism *)
+(** Type Telescopes *)
+Inductive ktele {Σ} :=
+  | KTeleO : ktele
+  | KTeleS {k} : (lty Σ k → ktele) → ktele.
+Arguments ktele : clear implicits.
+
+(** The telescope version of kind types *)
+Fixpoint ktele_fun {Σ} (kt : ktele Σ) (A : Type) :=
+  match kt with
+  | KTeleO => A
+  | KTeleS b => ∀ K, ktele_fun (b K) A
+  end.
+
+Notation "kt -k> A" :=
+  (ktele_fun kt A) (at level 99, A at level 200, right associativity).
+
+(** An eliminator for elements of [ktele_fun]. *)
+Definition ktele_fold {Σ X Y kt}
+    (step : ∀ {k}, (lty Σ k → Y) → Y) (base : X → Y) : (kt -k> X) → Y :=
+  (fix rec {kt} : (kt -k> X) → Y :=
+     match kt as kt return (kt -k> X) → Y with
+     | KTeleO => λ x : X, base x
+     | KTeleS b => λ f, step (λ x, rec (f x))
+     end) kt.
+Arguments ktele_fold {_ _ _ !_} _ _ _ /.
+
+(** A sigma-like type for an "element" of a telescope, i.e., the data it *)
+Inductive ltys {Σ} : ktele Σ → Type :=
+  | LTysO : ltys KTeleO
+  | LTysS {k b} : ∀ K : lty Σ k, ltys (b K) → ltys (KTeleS b).
+Arguments ltys : clear implicits.
+
+(** Inversion lemmas for [ltys] *)
+Lemma ltys_inv {Σ kt} (Ks : ltys Σ kt) :
+  match kt as kt return ltys _ kt → Prop with
+  | KTeleO => λ Ks, Ks = LTysO
+  | KTeleS f => λ Ks, ∃ K Ks', Ks = LTysS K Ks'
+  end Ks.
+Proof. induction Ks; eauto. Qed.
+Lemma ltys_O_inv {Σ} (Ks : ltys Σ KTeleO) : Ks = LTysO.
+Proof. exact (ltys_inv Ks). Qed.
+Lemma ltys_S_inv {Σ X} {f : lty Σ X → ktele Σ} (Ks : ltys Σ (KTeleS f)) :
+  ∃ K Ks', Ks = LTysS K Ks'.
+Proof. exact (ltys_inv Ks). Qed.
+
+Definition ktele_app {Σ kt T} (f : kt -k> T) (Ks : ltys Σ kt) : T :=
+  (fix rec {kt} (Ks : ltys Σ kt) : (kt -k> T) → T :=
+    match Ks in ltys _ kt return (kt -k> T) → T with
+    | LTysO => λ t : T, t
+    | LTysS K Ks => λ f, rec Ks (f K)
+    end) kt Ks f.
+Arguments ktele_app {_} {!_ _} _ !_ /.
+
+Fixpoint ktele_bind {Σ U kt} : (ltys Σ kt → U) → kt -k> U :=
+  match kt as kt return (ltys _ kt → U) → kt -k> U with
+  | KTeleO => λ F, F LTysO
+  | @KTeleS _ k b => λ (F : ltys Σ (KTeleS b) → U) (K : lty Σ k), (* b x -t> U *)
+                  ktele_bind (λ Ks, F (LTysS K Ks))
+  end.
+Arguments ktele_bind {_} {_ !_} _ /.
+
+Lemma ktele_app_bind {Σ U kt} (f : ltys Σ kt → U) K :
+  ktele_app (ktele_bind f) K = f K.
+Proof.
+  induction kt as [|k b IH]; simpl in *.
+  - by rewrite (ltys_O_inv K).
+  - destruct (ltys_S_inv K) as [K' [Ks' ->]]; simpl. by rewrite IH.
+Qed.

actris/logrel/term_types.v

+(** This file contains the definitions of the semantic interpretations of the
+term type formers of the type system. The semantic interpretation of a type
+(former) is a unary Iris predicate on values [val → iProp], which determines
+when a value belongs to a certain type.
+
+The following types are defined:
+- [unit], [bool], [int]: basic types for unit, Boolean and integer values,
+  respectively.
+- [any]: inhabited by all values.
+- [A ⊸ B]: the type of affine functions from [A] to [B]. Affine functions can
+  only be invoked once, since they might have captured affine resources.
+- [A → B]: the type of non-affine (copyable) functions from [A] to [B]. These
+  can be invoked any number of times. This is simply syntactic sugar for
+  [copy (A ⊸ B)].
+- [A * B], [A + B], [∀ X, A], [∃ X, A]: products, sums, universal types,
+  existential types.
+- [copy A]: inhabited by those values in the type [A] which are copyable. In the
+  case of functions, for instance, functions (closures) which capture affine
+  resources are not copyable, whereas functions that do not capture resources are.
+- [copy- A]: acts as a kind of "inverse" to [copy A]. More precisely, we have
+  that [copy- (copy A) :> A]. This type is used to indicate the results of
+  operations that might consume a resource, but do not always do so, depending
+  on whether the type [A] is copyable. Such operations result in a [copy- A],
+  which can be turned into an [A] using subtyping when [A] is copyable.
+- [ref_uniq A]: the type of uniquely-owned mutable references to a value of type [A].
+  Since the reference is guaranteed to be unique, it is possible for the type [A]
+  contained in the reference to change to a different type [B] by assigning to
+  the reference.
+- [ref_shr A]: the type of shared mutable references to a value of type [A].
+- [chan P]: the type of channels, governed by the session type [P].
+
+In addition, some important properties, such as contractivity and
+non-expansiveness of these type formers is proved. This is important in order to
+use these type formers to define recursive types. *)
+From iris.bi.lib Require Import core.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Export lib.spin_lock.
+From actris.logrel Require Export model.
+From actris.channel Require Export channel.
+
+Definition lty_unit {Σ} : ltty Σ := Ltty (λ w, ⌜ w = #() ⌝%I).
+Definition lty_bool {Σ} : ltty Σ := Ltty (λ w, ∃ b : bool, ⌜ w = #b ⌝)%I.
+Definition lty_int {Σ} : ltty Σ := Ltty (λ w, ∃ n : Z, ⌜ w = #n ⌝)%I.
+Definition lty_any {Σ} : ltty Σ := Ltty (λ w, True%I).
+
+Definition lty_arr `{heapGS Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
+  ∀ v, ▷ ltty_car A1 v -∗ WP w v {{ ltty_car A2 }})%I.
+(* TODO: Make a non-linear version of prod, using ∧ *)
+Definition lty_prod {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
+  ∃ w1 w2, ⌜w = (w1,w2)%V⌝ ∗ ▷ ltty_car A1 w1 ∗ ▷ ltty_car A2 w2)%I.
+Definition lty_sum {Σ} (A1 A2 : ltty Σ) : ltty Σ := Ltty (λ w,
+  (∃ w1, ⌜w = InjLV w1⌝ ∗ ▷ ltty_car A1 w1) ∨
+  (∃ w2, ⌜w = InjRV w2⌝ ∗ ▷ ltty_car A2 w2))%I.
+
+Definition lty_forall `{heapGS Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
+  Ltty (λ w, ∀ X, WP w #() {{ ltty_car (C X) }})%I.
+Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
+  Ltty (λ w, ∃ X, ▷ ltty_car (C X) w)%I.
+
+Definition lty_copy {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, □ ltty_car A w)%I.
+Definition lty_copy_minus {Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w, coreP (ltty_car A w)).
+
+Definition lty_ref_uniq `{heapGS Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
+  ∃ (l : loc) (v : val), ⌜w = #l⌝ ∗ l ↦ v ∗ ▷ ltty_car A v)%I.
+Definition ref_shrN := nroot .@ "shr_ref".
+Definition lty_ref_shr `{heapGS Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
+  ∃ l : loc, ⌜w = #l⌝ ∗ inv (ref_shrN .@ l) (∃ v, l ↦ v ∗ □ ltty_car A v))%I.
+
+Definition lty_chan `{heapGS Σ, chanG Σ} (P : lsty Σ) : ltty Σ :=
+  Ltty (λ w, w ↣ lsty_car P)%I.
+
+Global Instance: Params (@lty_copy) 1 := {}.
+Global Instance: Params (@lty_copy_minus) 1 := {}.
+Global Instance: Params (@lty_arr) 2 := {}.
+Global Instance: Params (@lty_prod) 1 := {}.
+Global Instance: Params (@lty_sum) 1 := {}.
+Global Instance: Params (@lty_forall) 2 := {}.
+Global Instance: Params (@lty_sum) 1 := {}.
+Global Instance: Params (@lty_ref_uniq) 2 := {}.
+Global Instance: Params (@lty_ref_shr) 2 := {}.
+Global Instance: Params (@lty_chan) 3 := {}.
+
+Notation any := lty_any.
+Notation "()" := lty_unit : lty_scope.
+Notation "'copy' A" := (lty_copy A) (at level 10) : lty_scope.
+Notation "'copy-' A" := (lty_copy_minus A) (at level 10) : lty_scope.
+
+Notation "A ⊸ B" := (lty_arr A B)
+  (at level 99, B at level 200, right associativity) : lty_scope.
+Notation "A → B" := (lty_copy (lty_arr A B)) : lty_scope.
+Infix "*" := lty_prod : lty_scope.
+Infix "+" := lty_sum : lty_scope.
+
+Notation "∀ X1 .. Xn , C" :=
+  (lty_forall (λ X1, .. (lty_forall (λ Xn, C%lty)) ..)) : lty_scope.
+Notation "∃ X1 .. Xn , C" :=
+  (lty_exist (λ X1, .. (lty_exist (λ Xn, C%lty)) ..)) : lty_scope.
+
+Notation "'ref_uniq' A" := (lty_ref_uniq A) (at level 10) : lty_scope.
+Notation "'ref_shr' A" := (lty_ref_shr A) (at level 10) : lty_scope.
+
+Notation "'chan' A" := (lty_chan A) (at level 10) : lty_scope.
+
+Section term_types.
+  Context {Σ : gFunctors}.
+  Implicit Types A : ltty Σ.
+
+  Global Instance lty_copy_ne : NonExpansive (@lty_copy Σ).
+  Proof. solve_proper. Qed.
+  Global Instance lty_copy_minus_ne : NonExpansive (@lty_copy_minus Σ).
+  Proof. solve_proper. Qed.
+
+  Global Instance lty_arr_contractive `{heapGS Σ} n :
+    Proper (dist_later n ==> dist_later n ==> dist n) lty_arr.
+  Proof.
+    intros A A' ? B B' ?. apply Ltty_ne=> v. f_equiv=> w.
+    f_equiv; [by f_contractive|].
+    apply (wp_contractive _ _ _ _ _)=> v'. dist_later_intro as n' Hn'. by f_equiv.
+  Qed.
+  Global Instance lty_arr_ne `{heapGS Σ} : NonExpansive2 lty_arr.
+  Proof. solve_proper. Qed.
+  Global Instance lty_prod_contractive n:
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lty_prod Σ).
+  Proof. solve_contractive. Qed.
+  Global Instance lty_prod_ne : NonExpansive2 (@lty_prod Σ).
+  Proof. solve_proper. Qed.
+  Global Instance lty_sum_contractive n :
+    Proper (dist_later n ==> dist_later n ==> dist n) (@lty_sum Σ).
+  Proof. solve_contractive. Qed.
+  Global Instance lty_sum_ne : NonExpansive2 (@lty_sum Σ).
+  Proof. solve_proper. Qed.
+
+  Global Instance lty_forall_contractive `{heapGS Σ} k n :
+    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_forall Σ _ k).
+  Proof.
+    intros F F' A. apply Ltty_ne=> w. f_equiv=> B.
+    apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
+    dist_later_intro as n' Hn'. by f_equiv.
+  Qed.
+  Global Instance lty_forall_ne `{heapGS Σ} k n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).
+  Proof. solve_proper. Qed.
+  Global Instance lty_exist_contractive k n :
+    Proper (pointwise_relation _ (dist_later n) ==> dist n) (@lty_exist Σ k).
+  Proof. solve_contractive. Qed.
+  Global Instance lty_exist_ne k n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_exist Σ k).
+  Proof. solve_proper. Qed.
+
+  Global Instance lty_ref_uniq_contractive `{heapGS Σ} : Contractive lty_ref_uniq.
+  Proof. solve_contractive. Qed.
+  Global Instance lty_ref_uniq_ne `{heapGS Σ} : NonExpansive lty_ref_uniq.
+  Proof. solve_proper. Qed.
+
+  Global Instance lty_ref_shr_contractive `{heapGS Σ} : Contractive lty_ref_shr.
+  Proof. solve_contractive. Qed.
+  Global Instance lty_ref_shr_ne `{heapGS Σ} : NonExpansive lty_ref_shr.
+  Proof. solve_proper. Qed.
+
+  Global Instance lty_chan_contractive `{heapGS Σ, chanG Σ} : Contractive lty_chan.
+  Proof. solve_contractive. Qed.
+  Global Instance lty_chan_ne `{heapGS Σ, chanG Σ} : NonExpansive lty_chan.
+  Proof. solve_proper. Qed.
+End term_types.

actris/logrel/term_typing_judgment.v

+(** This file contains the definitions of the semantic typing judgment
+[Γ ⊨ e : A ⫤ Γ'], indicating that in context [Γ], the expression [e] has type
+[A], producing a new context [Γ']. The context is allowed to change to
+accomodate things like changing the type of a channel after a receive.
+
+In addition, we use the adequacy of Iris in order to show type soundness:
+programs which satisfy the semantic typing relation are safe. That is,
+semantically well-typed programs do not get stuck. *)
+From iris.heap_lang Require Import metatheory adequacy.
+From actris.logrel Require Export term_types.
+From actris.logrel Require Export contexts.
+From iris.proofmode Require Import proofmode.
+
+(** The semantic typing judgment *)
+Definition ltyped `{!heapGS Σ}
+    (Γ1 Γ2 : ctx Σ) (e : expr) (A : ltty Σ) : iProp Σ :=
+  tc_opaque (■ ∀ vs, ctx_ltyped vs Γ1 -∗
+    WP subst_map vs e {{ v, ltty_car A v ∗ ctx_ltyped vs Γ2 }})%I.
+Global Instance: Params (@ltyped) 2 := {}.
+
+Notation "Γ1 ⊨ e : A ⫤ Γ2" := (ltyped Γ1 Γ2 e A)
+  (at level 100, e at next level, A at level 200) : bi_scope.
+Notation "Γ ⊨ e : A" := (Γ ⊨ e : A ⫤ Γ)%I
+  (at level 100, e at next level, A at level 200) : bi_scope.
+
+Notation "Γ1 ⊨ e : A ⫤ Γ2" := (⊢ Γ1 ⊨ e : A ⫤ Γ2)
+  (at level 100, e at next level, A at level 200) : type_scope.
+Notation "Γ ⊨ e : A" := (⊢ Γ ⊨ e : A ⫤ Γ)
+  (at level 100, e at next level, A at level 200) : type_scope.
+
+Section ltyped.
+  Context `{!heapGS Σ}.
+
+  Global Instance ltyped_plain Γ1 Γ2 e A : Plain (ltyped Γ1 Γ2 e A).
+  Proof. rewrite /ltyped /=. apply _. Qed.
+  Global Instance ltyped_ne n :
+    Proper (dist n ==> dist n ==> (=) ==> dist n ==> dist n) (@ltyped Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance ltyped_proper :
+    Proper ((≡) ==> (≡) ==> (=) ==> (≡) ==> (≡)) (@ltyped Σ _).
+  Proof. solve_proper. Qed.
+  Global Instance ltyped_Permutation :
+    Proper ((≡ₚ) ==> (≡ₚ) ==> (=) ==> (≡) ==> (≡)) (@ltyped Σ _).
+  Proof.
+    intros Γ1 Γ1' HΓ1 Γ2 Γ2' HΓ2 e ? <- A ? <-. rewrite /ltyped /=.
+    setoid_rewrite HΓ1. by setoid_rewrite HΓ2.
+  Qed.
+End ltyped.
+
+(** Expressions and values are defined mutually recursive in HeapLang,
+which means that only after a step of reduction we get that e.g.
+[Pair (Val v1, Val v2)] reduces to [PairV (v1,v2)].
+This makes typing of values tricky, for technical reasons.
+To circumvent this, we make use of the following typing judgement for values,
+that lets us type check values without requiring reduction steps.
+The value typing judgement subsumes the typing judgement on expressions,
+as made precise by the [ltyped_val_ltyped] lemma. *)
+Definition ltyped_val `{!heapGS Σ} (v : val) (A : ltty Σ) : iProp Σ :=
+  tc_opaque (■ ltty_car A v)%I.
+Global Instance: Params (@ltyped_val) 3 := {}.
+Notation "⊨ᵥ v : A" := (ltyped_val v A)
+  (at level 100, v at next level, A at level 200) : bi_scope.
+Notation "⊨ᵥ v : A" := (⊢ ⊨ᵥ v : A)
+  (at level 100, v at next level, A at level 200) : stdpp_scope.
+Arguments ltyped_val : simpl never.
+
+Section ltyped_val.
+  Context `{!heapGS Σ}.
+
+  Global Instance ltyped_val_plain v A : Plain (ltyped_val v A).
+  Proof. rewrite /ltyped_val /=. apply _. Qed.
+  Global Instance ltyped_val_ne n v :
+    Proper (dist n ==> dist n) (@ltyped_val Σ _ v).
+  Proof. solve_proper. Qed.
+  Global Instance ltyped_val_proper v :
+    Proper ((≡) ==> (≡)) (@ltyped_val Σ _ v).
+  Proof. solve_proper. Qed.
+
+End ltyped_val.
+
+Section ltyped_rel.
+  Context `{!heapGS Σ}.
+
+  Lemma ltyped_val_ltyped Γ v A : (⊨ᵥ v : A) -∗ Γ ⊨ v : A.
+  Proof.
+    iIntros "#HA" (vs) "!> HΓ".
+    iApply wp_value. iFrame "HΓ".
+    rewrite /ltyped_val /=.
+    iApply "HA".
+  Qed.
+
+End ltyped_rel.
+
+Lemma ltyped_safety `{heapGpreS Σ} e σ es σ' e' :
+  (∀ `{heapGS Σ}, ∃ 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). iIntros "_".
+  iDestruct (He $!∅ with "[]") as "He"; first by rewrite /ctx_ltyped.
+  iEval (rewrite -(subst_map_empty e)). iApply (wp_wand with "He"); auto.
+Qed.

actris/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 iris.bi.lib Require Import core.
+From iris.heap_lang Require Import metatheory.
+From iris.heap_lang.lib Require Export par.
+From actris.logrel Require Export subtyping_rules term_typing_judgment operators.
+From actris.channel Require Import proofmode.
+
+Section term_typing_rules.
+  Context `{heapGS Σ}.
+  Implicit Types A B : ltty Σ.
+  Implicit Types Γ : ctx Σ.
+
+  (** Frame rule *)
+  Lemma ltyped_frame Γ Γ1 Γ2 e A :
+    (Γ1 ⊨ e : A ⫤ Γ2) -∗
+    (Γ1 ++ Γ ⊨ e : A ⫤ Γ2 ++ Γ).
+  Proof.
+    iIntros "#He !>" (vs) "HΓ".
+    iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 HΓ]".
+    iApply (wp_wand with "(He HΓ1)").
+    iIntros (v) "[$ HΓ2]". by iApply (ctx_ltyped_app with "[$]").
+  Qed.
+
+  (** Variable properties *)
+  Lemma ltyped_var Γ (x : string) A :
+    Γ !! x = Some A →
+    Γ ⊨ x : A ⫤ ctx_cons x (copy- A) Γ.
+  Proof.
+    iIntros (HΓx%ctx_lookup_perm) "!>"; iIntros (vs) "HΓ /=".
+    rewrite {1}HΓx /=.
+    iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]". rewrite Hvs.
+    iAssert (ltty_car (copy- A) v)%lty as "#HAm"; [by iApply coreP_intro|].
+    iApply wp_value. iFrame "HA". iApply ctx_ltyped_cons. eauto with iFrame.
+  Qed.
+
+  (** Subtyping *)
+  Theorem ltyped_subsumption Γ1 Γ2 Γ1' Γ2' e τ τ' :
+    Γ1 <ctx: Γ1' -∗ τ' <: τ -∗ Γ2' <ctx: Γ2 -∗
+    (Γ1' ⊨ e : τ' ⫤ Γ2') -∗ (Γ1 ⊨ e : τ ⫤ Γ2).
+  Proof.
+    iIntros "#HleΓ1 #Hle #HleΓ2 #He" (vs) "!> HΓ1".
+    iApply (wp_wand with "(He (HleΓ1 HΓ1))").
+    iIntros (v) "[Hτ HΓ2]". iSplitL "Hτ"; [by iApply "Hle"|by iApply "HleΓ2"].
+  Qed.
+  Theorem ltyped_val_subsumption v τ τ' :
+    τ' <: τ -∗
+    (⊨ᵥ v : τ') -∗ (⊨ᵥ v : τ).
+  Proof.
+    iIntros "#Hle #Hv". iIntros "!>". iApply "Hle".
+    rewrite /ltyped_val /=. iApply "Hv".
+  Qed.
+  Lemma ltyped_post_nil Γ1 Γ2 e τ :
+    (Γ1 ⊨ e : τ ⫤ Γ2) -∗ (Γ1 ⊨ e : τ ⫤ []).
+  Proof.
+    iApply ltyped_subsumption;
+      [iApply ctx_le_refl|iApply lty_le_refl|iApply ctx_le_nil].
+  Qed.
+
+  (** Basic properties *)
+  Lemma ltyped_val_unit : ⊨ᵥ #() : ().
+  Proof. eauto. Qed.
+  Lemma ltyped_unit Γ : Γ ⊨ #() : ().
+  Proof. iApply ltyped_val_ltyped. iApply ltyped_val_unit. Qed.
+  Lemma ltyped_val_bool (b : bool) : ⊨ᵥ #b : lty_bool.
+  Proof. eauto. Qed.
+  Lemma ltyped_bool Γ (b : bool) : Γ ⊨ #b : lty_bool.
+  Proof. iApply ltyped_val_ltyped. iApply ltyped_val_bool. Qed.
+  Lemma ltyped_val_int (z: Z) : ⊨ᵥ #z : lty_int.
+  Proof. eauto. Qed.
+  Lemma ltyped_int Γ (i : Z) : Γ ⊨ #i : lty_int.
+  Proof. iApply ltyped_val_ltyped. iApply ltyped_val_int. Qed.
+
+  (** Operations *)
+  Lemma ltyped_un_op Γ1 Γ2 op e A B :
+    LTyUnOp op A B →
+    (Γ1 ⊨ e : A ⫤ Γ2) -∗
+    (Γ1 ⊨ UnOp op e : B ⫤ Γ2).
+  Proof.
+    iIntros (Hop) "#He !>". iIntros (vs) "HΓ1 /=".
+    wp_smart_apply (wp_wand with "(He [HΓ1 //])"). iIntros (v1) "[HA $]".
+    iDestruct (Hop with "HA") as (w ?) "HB". by wp_unop.
+  Qed.
+
+  Lemma ltyped_bin_op Γ1 Γ2 Γ3 op e1 e2 A1 A2 B :
+    LTyBinOp op A1 A2 B →
+    (Γ1 ⊨ e2 : A2 ⫤ Γ2) -∗
+    (Γ2 ⊨ e1 : A1 ⫤ Γ3) -∗
+    (Γ1 ⊨ BinOp op e1 e2 : B ⫤ Γ3).
+  Proof.
+    iIntros (Hop) "#He2 #He1 !>". iIntros (vs) "HΓ1 /=".
+    wp_smart_apply (wp_wand with "(He2 [HΓ1 //])"). iIntros (v2) "[HA2 HΓ2]".
+    wp_smart_apply (wp_wand with "(He1 [HΓ2 //])"). iIntros (v1) "[HA1 $]".
+    iDestruct (Hop with "HA1 HA2") as (w ?) "HB". by wp_binop.
+  Qed.
+
+  (** Conditionals *)
+  Lemma ltyped_if Γ1 Γ2 Γ3 e1 e2 e3 A :
+    (Γ1 ⊨ e1 : lty_bool ⫤ Γ2) -∗
+    (Γ2 ⊨ e2 : A ⫤ Γ3) -∗
+    (Γ2 ⊨ e3 : A ⫤ Γ3) -∗
+    (Γ1 ⊨ (if: e1 then e2 else e3) : A ⫤ Γ3).
+  Proof.
+    iIntros "#He1 #He2 #He3 !>" (v) "HΓ1 /=".
+    wp_smart_apply (wp_wand with "(He1 [HΓ1 //])"). iIntros (b) "[Hbool HΓ2]".
+    rewrite /lty_bool. iDestruct "Hbool" as ([]) "->".
+    - wp_smart_apply (wp_wand with "(He2 [HΓ2 //])"). iIntros (w) "[$$]".
+    - wp_smart_apply (wp_wand with "(He3 [HΓ2 //])"). iIntros (w) "[$$]".
+  Qed.
+
+  (** Arrow properties *)
+  Lemma ltyped_app Γ1 Γ2 Γ3 e1 e2 A1 A2 :
+    (Γ1 ⊨ e2 : A1 ⫤ Γ2) -∗ (Γ2 ⊨ e1 : A1 ⊸ A2 ⫤ Γ3) -∗
+    (Γ1 ⊨ e1 e2 : A2 ⫤ Γ3).
+  Proof.
+    iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
+    wp_smart_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
+    wp_smart_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf $]".
+    iApply ("Hf" $! v with "HA1").
+  Qed.
+
+  Lemma ltyped_app_copy Γ1 Γ2 Γ3 e1 e2 A1 A2 :
+    (Γ1 ⊨ e2 : A1 ⫤ Γ2) -∗ (Γ2 ⊨ e1 : A1 → A2 ⫤ Γ3) -∗
+    (Γ1 ⊨ e1 e2 : A2 ⫤ Γ3).
+  Proof.
+    iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
+    wp_smart_apply (wp_wand with "(H2 [HΓ //])"). iIntros (v) "[HA1 HΓ]".
+    wp_smart_apply (wp_wand with "(H1 [HΓ //])"). iIntros (f) "[Hf HΓ]".
+    iApply wp_frame_r. iFrame "HΓ". iApply ("Hf" $! v with "HA1").
+  Qed.
+
+  Lemma ltyped_lam Γ1 Γ2 x e A1 A2 :
+    (ctx_cons x A1 Γ1 ⊨ e : A2 ⫤ []) -∗
+    Γ1 ++ Γ2 ⊨ (λ: x, e) : A1 ⊸ A2 ⫤ Γ2.
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=". wp_pures.
+    iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]".
+    iIntros "!>" (v) "HA1". wp_pures.
+    iDestruct ("He" $! (binder_insert x v vs) with "[HA1 HΓ1]") as "He'".
+    { by iApply (ctx_ltyped_insert' with "HA1"). }
+    rewrite subst_map_binder_insert.
+    iApply (wp_wand with "He'"). by iIntros (w) "[$ _]".
+  Qed.
+
+  (* TODO: This might be derivable from rec value rule *)
+  Lemma ltyped_val_lam x e A1 A2 :
+    (ctx_cons x A1 [] ⊨ e : A2 ⫤ []) -∗
+    ⊨ᵥ (λ: x, e) : A1 ⊸ A2.
+  Proof.
+    iIntros "#He !>" (v) "HA1".
+    wp_pures.
+    iDestruct ("He" $!(binder_insert x v ∅) with "[HA1]") as "He'".
+    { iApply (ctx_ltyped_insert' ∅ ∅ x A1 v with "HA1").
+      iApply ctx_ltyped_nil. }
+    rewrite subst_map_binder_insert /= binder_delete_empty subst_map_empty.
+    iApply (wp_wand with "He'"). by iIntros (w) "[$ _]".
+  Qed.
+
+  (* Typing rule for introducing copyable functions *)
+  Definition ctx_copy_minus : ctx Σ → ctx Σ :=
+    fmap (λ xA, CtxItem (ctx_item_name xA) (lty_copy_minus (ctx_item_type xA))).
+
+  Lemma ltyped_rec Γ1 Γ2 f x e A1 A2 :
+    (ctx_cons f (A1 → A2) (ctx_cons x A1 (ctx_copy_minus Γ1)) ⊨ e : A2 ⫤ []) -∗
+    Γ1 ++ Γ2 ⊨ (rec: f x := e) : A1 → A2 ⫤ Γ2.
+  Proof.
+    iIntros "#He". iIntros (vs) "!> HΓ /=". wp_pures.
+    iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]".
+    iAssert (<pers> ctx_ltyped vs (ctx_copy_minus Γ1))%I as "{HΓ1} #HΓ1".
+    { iClear "He". rewrite /ctx_copy_minus big_sepL_persistently big_sepL_fmap.
+      iApply (big_sepL_impl with "HΓ1"). iIntros "!>" (k [y B] _) "/=".
+      iDestruct 1 as (v ?) "HB". iExists v. iSplit; [by auto|].
+      by iDestruct (coreP_intro with "HB") as "{HB} #HB". }
+    iModIntro. 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Γ1 HA1]") as "He'".
+    { iApply (ctx_ltyped_insert' with "IH").
+      by iApply (ctx_ltyped_insert' with "HA1"). }
+    rewrite !subst_map_binder_insert_2.
+    iApply (wp_wand with "He'"). iIntros (w) "[$ _]".
+  Qed.
+
+  Lemma ltyped_val_rec f x e A1 A2 :
+    (ctx_cons f (A1 → A2) (ctx_cons x A1 []) ⊨ e : A2 ⫤ []) -∗
+    ⊨ᵥ (rec: f x := e) : A1 → A2.
+  Proof.
+    iIntros "#He". simpl. iLöb as "IH".
+    iIntros (v) "!>!> HA1". wp_pures. set (r := RecV f x _).
+    iDestruct ("He"$! (binder_insert f r (binder_insert x v ∅))
+                 with "[HA1]") as "He'".
+    { iApply (ctx_ltyped_insert').
+      { rewrite /ltyped_val /=. iApply "IH". }
+      iApply (ctx_ltyped_insert' with "HA1").
+      iApply ctx_ltyped_nil. }
+    rewrite !subst_map_binder_insert_2 !binder_delete_empty subst_map_empty.
+    iApply (wp_wand with "He'").
+    iIntros (w) "[$ _]".
+  Qed.
+
+  Lemma ltyped_let Γ1 Γ2 Γ3 x e1 e2 A1 A2 :
+    (Γ1 ⊨ e1 : A1 ⫤ Γ2) -∗
+    (ctx_cons x A1 Γ2 ⊨ e2 : A2 ⫤ Γ3) -∗
+    (Γ1 ⊨ (let: x:=e1 in e2) : A2 ⫤ ctx_filter_eq x Γ2 ++ ctx_filter_ne x Γ3).
+  Proof.
+    iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
+    wp_smart_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HA1 HΓ2]". wp_pures.
+    rewrite {3}(ctx_filter_eq_perm Γ2 x).
+    iDestruct (ctx_ltyped_app with "HΓ2") as "[HΓ2eq HΓ2neq]".
+    iDestruct ("He2" $! (binder_insert x v vs) with "[HA1 HΓ2neq]") as "He'".
+    { by iApply (ctx_ltyped_insert with "HA1"). }
+    rewrite subst_map_binder_insert. iApply (wp_wand with "He'").
+    iIntros (w) "[$ HΓ3]".
+    iApply ctx_ltyped_app. iFrame "HΓ2eq". by iApply ctx_ltyped_delete.
+  Qed.
+
+  Lemma ltyped_seq Γ1 Γ2 Γ3 e1 e2 A B :
+    (Γ1 ⊨ e1 : A ⫤ Γ2) -∗
+    (Γ2 ⊨ e2 : B ⫤ Γ3) -∗
+    (Γ1 ⊨ (e1 ;; e2) : B ⫤ Γ3).
+  Proof.
+    iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
+    wp_smart_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[_ HΓ2]". wp_pures.
+    wp_smart_apply (wp_wand with "(He2 HΓ2)"); iIntros (w) "[HB HΓ3]".
+    iFrame "HB HΓ3".
+  Qed.
+
+  (** Product properties  *)
+  Lemma ltyped_pair Γ1 Γ2 Γ3 e1 e2 A1 A2 :
+    (Γ1 ⊨ e2 : A2 ⫤ Γ2) -∗ (Γ2 ⊨ e1 : A1 ⫤ Γ3) -∗
+    (Γ1 ⊨ (e1,e2) : A1 * A2 ⫤ Γ3).
+  Proof.
+    iIntros "#H2 #H1". iIntros (vs) "!> HΓ /=".
+    wp_smart_apply (wp_wand with "(H2 [HΓ //])"); iIntros (w2) "[HA2 HΓ]".
+    wp_smart_apply (wp_wand with "(H1 [HΓ //])"); iIntros (w1) "[HA1 HΓ]".
+    wp_pures. iFrame "HΓ". iExists w1, w2. by iFrame.
+  Qed.
+
+  Lemma ltyped_fst Γ A1 A2 (x : string) :
+    Γ !! x = Some (A1 * A2)%lty →
+    Γ ⊨ Fst x : A1 ⫤ ctx_cons x (copy- A1 * A2) Γ.
+  Proof.
+    iIntros (HΓx%ctx_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
+    iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures.
+    iAssert (ltty_car (copy- A1) v1)%lty as "#HA1m"; [by iApply coreP_intro|].
+    iFrame "HA1". iApply ctx_ltyped_cons. iModIntro. iExists _; iSplit; [done|]; iFrame "HΓ".
+    iExists v1, v2. eauto with iFrame.
+  Qed.
+
+  Lemma ltyped_snd Γ A1 A2 (x : string) :
+    Γ !! x = Some (A1 * A2)%lty →
+    Γ ⊨ Snd x : A2 ⫤ ctx_cons x (A1 * copy- A2) Γ.
+  Proof.
+    iIntros (HΓx%ctx_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
+    iDestruct "HA" as (v1 v2 ->) "[HA1 HA2]". wp_pures.
+    iAssert (ltty_car (copy- A2) v2)%lty as "#HA2m"; [by iApply coreP_intro|].
+    iFrame "HA2". iApply ctx_ltyped_cons. iModIntro. iExists _; iSplit; [done|]; iFrame "HΓ".
+    iExists v1, v2. eauto with iFrame.
+  Qed.
+
+  (** Sum Properties *)
+  Lemma ltyped_injl Γ1 Γ2 e A1 A2 :
+    (Γ1 ⊨ e : A1 ⫤ Γ2) -∗
+    (Γ1 ⊨ InjL e : A1 + A2 ⫤ Γ2).
+  Proof.
+    iIntros "#HA" (vs) "!> HΓ /=".
+    wp_smart_apply (wp_wand with "(HA [HΓ //])").
+    iIntros (v) "[HA' $]". wp_pures.
+    iLeft. iExists v. auto.
+  Qed.
+
+  Lemma ltyped_injr Γ1 Γ2 e A1 A2 :
+    (Γ1 ⊨ e : A2 ⫤ Γ2) -∗
+    (Γ1 ⊨ InjR e : A1 + A2 ⫤ Γ2).
+  Proof.
+    iIntros "#HA" (vs) "!> HΓ /=".
+    wp_smart_apply (wp_wand with "(HA [HΓ //])").
+    iIntros (v) "[HA' $]". wp_pures.
+    iRight. iExists v. auto.
+  Qed.
+
+  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).
+  Proof.
+    iIntros "#H1 #H2 #H3" (vs) "!> HΓ1 /=".
+    wp_smart_apply (wp_wand with "(H1 HΓ1)"). iIntros (s) "[[Hs|Hs] HΓ2]";
+      iDestruct "Hs" as (w ->) "HA"; wp_case.
+    - wp_smart_apply (wp_wand with "(H2 HΓ2)"). iIntros (v) "[Hv $]".
+      iApply (wp_wand with "(Hv HA)"). auto.
+    - wp_smart_apply (wp_wand with "(H3 HΓ2)"). iIntros (v) "[Hv $]".
+      iApply (wp_wand with "(Hv HA)"). auto.
+  Qed.
+
+  (** Universal Properties *)
+  Lemma ltyped_tlam Γ1 Γ2 Γ' e k (C : lty Σ k → ltty Σ) :
+    (∀ K, Γ1 ⊨ e : C K ⫤ []) -∗
+    (Γ1 ++ Γ2 ⊨ (λ: <>, e) : (∀ X, C X) ⫤ Γ2).
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=". wp_pures.
+    iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 $]".
+    iIntros "!>" (M) "/=". wp_pures.
+    iApply (wp_wand with "(He HΓ1)"). iIntros (v) "[$ _]".
+  Qed.
+
+  Lemma ltyped_tapp Γ Γ2 e k (C : lty Σ k → ltty Σ) K :
+    (Γ ⊨ e : (∀ X, C X) ⫤ Γ2) -∗
+    (Γ ⊨ e #() : C K ⫤ Γ2).
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=".
+    wp_smart_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB HΓ] /=".
+    iApply (wp_wand with "HB [HΓ]"). by iIntros (v) "$".
+  Qed.
+
+  (** Existential properties *)
+  Lemma ltyped_pack Γ1 Γ2 e k (C : lty Σ k → ltty Σ) K :
+    (Γ1 ⊨ e : C K ⫤ Γ2) -∗ Γ1 ⊨ e : (∃ X, C X) ⫤ Γ2.
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=".
+    wp_smart_apply (wp_wand with "(He [HΓ //])"); iIntros (w) "[HB $]". by iExists K.
+  Qed.
+
+  Lemma ltyped_unpack {k} Γ1 Γ2 Γ3 x e1 e2 (C : lty Σ k → ltty Σ) B :
+    (Γ1 ⊨ e1 : (∃ X, C X) ⫤ Γ2) -∗
+    (∀ K, ctx_cons x (C K) Γ2 ⊨ e2 : B ⫤ Γ3) -∗
+    (Γ1 ⊨ (let: x := e1 in e2) : B ⫤ ctx_filter_eq x Γ2 ++ ctx_filter_ne x Γ3).
+  Proof.
+    iIntros "#He1 #He2 !>". iIntros (vs) "HΓ1 /=".
+    wp_smart_apply (wp_wand with "(He1 HΓ1)"); iIntros (v) "[HC HΓ2]".
+    iDestruct "HC" as (X) "HX". wp_pures.
+    rewrite {3}(ctx_filter_eq_perm Γ2 x).
+    iDestruct (ctx_ltyped_app with "HΓ2") as "[HΓ2eq HΓ2neq]".
+    iDestruct ("He2" $! X (binder_insert x v vs) with "[HX HΓ2neq]") as "He'".
+    { by iApply (ctx_ltyped_insert with "HX"). }
+    rewrite subst_map_binder_insert. iApply (wp_wand with "He'").
+    iIntros (w) "[$ HΓ3]". iApply ctx_ltyped_app.
+    iFrame "HΓ2eq". by iApply ctx_ltyped_delete.
+  Qed.
+
+  (** Mutable Unique Reference properties *)
+  Lemma ltyped_alloc Γ1 Γ2 e A :
+    (Γ1 ⊨ e : A ⫤ Γ2) -∗
+    (Γ1 ⊨ ref e : ref_uniq A ⫤ Γ2).
+  Proof.
+    iIntros "#He" (vs) "!> HΓ1 /=".
+    wp_smart_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
+    wp_alloc l as "Hl". iExists l, v; eauto with iFrame.
+  Qed.
+
+  Lemma ltyped_free Γ1 Γ2 e A :
+    (Γ1 ⊨ e : ref_uniq A ⫤ Γ2) -∗
+    (Γ1 ⊨ Free e : () ⫤ Γ2).
+  Proof.
+    iIntros "#He" (vs) "!> HΓ1 /=".
+    wp_smart_apply (wp_wand with "(He HΓ1)"). iIntros (v) "[Hv $]".
+    iDestruct "Hv" as (l w ->) "[Hl Hw]". by wp_free.
+  Qed.
+
+  Lemma ltyped_load Γ (x : string) A :
+    Γ !! x = Some (ref_uniq A)%lty →
+    Γ ⊨ ! x : A ⫤ ctx_cons x (ref_uniq (copy- A)) Γ.
+  Proof.
+    iIntros (HΓx%ctx_lookup_perm vs) "!> HΓ /=". rewrite {1}HΓx /=.
+    iDestruct (ctx_ltyped_cons with "HΓ") as (v Hvs) "[HA HΓ]"; rewrite Hvs.
+    iDestruct "HA" as (l w ->) "[? HA]". wp_load.
+    iAssert (ltty_car (copy- A) w)%lty as "#HAm"; [by iApply coreP_intro|].
+    iFrame "HA". iApply ctx_ltyped_cons. iModIntro. iExists _; iSplit; [done|]; iFrame "HΓ".
+    iExists l, w. eauto with iFrame.
+  Qed.
+
+  Lemma ltyped_store Γ Γ' (x : string) e A B :
+    Γ' !! x = Some (ref_uniq A)%lty →
+    (Γ ⊨ e : B ⫤ Γ') -∗
+    (Γ ⊨ x <- e : () ⫤ ctx_cons x (ref_uniq B) Γ').
+  Proof.
+    iIntros (HΓx%ctx_lookup_perm) "#He"; iIntros (vs) "!> HΓ /=".
+    wp_smart_apply (wp_wand with "(He HΓ)"). iIntros (v) "[HB HΓ']".
+    rewrite {2}HΓx /=.
+    iDestruct (ctx_ltyped_cons with "HΓ'") as (vl Hvs) "[HA HΓ']"; rewrite Hvs.
+    iDestruct "HA" as (l w ->) "[? HA]". wp_store. iModIntro. iSplit; [done|].
+    iApply ctx_ltyped_cons. iExists _; iSplit; [done|]; iFrame "HΓ'".
+    iExists l, v. eauto with iFrame.
+  Qed.
+
+  (** Mutable Shared Reference properties *)
+  Lemma ltyped_upgrade_shared  Γ Γ' e A :
+    (Γ ⊨ e : ref_uniq (copy A) ⫤ Γ') -∗
+    (Γ ⊨ e : ref_shr A ⫤ Γ').
+  Proof.
+    iIntros "#He" (vs) "!> HΓ". iApply wp_fupd.
+    iApply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv $]".
+    iDestruct "Hv" as (l w ->) "[Hl HA]". iExists l.
+    iMod (inv_alloc (ref_shrN .@ l) _
+      (∃ v : val, l ↦ v ∗ □ ltty_car A v) with "[Hl HA]") as "$"; last done.
+    iExists w. iFrame "Hl HA".
+  Qed.
+
+  Lemma ltyped_load_shared Γ Γ' e A :
+    (Γ ⊨ e : ref_shr A ⫤ Γ') -∗
+    Γ ⊨ ! e : A ⫤ Γ'.
+  Proof.
+    iIntros "#He" (vs) "!> HΓ /=".
+    wp_smart_apply (wp_wand with "(He HΓ)"). iIntros (v) "[Hv $]".
+    iDestruct "Hv" as (l ->) "#Hv".
+    iInv (ref_shrN .@ l) as (v) "[>Hl #HA]" "Hclose".
+    wp_load.
+    iMod ("Hclose" with "[Hl HA]") as "_"; last done.
+    iExists v. iFrame "Hl HA".
+  Qed.
+
+  Lemma ltyped_store_shared Γ1 Γ2 Γ3 e1 e2 A :
+    (Γ1 ⊨ e2 : copy A ⫤ Γ2) -∗
+    (Γ2 ⊨ e1 : ref_shr A ⫤ Γ3) -∗
+    (Γ1 ⊨ e1 <- e2 : () ⫤ Γ3).
+  Proof.
+    iIntros "#H1 #H2" (vs) "!> HΓ1 /=".
+    wp_smart_apply (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 $]".
+    iDestruct "Hw" as (l ->) "#Hw".
+    iInv (ref_shrN .@ l) as (?) "[>Hl HA]" "Hclose".
+    wp_store.
+    iMod ("Hclose" with "[Hl Hv]") as "_"; eauto.
+  Qed.
+
+  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_smart_apply (wp_wand with "(H1 HΓ1)"). iIntros (v) "[Hv HΓ2]".
+    wp_smart_apply (wp_wand with "(H2 HΓ2)"). iIntros (w) "[Hw $]".
+    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. }
+    by iExists k.
+  Qed.
+
+  (** Parallel composition properties *)
+  Lemma ltyped_par `{spawnG Σ} Γ1 Γ1' Γ2 Γ2' e1 e2 A B :
+    (Γ1 ⊨ e1 : A ⫤ Γ1') -∗
+    (Γ2 ⊨ e2 : B ⫤ Γ2') -∗
+    (Γ1 ++ Γ2 ⊨ e1 ||| e2 : A * B ⫤ Γ1' ++ Γ2').
+  Proof.
+    iIntros "#He1 #He2 !>" (vs) "HΓ /=".
+    iDestruct (ctx_ltyped_app with "HΓ") as "[HΓ1 HΓ2]".
+    wp_smart_apply (wp_par with "(He1 HΓ1) (He2 HΓ2)").
+    iIntros (v1 v2) "[[HA HΓ1'] [HB HΓ2']] !>". iSplitL "HA HB".
+    + iExists v1, v2. by iFrame.
+    + iApply ctx_ltyped_app. by iFrame.
+  Qed.
+End term_typing_rules.

actris/utils/cofe_solver_2.v

+From iris.algebra Require Import cofe_solver.
+
+(** Version of the cofe_solver for a parametrized functor. Generalize and move
+to Iris. *)
+Record solution_2 (F : ofe → oFunctor) := Solution2 {
+  solution_2_car : ∀ An `{!Cofe An} A `{!Cofe A}, ofe;
+  solution_2_cofe `{!Cofe An, !Cofe A} : Cofe (solution_2_car An A);
+  solution_2_iso `{!Cofe An, !Cofe A} :>
+    ofe_iso (oFunctor_apply (F A) (solution_2_car A An)) (solution_2_car An A);
+}.
+Arguments solution_2_car {F}.
+Global Existing Instance solution_2_cofe.
+
+Section cofe_solver_2.
+  Context (F : ofe → oFunctor).
+  Context `{Fcontr : !∀ T, oFunctorContractive (F T)}.
+  Context `{Fcofe : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
+  Context `{Finh : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
+  Notation map := (oFunctor_map (F _)).
+
+  Definition F_2 (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : oFunctor :=
+    oFunctor_oFunctor_compose (F A) (F An).
+
+  Definition T_result `{!Cofe An, !Cofe A} : solution (F_2 An A) := solver.result _.
+  Definition T (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : ofe :=
+    T_result (An:=An) (A:=A).
+  Instance T_cofe `{!Cofe An, !Cofe A} : Cofe (T An A) := _.
+  Instance T_inhabited `{!Cofe An, !Cofe A} : Inhabited (T An A) :=
+    populate (ofe_iso_1 T_result inhabitant).
+
+  Definition T_iso_fun_aux `{!Cofe An, !Cofe A}
+      (rec : prodO (oFunctor_apply (F An) (T An A) -n> T A An)
+                   (T A An -n> oFunctor_apply (F An) (T An A))) :
+      prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+            (T An A -n> oFunctor_apply (F A) (T A An)) :=
+    (ofe_iso_1 T_result ◎ map (rec.1,rec.2), map (rec.2,rec.1) ◎ ofe_iso_2 T_result).
+  Instance T_iso_aux_fun_contractive `{!Cofe An, !Cofe A} :
+    Contractive (T_iso_fun_aux (An:=An) (A:=A)).
+  Proof. solve_contractive. Qed.
+
+  Definition T_iso_fun_aux_2 `{!Cofe An, !Cofe A}
+      (rec : prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+                   (T An A -n> oFunctor_apply (F A) (T A An))) :
+      prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+            (T An A -n> oFunctor_apply (F A) (T A An)) :=
+    T_iso_fun_aux (T_iso_fun_aux rec).
+  Instance T_iso_fun_aux_2_contractive `{!Cofe An, !Cofe A} :
+    Contractive (T_iso_fun_aux_2 (An:=An) (A:=A)).
+  Proof.
+    intros n rec1 rec2 Hrec. rewrite /T_iso_fun_aux_2.
+    f_equiv. by apply T_iso_aux_fun_contractive.
+  Qed.
+
+  Definition T_iso_fun `{!Cofe An, !Cofe A} :
+      prodO (oFunctor_apply (F A) (T A An) -n> T An A)
+            (T An A -n> oFunctor_apply (F A) (T A An)) :=
+    fixpoint T_iso_fun_aux_2.
+  Definition T_iso_fun_unfold_1 `{!Cofe An, !Cofe A} y :
+    T_iso_fun (An:=An) (A:=A).1 y ≡ (T_iso_fun_aux (T_iso_fun_aux T_iso_fun)).1 y.
+  Proof. apply (fixpoint_unfold T_iso_fun_aux_2). Qed.
+  Definition T_iso_fun_unfold_2 `{!Cofe An, !Cofe A} y :
+    T_iso_fun (An:=An) (A:=A).2 y ≡ (T_iso_fun_aux (T_iso_fun_aux T_iso_fun)).2 y.
+  Proof. apply (fixpoint_unfold T_iso_fun_aux_2). Qed.
+
+  Lemma result_2 : solution_2 F.
+  Proof using Fcontr Fcofe Finh.
+    apply (Solution2 F T _)=> An Hcn A Hc.
+    apply (OfeIso (T_iso_fun.1) (T_iso_fun.2)).
+    - intros y. apply equiv_dist=> n. revert An Hcn A Hc y.
+      induction (lt_wf n) as [n _ IH]; intros An ? A ? y.
+      rewrite T_iso_fun_unfold_1 T_iso_fun_unfold_2 /=.
+      rewrite -{2}(ofe_iso_12 T_result y). f_equiv.
+      rewrite -(oFunctor_map_id (F _) (ofe_iso_2 T_result y))
+              -!oFunctor_map_compose.
+      f_equiv; apply Fcontr; dist_later_intro as n' Hn'; split=> x /=;
+        rewrite ofe_iso_21 -{2}(oFunctor_map_id (F _) x)
+          -!oFunctor_map_compose; do 2 f_equiv; split=> z /=; auto.
+    - intros y. apply equiv_dist=> n. revert An Hcn A Hc y.
+      induction (lt_wf n) as [n _ IH]; intros An ? A ? y.
+      rewrite T_iso_fun_unfold_1 T_iso_fun_unfold_2 /= ofe_iso_21.
+      rewrite -(oFunctor_map_id (F _) y) -!oFunctor_map_compose.
+      f_equiv; apply Fcontr; dist_later_intro as n' Hn'; split=> x /=;
+        rewrite -{2}(ofe_iso_12 T_result x); f_equiv;
+        rewrite -{2}(oFunctor_map_id (F _) (ofe_iso_2 T_result x))
+                -!oFunctor_map_compose;
+        do 2 f_equiv; split=> z /=; auto.
+  Qed.
+End cofe_solver_2.

theories/utils/compare.v → actris/utils/compare.v

-(** This file includes a definition and specification
-for comparing values based on a given interpretation [I]
-and a relation [R], along with an implementation in the [heap_lang]
-language, given the [≤] relation.*)
+(** This file includes a specification [cmp_spec] for comparing values based on
+a given interpretation [I], a relation [R] that matches up with a HeapLang
+implementation [cmp]. The file also provides an instance for the [≤] relation
+on integers [Z].*)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 
-Definition cmp_spec `{!heapG Σ} {A} (I : A → val → iProp Σ)
+Definition cmp_spec `{!heapGS Σ} {A} (I : A → val → iProp Σ)
     (R : relation A) `{!RelDecision R} (cmp : val) : iProp Σ :=
   (∀ x x' v v',
     {{{ I x v ∗ I x' v' }}}
       cmp v v'
     {{{ RET #(bool_decide (R x x')); I x v ∗ I x' v' }}})%I.
 
-Definition IZ `{!heapG Σ} (x : Z) (v : val) : iProp Σ := ⌜v = #x⌝%I.
+Definition IZ `{!heapGS Σ} (x : Z) (v : val) : iProp Σ := ⌜v = #x⌝%I.
 Definition cmpZ : val := λ: "x" "y", "x" ≤ "y".
 
-Lemma cmpZ_spec `{!heapG Σ} : cmp_spec IZ (≤) cmpZ.
+Lemma cmpZ_spec `{!heapGS Σ} : ⊢ cmp_spec IZ (≤)%Z cmpZ.
 Proof.
   rewrite /IZ. iIntros (x x' v v' Φ [-> ->]) "!> HΦ".
   wp_lam. wp_pures. by iApply "HΦ".

theories/utils/contribution.v → actris/utils/contribution.v

-(** This file defines a ghost functor for tracking
-"contributions" made to a shared concurrent effort.
-It is ultimately defined as:
-[contribution := Auth (Option ((Pos * A) + Excl 1))]
-
-Intuitively it allows one to allocate a [server γ n v] and a
-number of [client γ v] fragments that can each hold resources.
-The intended use is to allocate a client for each thread that
-contributes to a channel endpoint, where the resources [v] are
-things that are currently owned by the thread, that is later
-used in the protocol.
-
-The server keeps track of the number of active clients [n],
-and what resources they are currently holding [v].*)
+(** This file defines the "authoritative contribution ghost theory" for tracking
+contributions made by clients towards a shared concurrent effort. Compared to
+the paper, the construction is defined over a user-given carrier camera [A],
+instead of multisets.
+
+This ghost theory construction exposes two connectives:
+
+- [server γ n v]: keeps track of the number of active clients [n] and the total
+  amount of resources hold by all clients [x : A].
+- [client γ x]: keeps track of the resources [x : A] hold by a single client.
+
+The intended use case is to allocate a [client] for each thread that contributes
+to a channel endpoint, where the resources [x] are owned by the thread, that is
+later used in the protocol.
+
+To model this ghost theory construction, we use the camera
+[auth (option (csum (positive * A) (excl unit)))]. *)
 From iris.base_logic Require Export base_logic lib.iprop lib.own.
-From iris.proofmode Require Export tactics.
-From iris.algebra Require Import excl auth csum gmultiset frac_auth.
+From iris.proofmode Require Export proofmode.
+From iris.algebra Require Import excl auth csum gmultiset numbers.
 From iris.algebra Require Export local_updates.
 
-Class contributionG Σ (A : ucmraT) `{!CmraDiscrete A} := {
-  contribution_inG :> inG Σ
+Class contributionG Σ (A : ucmra) `{!CmraDiscrete A} := {
+  contribution_inG :: inG Σ
     (authR (optionUR (csumR (prodR positiveR A) (exclR unitO))))
 }.
 
@@ -26,13 +29,13 @@ Definition server `{contributionG Σ A} (γ : gname) (n : nat) (x : A) : iProp
   (if decide (n = O)
    then x ≡ ε ∗ own γ (● (Some (Cinr (Excl ())))) ∗ own γ (◯ (Some (Cinr (Excl ()))))
    else own γ (● (Some (Cinl (Pos.of_nat n, x)))))%I.
-Typeclasses Opaque server.
-Instance: Params (@server) 6 := {}.
+Global Typeclasses Opaque server.
+Global Instance: Params (@server) 6 := {}.
 
 Definition client `{contributionG Σ A} (γ : gname) (x : A) : iProp Σ :=
   own γ (◯ (Some (Cinl (1%positive, x)))).
-Typeclasses Opaque client.
-Instance: Params (@client) 5 := {}.
+Global Typeclasses Opaque client.
+Global Instance: Params (@client) 5 := {}.
 
 Section contribution.
   Context `{contributionG Σ A}.
@@ -47,7 +50,7 @@ Section contribution.
   Global Instance client_proper γ : Proper ((≡) ==> (≡)) (client γ).
   Proof. apply (ne_proper _). Qed.
 
-  Lemma contribution_init : (|==> ∃ γ, server γ 0 ε)%I.
+  Lemma contribution_init : ⊢ |==> ∃ γ, server γ 0 ε.
   Proof.
     iMod (own_alloc (● (Some (Cinr (Excl ()))) ⋅ ◯ (Some (Cinr (Excl ())))))
       as (γ) "[Hγ Hγ']"; first by apply auth_both_valid_2.
@@ -60,8 +63,8 @@ Section contribution.
   Lemma server_1_agree γ x y : server γ 1 x -∗ client γ y -∗ ⌜ x ≡ y ⌝.
   Proof.
     rewrite /server /client. case_decide=> //. iIntros "Hs Hc".
-    iDestruct (own_valid_2 with "Hs Hc")
-      as %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid; first done.
+    iCombine "Hs Hc"
+      gives %[[[_ ?]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete; first done.
     move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[? _].
     by destruct (Pos.lt_irrefl 1).
   Qed.
@@ -84,9 +87,9 @@ Section contribution.
   Proof.
     rewrite /server /client. iIntros "Hs Hc". case_decide; subst.
     - iDestruct "Hs" as "(_ & _ & Hc')".
-      by iDestruct (own_valid_2 with "Hc Hc'") as %?.
-    - iDestruct (own_valid_2 with "Hs Hc")
-        as %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid.
+      by iCombine "Hc Hc'" gives %?%auth_frag_op_valid_1.
+    - iCombine "Hs Hc"
+        gives %[[[??]%(inj Cinl)|Hincl]%Some_included _]%auth_both_valid_discrete.
       { setoid_subst. by destruct n. }
       move: Hincl. rewrite Cinl_included prod_included /= pos_included=> -[??].
       by destruct n.
@@ -149,7 +152,7 @@ Section contribution.
 
   (** Derived *)
   Lemma contribution_init_pow n :
-    (|==> ∃ γ, server γ n ε ∗ [∗] replicate n (client γ ε))%I.
+    ⊢ |==> ∃ γ, server γ n ε ∗ [∗] replicate n (client γ ε).
   Proof.
     iMod (contribution_init) as (γ) "Hs". iExists γ.
     iInduction n as [|n] "IH"; simpl; first by iFrame.

theories/utils/group.v → actris/utils/group.v

-(** This file provides utility for grouping elements
-based on keys. *)
+(** This file provides utility functions for grouping association lists based on
+their keys, as well as basic theorems about them. *)
 From stdpp Require Export prelude.
 From Coq Require Export SetoidPermutation.
 
@@ -17,8 +17,8 @@ Fixpoint group {A} `{EqDecision K} (ixs : list (K * A)) : list (K * list A) :=
   | (i,x) :: ixs => group_insert i x (group ixs)
   end.
 
-Instance: Params (@group_insert) 5 := {}.
-Instance: Params (@group) 3 := {}.
+Global Instance: Params (@group_insert) 5 := {}.
+Global Instance: Params (@group) 3 := {}.
 
 Local Infix "≡ₚₚ" :=
   (PermutationA (prod_relation (=) (≡ₚ))) (at level 70, no associativity) : stdpp_scope.

theories/utils/llist.v → actris/utils/llist.v

-(** This file defines an encoding of lists in the [heap_lang]
-language, along with common functions such as append and split. *)
+(** This file defines a separation logic representation predicates [llist] for
+mutable linked-lists. It comes with a small library of operations (head, pop,
+lookup, length, append, prepend, snoc, split). *)
 From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import assert.
 
-(** Immutable ML-style functional lists *)
-Fixpoint llist `{heapG Σ} {A} (I : A → val → iProp Σ)
+(**  *)
+Fixpoint llist `{heapGS Σ} {A} (I : A → val → iProp Σ)
     (l : loc) (xs : list A) : iProp Σ :=
   match xs with
   | [] => l ↦ NONEV
@@ -74,8 +75,19 @@ Definition lsplit_at : val :=
 
 Definition lsplit : val := λ: "l", lsplit_at "l" (llength "l" `quot` #2).
 
+Definition lreverse_at : val :=
+  rec: "go" "l" "acc" :=
+    match: !"l" with
+      NONE => "acc"
+    | SOME "p" => (lcons (Fst "p") "acc");; "go" (Snd "p") "acc"
+    end.
+
+Definition lreverse : val :=
+  λ: "l", let: "l'" := ref (!"l") in
+          "l" <- !(lreverse_at "l'" (lnil #())).
+
 Section lists.
-Context `{heapG Σ} {A} (I : A → val → iProp Σ).
+Context `{heapGS Σ} {A} (I : A → val → iProp Σ).
 Implicit Types i : nat.
 Implicit Types xs : list A.
 Implicit Types l : loc.
@@ -138,7 +150,7 @@ Lemma lhead_spec l x xs :
     lhead #l
   {{{ v, RET v; I x v ∗ (I x v -∗ llist I l (x :: xs)) }}}.
 Proof.
-  iIntros (Φ) "Hll HΦ". wp_apply (lhead_spec_aux with "Hll").
+  iIntros (Φ) "Hll HΦ". wp_smart_apply (lhead_spec_aux with "Hll").
   iIntros (v l') "(HIx&?&?)". iApply "HΦ". iIntros "{$HIx} HIx".
   simpl; eauto with iFrame.
 Qed.
@@ -147,7 +159,7 @@ Lemma lpop_spec l x xs :
   {{{ llist I l (x :: xs) }}} lpop #l {{{ v, RET v; I x v ∗ llist I l xs }}}.
 Proof.
   iIntros (Φ) "/=". iDestruct 1 as (v l') "(HIx & Hl & Hll)". iIntros "HΦ".
-  wp_apply (lpop_spec_aux with "[$]"); iIntros "Hll". iApply "HΦ"; iFrame.
+  wp_smart_apply (lpop_spec_aux with "[$]"); iIntros "Hll". iApply "HΦ"; iFrame.
 Qed.
 
 Lemma llookup_spec l i xs x :
@@ -159,11 +171,11 @@ Proof.
   iIntros (Hi Φ) "Hll HΦ".
   iInduction xs as [|x' xs] "IH" forall (l i x Hi Φ); [done|simpl; wp_rec; wp_pures].
   destruct i as [|i]; simplify_eq/=; wp_pures.
-  - wp_apply (lhead_spec with "Hll"); iIntros (v) "[HI Hll]".
+  - wp_smart_apply (lhead_spec with "Hll"); iIntros (v) "[HI Hll]".
     iApply "HΦ"; eauto with iFrame.
   - iDestruct "Hll" as (v l') "(HIx' & Hl' & Hll)". wp_load; wp_pures.
     rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-    wp_apply ("IH" with "[//] Hll"); iIntros (v') "[HIx Hll]".
+    wp_smart_apply ("IH" with "[//] Hll"); iIntros (v') "[HIx Hll]".
     iApply "HΦ". iIntros "{$HIx} HIx". iExists v, l'. iFrame. by iApply "Hll".
 Qed.
 
@@ -174,14 +186,14 @@ Proof.
   iInduction xs as [|x xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
   - wp_load; wp_pures. by iApply "HΦ".
   - iDestruct "Hll" as (v l') "(HIx & Hl' & Hll)". wp_load; wp_pures.
-    wp_apply ("IH" with "Hll"); iIntros "Hll". wp_pures.
+    wp_smart_apply ("IH" with "Hll"); iIntros "Hll". wp_pures.
     rewrite (Nat2Z.inj_add 1). iApply "HΦ"; eauto with iFrame.
 Qed.
 
 Lemma lapp_spec l1 l2 xs1 xs2 :
   {{{ llist I l1 xs1 ∗ llist I l2 xs2 }}}
     lapp #l1 #l2
-  {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ l2 ↦ - }}}.
+  {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ (∃ v, l2 ↦ v) }}}.
 Proof.
   iIntros (Φ) "[Hll1 Hll2] HΦ".
   iInduction xs1 as [|x1 xs1] "IH" forall (l1 Φ); simpl; wp_rec; wp_pures.
@@ -190,17 +202,17 @@ Proof.
     + iDestruct "Hll2" as (v2 l2') "(HIx2 & Hl2 & Hll2)". wp_load. wp_store.
       iApply "HΦ". iSplitR "Hl2"; eauto 10 with iFrame.
   - iDestruct "Hll1" as (v1 l') "(HIx1 & Hl1 & Hll1)". wp_load; wp_pures.
-    wp_apply ("IH" with "Hll1 Hll2"); iIntros "[Hll Hl2]".
+    wp_smart_apply ("IH" with "Hll1 Hll2"); iIntros "[Hll Hl2]".
     iApply "HΦ"; eauto with iFrame.
 Qed.
 
 Lemma lprep_spec l1 l2 xs1 xs2 :
   {{{ llist I l1 xs2 ∗ llist I l2 xs1 }}}
     lprep #l1 #l2
-  {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ l2 ↦ - }}}.
+  {{{ RET #(); llist I l1 (xs1 ++ xs2) ∗ (∃ v, l2 ↦ v) }}}.
 Proof.
   iIntros (Φ) "[Hll1 Hll2] HΦ". wp_lam.
-  wp_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
+  wp_smart_apply (lapp_spec with "[$Hll2 $Hll1]"); iIntros "[Hll2 Hl1]".
   iDestruct "Hl1" as (w) "Hl1". destruct (xs1 ++ xs2) as [|x xs]; simpl; wp_pures.
   - wp_load. wp_store. iApply "HΦ"; eauto with iFrame.
   - iDestruct "Hll2" as (v l') "(HIx & Hl2 & Hll2)". wp_load. wp_store.
@@ -214,7 +226,7 @@ Proof.
   iInduction xs as [|x' xs] "IH" forall (l Φ); simpl; wp_rec; wp_pures.
   - wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
   - iDestruct "Hll" as (v' l') "(HIx' & Hl & Hll)". wp_load; wp_pures.
-    wp_apply ("IH" with "Hll HIx"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
+    wp_smart_apply ("IH" with "Hll HIx"); iIntros "Hll". iApply "HΦ"; eauto with iFrame.
 Qed.
 
 Lemma lsplit_at_spec l xs (n : nat) :
@@ -225,12 +237,12 @@ Proof.
   iIntros (Φ) "Hll HΦ".
   iInduction xs as [|x xs] "IH" forall (l n Φ); simpl; wp_rec; wp_pures.
   - destruct n as [|n]; simpl; wp_pures.
-    + wp_load. wp_alloc k. wp_store. iApply "HΦ"; iFrame.
-    + wp_load. wp_alloc k. iApply "HΦ"; iFrame.
+    + wp_load. wp_alloc k. wp_store. iApply "HΦ"; by iFrame.
+    + wp_load. wp_alloc k. iApply "HΦ"; by iFrame.
   - iDestruct "Hll" as (v l') "(HIx & Hl & Hll)". destruct n as [|n]; simpl; wp_pures.
     + wp_load. wp_alloc k. wp_store. iApply "HΦ"; eauto with iFrame.
     + wp_load; wp_pures. rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-      wp_apply ("IH" with "[$]"); iIntros (k) "[Hll Hlk]".
+      wp_smart_apply ("IH" with "[$]"); iIntros (k) "[Hll Hlk]".
       iApply "HΦ"; eauto with iFrame.
 Qed.
 
@@ -240,9 +252,52 @@ Lemma lsplit_spec l xs :
   {{{ k xs1 xs2, RET #k; ⌜ xs = xs1 ++ xs2 ⌝ ∗ llist I l xs1 ∗ llist I k xs2 }}}.
 Proof.
   iIntros (Φ) "Hl HΦ". wp_lam.
-  wp_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
-  rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Z2Nat_inj_div _ 2).
-  wp_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
+  wp_smart_apply (llength_spec with "Hl"); iIntros "Hl". wp_pures.
+  rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Nat2Z.inj_div _ 2).
+  wp_smart_apply (lsplit_at_spec with "Hl"); iIntros (k) "[Hl Hk]".
   iApply "HΦ". iFrame. by rewrite take_drop.
 Qed.
+
+Lemma lreverse_at_spec l xs acc ys :
+  {{{ llist I l xs ∗ llist I acc ys }}}
+    lreverse_at #l #acc
+  {{{ l', RET #l'; llist I l' (reverse xs ++ ys) }}}.
+Proof.
+  iIntros (Φ) "[Hl Hacc] HΦ".
+  iInduction xs as [|x xs] "IH" forall (l acc Φ ys); simpl; wp_lam.
+  - wp_load. wp_pures. iApply "HΦ". iApply "Hacc".
+  - iDestruct "Hl" as (v l') "[HI [Hl Hl']]".
+    wp_load. wp_smart_apply (lcons_spec with "[$Hacc $HI]").
+    iIntros "Hacc". wp_smart_apply ("IH" with "Hl' Hacc").
+    iIntros (l'') "Hl''". iApply "HΦ".
+    rewrite reverse_cons -assoc_L. iApply "Hl''".
+Qed.
+
+Lemma lreverse_spec l xs :
+  {{{ llist I l xs }}}
+    lreverse #l
+  {{{ RET #(); llist I l (reverse xs) }}}.
+Proof.
+  iIntros (Φ) "Hl HΦ". wp_lam.
+  destruct xs as [|x xs]; simpl.
+  - wp_load. wp_alloc l' as "Hl'".
+    wp_smart_apply (lnil_spec with "[//]").
+    iIntros (lnil) "Hlnil".
+    iAssert (llist I l' []) with "Hl'" as "Hl'".
+    wp_smart_apply (lreverse_at_spec with "[$Hl' $Hlnil]").
+    iIntros (l'') "Hl''".
+    wp_load. wp_store. iApply "HΦ". rewrite right_id_L. iApply "Hl".
+  - iDestruct "Hl" as (v lcons) "[HI [Hlcons Hrec]]".
+    wp_load. wp_alloc l' as "Hl'".
+    wp_smart_apply (lnil_spec with "[//]").
+    iIntros (lnil) "Hlnil".
+    wp_smart_apply (lreverse_at_spec _ (x :: xs) with "[Hl' HI Hrec $Hlnil]").
+    { simpl; eauto with iFrame. }
+    iIntros (l'') "Hl''". rewrite right_id_L. destruct (reverse _) as [|y ys].
+    + wp_load. wp_store. by iApply "HΦ".
+    + simpl. iDestruct "Hl''" as (v' lcons') "[HI [Hcons Hrec]]".
+      wp_load. wp_store.
+      iApply "HΦ". eauto with iFrame.
+Qed.
+
 End lists.

actris/utils/switch.v

+From stdpp Require Import pretty.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import metatheory proofmode notation assert.
+Set Default Proof Using "Type".
+
+Fixpoint switch_body (y : string) (i : nat) (xs : list Z)
+    (edef : expr) (ecase : nat → expr) : expr :=
+  match xs with
+  | [] => edef
+  | x :: xs => if: y = #x then ecase i
+               else switch_body y (S i) xs edef ecase
+  end.
+Fixpoint switch_lams (y : string) (i : nat) (n : nat) (e : expr) : expr :=
+  match n with
+  | O => e
+  | S n => λ: (y +:+ pretty i), switch_lams y (S i) n e
+  end.
+Definition switch_fail (xs : list Z) : val := λ: "y",
+  switch_lams "f" 0 (length xs) $
+    switch_body "y" 0 xs (assert: #false) $ λ i, ("f" +:+ pretty i) #().
+
+Fixpoint map_string_seq {A}
+    (s : string) (start : nat) (xs : list A) : gmap string A :=
+  match xs with
+  | [] => ∅
+  | x :: xs => <[s+:+pretty start:=x]> (map_string_seq s (S start) xs)
+  end.
+
+Lemma lookup_map_string_seq_Some {A} (j i : nat) (xs : list A) :
+  map_string_seq "f" j xs !! ("f" +:+ pretty (i + j)) = xs !! i.
+Proof.
+  revert i j. induction xs as [|x xs IH]=> -[|i] j //=.
+  - by rewrite lookup_insert.
+  - rewrite lookup_insert_ne; last (intros ?; simplify_eq/=; lia).
+    by rewrite -Nat.add_succ_r IH.
+Qed.
+
+Lemma lookup_map_string_seq_None {A} y j z (vs : list A) :
+  (∀ i : nat, y +:+ pretty i ≠ z) →
+  map_string_seq y j vs !! z = None.
+Proof.
+  intros. revert j. induction vs as [|v vs IH]=> j //=.
+  by rewrite lookup_insert_ne.
+Qed.
+
+Lemma lookup_map_string_seq_None_lt {A} y i j (xs : list A) :
+  i < j → map_string_seq y j xs !! (y +:+ pretty i) = None.
+Proof.
+  revert j. induction xs as [|x xs IH]=> j ? //=.
+  rewrite lookup_insert_ne; last (intros ?; simplify_eq/=; lia).
+  apply IH. lia.
+Qed.
+
+Lemma switch_lams_spec `{heapGS Σ} y i n ws vs e Φ :
+  length vs = n →
+  WP subst_map (map_string_seq y i vs ∪ ws) e {{ Φ }} -∗
+  WP subst_map ws (switch_lams y i n e) {{ w, WP fill (AppLCtx <$> vs) (of_val w) {{ Φ }} }}.
+  (* FIXME: Once we depend on Coq 8.13, make WP notation use [v closed binder]
+       so that we can add a type annotation at the [w] binder here. *)
+Proof.
+  iIntros (<-) "H".
+  iInduction vs as [|v vs] "IH" forall (i ws); csimpl.
+  { rewrite left_id_L.
+    iApply (wp_wand with "H"); iIntros (v) "H". by iApply wp_value. }
+  pose proof @pure_exec_fill.
+  wp_pures. iApply wp_bind.
+  iEval (rewrite -subst_map_insert insert_union_singleton_l).
+  iApply "IH". rewrite assoc_L insert_union_singleton_r //
+    lookup_map_string_seq_None_lt; auto with lia.
+Qed.
+
+Lemma switch_body_spec `{heapGS Σ} y xs i j ws (x : Z) edef ecase Φ :
+  fst <$> list_find (x =.) xs = Some i →
+  ws !! y = Some #x →
+  WP subst_map ws (ecase (i + j)%nat) {{ Φ }} -∗
+  WP subst_map ws (switch_body y j xs edef ecase) {{ Φ }}.
+Proof.
+  iIntros (Hi Hy) "H".
+  iInduction xs as [|x' xs] "IH" forall (i j Hi); simplify_eq/=.
+  rewrite Hy. case_decide; simplify_eq/=; wp_pures.
+  { rewrite bool_decide_true; last congruence. by wp_pures. }
+  move: Hi=> /fmap_Some [[??] [/fmap_Some [[i' x''] [??]] ?]]; simplify_eq/=.
+  rewrite bool_decide_false; last congruence. wp_pures.
+  iApply ("IH" $! i'). by simplify_option_eq. by rewrite Nat.add_succ_r.
+Qed.
+
+Lemma switch_fail_spec `{heapGS Σ} vfs xs i (x : Z) (vf : val) Φ :
+  length vfs = length xs →
+  fst <$> list_find (x =.) xs = Some i →
+  vfs !! i = Some vf →
+  ▷ WP vf #() {{ Φ }} -∗
+  WP fill (AppLCtx <$> vfs) (switch_fail xs #x) {{ Φ }}.
+Proof.
+  iIntros (???) "H". iApply wp_bind. wp_lam.
+  rewrite -subst_map_singleton. iApply switch_lams_spec; first done.
+  iApply switch_body_spec; [done|..].
+  - by rewrite lookup_union_r ?lookup_singleton // lookup_map_string_seq_None.
+  - by rewrite /= (lookup_union_Some_l _ _ _ vf) // lookup_map_string_seq_Some.
+Qed.

coq-actris.opam

+opam-version: "2.0"
+maintainer: "Robbert Krebbers"
+synopsis: "Actris: Session protocol reasoning in Iris"
+homepage: "https://gitlab.mpi-sws.org/iris/actris"
+authors: "Jonas Kastberg Hinrichsen, Daniël Louwrink, Jesper Bengtson, Robbert Krebbers"
+license: "BSD-3-Clause"
+bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
+
+depends: [
+  "coq-iris-heap-lang" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
+]
+
+build: ["./make-package" "actris" "-j%{jobs}%"]
+install: ["./make-package" "actris"  "install"]

experimental/encodable.v

-From iris.heap_lang Require Export notation.
-
-Class ValEnc A := val_encode : A → val.
-Class ValDec A := val_decode : val → option A.
-Class ValEncDec A `{!ValEnc A, !ValDec A} := {
-  val_encode_decode v : val_decode (val_encode v) = Some v;
-  val_decode_encode v x : val_decode v = Some x → val_encode x = v;
-}.
-
-Local Arguments val_encode _ _ !_ /.
-Local Arguments val_decode _ _ !_ /.
-
-Lemma val_encode_decode_iff `{ValEncDec A} v x :
-  val_encode x = v ↔ val_decode v = Some x.
-Proof.
-  split; last apply val_decode_encode. intros <-. by rewrite -val_encode_decode.
-Qed.
-Instance val_encode_inj `{ValEncDec A} : Inj (=) (=) val_encode.
-Proof.
-  intros x y Heq. apply (inj Some).
-  by rewrite -(val_encode_decode x) Heq val_encode_decode.
-Qed.
-
-(* Instances *)
-Instance val_val_enc : ValEnc val := id.
-Instance val_val_dec : ValDec val := id $ Some.
-Instance val_val_enc_dec : ValEncDec val.
-Proof. split. done. by intros ?? [= ->]. Qed.
-
-Instance int_val_enc : ValEnc Z := λ n, #n.
-Instance int_val_dec : ValDec Z := λ v,
-  match v with LitV (LitInt z) => Some z | _ => None end.
-Instance int_val_enc_dec : ValEncDec Z.
-Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
-
-Instance bool_val_enc : ValEnc bool := λ b, #b.
-Instance bool_val_dec : ValDec bool := λ v,
-  match v with LitV (LitBool b) => Some b | _ => None end.
-Instance bool_val_enc_dec : ValEncDec bool.
-Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
-
-Instance loc_val_enc : ValEnc loc := λ l, #l.
-Instance loc_val_dec : ValDec loc := λ v,
-  match v with LitV (LitLoc l) => Some l | _ => None end.
-Instance loc_val_enc_dec : ValEncDec loc.
-Proof. split. done. by intros [[]| | | |] ? [= ->]. Qed.
-
-Instance unit_val_enc : ValEnc unit := λ _, #().
-Instance unit_val_dec : ValDec unit := λ v,
-  match v with LitV LitUnit => Some () | _ => None end.
-Instance unit_val_enc_dec : ValEncDec unit.
-Proof. split. by intros []. by intros [[]| | | |] ? [= <-]. Qed.
-
-Instance pair_val_enc `{ValEnc A, ValEnc B} : ValEnc (A * B) := λ p,
-  (val_encode p.1, val_encode p.2)%V.
-Arguments pair_val_enc {_ _ _ _} !_ /.
-Instance pair_val_dec `{ValDec A, ValDec B} : ValDec (A * B) := λ v,
-  match v with
-  | PairV v1 v2 => x1 ← val_decode v1; x2 ← val_decode v2; Some (x1, x2)
-  | _ => None
-  end.
-Arguments pair_val_dec {_ _ _ _} !_ /.
-Instance pair_val_enc_dec `{ValEncDec A, ValEncDec B} : ValEncDec (A * B).
-Proof.
-  split.
-  - intros []. by rewrite /= val_encode_decode /= val_encode_decode.
-  - intros [] ??; simplify_option_eq;
-      by repeat match goal with
-      | H : val_decode _ = Some _ |- _ => apply val_decode_encode in H as <-
-      end.
-Qed.
-
-Instance option_val_enc `{ValEnc A} : ValEnc (option A) := λ mx,
-  match mx with Some x => SOMEV (val_encode x) | None => NONEV end%V.
-Arguments option_val_enc {_ _} !_ /.
-Instance option_val_dec `{ValDec A} : ValDec (option A) := λ v,
-  match v with
-  | SOMEV v => x ← val_decode v; Some (Some x)
-  | NONEV => Some None
-  | _ => None
-  end.
-Arguments option_val_dec {_ _} !_ /.
-Instance option_val_enc_dec `{ValEncDec A} : ValEncDec (option A).
-Proof.
-  split.
-  - intros []=> //. by rewrite /= val_encode_decode.
-  - intros [] ??; repeat (simplify_option_eq || case_match);
-      by repeat match goal with
-      | H : val_decode _ = Some _ |- _ => apply val_decode_encode in H as <-
-      end.
-Qed.

experimental/flist.v

-From iris.heap_lang Require Export proofmode notation.
-From iris.heap_lang Require Import assert.
-
-(** Immutable ML-style functional lists *)
-Fixpoint flist (vs : list val) : val :=
-  match vs with
-  | [] => NONEV
-  | v :: vs => SOMEV (v,flist vs)
-  end%V.
-Arguments flist : simpl never.
-
-Definition fnil : val := λ: <>, NONEV.
-Definition fcons : val := λ: "x" "l", SOME ("x", "l").
-
-Definition fisnil : val := λ: "l",
-  match: "l" with
-    SOME "p" => #false
-  | NONE => #true
-  end.
-
-Definition fhead : val := λ: "l",
-  match: "l" with
-    SOME "p" => Fst "p"
-  | NONE => assert: #false
-  end.
-
-Definition ftail : val := λ: "l",
-  match: "l" with
-    SOME "p" => Snd "p"
-  | NONE => assert: #false
-  end.
-
-Definition flookup : val :=
-  rec: "go" "n" "l" :=
-    if: "n" = #0 then fhead "l" else
-    let: "l" := ftail "l" in "go" ("n" - #1) "l".
-
-Definition finsert : val :=
-  rec: "go" "n" "x" "l" :=
-    if: "n" = #0 then let: "l" := ftail "l" in fcons "x" "l" else
-    let: "k" := ftail "l" in
-    let: "k" := "go" ("n" - #1) "x" "k" in
-    fcons (fhead "l") "k".
-
-Definition freplicate : val :=
-  rec: "go" "n" "x" :=
-    if: "n" = #0 then fnil #() else
-    let: "l" := "go" ("n" - #1) "x" in fcons "x" "l".
-
-Definition flength : val :=
-  rec: "go" "l" :=
-    match: "l" with
-      NONE => #0
-    | SOME "p" => #1 + "go" (Snd "p")
-    end.
-
-Definition fapp : val :=
-  rec: "go" "l" "k" :=
-    match: "l" with
-      NONE => "k"
-    | SOME "p" => fcons (Fst "p") ("go" (Snd "p") "k")
-    end.
-
-Definition fsnoc : val := λ: "l" "x", fapp "l" (fcons "x" (fnil #())).
-
-Definition ftake : val :=
-  rec: "go" "l" "n" :=
-    if: "n" ≤ #0 then NONEV else
-    match: "l" with
-      NONE => NONEV
-    | SOME "l" => fcons (Fst "l") ("go" (Snd "l") ("n"-#1))
-    end.
-
-Definition fdrop : val :=
-  rec: "go" "l" "n" :=
-    if: "n" ≤ #0 then "l" else
-    match: "l" with
-      NONE => NONEV
-    | SOME "l" => "go" (Snd "l") ("n"-#1)
-    end.
-
-Definition fsplit_at : val := λ: "l" "n", (ftake "l" "n", fdrop "l" "n").
-
-Definition fsplit : val := λ: "l", fsplit_at "l" (flength "l" `quot` #2).
-
-Section lists.
-Context `{heapG Σ}.
-Implicit Types i : nat.
-Implicit Types v : val.
-Implicit Types vs : list val.
-
-Lemma fnil_spec :
-  {{{ True }}} fnil #() {{{ RET flist []; True }}}.
-Proof. iIntros (Φ _) "HΦ". wp_lam. by iApply "HΦ". Qed.
-
-Lemma fcons_spec v vs :
-  {{{ True }}} fcons v (flist vs) {{{ RET flist (v :: vs); True }}}.
-Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
-
-Lemma fisnil_spec vs:
-  {{{ True }}}
-    fisnil (flist vs)
-  {{{ RET #(if vs is [] then true else false); True }}}.
-Proof. iIntros (Φ _) "HΦ". wp_lam. destruct vs; wp_pures; by iApply "HΦ". Qed.
-
-Lemma fhead_spec v vs :
-  {{{ True }}} fhead (flist (v :: vs)) {{{ RET v; True }}}.
-Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
-
-Lemma ftail_spec v vs :
-  {{{ True }}} ftail (flist (v :: vs)) {{{ RET flist vs; True }}}.
-Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
-
-Lemma flookup_spec i vs v :
-  vs !! i = Some v →
-  {{{ True }}} flookup #i (flist vs) {{{ RET v; True }}}.
-Proof.
-  iIntros (Hi Φ _) "HΦ".
-  iInduction vs as [|v' vs] "IH" forall (i Hi);
-    destruct i as [|i]=> //; simplify_eq/=.
-  { wp_lam. wp_pures. by iApply (fhead_spec with "[//]"). }
-  wp_lam. wp_pures.
-  wp_apply (ftail_spec with "[//]"); iIntros (_). wp_let.
-  wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l. by iApply "IH".
-Qed.
-
-Lemma finsert_spec i vs v :
-  is_Some (vs !! i) →
-  {{{ True }}} finsert #i v (flist vs) {{{ RET flist (<[i:=v]>vs); True }}}.
-Proof.
-  iIntros ([w Hi] Φ _) "HΦ".
-  iInduction vs as [|v' vs] "IH" forall (i Hi Φ);
-    destruct i as [|i]=> //; simplify_eq/=.
-  { wp_lam. wp_pures. wp_apply (ftail_spec with "[//]"); iIntros (_).
-    wp_let. by iApply (fcons_spec with "[//]"). }
-  wp_lam; wp_pures.
-  wp_apply (ftail_spec with "[//]"); iIntros (_). wp_let.
-  wp_op. rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
-  wp_apply ("IH" with "[//]"); iIntros (_).
-  wp_apply (fhead_spec with "[//]"); iIntros "_".
-  by wp_apply (fcons_spec with "[//]").
-Qed.
-
-Lemma freplicate_spec i v :
-  {{{ True }}} freplicate #i v {{{ RET flist (replicate i v); True }}}.
-Proof.
-  iIntros (Φ _) "HΦ". iInduction i as [|i] "IH" forall (Φ); simpl.
-  { wp_lam; wp_pures. iApply (fnil_spec with "[//]"); auto. }
-  wp_lam; wp_pures.
-  rewrite Nat2Z.inj_succ -Z.add_1_l Z.add_simpl_l.
-  wp_apply "IH"; iIntros (_). wp_let. by iApply (fcons_spec with "[//]").
-Qed.
-
-Lemma flength_spec vs :
-  {{{ True }}} flength (flist vs) {{{ RET #(length vs); True }}}.
-Proof.
-  iIntros (Φ _) "HΦ".
-  iInduction vs as [|v' vs] "IH" forall (Φ); simplify_eq/=.
-  { wp_lam. wp_match. by iApply "HΦ". }
-  wp_lam. wp_match. wp_proj.
-  wp_apply "IH"; iIntros "_ /=". wp_op.
-  rewrite (Nat2Z.inj_add 1). by iApply "HΦ".
-Qed.
-
-Lemma fapp_spec vs1 vs2 :
-  {{{ True }}} fapp (flist vs1) (flist vs2) {{{ RET (flist (vs1 ++ vs2)); True }}}.
-Proof.
-  iIntros (Φ _) "HΦ".
-  iInduction vs1 as [|v1 vs1] "IH" forall (Φ); simpl.
-  { wp_rec. wp_pures. by iApply "HΦ". }
-  wp_rec. wp_pures. wp_apply "IH". iIntros (_). by wp_apply fcons_spec.
-Qed.
-
-Lemma fsnoc_spec vs v :
-  {{{ True }}} fsnoc (flist vs) v {{{ RET (flist (vs ++ [v])); True }}}.
-Proof.
-  iIntros (Φ _) "HΦ". wp_lam. wp_apply (fnil_spec with "[//]"); iIntros (_).
-  wp_apply (fcons_spec with "[//]"); iIntros (_).
-  wp_apply (fapp_spec with "[//]"); iIntros (_). by iApply "HΦ".
-Qed.
-
-Lemma ftake_spec vs (n : nat) :
-  {{{ True }}} ftake (flist vs) #n {{{ RET flist (take n vs); True }}}.
-Proof.
-  iIntros (Φ _) "HΦ".
-  iInduction vs as [|x' vs] "IH" forall (n Φ).
-  - wp_rec. wp_pures.
-    destruct (bool_decide (n ≤ 0)); wp_pures; rewrite take_nil; by iApply "HΦ".
-  - wp_rec; destruct n as [|n]; wp_pures; first by iApply "HΦ".
-    rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-    wp_apply "IH"; iIntros (_).
-    wp_apply (fcons_spec with "[//]"); iIntros (_). by iApply "HΦ".
-Qed.
-
-Lemma fdrop_spec vs (n : nat) :
-  {{{ True }}} fdrop (flist vs) #n {{{ RET flist (drop n vs); True }}}.
-Proof.
-  iIntros (Φ _) "HΦ".
-  iInduction vs as [|x' vs] "IH" forall (n Φ).
-  - wp_rec. wp_pures.
-    destruct (bool_decide (n ≤ 0)); wp_pures; rewrite drop_nil; by iApply "HΦ".
-  - wp_rec; destruct n as [|n]; wp_pures; first by iApply "HΦ".
-    rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
-    wp_apply "IH"; iIntros (_). by iApply "HΦ".
-Qed.
-
-Lemma fsplit_at_spec vs (n : nat) :
-  {{{ True }}}
-    fsplit_at (flist vs) #n
-  {{{ RET (flist (take n vs), flist (drop n vs)); True }}}.
-Proof.
-  iIntros (Φ _) "HΦ". wp_lam.
-  wp_apply (fdrop_spec with "[//]"); iIntros (_).
-  wp_apply (ftake_spec with "[//]"); iIntros (_).
-  wp_pures. by iApply "HΦ".
-Qed.
-
-Lemma fsplit_spec vs :
-  {{{ True }}}
-    fsplit (flist vs)
-  {{{ ws1 ws2, RET (flist ws1, flist ws2); ⌜ vs = ws1 ++ ws2 ⌝ }}}.
-Proof.
-  iIntros (Φ _) "HΦ". wp_lam.
-  wp_apply (flength_spec with "[//]"); iIntros (_). wp_pures.
-  rewrite Z.quot_div_nonneg; [|lia..]. rewrite -(Z2Nat_inj_div _ 2).
-  wp_apply (fsplit_at_spec with "[//]"); iIntros (_).
-  iApply "HΦ". by rewrite take_drop.
-Qed.
-End lists.

experimental/producer_consumer.v

-From stdpp Require Import sorting.
-From actris.channel Require Import proto_channel proofmode.
-From iris.heap_lang Require Import proofmode notation.
-From iris.heap_lang Require Import assert.
-From actris.utils Require Import list compare spin_lock.
-
-Definition qenqueue : val := λ: "q" "v", #().
-Definition qdequeue : val := λ: "q", #().
-
-Definition enq := true.
-Definition deq := false.
-
-Definition cont := true.
-Definition stop := false.
-
-Definition some := true.
-Definition none := false.
-
-Definition pd_loop : val :=
-  rec: "go" "q" "pc" "cc" "c" :=
-    if: "cc" ≤ #0 then #() else 
-    if: recv "c" then (* enq/deq *)
-      if: recv "c" then (* cont/stop *)
-        let: "x" := recv "x" in
-        "go" (qenqueue "q" "x") "pc" "cc" "c"
-      else "go" "q" ("pc"-#1) "cc" "c"
-    else
-      if: lisnil "q" then
-        if: "pc" ≤ #0 then
-          send "c" #stop;;
-          "go" "q" "pc" ("cc"-#1) "c"
-        else
-          send "c" #cont;; send "c" #none;;
-          "go" "q" "pc" "cc" "c"
-      else
-        send "c" #cont;; send "c" #some;;
-        let: "qv" := qdequeue "q" in
-        send "c" (Snd "qv");;
-        "go" (Fst "qv") "pc" "cc" "c".
-
-Definition new_pd : val := λ: "pc" "cc",
-  let: "q" := lnil #() in
-  let: "c" := start_chan (λ: "c", pd_loop "q" "pc" "cc" "c") in
-  let: "l" := new_lock #() in
-  ("c", "l").
-
-Definition pd_send : val := λ: "cl" "x",
-  acquire (Snd "cl");;
-  send (Fst "cl") #enq;; send (Fst "cl") #cont;; send (Fst "cl") "x";;
-  release (Snd "cl").
-
-Definition pd_stop : val := λ: "cl",
-  acquire (Fst "cl");;
-  send (Snd "cl") #enq;; send (Snd "cl") #stop;;
-  release (Fst "cl").
-
-Definition pd_recv : val :=
-  rec: "go" "cl" :=
-    acquire (Fst "cl");;
-    send (Snd "cl") #deq;;
-    if: recv (Snd "cl") then    (* cont/stop *)
-       if: recv (Snd "cl") then (* some/none *)
-         let: "v" := recv (Snd "cl") in
-         release (Fst "cl");; SOME "v"
-       else release (Fst "cl");; "go" "c" "l"
-    else release (Fst "cl");; NONE.
-
-Section sort_elem.
-  Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
-
-  Definition queue_prot : iProto Σ := (END)%proto.
-
-  Lemma dist_queue_spec c :
-    {{{ c ↣ queue_prot @ N }}}
-      dist_queue (qnew #()) #0 #0 c
-    {{{ RET #(); c ↣ END @ N }}}.
-  Proof. Admitted.
-
-  (* Need predicate for end of production? *)
-  Definition produce_spec σ P (produce : val) :=
-    ∀ vs,
-    {{{ σ vs }}}
-      produce #()
-    {{{ v, RET v; (∃ w, ⌜v = SOMEV w⌝ ∧ P w ∗ σ (w::vs)) ∨ (⌜v = NONEV⌝) }}}.
-
-  Definition consume_spec σ P Q (consume : val) :=
-    ∀ vs, ∀ v : val,
-    {{{ σ vs ∗ P v }}}
-      consume v
-    {{{ RET #(); σ (v::vs) ∗ Q v }}}.
-
-  Lemma produce_consume_spec produce consume pσ cσ P Q pc cc :
-    pc > 0 → cc > 0 → 
-    produce_spec pσ P produce →
-    consume_spec cσ P Q consume →
-    {{{ pσ [] ∗ cσ [] }}}
-      produce_consume produce consume #pc #cc
-    {{{ vs, RET #(); pσ vs ∗ cσ vs ∗ [∗ list] v ∈ vs, Q v }}}.
-  Proof. Admitted.
-
-  (* Example producer *)
-  Definition ints_to_n (l : val) (n:nat) : val:=
-    λ: <>, let: "v" := !l in
-           if: "v" < #n
-           then l <- "v" + #1;; SOME "v"
-           else NONE.
-
-  Lemma ints_to_n_spec l n :
-    produce_spec (λ vs, (∃ loc, ⌜loc = LitV $ LitLoc l⌝ ∗ l ↦ #(length vs))%I)
-                 (λ v, ⌜∃ i, v = LitV $ LitInt i⌝%I) (ints_to_n #l n).
-  Proof.
-    iIntros (vs Φ) "Hσ HΦ".
-    iDestruct "Hσ" as (loc ->) "Hσ".
-    wp_lam. wp_load. wp_pures.
-    case_bool_decide.
-    - wp_store. wp_pures. iApply "HΦ".
-      (* Does this not exist? *)
-      assert (∀ n : nat, (n + 1) = (S n)). intros m. lia. rewrite H0.
-      by eauto 10 with iFrame.
-    - wp_pures. iApply "HΦ". by iRight.
-  Qed.
-
-  Definition consume_to_list l : val:=
-    λ: "v", 
-      let: "xs" := !l in
-      l <- lcons "v" "xs".
-
-  Lemma consume_to_list_spec l :
-    consume_spec (λ vs, (∃ loc, ⌜loc = LitV $ LitLoc l⌝ ∗ l ↦ val_encode vs)%I)
-                 (λ v, ⌜True⌝%I) (λ v, ⌜True⌝%I) (consume_to_list #l).
-  Proof. Admitted.

experimental/spin_lock.v

-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl auth frac csum.
-From iris.base_logic.lib Require Import cancelable_invariants.
-From iris.bi.lib Require Import fractional.
-Set Default Proof Using "Type".
-
-Definition new_lock : val := λ: <>, ref #false.
-Definition try_acquire : val := λ: "l", CAS "l" #false #true.
-Definition acquire : val :=
-  rec: "acquire" "l" := if: try_acquire "l" then #() else "acquire" "l".
-Definition release : val := λ: "l", "l" <- #false.
-
-Class lockG Σ := LockG {
-  lock_tokG :> inG Σ (authR (optionUR (exclR fracR)));
-  lock_cinvG :> cinvG Σ;
-}.
-Definition lockΣ : gFunctors := #[GFunctor (authR (optionUR (exclR fracR))); cinvΣ].
-
-Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
-Proof. solve_inG. Qed.
-
-Section proof.
-  Context `{!heapG Σ, !lockG Σ} (N : namespace).
-
-  Definition lock_inv (γ γi : gname) (lk : loc) (R : iProp Σ) : iProp Σ :=
-    (∃ b : bool, lk ↦ #b ∗
-                 if b then (∃ p, own γ (● (Excl' p)) ∗ cinv_own γi (p/2))
-                 else own γ (● None) ∗ R)%I.
-
-  Definition is_lock (lk : loc) (R : iProp Σ) : iProp Σ :=
-    (∃ γ γi : gname, meta lk N (γ,γi) ∗ cinv N γi (lock_inv γ γi lk R))%I.
-
-  Definition unlocked (lk : loc) (q : Qp) : iProp Σ :=
-    (∃ γ γi : gname, meta lk N (γ,γi) ∗ cinv_own γi q)%I.
-
-  Definition locked (lk : loc) (q : Qp) : iProp Σ :=
-    (∃ γ γi : gname, meta lk N (γ,γi) ∗ cinv_own γi (q/2) ∗ own γ (◯ (Excl' q)))%I.
-
-  Global Instance unlocked_fractional lk : Fractional (unlocked lk).
-  Proof.
-    intros q1 q2. iSplit.
-    - iDestruct 1 as (γ γi) "[#Hm [Hq Hq']]". iSplitL "Hq"; iExists γ, γi; by iSplit.
-    - iIntros "[Hq1 Hq2]". iDestruct "Hq1" as (γ γi) "[#Hm Hq1]".
-      iDestruct "Hq2" as (γ' γi') "[#Hm' Hq2]".
-      iDestruct (meta_agree with "Hm Hm'") as %[= <- <-].
-      iExists γ, γi; iSplit; first done. by iSplitL "Hq1".
-  Qed.
-  Global Instance unlocked_as_fractional γ :
-    AsFractional (unlocked γ p) (unlocked γ) p.
-  Proof. split. done. apply _. Qed.
-
-  Global Instance lock_inv_ne γ γi lk : NonExpansive (lock_inv γ γi lk).
-  Proof. solve_proper. Qed.
-  Global Instance is_lock_ne lk : NonExpansive (is_lock lk).
-  Proof. solve_proper. Qed.
-
-  Global Instance is_lock_persistent lk R : Persistent (is_lock lk R).
-  Proof. apply _. Qed.
-  Global Instance locked_timeless lk q : Timeless (locked lk q).
-  Proof. apply _. Qed.
-  Global Instance unlocked_timeless lk q : Timeless (unlocked lk q).
-  Proof. apply _. Qed.
-
-  Lemma lock_cancel E lk R : ↑ N ⊆ E → is_lock lk R -∗ unlocked lk 1 ={E}=∗ ▷ R.
-  Proof.
-    intros. iDestruct 1 as (γ γi) "#[Hm Hinv]". iDestruct 1 as (γ' γi') "[Hm' Hq]".
-    iDestruct (meta_agree with "Hm Hm'") as %[= <- <-]; iClear "Hm'".
-    iMod (cinv_open_strong with "[$] [$]") as "(HR & Hq & Hclose)"; first done.
-    iDestruct "HR" as ([]) "[Hl HR]".
-    - iDestruct "HR" as (p) "[_ Hq']". iDestruct (cinv_own_1_l with "Hq Hq'") as ">[]".
-    - iDestruct "HR" as "[_ $]". iApply "Hclose"; auto.
-  Qed.
-
-  Lemma new_lock_spec :
-    {{{ True }}}
-      new_lock #()
-    {{{ lk, RET #lk; unlocked lk 1 ∗ (∀ R, R ={⊤}=∗ is_lock lk R) }}}.
-  Proof.
-    iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam.
-    wp_apply (wp_alloc with "[//]"); iIntros (l) "[Hl Hm]".
-    iDestruct (meta_token_difference _ (↑N) with "Hm") as "[Hm1 Hm2]"; first done.
-    iMod (own_alloc (● None)) as (γ) "Hγ"; first by apply auth_auth_valid.
-    iMod (cinv_alloc_strong (λ _, True))
-      as (γi _) "[Hγi H]"; first by apply pred_infinite_True.
-    iMod (meta_set _ _ (γ,γi) with "Hm1") as "#Hm1"; first done.
-    iApply "HΦ"; iSplitL "Hγi"; first by (iExists γ, γi; auto).
-    iIntros "!>" (R) "HR".
-    iMod ("H" $! (lock_inv γ γi l R) with "[HR Hl Hγ]") as "#?".
-    { iIntros "!>". iExists false. by iFrame. }
-    iModIntro. iExists γ, γi; auto.
-  Qed.
-
-  Lemma try_acquire_spec lk R q :
-    {{{ is_lock lk R ∗ unlocked lk q }}}
-      try_acquire #lk
-    {{{ b, RET #b; if b is true then locked lk q ∗ R else unlocked lk q }}}.
-  Proof.
-    iIntros (Φ) "[#Hl Hq] HΦ". iDestruct "Hl" as (γ γi) "#[Hm Hinv]".
-    iDestruct "Hq" as (γ' γi') "[Hm' Hq]".
-    iDestruct (meta_agree with "Hm Hm'") as %[= <- <-]; iClear "Hm'".
-    wp_rec. wp_bind (CmpXchg _ _ _).
-    iInv N as "[HR Hq]"; iDestruct "HR" as ([]) "[Hl HR]".
-    - wp_cmpxchg_fail. iModIntro. iSplitL "Hl HR"; first (iExists true; iFrame).
-      wp_pures. iApply ("HΦ" $! false). iExists γ, γi; auto.
-    - wp_cmpxchg_suc. iDestruct "HR" as "[Hγ HR]". iDestruct "Hq" as "[Hq Hq']".
-      iMod (own_update with "Hγ") as "[Hγ Hγ']".
-      { by apply auth_update_alloc, (alloc_option_local_update (Excl q)). }
-      iModIntro. iSplitL "Hl Hγ Hq"; first (iNext; iExists true; eauto with iFrame).
-      wp_pures. iApply ("HΦ" $! true with "[$HR Hγ' Hq']"). iExists γ, γi; by iFrame.
-  Qed.
-
-  Lemma acquire_spec lk R q :
-    {{{ is_lock lk R ∗ unlocked lk q }}} acquire #lk {{{ RET #(); locked lk q ∗ R }}}.
-  Proof.
-    iIntros (Φ) "[#Hlk Hq] HΦ". iLöb as "IH". wp_rec.
-    wp_apply (try_acquire_spec with "[$Hlk $Hq]"); iIntros ([]).
-    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
-    - iIntros "Hq". wp_if. iApply ("IH" with "[$]"); auto.
-  Qed.
-
-  Lemma release_spec lk R q :
-    {{{ is_lock lk R ∗ locked lk q ∗ R }}} release #lk {{{ RET #(); unlocked lk q }}}.
-  Proof.
-    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
-    iDestruct "Hlock" as (γ γi) "#[Hm Hinv]".
-    iDestruct "Hlocked" as (γ' γi') "(#Hm' & Hq & Hγ')".
-    iDestruct (meta_agree with "Hm Hm'") as %[= <- <-].
-    wp_lam. iInv N as "[HR' Hq]"; iDestruct "HR'" as ([]) "[Hl HR']".
-    - iDestruct "HR'" as (p) ">[Hγ Hq']".
-      iDestruct (own_valid_2 with "Hγ Hγ'")
-        as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
-      iMod (own_update_2 with "Hγ Hγ'") as "Hγ".
-      { eapply auth_update_dealloc, delete_option_local_update; apply _. }
-      wp_store. iIntros "!>". iSplitL "Hl Hγ HR"; first (iExists false); iFrame.
-      iApply "HΦ". iExists γ, γi. iSplit; first done. by iSplitL "Hq".
-    - iDestruct "HR'" as "[>Hγ _]".
-      by iDestruct (own_valid_2 with "Hγ Hγ'")
-        as %[[[] ?%leibniz_equiv] _]%auth_both_valid.
-  Qed.
-End proof.
-
-Typeclasses Opaque is_lock locked.

make-package

+#!/bin/bash
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! grep -E -q "^$PROJECT/" _CoqProject; then
+    echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+    exit 1
+fi
+
+# Generate _CoqProject file and Makefile
+rm -f "$COQFILE"
+# Get the right "-Q" line.
+grep -E "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | grep -E -v "^-Q " >> "$COQFILE"
+# Get the files.
+grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
+# Now we can run coq_makefile.
+"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
+
+# Run build
+make -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*

multris/channel/channel.v

+(** This file contains the definition of the channels,
+and their primitive proof rules. Moreover:
+
+- It defines the connective [c ↣ prot] for ownership of channel endpoints,
+  which describes that channel endpoint [c] adheres to protocol [prot].
+- It proves Actris's specifications of [send] and [recv] w.r.t.
+  multiparty dependent separation protocols.
+
+In this file we define the three message-passing connectives:
+
+- [new_chan] creates an n*n matrix of references where [i,j] is the singleton
+  buffer from participant i to participant j
+- [send] takes an endpoint, a participant id, and a value, and puts the value in 
+  the reference corresponding to the participant id, and waits until recv takes
+  it out.
+- [recv] takes an endpoint, and a participant id, and waits until a value is put
+  into the corresponding reference.
+
+It is additionaly shown that the channel ownership [c ↣ prot] is closed under
+the subprotocol relation [⊑] *)
+From iris.algebra Require Import gmap excl_auth gmap_view.
+From iris.base_logic.lib Require Import invariants.
+From iris.heap_lang Require Export primitive_laws notation proofmode.
+From multris.utils Require Import matrix.
+From multris.channel Require Import proto_model.
+From multris.channel Require Export proto.
+Set Default Proof Using "Type".
+
+(** * The definition of the message-passing connectives *)
+Definition new_chan : val :=
+  λ: "n", new_matrix "n" "n" NONEV.
+
+Definition get_chan : val :=
+  λ: "cs" "i", ("cs","i").
+
+Definition wait : val :=
+  rec: "go" "c" :=
+    match: !"c" with
+      NONE => #()
+    | SOME <> => "go" "c"
+    end.
+
+Definition send : val :=
+  λ: "c" "j" "v",
+    let: "m" := Fst "c" in
+    let: "i" := Snd "c" in
+    let: "l" := matrix_get "m" "i" "j" in
+    "l" <- SOME "v";; wait "l".
+
+Definition recv : val :=
+  rec: "go" "c" "j" :=
+    let: "m" := Fst "c" in
+    let: "i" := Snd "c" in
+    let: "l" := matrix_get "m" "j" "i" in
+    let: "v" := Xchg "l" NONEV in
+    match: "v" with
+      NONE     => "go" "c" "j"
+    | SOME "v" => "v"
+    end.
+
+(** * Setup of Iris's cameras *)
+Class proto_exclG Σ V :=
+  protoG_exclG ::
+    inG Σ (excl_authR (laterO (proto (leibnizO V) (iPropO Σ) (iPropO Σ)))).
+
+Definition proto_exclΣ V := #[
+  GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
+].
+
+Class chanG Σ := {
+  chanG_proto_exclG :: proto_exclG Σ val;
+  chanG_tokG :: inG Σ (exclR unitO);
+  chanG_protoG :: protoG Σ val;
+}.
+Definition chanΣ : gFunctors := #[ proto_exclΣ val; protoΣ val; GFunctor (exclR unitO) ].
+Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
+Proof. solve_inG. Qed.
+
+(** * Definition of the pointsto connective *)
+Notation iProto Σ := (iProto Σ val).
+Notation iMsg Σ := (iMsg Σ val).
+
+Definition tok `{!chanG Σ} (γ : gname) : iProp Σ := own γ (Excl ()).
+
+Definition chan_inv `{!heapGS Σ, !chanG Σ} γ γE γt i j (l:loc) : iProp Σ :=
+  (l ↦ NONEV ∗ tok γt)%I ∨
+  (∃ v p, l ↦ SOMEV v ∗
+          iProto_own γ i (<(Send, j)> MSG v ; p)%proto ∗ own γE (●E (Next p))) ∨
+  (∃ p, l ↦ NONEV ∗
+          iProto_own γ i p ∗ own γE (●E (Next p))).
+
+Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
+    (c : val) (p : iProto Σ) : iProp Σ :=
+  ∃ γ (γEs : list gname) (m:val) (i:nat) (n:nat) p',
+    ⌜ c = (m,#i)%V ⌝ ∗
+    inv (nroot.@"ctx") (iProto_ctx γ n) ∗
+    is_matrix m n n
+      (λ i j l, ∃ γt, inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j l)) ∗
+    ▷ (p' ⊑ p) ∗
+    own (γEs !!! i) (●E (Next p')) ∗ own (γEs !!! i) (◯E (Next p')) ∗
+    iProto_own γ i p'.
+Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
+Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
+Definition iProto_pointsto_eq :
+  @iProto_pointsto = @iProto_pointsto_def := iProto_pointsto_aux.(seal_eq).
+Arguments iProto_pointsto {_ _ _} _ _%_proto.
+Global Instance: Params (@iProto_pointsto) 5 := {}.
+Notation "c ↣ p" := (iProto_pointsto c p)
+  (at level 20, format "c  ↣  p").
+
+Definition chan_pool `{!heapGS Σ, !chanG Σ}
+    (m : val) (i':nat) (ps : list (iProto Σ)) : iProp Σ :=
+  ∃ γ (γEs : list gname) (n:nat),
+    ⌜(i' + length ps = n)%nat⌝ ∗
+    inv (nroot.@"ctx") (iProto_ctx γ n) ∗
+    is_matrix m n n (λ i j l,
+      ∃ γt, inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j l)) ∗
+    [∗ list] i ↦ p ∈ ps,
+      (own (γEs !!! (i+i')) (●E (Next p)) ∗
+       own (γEs !!! (i+i')) (◯E (Next p)) ∗
+       iProto_own γ (i+i') p).
+
+Section channel.
+  Context `{!heapGS Σ, !chanG Σ}.
+  Implicit Types p : iProto Σ.
+  Implicit Types TT : tele.
+
+  Global Instance iProto_pointsto_ne c : NonExpansive (iProto_pointsto c).
+  Proof. rewrite iProto_pointsto_eq. solve_proper. Qed.
+  Global Instance iProto_pointsto_proper c : Proper ((≡) ==> (≡)) (iProto_pointsto c).
+  Proof. apply (ne_proper _). Qed.
+
+  Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
+  Proof.
+    rewrite iProto_pointsto_eq.
+    iDestruct 1 as (?????? ->) "(#IH & Hls & Hle & H● & H◯ & Hown)".
+    iIntros "Hle'". iExists _,_,_,_,_,p'.
+    iSplit; [done|]. iFrame "#∗".
+    iApply (iProto_le_trans with "Hle Hle'").
+  Qed.
+
+  (** ** Specifications of [send] and [recv] *)
+  Lemma new_chan_spec (ps:list (iProto Σ)) :
+    0 < length ps →
+    {{{ iProto_consistent ps }}}
+      new_chan #(length ps)
+    {{{ cs, RET cs; chan_pool cs 0 ps }}}.
+  Proof.
+    iIntros (Hle Φ) "Hps HΦ". wp_lam.
+    iMod (iProto_init with "Hps") as (γ) "[Hps Hps']".
+    iAssert (|==> ∃ (γEs : list gname),
+                ⌜length γEs = length ps⌝ ∗
+                [∗ list] i ↦ p ∈ ps,
+                  own (γEs !!! i) (●E (Next (ps !!! i))) ∗
+                  own (γEs !!! i) (◯E (Next (ps !!! i))) ∗
+                  iProto_own γ i (ps !!! i))%I with "[Hps']" as "H".
+    { clear Hle.
+      iInduction ps as [|p ps] "IHn" using rev_ind.
+      { iExists []. iModIntro. simpl. done. }
+      iDestruct "Hps'" as "[Hps' Hp]".
+      iMod (own_alloc (●E (Next p) ⋅ ◯E (Next p))) as (γE) "[Hauth Hfrag]".
+      { apply excl_auth_valid. }
+      iMod ("IHn" with "Hps'") as (γEs Hlen) "H".
+      iModIntro. iExists (γEs++[γE]).
+      rewrite !length_app Hlen.
+      iSplit; [iPureIntro=>/=;lia|]=> /=.
+      iSplitL "H".
+      { iApply (big_sepL_impl with "H").
+        iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)".
+        assert (i < length ps) as Hle.
+        { by apply lookup_lt_is_Some_1. }
+        rewrite !lookup_total_app_l; [|lia..]. iFrame. }
+      rewrite Nat.add_0_r.
+      simpl. rewrite right_id_L.
+      rewrite !lookup_total_app_r; [|lia..]. rewrite !Hlen.
+      rewrite Nat.sub_diag. simpl. iFrame.
+      iDestruct "Hp" as "[$ _]". }
+    iMod "H" as (γEs Hlen) "H".
+    iMod (inv_alloc with "Hps") as "#IHp".
+    wp_smart_apply (new_matrix_spec _ _ _ _
+                     (λ i j l, ∃ γt,
+            inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j
+                                       l))%I); [done..| |].
+    { iApply (big_sepL_intro). iIntros "!>" (k tt Hin). iApply (big_sepL_intro).
+      iIntros "!>" (k' tt' Hin'). iIntros (l) "Hl".
+      iMod (own_alloc (Excl ())) as (γ') "Hγ'"; [done|].
+      iExists γ'. iApply inv_alloc. iNext. iLeft. iFrame. }
+    iIntros (mat) "Hmat". iApply "HΦ".
+    iExists _, _, _. iFrame "#∗".
+    rewrite left_id. iSplit; [done|].
+    iApply (big_sepL_impl with "H").
+    iIntros "!>" (i ? HSome') "(Hauth & Hfrag & Hown)". iFrame.
+    rewrite (list_lookup_total_alt ps).
+    simpl. rewrite right_id_L. rewrite HSome'. iFrame.
+  Qed.
+
+  Lemma get_chan_spec cs i ps p :
+    {{{ chan_pool cs i (p::ps) }}}
+      get_chan cs #i
+    {{{ c, RET c; c ↣ p ∗ chan_pool cs (i+1) ps }}}.
+  Proof.
+    iIntros (Φ) "Hcs HΦ".
+    iDestruct "Hcs" as (γp γEs n <-) "(#IHp & #Hm & Hl)".
+    wp_lam. wp_pures.
+    iDestruct "Hl" as "[Hl Hls]".
+    iModIntro.
+    iApply "HΦ".
+    iSplitL "Hl".
+    { rewrite iProto_pointsto_eq. iExists _, _, _, _, _, _.
+      iSplit; [done|].
+      iFrame. iFrame "#∗". iNext. done. }
+    iExists γp, γEs, _. iSplit; [done|].
+    iFrame. iFrame "#∗".
+    simpl.
+    replace (i + 1 + length ps) with (i + (S $ length ps))%nat by lia.
+    iFrame "#".
+    iApply (big_sepL_impl with "Hls").
+    iIntros "!>" (k x HSome) "(H1 & H2 & H3)".
+    replace (S (k + i)) with (k + (i + 1)) by lia.
+    iFrame.
+  Qed.
+
+  Lemma send_spec c j v p :
+    {{{ c ↣ <(Send, j)> MSG v; p }}}
+      send c #j v
+    {{{ RET #(); c ↣ p }}}.
+  Proof.
+    rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
+    iDestruct "Hc" as
+      (γ γE l i n p' ->) "(#IH & #Hls & Hle & H● & H◯ & Hown)".
+    wp_bind (Fst _).
+    iInv "IH" as "Hctx".
+    iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
+    iRewrite "Heq" in "Hown".
+    iDestruct (iProto_ctx_agree with "Hctx [Hown//]") as "#Hi".
+    iDestruct (iProto_target with "Hctx [Hown//]") as "#Hj".
+    iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
+    wp_pures.
+    iDestruct "Hi" as %Hi.
+    iDestruct "Hj" as %Hj.
+    wp_smart_apply (matrix_get_spec with "Hls"); [done..|].
+    iIntros (l') "[Hl' _]".
+    iDestruct "Hl'" as (γt) "#IHl1".
+    wp_pures. wp_bind (Store _ _).
+    iInv "IHl1" as "HIp".
+    iDestruct "HIp" as "[HIp|HIp]"; last first.
+    { iDestruct "HIp" as "[HIp|HIp]".
+      - iDestruct "HIp" as (? p'') "(>Hl & Hown' & HIp)".
+        wp_store.
+        iDestruct (iProto_own_excl with "Hown Hown'") as %[].
+      - iDestruct "HIp" as (p'') "(>Hl' & Hown' & HIp)".
+        wp_store.
+        iDestruct (iProto_own_excl with "Hown Hown'") as %[]. }
+    iDestruct "HIp" as "[>Hl' Htok]".
+    wp_store.
+    iMod (own_update_2 with "H● H◯") as "[H● H◯]"; [by apply excl_auth_update|].
+    iModIntro.
+    iSplitL "Hl' H● Hown Hle".
+    { iRight. iLeft. iIntros "!>". iExists _, _. iFrame.
+      iDestruct (iProto_own_le with "Hown Hle") as "Hown".
+      by rewrite iMsg_base_eq. }
+    wp_pures.
+    iLöb as "HL".
+    wp_lam.
+    wp_bind (Load _).
+    iInv "IHl1" as "HIp".
+    iDestruct "HIp" as "[HIp|HIp]".
+    { iDestruct "HIp" as ">[Hl' Htok']".
+      iDestruct (own_valid_2 with "Htok Htok'") as %[]. }
+    iDestruct "HIp" as "[HIp|HIp]".
+    - iDestruct "HIp" as (? p'') "(>Hl' & Hown & HIp)".
+      wp_load. iModIntro.
+      iSplitL "Hl' Hown HIp".
+      { iRight. iLeft. iExists _,_. iFrame. }
+      wp_pures. iApply ("HL" with "HΦ Htok H◯").
+    - iDestruct "HIp" as (p'') "(>Hl' & Hown & H●)".
+      wp_load.
+      iModIntro.
+      iSplitL "Hl' Htok".
+      { iLeft. iFrame. }
+      iDestruct (own_valid_2 with "H● H◯") as "#Hagree".
+      iDestruct (excl_auth_agreeI with "Hagree") as "Hagree'".
+      wp_pures.
+      iMod (own_update_2 with "H● H◯") as "[H● H◯]".
+      { apply excl_auth_update. }
+      iModIntro.
+      iApply "HΦ".
+      iExists _, _, _, _, _, _.
+      iSplit; [done|]. iFrame "#∗".
+      iRewrite -"Hagree'". iApply iProto_le_refl.
+  Qed.
+
+  Lemma send_spec_tele {TT} c i (tt : TT)
+        (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+    {{{ c ↣ (<(Send,i) @.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
+      send c #i (v tt)
+    {{{ RET #(); c ↣ (p tt) }}}.
+  Proof.
+    iIntros (Φ) "[Hc HP] HΦ".
+    iDestruct (iProto_pointsto_le _ _ (<(Send,i)> MSG v tt; p tt)%proto
+                with "Hc [HP]") as "Hc".
+    { iIntros "!>". iApply iProto_le_trans. iApply iProto_le_texist_intro_l.
+      by iApply iProto_le_payload_intro_l. }
+    by iApply (send_spec with "Hc").
+  Qed.
+
+  Lemma recv_spec {TT} c j (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
+    {{{ c ↣ <(Recv, j) @.. x> MSG v x {{ ▷ P x }}; p x }}}
+      recv c #j
+    {{{ x, RET v x; c ↣ p x ∗ P x }}}.
+  Proof.
+    iIntros (Φ) "Hc HΦ". iLöb as "HL". wp_lam.
+    rewrite iProto_pointsto_eq.
+    iDestruct "Hc" as
+      (γ γE l i n p' ->) "(#IH & #Hls & Hle & H● & H◯ & Hown)".
+    do 5 wp_pure _.
+    wp_bind (Snd _).
+    iInv "IH" as "Hctx".
+    iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
+    iRewrite "Heq" in "Hown".
+    iDestruct (iProto_ctx_agree with "Hctx [Hown//]") as "#Hi".
+    iDestruct (iProto_target with "Hctx [Hown//]") as "#Hj".
+    iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
+    wp_pure _.
+    iDestruct "Hi" as %Hi.
+    iDestruct "Hj" as %Hj.
+    wp_smart_apply (matrix_get_spec with "Hls"); [done..|].
+    iIntros (l') "[Hl' _]".
+    iDestruct "Hl'" as (γt) "#IHl2".
+    wp_pures.
+    wp_bind (Xchg _ _).
+    iInv "IHl2" as "HIp".
+    iDestruct "HIp" as "[HIp|HIp]".
+    { iDestruct "HIp" as ">[Hl' Htok]".
+      wp_xchg. iModIntro.
+      iSplitL "Hl' Htok".
+      { iLeft. iFrame. }
+      wp_pures. iApply ("HL" with "[H● H◯ Hown Hle] HΦ").
+      iExists _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
+    iDestruct "HIp" as "[HIp|HIp]"; last first.
+    { iDestruct "HIp" as (p'') "[>Hl' [Hown' H◯']]".
+      wp_xchg.
+      iModIntro.
+      iSplitL "Hl' Hown' H◯'".
+      { iRight. iRight. iExists _. iFrame. }
+      wp_pures. iApply ("HL" with "[H● H◯ Hown Hle] HΦ").
+      iExists _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
+    iDestruct "HIp" as (w p'') "(>Hl' & Hown' & Hp')".
+    iInv "IH" as "Hctx".
+    wp_xchg.
+    iDestruct (iProto_own_le with "Hown Hle") as "Hown".
+    iMod (iProto_step with "Hctx Hown' Hown []") as
+      (p''') "(Hm & Hctx & Hown & Hown')".
+    { by rewrite iMsg_base_eq. }
+    iModIntro.
+    iSplitL "Hctx"; [done|].
+    iModIntro.
+    iSplitL "Hl' Hown Hp'".
+    { iRight. iRight. iExists _. iFrame. }
+    wp_pure _.
+    rewrite iMsg_base_eq.
+    iDestruct (iMsg_texist_exist with "Hm") as (x <-) "[Hp HP]".
+    wp_pures.
+    iMod (own_update_2 with "H● H◯") as "[H● H◯]";
+      [apply (excl_auth_update _ _ (Next p'''))|].
+    iModIntro. iApply "HΦ". rewrite /iProto_pointsto_def. iFrame "IH Hls ∗".
+    iSplit; [done|]. iRewrite "Hp". iApply iProto_le_refl.
+  Qed.
+
+End channel.

multris/channel/proofmode.v

+(** This file contains the definitions of Actris's tactics for symbolic
+execution of message-passing programs. The API of these tactics is documented
+in the [README.md] file. The implementation follows the same pattern for the
+implementation of these tactics that is used in Iris. In addition, it uses a
+standard pattern using type classes to perform the normalization.
+
+In addition to the tactics for symbolic execution, this file defines the tactic
+[solve_proto_contractive], which can be used to automatically prove that
+recursive protocols are contractive. *)
+From iris.algebra Require Import gmap.
+From iris.proofmode Require Import coq_tactics reduction spec_patterns.
+From iris.heap_lang Require Export proofmode notation.
+From multris.channel Require Import proto_model.
+From multris.channel Require Export channel.
+Set Default Proof Using "Type".
+
+(** * 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_proto_contractive :=
+  solve_proper_core ltac:(fun _ =>
+    first [f_contractive; simpl in * | f_equiv | f_dist_le]).
+
+(** * 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 := eq_refl.
+Global Instance action_dual_if_true_send i : ActionDualIf true (Send,i) (Recv,i) := eq_refl.
+Global Instance action_dual_if_true_recv i : ActionDualIf true (Recv,i) (Send,i) := eq_refl.
+
+Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
+    (pas : list (bool * iProto Σ)) (q : iProto Σ) :=
+  proto_normalize :
+    ⊢ iProto_dual_if d p <++>
+        foldr (iProto_app ∘ uncurry iProto_dual_if) END%proto pas ⊑ q.
+Global Hint Mode ProtoNormalize ! ! ! ! - : typeclass_instances.
+Arguments ProtoNormalize {_} _ _%_proto _%_proto _%_proto.
+
+Notation ProtoUnfold p1 p2 := (∀ d pas q,
+  ProtoNormalize d p2 pas q → ProtoNormalize d p1 pas q).
+
+Class MsgNormalize {Σ} (d : bool) (m1 : iMsg Σ)
+    (pas : list (bool * iProto Σ)) (m2 : iMsg Σ) :=
+  msg_normalize a :
+    ProtoNormalize d (<a> m1) pas (<(if d then action_dual a else a)> m2).
+Global Hint Mode MsgNormalize ! ! ! ! - : typeclass_instances.
+Arguments MsgNormalize {_} _ _%_msg _%_msg _%_msg.
+
+Section classes.
+  Context `{!chanG Σ, !heapGS Σ}.
+  Implicit Types TT : tele.
+  Implicit Types p : iProto Σ.
+  Implicit Types m : iMsg Σ.
+  Implicit Types P : iProp Σ.
+
+  Lemma proto_unfold_eq p1 p2 : p1 ≡ p2 → ProtoUnfold p1 p2.
+  Proof. rewrite /ProtoNormalize=> Hp d pas q. by rewrite Hp. Qed.
+
+  Global Instance proto_normalize_done p : ProtoNormalize false p [] p | 0.
+  Proof. rewrite /ProtoNormalize /= right_id. auto. Qed.
+  Global Instance proto_normalize_done_dual p :
+    ProtoNormalize true p [] (iProto_dual p) | 0.
+  Proof. rewrite /ProtoNormalize /= right_id. auto. Qed.
+  Global Instance proto_normalize_done_dual_end :
+    ProtoNormalize (Σ:=Σ) true END [] END | 0.
+  Proof. rewrite /ProtoNormalize /= right_id iProto_dual_end. auto. Qed.
+
+  Global Instance proto_normalize_dual d p pas q :
+    ProtoNormalize (negb d) p pas q →
+    ProtoNormalize d (iProto_dual p) pas q.
+  Proof. rewrite /ProtoNormalize. by destruct d; rewrite /= ?involutive. Qed.
+
+  Global Instance proto_normalize_app_l d p1 p2 pas q :
+    ProtoNormalize d p1 ((d,p2) :: pas) q →
+    ProtoNormalize d (p1 <++> p2) pas q.
+  Proof.
+    rewrite /ProtoNormalize /=. rewrite assoc.
+    by destruct d; by rewrite /= ?iProto_dual_app.
+  Qed.
+
+  Global Instance proto_normalize_end d d' p pas q :
+    ProtoNormalize d p pas q →
+    ProtoNormalize d' END ((d,p) :: pas) q | 0.
+  Proof.
+    rewrite /ProtoNormalize /=.
+    destruct d'; by rewrite /= ?iProto_dual_end left_id.
+  Qed.
+
+  Global Instance proto_normalize_app_r d p1 p2 pas q :
+    ProtoNormalize d p2 pas q →
+    ProtoNormalize false p1 ((d,p2) :: pas) (p1 <++> q) | 0.
+  Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed.
+
+  Global Instance proto_normalize_app_r_dual d p1 p2 pas q :
+    ProtoNormalize d p2 pas q →
+    ProtoNormalize true p1 ((d,p2) :: pas) (iProto_dual p1 <++> q) | 0.
+  Proof. rewrite /ProtoNormalize /= => H. by iApply iProto_le_app. Qed.
+
+  Global Instance msg_normalize_base d v P p q pas :
+    ProtoNormalize d p pas q →
+    MsgNormalize d (MSG v {{ P }}; p) pas (MSG v {{ P }}; q).
+  Proof.
+    rewrite /MsgNormalize /ProtoNormalize=> H a.
+    iApply iProto_le_trans; [|by iApply iProto_le_base].
+    destruct d; by rewrite /= ?iProto_dual_message ?iMsg_dual_base
+      iProto_app_message iMsg_app_base.
+  Qed.
+
+  Global Instance msg_normalize_exist {A} d (m1 m2 : A → iMsg Σ) pas :
+    (∀ x, MsgNormalize d (m1 x) pas (m2 x)) →
+    MsgNormalize d (∃ x, m1 x) pas (∃ x, m2 x).
+  Proof.
+    rewrite /MsgNormalize /ProtoNormalize=> H a.
+    destruct d, a as [[|]];
+                simpl in *; rewrite ?iProto_dual_message ?iMsg_dual_exist
+      ?iProto_app_message ?iMsg_app_exist /=; iIntros (x); iExists x; first
+      [move: (H x (Send,n)); by rewrite ?iProto_dual_message ?iProto_app_message
+      |move: (H x (Recv,n)); by rewrite ?iProto_dual_message ?iProto_app_message].
+  Qed.
+
+  Global Instance proto_normalize_message d a1 a2 m1 m2 pas :
+    ActionDualIf d a1 a2 →
+    MsgNormalize d m1 pas m2 →
+    ProtoNormalize d (<a1> m1) pas (<a2> m2).
+  Proof. by rewrite /ActionDualIf /MsgNormalize /ProtoNormalize=> ->. Qed.
+
+  (** Automatically perform normalization of protocols in the proof mode when
+  using [iAssumption] and [iFrame]. *)
+  Global Instance pointsto_proto_from_assumption q c p1 p2 :
+    ProtoNormalize false p1 [] p2 →
+    FromAssumption q (c ↣ p1) (c ↣ p2).
+  Proof.
+    rewrite /FromAssumption /ProtoNormalize /= right_id.
+    rewrite bi.intuitionistically_if_elim.
+    iIntros (?) "H". by iApply (iProto_pointsto_le with "H").
+  Qed.
+  Global Instance pointsto_proto_from_frame q c p1 p2 :
+    ProtoNormalize false p1 [] p2 →
+    Frame q (c ↣ p1) (c ↣ p2) True.
+  Proof.
+    rewrite /Frame /ProtoNormalize /= right_id.
+    rewrite bi.intuitionistically_if_elim.
+    iIntros (?) "[H _]". by iApply (iProto_pointsto_le with "H").
+  Qed.
+End classes.
+
+(** * Symbolic execution tactics *)
+(* TODO: Maybe strip laters from other hypotheses in the future? *)
+Lemma tac_wp_recv `{!chanG Σ, !heapGS Σ} {TT : tele} Δ i j K v (n:nat) c p m tv tP tP' tp Φ :
+  v = #n →
+  envs_lookup i Δ = Some (false, c ↣ p)%I →
+  ProtoNormalize false p [] (<(Recv,n)> m) →
+  MsgTele m tv tP tp →
+  (∀.. x, MaybeIntoLaterN false 1 (tele_app tP x) (tele_app tP' x)) →
+  let Δ' := envs_delete false i false Δ in
+  (∀.. x : TT,
+    match envs_app false
+        (Esnoc (Esnoc Enil j (tele_app tP' x)) i (c ↣ tele_app tp x)) Δ' with
+    | Some Δ'' => envs_entails Δ'' (WP fill K (of_val (tele_app tv x)) {{ Φ }})
+    | None => False
+    end) →
+  envs_entails Δ (WP fill K (recv c v) {{ Φ }}).
+Proof.
+  intros ->.
+  rewrite envs_entails_unseal /ProtoNormalize /MsgTele /MaybeIntoLaterN /=.
+  rewrite !tforall_forall right_id.
+  intros ? Hp Hm HP HΦ. rewrite envs_lookup_sound //; simpl.
+  assert (c ↣ p ⊢ c ↣ <(Recv,n) @.. x>
+    MSG tele_app tv x {{ ▷ tele_app tP' x }}; tele_app tp x) as ->.
+  { iIntros "Hc". iApply (iProto_pointsto_le with "Hc"). iIntros "!>".
+    iApply iProto_le_trans; [iApply Hp|rewrite Hm].
+    iApply iProto_le_texist_elim_l; iIntros (x).
+    iApply iProto_le_trans; [|iApply (iProto_le_texist_intro_r _ _ x)]; simpl.
+    iIntros "H". by iDestruct (HP with "H") as "$". }
+  rewrite -wp_bind. eapply bi.wand_apply;
+    [by eapply bi.wand_entails, (recv_spec _ n (tele_app tv) (tele_app tP') (tele_app tp))|f_equiv; first done].
+  rewrite -bi.later_intro; apply bi.forall_intro=> x.
+  specialize (HΦ x). destruct (envs_app _ _) as [Δ'|] eqn:HΔ'=> //.
+  rewrite envs_app_sound //; simpl. by rewrite right_id HΦ.
+Qed.
+
+Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
+  let solve_pointsto _ :=
+    let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
+    iAssumptionCore || fail "wp_recv: cannot find" c "↣ ? @ ?" in
+  wp_pures;
+  let Hnew := iFresh in
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_recv _ _ Hnew K))
+      |fail 1 "wp_recv: cannot find 'recv' in" e];
+    [|solve_pointsto ()
+       |tc_solve || fail 1 "wp_recv: protocol not of the shape <?>"
+    |tc_solve || fail 1 "wp_recv: cannot convert to telescope"
+    |tc_solve
+    |pm_reduce; simpl; tac_intros;
+     tac Hnew;
+     wp_finish];[try done|]
+  | _ => fail "wp_recv: 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" "(" 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) ")" "as"
+    "(" ne_simple_intropattern_list(ys) ")" constr(pat) :=
+  wp_recv_core (intros xs) as (fun H => _iDestructHyp H ys pat).
+    
+Lemma tac_wp_send `{!chanG Σ, !heapGS Σ} {TT : tele} Δ neg i js K (n:nat) w c v p m tv tP tp Φ :
+  w = #n →
+  envs_lookup i Δ = Some (false, c ↣ p)%I →
+  ProtoNormalize false p [] (<(Send,n)> m) →
+  MsgTele m tv tP tp →
+  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 ↣ tele_app tp x)) Δ2 with
+       | Some Δ2' =>
+          v = tele_app tv x ∧
+          envs_entails Δ1 (tele_app tP x) ∧
+          envs_entails Δ2' (WP fill K (of_val #()) {{ Φ }})
+       | None => False
+       end
+    | None => False
+    end) →
+  envs_entails Δ (WP fill K (send c w v) {{ Φ }}).
+Proof.
+  intros ->.
+  rewrite envs_entails_unseal /ProtoNormalize /MsgTele /= right_id texist_exist.
+  intros ? Hp Hm [x HΦ]. rewrite envs_lookup_sound //; simpl.
+  destruct (envs_split _ _ _) as [[Δ1 Δ2]|] eqn:? => //.
+  destruct (envs_app _ _ _) as [Δ2'|] eqn:? => //.
+  rewrite envs_split_sound //; rewrite (envs_app_sound Δ2) //; simpl.
+  destruct HΦ as (-> & -> & ->). rewrite right_id assoc.
+  assert (c ↣ p ⊢
+    c ↣ <(Send,n) @.. (x : TT)> MSG tele_app tv x {{ tele_app tP x }}; tele_app tp x) as ->.
+  { iIntros "Hc". iApply (iProto_pointsto_le with "Hc"); iIntros "!>".
+    iApply iProto_le_trans; [iApply Hp|]. by rewrite Hm. }
+  eapply bi.wand_apply; [rewrite -wp_bind; by eapply bi.wand_entails, send_spec_tele|].
+  by rewrite -bi.later_intro.
+Qed.
+
+Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) :=
+  let solve_pointsto _ :=
+    let c := match goal with |- _ = Some (_, (?c ↣ _)%I) => c end in
+    iAssumptionCore || fail "wp_send: cannot find" c "↣ ? @ ?" in
+  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
+     wp_pures;
+     lazymatch goal with
+     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+       first
+         [reshape_expr e ltac:(fun K e' => eapply (tac_wp_send _ neg _ Hs' K))
+         |fail 1 "wp_send: cannot find 'send' in" e];
+       [|solve_pointsto ()
+       |tc_solve || fail 1 "wp_send: protocol not of the shape <!>"
+       |tc_solve || fail 1 "wp_send: cannot convert to telescope"
+       |pm_reduce; simpl; tac_exist;
+        repeat lazymatch goal with
+        | |- ∃ _, _ => eexists _
+        end;
+        lazymatch goal with
+        | |- False => fail "wp_send:" Hs' "not found"
+        | _ => notypeclasses refine (conj (eq_refl _) (conj _ _));
+                [iFrame Hs_frame; solve_done d
+                |wp_finish]
+        end]; [try done|..]
+     | _ => fail "wp_send: not a 'wp'"
+     end
+  | _ => fail "wp_send: only a single goal spec pattern supported"
+  end.
+
+Tactic Notation "wp_send" "with" constr(pat) :=
+  wp_send_core (idtac) with pat.
+Tactic Notation "wp_send" "(" ne_uconstr_list(xs) ")" "with" constr(pat) :=
+  wp_send_core (ltac1_list_iter ltac:(fun x => eexists x) xs) with pat.
+
+Lemma iProto_consistent_equiv_proof {Σ} (ps : list (iProto Σ)) :
+  (∀ i j, valid_target ps i j) ∗
+  (∀ i j m1 m2,
+     (ps !!! i ≡ (<(Send, j)> m1)%proto) -∗
+     (ps !!! j ≡ (<(Recv, i)> m2)%proto) -∗
+     ∃ m1' m2' (TT1:tele) (TT2:tele) tv1 tP1 tp1 tv2 tP2 tp2,
+       (<(Send, j)> m1')%proto ≡ (<(Send, j)> m1)%proto ∗
+       (<(Recv, i)> m2')%proto ≡ (<(Recv, i)> m2)%proto ∗
+       ⌜MsgTele (TT:=TT1) m1' tv1 tP1 tp1⌝ ∗
+       ⌜MsgTele (TT:=TT2) m2' tv2 tP2 tp2⌝ ∗
+   ∀.. (x : TT1), tele_app tP1 x -∗
+   ∃.. (y : TT2), ⌜tele_app tv1 x = tele_app tv2 y⌝ ∗
+                  tele_app tP2 y ∗
+                  ▷ (iProto_consistent
+                       (<[i:=tele_app tp1 x]>(<[j:=tele_app tp2 y]>ps)))) -∗
+  iProto_consistent ps.
+Proof.
+  iIntros "[H' H]".
+  rewrite iProto_consistent_unfold.
+  iFrame.
+  iIntros (i j m1 m2) "Hm1 Hm2".
+  iDestruct ("H" with "Hm1 Hm2")
+    as (m1' m2' TT1 TT2 tv1 tP1 tp1 tv2 tP2 tp2)
+         "(Heq1 & Heq2& %Hm1' & %Hm2' & H)".
+  rewrite !iProto_message_equivI.
+  iDestruct "Heq1" as "[_ Heq1]".
+  iDestruct "Heq2" as "[_ Heq2]".
+  iIntros (v p1) "Hm1".
+  iSpecialize ("Heq1" $! v (Next p1)).
+  iRewrite -"Heq1" in "Hm1".
+  rewrite Hm1'.
+  rewrite iMsg_base_eq. rewrite iMsg_texist_exist.
+  iDestruct "Hm1" as (x Htv1) "[Hp1 HP1]".
+  iDestruct ("H" with "HP1") as (y Htv2) "[HP2 H]".
+  iExists (tele_app tp2 y).
+  iSpecialize ("Heq2" $! v (Next (tele_app tp2 y))).
+  iRewrite -"Heq2".
+  rewrite Hm2'. rewrite iMsg_base_eq. rewrite iMsg_texist_exist.
+  iSplitL "HP2".
+  { iExists y. iFrame.
+    iSplit; [|done].
+    iPureIntro. subst. done. }
+  iNext. iRewrite -"Hp1". done.
+Qed.
+
+Tactic Notation "iProto_consistent_take_step_step" :=
+  let i := fresh in
+  let j := fresh in
+  let m1 := fresh in
+  let m2 := fresh in
+  iIntros (i j m1 m2) "#Hm1 #Hm2";
+  repeat (destruct i as [|i]=> /=;
+          [try (by rewrite iProto_end_message_equivI);
+           iDestruct (iProto_message_equivI with "Hm1")
+                  as "[%Heq1 Hm1']";simplify_eq=> /=|
+            try (by rewrite iProto_end_message_equivI)]);
+  try (by rewrite iProto_end_message_equivI);
+  iDestruct (iProto_message_equivI with "Hm2")
+    as "[%Heq2 Hm2']";simplify_eq=> /=;
+  try (iClear "Hm1' Hm2'";
+       iExists _,_,_,_,_,_,_,_,_,_;
+       iSplitL "Hm1"; [iFrame "#"|];
+       iSplitL "Hm2"; [iFrame "#"|];
+       iSplit; [iPureIntro; tc_solve|];
+       iSplit; [iPureIntro; tc_solve|];
+       simpl; iClear "Hm1 Hm2"; clear m1 m2).
+
+Tactic Notation "iProto_consistent_take_step_target" :=
+  let i := fresh in
+  iIntros (i j a m); rewrite /valid_target;
+            iIntros "#Hm1";
+  repeat (destruct i as [|i]=> /=;
+          [try (by rewrite iProto_end_message_equivI);
+           by iDestruct (iProto_message_equivI with "Hm1")
+                    as "[%Heq1 _]" ; simplify_eq=> /=|
+           try (by rewrite iProto_end_message_equivI)]).
+
+Tactic Notation "iProto_consistent_take_step" :=
+  try iNext;
+  iApply iProto_consistent_equiv_proof;
+  iSplitR; [iProto_consistent_take_step_target|
+             iProto_consistent_take_step_step].
+
+Tactic Notation "iProto_consistent_resolve_step" :=
+  repeat iIntros (?); repeat iIntros "?";
+  repeat iExists _; repeat (iSplit; [done|]); try iFrame.
+
+Tactic Notation "iProto_consistent_take_steps" :=
+  repeat (iProto_consistent_take_step; iProto_consistent_resolve_step).
+
+Tactic Notation "wp_get_chan" "(" simple_intropattern(c) ")" constr(pat) :=
+  wp_smart_apply (get_chan_spec with "[$]"); iIntros (c) "[_TMP ?]";
+  iRevert "_TMP"; iIntros pat.
+
+Ltac ltac1_list_iter2 tac l1 l2 :=
+  let go := ltac2:(tac l1 l2 |- List.iter2 (ltac1:(tac x y |- tac x y) tac)
+                                          (of_ltac1_list l1) (of_ltac1_list l2)) in
+  go tac l1 l2.
+
+Tactic Notation "wp_new_chan" constr(prot) "as"
+       "(" simple_intropattern_list(xs) ")" constr_list(pats) :=
+  wp_smart_apply (new_chan_spec prot);
+    [set_solver| |iIntros (?) "?"];
+    [|ltac1_list_iter2 ltac:(fun x y => wp_get_chan (x) y) xs pats].
+
+Tactic Notation "wp_new_chan" constr(prot) "with" constr(lem) "as"
+       "(" simple_intropattern_list(xs) ")" constr_list(pats) :=
+  wp_smart_apply (new_chan_spec prot);
+    [set_solver|by iApply lem|iIntros (?) "?"];
+    ltac1_list_iter2 ltac:(fun x y => wp_get_chan (x) y) xs pats.