finish the store_strong example

_CoqProject

@@ -24,3 +24,4 @@ theories/tests/fact.v
 theories/tests/array_copy.v
 theories/tests/gcd.v
 theories/tests/par_inc.v
+theories/tests/store_strong.v

theories/tests/store_strong.v

@@ -6,11 +6,11 @@ From iris.algebra Require Import frac_auth csum excl agree.
 Definition storeme : val := λᶜ "l",
   c_ret "l" =ᶜ ♯ 10 ;ᶜ ♯ 10.
 
-Definition lol : val := λᶜ "l",
+Definition test : val := λᶜ "l",
   callᶜ (c_ret storeme) (c_ret "l") +ᶜ (c_ret "l" =ᶜ ♯11).
 
-Section lol.
-  Context `{cmonadG Σ, !inG Σ (frac_authR natR)}.
+Section test.
+  Context `{cmonadG Σ, !inG Σ (authR (optionUR (exclR boolC)))}.
 
   Lemma cwp_store_hard R Φ Ψ1 Ψ2 e1 e2 :
     CWP e1 @ R {{ Ψ1 }} -∗
@@ -41,7 +41,7 @@ Section lol.
     iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
     wp_apply (linsert_spec with "[//]"); [eauto|]. iIntros (ll' Hl').
     iApply wp_fupd. wp_store.
-    iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
+     iMod ("Hclose" $! _ LLvl with "[//] Hl") as "[Hσ Hl]".
     iMod ("HΦ" with "Hl") as "[$ $]". iIntros "!> !>".
     iExists ({[(#(cloc_base cl), #(cloc_offset cl))%V]} ∪ X), _.
     iFrame "Hσ Hlocks". iPureIntro. rewrite locked_locs_lock. set_solver.
@@ -54,73 +54,91 @@ Section lol.
     iIntros "? H". iApply cwp_fun; simpl. vcg; iIntros "? !>". by iApply "H".
   Qed.
 
-  Definition oneshotR := csumR (exclR unitR) (agreeR natC).
-  Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
-  Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
-  Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
-  Proof. solve_inG. Qed.
-
-  Definition pending γ `{oneshotG Σ} := own γ (Cinl (Excl ())).
-  Definition shot γ n `{oneshotG Σ} := own γ (Cinr (to_agree n)).
-  Lemma new_pending `{oneshotG Σ} : (|==> ∃ γ, pending γ)%I.
-  Proof. by apply own_alloc. Qed.
-  Lemma shoot γ m `{oneshotG Σ} : pending γ ==∗ shot γ m.
+  Definition gpointsto γ (b : bool) := own γ (◯ (Excl' b)).
+  Notation "γ '≔' b" := (gpointsto γ b) (at level 80).
+  Definition gauth γ b := own γ (● (Excl' b)).
+  Lemma gagree γ b1 b2 :
+    γ ≔ b1 -∗ gauth γ b2 -∗ ⌜b1 = b2⌝.
   Proof.
-    apply own_update.
-    intros n [f |]; simpl; eauto.
-    destruct f; simpl; try by inversion 1.
+    iIntros "H1 H2".
+    by iDestruct (own_valid_2 with "H2 H1")
+      as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
   Qed.
-  Lemma shot_not_pending γ b `{oneshotG Σ} :
-    shot γ b -∗ pending γ -∗ False.
+  Lemma gnew : (|==> ∃ γ, gauth γ false ∗ γ ≔ false)%I.
   Proof.
-    iIntros "Hs Hp".
-    iPoseProof (own_valid_2 with "Hs Hp") as "H".
-    iDestruct "H" as %[].
+    iMod (own_alloc (● (Excl' false) ⋅ ◯ (Excl' false)))%I as (γ) "[H1 H2]";
+      first done;
+      eauto with iFrame.
   Qed.
-
-  Lemma shot_agree γ m n `{oneshotG Σ} :
-    shot γ m -∗ shot γ n -∗ ⌜m = n⌝.
+  Lemma gupdate b3 γ b1 b2 :
+    γ ≔ b1 -∗ gauth γ b2 ==∗ γ ≔ b3 ∗ gauth γ b3.
   Proof.
-    iIntros "Hs Hs'".
-    iPoseProof (own_valid_2 with "Hs Hs'") as "H".
-    rewrite Cinr_op /=.
-    by iDestruct "H" as %LOL%agree_op_invL'.
+    iIntros "H1 H2".
+    iMod (own_update_2 with "H2 H1") as "[? ?]".
+    { apply auth_update, option_local_update.
+      by apply (exclusive_local_update (Excl b2) (Excl b3)). }
+    by iFrame.
   Qed.
 
-  Lemma lol_spec R cl `{oneshotG Σ} :
+  Lemma test_spec R cl `{inG Σ testR, inG Σ fracR} :
     cl ↦C #0%nat -∗
-    CWP lol (cloc_to_val cl) @ R {{ v, ⌜ v = #21 ⌝ ∧
+    CWP "x" ←ᶜ test (cloc_to_val cl);ᶜ c_ret "x" @ R {{ v, ⌜ v = #21 ⌝ ∧
         (cl ↦C #10 ∨ cl ↦C #11) }}.
   Proof.
-    iIntros "Hl". iApply cwp_fun.
-    iMod (own_alloc (●! 0%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]"; [done|].
-    set (lol_inv := ((cl ↦C #0 ∗ own γ (●! 0%nat))
-                     ∨ (cl ↦C #10 ∗ own γ (●! 10%nat))
-                     ∨ (cl ↦C[LLvl] #11 ∗ own γ (●! 11%nat))
+    iIntros "Hl". iApply cwp_seq_bind. iApply cwp_fun. simpl.
+    iMod gnew as (γl) "[H1 lb]".
+    iMod gnew as (γr) "[H2 rb]".
+    set (test_inv := (∃ b1 b2, gauth γl b1 ∗ gauth γr b2 ∗
+                              match b1, b2 with
+                              | false, false => cl ↦C #0
+                              | true, false => cl ↦C #10
+                              | false, true => cl ↦C[LLvl] #11
+                              | _, _ => cl ↦C #10 ∨ cl ↦C[LLvl] #11
+                              end
                     )%I).
-    iApply (cwp_insert_res _ _ lol_inv with "[Hγ Hl]").
-    { iNext. iLeft. eauto with iFrame. }
-    simpl.
-    iApply (cwp_bin_op _ _ (λ v, ⌜v = #10⌝ ∗ own γ (◯!{1 / 2} 10%nat))%I
-                           (λ v, ⌜v = #11⌝ ∗ own γ (◯!{1 / 2} 11%nat))%I
-              with "[Hγ1] [Hγ2]").
-    - vcg. unfold lol_inv. iIntros "[H R]".
-      admit.
+    iApply (cwp_insert_res _ _ test_inv with "[H1 H2 Hl]").
+    { iNext. iExists false,false. iFrame. }
+    iApply (cwp_bin_op _ _ (λ v, ⌜v = #10⌝ ∗ γl ≔ true)%I
+                           (λ v, ⌜v = #11⌝ ∗ γr ≔ true)%I
+              with "[lb] [rb]").
+    - vcg. unfold test_inv. iIntros "[H R]".
+      iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
+      iDestruct (gagree with "lb H1") as %<-.
+      destruct b2; iNext; iModIntro.
+      + iMod (gupdate true with "lb H1") as "[lb H1]".
+        iApply (storeme_spec with "H").
+        iIntros "Hl". iFrame "R".
+        iSplitR "lb"; last by (vcg_continue; eauto with iFrame).
+        iExists _,_; eauto with iFrame.
+      + iMod (gupdate true with "lb H1") as "[lb H1]".
+        iApply (storeme_spec with "H").
+        iIntros "Hl". iFrame "R".
+        iSplitR "lb"; last by (vcg_continue; eauto with iFrame).
+        iExists _,_; eauto with iFrame.
     - iApply (cwp_store_hard _ _ (λ v, ⌜v = cloc_to_val cl⌝)%I
                                  (λ v, ⌜v = #11⌝)%I).
       1,2: vcg; eauto.
-      iIntros (? ? -> ->) "[H R]". unfold lol_inv.
-      iDestruct "H" as "[[Hcl H] | [[Hcl H] | [Hcl H]]]".
+      iIntros (? ? -> ->) "[H R]". unfold test_inv.
+      iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
+      iDestruct (gagree with "rb H2") as %<-.
+      destruct b1; iEval (simpl) in "H".
       + iExists cl, _. iFrame. iSplit; first done.
-        iIntros "Hl". iMod (own_update_2 with "H Hγ2") as "[H Hγ2]".
-        { apply frac_auth_update.
-          apply (nat_local_update _ _ 11%nat 11%nat); lia. }
-        iModIntro. iFrame "Hγ2". iSplit; last done.
-        iRight. iRight. iFrame.
+        iIntros "Hl".
+        iMod (gupdate true with "rb H2") as "[rb H2]".
+        iModIntro. iSplitR "rb"; last by eauto with iFrame.
+        iExists _,_; eauto with iFrame.
       + iExists cl, _. iFrame. iSplit; first done.
-        iIntros "Hl". iMod (own_update_2 with "H Hγ2") as "[H Hγ2]".
-        { apply frac_auth_update.
-          apply (nat_local_update _ _ 11%nat 1%nat). lia. }
-        iModIntro. Abort.
-End lol.
+        iIntros "Hl".
+        iMod (gupdate true with "rb H2") as "[rb H2]".
+        iModIntro. iSplitR "rb"; last by eauto with iFrame.
+        iExists _,_; eauto with iFrame.
+    - iIntros (v1 v2) "[% lb] [% rb]"; simplify_eq/=.
+      iExists #21; simpl. iSplit; first done.
+      iIntros "H". iDestruct "H" as (b1 b2) "(H1 & H2 & H)".
+      do 3 iModIntro.
+      iDestruct (gagree with "lb H1") as %<-.
+      iDestruct (gagree with "rb H2") as %<-.
+      iDestruct "H" as "[H|H]"; iModIntro; vcg; eauto with iFrame.
+  Qed.
+End test.