From f8b4a43a0df554b5e580674a75070a66bad770c9 Mon Sep 17 00:00:00 2001
From: Hei Li <hei411@gmail.com>
Date: Mon, 21 Oct 2024 12:41:42 +0200
Subject: [PATCH] using cancellable invariants for message pass

---
 theories/coneris/examples/message_pass.v | 44 ++++++++++++++----------
 1 file changed, 26 insertions(+), 18 deletions(-)

diff --git a/theories/coneris/examples/message_pass.v b/theories/coneris/examples/message_pass.v
index 8ddcd124..d6e6e485 100644
--- a/theories/coneris/examples/message_pass.v
+++ b/theories/coneris/examples/message_pass.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import excl_auth.
-From iris.base_logic.lib Require Export invariants.
+From iris.base_logic.lib Require Export invariants cancelable_invariants.
 From clutch.coneris Require Import coneris par spawn lib.flip.
 
 Local Open Scope Z.
@@ -15,15 +15,15 @@ Definition prog (l:loc) : expr:=
                                         else "y"
                                      )%V !(#l))
                                      
-  );; !#l.
+  ).
 
 Section proof.
-  Context `{!conerisGS Σ, !spawnG Σ, inG Σ (excl_authR boolO)}.
+  Context `{!conerisGS Σ, !spawnG Σ, inG Σ (excl_authR boolO), cinvG Σ}.
   Lemma prog_spec l:
     {{{ ↯(/2)%R ∗ ∃ v, l↦v }}}
       prog l
       {{{
-            RET #0; True
+            v, RET v; l↦#0
       }}}.
   Proof.
     iIntros (Φ) "[Herr [%v Hl]] HΦ".
@@ -31,36 +31,44 @@ Section proof.
     wp_store.
     iMod (own_alloc (●E false ⋅ ◯E false)) as (γ) "[Hauth Hfrag]".
     { by apply excl_auth_valid. }
-    iMod (inv_alloc nroot _ (l↦#0 ∗ own γ (●E true) ∨ l↦ #(-1) ∗ own γ (●E false))%I with "[Hl Hauth]") as "#I"; first (iRight; iFrame).
+    iMod (cinv_alloc _ nroot (l↦#0 ∗ own γ (●E true) ∨ l↦ #(-1) ∗ own γ (●E false))%I with "[Hl Hauth]") as "[%γ1 [#I Hc]]"; first (iRight; iFrame).
     wp_pures.
-    wp_apply (wp_par (λ _, own γ (◯E true))%I (λ _, True)%I with "[Herr Hfrag][]").
+    iDestruct "Hc" as "[Hc Hc']".
+    iApply pgl_wp_fupd.
+    wp_apply (wp_par (λ _, own γ (◯E true) ∗ cinv_own γ1 (1/2)%Qp)%I (λ _, cinv_own γ1 (1/2)%Qp)%I with "[Herr Hfrag Hc][Hc']").
     - wp_apply (wp_flip_adv _ _ (λ x, if x then 0 else 1)%R with "[$]").
       + intros []; lra.
       + lra.
       + iIntros ([]) "Herr"; last by iDestruct (ec_contradict with "[$]") as "%".
         wp_pures.
-        iInv "I" as ">[[H Hauth]|[H Hauth]]" "Hclose".
+        iMod (cinv_acc_strong with "[I] [$]") as "K"; [done|done|..].
+        iDestruct "K" as "[>[[H Hauth]|[H Hauth]] [Hc Hclose]]".
         * iCombine "Hauth Hfrag" gives "%K". by apply excl_auth_agree_L in K.
         * wp_store.
           iMod (own_update_2 _ _ _ (●E true ⋅ ◯E true) with "Hauth Hfrag") as "[Hauth Hfrag]".
           { by apply excl_auth_update. }
-          iMod ("Hclose" with "[H Hauth]"); first (iLeft; iFrame). iModIntro. iFrame. 
+          iMod ("Hclose" with "[H Hauth]"); first (iLeft; iLeft; iFrame).
+          iFrame.
+          by rewrite -union_difference_L.
     - iLöb as "IH".
       wp_bind (!_)%E.
-      iInv "I" as ">[[??]|[??]]" "Hclose".
+      iMod (cinv_acc_strong with "[I] [$]") as "K"; [done|done|..].
+      iDestruct "K" as "[>[[H Hauth]|[H Hauth]] [Hc Hclose]]".
       + wp_load.
-        iMod ("Hclose" with "[-]"); first (iLeft; iFrame).
+        iMod ("Hclose" with "[-Hc]"); first (iLeft; iLeft; iFrame).
+        rewrite -union_difference_L; last done.
         iModIntro.
         by wp_pures.
       + wp_load.
-        iMod ("Hclose" with "[-]"); first (iRight; iFrame).
-        iModIntro. wp_pures. iApply "IH".
-    - iIntros (??) "[Hfrag _]".
-      iNext. wp_pures.
-      iInv "I" as ">[[H Hauth]|[H Hauth]]" "Hclose".
-      + wp_load.
-        iMod ("Hclose" with "[H Hauth]"); first (iLeft; iFrame). iModIntro.
-        by iApply "HΦ".
+        iMod ("Hclose" with "[-Hc]"); first (iLeft; iRight; iFrame).
+        rewrite -union_difference_L; last done.
+        iModIntro. wp_pures. by iApply "IH".
+    - iIntros (??) "[[Hfrag Hc] Hc']".
+      iCombine "Hc Hc'" as "Hc".
+      iNext.
+      iMod (cinv_cancel with "[][$]") as "H"; [done|done|].
+      iDestruct "H" as ">[[H Hauth]|[H Hauth]]".
+      + iModIntro. by iApply "HΦ".
       + iCombine "Hauth Hfrag" gives "%K". by apply excl_auth_agree_L in K.
   Qed.