adjust notation for step-taking updates

theories/base_logic/lib/fancy_updates.v

@@ -70,7 +70,7 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
-  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤,∅}▷=>^n |={⊤,∅}=> ⌜ φ ⌝) →
+  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n |={⊤,∅}=> ⌜ φ ⌝) →
   φ.
 Proof.
   intros Hiter.
@@ -88,7 +88,7 @@ Proof.
 Qed.
 
 Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
-  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤,∅}▷=>^n ⌜ φ ⌝)  →
+  (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
   iIntros (Hiter). eapply (step_fupdN_soundness _ n).

theories/bi/ascii.v

@@ -89,24 +89,24 @@ Notation "|={ E1 , E2 , E3 }|>=> Q" := (|={E1,E2,E3}▷=> Q)%I
   (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
 Notation "P ={ E1 , E2 , E3 }|>=* Q" := (P ={E1,E2,E3}▷=∗ Q)%I
   (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "|={ E1 , E2 }|>=> Q" := (|={E1,E2}▷=> Q)%I
+Notation "|={ E1 } [ E2 ]|>=> Q" := (|={E1}[E2]▷=> Q)%I
   (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
 
-Notation "P ={ E1 , E2 }|>=* Q" := (P ={E1,E2}▷=∗ Q)
+Notation "P ={ E1 } [ E2 ]|>=* Q" := (P ={E1}[E2]▷=∗ Q)
   (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ={ E1 , E2 }|>=* Q" := (P ={E1,E2}▷=∗ Q)%I
+Notation "P ={ E1 } [ E2 ]|>=* Q" := (P ={E1}[E2]▷=∗ Q)%I
   (at level 99, E1,E2 at level 50, Q at level 200, only parsing) : bi_scope.
 
 Notation "|={ E }|>=> Q" := (|={E}▷=> Q)%I
   (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
 Notation "P ={ E }|>=* Q" := (P ={E}▷=∗ Q)%I
   (at level 99, E at level 50, Q at level 200, only parsing) : bi_scope.
-Notation "|={ E1 , E2 }|>=>^ n Q" := (|={E1,E2}▷=>^n Q)%I
+Notation "|={ E1 } [ E2 ]|>=>^ n Q" := (|={E1}[E2]▷=>^n Q)%I
   (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
   : bi_scope.
-Notation "P ={ E1 , E2 }|>=*^ n Q" := (P ={E1,E2}▷=∗^n Q)%I
+Notation "P ={ E1 } [ E2 ]|>=*^ n Q" := (P ={E1}[E2]▷=∗^n Q)%I
   (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
    : stdpp_scope.
-Notation "P ={ E1 , E2 }|>=*^ n Q" := (P ={E1,E2}▷=∗^n Q)%I
+Notation "P ={ E1 } [ E2 ]|>=*^ n Q" := (P ={E1}[E2]▷=∗^n Q)%I
   (at level 99, E1,E2 at level 50, n at level 9, Q at level 200, only parsing)
   : bi_scope.

theories/bi/notation.v

@@ -99,24 +99,31 @@ Reserved Notation "|={ E1 , E2 , E3 }▷=> Q"
 Reserved Notation "P ={ E1 , E2 , E3 }▷=∗ Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "'[' P  '/' ={ E1 , E2 , E3 }▷=∗  Q ']'").
-Reserved Notation "|={ E1 , E2 }▷=> Q"
+Reserved Notation "|={ E1 } [ E2 ]▷=> Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }▷=>  Q").
-Reserved Notation "P ={ E1 , E2 }▷=∗ Q"
+   format "|={ E1 } [ E2 ]▷=>  Q").
+Reserved Notation "P ={ E1 } [ E2 ]▷=∗ Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
-   format "'[' P  '/' ={ E1 , E2 }▷=∗  Q ']'").
+   format "'[' P  '/' ={ E1 } [ E2 ]▷=∗  Q ']'").
 Reserved Notation "|={ E }▷=> Q"
   (at level 99, E at level 50, Q at level 200,
    format "|={ E }▷=>  Q").
 Reserved Notation "P ={ E }▷=∗ Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[' P  '/' ={ E }▷=∗  Q ']'").
-Reserved Notation "|={ E1 , E2 }▷=>^ n Q"
+
+Reserved Notation "|={ E1 } [ E2 ]▷=>^ n Q"
   (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
-   format "|={ E1 , E2 }▷=>^ n  Q").
-Reserved Notation "P ={ E1 , E2 }▷=∗^ n Q"
+   format "|={ E1 } [ E2 ]▷=>^ n  Q").
+Reserved Notation "P ={ E1 } [ E2 ]▷=∗^ n Q"
   (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
-   format "P  ={ E1 , E2 }▷=∗^ n  Q").
+   format "P  ={ E1 } [ E2 ]▷=∗^ n  Q").
+Reserved Notation "|={ E }▷=>^ n Q"
+  (at level 99, E at level 50, n at level 9, Q at level 200,
+   format "|={ E }▷=>^ n  Q").
+Reserved Notation "P ={ E }▷=∗^ n Q"
+  (at level 99, E at level 50, n at level 9, Q at level 200,
+   format "P  ={ E }▷=∗^ n  Q").
 
 (** * Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"

theories/bi/updates.v

@@ -26,17 +26,38 @@ Notation "|={ E }=> Q" := (fupd E E Q) : bi_scope.
 Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I : bi_scope.
 Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q) : stdpp_scope.
 
-(** Fancy updates that take a step. *)
+(** * Fancy updates that take a step. *)
+(** These have three masks: one they start with, one that is active when the step
+    is taken, and one they and with.*)
 Notation "|={ E1 , E2 , E3 }▷=> Q" := (|={E1,E2}=> (▷ |={E2,E3}=> Q))%I : bi_scope.
 Notation "P ={ E1 , E2 , E3 }▷=∗ Q" := (P -∗ |={ E1,E2,E3 }▷=> Q)%I : bi_scope.
-Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2,E1}▷=> Q)%I : bi_scope.
-Notation "P ={ E1 , E2 }▷=∗ Q" := (P ⊢ |={ E1 , E2, E1 }▷=> Q) (only parsing) : stdpp_scope.
-Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q)%I : bi_scope.
-Notation "|={ E }▷=> Q" := (|={E,E}▷=> Q)%I : bi_scope.
-Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I : bi_scope.
-Notation "|={ E1 , E2 }▷=>^ n Q" := (Nat.iter n (λ P, |={E1,E2}▷=> P) Q)%I : bi_scope.
-Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P ⊢ |={E1,E2}▷=>^n Q)%I (only parsing) : stdpp_scope.
-Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P -∗ |={E1,E2}▷=>^n Q)%I : bi_scope.
+Notation "P ={ E1 , E2 , E3 }▷=∗ Q" := (P -∗ |={ E1,E2,E3 }▷=> Q) (only parsing) : stdpp_scope.
+
+(** Often, the first and last mask are the same, so we just have two massk:
+    the "outer" one active at the beginning/end, and the "inner" one active
+    for each step. We avoid the "," here as that looks like a mask-changing update,
+    but this update really starts and ends at E1. *)
+Notation "|={ E1 } [ E2 ]▷=> Q" := (|={E1,E2,E1}▷=> Q)%I : bi_scope.
+Notation "P ={ E1 } [ E2 ]▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q)%I : bi_scope.
+Notation "P ={ E1 } [ E2 ]▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q) (only parsing) : stdpp_scope.
+
+Notation "|={ E }▷=> Q" := (|={E}[E]▷=> Q)%I : bi_scope.
+Notation "P ={ E }▷=∗ Q" := (P ={E}[E]▷=∗ Q)%I : bi_scope.
+Notation "P ={ E }▷=∗ Q" := (P ={E}[E]▷=∗ Q) : stdpp_scope.
+
+(** For the iterated version, in principle there are 4 masks:
+    "outer" and "inner" of [|={E1}[E2]▷=>], as well as a potentially
+    different "begin" and "end" mask. The latter can be obtained from
+    this notation by adding normal mask-changing update modalities:
+    [ |={Ebegin,Eouter}=> |={Eouter}[Einner]▷=>^n |={Eouter,Eend}=> Q]
+*)
+Notation "|={ E1 } [ E2 ]▷=>^ n Q" := (Nat.iter n (λ P, |={E1}[E2]▷=> P) Q)%I : bi_scope.
+Notation "P ={ E1 } [ E2 ]▷=∗^ n Q" := (P -∗ |={E1}[E2]▷=>^n Q)%I : bi_scope.
+Notation "P ={ E1 } [ E2 ]▷=∗^ n Q" := (P -∗ |={E1}[E2]▷=>^n Q) (only parsing) : stdpp_scope.
+
+Notation "|={ E1 }▷=>^ n Q" := (|={E1}[E1]▷=>^n Q)%I : bi_scope.
+Notation "P ={ E1 }▷=∗^ n Q" := (P ={E1}[E1]▷=∗^n Q)%I : bi_scope.
+Notation "P ={ E1 }▷=∗^ n Q" := (P ={E1}[E1]▷=∗^n Q) (only parsing) : stdpp_scope.
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
@@ -338,9 +359,9 @@ Section fupd_derived.
   Qed.
 
   Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
-    F1 ⊆ F2 → E1 ⊆ E2 → (|={E1,F2}▷=> P) ⊢ |={E2,F1}▷=> P.
+    F1 ⊆ F2 → E1 ⊆ E2 → (|={E1}[F2]▷=> P) ⊢ |={E2}[F1]▷=> P.
   Proof.
-    intros ??. rewrite -(emp_sep (|={E1,F2}▷=> P)%I).
+    intros ??. rewrite -(emp_sep (|={E1}[F2]▷=> P)%I).
     rewrite (fupd_intro_mask E2 E1 emp%I) //.
     rewrite fupd_frame_r -(fupd_trans E2 E1 F1). f_equiv.
     rewrite fupd_frame_l -(fupd_trans E1 F2 F1). f_equiv.
@@ -352,11 +373,11 @@ Section fupd_derived.
     by rewrite fupd_frame_r left_id.
   Qed.
 
-  Lemma step_fupd_intro E1 E2 P : E2 ⊆ E1 → ▷ P -∗ |={E1,E2}▷=> P.
+  Lemma step_fupd_intro E1 E2 P : E2 ⊆ E1 → ▷ P -∗ |={E1}[E2]▷=> P.
   Proof. intros. by rewrite -(step_fupd_mask_mono E2 _ _ E2) // -!fupd_intro. Qed.
 
   Lemma step_fupd_frame_l E1 E2 R Q :
-    (R ∗ |={E1, E2}▷=> Q) -∗ |={E1, E2}▷=> (R ∗ Q).
+    (R ∗ |={E1}[E2]▷=> Q) -∗ |={E1}[E2]▷=> (R ∗ Q).
   Proof.
     rewrite fupd_frame_l.
     apply fupd_mono.
@@ -364,7 +385,7 @@ Section fupd_derived.
     by apply later_mono, fupd_mono.
   Qed.
 
-  Lemma step_fupd_fupd E E' P : (|={E,E'}▷=> P) ⊣⊢ (|={E,E'}▷=> |={E}=> P).
+  Lemma step_fupd_fupd E E' P : (|={E}[E']▷=> P) ⊣⊢ (|={E}[E']▷=> |={E}=> P).
   Proof.
     apply (anti_symm (⊢)).
     - by rewrite -fupd_intro.
@@ -372,13 +393,13 @@ Section fupd_derived.
   Qed.
 
   Lemma step_fupdN_mono E1 E2 n P Q :
-    (P ⊢ Q) → (|={E1,E2}▷=>^n P) ⊢ (|={E1,E2}▷=>^n Q).
+    (P ⊢ Q) → (|={E1}[E2]▷=>^n P) ⊢ (|={E1}[E2]▷=>^n Q).
   Proof.
     intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
   Qed.
 
   Lemma step_fupdN_wand E1 E2 n P Q :
-    (|={E1,E2}▷=>^n P) -∗ (P -∗ Q) -∗ (|={E1,E2}▷=>^n Q).
+    (|={E1}[E2]▷=>^n P) -∗ (P -∗ Q) -∗ (|={E1}[E2]▷=>^n Q).
   Proof.
     apply wand_intro_l. induction n as [|n IH]=> /=.
     { by rewrite wand_elim_l. }
@@ -387,14 +408,14 @@ Section fupd_derived.
   Qed.
 
   Lemma step_fupdN_S_fupd n E P:
-    (|={E, ∅}▷=>^(S n) P) ⊣⊢ (|={E, ∅}▷=>^(S n) |={E}=> P).
+    (|={E}[∅]▷=>^(S n) P) ⊣⊢ (|={E}[∅]▷=>^(S n) |={E}=> P).
   Proof.
     apply (anti_symm (⊢)); rewrite !Nat_iter_S_r; apply step_fupdN_mono;
       rewrite -step_fupd_fupd //.
   Qed.
 
   Lemma step_fupdN_frame_l E1 E2 n R Q :
-    (R ∗ |={E1, E2}▷=>^n Q) -∗ |={E1, E2}▷=>^n (R ∗ Q).
+    (R ∗ |={E1}[E2]▷=>^n Q) -∗ |={E1}[E2]▷=>^n (R ∗ Q).
   Proof.
     induction n as [|n IH]; simpl; [done|].
     rewrite step_fupd_frame_l IH //=.
@@ -465,13 +486,13 @@ Section fupd_derived.
       (|={E}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E}=> Φ x).
     Proof. by apply fupd_plain_forall. Qed.
 
-    Lemma step_fupd_plain E E' P `{!Plain P} : (|={E,E'}▷=> P) ={E}=∗ ▷ ◇ P.
+    Lemma step_fupd_plain E E' P `{!Plain P} : (|={E}[E']▷=> P) ={E}=∗ ▷ ◇ P.
     Proof.
       rewrite -(fupd_plain_mask _ E' (▷ ◇ P)%I).
       apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
     Qed.
 
-    Lemma step_fupdN_plain E E' n P `{!Plain P} : (|={E,E'}▷=>^n P) ={E}=∗ ▷^n ◇ P.
+    Lemma step_fupdN_plain E E' n P `{!Plain P} : (|={E}[E']▷=>^n P) ={E}=∗ ▷^n ◇ P.
     Proof.
       induction n as [|n IH].
       - by rewrite -fupd_intro -except_0_intro.
@@ -483,7 +504,7 @@ Section fupd_derived.
 
     Lemma step_fupd_plain_forall E1 E2 {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
       E2 ⊆ E1 →
-      (|={E1,E2}▷=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1,E2}▷=> Φ x).
+      (|={E1}[E2]▷=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1}[E2]▷=> Φ x).
     Proof.
       intros. apply (anti_symm _).
       { apply forall_intro=> x. by rewrite (forall_elim x). }

theories/program_logic/adequacy.v

@@ -18,7 +18,7 @@ Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ fork_post }})%I.
 
 Lemma wp_step s e1 σ1 κ κs e2 σ2 efs m Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
-  state_interp σ1 (κ ++ κs) m -∗ WP e1 @ s; ⊤ {{ Φ }} ={⊤,∅}▷=∗
+  state_interp σ1 (κ ++ κs) m -∗ WP e1 @ s; ⊤ {{ Φ }} ={⊤}[∅]▷=∗
   state_interp σ2 κs (length efs + m) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s efs.
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "Hσ H".
@@ -32,7 +32,7 @@ Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
   step (e1 :: t1,σ1) κ (t2, σ2) →
   state_interp σ1 (κ ++ κs) (length t1) -∗ WP e1 @ s; ⊤ {{ Φ }} -∗ wptp s t1 ==∗
   ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗
-  |={⊤,∅}▷=> state_interp σ2 κs (pred (length t2)) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2'.
+  |={⊤}[∅]▷=> state_interp σ2 κs (pred (length t2)) ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2'.
 Proof.
   iIntros (Hstep) "Hσ He Ht".
   destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
@@ -52,7 +52,7 @@ Qed.
 Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   state_interp σ1 (κs ++ κs') (length t1) -∗ WP e1 @ s; ⊤ {{ Φ }} -∗ wptp s t1
-  ={⊤,∅}▷=∗^n ∃ e2 t2',
+  ={⊤}[∅]▷=∗^n ∃ e2 t2',
     ⌜t2 = e2 :: t2'⌝ ∗
     state_interp σ2 κs' (pred (length t2)) ∗
     WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2'.
@@ -80,7 +80,7 @@ Lemma wptp_strong_adequacy Φ κs' s n e1 t1 κs t2 σ1 σ2 :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   state_interp σ1 (κs ++ κs') (length t1) -∗
   WP e1 @ s; ⊤ {{ Φ }} -∗
-  wptp s t1 ={⊤,∅}▷=∗^(S n) ∃ e2 t2',
+  wptp s t1 ={⊤}[∅]▷=∗^(S n) ∃ e2 t2',
     ⌜ t2 = e2 :: t2' ⌝ ∗
     ⌜ ∀ e2, s = NotStuck → e2 ∈ t2 → not_stuck e2 σ2 ⌝ ∗
     state_interp σ2 κs' (length t2') ∗

theories/program_logic/ectx_lifting.v

@@ -70,7 +70,7 @@ Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -102,7 +102,7 @@ Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
       ⌜efs = []⌝ ∗ state_interp σ2 κs n ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
@@ -132,7 +132,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
     head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
-  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E}[E']▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2); eauto.
   destruct s; by auto.

theories/program_logic/lifting.v

@@ -55,7 +55,7 @@ Qed.
 Lemma wp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E E' Φ e1 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
-  (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E {{ Φ }})
+  (|={E}[E']▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E {{ Φ }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
@@ -85,7 +85,7 @@ Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1}[E2]▷=∗
       state_interp σ2 κs (length efs + n) ∗
       from_option Φ False (to_val e2) ∗
       [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
@@ -123,7 +123,7 @@ Lemma wp_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E E' Φ} e1 e2 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
     κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
-  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E}[E']▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step_no_fork s E E'); try done.
   { naive_solver. }
@@ -134,7 +134,7 @@ Qed.
 Lemma wp_pure_step_fupd `{!Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
   φ →
-  (|={E,E'}▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
+  (|={E}[E']▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
   iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.

theories/program_logic/weakestpre.v

@@ -141,7 +141,7 @@ Qed.
 
 Lemma wp_step_fupd s E1 E2 e P Φ :
   TCEq (to_val e) None → E2 ⊆ E1 →
-  (|={E1,E2}▷=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; E1 {{ Φ }}.
+  (|={E1}[E2]▷=> P) -∗ WP e @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; E1 {{ Φ }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
   iIntros (σ1 κ κs n) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
@@ -221,14 +221,14 @@ Proof. iIntros "[H ?]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
 
 Lemma wp_frame_step_l s E1 E2 e Φ R :
   TCEq (to_val e) None → E2 ⊆ E1 →
-  (|={E1,E2}▷=> R) ∗ WP e @ s; E2 {{ Φ }} ⊢ WP e @ s; E1 {{ v, R ∗ Φ v }}.
+  (|={E1}[E2]▷=> R) ∗ WP e @ s; E2 {{ Φ }} ⊢ WP e @ s; E1 {{ v, R ∗ Φ v }}.
 Proof.
   iIntros (??) "[Hu Hwp]". iApply (wp_step_fupd with "Hu"); try done.
   iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
 Qed.
 Lemma wp_frame_step_r s E1 E2 e Φ R :
   TCEq (to_val e) None → E2 ⊆ E1 →
-  WP e @ s; E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ WP e @ s; E1 {{ v, Φ v ∗ R }}.
+  WP e @ s; E2 {{ Φ }} ∗ (|={E1}[E2]▷=> R) ⊢ WP e @ s; E1 {{ v, Φ v ∗ R }}.
 Proof.
   rewrite [(WP _ @ _; _ {{ _ }} ∗ _)%I]comm; setoid_rewrite (comm _ _ R).
   apply wp_frame_step_l.

theories/proofmode/class_instances_updates.v

@@ -109,7 +109,7 @@ Global Instance from_forall_step_fupd
   (* Some cases in which [E2 ⊆ E1] holds *)
   TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
   FromForall P Φ → (∀ x, Plain (Φ x)) →
-  FromForall (|={E1,E2}▷=> P)%I (λ a, |={E1,E2}▷=> (Φ a))%I.
+  FromForall (|={E1}[E2]▷=> P)%I (λ a, |={E1}[E2]▷=> (Φ a))%I.
 Proof.
   rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
 Qed.