Improved CLH lock proof.

theories/examples/wip/logatom/atomic_clhlock.v

@@ -82,8 +82,9 @@ Section spec.
   Definition queued_loc γe l γ : iProp Σ := 
     own γ (to_agree l, 1%Qp) ∨ (∃ (b : bool), l ↦{#1/2} #b ∗ (⌜b = true⌝ ∨ (⌜b = false⌝ ∗ own γe (◯ (Excl' l)) ∗ own γ (to_agree l, 1/2)%Qp ∗ l ↦{#1/2} #b))).
 
-  Global Program Instance own_frac_or_as_forall l γ R : 
-    IntoForallCareful (own γ (to_agree l, 1%Qp) ∨ R)%I (λ (q : Qp), own γ (to_agree l, q) -∗ (own γ (to_agree l, q) ∗ R))%I.
+  Global Instance own_frac_or_as_forall l γ R : 
+    IntoForallCareful (own γ (to_agree l, 1%Qp) ∨ R)%I (λ (q : Qp), own γ (to_agree l, q) -∗ (R ∗ ◇ own γ (to_agree l, q)))%I.
+  Proof. rewrite /IntoForallCareful. by iStepsS. Qed.
 
   Definition is_queued_loc γe l' : iProp Σ :=
       ∃ γ, own γ (to_agree l', 1/2)%Qp ∗ inv N_node (queued_loc γe l' γ).
@@ -105,68 +106,11 @@ Section spec.
   Proof.
     iStepsS. iLeft.
     iStepS. iRight.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS.
-    iStepS. (* need to manually open invs, otherwise the AU will and can no longer be be opened. 
-               I think this could be fixed by instead using |={⊤,E}=> masks instead of |={⊤ ∖ E, ∅}=> masks.. *)
-    iMod (inv_acc with "H7") as "[HN HNcl]"; first done.
-    iMod "H5" as (p) "[[Hl >Hp] Hcl]".
-    iReIntro "HN".
-    - iStepS.
-      iStepS.
-      iStepS; first iStepS.
-      iStepS.
-      iStepS. iDestruct "Hcl" as "[Hcl _]".
-      iMod ("Hcl" with "[Hl Hp]") as "HAU"; first iFrame.
-      iMod ("HNcl" with "[H5]") as "_"; first iSmash.
-      iStepS.
-      iStepS.
-      iStepS.
-      iStepS.
-      iStepS.
-      iStepS.
-      iStepS.
-    - iStepS.
-      iStepS.
-      iStepS.
-      * iStepS.
-        iStepS. iDestruct "Hcl" as "[_ Hcl]".
-        iMod ("Hcl" with "[H6 Hp H9 H5 H1 H3 H4 Hl]") as "HAU"; first (iFrame; iStepsS).
-        iMod ("HNcl" with "[H10]") as "_"; first iSmash.
-        iStepS.
-        iStepS.
-        iStepS.
-        iStepS.
-      * iStepS.
-        iStepS. iDestruct "Hcl" as "[Hcl _]".
-        iMod ("Hcl" with "[Hl Hp]") as "HAU"; first iFrame.
-        iDestruct "H10" as "[H10 H10']".
-        iMod ("HNcl" with "[H10 H5 H9]") as "_"; first iSmash.
-        iStepS.
-        iStepS.
-        iStepS.
-        iStepS.
-        iStepS.
-        iStepS.
-        iStepS.
+    iStepsS; [iSmash| | iSmash].
+    iMod "H5" as (p) "[[Hl >Hp] [_ Hcl]]".
+    iReIntro "Hp". rewrite left_id.
+    iMod ("Hcl" with "[Hl H5 H6 H10 H11 H1 H3 H4]") as "HAU"; first (iFrame; iStepsS).
+    iSmash.
   Qed.
 
   Instance release_with_phys (l n : loc) γe p' :
@@ -203,15 +147,8 @@ Section spec.
   Definition locked_at (γe : gname) (p : loc) (v : val) : iProp Σ 
     := ∃ (n : loc), ⌜v = #n⌝ ∗ acquired_node γe n p.
 
-  Obligation Tactic := idtac.
   Global Program Instance clh_lock_atomic_lock : atomic_state_freezer.atomic_freezer Σ :=
     atomic_state_freezer.AtomicFreezer _ _ new_lock acquire release gname loc loc (⊤ ∖ ↑ N_node) (nroot.@ "free") (λ l, #l) lock_state locked_at _ _ _ _ _ _ _.
-  Next Obligation. verify_tac. Qed.
-  Next Obligation. verify_tac. Qed.
-  Next Obligation. verify_tac. Qed.
-  Next Obligation. smash_verify_tac. Qed.
-  Next Obligation. intros; iSmash. Qed.
-    (* fails because we don't DropModal ▷ on WPs *)
 End spec.
 
 

theories/symb_exec/weakestpre_logatom.v

-From iris.bi Require Export bi telescopes lib.atomic.
+From iris.bi Require Export bi telescopes lib.atomic updates.
 From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Import weakestpre lifting atomic.
 From iris_automation Require Import proofmode_base.
@@ -11,6 +11,32 @@ Import bi.
 Section atomic_template.
   Context `{BiFUpd PROP}.
 
+  (* some thoughts on the masks for atomic_update. The lemmas below show that the current requirement is stronger (so the specification weaker)
+     than the other option, |={⊤, M}=>. However, one is not necessarily better than the other - it depends on the syntactic order of opening
+     the implementation invariant and the supplied atomic update. For the current examples, I think Iris's default approach is fine: usually,
+     the implemantation invariant contains the resource that is syntactically required, and sometimes we need to open the atomic update to 
+     complete the proof. In this order, |={⊤ ∖ M, ∅}=> does exactly what we want.  *)
+  Lemma acc_1 (M : coPset) (P : PROP) : (|={⊤ ∖ M, ∅}=> P) ⊢ |={⊤, M}=> P.
+  Proof.
+    iIntros "HP".
+    iMod (fupd_mask_subseteq_emptyset_difference) as "HM"; last first.
+    iMod "HP". 2:{ set_solver. }
+    iMod "HM". replace (⊤ ∖ (⊤ ∖ M)) with M. by iFrame "HP".
+    apply set_eq => x; split; set_solver.
+  Qed.
+
+  Lemma acc_2 (M : coPset) (P Q : PROP) : (|={⊤ ∖ M, ∅}=> P ∗ |={∅, ⊤ ∖ M}=> Q) ⊢ |={⊤, M}=> P ∗ |={M, ⊤}=> Q.
+  Proof.
+    iIntros "HPQ".
+    iPoseProof (fupd_mask_intro_subseteq ⊤ (⊤ ∖ M) bi_emp) as "H"; first set_solver.
+    rewrite left_id.
+    iMod "H".
+    iMod "HPQ" as "[$ HQ]".
+    iMod "HQ" as "$".
+    iMod "H".
+    iApply fupd_mask_intro_subseteq. set_solver. done.
+  Qed.
+
   Definition atomic_templateM (M : coPset) (P1 : PROP) TT1 TT2 (P2 : TT1 -t> PROP) (Q1 Q2 : TT1 -t> TT2 -t> PROP) : (TT1 * TT2 → PROP) → PROP
     := (λ Ψ, |={⊤}=> P1 ∗ atomic_update (⊤∖ M) ∅ (tele_app P2) (tele_app (tele_map tele_app Q2)) (λ a b, tele_app (tele_app Q1 a) b -∗ Ψ (a, b)))%I.