prove lemmas to compose atomic steps

theories/bi/lib/atomic.v

@@ -24,16 +24,16 @@ Section definition.
           ((α x ={Ei, Eo}=∗ P) ∧ (∀ y, β x y ={Ei, Eo}=∗ Φ x y))
     )%I.
 
-  Lemma atomic_step_mono Eo Ei α P1 P2 β Φ :
-    □ (P1 -∗ P2) -∗
-    □ (atomic_step Eo Ei α P1 β Φ -∗ atomic_step Eo Ei α P2 β Φ).
+  Lemma atomic_step_wand Eo Ei α P1 P2 β Φ1 Φ2 :
+    ((P1 -∗ P2) ∧ (∀ x y, Φ1 x y -∗ Φ2 x y)) -∗
+    (atomic_step Eo Ei α P1 β Φ1 -∗ atomic_step Eo Ei α P2 β Φ2).
   Proof.
-    iIntros "#HP12 !# AS". iMod "AS" as (x) "[Hα Hclose]".
+    iIntros "HP12 AS". iMod "AS" as (x) "[Hα Hclose]".
     iModIntro. iExists x. iFrame "Hα". iSplit.
     - iIntros "Hα". iDestruct "Hclose" as "[Hclose _]".
       iApply "HP12". iApply "Hclose". done.
     - iIntros (y) "Hβ". iDestruct "Hclose" as "[_ Hclose]".
-      iApply "Hclose". done.
+      iApply "HP12". iApply "Hclose". done.
   Qed.
 
   Lemma atomic_step_mask Eo Em α P β Φ :
@@ -64,8 +64,8 @@ Section definition.
     constructor.
     - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
       iDestruct "AU" as (P) "[HP #AS]". iExists P. iFrame.
-      iIntros "!# HP". iApply (atomic_step_mono with "HP12").
-      iApply "AS"; done.
+      iIntros "!# HP". iApply (atomic_step_wand with "[HP12]"); last by iApply "AS".
+      iSplit; last by eauto. iApply "HP12".
     - intros ??. solve_proper.
   Qed.
 
@@ -143,7 +143,7 @@ Section lemmas.
     iApply HAU. by iFrame.
   Qed.
 
-  Lemma astep_intro Eo Ei α P β Φ x :
+  Lemma astep_intro x Eo Ei α P β Φ :
     Ei ⊆ Eo → α x -∗
     ((α x ={Eo}=∗ P) ∧ (∀ y, β x y ={Eo}=∗ Φ x y)) -∗
     atomic_step Eo Ei α P β Φ.
@@ -179,6 +179,79 @@ Section lemmas.
       iModIntro. destruct (γ' x'); iApply "HΦ"; done.
   Qed.
 
+  Lemma astep_astep {A' B'} E1 E2 E3
+        α P β Φ
+        (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
+    atomic_step E1 E2 α P β Φ -∗
+    (∀ x, α x -∗ atomic_step E2 E3 α' (α x ∗ (P ={E1}=∗ P')) β'
+            (λ x' y', (α x ∗ (P ={E1}=∗ Φ' x' y'))
+                    ∨ ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
+    atomic_step E1 E3 α' P' β' Φ'.
+  Proof.
+    iIntros "Hupd Hstep". iMod ("Hupd") as (x) "[Hα Hclose]".
+    iMod ("Hstep" with "Hα") as (x') "[Hα' Hclose']".
+    iModIntro. iExists x'. iFrame "Hα'". iSplit.
+    - iIntros "Hα'". iDestruct "Hclose'" as "[Hclose' _]".
+      iMod ("Hclose'" with "Hα'") as "[Hα Hupd]".
+      iDestruct "Hclose" as "[Hclose _]".
+      iMod ("Hclose" with "Hα"). iApply "Hupd". auto.
+    - iIntros (y') "Hβ'". iDestruct "Hclose'" as "[_ Hclose']".
+      iMod ("Hclose'" with "Hβ'") as "[[Hα HΦ']|Hcont]".
+      + (* Abort the step we are eliminating *)
+        iDestruct "Hclose" as "[Hclose _]".
+        iMod ("Hclose" with "Hα") as "HP".
+        iApply "HΦ'". done.
+      + (* Complete the step we are eliminating *)
+        iDestruct "Hclose" as "[_ Hclose]".
+        iDestruct "Hcont" as (y) "[Hβ HΦ']".
+        iMod ("Hclose" with "Hβ") as "HΦ".
+        iApply "HΦ'". done.
+  Qed.
+
+  Lemma astep_aupd {A' B'} E1 E2 Eo Em
+        α β Φ
+        (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
+    Eo ⊆ E1 →
+    atomic_update Eo Em α β Φ -∗
+    (∀ x, α x -∗ atomic_step (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β'
+            (λ x' y', (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ Φ' x' y'))
+                    ∨ ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
+    atomic_step E1 E2 α' P' β' Φ'.
+  Proof.
+    iIntros (?) "Hupd Hstep". iApply (astep_astep with "[Hupd] Hstep").
+    iApply aupd_acc; done.
+  Qed.
+
+  Lemma astep_aupd_commit {A' B'} E1 E2 Eo Em
+        α β Φ
+        (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
+    Eo ⊆ E1 →
+    atomic_update Eo Em α β Φ -∗
+    (∀ x, α x -∗ atomic_step (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β'
+            (λ x' y', ∃ y, β x y ∗ (Φ x y ={E1}=∗ Φ' x' y'))) -∗
+    atomic_step E1 E2 α' P' β' Φ'.
+  Proof.
+    iIntros (?) "Hupd Hstep". iApply (astep_aupd with "Hupd"); first done.
+    iIntros (x) "Hα". iApply atomic_step_wand; last first.
+    { iApply "Hstep". done. }
+    iSplit; first by eauto. iIntros (??) "?". by iRight.
+  Qed.
+
+  Lemma astep_aupd_abort {A' B'} E1 E2 Eo Em
+        α β Φ
+        (α' : A' → PROP) P' (β' Φ' : A' → B' → PROP) :
+    Eo ⊆ E1 →
+    atomic_update Eo Em α β Φ -∗
+    (∀ x, α x -∗ atomic_step (E1∖Em) E2 α' (α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ P')) β'
+            (λ x' y', α x ∗ (atomic_update Eo Em α β Φ ={E1}=∗ Φ' x' y'))) -∗
+    atomic_step E1 E2 α' P' β' Φ'.
+  Proof.
+    iIntros (?) "Hupd Hstep". iApply (astep_aupd with "Hupd"); first done.
+    iIntros (x) "Hα". iApply atomic_step_wand; last first.
+    { iApply "Hstep". done. }
+    iSplit; first by eauto. iIntros (??) "?". by iLeft.
+  Qed.
+
 End lemmas.
 
 (** ProofMode support for atomic updates *)

theories/heap_lang/lib/increment.v

@@ -29,24 +29,24 @@ Section increment.
     iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let.
     wp_apply (load_spec with "[HQ]"); first by iAccu.
     (* Prove the atomic shift for load *)
-    iAuIntro.
-    iMod (aupd_acc with "AU") as (x) "[H↦ [Hclose _]]"; first solve_ndisj.
-    iModIntro. iExists (#x, 1%Qp). iFrame "H↦". iSplit; first done.
-    iIntros ([]) "H↦". iMod ("Hclose" with "H↦") as "AU". iIntros "!> HQ".
+    iAuIntro. iApply (astep_aupd_abort with "AU"); first done.
+    iIntros (x) "H↦".
+    iApply (astep_intro (_, _) with "[H↦]"); [solve_ndisj|done|iSplit].
+    { iIntros "$ !> $ !> //". }
+    iIntros ([]) "$ !> AU !> HQ".
     (* Now go on *)
     wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
     wp_apply (cas_spec with "[HQ]"); first by iAccu.
     (* Prove the atomic shift for CAS *)
-    iAuIntro.
-    iMod (aupd_acc with "AU") as (x') "[H↦ Hclose]"; first solve_ndisj.
-    iModIntro. iExists #x'. iFrame. iSplit.
-    { iDestruct "Hclose" as "[Hclose _]". iApply "Hclose". }
-    iIntros ([]). destruct (decide (#x' = #x)) as [[= Hx]|Hx].
-    - iIntros "H↦". iDestruct "Hclose" as "[_ Hclose]". subst.
-      iMod ("Hclose" $! () with "H↦") as "HΦ". iIntros "!> HQ".
+    iAuIntro. iApply (astep_aupd with "AU"); first done.
+    iIntros (x') "H↦".
+    iApply (astep_intro with "[H↦]"); [solve_ndisj|done|iSplit].
+    { iIntros "$ !> $ !> //". }
+    iIntros ([]) "H↦ !>".
+    destruct (decide (#x' = #x)) as [[= ->]|Hx].
+    - iRight. iExists (). iFrame. iIntros "HΦ !> HQ".
       wp_if. by iApply "HΦ".
-    - iDestruct "Hclose" as "[Hclose _]". iIntros "H↦".
-      iMod ("Hclose" with "H↦") as "AU". iIntros "!> HQ".
+    - iLeft. iFrame. iIntros "AU !> HQ".
       wp_if. iApply ("IH" with "HQ"). done.
   Qed.
 
@@ -70,8 +70,8 @@ Section increment_client.
     iAssert (□ WP incr primitive_atomic_heap #l {{ _, True }})%I as "#Aupd".
     { iAlways. wp_apply (incr_spec with "[]"); first by iAccu. clear x.
       iAuIntro. iInv nroot as (x) ">H↦".
-      iApply (astep_intro with "[H↦]"); [solve_ndisj|done|].
-      iSplit; first by eauto 10.
+      iApply (astep_intro with "[H↦]"); [solve_ndisj|done|iSplit].
+      { by eauto 10. }
       iIntros ([]) "H↦ !>". iSplitL "H↦"; first by eauto 10.
       (* The continuation: From after the atomic triple to the postcondition of the WP *)
       done.