Bumped protocol polymorphism to session types

theories/logrel/examples/double.v

@@ -85,14 +85,14 @@ Section double.
   Qed.
 
   Lemma prog_typed :
-    ⊢ ∅ ⊨ prog : chan (<??> lty_int; <??> lty_int; END) ⊸ lty_int * lty_int.
+    ⊢ ∅ ⊨ prog : chan (<??> TY lty_int; <??> TY lty_int; END) ⊸ lty_int * lty_int.
   Proof.
     iIntros (vs) "!> HΓ /=".
     iApply wp_value.
     iSplitL; last by iApply env_ltyped_empty.
     iIntros (c) "Hc".
     iApply (wp_prog with "[Hc]").
-    { iApply (iProto_mapsto_le _ (lsty_car (<??> lty_int; <??> lty_int; END)) with "Hc").
+    { iApply (iProto_mapsto_le _ (lsty_car (<??> TY lty_int; <??> TY lty_int; END)) with "Hc").
       iIntros "!> !>" (v1). iMod 1 as %[x1 ->]. iExists x1.
       iIntros "!>" (v2). iMod 1 as %[x2 ->]. iExists x2. auto. }
     iIntros "!>" (k1 k2 _).

theories/logrel/examples/pair.v

@@ -7,7 +7,7 @@ Section pair.
   Context `{heapG Σ, chanG Σ}.
 
   Lemma prog_typed :
-    ⊢ ∅ ⊨ prog : chan (<??> lty_int; <??> lty_int; END) ⊸ lty_int * lty_int.
+    ⊢ ∅ ⊨ prog : chan (<??> TY lty_int; <??> TY lty_int; END) ⊸ lty_int * lty_int.
   Proof.
     rewrite /prog.
     iApply ltyped_lam. iApply ltyped_pair.

theories/logrel/session_types.v

@@ -2,10 +2,20 @@ From iris.algebra Require Export gmap.
 From actris.logrel Require Export model.
 From actris.channel Require Export channel.
 
+Definition lmsg Σ := iMsg Σ.
+Delimit Scope lmsg_scope with lmsg.
+Bind Scope lmsg_scope with lmsg.
+
+Definition lty_msg_exist {Σ} {k} (M : lty Σ k → lmsg Σ) : lmsg Σ :=
+  iMsg_exist M.
+
+Definition lty_msg_base {Σ} (A : ltty Σ) (S : lsty Σ) : lmsg Σ :=
+  iMsg_exist (λ v, iMsg_base v (▷ ltty_car A v) (lsty_car S)).
+
 Definition lty_end {Σ} : lsty Σ := Lsty END.
 
-Definition lty_message {Σ} (a : action) (A : ltty Σ) (S : lsty Σ) : lsty Σ :=
-  Lsty (<a@v> MSG v {{ ▷ ltty_car A v }}; lsty_car S).
+Definition lty_message {Σ} (a : action) (M : lmsg Σ) : lsty Σ :=
+  Lsty (<a> M).
 
 Definition lty_choice {Σ} (a : action) (Ss : gmap Z (lsty Σ)) : lsty Σ :=
   Lsty (<a@(x : Z)> MSG #x {{ ⌜is_Some (Ss !! x)⌝ }}; lsty_car (Ss !!! x)).
@@ -20,11 +30,25 @@ Instance: Params (@lty_choice) 2 := {}.
 Instance: Params (@lty_dual) 1 := {}.
 Instance: Params (@lty_app) 1 := {}.
 
+Notation "'TY' A ; S" := (lty_msg_base A S)
+  (at level 200, right associativity,
+   format "'TY'  A  ;  S") : lmsg_scope.
+Notation "∃ x .. y , m" :=
+  (lty_msg_exist (λ x, .. (lty_msg_exist (λ y, m)) ..)%lmsg) : lmsg_scope.
+
 Notation "'END'" := lty_end : lty_scope.
-Notation "<!!> A ; S" :=
-  (lty_message Send A S) (at level 20, A, S at level 200) : lty_scope.
-Notation "<??> A ; S" :=
-  (lty_message Recv A S) (at level 20, A, S at level 200) : lty_scope.
+Notation "<!!> M" :=
+  (lty_message Send M) (at level 200, M at level 200) : lty_scope.
+Notation "<!! x1 .. xn > M" :=
+  (lty_message Send (∃ x1, .. (∃ xn, M) ..))
+    (at level 200, x1 closed binder, xn closed binder, M at level 200,
+     format "<!!  x1  ..  xn >  M") : lty_scope.
+Notation "<??> M" :=
+  (lty_message Recv M) (at level 200, M at level 200) : lty_scope.
+Notation "<?? x1 .. xn > M" :=
+  (lty_message Recv (∃ x1, .. (∃ xn, M) ..))
+    (at level 200, x1 closed binder, xn closed binder, M at level 200,
+     format "<??  x1  ..  xn >  M") : lty_scope.
 Notation lty_select := (lty_choice Send).
 Notation lty_branch := (lty_choice Recv).
 Infix "<++>" := lty_app (at level 60) : lty_scope.
@@ -34,14 +58,27 @@ Notation "(.<++> T )" := (λ S, lty_app S T) (only parsing) : lty_scope.
 Section session_types.
   Context {Σ : gFunctors}.
 
-  Global Instance lty_message_ne a : NonExpansive2 (@lty_message Σ a).
+  Global Instance lty_msg_exist_ne k :
+    Proper (pointwise_relation _ (dist n) ==> (dist n)) (@lty_msg_exist Σ k).
+  Proof. solve_proper. Qed.
+  Global Instance lty_msg_exist_proper k :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (@lty_msg_exist Σ k).
+  Proof. solve_proper. Qed.
+  Global Instance lty_msg_base_ne a : NonExpansive2 (@lty_msg_base Σ a).
+  Proof. rewrite /lty_msg_base. solve_proper. Qed.
+  Global Instance lty_msg_base_proper a :
+    Proper ((≡) ==> (≡) ==> (≡)) (@lty_msg_base Σ a).
+  Proof. rewrite /lty_msg_base. apply ne_proper_2, _. Qed.
+  (* FIXME: Not contractive since lty_msg_exist is not contractive *)
+  (* Global Instance lty_msg_base_contractive n a : *)
+  (*   Proper (dist n ==> dist_later n ==> dist n) (@lty_msg_base Σ a). *)
+  (* Proof. rewrite /lty_msg_base. solve_contractive. Qed. *)
+
+  Global Instance lty_message_ne a : NonExpansive (@lty_message Σ a).
   Proof. solve_proper. Qed.
   Global Instance lty_message_proper a :
-    Proper ((≡) ==> (≡) ==> (≡)) (@lty_message Σ a).
-  Proof. apply ne_proper_2, _. Qed.
-  Global Instance lty_message_contractive n a :
-    Proper (dist_later n ==> dist_later n ==> dist n) (@lty_message Σ a).
-  Proof. solve_contractive. Qed.
+    Proper ((≡) ==> (≡)) (@lty_message Σ a).
+  Proof. apply ne_proper, _. Qed.
 
   Global Instance lty_choice_ne a : NonExpansive (@lty_choice Σ a).
   Proof. solve_proper. Qed.

theories/logrel/subtyping_rules.v

@@ -248,7 +248,7 @@ Section subtyping_rules.
   (** Session subtyping *)
   Lemma lty_le_send A1 A2 S1 S2 :
     ▷ (A2 <: A1) -∗ ▷ (S1 <: S2) -∗
-    (<!!> A1 ; S1) <: (<!!> A2 ; S2).
+    (<!!> TY A1 ; S1) <: (<!!> TY A2 ; S2).
   Proof.
     iIntros "#HAle #HSle !>" (v) "H". iExists v. 
     iDestruct ("HAle" with "H") as "$". by iModIntro.
@@ -256,14 +256,14 @@ Section subtyping_rules.
 
   Lemma lty_le_recv A1 A2 S1 S2 :
     ▷ (A1 <: A2) -∗ ▷ (S1 <: S2) -∗
-    (<??> A1 ; S1) <: (<??> A2 ; 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_swap_recv_send A1 A2 S :
-    ⊢ (<??> A1; <!!> A2; S) <: (<!!> A2; <??> A1; S).
+    ⊢ (<??> TY A1; <!!> TY A2; S) <: (<!!> TY A2; <??> TY A1; S).
   Proof.
     iIntros "!>" (v1 v2).
     iApply iProto_le_trans;
@@ -274,7 +274,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_swap_recv_select A Ss :
-    ⊢ (<??> A; lty_select Ss) <: lty_select ((λ S, <??> A; S) <$> Ss)%lty.
+    ⊢ (<??> TY A; lty_select Ss) <: lty_select ((λ S, <??> TY A; S) <$> Ss)%lty.
   Proof.
     iIntros "!>" (v1 x2).
     iApply iProto_le_trans;
@@ -286,7 +286,7 @@ Section subtyping_rules.
   Qed.
 
   Lemma lty_le_swap_branch_send A Ss :
-    ⊢ lty_branch ((λ S, <!!> A; S) <$> Ss)%lty <: (<!!> A; lty_branch Ss).
+    ⊢ lty_branch ((λ S, <!!> TY A; S) <$> Ss)%lty <: (<!!> TY A; lty_branch Ss).
   Proof.
     iIntros "!>" (x1 v2).
     iApply iProto_le_trans;
@@ -353,12 +353,12 @@ Section subtyping_rules.
     ⊢ (S1 <++> S2) <++> S3 <:> S1 <++> (S2 <++> S3).
   Proof. rewrite /lty_app assoc. iSplit; by iModIntro. Qed.
 
-  Lemma lty_le_app_send A S1 S2 : ⊢ (<!!> A; S1) <++> S2 <:> (<!!> A; S1 <++> S2).
+  Lemma lty_le_app_send A S1 S2 : ⊢ (<!!> TY A; S1) <++> S2 <:> (<!!> TY A; S1 <++> S2).
   Proof.
     rewrite /lty_app iProto_app_message iMsg_app_exist.
     setoid_rewrite iMsg_app_base. iSplit; by iIntros "!> /=".
   Qed.
-  Lemma lty_le_app_recv A S1 S2 : ⊢ (<??> A; S1) <++> S2 <:> (<??> A; S1 <++> S2).
+  Lemma lty_le_app_recv A S1 S2 : ⊢ (<??> TY A; S1) <++> S2 <:> (<??> TY A; S1 <++> S2).
   Proof.
     rewrite /lty_app iProto_app_message iMsg_app_exist.
     setoid_rewrite iMsg_app_base. iSplit; by iIntros "!> /=".
@@ -391,14 +391,14 @@ Section subtyping_rules.
   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 A S) <:> lty_message (action_dual a) A (lty_dual 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 A S : ⊢ lty_dual (<!!> A; S) <:> (<??> A; lty_dual S).
+  Lemma lty_le_dual_send A S : ⊢ lty_dual (<!!> TY A; S) <:> (<??> TY A; lty_dual S).
   Proof. apply lty_le_dual_message. Qed.
-  Lemma lty_le_dual_recv A S : ⊢ lty_dual (<??> A; S) <:> (<!!> A; lty_dual S).
+  Lemma lty_le_dual_recv A S : ⊢ lty_dual (<??> TY A; S) <:> (<!!> TY A; lty_dual S).
   Proof. apply lty_le_dual_message. Qed.
 
   Lemma lty_le_dual_choice a (Ss : gmap Z (lsty Σ)) :

theories/logrel/term_typing_rules.v

@@ -460,7 +460,7 @@ Section properties.
 
     Definition chansend : val := λ: "chan" "val", send "chan" "val";; "chan".
     Lemma ltyped_chansend A S :
-      ⊢ ∅ ⊨ chansend : chan (<!!> A; S) → A ⊸ chan S.
+      ⊢ ∅ ⊨ chansend : chan (<!!> TY A; S) → A ⊸ chan S.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
       iSplitL; last by iApply env_ltyped_empty.
@@ -470,7 +470,7 @@ Section properties.
     Qed.
 
     Lemma ltyped_send Γ Γ' (x : string) e A S :
-      (Γ ⊨ e : A ⫤ <[x:=(chan (<!!> A; S))%lty]> Γ') -∗
+      (Γ ⊨ e : A ⫤ <[x:=(chan (<!!> TY A; S))%lty]> Γ') -∗
       Γ ⊨ send x e : () ⫤ <[x:=(chan S)%lty]> Γ'.
     Proof.
       iIntros "#He !>" (vs) "HΓ"=> /=.
@@ -488,7 +488,7 @@ Section properties.
 
     Definition chanrecv : val := λ: "chan", (recv "chan", "chan").
     Lemma ltyped_chanrecv A S :
-      ⊢ ∅ ⊨ chanrecv : chan (<??> A; S) → A * chan S.
+      ⊢ ∅ ⊨ chanrecv : chan (<??> TY A; S) → A * chan S.
     Proof.
       iIntros (vs) "!> HΓ /=". iApply wp_value.
       iSplitL; last by iApply env_ltyped_empty.
@@ -498,7 +498,7 @@ Section properties.
     Qed.
 
     Lemma ltyped_recv Γ (x : string) A S :
-      ⊢ <[x := (chan (<??> A; S))%lty]> Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
+      ⊢ <[x := (chan (<??> TY A; S))%lty]> Γ ⊨ recv x : A ⫤ <[x:=(chan S)%lty]> Γ.
     Proof.
       iIntros "!>" (vs) "HΓ"=> /=.
       iDestruct (env_ltyped_lookup with "HΓ") as (v' Heq) "[Hc HΓ]".