From 703718edb667360d1375836aec9608aa130f8caf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 8 Jul 2021 00:08:19 +0200
Subject: [PATCH] make atomic_wp mask work more like wp mask

---
 iris/program_logic/atomic.v      | 83 ++++++++++++++------------------
 iris_heap_lang/lib/atomic_heap.v | 14 +++---
 iris_heap_lang/lib/increment.v   |  8 +--
 3 files changed, 48 insertions(+), 57 deletions(-)

diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 02a1b3fe2..8feb932af 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -10,22 +10,24 @@ From iris.prelude Require Import options.
 example where we want it to be anything else. *)
 Definition atomic_wp `{!irisGS Λ Σ} {TA TB : tele}
   (e: expr Λ) (* expression *)
-  (Eo : coPset) (* (outer) mask *)
+  (E : coPset) (* *implementation* 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 Σ :=
     ∀ (Φ : val Λ → iProp Σ),
-            atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
+            (* The (outer) user mask is what is left after the implementation
+            opened its things. *)
+            atomic_update (⊤∖E) ∅ α β (λ.. x y, Φ (f x y)) -∗
             WP e {{ Φ }}.
 (* Note: To add a private postcondition, use
    atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
 
-Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
              e%E
-             Eo
+             E
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, α%I) ..)
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
@@ -39,15 +41,15 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v
                          (λ 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  '>>>' ']' ']'")
+  (at level 20, E, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
+   format "'[hv' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
-Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
+Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
              (TB:=TeleO)
              e%E
-             Eo
+             E
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, α%I) ..)
              (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
@@ -59,15 +61,15 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
                          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  '>>>' ']' ']'")
+  (at level 20, E, α, β, v at level 200, x1 binder, xn binder,
+   format "'[hv' '<<<'  ∀  x1  ..  xn ,  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
-Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
+Notation "'<<<' α '>>>' e @ E '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
              e%E
-             Eo
+             E
              (tele_app (TT:=TeleO) α%I)
              (tele_app (TT:=TeleO) $
                        tele_app (TT:=TeleS (λ y1, .. (TeleS (λ yn, TeleO)) .. ))
@@ -76,21 +78,21 @@ Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
                        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  '>>>' ']' ']'")
+  (at level 20, E, α, β, v at level 200, y1 binder, yn binder,
+   format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  ∃  y1  ..  yn ,  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
-Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
+Notation "'<<<' α '>>>' e @ E '<<<' β , 'RET' v '>>>'" :=
   (atomic_wp (TA:=TeleO)
              (TB:=TeleO)
              e%E
-             Eo
+             E
              (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  '>>>' ']' ']'")
+  (at level 20, E, α, β, v at level 200,
+   format "'[hv' '<<<'  α  '>>>'  '/  ' e  @  E  '/' '[    ' '<<<'  β ,  '/' 'RET'  v  '>>>' ']' ']'")
   : bi_scope.
 
 (** Theory *)
@@ -99,16 +101,9 @@ Section lemmas.
   Notation iProp := (iProp Σ).
   Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
 
-  Lemma atomic_wp_mask_weaken e Eo1 Eo2 α β f :
-    Eo2 ⊆ Eo1 → atomic_wp e Eo1 α β f -∗ atomic_wp e Eo2 α β f.
-  Proof.
-    iIntros (HEo) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
-    iApply atomic_update_mask_weaken; last done. done.
-  Qed.
-
   (* Atomic triples imply sequential triples if the precondition is laterable. *)
-  Lemma atomic_wp_seq e Eo α β f {HL : ∀.. x, Laterable (α x)} :
-    atomic_wp e Eo α β f -∗
+  Lemma atomic_wp_seq e E α β f {HL : ∀.. x, Laterable (α x)} :
+    atomic_wp e E α β f -∗
     ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
   Proof.
     rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
@@ -120,9 +115,9 @@ Section lemmas.
 
   (** This version matches the Texan triple, i.e., with a later in front of the
   [(∀.. y, β x y -∗ Φ (f x y))]. *)
-  Lemma atomic_wp_seq_step e Eo α β f {HL : ∀.. x, Laterable (α x)} :
+  Lemma atomic_wp_seq_step e E α β f {HL : ∀.. x, Laterable (α x)} :
     TCEq (to_val e) None →
-    atomic_wp e Eo α β f -∗
+    atomic_wp e E α β f -∗
     ∀ Φ, ∀.. x, α x -∗ ▷ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
   Proof.
     iIntros (?) "H"; iIntros (Φ x) "Hα HΦ".
@@ -133,9 +128,9 @@ Section lemmas.
   Qed.
 
   (* Sequential triples with the empty mask for a physically atomic [e] are atomic. *)
-  Lemma atomic_seq_wp_atomic e Eo α β f `{!Atomic WeaklyAtomic e} :
+  Lemma atomic_seq_wp_atomic e E α β f `{!Atomic WeaklyAtomic e} :
     (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e @ ∅ {{ Φ }}) -∗
-    atomic_wp e Eo α β f.
+    atomic_wp e E α β f.
   Proof.
     iIntros "Hwp" (Φ) "AU". iMod "AU" as (x) "[Hα [_ Hclose]]".
     iApply ("Hwp" with "Hα"). iIntros (y) "Hβ".
@@ -145,10 +140,10 @@ Section lemmas.
 
   (** Sequential triples with a persistent precondition and no initial quantifier
   are atomic. *)
-  Lemma persistent_seq_wp_atomic e Eo (α : [tele] → iProp) (β : [tele] → TB → iProp)
+  Lemma persistent_seq_wp_atomic e E (α : [tele] → iProp) (β : [tele] → TB → iProp)
         (f : [tele] → TB → val Λ) {HP : Persistent (α [tele_arg])} :
     (∀ Φ, α [tele_arg] -∗ (∀.. y, β [tele_arg] y -∗ Φ (f [tele_arg] y)) -∗ WP e {{ Φ }}) -∗
-    atomic_wp e Eo α β f.
+    atomic_wp e E α β f.
   Proof.
     simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.
     iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
@@ -158,26 +153,22 @@ Section lemmas.
     rewrite ->!tele_app_bind. done.
   Qed.
 
-  (** The polarity of [Eo] is the opposite of what one might expect: if you have
-      an atomic triple with some mask, you can always *shrink* that mask. *)
-  Lemma wp_atomic_mask e Eo1 Eo2 α β f :
-    Eo2 ⊆ Eo1 →
-    atomic_wp e Eo1 α β f -∗
-    atomic_wp e Eo2 α β f.
+  Lemma atomic_wp_mask_weaken e E1 E2 α β f :
+    E1 ⊆ E2 → atomic_wp e E1 α β f -∗ atomic_wp e E2 α β f.
   Proof.
-    intros ?. iIntros "Hwp" (Φ) "AU". iApply "Hwp".
-    iApply atomic_update_mask_weaken; done.
+    iIntros (HE) "Hwp". iIntros (Φ) "AU". iApply "Hwp".
+    iApply atomic_update_mask_weaken; last done. set_solver.
   Qed.
 
   (** We can open invariants around atomic triples.
       (Just for demonstration purposes; we always use [iInv] in proofs.) *)
-  Lemma wp_atomic_inv e Eo α β f N I :
-    ↑N ⊆ Eo →
-    atomic_wp e Eo (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) f -∗
-    inv N I -∗ atomic_wp e (Eo ∖ ↑N) α β f.
+  Lemma atomic_wp_inv e E α β f N I :
+    ↑N ⊆ E →
+    atomic_wp e (E ∖ ↑N) (λ.. x, ▷ I ∗ α x) (λ.. x y, ▷ I ∗ β x y) f -∗
+    inv N I -∗ atomic_wp e E α β f.
   Proof.
     intros ?. iIntros "Hwp #Hinv" (Φ) "AU". iApply "Hwp". iAuIntro.
-    iInv N as "HI". iApply (aacc_aupd with "AU"); first done.
+    iInv N as "HI". iApply (aacc_aupd with "AU"); first solve_ndisj.
     iIntros (x) "Hα". iAaccIntro with "[HI Hα]"; rewrite ->!tele_app_bind; first by iFrame.
     - (* abort *)
       iIntros "[HI $]". by eauto with iFrame.
diff --git a/iris_heap_lang/lib/atomic_heap.v b/iris_heap_lang/lib/atomic_heap.v
index 302215a8a..af057db21 100644
--- a/iris_heap_lang/lib/atomic_heap.v
+++ b/iris_heap_lang/lib/atomic_heap.v
@@ -29,9 +29,9 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
   free_spec (l : loc) (v : val) :
     {{{ mapsto l (DfracOwn 1) v }}} free #l {{{ l, RET #l; True }}};
   load_spec (l : loc) :
-    ⊢ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
+    ⊢ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ∅ <<< mapsto l q v, RET v >>>;
   store_spec (l : loc) (w : val) :
-    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> store #l w @ ⊤
+    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> store #l w @ ∅
       <<< mapsto l (DfracOwn 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]
@@ -41,7 +41,7 @@ Class atomic_heap {Σ} `{!heapGS Σ} := AtomicHeap {
   [destruct (decide (a = b))] and it will simplify in both places. *)
   cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ⊤
+    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> cmpxchg #l w1 w2 @ ∅
       <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
         RET (v, #if decide (v = w1) then true else false) >>>;
 }.
@@ -75,7 +75,7 @@ Section derived.
 
   Lemma cas_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
-    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @ ⊤
+    ⊢ <<< ∀ v, mapsto l (DfracOwn 1) v >>> CAS #l w1 w2 @ ∅
     <<< if decide (v = w1) then mapsto l (DfracOwn 1) w2 else mapsto l (DfracOwn 1) v,
         RET #if decide (v = w1) then true else false >>>.
   Proof.
@@ -114,7 +114,7 @@ Section proof.
   Qed.
 
   Lemma primitive_load_spec (l : loc) :
-    ⊢ <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
+    ⊢ <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ∅
     <<< l ↦{q} v, RET v >>>.
   Proof.
     iIntros (Φ) "AU". wp_lam.
@@ -123,7 +123,7 @@ Section proof.
   Qed.
 
   Lemma primitive_store_spec (l : loc) (w : val) :
-    ⊢ <<< ∀ v, l ↦ v >>> primitive_store #l w @ ⊤
+    ⊢ <<< ∀ v, l ↦ v >>> primitive_store #l w @ ∅
     <<< l ↦ w, RET #() >>>.
   Proof.
     iIntros (Φ) "AU". wp_lam. wp_let.
@@ -134,7 +134,7 @@ Section proof.
   Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
     val_is_unboxed w1 →
     ⊢ <<< ∀ (v : val), l ↦ v >>>
-      primitive_cmpxchg #l w1 w2 @ ⊤
+      primitive_cmpxchg #l w1 w2 @ ∅
     <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
         RET (v, #if decide (v = w1) then true else false) >>>.
   Proof.
diff --git a/iris_heap_lang/lib/increment.v b/iris_heap_lang/lib/increment.v
index bf82e9b84..3f166ca57 100644
--- a/iris_heap_lang/lib/increment.v
+++ b/iris_heap_lang/lib/increment.v
@@ -21,7 +21,7 @@ Section increment_physical.
          else "incr" "l".
 
   Lemma incr_phy_spec (l: loc) :
-    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
@@ -52,7 +52,7 @@ Section increment.
   (** A proof of the incr specification that unfolds the definition of atomic
       accessors.  This is the style that most logically atomic proofs take. *)
   Lemma incr_spec_direct (l: loc) :
-    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
@@ -91,7 +91,7 @@ Section increment.
       prove are in 1:1 correspondence; most logically atomic proofs will not be
       able to use them. *)
   Lemma incr_spec (l: loc) :
-    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
+    ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ∅ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     awp_apply load_spec.
@@ -126,7 +126,7 @@ Section increment.
   Lemma weak_incr_spec (l: loc) (v : Z) :
     l ↦{#1/2} #v -∗
     <<< ∀ (v' : Z), l ↦{#1/2} #v' >>>
-      weak_incr #l @ ⊤
+      weak_incr #l @ ∅
     <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
   Proof.
     iIntros "Hl" (Φ) "AU". wp_lam.
-- 
GitLab