Use telescopes for atomic accessors, updates and triples; improve mask...

Use telescopes for atomic accessors, updates and triples; improve mask handling; add notation for all of them

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/heap_lang/lib/atomic_heap.v

@@ -21,29 +21,20 @@ Structure atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
   alloc_spec v :
     {{{ True }}} alloc v {{{ 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 _ {_}.
 
@@ -67,42 +58,35 @@ Section proof.
   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 (aupd_aacc with "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 (aupd_aacc with "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 (aupd_aacc with "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 Σ :=

theories/heap_lang/lib/increment.v

@@ -19,31 +19,32 @@ Section increment.
          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), aheap.(mapsto) l 1 #v >>> incr #l @ ⊤
+    <<< aheap.(mapsto) l 1 #(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 *)
     iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
     iIntros (x) "H↦".
-    iApply (aacc_intro (_, _) with "[H↦]"); [solve_ndisj|done|iSplit].
+    (* FIXME: Oh wow this is bad. *)
+    iApply (aacc_intro $! ([tele_arg _; _] : [tele (_:val) (_:Qp)]) with "[H↦]"); [solve_ndisj|done|iSplit].
     { iIntros "$ !> $ !> //". }
-    iIntros ([]) "$ !> AU !> HQ".
+    iIntros "$ !> AU !> HQ".
     (* Now go on *)
     wp_let. wp_op. wp_bind (aheap.(cas) _)%I.
-    wp_apply (cas_spec with "[HQ]"); first done; first by iAccu.
+    wp_apply (cas_spec with "[HQ]"); [done|iAccu|].
     (* Prove the atomic shift for CAS *)
     iAuIntro. iApply (aacc_aupd with "AU"); first done.
     iIntros (x') "H↦".
-    iApply (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
+    (* FIXME: Oh wow this is bad. *)
+    iApply (aacc_intro $! ([tele_arg _] : [tele (_:val)]) with "[H↦]"); [solve_ndisj|simpl; by auto with iFrame|iSplit].
     { eauto 10 with iFrame. }
-    iIntros ([]) "H↦ !>".
+    (* FIXME: Manual reduction should not be needed. *)
+    reduction.pm_reduce.
+    iIntros "H↦ !>".
     destruct (decide (#x' = #x)) as [[= ->]|Hx].
-    - iRight. iExists (). iFrame. iIntros "HΦ !> HQ".
+    - iRight. iFrame. iIntros "HΦ !> HQ".
       wp_if. by iApply "HΦ".
     - iLeft. iFrame. iIntros "AU !> HQ".
       wp_if. iApply ("IH" with "HQ"). done.
@@ -69,9 +70,10 @@ 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 (aacc_intro with "[H↦]"); [solve_ndisj|done|iSplit].
+      (* FIXME: Oh wow this is bad. *)
+      iApply (aacc_intro $! ([tele_arg _] : [tele (_:Z)]) with "[H↦]"); [solve_ndisj|done|iSplit].
       { by eauto 10. }
-      iIntros ([]) "H↦ !>". iSplitL "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 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.