Formalized Send Session Type Triple

theories/channel.v

@@ -82,11 +82,17 @@ 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.
 
+  Global Instance chan_ctx_persistent : Persistent (chan_ctx γ c).
+  Proof. by apply _. Qed.
+
   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.
 
+  Global Instance chan_frag_timeless : Timeless (chan_frag γ c ls rs).
+  Proof. by apply _. Qed.
+
   Definition is_chan (γ : chan_name) (c : val) (ls rs : list val) : iProp Σ :=
     (chan_ctx γ c ∗ chan_frag γ c ls rs)%I.
 
@@ -122,22 +128,19 @@ Section channel.
     eauto 10 with iFrame.
   Qed.
 
-  Definition send_upd γ c ls rs s v : iProp Σ :=
+  Definition chan_frag_snoc γ c ls rs s v : iProp Σ :=
     match s with
     | 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,
-      chan_frag γ c ls rs ∗
-      (send_upd γ c ls rs s v ={E,⊤}=∗ Φ #()))%I.
-
   Lemma send_spec Φ E γ (c v s : val) :
     is_side s →
     chan_ctx γ c -∗
-    send_vs E γ c s Φ v -∗
+    (|={⊤,E}=> ∃ ls rs,
+      chan_frag γ c ls rs ∗
+      ▷ (chan_frag_snoc γ c ls rs s v ={E,⊤}=∗ Φ #())) -∗
     WP send c s v {{ Φ }}.
   Proof.
     iIntros (Hside) "Hc HΦ". wp_lam; wp_pures.
@@ -147,8 +150,9 @@ Section channel.
     destruct Hside as [-> | ->].
     - wp_pures. iDestruct "Hl" as (ll lhd ->) "(Hl & Hll)".
       wp_load. wp_apply (lsnoc_spec with "Hll").
-      iIntros (hd') "Hll". wp_store. wp_pures.
-      iApply fupd_wp. iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
+      iIntros (hd') "Hll". wp_pures.
+      wp_bind (_ <- _)%E. iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
+      wp_store.
       iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hls' Hrs']".
       iDestruct (excl_eq with "Hls Hls'") as %->.
       iMod (excl_update _ _ _ (ls ++ [v]) with "Hls Hls'") as "[Hls Hls']".
@@ -160,8 +164,9 @@ Section channel.
       iIntros "_ //".
     - wp_pures. iDestruct "Hr" as (lr rhd ->) "(Hr & Hlr)".
       wp_load. wp_apply (lsnoc_spec with "Hlr").
-      iIntros (hd') "Hlr". wp_store. wp_pures.
-      iApply fupd_wp. iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
+      iIntros (hd') "Hlr". wp_pures.
+      wp_bind (_ <- _)%E. iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
+      wp_store.
       iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hls' Hrs']".
       iDestruct (excl_eq with "Hrs Hrs'") as %->.
       iMod (excl_update _ _ _ (rs ++ [v]) with "Hrs Hrs'") as "[Hrs Hrs']".

theories/logrel.v

@@ -8,7 +8,6 @@ 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).
@@ -44,28 +43,48 @@ Section logrel.
         st_eval (v::vs) st1 (TRecv P st2).
   Hint Constructors st_eval.
 
+  Lemma st_eval_send :
+    ∀ (P : val → Prop) (st : val → stype) (l : list val) (str : stype) (v : val),
+      P v → st_eval l (TSend P st) str → st_eval (l ++ [v]) (st v) str.
+  Proof.
+    intros P st l str v HP Heval.
+    generalize dependent str.
+    induction l; intros.
+    - inversion Heval; by constructor.
+    - inversion Heval; subst. simpl.
+      constructor=> //.
+      apply IHl=> //.
+  Qed.
+
   Definition inv_st (γ :st_name) (c : val) : iProp Σ :=
     (∃ l r stl str,
-      is_chan N (st_c_name γ) c l r ∗
+      chan_frag (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.
+      ((⌜r = []⌝ ∗ ⌜st_eval l stl str⌝) ∨ 
+       (⌜l = []⌝ ∗ ⌜st_eval r str stl⌝)))%I.
+
+  Definition st_ctx (γ : st_name) (st : stype) (c : val) : iProp Σ :=
+    (chan_ctx N (st_c_name γ) c ∗ inv N (inv_st γ c))%I.
 
-  Definition interp_st (γ : st_name) (st : stype) c s : iProp Σ :=
-    (stmapsto_frag γ st s ∗ inv N (inv_st γ c))%I.
+  Definition st_frag  (γ : st_name) (st : stype) (s : side) : iProp Σ :=
+    stmapsto_frag γ st s.
 
-  Notation "⟦ ep : sτ ⟧{ γ }" :=
-  (interp_st γ sτ (ep.1) (ep.2))
-    (ep at level 99).
+  Definition interp_st (γ : st_name) (st : stype) (c : val) (s : side) : iProp Σ :=
+    (st_frag γ st s ∗ st_ctx γ st c)%I.
 
+  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st γ sτ c s)
+    (at level 10, s at next level, sτ at next level, γ at next level,
+     format "⟦  c  @  s  :  sτ  ⟧{ γ }").
+
+  
   Lemma new_chan_vs st E c cγ :
     is_chan N cγ c [] [] ={E}=∗
-      ∃ lγ rγ, 
+      ∃ lγ rγ,
         let γ := SessionType_name cγ lγ rγ in
-        ⟦ (c,Left) : st ⟧{γ} ∗ ⟦ (c,Right) : (dual_stype st) ⟧{γ}.
+        ⟦ c @ Left : st ⟧{γ} ∗ ⟦ c @ Right : dual_stype st ⟧{γ}.
   Proof.
-    iIntros "Hc".
+    iIntros "[#Hcctx Hcf]".
     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)). 
@@ -74,15 +93,18 @@ Section logrel.
     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".
+    iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
     { iNext. rewrite /inv_st. eauto 10 with iFrame. }
-    eauto 10 with iFrame.
+    iModIntro.
+    iExists _, _.
+    iFrame. simpl.
+    repeat iSplitL=> //.
   Qed.
   
   Lemma new_chan_st_spec st :
     {{{ True }}}
       new_chan #()
-    {{{ c γ, RET c; ⟦ (c,Left) : st ⟧{γ} ∗ ⟦ (c,Right) : dual_stype st ⟧{γ} }}}.
+    {{{ c γ, RET c;  ⟦ c @ Left : st ⟧{γ} ∗ ⟦ c @ Right : dual_stype st ⟧{γ} }}}.
   Proof.
     iIntros (Φ _) "HΦ".
     iApply (wp_fupd).
@@ -95,6 +117,92 @@ Section logrel.
     iApply "HΦ".
     iModIntro.
     iFrame.
-  Qed.      
+  Qed.
+
+Lemma send_vs c γ s (P : val → Prop) st E :
+    ↑N ⊆ E →
+    ⟦ c @ s : TSend P st ⟧{γ} ={E,E∖↑N}=∗
+      ∃ l r, chan_frag (st_c_name γ) c l r ∗
+      ▷ (∀ v, ⌜P v⌝ -∗ 
+              match s with 
+              | Left  => chan_frag (st_c_name γ) c (l ++ [v]) r
+              | Right => chan_frag (st_c_name γ) c l (r ++ [v])
+              end ={E∖ ↑N,E}=∗ ⟦ c @ s : st v ⟧{γ}).
+  Proof.
+    iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
+    iMod (inv_open with "Hinv") as "Hinv'"=> //.
+    iDestruct "Hinv'" as "[Hinv' Hinvstep]".
+    iDestruct "Hinv'" as (l r stl str) "(>Hcf & Hstla & Hstra & Hinv')".
+    iModIntro.
+    rewrite /stmapsto_frag /stmapsto_full.
+    iExists l, r.
+    iIntros "{$Hcf} !>" (v HP) "Hcf".
+    destruct s.
+    - iRename "Hstf" into "Hstlf".
+      iDestruct (excl_eq with "Hstla Hstlf") as %<-.
+      iMod (excl_update _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]".
+      iMod ("Hinvstep" with "[-Hstlf]") as "_".
+      { iNext.
+        iExists _,_,_,_. iFrame.
+        iLeft.
+        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]";
+          iDestruct "Heval" as %Heval.
+        - iSplit=> //.
+          iPureIntro.
+          by eapply st_eval_send.
+        - inversion Heval; subst.
+          iSplit=> //.
+          iPureIntro.
+          destruct str; inversion H2.
+          apply st_eval_cons=> //. subst.
+          rewrite (involutive (st0 v)).
+          rewrite -(involutive (dual_stype (st0 v))).
+          constructor. }
+      iModIntro. iFrame "Hcctx ∗ Hinv".
+    - iRename "Hstf" into "Hstrf".
+      iDestruct (excl_eq with "Hstra Hstrf") as %<-.
+      iMod (excl_update _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]".
+      iMod ("Hinvstep" with "[-Hstrf]") as "_".
+      { iNext.
+        iExists _,_. iFrame.
+        iExists _,_. iFrame.
+        iRight.
+        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]";
+          iDestruct "Heval" as %Heval.
+        - inversion Heval; subst.
+          iSplit=> //.
+          iPureIntro.
+          destruct stl; inversion H2.
+          apply st_eval_cons=> //. subst.
+          rewrite (involutive (st0 v)).
+          rewrite -(involutive (dual_stype (st0 v))).
+          constructor.
+        - iSplit=> //.
+          iPureIntro.
+          by eapply st_eval_send. }
+      iModIntro. iFrame "Hcctx ∗ Hinv".
+  Qed.
+
+  Definition to_side s :=
+    match s with
+    | Left  => #true
+    | Right => #false
+    end.
+
+  Lemma send_st_spec st γ c s (P : val → Prop) v :
+    P v →
+    {{{ ⟦ c @ s : TSend P st ⟧{γ} }}}
+      send c (to_side s) v
+    {{{ RET #(); ⟦ c @ s : st v ⟧{γ} }}}.
+  Proof.
+    iIntros (HP Φ) "Hsend HΦ".
+    iApply (send_spec with "[#]").
+    { destruct s. by left. by right. }
+    { iDestruct "Hsend" as "[? [$ ?]]". }
+    iMod (send_vs with "Hsend") as (ls lr) "[Hch H]"; first done.
+    iModIntro. iExists ls, lr. iFrame "Hch".
+    iIntros "!> Hupd". iApply "HΦ".
+    iApply ("H" $! v HP with "[Hupd]"). by destruct s.
+  Qed.
 
 End logrel.
\ No newline at end of file

theories/typing.v

 From iris.heap_lang Require Export lang.
+Require Import FunctionalExtensionality.
 
-Section typing.
+Inductive side : Set :=
+| Left
+| Right.
 
-  Inductive side : Set :=
-  | Left
-  | Right.
+Inductive stype :=
+| TEnd
+| TSend (P : val → Prop) (st : val → stype)
+| TRecv (P : val → Prop) (st : val → stype).
 
-  Inductive stype :=
-  | TEnd
-  | TSend (P : val → Prop) (sτ : val → stype)
-  | TRecv (P : val → Prop) (sτ : val → stype).
+Instance stype_inhabited : Inhabited stype := populate TEnd.
 
-  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.
+Fixpoint dual_stype (st :stype) :=
+  match st with
+  | TEnd => TEnd
+  | TSend P st => TRecv P (λ v, dual_stype (st v))
+  | TRecv P st => TSend P (λ v, dual_stype (st v))
+  end.
 
-End typing.
+Class Involutive {T} (f : T → T) :=
\ No newline at end of file
+  involutive : ∀ t : T, t = f (f t).
+
+Instance dual_stype_involutive : Involutive dual_stype.
+Proof.
+  intros st.
+  induction st => //; simpl;
+    assert (st = (λ v : val, dual_stype (dual_stype (st v)))) as Heq
+        by apply functional_extensionality => //;
+    rewrite -Heq => //.
+Qed.