Merge branch 'ci/ralf/atomic' into 'master'

Logically atomic triples: Notation, tactics, small example

See merge request FP/iris-coq!163

CHANGELOG.md

@@ -20,6 +20,8 @@ Changes in and extensions of the theory:
 * [#] The Löb rule is now a derived rule; it follows from later-intro, later
   being contractive and the fact that we can take fixpoints of contractive
   functions.
+* [#] Add atomic updates and logically atomic triples, including tactic support.
+  See `heap_lang/lib/increment.v` for an example.
 
 Changes in Coq:
 

tests/atomic.ref

+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  ============================
+  <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  P : val → iProp Σ
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << ∀ x : val, P x
+              ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
+                       << ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << ∀ x : val, l ↦ x
+              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅
+                       << l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+           << l ↦ x, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << l ↦ #()
+              ABORT AU << l ↦ #() >> @ ⊤, ∅
+                       << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AACC << l ↦ #()
+              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >> 
+           @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+"Now come the long pre/post tests"
+     : string
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
+            @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+    code @ ⊤
+  <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+      RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
+         << ∃ yyyy : val, l ↦ yyyy
+                          ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+            COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  ============================
+  <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< l ↦ x, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << l ↦ x, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  ============================
+  <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< ∃ y : val, l ↦ y, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  ============================
+  <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+    code @ ⊤
+  <<< l ↦ #(), RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  x : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
+            << l ↦ #(), COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  ============================
+  <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+    code @ ⊤
+  <<< l ↦ yyyy, RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
+            @ ⊤, ∅ << l ↦ yyyy, COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  ============================
+  <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+    code @ ⊤
+  <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+      RET #() >>>
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  xx, yyyy : val
+  Q : iPropI Σ
+  Φ : language.val heap_lang → iProp Σ
+  ============================
+  _ : Q
+  "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
+            << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+               COMM Q -∗ Φ #() >>
+  --------------------------------------∗
+  WP code {{ v, Φ v }}
+  

tests/atomic.v

+From iris.heap_lang Require Export lifting notation.
+From iris.program_logic Require Export atomic.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
+Set Default Proof Using "Type".
+
+(* Test if AWP and the AU obtained from AWP print. *)
+Section printing.
+  Context `{!heapG Σ}.
+
+  Definition code : expr := #().
+
+  Lemma print_both_quant (P : val → iProp Σ) :
+    <<< ∀ x, P x >>> code @ ⊤ <<< ∃ y, P y, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+    iPoseProof (aupd_aacc with "AU") as "?". Show.
+  Abort.
+
+  Lemma print_first_quant l :
+    <<< ∀ x, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+    iPoseProof (aupd_aacc with "AU") as "?". Show.
+  Abort.
+
+  Lemma print_second_quant l :
+    <<< l ↦ #() >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+    iPoseProof (aupd_aacc with "AU") as "?". Show.
+  Abort.
+
+  Lemma print_no_quant l :
+    <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+    iPoseProof (aupd_aacc with "AU") as "?". Show.
+  Abort.
+
+  Check "Now come the long pre/post tests".
+
+  Lemma print_both_quant_long l :
+    <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+  Abort.
+
+  Lemma print_both_quant_longpre l :
+    <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+  Abort.
+
+  Lemma print_both_quant_longpost l :
+    <<< ∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< ∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? ?". Show.
+  Abort.
+
+  Lemma print_first_quant_long l :
+    <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+  Abort.
+
+  Lemma print_second_quant_long l x :
+    <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+  Abort.
+
+  Lemma print_no_quant_long l x :
+    <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+  Abort.
+
+  Lemma print_no_quant_longpre l xx yyyy :
+    <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+  Abort.
+
+  Lemma print_no_quant_longpost l xx yyyy :
+    <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+  Proof.
+    Show. iIntros (Q Φ) "? AU". Show.
+  Abort.
+
+End printing.

theories/bi/lib/laterable.v

@@ -14,6 +14,9 @@ Section instances.
   Implicit Types P : PROP.
   Implicit Types Ps : list PROP.
 
+  Global Instance laterable_proper : Proper ((⊣⊢) ==> (↔)) (@Laterable PROP).
+  Proof. solve_proper. Qed.
+
   Global Instance later_laterable P : Laterable (▷ P).
   Proof.
     rewrite /Laterable. iIntros "HP". iExists P. iFrame.
@@ -57,4 +60,44 @@ Section instances.
     TCForall Laterable Ps →
     Laterable ([∗] Ps).
   Proof. induction 2; simpl; apply _. Qed.
+
+  (* A wrapper to obtain a weaker, laterable form of any assertion. *)
+  Definition make_laterable (Q : PROP) : PROP :=
+    (∃ P, ▷ P ∗ □ (▷ P -∗ Q))%I.
+
+  Global Instance make_laterable_ne : NonExpansive make_laterable.
+  Proof. solve_proper. Qed.
+  Global Instance make_laterable_proper : Proper ((≡) ==> (≡)) make_laterable := ne_proper _.
+
+  Lemma make_laterable_wand Q1 Q2 :
+    □ (Q1 -∗ Q2) -∗ (make_laterable Q1 -∗ make_laterable Q2).
+  Proof.
+    iIntros "#HQ HQ1". iDestruct "HQ1" as (P) "[HP #HQ1]".
+    iExists P. iFrame. iIntros "!# HP". iApply "HQ". iApply "HQ1". done.
+  Qed.
+
+  Global Instance make_laterable_laterable Q :
+    Laterable (make_laterable Q).
+  Proof.
+    rewrite /Laterable. iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]".
+    iExists P. iFrame. iIntros "!# HP !>". iExists P. by iFrame.
+  Qed.
+
+  Lemma make_laterable_elim Q :
+    make_laterable Q -∗ Q.
+  Proof.
+    iIntros "HQ". iDestruct "HQ" as (P) "[HP #HQ]". by iApply "HQ".
+  Qed.
+
+  Lemma make_laterable_intro P Q :
+    Laterable P →
+    □ (◇ P -∗ Q) -∗ P -∗ make_laterable Q.
+  Proof.
+    iIntros (?) "#HQ HP".
+    iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'.
+    iFrame. iIntros "!# HP'". iApply "HQ". iApply "HPi". done.
+  Qed.
+
 End instances.
+
+Typeclasses Opaque make_laterable.

theories/heap_lang/lib/atomic_heap.v

 From iris.heap_lang Require Export lifting notation.
-From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
+From iris.bi.lib Require Import fractional.
 Set Default Proof Using "Type".
 
 (** A general logically atomic interface for a heap. *)
-Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
+Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   (* -- operations -- *)
   alloc : val;
   load : val;
   store : val;
   cas : val;
   (* -- predicates -- *)
-  (* name is used to associate locked with is_lock *)
   mapsto (l : loc) (q: Qp) (v : val) : iProp Σ;
-  (* -- general properties -- *)
-  mapsto_timeless l q v : Timeless (mapsto l q v);
+  (* -- mapsto properties -- *)
+  mapsto_timeless l q v :> Timeless (mapsto l q v);
+  mapsto_fractional l v :> Fractional (λ q, mapsto l q v);
+  mapsto_as_fractional l q v :>
+    AsFractional (mapsto l q v) (λ q, mapsto l q v) q;
+  mapsto_agree l q1 q2 v1 v2 :> mapsto l q1 v1 -∗ mapsto l q2 v2 -∗ ⌜v1 = v2⌝;
   (* -- operation specs -- *)
-  alloc_spec v :
-    {{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
+  alloc_spec e v :
+    IntoVal e v → {{{ True }}} alloc e {{{ l, RET #l; mapsto l 1 v }}};
   load_spec (l : loc) :
-    atomic_wp (load #l)%E
-              ⊤ ⊤
-              (λ '(v, q), mapsto l q v)
-              (λ '(v, q) (_:()), mapsto l q v)
-              (λ '(v, q) _, v);
+    <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
   store_spec (l : loc) (e : expr) (w : val) :
     IntoVal e w →
-    atomic_wp (store (#l, e))%E
-              ⊤ ⊤
-              (λ v, mapsto l 1 v)
-              (λ v (_:()), mapsto l 1 w)
-              (λ _ _, #()%V);
+    <<< ∀ v, mapsto l 1 v >>> store (#l, e) @ ⊤
+    <<< mapsto l 1 w, RET #() >>>;
   (* This spec is slightly weaker than it could be: It is sufficient for [w1]
   *or* [v] to be unboxed.  However, by writing it this way the [val_is_unboxed]
   is outside the atomic triple, which makes it much easier to use -- and the
   spec is still good enough for all our applications. *)
   cas_spec (l : loc) (e1 e2 : expr) (w1 w2 : val) :
     IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
-    atomic_wp (cas (#l, e1, e2))%E
-              ⊤ ⊤
-              (λ v, mapsto l 1 v)%I
-              (λ v (_:()), if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v)
-              (λ v _, #(if decide (v = w1) then true else false)%V);
+    <<< ∀ v, mapsto l 1 v >>> cas (#l, e1, e2) @ ⊤
+    <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
+        RET #(if decide (v = w1) then true else false) >>>;
 }.
 Arguments atomic_heap _ {_}.
 
+(** Notation for heap primitives, in a module so you can import it separately. *)
+Module notation.
+Notation "l ↦{ q } v" := (mapsto l q v)
+  (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
+Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
+
+Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
+  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
+Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
+
+Notation "'ref' e" := (alloc e) : expr_scope.
+Notation "! e" := (load e) : expr_scope.
+Notation "e1 <- e2" := (store (e1, e2)%E) : expr_scope.
+
+Notation CAS e1 e2 e3 := (cas (e1, e2, e3)%E).
+
+End notation.
+
 (** Proof that the primitive physical operations of heap_lang satisfy said interface. *)
 Definition primitive_alloc : val :=
   λ: "v", ref "v".
@@ -60,54 +72,50 @@ Definition primitive_cas : val :=
 Section proof.
   Context `{!heapG Σ}.
 
-  Lemma primitive_alloc_spec v :
-    {{{ True }}} primitive_alloc v {{{ l, RET #l; l ↦ v }}}.
+  Lemma primitive_alloc_spec e v :
+    IntoVal e v → {{{ True }}} primitive_alloc e {{{ l, RET #l; l ↦ v }}}.
   Proof.
-    iIntros (Φ) "_ HΦ". wp_let. wp_alloc l. iApply "HΦ". done.
+    iIntros (<- Φ) "_ HΦ". wp_let. wp_alloc l. iApply "HΦ". done.
   Qed.
 
   Lemma primitive_load_spec (l : loc) :
-    atomic_wp (primitive_load #l)%E
-              ⊤ ⊤
-              (λ '(v, q), l ↦{q} v)%I
-              (λ '(v, q) (_:()), l ↦{q} v)%I
-              (λ '(v, q) _, v).
+    <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
+    <<< l ↦{q} v, RET v >>>.
   Proof.
     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Φ".
+    iMod "AU" as (v q) "[H↦ [_ Hclose]]".
+    wp_load. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
   Qed.
 
   Lemma primitive_store_spec (l : loc) (e : expr) (w : val) :
     IntoVal e w →
-    atomic_wp (primitive_store (#l, e))%E
-              ⊤ ⊤
-              (λ v, l ↦ v)%I
-              (λ v (_:()), l ↦ w)%I
-              (λ _ _, #()%V).
+    <<< ∀ v, l ↦ v >>> primitive_store (#l, e) @ ⊤
+    <<< l ↦ w, RET #() >>>.
   Proof.
     iIntros (<- 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Φ".
+    iMod "AU" as (v) "[H↦ [_ Hclose]]".
+    wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
   Qed.
 
   Lemma primitive_cas_spec (l : loc) e1 e2 (w1 w2 : val) :
     IntoVal e1 w1 → IntoVal e2 w2 → val_is_unboxed w1 →
-    atomic_wp (primitive_cas (#l, e1, e2))%E
-              ⊤ ⊤
-              (λ v, l ↦ v)%I
-              (λ v (_:()), if decide (v = w1) then l ↦ w2 else l ↦ v)%I
-              (λ v _, #(if decide (v = w1) then true else false)%V).
+    <<< ∀ (v : val), l ↦ v >>>
+      primitive_cas (#l, e1, e2) @ ⊤
+    <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
+        RET #(if decide (v = w1) then true else false) >>>.
   Proof.
     iIntros (<- <- ? Q Φ) "? AU". wp_let. repeat wp_proj.
-    iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj.
+    iMod "AU" as (v) "[H↦ [_ Hclose]]".
     destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
-    iMod ("Hclose" $! () with "H↦") as "HΦ"; by iApply "HΦ".
+    iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
   Qed.
-
-  Definition primitive_atomic_heap : atomic_heap Σ :=
-    {| alloc_spec := primitive_alloc_spec;
-       load_spec := primitive_load_spec;
-       store_spec := primitive_store_spec;
-       cas_spec := primitive_cas_spec |}.
 End proof.
+
+(* NOT an instance because users should choose explicitly to use it
+     (using [Explicit Instance]). *)
+Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
+  {| alloc_spec := primitive_alloc_spec;
+     load_spec := primitive_load_spec;
+     store_spec := primitive_store_spec;
+     cas_spec := primitive_cas_spec;
+     mapsto_agree := gen_heap.mapsto_agree  |}.

theories/heap_lang/lib/increment.v

@@ -2,51 +2,73 @@ From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation atomic_heap par.
+From iris.bi.lib Require Import fractional.
 Set Default Proof Using "Type".
 
 (** Show that implementing fetch-and-add on top of CAS preserves logical
 atomicity. *)
 
-(* TODO: Move this to iris-examples once gen_proofmode is merged. *)
 Section increment.
-  Context `{!heapG Σ} (aheap: atomic_heap Σ).
+  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+
+  Import atomic_heap.notation.
 
   Definition incr: val :=
     rec: "incr" "l" :=
-       let: "oldv" := aheap.(load) "l" in
-       if: aheap.(cas) ("l", "oldv", ("oldv" + #1))
+       let: "oldv" := !"l" in
+       if: CAS "l" "oldv" ("oldv" + #1)
          then "oldv" (* return old value if success *)
          else "incr" "l".
 
   Lemma incr_spec (l: loc) :
-        atomic_wp (incr #l)
-                  ⊤ ⊤
-                  (λ (v: Z), aheap.(mapsto) l 1 #v)%I
-                  (λ v (_:()), aheap.(mapsto) l 1 #(v + 1))%I
-                  (λ v _, #v).
+    <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
-    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 *)
+    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_let.
+    wp_apply load_spec; first by iAccu.
+    (* Prove the atomic update for load *)
     iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
-    iIntros (x) "H↦".
-    iApply (aacc_intro (_, _) with "[H↦]"); [solve_ndisj|done|iSplit].
-    { iIntros "$ !> $ !> //". }
-    iIntros ([]) "$ !> AU !> HQ".
+    iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
+    iIntros "$ !> AU !> _".
     (* Now go on *)
-    wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
-    wp_apply (cas_spec with "[HQ]"); first done; first by iAccu.
-    (* Prove the atomic shift for CAS *)
+    wp_let. wp_op. wp_bind (CAS _ _ _)%I.
+    wp_apply cas_spec; [done|iAccu|].
+    (* Prove the atomic update for CAS *)
     iAuIntro. iApply (aacc_aupd with "AU"); first done.
-    iIntros (x') "H↦".
-    iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
-    { eauto 10 with iFrame. }
-    iIntros ([]) "H↦ !>".
+    iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
+    iIntros "H↦ !>".
     destruct (decide (#x' = #x)) as [[= ->]|Hx].
-    - iRight. iExists (). iFrame. iIntros "HΦ !> HQ".
+    - iRight. iFrame. iIntros "HΦ !> _".
       wp_if. by iApply "HΦ".
-    - iLeft. iFrame. iIntros "AU !> HQ".
-      wp_if. iApply ("IH" with "HQ"). done.
+    - iLeft. iFrame. iIntros "AU !> _".
+      wp_if. iApply "IH". done.
+  Qed.
+
+  Definition weak_incr: val :=
+    rec: "weak_incr" "l" :=
+       let: "oldv" := !"l" in
+       "l" <- ("oldv" + #1);;
+       "oldv" (* return old value *).
+
+  (* TODO: Generalize to q and 1-q, based on some theory for a "maybe-mapsto"
+     connective that works on [option Qp] (the type of 1-q). *)
+  Lemma weak_incr_spec (l: loc) (v : Z) :
+    l ↦{1/2} #v -∗
+    <<< ∀ (v' : Z), l ↦{1/2} #v' >>>
+      weak_incr #l @ ⊤
+    <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
+  Proof.
+    iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_let.
+    wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
+    iIntros "Hl". wp_let. wp_op.
+    wp_apply store_spec; first by iAccu.
+    (* Prove the atomic update for store *)
+    iAuIntro. iApply (aacc_aupd_commit with "AU"); first done.
+    iIntros (x) "H↦".
+    iDestruct (mapsto_agree with "Hl H↦") as %[= <-].
+    iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl".
+    { iIntros "[$ $]"; eauto. }
+    iIntros "$ !>". iSplit; first done.
+    iIntros "HΦ !> _". wp_seq. done.
   Qed.
 
 End increment.
@@ -54,10 +76,12 @@ End increment.
 Section increment_client.
   Context `{!heapG Σ, !spawnG Σ}.
 
+  Existing Instance primitive_atomic_heap.
+
   Definition incr_client : val :=
     λ: "x",
        let: "l" := ref "x" in
-       incr primitive_atomic_heap "l" ||| incr primitive_atomic_heap "l".
+       incr "l" ||| incr "l".
 
   Lemma incr_client_safe (x: Z):
     WP incr_client #x {{ _, True }}%I.
@@ -66,12 +90,10 @@ Section increment_client.
     iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#Hinv"; first eauto.
     (* FIXME: I am only using persistent stuff, so I should be allowed
        to move this to the persisten context even without the additional □. *)
-    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 (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
-      { by eauto 10. }
-      iIntros ([]) "H↦ !>". iSplitL "H↦"; first by eauto 10.
+    iAssert (□ WP incr #l {{ _, True }})%I as "#Aupd".
+    { iAlways. wp_apply incr_spec; first by iAccu. clear x.
+      iAuIntro. iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first 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.
     }

theories/program_logic/atomic.v

+From stdpp Require Import namespaces.
 From iris.program_logic Require Export weakestpre.
 From iris.proofmode Require Import tactics classes.
 From iris.bi.lib Require Export atomic.
+From iris.bi Require Import telescopes.
 Set Default Proof Using "Type".
 
-Definition atomic_wp `{irisG Λ Σ} {A B : Type}
+(* This hard-codes the inner mask to be empty, because we have yet to find an
+example where we want it to be anything else. *)
+Definition atomic_wp `{irisG Λ Σ} {TA TB : tele}
   (e: expr Λ) (* expression *)
-  (Eo Em : coPset) (* outside/module masks *)
-  (α: A → iProp Σ) (* atomic pre-condition *)
-  (β: A → B → iProp Σ) (* atomic post-condition *)
-  (f: A → B → val Λ) (* Turn the return data into the return value *)
+  (Eo : coPset) (* (outer) mask *)
+  (α: TA → iProp Σ) (* atomic pre-condition *)
+  (β: TA → TB → iProp Σ) (* atomic post-condition *)
+  (f: TA → TB → val Λ) (* Turn the return data into the return value *)
   : iProp Σ :=
-    (∀ Q Φ, Q -∗ atomic_update Eo Em α β (λ x y, Q -∗ Φ (f x y)) -∗
+    (∀ Q (Φ : val Λ → iProp Σ), Q -∗
+             atomic_update Eo ∅ α β (λ.. 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)) *)
+   atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
+
+Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+  (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+             (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             e%E
+             Eo
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn, α%I) ..)
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn,
+                         tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                         (λ y1, .. (λ yn, β%I) .. )
+                        ) .. )
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn,
+                         tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                         (λ y1, .. (λ yn, v%V) .. )
+                        ) .. )
+  )
+  (at level 20, Eo, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
+   format "'[hv' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  '/  ' e  @  Eo  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+  : stdpp_scope.
+
+Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
+  (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+             (TB:=TeleO)
+             e%E
+             Eo
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn, α%I) ..)
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn,
+                         tele_app (TT:=TeleO) β%I
+                        ) .. )
+             (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+                       λ x1, .. (λ xn,
+                         tele_app (TT:=TeleO) v%V
+                        ) .. )
+  )
+  (at level 20, Eo, α, β, v at level 200, x1 binder, xn binder,
+   format "'[hv' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  '/  ' e  @  Eo  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+  : stdpp_scope.
+
+Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+  (atomic_wp (TA:=TeleO)
+             (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+             e%E
+             Eo
+             (tele_app (TT:=TeleO) α%I)
+             (tele_app (TT:=TeleO) $
+                       tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                         (λ y1, .. (λ yn, β%I) .. ))
+             (tele_app (TT:=TeleO) $
+                       tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
+                         (λ y1, .. (λ yn, v%V) .. ))
+  )
+  (at level 20, Eo, α, β, v at level 200, y1 binder, yn binder,
+   format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  Eo  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+  : stdpp_scope.
+
+Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
+  (atomic_wp (TA:=TeleO)
+             (TB:=TeleO)
+             e%E
+             Eo
+             (tele_app (TT:=TeleO) α%I)
+             (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) β%I)
+             (tele_app (TT:=TeleO) $ tele_app (TT:=TeleO) v%V)
+  )
+  (at level 20, Eo, α, β, v at level 200,
+   format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  Eo  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
+  : stdpp_scope.
+
+(** Theory *)
+Section lemmas.
+  Context `{irisG Λ Σ} {TA TB : tele}.
+  Notation iProp := (iProp Σ).
+  Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
+
+  Lemma atomic_wp_seq e Eo α β f {HL : ∀.. x, Laterable (α x)} :
+    atomic_wp e Eo α β f -∗
+    ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
+  Proof.
+    rewrite ->tforall_forall in HL.
+    iIntros "Hwp" (Φ x) "Hα HΦ". iApply ("Hwp" with "[HΦ]"); first iAccu.
+    iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
+    (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
+    rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
+  Qed.
+
+  (* Sequential triples with a persistent precondition and no initial quantifier
+  are atomic. *)
+  Lemma seq_wp_atomic e Eo (α : [tele] → iProp) (β : [tele] → TB → iProp)
+        (f : [tele] → TB → val Λ) {HP : ∀.. x, Persistent (α x)} :
+    (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}) -∗
+    atomic_wp e Eo α β f.
+  Proof.
+    simpl in HP. iIntros "Hwp" (Q Φ) "HQ HΦ". iApply fupd_wp.
+    iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
+    iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!>" (y) "Hβ".
+    iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ".
+    (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
+    rewrite ->!tele_app_bind. iApply "HΦ". done.
+  Qed.
+
+  (* Way to prove an atomic triple without seeing the Q *)
+  Lemma wp_atomic_intro e Eo α β f :
+    (∀ (Φ : val Λ → iProp),
+             atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
+             WP e {{ Φ }}) -∗
+    atomic_wp e Eo α β f.
+  Proof.
+    iIntros "Hwp" (Q Φ) "HQ AU". iApply (wp_wand with "[-HQ]").
+    { iApply ("Hwp" $! (λ v, Q -∗ Φ v)%I). done. }
+    iIntros (v) "HΦ". iApply "HΦ". done.
+  Qed.
+End lemmas.