WIP: bump of regular MP channel specs. Still need subprotocols

multris/channel/channel.v

@@ -91,14 +91,13 @@ Definition chan_inv `{!heapGS Σ, !chanG Σ} γ γE γt i j (l:loc) : iProp Σ :
 
 Definition iProto_pointsto_def `{!heapGS Σ, !chanG Σ}
     (c : val) (p : iProto Σ) : iProp Σ :=
-  ∃ γ (γEs : list gname) (m:val) (i:nat) (n:nat) p',
+  ∃ γ (γEs : list gname) (m:val) (i:nat) (n:nat),
     ⌜ c = (m,#i)%V ⌝ ∗
     inv (nroot.@"ctx") (iProto_ctx γ n) ∗
     is_matrix m n n
       (λ i j l, ∃ γt, inv (nroot.@"p") (chan_inv γ (γEs !!! i) γt i j l)) ∗
-    ▷ (p' ⊑ p) ∗
-    own (γEs !!! i) (●E (Next p')) ∗ own (γEs !!! i) (◯E (Next p')) ∗
-    iProto_own γ i p'.
+    own (γEs !!! i) (●E (Next p)) ∗ own (γEs !!! i) (◯E (Next p)) ∗
+    iProto_own γ i p.
 Definition iProto_pointsto_aux : seal (@iProto_pointsto_def). by eexists. Qed.
 Definition iProto_pointsto := iProto_pointsto_aux.(unseal).
 Definition iProto_pointsto_eq :
@@ -130,15 +129,6 @@ Section channel.
   Global Instance iProto_pointsto_proper c : Proper ((≡) ==> (≡)) (iProto_pointsto c).
   Proof. apply (ne_proper _). Qed.
 
-  Lemma iProto_pointsto_le c p1 p2 : c ↣ p1 ⊢ ▷ (p1 ⊑ p2) -∗ c ↣ p2.
-  Proof.
-    rewrite iProto_pointsto_eq.
-    iDestruct 1 as (?????? ->) "(#IH & Hls & Hle & H● & H◯ & Hown)".
-    iIntros "Hle'". iExists _,_,_,_,_,p'.
-    iSplit; [done|]. iFrame "#∗".
-    iApply (iProto_le_trans with "Hle Hle'").
-  Qed.
-
   (** ** Specifications of [send] and [recv] *)
   Lemma new_chan_spec (ps:list (iProto Σ)) :
     0 < length ps →
@@ -206,9 +196,9 @@ Section channel.
     iModIntro.
     iApply "HΦ".
     iSplitL "Hl".
-    { rewrite iProto_pointsto_eq. iExists _, _, _, _, _, _.
+    { rewrite iProto_pointsto_eq. iExists _, _, _, _, _.
       iSplit; [done|].
-      iFrame. iFrame "#∗". iNext. done. }
+      iFrame. iFrame "#∗". }
     iExists γp, γEs, _. iSplit; [done|].
     iFrame. iFrame "#∗".
     simpl.
@@ -227,14 +217,12 @@ Section channel.
   Proof.
     rewrite iProto_pointsto_eq. iIntros (Φ) "Hc HΦ". wp_lam; wp_pures.
     iDestruct "Hc" as
-      (γ γE l i n p' ->) "(#IH & #Hls & Hle & H● & H◯ & Hown)".
+      (γ γE l i n ->) "(#IH & #Hls & H● & H◯ & Hown)".
     wp_bind (Fst _).
     iInv "IH" as "Hctx".
-    iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
-    iRewrite "Heq" in "Hown".
     iDestruct (iProto_ctx_agree with "Hctx [Hown//]") as "#Hi".
     iDestruct (iProto_target with "Hctx [Hown//]") as "#Hj".
-    iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
+    wp_pures. iModIntro. iFrame.
     wp_pures.
     iDestruct "Hi" as %Hi.
     iDestruct "Hj" as %Hj.
@@ -255,10 +243,8 @@ Section channel.
     wp_store.
     iMod (own_update_2 with "H● H◯") as "[H● H◯]"; [by apply excl_auth_update|].
     iModIntro.
-    iSplitL "Hl' H● Hown Hle".
-    { iRight. iLeft. iIntros "!>". iExists _, _. iFrame.
-      iDestruct (iProto_own_le with "Hown Hle") as "Hown".
-      by rewrite iMsg_base_eq. }
+    iSplitL "Hl' H● Hown".
+    { iRight. iLeft. iIntros "!>". iExists _, _. iFrame. }
     wp_pures.
     iLöb as "HL".
     wp_lam.
@@ -285,24 +271,17 @@ Section channel.
       { apply excl_auth_update. }
       iModIntro.
       iApply "HΦ".
-      iExists _, _, _, _, _, _.
+      iExists _, _, _, _, _.
       iSplit; [done|]. iFrame "#∗".
-      iRewrite -"Hagree'". iApply iProto_le_refl.
+      iRewrite -"Hagree'". done.
   Qed.
 
-  Lemma send_spec_tele {TT} c i (tt : TT)
+  Lemma send_spec_tele {TT} c j (tt : TT)
         (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
-    {{{ c ↣ (<(Send,i) @.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
-      send c #i (v tt)
+    {{{ c ↣ (<(Send,j) @.. x > MSG v x {{ P x }}; p x) ∗ P tt }}}
+      send c #j (v tt)
     {{{ RET #(); c ↣ (p tt) }}}.
-  Proof.
-    iIntros (Φ) "[Hc HP] HΦ".
-    iDestruct (iProto_pointsto_le _ _ (<(Send,i)> MSG v tt; p tt)%proto
-                with "Hc [HP]") as "Hc".
-    { iIntros "!>". iApply iProto_le_trans. iApply iProto_le_texist_intro_l.
-      by iApply iProto_le_payload_intro_l. }
-    by iApply (send_spec with "Hc").
-  Qed.
+  Proof. Admitted.
 
   Lemma recv_spec {TT} c j (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
     {{{ c ↣ <(Recv, j) @.. x> MSG v x {{ ▷ P x }}; p x }}}
@@ -312,15 +291,13 @@ Section channel.
     iIntros (Φ) "Hc HΦ". iLöb as "HL". wp_lam.
     rewrite iProto_pointsto_eq.
     iDestruct "Hc" as
-      (γ γE l i n p' ->) "(#IH & #Hls & Hle & H● & H◯ & Hown)".
+      (γ γE l i n ->) "(#IH & #Hls & H● & H◯ & Hown)".
     do 5 wp_pure _.
     wp_bind (Snd _).
     iInv "IH" as "Hctx".
-    iDestruct (iProto_le_msg_inv_r with "Hle") as (m') "#Heq".
-    iRewrite "Heq" in "Hown".
     iDestruct (iProto_ctx_agree with "Hctx [Hown//]") as "#Hi".
     iDestruct (iProto_target with "Hctx [Hown//]") as "#Hj".
-    iRewrite -"Heq" in "Hown". wp_pures. iModIntro. iFrame.
+    wp_pures. iModIntro. iFrame.
     wp_pure _.
     iDestruct "Hi" as %Hi.
     iDestruct "Hj" as %Hj.
@@ -335,20 +312,19 @@ Section channel.
       wp_xchg. iModIntro.
       iSplitL "Hl' Htok".
       { iLeft. iFrame. }
-      wp_pures. iApply ("HL" with "[H● H◯ Hown Hle] HΦ").
-      iExists _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
+      wp_pures. iApply ("HL" with "[H● H◯ Hown] HΦ").
+      iExists _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
     iDestruct "HIp" as "[HIp|HIp]"; last first.
     { iDestruct "HIp" as (p'') "[>Hl' [Hown' H◯']]".
       wp_xchg.
       iModIntro.
       iSplitL "Hl' Hown' H◯'".
       { iRight. iRight. iExists _. iFrame. }
-      wp_pures. iApply ("HL" with "[H● H◯ Hown Hle] HΦ").
-      iExists _, _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
+      wp_pures. iApply ("HL" with "[H● H◯ Hown] HΦ").
+      iExists _, _, _, _, _. iSplit; [done|]. iFrame "#∗". }
     iDestruct "HIp" as (w p'') "(>Hl' & Hown' & Hp')".
     iInv "IH" as "Hctx".
     wp_xchg.
-    iDestruct (iProto_own_le with "Hown Hle") as "Hown".
     iMod (iProto_step with "Hctx Hown' Hown []") as
       (p''') "(Hm & Hctx & Hown & Hown')".
     { by rewrite iMsg_base_eq. }
@@ -364,7 +340,7 @@ Section channel.
     iMod (own_update_2 with "H● H◯") as "[H● H◯]";
       [apply (excl_auth_update _ _ (Next p'''))|].
     iModIntro. iApply "HΦ". rewrite /iProto_pointsto_def. iFrame "IH Hls ∗".
-    iSplit; [done|]. iRewrite "Hp". iApply iProto_le_refl.
+    iExists _. iSplit; [done|]. iRewrite "Hp". iFrame.
   Qed.
 
 End channel.