subprotocol example

theories/examples/subprotocols.v

 From actris.channel Require Import proofmode proto channel.
+From actris.logrel Require Import subtyping_rules.
+From iris.proofmode Require Import tactics.
 
 Section basics.
   Context `{heapG Σ, chanG Σ}.

theories/logrel/examples/subtyping.v

+From actris.channel Require Import proofmode proto channel.
+From actris.logrel Require Import subtyping_rules.
+From iris.proofmode Require Import tactics.
+
+Section basics.
+  Context `{heapG Σ, chanG Σ}.
+
+  Definition prot1_aux : (lsty Σ → lsty Σ) :=
+    λ rec, (<!!X Y> TY (X ⊸ Y)%lty ; <!!> TY X;
+           <??> TY Y; rec)%lty.
+  Instance prot1_aux_contractive : Contractive prot1_aux.
+  Proof. solve_proto_contractive. Qed.
+  Definition prot1 := lty_rec prot1_aux.
+
+  Definition prot1'_aux : (lsty Σ → lsty Σ) :=
+    λ rec, (<!!X Y> TY (X ⊸ Y)%lty ; <!!> TY X;
+           <??> TY Y;
+           <!!X Y> TY (X ⊸ Y)%lty ; <!!> TY X;
+           <??> TY Y; rec)%lty.
+  Instance prot1'_aux_contractive : Contractive prot1'_aux.
+  Proof. solve_proto_contractive. Qed.
+  Definition prot1' := lty_rec prot1'_aux.
+
+  Definition prot2_aux : (lsty Σ → lsty Σ) :=
+    λ rec, (<!!X> TY (X ⊸ lty_bool)%lty ; <!!> TY X;
+            <!!Y> TY (Y ⊸ lty_int)%lty ; <!!> TY Y;
+            <??> TY lty_bool; <??> TY lty_int; rec)%lty.
+  Instance prot2_aux_contractive : Contractive prot2_aux.
+  Proof. solve_proto_contractive. Qed.
+  Definition prot2 := lty_rec prot2_aux.
+
+  Lemma rec_swap_example :
+    ⊢ prot1 <: prot2.
+  Proof.
+    iApply (lty_le_trans _ prot1').
+    { iLöb as "IH".
+      iEval (rewrite /prot1 /prot1').
+      iDestruct (lty_le_rec_unfold (prot1_aux)) as "[H1 _]".
+      iDestruct (lty_le_rec_unfold (prot1'_aux)) as "[_ H2]".
+      iApply (lty_le_trans with "H1"). iApply (lty_le_trans with "[] H2").
+      iIntros (X Y). iExists X, Y. do 3 iModIntro.
+      iApply (lty_le_trans with "H1").
+      iIntros (X' Y'). iExists X', Y'. do 3 iModIntro.
+      iApply "IH".
+    }
+    iApply lty_le_rec.
+    iIntros (M1 M2) "#Hrec".
+    iIntros (X). iExists X, lty_bool. iModIntro. iModIntro.
+    iIntros (Y).
+    iApply (lty_le_trans _ (<??> TY lty_bool ; <!!> TY Y ⊸ lty_int ;
+                            <!!> TY Y ; <??> TY lty_int ; M2)); last first.
+    {
+      iApply (lty_le_trans _ (<!!> TY Y ⊸ lty_int ; <??> TY lty_bool ;
+                              <!!> TY Y ; <??> TY lty_int ; M2)).
+      { iApply lty_le_swap_recv_send. }
+      iModIntro. iApply lty_le_swap_recv_send.
+    }
+    iModIntro. iExists Y, lty_int.
+    by do 3 iModIntro.
+  Qed.
+
+End basics.

theories/logrel/subtyping_rules.v

@@ -501,5 +501,47 @@ Section subtyping_rules.
     ⊢ lty_dual (lty_branch Ss) <:> lty_select (lty_dual <$> Ss).
   Proof. iApply lty_le_dual_choice. Qed.
 
+  Global Instance lty_le_from_forall_l k (M : lty Σ k → lmsg Σ) (S : lsty Σ) :
+    FromForall (lty_le (<?? X> M X) S)%lty (λ X, (lty_le (<??> M X) S)%lty) | 10.
+  Proof. apply lty_le_exist_elim_l. Qed.
+  Global Instance lty_le_from_forall_r k (S : lsty Σ) (M : lty Σ k → lmsg Σ) :
+    FromForall (lty_le S (<!! X> M X))%lty (λ X, (lty_le S (<!!> M X))%lty) | 11.
+  Proof. 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 | 10.
+  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 | 11.
+  Proof.
+    rewrite /FromExist. iDestruct 1 as (x) "H".
+    iApply (lty_le_trans with "H"). iApply lty_le_exist_intro_r.
+  Qed.
+
+  Lemma lty_le_base_send A (S1 S2 : lsty Σ) :
+    ▷ (S1 <: S2) -∗
+    (<!!> TY A ; S1) <: (<!!> TY A ; S2).
+  Proof. iIntros "H". iApply lty_le_send. iApply lty_le_refl. eauto. Qed.
+
+  Global Instance lty_le_from_modal_send A (S1 S2 : lsty Σ) :
+    FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
+              ((<!!> TY A; S1) <: (<!!> TY A; S2)) (S1 <: S2).
+  Proof. apply lty_le_base_send. Qed.
+
+  Lemma lty_le_base_recv A (S1 S2 : lsty Σ) :
+    ▷ (S1 <: S2) -∗
+    (<??> TY A ; S1) <: (<??> TY A ; S2).
+  Proof. iIntros "H". iApply lty_le_recv. iApply lty_le_refl. eauto. Qed.
+
+  Global Instance lty_le_from_modal_recv A (S1 S2 : lsty Σ) :
+    FromModal (modality_instances.modality_laterN 1) (S1 <: S2)
+              ((<??> TY A; S1) <: (<??> TY A; S2)) (S1 <: S2).
+  Proof. apply lty_le_base_recv. Qed.
+
 End subtyping_rules.
 
+Hint Extern 0 (environments.envs_entails _ (?x <: ?y)) =>
+  first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.