Added close definition and spec

Added a definition and specification for "closing" channels. The idea is that a channel endpoint, once it reaches END can guarantee that its inbound buffer (i.e. vsr for Left, and vsl for Right) is empty, and is no longer used by either party. As such, it can Free the buffer (using the primitive Free instruction) to deallocate the memory. In doing so, it gives up its endpoint ownership c >-> END.

This is achieved by changing the channel invariant to either hold the buffers, or the terminated channel endpoint:

Definition iProto_mapsto_def `{!heapGS Σ, !chanG Σ}
    (c : val) (p : iProto Σ) : iProp Σ :=
  ∃ γ s (l r : loc) (lk : val),
    ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
    is_lock (chan_lock_name γ) lk (∃ vsl vsr,
      (llist internal_eq l vsl ∨ iProto_own (chan_proto_name γ) Right END%proto) ∗
      (llist internal_eq r vsr ∨ iProto_own (chan_proto_name γ) Left END%proto) ∗
      steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
      iProto_ctx (chan_proto_name γ) vsl vsr) ∗
    iProto_own (chan_proto_name γ) s p.

The proof relies on three observations:

• We can always receive (e.g. on vsr for Left), as we can derive a contradiction between our local endpoint ownership, and the one in the invariant. (new lemma iProto_own_exclusive)
• We can always send (e.g. on vsl for Left), as we can derive that whenever one protocol is sending (i.e. (<! xs> MSG v {{ P }} ; p), then the other protocol has not terminated (i.e. it is not END), and so it cannot be in the invariant. (new lemmas iProto_interp_send_end_inv_{l,r})
• When our endpoint is END, the inbound buffer is always empty, and so we can close it without worrying about leftover resources (new lemmas iProto_interp_end_inv_{l,r}).

EDIT: Closed the outstanding lemmas

theories/channel/channel.v

@@ -64,6 +64,13 @@ Definition recv : val :=
     | NONE => "go" "c"
     end.
 
+Definition close : val :=
+  λ: "c",
+    let: "lk" := Snd "c" in
+    let: "l" := Fst (Fst "c") in
+    let: "r" := Snd (Fst "c") in
+    acquire "lk";; lfree "r";; release "lk".
+
 (** * Setup of Iris's cameras *)
 Class chanG Σ := {
   chanG_lockG :> lockG Σ;
@@ -96,8 +103,8 @@ Definition iProto_mapsto_def `{!heapGS Σ, !chanG Σ}
   ∃ γ s (l r : loc) (lk : val),
     ⌜ c = ((#(side_elim s l r), #(side_elim s r l)), lk)%V ⌝ ∗
     is_lock (chan_lock_name γ) lk (∃ vsl vsr,
-      llist internal_eq l vsl ∗
-      llist internal_eq r vsr ∗
+      (llist internal_eq l vsl ∨ iProto_own (chan_proto_name γ) Right END) ∗
+      (llist internal_eq r vsr ∨ iProto_own (chan_proto_name γ) Left END) ∗
       steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
       iProto_ctx (chan_proto_name γ) vsl vsr) ∗
     iProto_own (chan_proto_name γ) s p.
@@ -211,7 +218,8 @@ Section channel.
     wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (r) "Hr".
     iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
     wp_smart_apply (newlock_spec (∃ vsl vsr,
-      llist internal_eq l vsl ∗ llist internal_eq r vsr ∗
+      (llist internal_eq l vsl ∨ iProto_own γp Right END) ∗
+      (llist internal_eq r vsr ∨ iProto_own γp Left END) ∗
       steps_lb (length vsl) ∗ steps_lb (length vsr) ∗
       iProto_ctx γp vsl vsr) with "[Hl Hr Hctx]").
     { iExists [], []. iFrame "#∗". }
@@ -243,7 +251,16 @@ Section channel.
     wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
     iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
     destruct s; simpl.
-    - wp_pures. wp_bind (lsnoc _ _).
+    - iDestruct "Hl" as "[Hl | Hl]"; last first.
+      { iDestruct (iProto_send_end_inv_l with "Hctx H Hl") as "#HF".
+        wp_bind (Rec _ _ _).
+        iApply (wp_step_fupdN_lb with "Hlbr [Hctx H]"); [done| |].
+        { iApply fupd_mask_intro; [set_solver|]. simpl.
+          iIntros "Hclose !> !> !>".
+          iApply step_fupdN_intro; [done|]. iNext.
+          iMod "Hclose". iModIntro. iExact "HF". }
+        wp_pures. iIntros "!>[]". }
+      wp_pures. wp_bind (lsnoc _ _).
       iApply (wp_step_fupdN_lb with "Hlbr [Hctx H]"); [done| |].
       { iApply fupd_mask_intro; [set_solver|]. simpl.
         iIntros "Hclose !>!>".
@@ -263,7 +280,16 @@ Section channel.
         replace (length vsl + 1) with (S (length vsl)) by lia.
         iFrame "#∗". }
       iIntros "_". iApply "HΦ". iExists γ, Left, l, r, lk. eauto 10 with iFrame.
-    - wp_pures. wp_bind (lsnoc _ _).
+    - iDestruct "Hr" as "[Hr | Hr]"; last first.
+      { iDestruct (iProto_send_end_inv_r with "Hctx Hr H") as "#HF".
+        wp_bind (Rec _ _ _).
+        iApply (wp_step_fupdN_lb with "Hlbl [Hctx H]"); [done| |].
+        { iApply fupd_mask_intro; [set_solver|]. simpl.
+          iIntros "Hclose !> !> !>".
+          iApply step_fupdN_intro; [done|]. iNext.
+          iMod "Hclose". iModIntro. iExact "HF". }
+        wp_pures. iIntros "!>[]". }
+      wp_pures. wp_bind (lsnoc _ _).
       iApply (wp_step_fupdN_lb with "Hlbl [Hctx H]"); [done| |].
       { iApply fupd_mask_intro; [set_solver|]. simpl.
         iIntros "Hclose !>!>".
@@ -310,8 +336,11 @@ Section channel.
     rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
     iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
     wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
-    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)". destruct s; simpl.
-    - wp_smart_apply (lisnil_spec with "Hr"); iIntros "Hr".
+    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
+    destruct s; simpl.
+    - iDestruct "Hr" as "[Hr | Hr]"; last first.
+      { iDestruct (iProto_own_exclusive with "H Hr") as "[]". }
+      wp_smart_apply (lisnil_spec with "Hr"); iIntros "Hr".
       destruct vsr as [|vr vsr]; wp_pures.
       { wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
         iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
@@ -325,7 +354,9 @@ Section channel.
       iIntros "_". wp_pures. iModIntro. iApply "HΦ". iRight. iExists x. iSplit; [done|].
       iFrame "HP". iExists γ, Left, l, r, lk. iSplit; [done|]. iFrame "Hlk".
       by iRewrite "Hp".
-    - wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
+    - iDestruct "Hl" as "[Hl | Hl]"; last first.
+      { iDestruct (iProto_own_exclusive with "H Hl") as "[]". }
+      wp_smart_apply (lisnil_spec with "Hl"); iIntros "Hl".
       destruct vsl as [|vl vsl]; wp_pures.
       { wp_smart_apply (release_spec with "[Hl Hr Hctx $Hlk $Hlkd]"); [by eauto with iFrame|].
         iIntros "_". wp_pures. iModIntro. iApply "HΦ". iLeft. iSplit; [done|].
@@ -352,6 +383,36 @@ Section channel.
     iDestruct "H" as (x ->) "[Hc HP]". wp_pures. iApply "HΦ". by iFrame.
   Qed.
 
+  Lemma close_spec c :
+    {{{ c ↣ END%proto }}}
+      close c
+    {{{ RET #(); True }}}.
+  Proof.
+    rewrite iProto_mapsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
+    iDestruct "Hc" as (γ s l r lk ->) "[#Hlk H]"; wp_pures.
+    wp_smart_apply (acquire_spec with "Hlk"); iIntros "[Hlkd Hinv]".
+    iDestruct "Hinv" as (vsl vsr) "(Hl & Hr & #Hlbl & #Hlbr & Hctx)".
+    destruct s; simpl.
+    - iDestruct "Hr" as "[Hr | Hr]"; last first.
+      { iDestruct (iProto_own_exclusive with "H Hr") as "[]". }
+      iDestruct (iProto_end_inv_l with "Hctx H") as "#Heq".
+      wp_pures. iDestruct "Heq" as %->.
+      wp_smart_apply (lfree_spec with "Hr").
+      iIntros "_".
+      wp_smart_apply (release_spec with "[Hl H Hctx $Hlk $Hlkd]").
+      { eauto with iFrame. }
+      done.
+    - iDestruct "Hl" as "[Hl | Hl]"; last first.
+      { iDestruct (iProto_own_exclusive with "H Hl") as "[]". }
+      iDestruct (iProto_end_inv_r with "Hctx H") as "#Heq".
+      wp_pures. iDestruct "Heq" as %->.
+      wp_smart_apply (lfree_spec with "Hl").
+      iIntros "_".
+      wp_smart_apply (release_spec with "[Hr H Hctx $Hlk $Hlkd]").
+      { eauto with iFrame. }
+      done.
+  Qed.
+
   (** ** Specifications for choice *)
   Lemma select_spec c (b : bool) P1 P2 p1 p2 :
     {{{ c ↣ (p1 <{P1}+{P2}> p2) ∗ if b then P1 else P2 }}}