Changed side matching to inline, making proofs less branchy

_CoqProject

@@ -2,6 +2,6 @@
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
 theories/list.v
 theories/auth_excl.v
-theories/channel.v
 theories/typing.v
+theories/channel.v
 theories/logrel.v
\ No newline at end of file

theories/channel.v

@@ -7,6 +7,7 @@ From iris.base_logic.lib Require Import auth.
 From iris.heap_lang.lib Require Import spin_lock.
 From osiris Require Import list.
 From osiris Require Import auth_excl.
+From osiris Require Import typing.
 Set Default Proof Using "Type".
 Import uPred.
 
@@ -17,20 +18,17 @@ Definition new_chan : val :=
      let: "lk" := newlock #() in
      (("l","r"),"lk").
 
-Inductive side := Left | Right.
 Coercion side_to_bool (s : side) : bool :=
   match s with Left => true | Right => false end.
+Definition side_elim {A} (s : side) (l r : A) : A :=
+  match s with Left => l | Right => r end.
 
-Definition get_buffs c := Fst c.
-Definition get_left c := Fst (get_buffs c).
-Definition get_right c := Snd (get_buffs c).
-Definition get_lock c := Snd c.
+Definition get_side : val := λ: "c" "s",
+  (if: "s" = #Left then Fst (Fst "c") else Snd (Fst "c"))%E.
+Definition get_lock : val := λ: "c", Snd "c".
 
-Definition dual_side s :=
-  (if: s = #Left then #Right else #Left)%E.
-
-Definition get_side c s :=
-  (if: s = #Left then get_left c else get_right c)%E.
+Definition get_dual_side : val := λ: "s",
+  (if: "s" = #Left then #Right else #Left)%E.
 
 Definition send : val :=
   λ: "c" "s" "v",
@@ -44,11 +42,13 @@ Definition try_recv : val :=
   λ: "c" "s",
     let: "lk" := get_lock "c" in
     acquire "lk";;
-    let: "l" := (get_side "c" (dual_side "s")) in
-    match: !"l" with
-      SOME "p" => "l" <- Snd "p";; release "lk";; SOME (Fst "p")
-    | NONE => release "lk";; NONE
-    end.
+    let: "l" := get_side "c" (get_dual_side "s") in
+    let: "ret" :=
+      match: !"l" with
+        SOME "p" => "l" <- Snd "p";; SOME (Fst "p")
+      | NONE => NONE
+      end in
+    release "lk";; "ret".
 
 Definition recv : val :=
   rec: "go" "c" "s" :=
@@ -69,34 +69,46 @@ Section channel.
     chan_r_name : gname
   }.
 
-  Definition chan_ctx (γ : chan_name) (c : val) : iProp Σ :=
+  Definition chan_inv (γ : chan_name) (l r : val) : iProp Σ :=
+    (∃ ls rs,
+      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.
+  Typeclasses Opaque chan_inv.
+
+  Definition is_chan (γ : chan_name) (c : val) : iProp Σ :=
     (∃ l r lk : val,
       ⌜c = ((l, r), lk)%V⌝ ∧
-      is_lock N (chan_lock_name γ) lk (∃ ls rs,
-        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.
+      is_lock N (chan_lock_name γ) lk (chan_inv γ l r))%I.
 
-  Global Instance chan_ctx_persistent : Persistent (chan_ctx γ c).
+  Global Instance is_chan_persistent : Persistent (is_chan γ 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.
+  Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
+    own (side_elim s chan_l_name chan_r_name γ) (◯ to_auth_excl vs)%I.
 
-  Global Instance chan_frag_timeless : Timeless (chan_frag γ c ls rs).
+  Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
   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.
+  Lemma get_side_spec Φ s (l r lk : val) :
+    Φ (side_elim s l r) -∗
+    WP get_side ((l, r), lk)%V #s {{ Φ }}.
+  Proof. iIntros "?". wp_lam. by destruct s; wp_pures. Qed.
+
+  Lemma get_lock_spec Φ (l r lk : val) :
+    Φ lk -∗
+    WP get_lock ((l, r), lk)%V {{ Φ }}.
+  Proof. iIntros "?". wp_lam. by wp_pures. Qed.
+
+  Lemma dual_side_spec Φ s :
+    Φ #(dual_side s) -∗ WP get_dual_side #s {{ Φ }}.
+  Proof. iIntros "?". wp_lam. by destruct s; wp_pures. Qed.
 
   Lemma new_chan_spec :
     {{{ True }}}
       new_chan #()
-    {{{ c γ, RET c; is_chan γ c [] [] }}}.
+    {{{ c γ, RET c; is_chan γ c ∗ chan_own γ Left [] ∗ chan_own γ Right [] }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_ctx /chan_frag.
+    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_own.
     wp_lam.
     wp_apply (lnil_spec with "[//]"); iIntros (ls Hls). wp_alloc l as "Hl".
     wp_apply (lnil_spec with "[//]"); iIntros (rs Hrs). wp_alloc r as "Hr".
@@ -114,187 +126,120 @@ Section channel.
                 with "[Hl Hr Hls Hrs]").
     { eauto 10 with iFrame. }
     iIntros (lk γlk) "#Hlk". wp_pures.
-    iApply ("HΦ" $! _ (Chan_name γlk lsγ rsγ)).
-    eauto 20 with iFrame.
+    iApply ("HΦ" $! _ (Chan_name γlk lsγ rsγ)); simpl.
+    rewrite /chan_inv /=. eauto 20 with iFrame.
   Qed.
 
-  Definition chan_frag_snoc (γ : chan_name) (c : val)
-             (l r : list val) (s : side) (v : val)
-    : iProp Σ :=
-    match s with
-    | Left  => chan_frag γ c (l ++ [v]) r
-    | Right => chan_frag γ c l (r ++ [v])
-    end.
+  Lemma chan_inv_alt s γ l r :
+    chan_inv γ l r ⊣⊢ ∃ ls rs,
+      is_list_ref (side_elim s l r) ls ∗
+      own (side_elim s chan_l_name chan_r_name γ) (● to_auth_excl ls) ∗
+      is_list_ref (side_elim s r l) rs ∗
+      own (side_elim s chan_r_name chan_l_name γ) (● to_auth_excl rs).
+  Proof.
+    destruct s; rewrite /chan_inv //=.
+    iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
+  Qed.
 
   Lemma send_spec Φ E γ c v s :
-    chan_ctx γ c -∗
-    (|={⊤,E}=> ∃ ls rs,
-      chan_frag γ c ls rs ∗
-      ▷ (chan_frag_snoc γ c ls rs s v ={E,⊤}=∗ Φ #())) -∗
+    is_chan γ c -∗
+    (|={⊤,E}=> ∃ vs,
+      chan_own γ s vs ∗
+      ▷ (chan_own γ s (vs ++ [v]) ={E,⊤}=∗ Φ #())) -∗
     WP send c #s v {{ Φ }}.
   Proof.
     iIntros "Hc HΦ". wp_lam; wp_pures.
     iDestruct "Hc" as (l r lk ->) "#Hlock"; wp_pures.
+    wp_apply get_lock_spec; wp_pures.
     wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
-    iDestruct "Hinv" as (ls rs) "(Hl & Hls & Hr & Hrs)".
-    destruct s.
-    - wp_pures. iDestruct "Hl" as (ll lhd ->) "(Hl & Hll)".
-      wp_load. wp_apply (lsnoc_spec with "Hll").
-      iIntros (hd' Hll).
-      wp_bind (_ <- _)%E. iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
-      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']".
-      wp_store.
-      iMod ("HΦ" with "[Hls' Hrs']") as "HΦ".
-      { rewrite /= /chan_frag. eauto with iFrame. }
-      iModIntro.
-      wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
-      { rewrite /is_list_ref. eauto 10 with iFrame. }
-    - wp_pures. iDestruct "Hr" as (lr rhd ->) "(Hr & Hlr)".
-      wp_load. wp_apply (lsnoc_spec with "Hlr").
-      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']".
-      iMod ("HΦ" with "[Hls' Hrs']") as "HΦ".
-      { rewrite /= /chan_frag. eauto with iFrame. }
-      iModIntro.
-      wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
-      { rewrite /is_list_ref. eauto 10 with iFrame. }
+    wp_apply get_side_spec; wp_pures.
+    iDestruct (chan_inv_alt s with "Hinv") as
+        (vs ws) "(Href & Hvs & Href' & Hws)".
+    iDestruct "Href" as (ll lhd Hslr) "(Hll & Hlvs)"; rewrite Hslr.
+    wp_load. wp_apply (lsnoc_spec with "Hlvs"). iIntros (lhd' Hlvs).
+    wp_bind (_ <- _)%E.
+    iMod "HΦ" as (vs') "[Hchan HΦ]".
+    iDestruct (excl_eq with "Hvs Hchan") as %->.
+    iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]".
+    wp_store. iMod ("HΦ" with "Hchan") as "HΦ".
+    iModIntro.
+    wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
+    iApply (chan_inv_alt s).
+    rewrite /is_list_ref. eauto 10 with iFrame.
   Qed.
 
-  Definition try_recv_fail (γ : chan_name) (c : val)
-             (l r : list val) (s : side) : iProp Σ :=
-    match s with
-    | Left  => (chan_frag γ c l r ∧ ⌜r = []⌝)%I
-    | Right => (chan_frag γ c l r ∧ ⌜l = []⌝)%I
-    end.
-
-  Definition try_recv_succ (γ : chan_name) (c : val)
-             (l r : list val) (s : side) (v : val) : iProp Σ :=
-    match s with
-    | Left =>  (∃ r', chan_frag γ c l  r' ∧ ⌜r = v::r'⌝)%I
-    | Right => (∃ l', chan_frag γ c l' r  ∧ ⌜l = v::l'⌝)%I
-    end.
-
   Lemma try_recv_spec Φ E γ c s :
-    chan_ctx γ c -∗
-    (|={⊤,E}=> ∃ ls rs,
-      chan_frag γ c ls rs ∗
-      ▷ ((try_recv_fail γ c ls rs s ={E,⊤}=∗ Φ NONEV) ∧
-         (∀ v, try_recv_succ γ c ls rs s v ={E,⊤}=∗ Φ (SOMEV v)))) -∗
+    is_chan γ c -∗
+    (|={⊤,E}=> ∃ vs,
+      chan_own γ (dual_side s) vs ∗
+      ▷ ((⌜vs = []⌝ -∗ chan_own γ (dual_side s) vs ={E,⊤}=∗ Φ NONEV) ∧
+         (∀ v vs', ⌜vs = v :: vs'⌝ -∗
+                   chan_own γ (dual_side s) vs' ={E,⊤}=∗ Φ (SOMEV v)))) -∗
     WP try_recv c #s {{ Φ }}.
   Proof.
     iIntros "Hc HΦ". wp_lam; wp_pures.
     iDestruct "Hc" as (l r lk ->) "#Hlock"; wp_pures.
-    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]".
-    iDestruct "Hinv" as (ls rs) "(Hls & Hlsa & Hrs & Hrsa)".
-    destruct s; simpl.
-    - iDestruct "Hrs" as (rl rhd ->) "[Hrs #Hrhd]".
-      wp_pures.
-      wp_bind (Load _).
-      iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
-      wp_load.
-      destruct rs; simpl.
-      + iDestruct "Hrhd" as %->.
-        iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hlsf Hrsf]".
-        iDestruct (excl_eq with "Hlsa Hlsf") as %->.
-        iDestruct (excl_eq with "Hrsa Hrsf") as %->.
-        iDestruct "HΦ" as "[HΦ _]".
-        iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_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. }
-        iIntros (_).
-        wp_pures.
-        by iApply "HΦ".
-      + iDestruct "Hrhd" as %[hd' [-> Hrhd']].
-        iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hlsf Hrsf]".
-        iDestruct (excl_eq with "Hlsa Hlsf") as %->.
-        iDestruct (excl_eq with "Hrsa Hrsf") as %->.
-        iDestruct (excl_update _ _ _ (rs) with "Hrsa Hrsf") as ">[Hrsa Hrsf]".
-        iDestruct "HΦ" as "[_ HΦ]".
-        iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_succ /chan_frag.
-          eauto 10 with iFrame. }
-        iModIntro.
-        wp_store.
-        wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
-        { rewrite /is_list_ref /is_list. eauto 10 with iFrame. }
-        iIntros (_).
-        wp_pures.
-        by iApply "HΦ".
-    - iDestruct "Hls" as (ll lhd ->) "[Hls #Hlhd]".
-      wp_pures.
-      wp_bind (Load _).
-      iMod "HΦ" as (ls' rs') "[Hchan HΦ]".
-      wp_load.
-      destruct ls; simpl.
-      + iDestruct "Hlhd" as %->.
-        iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hlsf Hrsf]".
-        iDestruct (excl_eq with "Hlsa Hlsf") as %->.
-        iDestruct (excl_eq with "Hrsa Hrsf") as %->.
-        iDestruct "HΦ" as "[HΦ _]".
-        iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_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. }
-        iIntros (_).
-        wp_pures.
-        by iApply "HΦ".
-      + iDestruct "Hlhd" as %[hd' [-> Hlhd']].
-        iDestruct "Hchan" as (l' r' lk' [= <- <- <-]) "[Hlsf Hrsf]".
-        iDestruct (excl_eq with "Hlsa Hlsf") as %->.
-        iDestruct (excl_eq with "Hrsa Hrsf") as %->.
-        iDestruct (excl_update _ _ _ (ls) with "Hlsa Hlsf") as ">[Hlsa Hlsf]".
-        iDestruct "HΦ" as "[_ HΦ]".
-        iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_succ /chan_frag. eauto 10 with iFrame. }
-        iModIntro.
-        wp_store.
-        wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
-        { rewrite /is_list_ref /is_list. eauto 10 with iFrame. }
-        iIntros (_).
-        wp_pures.
-        by iApply "HΦ".
+    wp_apply get_lock_spec; wp_pures.
+    wp_apply (acquire_spec with "Hlock"); iIntros "[Hlocked Hinv]". wp_pures.
+    wp_apply dual_side_spec. wp_apply get_side_spec; wp_pures.
+    iDestruct (chan_inv_alt (dual_side s) with "Hinv") as
+        (vs ws) "(Href & Hvs & Href' & Hws)".
+    iDestruct "Href" as (ll lhd Hslr) "(Hll & Hlvs)"; rewrite Hslr.
+    wp_bind (! _)%E.
+    iMod "HΦ" as (vs') "[Hchan HΦ]".
+    wp_load.
+    iDestruct (excl_eq with "Hvs Hchan") as %->.
+    destruct vs as [|v vs]; simpl.
+    - iDestruct "Hlvs" as %->.
+      iDestruct "HΦ" as "[HΦ _]".
+      iMod ("HΦ" with "[//] Hchan") as "HΦ".
+      iModIntro.
+      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
+      { iApply (chan_inv_alt (dual_side s)).
+        rewrite /is_list_ref. eauto 10 with iFrame. }
+      iIntros (_). wp_pures. by iApply "HΦ".
+    - iDestruct "Hlvs" as %(hd' & -> & Hhd').
+      iMod (excl_update _ _ _ vs with "Hvs Hchan") as "[Hvs Hchan]".
+      iDestruct "HΦ" as "[_ HΦ]".
+      iMod ("HΦ" with "[//] Hchan") as "HΦ".
+      iModIntro. wp_store.
+      wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
+      { iApply (chan_inv_alt (dual_side s)).
+        rewrite /is_list_ref. eauto 10 with iFrame. }
+      iIntros (_). wp_pures. by iApply "HΦ".
   Qed.
 
   Lemma recv_spec Φ E γ c s :
-    chan_ctx γ c -∗
-    (□ (|={⊤,E}=> ∃ ls rs,
-      chan_frag γ c ls rs ∗
-        ▷ ((try_recv_fail γ c ls rs s ={E,⊤}=∗ True) ∗
-          (∀ v, try_recv_succ γ c ls rs s v ={E,⊤}=∗ Φ v)))) -∗
+    is_chan γ c -∗
+    (□ (|={⊤,E}=> ∃ vs,
+      chan_own γ (dual_side s) vs ∗
+        ▷ ((⌜vs = []⌝ -∗ chan_own γ (dual_side s) vs ={E,⊤}=∗ True) ∗
+          (∀ v vs', ⌜vs = v :: vs'⌝ -∗
+                    chan_own γ (dual_side s) vs' ={E,⊤}=∗ Φ v)))) -∗
     WP recv c #s {{ Φ }}.
   Proof.
     iIntros "#Hc #HΦ".
     rewrite /recv.
     iLöb as "IH".
     wp_apply (try_recv_spec with "Hc")=> //.
-    iMod "HΦ" as (ls rs) "[Hchan [HΦfail HΦsucc]]".
+    iMod "HΦ" as (vs) "[Hchan [HΦfail HΦsucc]]".
     iModIntro.
-    iExists _, _.
+    iExists _.
     iFrame.
     iNext.
     iSplitL "HΦfail".
-    - iIntros "Hupd".
-      iDestruct ("HΦfail") as "HΦ".
-      iMod ("HΦ" with "Hupd") as "HΦ".
+    - iIntros "Hvs Hown".
+      iRename ("HΦfail") into "HΦ".
+      iDestruct ("HΦ" with "Hvs Hown") as "HΦ".
+      iMod ("HΦ") as "HΦ".
       iModIntro.
       wp_match.
       by iApply ("IH").
-    - iDestruct ("HΦsucc") as "HΦ".
-      iIntros (v) "Hupd".
-      iSpecialize("HΦ" $!v).
-      iMod ("HΦ" with "Hupd") as "HΦ".
+    - iRename ("HΦsucc") into "HΦ".
+      iIntros (v vs') "Hvs Hown".
+      iMod ("HΦ" with "Hvs Hown") as "HΦ".
       iModIntro.
       by wp_pures.
   Qed.
+
 End channel.
\ No newline at end of file

theories/logrel.v

@@ -18,21 +18,11 @@ Section logrel.
     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 st_own (γ : st_name) (s : side) (st : stype) : iProp Σ :=
+    own (side_elim s st_l_name st_r_name γ) (◯ 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.
+  Definition st_ctx (γ : st_name) (s : side) (st : stype) : iProp Σ :=
+    own (side_elim s st_l_name st_r_name γ) (● to_auth_excl st)%I.
 
   Fixpoint st_eval (vs : list val) (st1 st2 : stype) : Prop :=
     match vs with
@@ -70,33 +60,34 @@ Section logrel.
 
   Definition inv_st (γ :st_name) (c : val) : iProp Σ :=
     (∃ l r stl str,
-      chan_frag (st_c_name γ) c l r ∗
-      stmapsto_full γ stl Left  ∗
-      stmapsto_full γ str Right ∗
+      chan_own (st_c_name γ) Left l ∗
+      chan_own (st_c_name γ) Right r ∗
+      st_ctx γ Left stl  ∗
+      st_ctx γ Right str ∗
       ((⌜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 st_frag  (γ : st_name) (st : stype) (s : side) : iProp Σ :=
-    stmapsto_frag γ st s.
+  Definition is_st (γ : st_name) (st : stype) (c : val) : iProp Σ :=
+    (is_chan N (st_c_name γ) c ∗ inv N (inv_st γ c))%I.
 
   Definition interp_st (γ : st_name) (st : stype)
       (c : val) (s : side) : iProp Σ :=
-    (st_frag γ st s ∗ st_ctx γ st c)%I.
+    (st_own γ s st ∗ is_st γ 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}=∗
+    is_chan N cγ c ∗
+    chan_own cγ Left [] ∗
+    chan_own cγ Right []
+    ={E}=∗
       ∃ lγ rγ,
         let γ := SessionType_name cγ lγ rγ in
         ⟦ c @ Left : st ⟧{γ} ∗ ⟦ c @ Right : dual_stype st ⟧{γ}.
   Proof.
-    iIntros "[#Hcctx Hcf]".
+    iIntros "[#Hcctx [Hcol Hcor]]".
     iMod (own_alloc (● (to_auth_excl st) ⋅
                      ◯ (to_auth_excl st)))
       as (lγ) "[Hlsta Hlstf]"; first done.
@@ -108,8 +99,7 @@ Section logrel.
     { iNext. rewrite /inv_st. eauto 10 with iFrame. }
     iModIntro.
     iExists _, _.
-    iFrame. simpl.
-    repeat iSplitL=> //.
+    iFrame "Hlstf Hrstf Hcctx Hinv".
   Qed.
 
   Lemma new_chan_st_spec st :
@@ -127,35 +117,32 @@ Section logrel.
     { rewrite /is_chan. eauto with iFrame. }
     iDestruct "H" as (lγ rγ) "[Hl Hr]".
     iApply "HΦ".
-    iModIntro.
-    iFrame.
+    by iFrame.
   Qed.
 
-  Coercion side_to_side (s : side) : channel.side :=
-    match s with Left => channel.Left | Right => channel.Right end.
-
   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 ∗
+      ∃ vs, chan_own (st_c_name γ) s vs ∗
       ▷ (∀ v, ⌜P v⌝ -∗
-               chan_frag_snoc (st_c_name γ) c l r s v
-              ={E∖ ↑N,E}=∗ ⟦ c @ s : st v ⟧{γ}).
+               chan_own (st_c_name γ) s (vs ++ [v])
+               ={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')".
+    iDestruct "Hinv'" as
+        (l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')".
     iModIntro.
-    rewrite /stmapsto_frag /stmapsto_full.
-    iExists l, r.
-    iIntros "{$Hcf} !>" (v HP) "Hcf".
     destruct s.
-    - iRename "Hstf" into "Hstlf".
+    - iExists _.
+      iIntros "{$Hclf} !>" (v HP) "Hclf".
+      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.
+      {
+        iNext.
         iExists _,_,_,_. iFrame.
         iLeft.
         iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]";
@@ -172,11 +159,14 @@ Section logrel.
           split=> //.
       }
       iModIntro. iFrame "Hcctx ∗ Hinv".
-    - iRename "Hstf" into "Hstrf".
+    - iExists _.
+      iIntros "{$Hcrf} !>" (v HP) "Hcrf".
+      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.
+      {
+        iNext.
         iExists _,_, _, _. iFrame.
         iRight.
         iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]";
@@ -190,7 +180,8 @@ Section logrel.
           split=> //.
         - iSplit=> //.
           iPureIntro.
-          by eapply st_eval_send. }
+          by eapply st_eval_send.
+      }
       iModIntro. iFrame "Hcctx ∗ Hinv".
   Qed.
 
@@ -203,8 +194,8 @@ Section logrel.
     iIntros (HP Φ) "Hsend HΦ".
     iApply (send_spec with "[#]").
     { iDestruct "Hsend" as "[? [$ ?]]". }
-    iMod (send_vs with "Hsend") as (ls lr) "[Hch H]"; first done.
-    iModIntro. iExists ls, lr. iFrame "Hch".
+    iMod (send_vs with "Hsend") as (vs) "[Hch H]"; first done.
+    iModIntro. iExists vs. iFrame "Hch".
     iIntros "!> Hupd". iApply "HΦ".
     iApply ("H" $! v HP with "[Hupd]"). by destruct s.
   Qed.
@@ -213,33 +204,32 @@ Section logrel.
     ↑N ⊆ E →
     ⟦ c @ s : TRecv P st ⟧{γ}
     ={E,E∖↑N}=∗
-      ∃ l r, chan_frag (st_c_name γ) c l r ∗
-      (▷ ((try_recv_fail (st_c_name γ) c l r s ={E∖↑N,E}=∗
+      ∃ vs, chan_own (st_c_name γ) (dual_side s) vs ∗
+      (▷ ((⌜vs = []⌝ -∗ chan_own (st_c_name γ) (dual_side s) vs ={E∖↑N,E}=∗
            ⟦ c @ s : TRecv P st ⟧{γ}) ∧
-         (∀ v, try_recv_succ (st_c_name γ) c l r s v ={E∖↑N,E}=∗
+         (∀ v vs', ⌜vs = v :: vs'⌝ -∗
+               chan_own (st_c_name γ) (dual_side s) vs' ={E∖↑N,E}=∗
                ⟦ c @ s : (st v) ⟧{γ} ∗ ⌜P 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')".
+    iDestruct "Hinv'" as
+        (l r stl str) "(>Hclf & >Hcrf & Hstla & Hstra & Hinv')".
     iModIntro.
-    rewrite /stmapsto_frag /stmapsto_full.
-    iExists l, r.
-    iIntros "{$Hcf} !>".
     destruct s.
-    - iRename "Hstf" into "Hstlf".
+    - iExists _.
+      iIntros "{$Hcrf} !>".
+      iRename "Hstf" into "Hstlf".
+      rewrite /st_own /st_ctx. simpl.
       iDestruct (excl_eq with "Hstla Hstlf") as %<-.
       iSplit=> //.
-      + iIntros "[Hfail Hemp]".
+      + iIntros "Hvs Hown".
         iMod ("Hinvstep" with "[-Hstlf]") as "_".
         { iNext. iExists l,r,_,_. iFrame. }
         iModIntro. iFrame "Hcctx ∗ Hinv".
-      + simpl. iIntros (v) "Hsucc".
-        rewrite /try_recv_succ. simpl.
-        iDestruct "Hsucc" as (r') "[Hsucc Hr]".
-        iDestruct "Hr" as %Hr.
-        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; first inversion Hr.
+      + iIntros (v vs Hvs) "Hown".
+        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; first inversion Hvs.
         iMod (excl_update _ _ _ (st v) with "Hstla Hstlf") as "[Hstla Hstlf]".
         subst.
         iDestruct "Heval" as %Heval.
@@ -247,18 +237,17 @@ Section logrel.
         iMod ("Hinvstep" with "[-Hstlf]") as "_".
         { iExists _,_,_,_. iFrame. iRight=> //. }
         by iFrame (HP) "Hcctx Hinv".
-    - iRename "Hstf" into "Hstrf".
+    - iExists _.
+      iIntros "{$Hclf} !>".
+      iRename "Hstf" into "Hstrf".
       iDestruct (excl_eq with "Hstra Hstrf") as %<-.
       iSplit=> //.
-      + iIntros "[Hfail Hemp]".
+      + iIntros "Hvs Hown".
         iMod ("Hinvstep" with "[-Hstrf]") as "_".
         { iNext. iExists l,r,_,_. iFrame. }
         iModIntro. iFrame "Hcctx ∗ Hinv".
-      +  simpl. iIntros (v) "Hsucc".
-        rewrite /try_recv_succ. simpl.
-        iDestruct "Hsucc" as (r') "[Hsucc Hr]".
-        iDestruct "Hr" as %Hl.
-        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last inversion Hl.
+      +  simpl. iIntros (v vs' Hvs) "Hown".
+        iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]"; last inversion Hvs.
         iMod (excl_update _ _ _ (st v) with "Hstra Hstrf") as "[Hstra Hstrf]".
         subst.
         iDestruct "Heval" as %Heval.
@@ -277,19 +266,21 @@ Section logrel.
     iIntros (Φ) "Hrecv HΦ".
     iApply (try_recv_spec with "[#]").
     { iDestruct "Hrecv" as "[? [$ ?]]". }
-    iMod (try_recv_vs with "Hrecv") as (ls lr) "[Hch H]"; first done.
-    iModIntro. iExists ls, lr. iFrame "Hch".
+    iMod (try_recv_vs with "Hrecv") as (vs) "[Hch H]"; first done.
+    iModIntro. iExists vs. iFrame "Hch".
     iIntros "!>".
     iSplit.
-    - iIntros "Hupd".
+    - iIntros (Hvs) "Hown".
       iDestruct "H" as "[H _]".
-      iMod ("H" with "Hupd") as "H".
+      iSpecialize ("H" $!Hvs).
+      iMod ("H" with "Hown") as "H".
       iModIntro.
       iApply "HΦ"=> //.
       eauto with iFrame.
-    - iIntros (v) "Hupd".
+    - iIntros (v vs' Hvs) "Hown".
       iDestruct "H" as "[_ H]".
-      iMod ("H" with "Hupd") as "H".
+      iSpecialize ("H" $!v vs' Hvs).
+      iMod ("H" with "Hown") as "H".
       iModIntro.
       iApply "HΦ"=> //.
       eauto with iFrame.

theories/typing.v

 From iris.heap_lang Require Export lang.
 Require Import FunctionalExtensionality.
 
+
+Class Involutive {T} (f : T → T) :=
+  involutive : ∀ t : T, t = f (f t).
+
 Inductive side : Set :=
 | Left
 | Right.
 
+Instance side_inhabited : Inhabited side := populate Left.
+
+Definition dual_side (s : side) : side :=
+  match s with Left => Right | Right => Left end.
+
+Instance dual_side_involutive : Involutive dual_side.
+Proof. intros s; destruct s; eauto. Qed.
+
 Inductive stype :=
 | TEnd
 | TSend (P : val → Prop) (st : val → stype)
@@ -19,9 +31,6 @@ Fixpoint dual_stype (st :stype) :=
   | TRecv P st => TSend P (λ v, dual_stype (st v))
   end.
 
-Class Involutive {T} (f : T → T) :=
-  involutive : ∀ t : T, t = f (f t).
-
 Instance dual_stype_involutive : Involutive dual_stype.
 Proof.
   intros st.