New atomic updates: defined as a fixed point with existential quantifier;...

New atomic updates: defined as a fixed point with existential quantifier; intro lemma using class of Laterable assertions

_CoqProject

@@ -40,6 +40,7 @@ theories/bi/embedding.v
 theories/bi/lib/counter_examples.v
 theories/bi/lib/fixpoint.v
 theories/bi/lib/fractional.v
+theories/bi/lib/laterable.v
 theories/bi/lib/atomic.v
 theories/bi/lib/core.v
 theories/base_logic/upred.v

theories/bi/lib/atomic.v

 From iris.bi Require Export bi updates.
+From iris.bi.lib Require Import fixpoint laterable.
 From stdpp Require Import coPset.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition atomic_shift `{BiFUpd PROP} {A B : Type}
-  (α : A → PROP) (* atomic pre-condition *)
-  (β : A → B → PROP) (* atomic post-condition *)
-  (Eo Em : coPset) (* outside/module masks *)
-  (P : PROP) (* pre-condition *)
-  (Q : A → B → PROP) (* post-condition *)
-  : PROP :=
-    (□ (∀ E, ⌜Eo ⊆ E⌝ -∗ P ={E, E∖Em}=∗ ∃ x, α x ∗
-          ((α x ={E∖Em, E}=∗ P) ∧ (∀ y, β x y ={E∖Em, E}=∗ Q x y)))
-    )%I.
+(** atomic_update as a fixed-point of the equation
+   AU = ∃ P. ▷ P ∗ □ (▷ P ==∗ α ∗ (α ==∗ AU) ∧ (β ==∗ Q))
+ *)
+Section definition.
+  Context `{BiFUpd PROP} {A B : Type}
+    (α : A → PROP) (* atomic pre-condition *)
+    (β : A → B → PROP) (* atomic post-condition *)
+    (Eo Em : coPset) (* outside/module masks *)
+    (Φ : A → B → PROP) (* post-condition *)
+  .
 
-Definition atomic_update `{BiFUpd PROP} {A B : Type}
-  (α : A → PROP) (* atomic pre-condition *)
-  (β : A → B → PROP) (* atomic post-condition *)
-  (Eo Em : coPset) (* outside/module masks *)
-  (Q : A → B → PROP) (* post-condition *)
-  : PROP :=
-    tc_opaque (
-      ∃ (F P : PROP), F ∗ ▷ P ∗ atomic_shift α β Eo Em (▷ P) (λ x y, F -∗ Q x y)
+  Definition atomic_shift (P P' : PROP) : PROP :=
+    (□ (∀ E, ⌜Eo ⊆ E⌝ → P ={E, E∖Em}=∗ ∃ x, α x ∗
+          ((α x ={E∖Em, E}=∗ P') ∧ (∀ y, β x y ={E∖Em, E}=∗ Φ x y)))
     )%I.
 
+  Lemma atomic_shift_mono P P1 P2:
+    □ (P1 -∗ P2) -∗ □ (atomic_shift P P1 -∗ atomic_shift P P2).
+  Proof.
+    iIntros "#HP12 !# #AS !# * % HP".
+    iMod ("AS" with "[% //] HP") 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.
+  Qed.
+
+  Definition atomic_update_pre (Ψ : () → PROP) (_ : ()) : PROP :=
+    (∃ (P : PROP), ▷ P ∗ atomic_shift (▷ P) (Ψ ()))%I.
+
+  Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre.
+  Proof.
+    constructor.
+    - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
+      iDestruct "AU" as (P) "[HP AS]". iExists P. iFrame.
+      iApply (atomic_shift_mono with "[HP12]"); last done.
+      iAlways. iApply "HP12".
+    - intros ??. solve_proper.
+  Qed.
+
+  Definition atomic_update_def :=
+    bi_greatest_fixpoint atomic_update_pre ().
+End definition.
+
+(** Seal it *)
+Definition atomic_update_aux : seal (@atomic_update_def). by eexists. Qed.
+Definition atomic_update `{BiFUpd PROP} {A B : Type} := atomic_update_aux.(unseal) PROP _ A B.
+Definition atomic_update_eq :
+  @atomic_update = @atomic_update_def := atomic_update_aux.(seal_eq).
+
+(** Lemmas about AU *)
 Section lemmas.
   Context `{BiFUpd PROP} {A B : Type}.
-  Implicit Types (α : A → PROP) (β: A → B → PROP) (P : PROP) (Q : A → B → PROP).
+  Implicit Types (α : A → PROP) (β: A → B → PROP) (P : PROP) (Φ : A → B → PROP).
+
+  Local Existing Instance atomic_update_pre_mono.
 
-  Lemma aupd_acc α β Eo Em Q E :
+  (** The ellimination form: an accessor *)
+  Lemma aupd_acc α β Eo Em Φ E :
     Eo ⊆ E →
-    atomic_update α β Eo Em Q -∗
+    atomic_update α β Eo Em Φ -∗
     |={E, E∖Em}=> ∃ x, α x ∗
-      ((α x ={E∖Em, E}=∗ atomic_update α β Eo Em Q) ∧
-       (∀ y, β x y ={E∖Em, E}=∗ Q x y)).
+      ((α x ={E∖Em, E}=∗ atomic_update α β Eo Em Φ) ∧
+       (∀ y, β x y ={E∖Em, E}=∗ Φ x y)).
   Proof using Type*.
-    rewrite {1}/atomic_update /=. iIntros (HE) "HUpd".
-    iDestruct "HUpd" as (F P) "(HF & HP & #Hshift)".
+    rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros (HE) "HUpd".
+    iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd".
+    iDestruct "HUpd" as (P) "(HP & Hshift)".
     iMod ("Hshift" with "[% //] HP") as (x) "[Hα Hclose]".
-    iModIntro. iExists x. iFrame "Hα". iSplit.
-    - iIntros "Hα". iDestruct "Hclose" as "[Hclose _]".
-      iMod ("Hclose" with "Hα"). iModIntro. iExists F, P.
-      by iFrame.
-    - iIntros (y) "Hβ". iDestruct "Hclose" as "[_ Hclose]".
-      iMod ("Hclose" with "Hβ") as "HQ". iModIntro. by iApply "HQ".
+    iModIntro. iExists x. iFrame.
+  Qed.
+
+  Global Instance aupd_laterable α β Eo Em Φ :
+    Laterable (atomic_update α β Eo Em Φ).
+  Proof.
+    rewrite /Laterable atomic_update_eq {1}/atomic_update_def /=. iIntros "AU".
+    iPoseProof (greatest_fixpoint_unfold_1 with "AU") as (P) "[HP #AS]".
+    iExists P. iFrame. iIntros "!# HP !>".
+    iApply greatest_fixpoint_unfold_2. iExists P. iFrame "#∗".
+  Qed.
+
+  Lemma aupd_intro P α β Eo Em Φ :
+    Em ⊆ Eo → Laterable P →
+    P -∗
+    □ (P -∗ |={Eo, Eo∖Em}=> ∃ x, α x ∗
+      ((α x ={Eo∖Em, Eo}=∗ P) ∧ (∀ y, β x y ={Eo∖Em, Eo}=∗ Φ x y))) -∗
+    atomic_update α β Eo Em Φ.
+  Proof.
+    rewrite atomic_update_eq {1}/atomic_update_def /=.
+    iIntros (??) "HP #AU".
+    iApply (greatest_fixpoint_coind _ (λ _, P)); last done. iIntros "!#" ([]) "HP".
+    iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'. iFrame.
+    iIntros "!#" (E HE) "HP'". iDestruct ("HPi" with "HP'") as ">HP {HPi}".
+    iApply fupd_mask_frame_diff_open; last
+      iMod ("AU" with "HP") as (x) "[Hα Hclose] {AU}"; [done..|].
+    iModIntro. iExists x. iFrame. iSplit.
+    - iDestruct "Hclose" as "[Hclose _]". iIntros "Hα".
+      iApply fupd_mask_frame_diff_close; last (by iApply "Hclose"); done.
+    - iDestruct "Hclose" as "[_ Hclose]". iIntros (y) "Hβ".
+      iApply fupd_mask_frame_diff_close; last (by iApply "Hclose"); done.
   Qed.
 End lemmas.

theories/bi/lib/laterable.v

+From iris.bi Require Export bi.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+(** The class of laterable assertions *)
+Class Laterable {PROP : sbi} (P : PROP) := laterable :
+  P -∗ ∃ Q, ▷ Q ∗ □ (▷ Q -∗ ◇ P).
+Arguments Laterable {_} _%I : simpl never.
+Arguments laterable {_} _%I {_}.
+Hint Mode Laterable + ! : typeclass_instances.
+
+Section instances.
+  Context {PROP : sbi}.
+  Implicit Type (P : PROP).
+
+  Global Instance later_laterable P : Laterable (▷ P).
+  Proof.
+    rewrite /Laterable. iIntros "HP". iExists P. iFrame.
+    iIntros "!# HP !>". done.
+  Qed.
+
+  Global Instance timeless_laterable P :
+    Timeless P → Laterable P.
+  Proof.
+    rewrite /Laterable. iIntros (?) "HP". iExists P%I. iFrame.
+    iSplitR; first by iNext. iIntros "!# >HP !>". done.
+  Qed.
+
+  (** This lemma is not very useful: It needs a strange assumption about
+      emp, and most of the time intuitionistic propositions can be just kept
+      around anyway and don't need to be "latered".  The lemma exists
+      because the fact that it needs the side-condition is interesting;
+      it is not an instance because it won't usually get used. *)
+  Lemma intuitionistic_laterable P :
+    Timeless (PROP:=PROP) emp → Affine P → Persistent P → Laterable P.
+  Proof.
+    rewrite /Laterable. iIntros (???) "#HP".
+    iExists emp%I. iSplitL; first by iNext.
+    iIntros "!# >_". done.
+  Qed.
+
+  Global Instance sep_laterable P Q :
+    Laterable P → Laterable Q → Laterable (P ∗ Q).
+  Proof.
+    rewrite /Laterable. iIntros (LP LQ) "[HP HQ]".
+    iDestruct (LP with "HP") as (P') "[HP' #HP]".
+    iDestruct (LQ with "HQ") as (Q') "[HQ' #HQ]".
+    iExists (P' ∗ Q')%I. iSplitL; first by iFrame.
+    iIntros "!# [HP' HQ']". iSplitL "HP'".
+    - iApply "HP". done.
+    - iApply "HQ". done.
+  Qed.
+End instances.

theories/heap_lang/lib/atomic_heap.v

@@ -69,9 +69,9 @@ Section proof.
               ⊤ ⊤
               (λ '(v, q) _, v).
   Proof.
-    iIntros (Φ) "Aupd". wp_let.
-    iMod (aupd_acc with "Aupd") as ((v, q)) "[H↦ [_ Hclose]]"; first solve_ndisj.
-    wp_load. iMod ("Hclose" $! () with "H↦"). done.
+    iIntros (Q Φ) "? AU". wp_let.
+    iMod (aupd_acc with "AU") as ((v, q)) "[H↦ [_ Hclose]]"; first solve_ndisj.
+    wp_load. iMod ("Hclose" $! () with "H↦") as "HΦ". by iApply "HΦ".
   Qed.
 
   Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
@@ -82,9 +82,9 @@ Section proof.
               ⊤ ⊤
               (λ _ _, #()%V).
   Proof.
-    iIntros (<-%of_to_val Φ) "Aupd". wp_let. wp_proj. wp_proj.
-    iMod (aupd_acc with "Aupd") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
-    wp_store. iMod ("Hclose" $! () with "H↦"). done.
+    iIntros (<-%of_to_val Q Φ) "? AU". wp_let. wp_proj. wp_proj.
+    iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
+    wp_store. iMod ("Hclose" $! () with "H↦") as "HΦ". by iApply "HΦ".
   Qed.
 
   Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
@@ -95,10 +95,10 @@ Section proof.
               ⊤ ⊤
               (λ v _, #(if decide (v = w1) then true else false)%V).
   Proof.
-    iIntros (<-%of_to_val <-%of_to_val Φ) "Aupd". wp_let. repeat wp_proj.
-    iMod (aupd_acc with "Aupd") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
+    iIntros (<-%of_to_val <-%of_to_val Q Φ) "? AU". wp_let. repeat wp_proj.
+    iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
     destruct (decide (v = w1)) as [Hv|Hv]; [wp_cas_suc|wp_cas_fail];
-    iMod ("Hclose" $! () with "H↦"); done.
+    iMod ("Hclose" $! () with "H↦") as "HΦ"; by iApply "HΦ".
   Qed.
 
   Definition primitive_atomic_heap : atomic_heap Σ :=

theories/heap_lang/lib/increment.v

@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation atomic_heap par.
 Set Default Proof Using "Type".
 
-(** Show taht implementing fetch-and-add on top of CAS preserves logical
+(** Show that implementing fetch-and-add on top of CAS preserves logical
 atomicity. *)
 
 (* TODO: Move this to iris-examples once gen_proofmode is merged. *)
@@ -26,32 +26,28 @@ Section increment.
                   ⊤ ⊤
                   (λ v _, #v).
   Proof.
-    iIntros (Φ) "AUpd". iLöb as "IH". wp_let.
-    wp_apply load_spec.
+    iIntros (Q Φ) "HQ AU". iLöb as "IH". wp_let.
+    wp_apply (load_spec with "HQ").
     (* Prove the atomic shift for load *)
-    iDestruct "AUpd" as (F P) "(HF & HP & #AShft)".
-    iExists F, P. iFrame. iIntros "!#" (E ?) "HP".
-    iMod ("AShft" with "[%] HP") as (x) "[H↦ Hclose]"; first done.
-    iModIntro. iExists (#x, 1%Qp). iFrame. iSplit.
-    { iDestruct "Hclose" as "[Hclose _]". iApply "Hclose". }
-    iIntros (_) "H↦". iDestruct "Hclose" as "[Hclose _]".
-    iMod ("Hclose" with "H↦") as "HP". iIntros "!> HF".
-    clear dependent E.
+    iApply (aupd_intro with "AU"); first done. iIntros "!# AU".
+    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".
     (* Now go on *)
     wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
-    wp_apply cas_spec.
+    wp_apply (cas_spec with "HQ").
     (* Prove the atomic shift for CAS *)
-    iExists F, P. iFrame. iIntros "!# * % HP".
-    iMod ("AShft" with "[%] HP") as (x') "[H↦ Hclose]"; first done.
+    iApply (aupd_intro with "AU"); first done. iIntros "!# AU".
+    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 ([]). destruct (decide (#x' = #x)) as [[= Hx]|Hx].
     - iIntros "H↦". iDestruct "Hclose" as "[_ Hclose]". subst.
-      iMod ("Hclose" $! () with "H↦") as "HΦ". iIntros "!> HF".
+      iMod ("Hclose" $! () with "H↦") as "HΦ". iIntros "!> HQ".
       wp_if. by iApply "HΦ".
     - iDestruct "Hclose" as "[Hclose _]". iIntros "H↦".
-      iMod ("Hclose" with "H↦") as "HP". iIntros "!> HF".
-      wp_if. iApply "IH". iExists F, P. iFrame. done.
+      iMod ("Hclose" with "H↦") as "AU". iIntros "!> HQ".
+      wp_if. iApply ("IH" with "HQ"). done.
   Qed.
 
 End increment.
@@ -71,13 +67,9 @@ Section increment_client.
     iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
     (* FIXME: I am only usign persistent stuff, so I should be allowed
        to move this to the persisten context even without the additional □. *)
-    iAssert (□ atomic_update (λ (v: Z), l ↦ #v)
-                           (λ v (_:()), l ↦ #(v + 1))
-                           ⊤ ⊤
-                           (λ _ _, True))%I as "#Aupd".
-    { iAlways. iExists True%I, True%I. repeat (iSplit; first done). clear x.
-      iIntros "!#" (E) "% _".
-      assert (E = ⊤) as -> by set_solver.
+    iAssert (□ WP incr primitive_atomic_heap #l {{ _, True }})%I as "#Aupd".
+    { iAlways. wp_apply (incr_spec with "[]"); first iEmpIntro. clear x.
+      iApply (aupd_intro with "[]"); try iEmpIntro; [done|apply _|]. iIntros "!# _".
       iInv nroot as (x) ">H↦" "Hclose".
       iMod fupd_intro_mask' as "Hclose2"; last iModIntro; first set_solver.
       iExists _. iFrame. iSplit.
@@ -85,10 +77,9 @@ Section increment_client.
         iNext. iExists _. iFrame. }
       iIntros (_) "H↦". iMod "Hclose2" as "_".
       iMod ("Hclose" with "[-]"); last done. iNext. iExists _. iFrame. }
-    wp_apply (wp_par (λ _, True)%I (λ _, True)%I).
-    - wp_apply incr_spec. iAssumption. (* FIXME: without giving the
-      postconditions above, this diverges. *)
-    - wp_apply incr_spec. iAssumption.
+    wp_apply wp_par.
+    - iAssumption.
+    - iAssumption.
     - iIntros (??) "_ !>". done.
   Qed.
 

theories/program_logic/atomic.v

@@ -10,7 +10,7 @@ Definition atomic_wp `{irisG Λ Σ} {A B : Type}
   (Eo Em : coPset) (* outside/module masks *)
   (f: A → B → val Λ) (* Turn the return data into the return value *)
   : iProp Σ :=
-    (∀ Φ, atomic_update α β Eo Em (λ x y, Φ (f x y)) -∗
-          WP e {{ Φ }})%I.
+    (∀ Q Φ, Q -∗ atomic_update α β Eo Em (λ x y, Q -∗ Φ (f x y)) -∗
+             WP e {{ Φ }})%I.
 (* Note: To add a private postcondition, use
    atomic_update α β Eo Em (λ x y, POST x y -∗ Φ (f x y)) *)