diff --git a/naming.txt b/naming.txt
index 191c1664e7b820563ec755f3554a0cf746ce9e0f..056cad64319a7e9628a86d31846ac5cc4b777d9b 100644
--- a/naming.txt
+++ b/naming.txt
@@ -14,7 +14,7 @@ l
 m : iGst = ghost state
 n
 o
-p
+p : progress bits
 q
 r : iRes = resources
 s : state (STSs)
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index fa3bc513f177ede6d839a3f2efce31bf0dd20117..a9b9a24346340832bc6224320007fabfacb30f42 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -16,7 +16,7 @@ Proof. solve_inG. Qed.
 
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
   (∀ `{heapG Σ}, WP e {{ v, ⌜φ v⌝ }}%I) →
-  adequate e σ φ.
+  adequate true e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 46c2aeb8ba29898624b6937479afb1c8ad863da0..7a99bec9935e0f4a9219f3cd59844d88cf5989e0 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -76,7 +76,7 @@ Lemma wp_fork E e Φ :
   ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
   rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ (Lit _)) // right_id.
+  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ _ (Lit _)) // right_id.
   - intros; inv_head_step; eauto.
 Qed.
 
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 677aa60634ba8c6f1518ab3dcd199e846caffd21..919fbf058fd8de5b9cc967d09f3453532e765067 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -27,7 +27,7 @@ Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
+  | |- envs_entails _ (wp true ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
     [simpl; apply _                 (* PureExec *)
@@ -66,7 +66,7 @@ Ltac wp_bind_core K :=
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp true ?E ?e ?Q) =>
     reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
     || fail "wp_bind: cannot find" efoc "in" e
   | _ => fail "wp_bind: not a 'wp'"
@@ -151,7 +151,7 @@ End heap.
 Tactic Notation "wp_apply" open_constr(lem) :=
   iPoseProofCore lem as false true (fun H =>
     lazymatch goal with
-    | |- envs_entails _ (wp ?E ?e ?Q) =>
+    | |- envs_entails _ (wp true ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
         wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
       lazymatch iTypeOf H with
@@ -163,7 +163,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp true ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_alloc _ _ _ H K); [apply _|..])
@@ -182,7 +182,7 @@ Tactic Notation "wp_alloc" ident(l) :=
 Tactic Notation "wp_load" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp true ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K))
       |fail 1 "wp_load: cannot find 'Load' in" e];
@@ -196,7 +196,7 @@ Tactic Notation "wp_load" :=
 Tactic Notation "wp_store" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp true ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_store _ _ _ _ _ K); [apply _|..])
@@ -212,7 +212,7 @@ Tactic Notation "wp_store" :=
 Tactic Notation "wp_cas_fail" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp true ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_cas_fail _ _ _ _ K); [apply _|apply _|..])
@@ -228,7 +228,7 @@ Tactic Notation "wp_cas_fail" :=
 Tactic Notation "wp_cas_suc" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp true ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 1198fb520ac2490fd90ca8390bb499a2dd0f47c2..6cfa3e1dfe59835007d5365c6faf66b727f9f729 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -187,11 +187,10 @@ Definition is_atomic (e : expr) :=
   | App (Rec _ _ (Lit _)) (Lit _) => true
   | _ => false
   end.
-Lemma is_atomic_correct e : is_atomic e → Atomic (to_expr e).
+Lemma is_atomic_correct e : is_atomic e → StronglyAtomic (to_expr e).
 Proof.
-  intros He. apply ectx_language_atomic.
-  - intros σ e' σ' ef Hstep; simpl in *.
-    apply language.val_irreducible; revert Hstep.
+  intros He. apply ectx_language_strongly_atomic.
+  - intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
     destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
     unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
@@ -227,11 +226,11 @@ Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with
-  | |- Atomic ?e =>
-     let e' := W.of_expr e in change (Atomic (W.to_expr e'));
+  | |- StronglyAtomic ?e =>
+     let e' := W.of_expr e in change (StronglyAtomic (W.to_expr e'));
      apply W.is_atomic_correct; vm_compute; exact I
   end.
-Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances.
+Hint Extern 10 (StronglyAtomic _) => solve_atomic : typeclass_instances.
 
 (** Substitution *)
 Ltac simpl_subst :=
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 8d6f9a85b3517fdd6c8e9be2b3bc322859fcb903..f1ca9358797dfaf5ef1335a50957d900b718f148 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -34,23 +34,24 @@ Proof.
 Qed.
 
 (* Program logic adequacy *)
-Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
+Record adequate {Λ} (p : bool) (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
   adequate_result t2 σ2 v2 :
    rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2;
   adequate_safe t2 σ2 e2 :
+   p →
    rtc step ([e1], σ1) (t2, σ2) →
-   e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2)
+   e2 ∈ t2 → progressive e2 σ2
 }.
 
 Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
-  adequate e1 σ1 φ →
+  adequate true e1 σ1 φ →
   rtc step ([e1], σ1) (t2, σ2) →
   Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
 Proof.
   intros Had ?.
   destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
   apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
-  destruct (adequate_safe e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
+  destruct (adequate_safe true e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
     rewrite ?eq_None_not_Some; auto.
   { exfalso. eauto. }
   destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
@@ -58,19 +59,22 @@ Proof.
 Qed.
 
 Section adequacy.
-Context `{irisG Λ Σ}.
+Context `{irisG Λ Σ} (p : bool).
 Implicit Types e : expr Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
 
-Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ)%I.
+Notation world' E σ := (wsat ∗ ownE E ∗ state_interp σ)%I.
+Notation world σ := (world' ⊤ σ).
 
-Notation wptp t := ([∗ list] ef ∈ t, WP ef {{ _, True }})%I.
+Notation wp' E e Φ := (WP e @ p; E {{ Φ }})%I.
+Notation wp e Φ := (wp' ⊤ e Φ).
+Notation wptp t := ([∗ list] ef ∈ t, WP ef @ p; ⊤ {{ _, True }})%I.
 
-Lemma wp_step e1 σ1 e2 σ2 efs Φ :
+Lemma wp_step E e1 σ1 e2 σ2 efs Φ :
   prim_step e1 σ1 e2 σ2 efs →
-  world σ1 ∗ WP e1 {{ Φ }} ==∗ ▷ |==> ◇ (world σ2 ∗ WP e2 {{ Φ }} ∗ wptp efs).
+  world' E σ1 ∗ wp' E e1 Φ ==∗ ▷ |==> ◇ (world' E σ2 ∗ wp' E e2 Φ ∗ wptp efs).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
   rewrite (val_stuck e1 σ1 e2 σ2 efs) // fupd_eq /fupd_def.
@@ -81,8 +85,8 @@ Qed.
 
 Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
   step (e1 :: t1,σ1) (t2, σ2) →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1
-  ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 {{ Φ }} ∗ wptp t2').
+  world σ1 ∗ wp e1 Φ ∗ wptp t1
+  ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ wp e2 Φ ∗ wptp t2').
 Proof.
   iIntros (Hstep) "(HW & He & Ht)".
   destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
@@ -95,9 +99,9 @@ Qed.
 
 Lemma wptp_steps n e1 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢
+  world σ1 ∗ wp e1 Φ ∗ wptp t1 ⊢
   Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ WP e2 {{ Φ }} ∗ wptp t2').
+    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ wp e2 Φ ∗ wptp t2').
 Proof.
   revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=.
   { inversion_clear 1; iIntros "?"; eauto 10. }
@@ -121,7 +125,7 @@ Qed.
 
 Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
   nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) →
-  world σ1 ∗ WP e1 {{ v, ⌜φ v⌝ }} ∗ wptp t1 ⊢ ▷^(S (S n)) ⌜φ v2⌝.
+  world σ1 ∗ wp e1 (λ v, ⌜φ v⌝ ) ∗ wptp t1 ⊢ ▷^(S (S n)) ⌜φ v2⌝.
 Proof.
   intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
   iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
@@ -129,18 +133,20 @@ Proof.
   iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
 Qed.
 
-Lemma wp_safe e σ Φ :
-  world σ -∗ WP e {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
+Lemma wp_safe E e σ Φ :
+  world' E σ -∗ wp' E e Φ ==∗ ▷ ⌜if p then progressive e σ else True⌝.
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
-  destruct (to_val e) as [v|] eqn:?; [eauto 10|].
-  rewrite fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; eauto 10 with iFrame.
+  destruct (to_val e) as [v|] eqn:?.
+  { destruct p; last done. iIntros "!> !> !%". left. by exists v. }
+  rewrite fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
+  destruct p; last done. iIntros "!> !> !%". by right.
 Qed.
 
 Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢
-  ▷^(S (S n)) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
+  world σ1 ∗ wp e1 Φ ∗ wptp t1 ⊢
+  ▷^(S (S n)) ⌜if p then progressive e2 σ2 else True⌝.
 Proof.
   intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
   iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq.
@@ -151,7 +157,7 @@ Qed.
 
 Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 φ Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1
+  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ wp e1 Φ ∗ wptp t1
   ⊢ ▷^(S (S n)) ⌜φ⌝.
 Proof.
   intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
@@ -162,12 +168,12 @@ Proof.
 Qed.
 End adequacy.
 
-Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ :
+Theorem wp_adequacy Σ Λ `{invPreG Σ} p e σ φ :
   (∀ `{Hinv : invG Σ},
      (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ ∗ WP e {{ v, ⌜φ v⌝ }})%I) →
-  adequate e σ φ.
+       stateI σ ∗ WP e @ p; ⊤ {{ v, ⌜φ v⌝ }})%I) →
+  adequate p e σ φ.
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n ?]%rtc_nsteps.
@@ -176,19 +182,19 @@ Proof.
     rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
     iDestruct "Hwp" as (Istate) "[HI Hwp]".
     iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
-  - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
+  - destruct p; last done. intros t2 σ2 e2 _ [n ?]%rtc_nsteps ?.
     eapply (soundness (M:=iResUR Σ) _ (S (S n))).
     iMod wsat_alloc as (Hinv) "[Hw HE]".
     rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
     iDestruct "Hwp" as (Istate) "[HI Hwp]".
-    iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
+    iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate) true); eauto with iFrame.
 Qed.
 
-Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
+Theorem wp_invariance Σ Λ `{invPreG Σ} p e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ},
      (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ1 ∗ WP e {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) →
+       stateI σ1 ∗ WP e @ p; ⊤ {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) →
   rtc step ([e], σ1) (t2, σ2) →
   φ.
 Proof.
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index d8330354d3150be4dd10d200a839b13f77e2584c..af8b796f9036be1a2117ff1f6c3d3926cfa4ebd7 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -127,6 +127,16 @@ Section ectx_language.
     rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
   Qed.
 
+  Lemma ectx_language_strongly_atomic e :
+    (∀ σ e' σ' efs, head_step e σ e' σ' efs → is_Some (to_val e')) →
+    sub_values e →
+    StronglyAtomic e.
+  Proof.
+    intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
+    assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
+    rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
+  Qed.
+
   Lemma head_reducible_prim_step e1 σ1 e2 σ2 efs :
     head_reducible e1 σ1 →
     prim_step e1 σ1 e2 σ2 efs →
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 82275d0f3d9a0e3616de7feb92507027cdb72f97..4dca79e7f37c93c1cf71c51e95db04966468e476 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -12,61 +12,93 @@ Implicit Types v : val.
 Implicit Types e : expr.
 Hint Resolve head_prim_reducible head_reducible_prim_step.
 
-Lemma wp_ectx_bind {E Φ} K e :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+Definition head_progressive (e : expr) (σ : state) :=
+  is_Some(to_val e) ∨ ∃ K e', e = fill K e' ∧ head_reducible e' σ.
+
+Lemma progressive_head_progressive e σ :
+  progressive e σ → head_progressive e σ.
+Proof.
+  case=>[?|Hred]; first by left.
+  right. move: Hred=> [] e' [] σ' [] efs [] K e1' e2' EQ EQ' Hstep. subst.
+  exists K, e1'. split; first done. by exists e2', σ', efs.
+Qed.
+Hint Resolve progressive_head_progressive.
+
+Lemma wp_ectx_bind {p E e} K Φ :
+  WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }} ⊢ WP fill K e @ p; E {{ Φ }}.
 Proof. apply: weakestpre.wp_bind. Qed.
 
-Lemma wp_ectx_bind_inv {E Φ} K e :
-  WP fill K e @ E {{ Φ }} ⊢ WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }}.
+Lemma wp_ectx_bind_inv {p E Φ} K e :
+  WP fill K e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }}.
 Proof. apply: weakestpre.wp_bind_inv. Qed.
 
-Lemma wp_lift_head_step {E Φ} e1 :
+Lemma wp_lift_head_step {p E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+      state_interp σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step E)=>//. iIntros (σ1) "Hσ".
+  iIntros (?) "H". iApply wp_lift_step=>//. iIntros (σ1) "Hσ".
   iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
   iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%".
   iApply "H". by eauto.
 Qed.
 
-Lemma wp_lift_pure_head_step {E E' Φ} e1 :
+Lemma wp_lift_head_stuck E Φ e :
+  to_val e = None →
+  (∀ σ, state_interp σ ={E,∅}=∗ ⌜¬ head_progressive e σ⌝)
+  ⊢ WP e @ E ?{{ Φ }}.
+Proof.
+  iIntros (?) "H". iApply wp_lift_stuck; first done.
+  iIntros (σ) "Hσ". iMod ("H" $! _ with "Hσ") as "%". iModIntro. by auto.
+Qed.
+
+Lemma wp_lift_pure_head_step {p E E' Φ} e1 :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
   (|={E,E'}▷=> ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
-    WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+    WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof using Hinh.
   iIntros (??) "H". iApply wp_lift_pure_step; eauto.
   iApply (step_fupd_wand with "H"); iIntros "H".
   iIntros (????). iApply "H"; eauto.
 Qed.
 
-Lemma wp_lift_atomic_head_step {E Φ} e1 :
+Lemma wp_lift_pure_head_stuck `{Inhabited state} E Φ e :
+  to_val e = None →
+  (∀ K e1 σ1 e2 σ2 efs, e = fill K e1 → ¬ head_step e1 σ1 e2 σ2 efs) →
+  WP e @ E ?{{ Φ }}%I.
+Proof.
+  iIntros (Hnv Hnstep). iApply wp_lift_head_stuck; first done.
+  iIntros (σ) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
+  iModIntro. iPureIntro. case; first by rewrite Hnv; case.
+  move=>[] K [] e1 [] Hfill [] e2 [] σ2 [] efs /= Hstep. exact: Hnstep.
+Qed.
+
+Lemma wp_lift_atomic_head_step {p E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
   iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%". iApply "H"; auto.
 Qed.
 
-Lemma wp_lift_atomic_head_step_no_fork {E Φ} e1 :
+Lemma wp_lift_atomic_head_step_no_fork {p E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
       ⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
-  ⊢ WP e1 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
@@ -74,32 +106,32 @@ Proof.
   iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
 Qed.
 
-Lemma wp_lift_pure_det_head_step {E E' Φ} e1 e2 efs :
+Lemma wp_lift_pure_det_head_step {p E E' Φ} e1 e2 efs :
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs',
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-  (|={E,E'}▷=> WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
 
-Lemma wp_lift_pure_det_head_step_no_fork {E E' Φ} e1 e2 :
+Lemma wp_lift_pure_det_head_step_no_fork {p E E' Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs',
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
-  (|={E,E'}▷=> WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ p; E {{ Φ }}) ⊢ WP e1 @ p; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
 Qed.
 
-Lemma wp_lift_pure_det_head_step_no_fork' {E Φ} e1 e2 :
+Lemma wp_lift_pure_det_head_step_no_fork' {p E Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs',
     head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+  ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
 Proof using Hinh.
-  intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
+  intros. rewrite -[(WP e1 @ _; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
   rewrite -step_fupd_intro //.
 Qed.
 End wp.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index cb110957a6880febd9f6dc2bdbc95021dedaac19..b3a8a4677eb5ae9ed0eea8ccf4a08efe89b609e1 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -3,24 +3,42 @@ From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
+Definition ht `{irisG Λ Σ} (p : bool) (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
-  (□ (P -∗ WP e @ E {{ Φ }}))%I.
-Instance: Params (@ht) 4.
+  (□ (P -∗ WP e @ p; E {{ Φ }}))%I.
+Instance: Params (@ht) 5.
 
-Notation "{{ P } } e @ E {{ Φ } }" := (ht E P%I e%E Φ%I)
+Notation "{{ P } } e @ p ; E {{ Φ } }" := (ht p E P%I e%E Φ%I)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  p ;  E  {{  Φ  } }") : C_scope.
+Notation "{{ P } } e @ E {{ Φ } }" := (ht true E P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
-Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P%I e%E Φ%I)
+Notation "{{ P } } e @ E ? {{ Φ } }" := (ht false E P%I e%E Φ%I)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  E  ? {{  Φ  } }") : C_scope.
+Notation "{{ P } } e {{ Φ } }" := (ht true ⊤ P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : C_scope.
+Notation "{{ P } } e ? {{ Φ } }" := (ht false ⊤ P%I e%E Φ%I)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  ? {{  Φ  } }") : C_scope.
 
-Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e @ p ; E {{ v , Q } }" := (ht p E P%I e%E (λ v, Q)%I)
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  @  p ;  E  {{  v ,  Q  } }") : C_scope.
+Notation "{{ P } } e @ E {{ v , Q } }" := (ht true E P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
-Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht false E P%I e%E (λ v, Q)%I)
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  @  E  ? {{  v ,  Q  } }") : C_scope.
+Notation "{{ P } } e {{ v , Q } }" := (ht true ⊤ P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.
+Notation "{{ P } } e ? {{ v , Q } }" := (ht false ⊤ P%I e%E (λ v, Q)%I)
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  ? {{  v ,  Q  } }") : C_scope.
 
 Section hoare.
 Context `{irisG Λ Σ}.
@@ -29,100 +47,106 @@ Implicit Types Φ Ψ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Import uPred.
 
-Global Instance ht_ne E n :
-  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht E).
+Global Instance ht_ne p E n :
+  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht p E).
 Proof. solve_proper. Qed.
-Global Instance ht_proper E :
-  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht E).
+Global Instance ht_proper p E :
+  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht p E).
 Proof. solve_proper. Qed.
-Lemma ht_mono E P P' Φ Φ' e :
-  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}.
+Lemma ht_mono p E P P' Φ Φ' e :
+  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ p; E {{ Φ' }} ⊢ {{ P }} e @ p; E {{ Φ }}.
 Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
-Global Instance ht_mono' E :
-  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht E).
+Global Instance ht_mono' p E :
+  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht p E).
 Proof. solve_proper. Qed.
 
-Lemma ht_alt E P Φ e : (P ⊢ WP e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
+Lemma ht_alt p E P Φ e : (P ⊢ WP e @ p; E {{ Φ }}) → {{ P }} e @ p; E {{ Φ }}.
 Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.
 
-Lemma ht_val E v : {{ True }} of_val v @ E {{ v', ⌜v = v'⌝ }}.
+Lemma ht_val p E v : {{ True }} of_val v @ p; E {{ v', ⌜v = v'⌝ }}.
 Proof. iIntros "!# _". by iApply wp_value'. Qed.
 
-Lemma ht_vs E P P' Φ Φ' e :
-  (P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
-  ⊢ {{ P }} e @ E {{ Φ }}.
+Lemma ht_vs p E P P' Φ Φ' e :
+  (P ={E}=> P') ∧ {{ P' }} e @ p; E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
+  ⊢ {{ P }} e @ p; E {{ Φ }}.
 Proof.
   iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
   iApply wp_fupd. iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
-Lemma ht_atomic E1 E2 P P' Φ Φ' e :
-  Atomic e →
-  (P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
-  ⊢ {{ P }} e @ E1 {{ Φ }}.
+Lemma ht_atomic p E1 E2 P P' Φ Φ' e :
+  StronglyAtomic e →
+  (P ={E1,E2}=> P') ∧ {{ P' }} e @ p; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
+  ⊢ {{ P }} e @ p; E1 {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ E2); auto.
+  iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ _ E2); auto.
   iMod ("Hvs" with "HP") as "HP". iModIntro.
   iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
   iIntros (v) "Hv". by iApply "HΦ".
 Qed.
 
-Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
-  {{ P }} e @ E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
-  ⊢ {{ P }} K e @ E {{ Φ' }}.
+Lemma ht_bind `{LanguageCtx Λ K} p E P Φ Φ' e :
+  {{ P }} e @ p; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ p; E {{ Φ' }})
+  ⊢ {{ P }} K e @ p; E {{ Φ' }}.
 Proof.
   iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
   iApply (wp_wand with "[HP]"); [by iApply "Hwpe"|].
   iIntros (v) "Hv". by iApply "HwpK".
 Qed.
 
-Lemma ht_mask_weaken E1 E2 P Φ e :
-  E1 ⊆ E2 → {{ P }} e @ E1 {{ Φ }} ⊢ {{ P }} e @ E2 {{ Φ }}.
+Lemma ht_forget_progress E P Φ e :
+  {{ P }} e @ E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
+Proof.
+  by iIntros "#Hwp !# ?"; iApply wp_forget_progress; iApply "Hwp".
+Qed.
+
+Lemma ht_mask_weaken p E1 E2 P Φ e :
+  E1 ⊆ E2 → {{ P }} e @ p; E1 {{ Φ }} ⊢ {{ P }} e @ p; E2 {{ Φ }}.
 Proof.
-  iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono E1 E2); try done.
+  iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono _ E1 E2); try done.
   by iApply "Hwp".
 Qed.
 
-Lemma ht_frame_l E P Φ R e :
-  {{ P }} e @ E {{ Φ }} ⊢ {{ R ∗ P }} e @ E {{ v, R ∗ Φ v }}.
+Lemma ht_frame_l p E P Φ R e :
+  {{ P }} e @ p; E {{ Φ }} ⊢ {{ R ∗ P }} e @ p; E {{ v, R ∗ Φ v }}.
 Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.
 
-Lemma ht_frame_r E P Φ R e :
-  {{ P }} e @ E {{ Φ }} ⊢ {{ P ∗ R }} e @ E {{ v, Φ v ∗ R }}.
+Lemma ht_frame_r p E P Φ R e :
+  {{ P }} e @ p; E {{ Φ }} ⊢ {{ P ∗ R }} e @ p; E {{ v, Φ v ∗ R }}.
 Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
 
-Lemma ht_frame_step_l E1 E2 P R1 R2 e Φ :
+Lemma ht_frame_step_l p E1 E2 P R1 R2 e Φ :
   to_val e = None → E2 ⊆ E1 →
-  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }}
-  ⊢ {{ R1 ∗ P }} e @ E1 {{ λ v, R2 ∗ Φ v }}.
+  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ p; E2 {{ Φ }}
+  ⊢ {{ R1 ∗ P }} e @ p; E1 {{ λ v, R2 ∗ Φ v }}.
 Proof.
   iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
-  iApply (wp_frame_step_l E1 E2); try done.
+  iApply (wp_frame_step_l _ E1 E2); try done.
   iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
 Qed.
 
-Lemma ht_frame_step_r E1 E2 P R1 R2 e Φ :
+Lemma ht_frame_step_r p E1 E2 P R1 R2 e Φ :
   to_val e = None → E2 ⊆ E1 →
-  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }}
-  ⊢ {{ P ∗ R1 }} e @ E1 {{ λ v, Φ v ∗ R2 }}.
+  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ p; E2 {{ Φ }}
+  ⊢ {{ P ∗ R1 }} e @ p; E1 {{ λ v, Φ v ∗ R2 }}.
 Proof.
   iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
-  iApply (wp_frame_step_r E1 E2); try done.
+  iApply (wp_frame_step_r _ E1 E2); try done.
   iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
 Qed.
 
-Lemma ht_frame_step_l' E P R e Φ :
+Lemma ht_frame_step_l' p E P R e Φ :
   to_val e = None →
-  {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ E {{ v, R ∗ Φ v }}.
+  {{ P }} e @ p; E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ p; E {{ v, R ∗ Φ v }}.
 Proof.
   iIntros (?) "#Hwp !# [HR HP]".
   iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
 Qed.
 
-Lemma ht_frame_step_r' E P Φ R e :
+Lemma ht_frame_step_r' p E P Φ R e :
   to_val e = None →
-  {{ P }} e @ E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ E {{ v, Φ v ∗ R }}.
+  {{ P }} e @ p; E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ p; E {{ v, Φ v ∗ R }}.
 Proof.
   iIntros (?) "#Hwp !# [HP HR]".
   iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index d600c5e7548eb0a1d2ea70d1445528cd378491be..af3357fe1753d98205ab405938742058a7fc6d6c 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -51,6 +51,8 @@ Section language.
     ∃ e' σ' efs, prim_step e σ e' σ' efs.
   Definition irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ e' σ' efs, ¬prim_step e σ e' σ' efs.
+  Definition progressive (e : expr Λ) (σ : state Λ) :=
+    is_Some (to_val e) ∨ reducible e σ.
 
   (* This (weak) form of atomicity is enough to open invariants when WP ensures
      safety, i.e., programs never can get stuck.  We have an example in
@@ -82,6 +84,8 @@ Section language.
   Proof. unfold reducible, irreducible. naive_solver. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
+  Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ.
+  Proof. intros [??] ??? ?%val_stuck. by destruct (to_val e). Qed.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 41edd498d69b7b9a31894f40311a389b84e66779..c013ded44f00ebbdd17a39842bb14f9494c5053c 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -11,22 +11,36 @@ Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
-Lemma wp_lift_step E Φ e1 :
+Lemma wp_lift_step p E Φ e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
     ⌜reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
-Proof. by rewrite wp_unfold /wp_pre=> ->. Qed.
+      state_interp σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof.
+  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1) "Hσ".
+  iMod ("H" with "Hσ") as "(%&?)". iModIntro. iSplit. by destruct p. done.
+Qed.
+
+Lemma wp_lift_stuck E Φ e :
+  to_val e = None →
+  (∀ σ, state_interp σ ={E,∅}=∗ ⌜¬ progressive e σ⌝)
+  ⊢ WP e @ E ?{{ Φ }}.
+Proof.
+  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1) "Hσ".
+  iMod ("H" with "Hσ") as "Hstuck". iDestruct "Hstuck" as %Hstuck.
+  iModIntro. iSplit; first done. iIntros "!>" (e2 σ2 efs) "%". exfalso.
+  apply Hstuck. right. by exists e2, σ2, efs.
+Qed.
 
 (** Derived lifting lemmas. *)
-Lemma wp_lift_pure_step `{Inhabited (state Λ)} E E' Φ e1 :
+Lemma wp_lift_pure_step `{Inhabited (state Λ)} p E E' Φ e1 :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
   (|={E,E'}▷=> ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
-    WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+    WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
   { eapply reducible_not_val, (Hsafe inhabitant). }
@@ -37,18 +51,29 @@ Proof.
   iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
 Qed.
 
+Lemma wp_lift_pure_stuck `{Inhabited (state Λ)} E Φ e :
+  (∀ σ, ¬ progressive e σ) →
+  True ⊢ WP e @ E ?{{ Φ }}.
+Proof.
+  iIntros (Hstuck) "_". iApply wp_lift_stuck.
+  - destruct(to_val e) as [v|] eqn:He; last done.
+    exfalso. apply (Hstuck inhabitant). left. by exists v.
+  - iIntros (σ) "_". iMod (fupd_intro_mask' E ∅) as "_".
+    by set_solver. by auto.
+Qed.
+
 (* Atomic steps don't need any mask-changing business here, one can
    use the generic lemmas here. *)
-Lemma wp_lift_atomic_step {E Φ} e1 :
+Lemma wp_lift_atomic_step {p E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
     ⌜reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step E _ e1)=>//; iIntros (σ1) "Hσ1".
+  iIntros (?) "H". iApply (wp_lift_step p E _ e1)=>//; iIntros (σ1) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
   iModIntro; iNext; iIntros (e2 σ2 efs) "%". iMod "Hclose" as "_".
@@ -57,13 +82,13 @@ Proof.
   by iApply wp_value.
 Qed.
 
-Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E E' Φ} e1 e2 efs :
+Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {p E E' Φ} e1 e2 efs :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-  (|={E,E'}▷=> WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
-  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E); try done.
+  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step p E); try done.
   { by intros; eapply Hpuredet. }
   iApply (step_fupd_wand with "H"); iIntros "H".
   by iIntros (e' efs' σ (_&->&->)%Hpuredet).
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 1c3a8d3e34439ae1684659138937e0dd672729dd..dc9bd83a2e127f77115db9f4f94f6c0c452c5963 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -39,9 +39,9 @@ Instance: Params (@ownP) 3.
 
 
 (* Adequacy *)
-Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} e σ φ :
-  (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e {{ v, ⌜φ v⌝ }}) →
-  adequate e σ φ.
+Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} p e σ φ :
+  (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e @ p; ⊤ {{ v, ⌜φ v⌝ }}) →
+  adequate p e σ φ.
 Proof.
   intros Hwp. apply (wp_adequacy Σ _).
   iIntros (?) "". iMod (own_alloc (● (Excl' (σ : leibnizC _)) ⋅ ◯ (Excl' σ)))
@@ -50,13 +50,13 @@ Proof.
   iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP.
 Qed.
 
-Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ :
+Theorem ownP_invariance Σ `{ownPPreG Λ Σ} p e σ1 t2 σ2 φ :
   (∀ `{ownPG Λ Σ},
-    ownP σ1 ={⊤}=∗ WP e {{ _, True }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
+    ownP σ1 ={⊤}=∗ WP e @ p; ⊤ {{ _, True }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
   rtc step ([e], σ1) (t2, σ2) →
   φ σ2.
 Proof.
-  intros Hwp Hsteps. eapply (wp_invariance Σ Λ e σ1 t2 σ2 _)=> //.
+  intros Hwp Hsteps. eapply (wp_invariance Σ Λ p e σ1 t2 σ2 _)=> //.
   iIntros (?) "". iMod (own_alloc (● (Excl' (σ1 : leibnizC _)) ⋅ ◯ (Excl' σ1)))
     as (γσ) "[Hσ Hσf]"; first done.
   iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))). iFrame "Hσ".
@@ -78,11 +78,11 @@ Section lifting.
   Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) Σ _ σ).
   Proof. rewrite /ownP; apply _. Qed.
 
-  Lemma ownP_lift_step E Φ e1 :
+  Lemma ownP_lift_step p E Φ e1 :
     (|={E,∅}=> ∃ σ1, ⌜reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
       ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-            ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+            ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
     iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
     - apply of_to_val in EQe1 as <-. iApply fupd_wp.
@@ -99,12 +99,26 @@ Section lifting.
       iFrame "Hσ". iApply ("H" with "[]"); eauto.
   Qed.
 
-  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
+  Lemma ownP_lift_stuck E Φ e :
+    (|={E,∅}=> ∃ σ, ⌜¬ progressive e σ⌝ ∗ ▷ ownP σ)
+    ⊢ WP e @ E ?{{ Φ }}.
+  Proof.
+    iIntros "H". destruct (to_val e) as [v|] eqn:EQe.
+    - apply of_to_val in EQe as <-; iApply fupd_wp.
+      iMod "H" as (σ1) "[#H _]"; iDestruct "H" as %Hstuck; exfalso.
+      by apply Hstuck; left; rewrite to_of_val; exists v.
+    - iApply wp_lift_stuck; [done|]; iIntros (σ1) "Hσ".
+      iMod "H" as (σ1') "(% & >Hσf)"; rewrite /ownP.
+      by iDestruct (own_valid_2 with "Hσ Hσf")
+        as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+  Qed.
+
+  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} p E Φ e1 :
     (∀ σ1, reducible e1 σ1) →
     (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
     (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
-      WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+      WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
     iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
     { eapply reducible_not_val, (Hsafe inhabitant). }
@@ -115,13 +129,13 @@ Section lifting.
   Qed.
 
   (** Derived lifting lemmas. *)
-  Lemma ownP_lift_atomic_step {E Φ} e1 σ1 :
+  Lemma ownP_lift_atomic_step {p E Φ} e1 σ1 :
     reducible e1 σ1 →
     (▷ ownP σ1 ∗ ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
-    iIntros (?) "[Hσ H]". iApply (ownP_lift_step E _ e1).
+    iIntros (?) "[Hσ H]". iApply ownP_lift_step.
     iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iModIntro.
     iExists σ1. iFrame "Hσ"; iSplit; eauto.
     iNext; iIntros (e2 σ2 efs) "% Hσ".
@@ -130,28 +144,47 @@ Section lifting.
     iMod "Hclose". iApply wp_value; auto using to_of_val. done.
   Qed.
 
-  Lemma ownP_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
+  Lemma ownP_lift_atomic_det_step {p E Φ e1} σ1 v2 σ2 efs :
     reducible e1 σ1 →
     (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
                      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
     ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
-      Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+      Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
-    iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (ownP_lift_atomic_step _ σ1); try done.
+    iIntros (? Hdet) "[Hσ1 Hσ2]". iApply ownP_lift_atomic_step; try done.
     iFrame. iNext. iIntros (e2' σ2' efs') "% Hσ2'".
     edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
   Qed.
 
-  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
+  Lemma ownP_lift_atomic_det_step_no_fork {p E e1} σ1 v2 σ2 :
+    reducible e1 σ1 →
+    (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
+      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
+    {{{ ▷ ownP σ1 }}} e1 @ p; E {{{ RET v2; ownP σ2 }}}.
+  Proof.
+    intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
+    rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
+  Qed.
+
+  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {p E Φ} e1 e2 efs :
     (∀ σ1, reducible e1 σ1) →
     (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-    ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
-    iIntros (? Hpuredet) "?". iApply (ownP_lift_pure_step E); try done.
+    iIntros (? Hpuredet) "?". iApply ownP_lift_pure_step; try done.
     by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
   Qed.
+
+  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {p E Φ} e1 e2 :
+    to_val e1 = None →
+    (∀ σ1, reducible e1 σ1) →
+    (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
+  Proof.
+    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
+  Qed.
 End lifting.
 
 Section ectx_lifting.
@@ -162,73 +195,66 @@ Section ectx_lifting.
   Implicit Types e : expr.
   Hint Resolve head_prim_reducible head_reducible_prim_step.
 
-  Lemma ownP_lift_head_step E Φ e1 :
+  Lemma ownP_lift_head_step p E Φ e1 :
     (|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
       ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-            ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+            ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
-    iIntros "H". iApply (ownP_lift_step E); try done.
+    iIntros "H". iApply (ownP_lift_step p E); try done.
     iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1.
     iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
     iApply ("Hwp" with "[]"); eauto.
   Qed.
 
-  Lemma ownP_lift_pure_head_step E Φ e1 :
+  Lemma ownP_lift_pure_head_step p E Φ e1 :
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
     (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
-      WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+      WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
   Proof using Hinh.
     iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
     iIntros (????). iApply "H". eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_head_step {E Φ} e1 σ1 :
+  Lemma ownP_lift_atomic_head_step {p E Φ} e1 σ1 :
     head_reducible e1 σ1 →
     ▷ ownP σ1 ∗ ▷ (∀ e2 σ2 efs,
     ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
   Proof.
     iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto. iFrame. iNext.
     iIntros (???) "% ?". iApply ("H" with "[]"); eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
+  Lemma ownP_lift_atomic_det_head_step {p E Φ e1} σ1 v2 σ2 efs :
     head_reducible e1 σ1 →
     (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
       σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
-    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
   Proof. eauto using ownP_lift_atomic_det_step. Qed.
 
-  Lemma ownP_lift_atomic_det_head_step_no_fork {E e1} σ1 v2 σ2 :
+  Lemma ownP_lift_atomic_det_head_step_no_fork {p E e1} σ1 v2 σ2 :
     head_reducible e1 σ1 →
     (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
       σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
-    {{{ ▷ ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
-  Proof.
-    intros. rewrite -(ownP_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
-    rewrite /= right_id. by apply uPred.wand_intro_r.
-  Qed.
+    {{{ ▷ ownP σ1 }}} e1 @ p; E {{{ RET v2; ownP σ2 }}}.
+  Proof. eauto using ownP_lift_atomic_det_step_no_fork. Qed.
 
-  Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
+  Lemma ownP_lift_pure_det_head_step {p E Φ} e1 e2 efs :
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-    ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
-  Proof using Hinh.
-    intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_step; eauto.
-  Qed.
+    ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
+  Proof using Hinh. eauto using ownP_lift_pure_det_step. Qed.
 
-  Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
+  Lemma ownP_lift_pure_det_head_step_no_fork {p E Φ} e1 e2 :
     to_val e1 = None →
     (∀ σ1, head_reducible e1 σ1) →
     (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
-    ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
-  Proof using Hinh.
-    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
-  Qed.
+    ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
+  Proof using Hinh. eauto using ownP_lift_pure_det_step_no_fork. Qed.
 End ectx_lifting.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 32b98d8ffa0e467c906d2cc02bf94778174cf49c..b205ee3995218edc155578a5ccccbea508f96246 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -12,84 +12,156 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
 Definition wp_pre `{irisG Λ Σ}
-    (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
-    coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
+    (wp : bool -c> coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
+    bool -c> coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ p E e1 Φ,
   match to_val e1 with
   | Some v => |={E}=> Φ v
   | None => ∀ σ1,
-     state_interp σ1 ={E,∅}=∗ ⌜reducible e1 σ1⌝ ∗
+     state_interp σ1 ={E,∅}=∗ ⌜if p then reducible e1 σ1 else True⌝ ∗
      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
-       state_interp σ2 ∗ wp E e2 Φ ∗
-       [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
+       state_interp σ2 ∗ wp p E e2 Φ ∗
+       [∗ list] ef ∈ efs, wp p ⊤ ef (λ _, True)
   end%I.
 
 Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
 Proof.
-  rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
+  rewrite /wp_pre=> n wp wp' Hwp p E e1 Φ.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
 Definition wp_def `{irisG Λ Σ} :
-  coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint wp_pre.
+  bool → coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint wp_pre.
 Definition wp_aux : seal (@wp_def). by eexists. Qed.
 Definition wp := unseal wp_aux.
 Definition wp_eq : @wp = @wp_def := seal_eq wp_aux.
 
-Arguments wp {_ _ _} _ _%E _.
-Instance: Params (@wp) 5.
+Arguments wp {_ _ _} _ _ _%E _.
+Instance: Params (@wp) 6.
 
-Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
+Notation "'WP' e @ p ; E {{ Φ } }" := (wp p E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  p ;  E  {{  Φ  } } ']'") : uPred_scope.
+Notation "'WP' e @ E {{ Φ } }" := (wp true E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' @  E  {{  Φ  } } ']'") : uPred_scope.
-Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
+Notation "'WP' e @ E ? {{ Φ } }" := (wp false E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  E  ? {{  Φ  } } ']'") : uPred_scope.
+Notation "'WP' e {{ Φ } }" := (wp true ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : uPred_scope.
+Notation "'WP' e ? {{ Φ } }" := (wp false ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' ? {{  Φ  } } ']'") : uPred_scope.
 
-Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
+Notation "'WP' e @ p ; E {{ v , Q } }" := (wp p E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' @  p ;  E  {{  v ,  Q  } } ']'") : uPred_scope.
+Notation "'WP' e @ E {{ v , Q } }" := (wp true E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' @  E  {{  v ,  Q  } } ']'") : uPred_scope.
-Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
+Notation "'WP' e @ E ? {{ v , Q } }" := (wp false E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' @  E  ? {{  v ,  Q  } } ']'") : uPred_scope.
+Notation "'WP' e {{ v , Q } }" := (wp true ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' {{  v ,  Q  } } ']'") : uPred_scope.
+Notation "'WP' e ? {{ v , Q } }" := (wp false ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' ? {{  v ,  Q  } } ']'") : uPred_scope.
 
 (* Texan triples *)
+Notation "'{{{' P } } } e @ p ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ p; E {{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  @  p ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : uPred_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q } } }") : uPred_scope.
 Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (□ ∀ Φ,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})%I
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  {{{  x .. y ,   RET  pat ;  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  ? {{{  x .. y ,   RET  pat ;  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ p ; E {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ p; E {{ Φ }})%I
+    (at level 20,
+     format "{{{  P  } } }  e  @  p ;  E  {{{  RET  pat ;  Q } } }") : uPred_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})%I
     (at level 20,
      format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})%I
+    (at level 20,
+     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q } } }") : uPred_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
   (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})%I
     (at level 20,
      format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : uPred_scope.
+Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})%I
+    (at level 20,
+     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q } } }") : uPred_scope.
 
+Notation "'{{{' P } } } e @ p ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ p; E {{ Φ }})
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  @  p ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
 Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
+Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  @  E  ? {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
 Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _,
       P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})
     (at level 20, x closed binder, y closed binder,
      format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
+Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  ? {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
+Notation "'{{{' P } } } e @ p ; E {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ p; E {{ Φ }})
+    (at level 20,
+     format "{{{  P  } } }  e  @  p ;  E  {{{  RET  pat ;  Q } } }") : C_scope.
 Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})
     (at level 20,
      format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : C_scope.
+Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})
+    (at level 20,
+     format "{{{  P  } } }  e  @  E  ? {{{  RET  pat ;  Q } } }") : C_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})
     (at level 20,
      format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : C_scope.
+Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})
+    (at level 20,
+     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q } } }") : C_scope.
 
 Section wp.
 Context `{irisG Λ Σ}.
@@ -99,11 +171,11 @@ Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 
 (* Weakest pre *)
-Lemma wp_unfold E e Φ : WP e @ E {{ Φ }} ⊣⊢ wp_pre wp E e Φ.
+Lemma wp_unfold p E e Φ : WP e @ p; E {{ Φ }} ⊣⊢ wp_pre wp p E e Φ.
 Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.
 
-Global Instance wp_ne E e n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ E e).
+Global Instance wp_ne p E e n :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ p E e).
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
   rewrite !wp_unfold /wp_pre.
@@ -113,19 +185,19 @@ Proof.
   do 17 (f_contractive || f_equiv). apply IH; first lia.
   intros v. eapply dist_le; eauto with omega.
 Qed.
-Global Instance wp_proper E e :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ _ E e).
+Global Instance wp_proper p E e :
+  Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ _ p E e).
 Proof.
   by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
 Qed.
 
-Lemma wp_value' E Φ v : Φ v ⊢ WP of_val v @ E {{ Φ }}.
+Lemma wp_value' p E Φ v : Φ v ⊢ WP of_val v @ p; E {{ Φ }}.
 Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
-Lemma wp_value_inv E Φ v : WP of_val v @ E {{ Φ }} ={E}=∗ Φ v.
+Lemma wp_value_inv p E Φ v : WP of_val v @ p; E {{ Φ }} ={E}=∗ Φ v.
 Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
 
-Lemma wp_strong_mono E1 E2 e Φ Ψ :
-  E1 ⊆ E2 → (∀ v, Φ v ={E2}=∗ Ψ v) ∗ WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Ψ }}.
+Lemma wp_strong_mono p E1 E2 e Φ Ψ :
+  E1 ⊆ E2 → (∀ v, Φ v ={E2}=∗ Ψ v) ∗ WP e @ p; E1 {{ Φ }} ⊢ WP e @ p; E2 {{ Ψ }}.
 Proof.
   iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
@@ -137,128 +209,141 @@ Proof.
   iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
 Qed.
 
-Lemma fupd_wp E e Φ : (|={E}=> WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Φ }}.
+Lemma wp_forget_progress E e Φ : WP e @ E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
+Proof.
+  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
+  destruct (to_val e) as [v|]; first iExact "H".
+  iIntros (σ1) "Hσ". iMod ("H" with "Hσ") as "[#Hred H]". iModIntro.
+  iSplit; first done. iNext. iIntros (e2 σ2 efs) "#Hstep".
+  iMod ("H" with "Hstep") as "($ & He2 & Hefs)". iModIntro.
+  iSplitL "He2"; first by iApply ("IH" with "He2"). iClear "Hred Hstep".
+  induction efs as [|ef efs IH]; first by iApply big_sepL_nil.
+  rewrite !big_sepL_cons. iDestruct "Hefs" as "(Hef & Hefs)".
+  iSplitL "Hef". by iApply ("IH" with "Hef"). exact: IH. 
+Qed.
+
+Lemma fupd_wp p E e Φ : (|={E}=> WP e @ p; E {{ Φ }}) ⊢ WP e @ p; E {{ Φ }}.
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
   { by iMod "H". }
   iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
 Qed.
-Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
-Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
+Lemma wp_fupd p E e Φ : WP e @ p; E {{ v, |={E}=> Φ v }} ⊢ WP e @ p; E {{ Φ }}.
+Proof. iIntros "H". iApply (wp_strong_mono p E); try iFrame; auto. Qed.
 
-Lemma wp_atomic E1 E2 e Φ :
-  Atomic e →
-  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
+Lemma wp_atomic p E1 E2 e Φ :
+  StronglyAtomic e →
+  (|={E1,E2}=> WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ p; E1 {{ Φ }}.
 Proof.
   iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
-  destruct (to_val e) as [v|] eqn:He.
+  destruct (to_val e) as [v|].
   { by iDestruct "H" as ">>> $". }
   iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
   iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" with "[//]") as "(Hphy & H & $)".
-  rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
-  - iDestruct "H" as ">> $". eauto with iFrame.
-  - iMod ("H" with "[$]") as "[H _]".
-    iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hatomic _ _ _ _ Hstep).
+  destruct (Hatomic _ _ _ _ Hstep) as [v <-%of_to_val].
+  iMod ("H" with "[#]") as "($ & H & $)"; first done.
+  iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
 Qed.
 
-Lemma wp_step_fupd E1 E2 e P Φ :
+Lemma wp_step_fupd p E1 E2 e P Φ :
   to_val e = None → E2 ⊆ E1 →
-  (|={E1,E2}▷=> P) -∗ WP e @ E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ E1 {{ Φ }}.
+  (|={E1,E2}▷=> P) -∗ WP e @ p; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ p; E1 {{ Φ }}.
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
   iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
   iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
-  iMod "HR". iModIntro. iApply (wp_strong_mono E2); first done.
+  iMod "HR". iModIntro. iApply (wp_strong_mono p E2); first done.
   iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
 Qed.
 
-Lemma wp_bind K `{!LanguageCtx Λ K} E e Φ :
-  WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} ⊢ WP K e @ E {{ Φ }}.
+Lemma wp_bind K `{!LanguageCtx Λ K} p E e Φ :
+  WP e @ p; E {{ v, WP K (of_val v) @ p; E {{ Φ }} }} ⊢ WP K e @ p; E {{ Φ }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by iApply fupd_wp. }
   rewrite wp_unfold /wp_pre fill_not_val //.
   iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
-  { iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
+  { iPureIntro. destruct p; last done.
+    unfold reducible in *. naive_solver eauto using fill_step. }
   iNext; iIntros (e2 σ2 efs Hstep).
   destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
   iMod ("H" $! e2' σ2 efs with "[//]") as "($ & H & $)".
   by iApply "IH".
 Qed.
 
-Lemma wp_bind_inv K `{!LanguageCtx Λ K} E e Φ :
-  WP K e @ E {{ Φ }} ⊢ WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}.
+Lemma wp_bind_inv K `{!LanguageCtx Λ K} p E e Φ :
+  WP K e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, WP K (of_val v) @ p; E {{ Φ }} }}.
 Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
   rewrite fill_not_val //.
   iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
-  { eauto using reducible_fill. }
+  { destruct p; eauto using reducible_fill. }
   iNext; iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! (K e2) σ2 efs with "[]") as "($ & H & $)"; eauto using fill_step.
   by iApply "IH".
 Qed.
 
 (** * Derived rules *)
-Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
+Lemma wp_mono p E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ Ψ }}.
 Proof.
-  iIntros (HΦ) "H"; iApply (wp_strong_mono E E); auto.
+  iIntros (HΦ) "H"; iApply (wp_strong_mono p E E); auto.
   iIntros "{$H}" (v) "?". by iApply HΦ.
 Qed.
-Lemma wp_mask_mono E1 E2 e Φ : E1 ⊆ E2 → WP e @ E1 {{ Φ }} ⊢ WP e @ E2 {{ Φ }}.
-Proof. iIntros (?) "H"; iApply (wp_strong_mono E1 E2); auto. iFrame; eauto. Qed.
-Global Instance wp_mono' E e :
-  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ E e).
+Lemma wp_mask_mono p E1 E2 e Φ : E1 ⊆ E2 → WP e @ p; E1 {{ Φ }} ⊢ WP e @ p; E2 {{ Φ }}.
+Proof. iIntros (?) "H"; iApply (wp_strong_mono p E1 E2); auto. iFrame; eauto. Qed.
+Global Instance wp_mono' p E e :
+  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ p E e).
 Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
 
-Lemma wp_value E Φ e v `{!IntoVal e v} : Φ v ⊢ WP e @ E {{ Φ }}.
+Lemma wp_value p E Φ e v `{!IntoVal e v} : Φ v ⊢ WP e @ p; E {{ Φ }}.
 Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
-Lemma wp_value_fupd' E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ E {{ Φ }}.
+Lemma wp_value_fupd' p E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ p; E {{ Φ }}.
 Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
-Lemma wp_value_fupd E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) ⊢ WP e @ E {{ Φ }}.
+Lemma wp_value_fupd p E Φ e v `{!IntoVal e v} :
+  (|={E}=> Φ v) ⊢ WP e @ p; E {{ Φ }}.
 Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
 
-Lemma wp_frame_l E e Φ R : R ∗ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ∗ Φ v }}.
-Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.
-Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }} ∗ R ⊢ WP e @ E {{ v, Φ v ∗ R }}.
-Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.
+Lemma wp_frame_l p E e Φ R : R ∗ WP e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, R ∗ Φ v }}.
+Proof. iIntros "[??]". iApply (wp_strong_mono p E E _ Φ); try iFrame; eauto. Qed.
+Lemma wp_frame_r p E e Φ R : WP e @ p; E {{ Φ }} ∗ R ⊢ WP e @ p; E {{ v, Φ v ∗ R }}.
+Proof. iIntros "[??]". iApply (wp_strong_mono p E E _ Φ); try iFrame; eauto. Qed.
 
-Lemma wp_frame_step_l E1 E2 e Φ R :
+Lemma wp_frame_step_l p E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
-  (|={E1,E2}▷=> R) ∗ WP e @ E2 {{ Φ }} ⊢ WP e @ E1 {{ v, R ∗ Φ v }}.
+  (|={E1,E2}▷=> R) ∗ WP e @ p; E2 {{ Φ }} ⊢ WP e @ p; 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 E1 E2 e Φ R :
+Lemma wp_frame_step_r p E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
-  WP e @ E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ WP e @ E1 {{ v, Φ v ∗ R }}.
+  WP e @ p; E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ WP e @ p; E1 {{ v, Φ v ∗ R }}.
 Proof.
-  rewrite [(WP _ @ _ {{ _ }} ∗ _)%I]comm; setoid_rewrite (comm _ _ R).
+  rewrite [(WP _ @ _; _ {{ _ }} ∗ _)%I]comm; setoid_rewrite (comm _ _ R).
   apply wp_frame_step_l.
 Qed.
-Lemma wp_frame_step_l' E e Φ R :
-  to_val e = None → ▷ R ∗ WP e @ E {{ Φ }} ⊢ WP e @ E {{ v, R ∗ Φ v }}.
-Proof. iIntros (?) "[??]". iApply (wp_frame_step_l E E); try iFrame; eauto. Qed.
-Lemma wp_frame_step_r' E e Φ R :
-  to_val e = None → WP e @ E {{ Φ }} ∗ ▷ R ⊢ WP e @ E {{ v, Φ v ∗ R }}.
-Proof. iIntros (?) "[??]". iApply (wp_frame_step_r E E); try iFrame; eauto. Qed.
+Lemma wp_frame_step_l' p E e Φ R :
+  to_val e = None → ▷ R ∗ WP e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, R ∗ Φ v }}.
+Proof. iIntros (?) "[??]". iApply (wp_frame_step_l p E E); try iFrame; eauto. Qed.
+Lemma wp_frame_step_r' p E e Φ R :
+  to_val e = None → WP e @ p; E {{ Φ }} ∗ ▷ R ⊢ WP e @ p; E {{ v, Φ v ∗ R }}.
+Proof. iIntros (?) "[??]". iApply (wp_frame_step_r p E E); try iFrame; eauto. Qed.
 
-Lemma wp_wand E e Φ Ψ :
-  WP e @ E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ E {{ Ψ }}.
+Lemma wp_wand p E e Φ Ψ :
+  WP e @ p; E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ p; E {{ Ψ }}.
 Proof.
-  iIntros "Hwp H". iApply (wp_strong_mono E); auto.
+  iIntros "Hwp H". iApply (wp_strong_mono p E); auto.
   iIntros "{$Hwp}" (?) "?". by iApply "H".
 Qed.
-Lemma wp_wand_l E e Φ Ψ :
-  (∀ v, Φ v -∗ Ψ v) ∗ WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
+Lemma wp_wand_l p E e Φ Ψ :
+  (∀ v, Φ v -∗ Ψ v) ∗ WP e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ Ψ }}.
 Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
-Lemma wp_wand_r E e Φ Ψ :
-  WP e @ E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ E {{ Ψ }}.
+Lemma wp_wand_r p E e Φ Ψ :
+  WP e @ p; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ p; E {{ Ψ }}.
 Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
 End wp.
 
@@ -268,25 +353,25 @@ Section proofmode_classes.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : val Λ → iProp Σ.
 
-  Global Instance frame_wp p E e R Φ Ψ :
-    (∀ v, Frame p R (Φ v) (Ψ v)) → Frame p R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
+  Global Instance frame_wp p p' E e R Φ Ψ :
+    (∀ v, Frame p' R (Φ v) (Ψ v)) → Frame p' R (WP e @ p; E {{ Φ }}) (WP e @ p; E {{ Ψ }}).
   Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
 
-  Global Instance is_except_0_wp E e Φ : IsExcept0 (WP e @ E {{ Φ }}).
+  Global Instance is_except_0_wp p E e Φ : IsExcept0 (WP e @ p; E {{ Φ }}).
   Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
 
-  Global Instance elim_modal_bupd_wp E e P Φ :
-    ElimModal (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+  Global Instance elim_modal_bupd_wp p E e P Φ :
+    ElimModal (|==> P) P (WP e @ p; E {{ Φ }}) (WP e @ p; E {{ Φ }}).
   Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
 
-  Global Instance elim_modal_fupd_wp E e P Φ :
-    ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+  Global Instance elim_modal_fupd_wp p E e P Φ :
+    ElimModal (|={E}=> P) P (WP e @ p; E {{ Φ }}) (WP e @ p; E {{ Φ }}).
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
 
   (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
   Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
-    Atomic e →
+    StronglyAtomic e →
     ElimModal (|={E1,E2}=> P) P
-            (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
+            (WP e @ p; E1 {{ Φ }}) (WP e @ p; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
 End proofmode_classes.
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 51681a36571459c2906a42b24794d8fbce80cfbf..598ec56105e844be72651ac43c8b85b20c7fd7c7 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -86,5 +86,5 @@ Section LiftingTests.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
-Lemma heap_e_adequate σ : adequate heap_e σ (= #2).
+Lemma heap_e_adequate σ : adequate true heap_e σ (= #2).
 Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 6834c5c5e3928fd626f706c6eda0a8daf90d433e..0922cd5bbb09d343c208b52172a4c0fb378479f5 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -101,7 +101,7 @@ update modalities (which we did not cover in the paper). Normally we use these
 mask changing update modalities directly in our proofs, but in this file we use
 the first prove the rule as a lemma, and then use that. *)
 Lemma wp_inv_open `{irisG Λ Σ} N E P e Φ :
-  nclose N ⊆ E → Atomic e →
+  nclose N ⊆ E → StronglyAtomic e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".