Introduced session types and logical relation.

Made initial definition of session type allocation on new channel creation.

_CoqProject

@@ -3,4 +3,5 @@
 theories/list.v
 theories/auth_excl.v
 theories/channel.v
-
+theories/typing.v
+theories/logrel.v
\ No newline at end of file

theories/auth_excl.v

@@ -4,6 +4,28 @@ From iris.algebra Require Import excl auth.
 From iris.base_logic.lib Require Import auth.
 Set Default Proof Using "Type".
 
+(* Definition exclUR (A : Type) : ucmraT := *)
+(*   optionUR (exclR (leibnizC A)). *)
+
+(* Definition to_auth_excl {A : Type} (a : A) : exclUR A := *)
+(*   Excl' (a: leibnizC A). *)
+
+(* Section auth_excl. *)
+
+(* Class auth_exclG (A : Type) (Σ :gFunctors) := *)
+(*   AuthExclG { *)
+(*       exclG_authG :> authG Σ (exclUR A); *)
+(*     }. *)
+
+(* Definition auth_exclΣ (A : Type) : gFunctors := *)
+(*   #[GFunctor (authR (exclUR A))]. *)
+
+(* Instance subG_auth_exclG {Σ} (A : Type) : *)
+(*   subG (auth_exclΣ) Σ → (auth_exclG) Σ. *)
+(* Proof. solve_inG. Qed. *)
+
+(* End auth_excl. *)
+
 Definition exclUR (A : Type) : ucmraT :=
   optionUR (exclR (leibnizC A)).
 
@@ -22,6 +44,7 @@ Proof. solve_inG. Qed.
 Definition to_auth_excl {A : Type} (a : A) : exclUR A :=
   Excl' (a: leibnizC A).
 
+
 Section auth_excl.
   Context `{!auth_exclG A Σ} (N : namespace).
 

theories/channel.v

@@ -82,17 +82,20 @@ Section channel.
         is_list_ref l ls ∗ own (chan_l_name γ) (● to_auth_excl ls) ∗
         is_list_ref r rs ∗ own (chan_r_name γ) (● to_auth_excl rs)))%I.
 
-  Definition is_chan (γ : chan_name) (c : val) (ls rs : list val) : iProp Σ :=
+  Definition chan_frag (γ : chan_name) (c : val) (ls rs : list val) : iProp Σ :=
     (∃ l r lk : val,
       ⌜c = ((l, r), lk)%V⌝ ∧
       own (chan_l_name γ) (◯ to_auth_excl ls) ∗ own (chan_r_name γ) (◯ to_auth_excl rs))%I.
 
+  Definition is_chan (γ : chan_name) (c : val) (ls rs : list val) : iProp Σ :=
+    (chan_ctx γ c ∗ chan_frag γ c ls rs)%I.
+
   Lemma new_chan_spec :
     {{{ True }}}
       new_chan #()
-    {{{ c γ, RET c; is_chan γ c [] [] ∗ chan_ctx γ c }}}.
+    {{{ c γ, RET c; is_chan γ c [] [] }}}.
   Proof. 
-    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_ctx /is_lock.
+    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_ctx /chan_frag /is_lock.
     repeat wp_lam. wp_alloc lk as "Hlk".
     iMod (own_alloc (Excl ())) as (lkγ) "Hγlk"; first done.
     repeat wp_lam. wp_alloc r as "Hr".
@@ -114,21 +117,21 @@ Section channel.
     }
     wp_pures.
     iSpecialize ("HΦ" $!(#l, #r, #lk)%V c).
-    iApply ("HΦ"). 
-    iSplitL "Hlsf Hrsf"=> //;
+    iApply ("HΦ").
+    iSplitR "Hlsf Hrsf"=> //;
     eauto 10 with iFrame.
   Qed.
 
   Definition send_upd γ c ls rs s v : iProp Σ :=
     match s with
-    | left  => is_chan γ c (ls ++ [v]) rs
-    | right => is_chan γ c ls (rs ++ [v])
+    | left  => chan_frag γ c (ls ++ [v]) rs
+    | right => chan_frag γ c ls (rs ++ [v])
     | _ => ⌜False⌝%I
     end.
 
   Definition send_vs E γ c s Φ v :=
     (|={⊤,E}=> ∃ ls rs,
-      is_chan γ c ls rs ∗
+      chan_frag γ c ls rs ∗
       (send_upd γ c ls rs s v ={E,⊤}=∗ Φ #()))%I.
 
   Lemma send_spec Φ E γ (c v s : val) :
@@ -150,7 +153,7 @@ Section channel.
       iDestruct (excl_eq with "Hls Hls'") as %->.
       iMod (excl_update _ _ _ (ls ++ [v]) with "Hls Hls'") as "[Hls Hls']".
       iMod ("HΦ" with "[Hls' Hrs']") as "HΦ".
-      { rewrite /= /is_chan. eauto with iFrame. }
+      { rewrite /= /chan_frag. eauto with iFrame. }
       iModIntro.
       wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]").
       { rewrite /is_list_ref. eauto 10 with iFrame. }
@@ -163,25 +166,24 @@ Section channel.
       iDestruct (excl_eq with "Hrs Hrs'") as %->.
       iMod (excl_update _ _ _ (rs ++ [v]) with "Hrs Hrs'") as "[Hrs Hrs']".
       iMod ("HΦ" with "[Hls' Hrs']") as "HΦ".
-      { rewrite /= /is_chan. eauto with iFrame. }
+      { rewrite /= /chan_frag. eauto with iFrame. }
       iModIntro.
       wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]").
       { rewrite /is_list_ref. eauto 10 with iFrame. }
       iIntros "_ //".
   Qed.
 
-
   Definition try_recv_upd_fail γ c ls rs s : iProp Σ :=
     match s with
-    | left  => (is_chan γ c ls rs ∧ ⌜rs = []⌝)%I
-    | right => (is_chan γ c ls rs ∧ ⌜ls = []⌝)%I
+    | left  => (chan_frag γ c ls rs ∧ ⌜rs = []⌝)%I
+    | right => (chan_frag γ c ls rs ∧ ⌜ls = []⌝)%I
     | _ => ⌜False⌝%I
     end.
 
   Definition try_recv_upd_succ γ c ls rs s v : iProp Σ :=
     match s with
-    | left =>  (∃ rs', is_chan γ c ls  rs' ∧ ⌜rs = v::rs'⌝)%I
-    | right => (∃ ls', is_chan γ c ls' rs  ∧ ⌜ls = v::ls'⌝)%I
+    | left =>  (∃ rs', chan_frag γ c ls  rs' ∧ ⌜rs = v::rs'⌝)%I
+    | right => (∃ ls', chan_frag γ c ls' rs  ∧ ⌜ls = v::ls'⌝)%I
     | _ => ⌜False⌝%I
     end.
 
@@ -194,7 +196,7 @@ Section channel.
 
   Definition try_recv_vs E γ c s Φ :=
     (|={⊤,E}=> ∃ ls rs,
-      is_chan γ c ls rs ∗
+      chan_frag γ c ls rs ∗
       (∀ v, try_recv_upd γ c ls rs s v ={E,⊤}=∗ Φ v))%I.
 
   Lemma try_recv_spec Φ E γ (c s : val) :
@@ -220,7 +222,7 @@ Section channel.
         iDestruct (excl_eq with "Hrsa Hrsf") as %->.
         iSpecialize ("HΦ" $!(InjLV #())).
         iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_upd /try_recv_upd_fail /is_chan. eauto 10 with iFrame. } 
+        { rewrite /try_recv_upd /try_recv_upd_fail /chan_frag. eauto 10 with iFrame. } 
         iModIntro.
         wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
         { rewrite /is_list_ref /is_list. eauto 10 with iFrame. }
@@ -237,7 +239,7 @@ Section channel.
         iDestruct (excl_update _ _ _ (rs) with "Hrsa Hrsf") as ">[Hrsa Hrsf]".
         iSpecialize ("HΦ" $!(InjRV (v))).
         iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_upd /try_recv_upd_succ /is_chan. eauto 10 with iFrame. }
+        { rewrite /try_recv_upd /try_recv_upd_succ /chan_frag. eauto 10 with iFrame. }
         iModIntro.
         wp_store.
         wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
@@ -257,7 +259,7 @@ Section channel.
         iDestruct (excl_eq with "Hrsa Hrsf") as %->.
         iSpecialize ("HΦ" $!(InjLV #())).
         iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_upd /try_recv_upd_fail /is_chan. eauto 10 with iFrame. } 
+        { rewrite /try_recv_upd /try_recv_upd_fail /chan_frag. eauto 10 with iFrame. } 
         iModIntro.
         wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
         { rewrite /is_list_ref /is_list. eauto 10 with iFrame. }
@@ -274,7 +276,7 @@ Section channel.
         iDestruct (excl_update _ _ _ (ls) with "Hlsa Hlsf") as ">[Hlsa Hlsf]".
         iSpecialize ("HΦ" $!(InjRV (v))).
         iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_upd /try_recv_upd_succ /is_chan. eauto 10 with iFrame. }
+        { rewrite /try_recv_upd /try_recv_upd_succ /chan_frag. eauto 10 with iFrame. }
         iModIntro.
         wp_store.
         wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
@@ -286,7 +288,7 @@ Section channel.
 
   Definition recv_vs E γ c s Φ :=
     (□ (|={⊤,E}=> ∃ ls rs,
-      is_chan γ c ls rs ∗
+      chan_frag γ c ls rs ∗
         ((try_recv_upd_fail γ c ls rs s ={E,⊤}=∗ True) ∗
          (∀ v, try_recv_upd_succ γ c ls rs s v ={E,⊤}=∗ Φ v))))%I.
 

theories/logrel.v

+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang.lib Require Import lock.
+From iris.heap_lang.lib Require Import spin_lock.
+From osiris Require Import typing auth_excl channel.
+From iris.algebra Require Import list auth excl.
+From iris.base_logic Require Import invariants auth saved_prop.
+Require Import FunctionalExtensionality.
+Import uPred.
+
+Section logrel.
+  Context `{!heapG Σ, !lockG Σ} (N : namespace).
+  Context `{!auth_exclG (list val) Σ}.
+  Context `{!auth_exclG stype Σ}.
+  
+  Record st_name := SessionType_name {
+    st_c_name : chan_name;
+    st_l_name : gname;
+    st_r_name : gname
+  }.
+
+  Definition stmapsto_frag γ (st : stype) s : iProp Σ :=
+    let γ :=
+        match s with
+        | Left  => st_l_name γ
+        | Right => st_r_name γ
+        end in
+    own γ (◯  to_auth_excl st)%I.
+
+  Definition stmapsto_full γ (st : stype) s : iProp Σ :=
+    let γ :=
+        match s with
+        | Left  => st_l_name γ
+        | Right => st_r_name γ
+        end in
+    own γ (● to_auth_excl st)%I.
+
+  Inductive st_eval : list val -> stype -> stype -> Prop :=
+    | st_eval_nil st : st_eval [] st (dual_stype st)
+    | st_eval_cons (P:val -> Prop) v vs st1 st2 :
+        P v -> st_eval vs st1 (st2 v) ->
+        st_eval (v::vs) st1 (TRecv P st2).
+  Hint Constructors st_eval.
+
+  Definition inv_st (γ :st_name) (c : val) : iProp Σ :=
+    (∃ l r stl str,
+      is_chan N (st_c_name γ) c l r ∗
+      stmapsto_full γ stl Left  ∗
+      stmapsto_full γ str Right ∗
+      ((⌜r = []⌝ ∗ ⌜st_eval r stl str⌝) ∨ 
+       (⌜l = []⌝ ∗ ⌜st_eval l stl str⌝)))%I.
+
+  Definition interp_st (γ : st_name) (st : stype) c s : iProp Σ :=
+    (stmapsto_frag γ st s ∗ inv N (inv_st γ c))%I.
+
+  Notation "⟦ ep : sτ ⟧{ γ }" :=
+  (interp_st γ sτ (ep.1) (ep.2))
+    (ep at level 99).
+
+  Lemma new_chan_vs st E c cγ :
+    is_chan N cγ c [] [] ={E}=∗
+      ∃ lγ rγ, 
+        let γ := SessionType_name cγ lγ rγ in
+        ⟦ (c,Left) : st ⟧{γ} ∗ ⟦ (c,Right) : (dual_stype st) ⟧{γ}.
+  Proof.
+    iIntros "Hc".
+    iMod (own_alloc (Auth (Excl' (to_auth_excl st)) (to_auth_excl st))) as (lγ) "Hlst"; first done.
+    iMod (own_alloc (Auth (Excl' (to_auth_excl (dual_stype st))) (to_auth_excl (dual_stype st)))) as (rγ) "Hrst"; first done.
+    rewrite (auth_both_op (to_auth_excl st)). 
+    rewrite (auth_both_op (to_auth_excl (dual_stype st))). 
+    rewrite own_op own_op.
+    iDestruct "Hlst" as "[Hlsta Hlstf]".
+    iDestruct "Hrst" as "[Hrsta Hrstf]".
+    pose (SessionType_name cγ lγ rγ) as stγ.
+    iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf]") as "#Hinv".
+    { iNext. rewrite /inv_st. eauto 10 with iFrame. }
+    eauto 10 with iFrame.
+  Qed.
+  
+  Lemma new_chan_st_spec st :
+    {{{ True }}}
+      new_chan #()
+    {{{ c γ, RET c; ⟦ (c,Left) : st ⟧{γ} ∗ ⟦ (c,Right) : dual_stype st ⟧{γ} }}}.
+  Proof.
+    iIntros (Φ _) "HΦ".
+    iApply (wp_fupd).
+    iApply (new_chan_spec)=> //.
+    iModIntro.
+    iIntros (c γ) "[Hc Hctx]".
+    iMod (new_chan_vs st ⊤ c γ with "[-HΦ]") as "H".
+    { rewrite /is_chan. eauto with iFrame. }
+    iDestruct "H" as (lγ rγ) "[Hl Hr]".
+    iApply "HΦ".
+    iModIntro.
+    iFrame.
+  Qed.      
+
+End logrel.
\ No newline at end of file

theories/typing.v

+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From stdpp Require Import gmap.
+From iris.base_logic Require Import invariants.
+Require Import FunctionalExtensionality.
+
+Section typing.
+
+  (* Sides *)
+  Inductive side : Set :=
+  | Left
+  | Right.
+
+  (* Session Types *)
+  Inductive stype :=
+  | TEnd
+  | TSend (P : heap_lang.val → Prop) (sτ : heap_lang.val → stype)
+  | TRecv (P : heap_lang.val → Prop) (sτ : heap_lang.val → stype).
+
+  Fixpoint dual_stype (sτ :stype) :=
+    match sτ with
+    | TEnd => TEnd
+    | TSend P sτ => TRecv P (λ v, dual_stype (sτ v))
+    | TRecv P sτ => TSend P (λ v, dual_stype (sτ v))
+    end.
+
+End typing.
\ No newline at end of file