diff --git a/CHANGELOG.md b/CHANGELOG.md
index d8d228dc633630c261d424f221d7719d3ee6db05..e5a006f462aad96148893a528d5d342848236947 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,14 @@ Changes in and extensions of the theory:
 * Constructions for least and greatest fixed points over monotone predicates
   (defined in the logic of Iris using impredicative quantification).
 * Add a proof of the inverse of `wp_bind`.
+* Support verifying code that might get stuck by distinguishing "non-stuck"
+  vs. "(potentially) stuck" weakest preconditions. (See
+  [Swasey et al., OOPSLA '17] for examples.) The non-stuck `WP e @ E {{ Φ }}`
+  ensures that, as `e` runs, it does not get stuck. The stuck `WP e @ E ?{{ Φ
+  }}` ensures that, as usual, all invariants are preserved while `e` runs, but
+  it permits execution to get stuck. The former implies the latter. The full
+  judgment is `WP e @ s; E {{ Φ }}`, where non-stuck WP uses *stuckness bit* `s
+  = NotStuck` while stuck WP uses `s = MaybeStuck`.
 
 Changes in Coq:
 
@@ -100,6 +108,10 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
 * Move the `prelude` folder to its own project: std++
 * The rules `internal_eq_rewrite` and `internal_eq_rewrite_contractive` are now
   stated in the logic, i.e. they are `iApply` friendly.
+* Restore the original, stronger notion of atomicity alongside the weaker
+  notion. These are `Atomic a e` where the stuckness bit `s` indicates whether
+  expression `e` is weakly (`a = WeaklyAtomic`) or strongly (`a =
+  StronglyAtomic`) atomic.
 
 ## Iris 3.0.0 (released 2017-01-11)
 
diff --git a/naming.txt b/naming.txt
index 191c1664e7b820563ec755f3554a0cf746ce9e0f..ed87ef4c324a8540f23e23e8147d0c83fc2a8646 100644
--- a/naming.txt
+++ b/naming.txt
@@ -17,7 +17,7 @@ o
 p
 q
 r : iRes = resources
-s : state (STSs)
+s : state (STSs), stuckness bits
 t
 u
 v : val = values of language
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index a184a59657dfd639315dd8aa4416f314160e0bd5..51529438b392a93878e3f21458f0be2b7982d7fd 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -14,9 +14,9 @@ Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. solve_inG. Qed.
 
-Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
-  (∀ `{heapG Σ}, WP e {{ v, ⌜φ v⌝ }}%I) →
-  adequate e σ φ.
+Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
+  (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) →
+  adequate s e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
   iMod (gen_heap_init σ) as (?) "Hh".
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 2adfe9d5e639485dc7a4f83cb51dbd06d91b859d..04abfc8b22f0b9368f99fe7cd30d07aa4209eb06 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -47,7 +47,7 @@ Ltac inv_head_step :=
      inversion H; subst; clear H
   end.
 
-Local Hint Extern 0 (atomic _) => solve_atomic.
+Local Hint Extern 0 (atomic _ _) => solve_atomic.
 Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
 
 Local Hint Constructors head_step.
@@ -62,11 +62,11 @@ Implicit Types efs : list expr.
 Implicit Types σ : state.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork E e Φ :
-  ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
+Lemma wp_fork s E e Φ :
+  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; 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.
 
@@ -122,9 +122,9 @@ Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
 Proof. solve_pure_exec. Qed.
 
 (** Heap *)
-Lemma wp_alloc E e v :
+Lemma wp_alloc s E e v :
   IntoVal e v →
-  {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
+  {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>"; iSplit; first by auto.
@@ -133,8 +133,8 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_load E l q v :
-  {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l ↦{q} v }}}.
+Lemma wp_load s E l q v :
+  {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}.
 Proof.
   iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -143,9 +143,9 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_store E l v' e v :
+Lemma wp_store s E l v' e v :
   IntoVal e v →
-  {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l ↦ v }}}.
+  {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ s; E {{{ RET LitV LitUnit; l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
@@ -155,9 +155,9 @@ Proof.
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_fail E l q v' e1 v1 e2 :
+Lemma wp_cas_fail s E l q v' e1 v1 e2 :
   IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
-  {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
+  {{{ ▷ l ↦{q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
   {{{ RET LitV (LitBool false); l ↦{q} v' }}}.
 Proof.
   iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) ">Hl HΦ".
@@ -167,9 +167,9 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_suc E l e1 v1 e2 v2 :
+Lemma wp_cas_suc s E l e1 v1 e2 v2 :
   IntoVal e1 v1 → IntoVal e2 v2 →
-  {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
+  {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ s; E
   {{{ RET LitV (LitBool true); l ↦ v2 }}}.
 Proof.
   iIntros (<-%of_to_val <-%of_to_val Φ) ">Hl HΦ".
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 26201a3da005d72000a66cfbbec1c21b228c9690..31c941ec2e5567b2fb018a683cbe23605841b5fc 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -5,9 +5,9 @@ From iris.heap_lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma tac_wp_expr_eval `{heapG Σ} Δ E Φ e e' :
+Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
   e = e' →
-  envs_entails Δ (WP e' @ E {{ Φ }}) → envs_entails Δ (WP e @ E {{ Φ }}).
+  envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
 
 Ltac wp_expr_eval t :=
@@ -17,20 +17,20 @@ Ltac wp_expr_eval t :=
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
 
-Lemma tac_wp_pure `{heapG Σ} Δ Δ' E e1 e2 φ Φ :
+Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
   IntoLaterNEnvs 1 Δ Δ' →
-  envs_entails Δ' (WP e2 @ E {{ Φ }}) →
-  envs_entails Δ (WP e1 @ E {{ Φ }}).
+  envs_entails Δ' (WP e2 @ s; E {{ Φ }}) →
+  envs_entails Δ (WP e1 @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite HΔ' -wp_pure_step_later //.
 Qed.
 
-Lemma tac_wp_value `{heapG Σ} Δ E Φ e v :
+Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
   IntoVal e v →
-  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
 
 Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
@@ -38,11 +38,11 @@ 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) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     let e := eval simpl in e in
     reshape_expr e ltac:(fun K e' =>
       unify e' efoc;
-      eapply (tac_wp_pure _ _ _ (fill K e'));
+      eapply (tac_wp_pure _ _ _ _ (fill K e'));
       [apply _                        (* PureExec *)
       |try fast_done                  (* The pure condition for PureExec *)
       |apply _                        (* IntoLaters *)
@@ -66,10 +66,10 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
 Tactic Notation "wp_case" := wp_pure (Case _ _ _).
 Tactic Notation "wp_match" := wp_case; wp_let.
 
-Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e f :
+Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
-  envs_entails Δ (WP e @ E {{ v, WP f (of_val v) @ E {{ Φ }} }})%I →
-  envs_entails Δ (WP fill K e @ E {{ Φ }}).
+  envs_entails Δ (WP e @ s; E {{ v, WP f (of_val v) @ s; E {{ Φ }} }})%I →
+  envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> -> ->. by apply: wp_bind. Qed.
 
 Ltac wp_bind_core K :=
@@ -81,7 +81,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 ?s ?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'"
@@ -94,13 +94,13 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (iResUR Σ).
 
-Lemma tac_wp_alloc Δ Δ' E j K e v Φ :
+Lemma tac_wp_alloc Δ Δ' s E j K e v Φ :
   IntoVal e v →
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ E {{ Φ }})) →
-  envs_entails Δ (WP fill K (Alloc e) @ E {{ Φ }}).
+    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ s; E {{ Φ }})) →
+  envs_entails Δ (WP fill K (Alloc e) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ?? HΔ.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
@@ -109,11 +109,11 @@ Proof.
   by rewrite right_id HΔ'.
 Qed.
 
-Lemma tac_wp_load Δ Δ' E i K l q v Φ :
+Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}).
+  envs_entails Δ' (WP fill K (of_val v) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ???.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
@@ -121,13 +121,13 @@ Proof.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ :
+Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
   IntoVal e v' →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  envs_entails Δ'' (WP fill K (Lit LitUnit) @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}).
+  envs_entails Δ'' (WP fill K (Lit LitUnit) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ?????.
   rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
@@ -135,12 +135,12 @@ Proof.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 Φ :
+Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
-  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
+  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ??????.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
@@ -148,13 +148,13 @@ Proof.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas_suc Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ :
+Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
   IntoVal e1 v1 → IntoVal e2 v2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
+  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ???????; subst.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
@@ -180,7 +180,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 ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
         wp_bind_core K; iApplyHyp H; try iNext; wp_expr_simpl) ||
       lazymatch iTypeOf H with
@@ -192,10 +192,10 @@ 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 ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_alloc _ _ _ H K); [apply _|..])
+         eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..])
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
     [apply _
     |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
@@ -211,9 +211,9 @@ Tactic Notation "wp_alloc" ident(l) :=
 Tactic Notation "wp_load" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K))
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
       |fail 1 "wp_load: cannot find 'Load' in" e];
     [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
@@ -225,10 +225,10 @@ Tactic Notation "wp_load" :=
 Tactic Notation "wp_store" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_store _ _ _ _ _ K); [apply _|..])
+         eapply (tac_wp_store _ _ _ _ _ _ K); [apply _|..])
       |fail 1 "wp_store: cannot find 'Store' in" e];
     [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
@@ -241,10 +241,10 @@ Tactic Notation "wp_store" :=
 Tactic Notation "wp_cas_fail" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_cas_fail _ _ _ _ K); [apply _|apply _|..])
+         eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..])
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
@@ -257,10 +257,10 @@ Tactic Notation "wp_cas_fail" :=
 Tactic Notation "wp_cas_suc" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
+         eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [apply _|apply _|..])
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index c5956371f787ffee583d13ffa9bf9f4bc8ddc51a..5cafc8f7b5cda3be5d31391615092867a4a182fc 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -193,11 +193,12 @@ 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 s e : is_atomic e → Atomic s (to_expr e).
 Proof.
+  enough (is_atomic e → Atomic StronglyAtomic (to_expr e)).
+  { destruct s; auto using strongly_atomic_atomic. }
   intros He. apply ectx_language_atomic.
-  - intros σ e' σ' ef Hstep; simpl in *.
-    apply language.val_irreducible; revert Hstep.
+  - 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.
@@ -233,11 +234,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'));
+  | |- Atomic ?s ?e =>
+     let e' := W.of_expr e in change (Atomic s (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 (Atomic _ _) => solve_atomic : typeclass_instances.
 
 (** Substitution *)
 Ltac simpl_subst :=
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 8d6f9a85b3517fdd6c8e9be2b3bc322859fcb903..6192bd377000010addebb5ccdf7fbf5cc6489a8c 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 {Λ} (s : stuckness) (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 :
+   s = NotStuck →
    rtc step ([e1], σ1) (t2, σ2) →
    e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2)
 }.
 
 Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
-  adequate e1 σ1 φ →
+  adequate NotStuck 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 NotStuck 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.
@@ -64,13 +65,15 @@ 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 (only parsing).
+Notation world σ := (world' ⊤ σ) (only parsing).
 
-Notation wptp t := ([∗ list] ef ∈ t, WP ef {{ _, True }})%I.
+Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
 
-Lemma wp_step e1 σ1 e2 σ2 efs Φ :
+Lemma wp_step s 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 e1 @ s; E {{ Φ }}
+  ==∗ ▷ |==> ◇ (world' E σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s 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.
@@ -79,10 +82,10 @@ Proof.
   iMod ("H" $! e2 σ2 efs with "[%] [$Hw $HE]") as ">($ & $ & $ & $)"; auto.
 Qed.
 
-Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
+Lemma wptp_step s 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 @ s; ⊤ {{ Φ }} ∗ wptp s t1
+  ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
   iIntros (Hstep) "(HW & He & Ht)".
   destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
@@ -93,11 +96,11 @@ Proof.
     iApply wp_step; eauto with iFrame.
 Qed.
 
-Lemma wptp_steps n e1 t1 t2 σ1 σ2 Φ :
+Lemma wptp_steps s n e1 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢
+  world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s 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 @ s; ⊤ {{ Φ }} ∗ wptp s 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. }
@@ -119,9 +122,9 @@ Proof.
   by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
 Qed.
 
-Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
+Lemma wptp_result s 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 @ s; ⊤ {{ v, ⌜φ v⌝ }} ∗ wptp s 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 +132,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 {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
 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:?.
+  { iIntros "!> !> !%". left. by exists v. }
+  rewrite fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
+  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 NotStuck t1
+  ⊢ ▷^(S (S n)) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
 Proof.
   intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
   iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq.
@@ -149,9 +154,9 @@ Proof.
   - iMod (wp_safe with "Hw [Htp]") as "$". by iApply (big_sepL_elem_of with "Htp").
 Qed.
 
-Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 φ Φ :
+Lemma wptp_invariance s 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 @ s; ⊤ {{ Φ }} ∗ wptp s t1
   ⊢ ▷^(S (S n)) ⌜φ⌝.
 Proof.
   intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
@@ -162,12 +167,12 @@ Proof.
 Qed.
 End adequacy.
 
-Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ :
+Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
   (∀ `{Hinv : invG Σ},
      (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ ∗ WP e {{ v, ⌜φ v⌝ }})%I) →
-  adequate e σ φ.
+       stateI σ ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) →
+  adequate s e σ φ.
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n ?]%rtc_nsteps.
@@ -176,7 +181,7 @@ 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 s; 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)".
@@ -184,11 +189,11 @@ Proof.
     iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
 Qed.
 
-Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
+Theorem wp_invariance Σ Λ `{invPreG Σ} s 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 @ s; ⊤ {{ _, 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 9f00ed60a5e99b9ddfccd639f42a48d3972a4ab7..25a2412795b3c11d821ebb0a93a4d443b6caba93 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -100,6 +100,8 @@ Section ectx_language.
     ∃ e' σ' efs, head_step e σ e' σ' efs.
   Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ e' σ' efs, ¬head_step e σ e' σ' efs.
+  Definition head_stuck (e : expr Λ) (σ : state Λ) :=
+    to_val e = None ∧ ∀ K e', e = fill K e' → head_irreducible e' σ.
 
   (* All non-value redexes are at the root.  In other words, all sub-redexes are
      values. *)
@@ -127,6 +129,11 @@ Section ectx_language.
 
   Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
 
+  Definition head_atomic (a : atomicity) (e : expr Λ) : Prop :=
+    ∀ σ e' σ' efs,
+      head_step e σ e' σ' efs →
+      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
+
   (* Some lemmas about this language *)
   Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
   Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
@@ -158,10 +165,16 @@ Section ectx_language.
     rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
   Qed.
 
-  Lemma ectx_language_atomic e :
-    (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
-    sub_redexes_are_values e →
-    Atomic e.
+  Lemma head_stuck_stuck e σ :
+    head_stuck e σ → sub_redexes_are_values e → stuck e σ.
+  Proof.
+    move=>[] ? Hirr ?. split; first done.
+    apply prim_head_irreducible; last done.
+    apply (Hirr empty_ectx). by rewrite fill_empty.
+  Qed.
+
+  Lemma ectx_language_atomic a e :
+    head_atomic a e → sub_redexes_are_values e → Atomic a e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index a68162c0134025c25e9aeaad7c237a942df7f34c..4a8228a62c594553e7e8a2d3c0d9b6673e58a9e6 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -5,59 +5,85 @@ Set Default Proof Using "Type".
 
 Section wp.
 Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
+Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Hint Resolve head_prim_reducible head_reducible_prim_step.
+Hint Resolve (reducible_not_val _ inhabitant).
+Hint Resolve head_stuck_stuck.
 
-Lemma wp_lift_head_step {E Φ} e1 :
+Lemma wp_lift_head_step {s 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 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step E)=>//. iIntros (σ1) "Hσ".
-  iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
-  iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%".
-  iApply "H". by eauto.
+  iIntros (?) "H". iApply wp_lift_step=>//. iIntros (σ1) "Hσ".
+  iMod ("H" with "Hσ") as "[% H]"; iModIntro.
+  iSplit; first by destruct s; eauto. iNext. iIntros (e2 σ2 efs) "%".
+  iApply "H"; eauto.
 Qed.
 
-Lemma wp_lift_pure_head_step {E E' Φ} e1 :
+Lemma wp_lift_head_stuck E Φ e :
+  to_val e = None →
+  sub_redexes_are_values e →
+  (∀ σ, state_interp σ ={E,∅}=∗ ⌜head_stuck e σ⌝)
+  ⊢ WP e @ E ?{{ Φ }}.
+Proof.
+  iIntros (??) "H". iApply wp_lift_stuck; first done.
+  iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
+Qed.
+
+Lemma wp_lift_pure_head_step {s 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 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   iIntros (??) "H". iApply wp_lift_pure_step; eauto.
+  { by destruct s; auto. }
   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 E Φ e :
+  to_val e = None →
+  sub_redexes_are_values e →
+  (∀ σ, head_stuck e σ) →
+  WP e @ E ?{{ Φ }}%I.
+Proof using Hinh.
+  iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
+  iIntros (σ) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
+  by auto.
+Qed.
+
+Lemma wp_lift_atomic_head_step {s 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 @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; 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.
+  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct s; auto. 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 {s 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 @ s; E {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
@@ -65,25 +91,29 @@ 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 {s 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 {{ Φ }}.
-Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
+  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
+Proof using Hinh.
+  intros. rewrite -(wp_lift_pure_det_step e1 e2 efs); eauto.
+  destruct s; by auto.
+Qed.
 
-Lemma wp_lift_pure_det_head_step_no_fork {E E' Φ} e1 e2 :
+Lemma wp_lift_pure_det_head_step_no_fork {s 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 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
+  destruct s; by auto.
 Qed.
 
-Lemma wp_lift_pure_det_head_step_no_fork' {E Φ} e1 e2 :
+Lemma wp_lift_pure_det_head_step_no_fork' {s E Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs',
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 78bc878289ec3d5b06e121f8ae9f5c93e663c9a5..23857734d46f7caf190cbed7db95704390d4ad7e 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -3,126 +3,153 @@ 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 Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
-  (□ (P -∗ WP e @ E {{ Φ }}))%I.
-Instance: Params (@ht) 4.
+  (□ (P -∗ WP e @ s; E {{ Φ }}))%I.
+Instance: Params (@ht) 5.
 
-Notation "{{ P } } e @ E {{ Φ } }" := (ht E P%I e%E Φ%I)
+Notation "{{ P } } e @ s ; E {{ Φ } }" := (ht s E P%I e%E Φ%I)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  s ;  E  {{  Φ  } }") : stdpp_scope.
+Notation "{{ P } } e @ E {{ Φ } }" := (ht NotStuck E P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  {{  Φ  } }") : stdpp_scope.
-Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P%I e%E Φ%I)
+Notation "{{ P } } e @ E ? {{ Φ } }" := (ht MaybeStuck E P%I e%E Φ%I)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  E  ? {{  Φ  } }") : stdpp_scope.
+Notation "{{ P } } e {{ Φ } }" := (ht NotStuck ⊤ P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : stdpp_scope.
+Notation "{{ P } } e ? {{ Φ } }" := (ht MaybeStuck ⊤ P%I e%E Φ%I)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  ? {{  Φ  } }") : stdpp_scope.
 
-Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e @ s ; E {{ v , Q } }" := (ht s E P%I e%E (λ v, Q)%I)
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  @  s ;  E  {{  v ,  Q  } }") : stdpp_scope.
+Notation "{{ P } } e @ E {{ v , Q } }" := (ht NotStuck E P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : stdpp_scope.
-Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht MaybeStuck E P%I e%E (λ v, Q)%I)
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  @  E  ? {{  v ,  Q  } }") : stdpp_scope.
+Notation "{{ P } } e {{ v , Q } }" := (ht NotStuck ⊤ P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  {{  v ,  Q  } }") : stdpp_scope.
+Notation "{{ P } } e ? {{ v , Q } }" := (ht MaybeStuck ⊤ P%I e%E (λ v, Q)%I)
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  ? {{  v ,  Q  } }") : stdpp_scope.
 
 Section hoare.
 Context `{irisG Λ Σ}.
+Implicit Types s : stuckness.
 Implicit Types P Q : iProp Σ.
 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 s E n :
+  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht s E).
 Proof. solve_proper. Qed.
-Global Instance ht_proper E :
-  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht E).
+Global Instance ht_proper s E :
+  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht s 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 s E P P' Φ Φ' e :
+  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ s; E {{ Φ' }} ⊢ {{ P }} e @ s; E {{ Φ }}.
 Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
-Global Instance ht_mono' E :
-  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht E).
+Lemma ht_stuck_mono s1 s2 E P Φ e :
+  s1 ⊑ s2 → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}.
+Proof. by intros; apply persistently_mono, wand_mono, wp_stuck_mono. Qed.
+Global Instance ht_mono' s E :
+  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E).
 Proof. solve_proper. Qed.
 
-Lemma ht_alt E P Φ e : (P ⊢ WP e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
+Lemma ht_alt s E P Φ e : (P ⊢ WP e @ s; E {{ Φ }}) → {{ P }} e @ s; 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 s E v : {{ True }} of_val v @ s; 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 s E P P' Φ Φ' e :
+  (P ={E}=> P') ∧ {{ P' }} e @ s; E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
+  ⊢ {{ P }} e @ s; 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 s E1 E2 P P' Φ Φ' e `{!Atomic (stuckness_to_atomicity s) e} :
+  (P ={E1,E2}=> P') ∧ {{ P' }} e @ s; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
+  ⊢ {{ P }} e @ s; 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} s E P Φ Φ' e :
+  {{ P }} e @ s; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
+  ⊢ {{ P }} K e @ s; 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_stuck_weaken s E P Φ e :
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
+Proof.
+  by iIntros "#Hwp !# ?"; iApply wp_stuck_weaken; iApply "Hwp".
+Qed.
+
+Lemma ht_mask_weaken s E1 E2 P Φ e :
+  E1 ⊆ E2 → {{ P }} e @ s; E1 {{ Φ }} ⊢ {{ P }} e @ s; 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 s E P Φ R e :
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ R ∗ P }} e @ s; 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 s E P Φ R e :
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ R }} e @ s; 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 s 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 @ s; E2 {{ Φ }}
+  ⊢ {{ R1 ∗ P }} e @ s; 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 s 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 @ s; E2 {{ Φ }}
+  ⊢ {{ P ∗ R1 }} e @ s; 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' s E P R e Φ :
   to_val e = None →
-  {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ E {{ v, R ∗ Φ v }}.
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ s; 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' s E P Φ R e :
   to_val e = None →
-  {{ P }} e @ E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ E {{ v, Φ v ∗ R }}.
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ s; 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 a3704c7029b09f3873f4bd844ad2cfcede647c92..26f813c5f55797ec836638ee85968fa61eb58554 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -53,6 +53,8 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
 Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
 Proof. constructor; naive_solver. Qed.
 
+Inductive atomicity := StronglyAtomic | WeaklyAtomic.
+
 Section language.
   Context {Λ : language}.
   Implicit Types v : val Λ.
@@ -69,22 +71,24 @@ Section language.
     ∃ e' σ' efs, prim_step e σ e' σ' efs.
   Definition irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ e' σ' efs, ¬prim_step e σ e' σ' efs.
-
-  (* 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
-     lambdaRust of an expression that is atomic in this sense, but not in the
-     stronger sense defined below, and we have to be able to open invariants
-     around that expression.  See `CasStuckS` in
-     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v). *)
-  Class Atomic (e : expr Λ) : Prop :=
-    atomic σ e' σ' efs : prim_step e σ e' σ' efs → irreducible e' σ'.
-
-  (* To open invariants with a WP that does not ensure safety, we need a
-     stronger form of atomicity.  With the above definition, in case `e` reduces
-     to a stuck non-value, there is no proof that the invariants have been
-     established again. *)
-  Class StronglyAtomic (e : expr Λ) : Prop :=
-    strongly_atomic σ e' σ' efs : prim_step e σ e' σ' efs → is_Some (to_val e').
+  Definition stuck (e : expr Λ) (σ : state Λ) :=
+    to_val e = None ∧ irreducible e σ.
+
+  (* [Atomic WeaklyAtomic]: 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 lambdaRust of an expression that is atomic in this
+     sense, but not in the stronger sense defined below, and we have to be able
+     to open invariants around that expression.  See `CasStuckS` in
+     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
+
+     [Atomic StronglyAtomic]: To open invariants with a WP that does not ensure
+     safety, we need a stronger form of atomicity.  With the above definition,
+     in case `e` reduces to a stuck non-value, there is no proof that the
+     invariants have been established again. *)
+  Class Atomic (a : atomicity) (e : expr Λ) : Prop :=
+    atomic σ e' σ' efs :
+      prim_step e σ e' σ' efs →
+      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
 
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
@@ -105,8 +109,9 @@ Section language.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
-  Lemma strongly_atomic_atomic e : StronglyAtomic e → Atomic e.
-  Proof. unfold StronglyAtomic, Atomic. eauto using val_irreducible. Qed.
+  Lemma strongly_atomic_atomic e :
+    Atomic StronglyAtomic e → Atomic WeaklyAtomic e.
+  Proof. unfold Atomic. eauto using val_irreducible. Qed.
 
   Lemma reducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 41edd498d69b7b9a31894f40311a389b84e66779..f1299cee628ffbf79759ea943f47c145bc1576d4 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -5,50 +5,77 @@ Set Default Proof Using "Type".
 
 Section lifting.
 Context `{irisG Λ Σ}.
+Implicit Types s : stuckness.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
-Lemma wp_lift_step E Φ e1 :
+Lemma wp_lift_step s E Φ e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
-    ⌜reducible e1 σ1⌝ ∗
+    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ 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 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
+Proof.
+  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1) "Hσ".
+  iMod ("H" with "Hσ") as "(%&?)". iModIntro. iSplit. by destruct s. done.
+Qed.
+
+Lemma wp_lift_stuck E Φ e :
+  to_val e = None →
+  (∀ σ, state_interp σ ={E,∅}=∗ ⌜stuck e σ⌝)
+  ⊢ WP e @ E ?{{ Φ }}.
+Proof.
+  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1) "Hσ".
+  iMod ("H" with "Hσ") as %[? Hirr]. iModIntro. iSplit; first done.
+  iIntros "!>" (e2 σ2 efs) "%". by case: (Hirr e2 σ2 efs).
+Qed.
 
 (** Derived lifting lemmas. *)
-Lemma wp_lift_pure_step `{Inhabited (state Λ)} E E' Φ e1 :
-  (∀ σ1, reducible e1 σ1) →
+Lemma wp_lift_pure_step `{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 → σ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 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
-  { eapply reducible_not_val, (Hsafe inhabitant). }
+  { specialize (Hsafe inhabitant). destruct s; last done.
+      by eapply reducible_not_val. }
   iIntros (σ1) "Hσ". iMod "H".
-  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
-  iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
+  { iPureIntro. destruct s; done. }
+  iNext. iIntros (e2 σ2 efs ?).
   destruct (Hstep σ1 e2 σ2 efs); auto; subst.
   iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
 Qed.
 
+Lemma wp_lift_pure_stuck `{Inhabited (state Λ)} E Φ e :
+  (∀ σ, stuck e σ) →
+  True ⊢ WP e @ E ?{{ Φ }}.
+Proof.
+  iIntros (Hstuck) "_". iApply wp_lift_stuck.
+  - destruct(to_val e) as [v|] eqn:He; last done.
+    rewrite -He. by case: (Hstuck inhabitant).
+  - 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 {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
-    ⌜reducible e1 σ1⌝ ∗
+    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ 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 @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step E _ e1)=>//; iIntros (σ1) "Hσ1".
+  iIntros (?) "H". iApply (wp_lift_step s 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,32 +84,34 @@ Proof.
   by iApply wp_value.
 Qed.
 
-Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E E' Φ} e1 e2 efs :
-  (∀ σ1, reducible e1 σ1) →
+Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
+  (∀ σ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' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-  (|={E,E'}▷=> WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+  ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
-  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step E); try done.
+  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step s E E'); try done.
   { by intros; eapply Hpuredet. }
   iApply (step_fupd_wand with "H"); iIntros "H".
   by iIntros (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 
-Lemma wp_pure_step_fupd `{Inhabited (state Λ)} E E' e1 e2 φ Φ :
+Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
-  (|={E,E'}▷=> WP e2 @ E {{ Φ }}) ⊢ WP e1 @ E {{ Φ }}.
+  (|={E,E'}▷=> WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros ([??] Hφ) "HWP".
-  iApply (wp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|].
-  rewrite big_sepL_nil right_id //.
+  iApply (wp_lift_pure_det_step with "[HWP]").
+  - intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val.
+  - destruct s; naive_solver.
+  - by rewrite big_sepL_nil right_id.
 Qed.
 
-Lemma wp_pure_step_later `{Inhabited (state Λ)} E e1 e2 φ Φ :
+Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+  ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //.
 Qed.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 9a4aca00be2f8529bd0d006c93243f06a29f502c..abd3aa7da9fcff5683e152cf3facf8b9f26a2530 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 Λ Σ} s e σ φ :
+  (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+  adequate s e σ φ.
 Proof.
   intros Hwp. apply (wp_adequacy Σ _).
   iIntros (?) "". iMod (own_alloc (● (Excl' (σ : leibnizC _)) ⋅ ◯ (Excl' σ)))
@@ -50,18 +50,18 @@ Proof.
   iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP.
 Qed.
 
-Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ :
+Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
   (∀ `{ownPG Λ Σ},
-    ownP σ1 ={⊤}=∗ WP e {{ _, True }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
+    ownP σ1 ={⊤}=∗ WP e @ s; ⊤ {{ _, 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 Σ Λ s 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σ".
   iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]"; first by rewrite /ownP.
-  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
+  iIntros "!> Hσ". iMod "H" as (σ2') "[Hσf %]". rewrite/ownP.
   iDestruct (own_valid_2 with "Hσ Hσf")
     as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2; auto.
 Qed.
@@ -70,164 +70,220 @@ Qed.
 (** Lifting *)
 Section lifting.
   Context `{ownPG Λ Σ}.
+  Implicit Types s : stuckness.
   Implicit Types e : expr Λ.
   Implicit Types Φ : val Λ → iProp Σ.
 
+  Lemma ownP_eq σ1 σ2 : state_interp σ1 -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
+  Proof.
+    iIntros "Hσ1 Hσ2"; rewrite/ownP.
+    by iDestruct (own_valid_2 with "Hσ1 Hσ2")
+      as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+  Qed.
   Lemma ownP_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
   Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
   Global Instance ownP_timeless σ : Timeless (@ownP (state Λ) Σ _ σ).
   Proof. rewrite /ownP; apply _. Qed.
 
-  Lemma ownP_lift_step E Φ e1 :
-    (|={E,∅}=> ∃ σ1, ⌜reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
+  Lemma ownP_lift_step s E Φ e1 :
+    (|={E,∅}=> ∃ σ1, ⌜if s is NotStuck then reducible e1 σ1 else to_val e1 = None⌝ ∗ ▷ 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 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
     - apply of_to_val in EQe1 as <-. iApply fupd_wp.
-      iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred%reducible_not_val.
+      iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred.
+      destruct s; last done. apply reducible_not_val in Hred.
       move: Hred; by rewrite to_of_val.
     - iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ".
-      iMod "H" as (σ1' ?) "[>Hσf H]". rewrite /ownP.
-      iDestruct (own_valid_2 with "Hσ Hσf")
-        as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
-      iModIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
-      iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
+      iMod "H" as (σ1' ?) "[>Hσf H]". iDestruct (ownP_eq with "Hσ Hσf") as %->.
+      iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep).
+      rewrite /ownP; iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
       { by apply auth_update, option_local_update,
           (exclusive_local_update _ (Excl σ2)). }
       iFrame "Hσ". iApply ("H" with "[]"); eauto.
   Qed.
 
-  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
-    (∀ σ1, reducible e1 σ1) →
+  Lemma ownP_lift_stuck E Φ e :
+    (|={E,∅}=> ∃ σ, ⌜stuck 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 %[Hnv _]. exfalso.
+      by rewrite to_of_val in Hnv.
+    - iApply wp_lift_stuck; [done|]. iIntros (σ1) "Hσ".
+      iMod "H" as (σ1') "(% & >Hσf)".
+      by iDestruct (ownP_eq with "Hσ Hσf") as %->.
+  Qed.
+
+  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s 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 → σ1 = σ2) →
     (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
-      WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+      WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
-    { eapply reducible_not_val, (Hsafe inhabitant). }
+    iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
+    { specialize (Hsafe inhabitant). destruct s; last done.
+      by eapply reducible_not_val. }
     iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-    iModIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
+    iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
     destruct (Hstep σ1 e2 σ2 efs); auto; subst.
-    iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
+    by iMod "Hclose"; iModIntro; iFrame; iApply "H".
   Qed.
 
   (** Derived lifting lemmas. *)
-  Lemma ownP_lift_atomic_step {E Φ} e1 σ1 :
-    reducible e1 σ1 →
+  Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
+    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (▷ 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 @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    iIntros (?) "[Hσ H]". iApply (ownP_lift_step E _ e1).
-    iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iModIntro.
-    iExists σ1. iFrame "Hσ"; iSplit; eauto.
+    iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
+    iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+    iModIntro; iExists σ1; iFrame; iSplit; first by destruct s.
     iNext; iIntros (e2 σ2 efs) "% Hσ".
     iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
     destruct (to_val e2) eqn:?; last by iExFalso.
-    iMod "Hclose". iApply wp_value; auto using to_of_val. done.
+    by iMod "Hclose"; iApply wp_value; auto using to_of_val.
   Qed.
 
-  Lemma ownP_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
-    reducible e1 σ1 →
+  Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :
+    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (∀ 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 @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
+  Proof.
+    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. by rewrite Hval; iApply "Hσ2".
+  Qed.
+
+  Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
+    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
+    (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
+      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
+    {{{ ▷ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
   Proof.
-    iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (ownP_lift_atomic_step _ σ1); try done.
-    iFrame. iNext. iIntros (e2' σ2' efs') "% Hσ2'".
-    edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
+    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 Λ)} {E Φ} e1 e2 efs :
-    (∀ σ1, reducible e1 σ1) →
+  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
+    (∀ σ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' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-    ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤{{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    iIntros (? Hpuredet) "?". iApply (ownP_lift_pure_step E); try done.
-    by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
+    iIntros (? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
+    by apply Hpuredet. by iNext; iIntros (e' efs' σ (_&->&->)%Hpuredet).
+  Qed.
+
+  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s 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' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
+  Proof.
+    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
   Qed.
 End lifting.
 
 Section ectx_lifting.
   Import ectx_language.
   Context {Λ : ectxLanguage} `{ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
+  Implicit Types s : stuckness.
   Implicit Types Φ : val Λ → iProp Σ.
   Implicit Types e : expr Λ.
   Hint Resolve head_prim_reducible head_reducible_prim_step.
+  Hint Resolve (reducible_not_val _ inhabitant).
+  Hint Resolve head_stuck_stuck.
 
-  Lemma ownP_lift_head_step E Φ e1 :
+  Lemma ownP_lift_head_step s 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 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    iIntros "H". iApply (ownP_lift_step E); try done.
-    iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1.
-    iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
+    iIntros "H". iApply ownP_lift_step.
+    iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1. iSplit.
+    { destruct s; try by eauto using reducible_not_val. }
+    iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
     iApply ("Hwp" with "[]"); eauto.
   Qed.
 
-  Lemma ownP_lift_pure_head_step E Φ e1 :
+  Lemma ownP_lift_head_stuck E Φ e :
+    sub_redexes_are_values e →
+    (|={E,∅}=> ∃ σ, ⌜head_stuck e σ⌝ ∗ ▷ ownP σ)
+    ⊢ WP e @ E ?{{ Φ }}.
+  Proof.
+    iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]".
+    iExists σ. by auto.
+  Qed.
+
+  Lemma ownP_lift_pure_head_step s 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 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
-    iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
-    iIntros (????). iApply "H". eauto.
+    iIntros (??) "H".  iApply ownP_lift_pure_step; eauto.
+    { by destruct s; auto. }
+    iNext. iIntros (????). iApply "H"; eauto.
   Qed.
 
-  Lemma ownP_lift_atomic_head_step {E Φ} e1 σ1 :
+  Lemma ownP_lift_atomic_head_step {s 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 @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto. iFrame. iNext.
-    iIntros (???) "% ?". iApply ("H" with "[]"); eauto.
+    iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto.
+    { by destruct s; eauto using reducible_not_val. }
+    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 {s 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 {{ Φ }}.
-  Proof. eauto using ownP_lift_atomic_det_step. Qed.
+    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
+  Proof.
+    by destruct s; eauto 10 using ownP_lift_atomic_det_step, reducible_not_val.
+  Qed.
 
-  Lemma ownP_lift_atomic_det_head_step_no_fork {E e1} σ1 v2 σ2 :
+  Lemma ownP_lift_atomic_det_head_step_no_fork {s 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 }}}.
+    {{{ ▷ ownP σ1 }}} e1 @ s; 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.
+    intros ???; apply ownP_lift_atomic_det_step_no_fork; eauto.
+    by destruct s; eauto using reducible_not_val.
   Qed.
 
-  Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
+  Lemma ownP_lift_pure_det_head_step {s 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 {{ Φ }}.
+    ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
+    ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
-    intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_step; eauto.
+    iIntros (??) "H"; iApply wp_lift_pure_det_step; eauto.
+    by destruct s; eauto using reducible_not_val.
   Qed.
 
-  Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
-    to_val e1 = None →
+  Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
     (∀ σ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 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
-    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
+    iIntros (??) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
+    by destruct s; eauto using reducible_not_val.
   Qed.
 End ectx_lifting.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 97096107c17d524ba6b62b1660d6262b4373997a..677f071d729775ae8f35c0521e86e57fd6cff52c 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -11,99 +11,188 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
-Definition wp_pre `{irisG Λ Σ}
+Inductive stuckness := NotStuck | MaybeStuck.
+
+Definition stuckness_le (s1 s2 : stuckness) : bool :=
+  match s1, s2 with
+  | MaybeStuck, NotStuck => false
+  | _, _ => true
+  end.
+Instance: PreOrder stuckness_le.
+Proof.
+  split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
+Qed.
+Instance: SqSubsetEq stuckness := stuckness_le.
+
+Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
+  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
+
+Definition wp_pre `{irisG Λ Σ} (s : stuckness)
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ 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 s is NotStuck 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)
   end%I.
 
-Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
+Local Instance wp_pre_contractive `{irisG Λ Σ} s : Contractive (wp_pre s).
 Proof.
   rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
-Definition wp_def `{irisG Λ Σ} :
-  coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint wp_pre.
+Definition wp_def `{irisG Λ Σ} s :
+  coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
 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 @ s ; E {{ Φ } }" := (wp s E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  s ;  E  {{  Φ  } } ']'") : uPred_scope.
+Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck 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 MaybeStuck E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  E  ? {{  Φ  } } ']'") : uPred_scope.
+Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : uPred_scope.
+Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ 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 @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' @  s ;  E  {{  v ,  Q  } } ']'") : uPred_scope.
+Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck 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 MaybeStuck 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 NotStuck ⊤ 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 MaybeStuck ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' ? {{  v ,  Q  } } ']'") : uPred_scope.
 
 (* Texan triples *)
+Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})%I
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  @  s ;  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 @ s ; E {{{ 'RET' pat ; Q } } }" :=
+  (□ ∀ Φ, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})%I
+    (at level 20,
+     format "{{{  P  } } }  e  @  s ;  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 @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})
+    (at level 20, x closed binder, y closed binder,
+     format "{{{  P  } } }  e  @  s ;  E  {{{  x .. y ,  RET  pat ;  Q } } }") : stdpp_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 } } }") : stdpp_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 } } }") : stdpp_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 } } }") : stdpp_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 } } }") : stdpp_scope.
+Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})
+    (at level 20,
+     format "{{{  P  } } }  e  @  s ;  E  {{{  RET  pat ;  Q } } }") : stdpp_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 } } }") : stdpp_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 } } }") : stdpp_scope.
 Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
   (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})
     (at level 20,
      format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : stdpp_scope.
+Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
+  (∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})
+    (at level 20,
+     format "{{{  P  } } }  e  ? {{{  RET  pat ;  Q } } }") : stdpp_scope.
 
 Section wp.
 Context `{irisG Λ Σ}.
+Implicit Types s : stuckness.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 
 (* Weakest pre *)
-Lemma wp_unfold E e Φ : WP e @ E {{ Φ }} ⊣⊢ wp_pre wp E e Φ.
-Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.
+Lemma wp_unfold s E e Φ : WP e @ s; E {{ Φ }} ⊣⊢ wp_pre s (wp s) E e Φ.
+Proof. rewrite wp_eq. apply (fixpoint_unfold (wp_pre s)). Qed.
 
-Global Instance wp_ne E e n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ E e).
+Global Instance wp_ne s E e n :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ s E e).
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
   rewrite !wp_unfold /wp_pre.
@@ -113,19 +202,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 s E e :
+  Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ _ s 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' s E Φ v : Φ v ⊢ WP of_val v @ s; 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 s E Φ v : WP of_val v @ s; 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 s E1 E2 e Φ Ψ :
+  E1 ⊆ E2 → (∀ v, Φ v ={E2}=∗ Ψ v) ∗ WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; 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 +226,149 @@ Proof.
   iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
 Qed.
 
-Lemma fupd_wp E e Φ : (|={E}=> WP e @ E {{ Φ }}) ⊢ WP e @ E {{ Φ }}.
+Lemma wp_stuck_weaken s E e Φ :
+  WP e @ s; 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 s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; 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 s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
+Proof. iIntros "H". iApply (wp_strong_mono s 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 s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
+  (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
 Proof.
-  iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
+  iIntros "H". rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:He.
   { 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).
+  iModIntro. iNext. iIntros (e2 σ2 efs Hstep). destruct s.
+  - iMod ("H" with "[//]") as "(Hphy & H & $)".
+    rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
+    + iDestruct "H" as ">> $". by iFrame.
+    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
+      by edestruct (atomic _ _ _ _ Hstep).
+  - destruct (atomic _ _ _ _ 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 s 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 @ s; E2 {{ v, P ={E1}=∗ Φ v }} -∗ WP e @ s; 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 s 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} s E e Φ :
+  WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }} ⊢ WP K e @ s; 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 s; 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} s E e Φ :
+  WP K e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, WP K (of_val v) @ s; 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 s; 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 s E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ Ψ }}.
 Proof.
-  iIntros (HΦ) "H"; iApply (wp_strong_mono E E); auto.
+  iIntros (HΦ) "H"; iApply (wp_strong_mono s 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_stuck_mono s1 s2 E e Φ :
+  s1 ⊑ s2 → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
+Proof. case: s1; case: s2 => // _. exact: wp_stuck_weaken. Qed.
+Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
+Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. Qed.
+Global Instance wp_mono' s E e :
+  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ s 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 s E Φ e v `{!IntoVal e v} : Φ v ⊢ WP e @ s; 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' s E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ s; 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 s E Φ e v `{!IntoVal e v} :
+  (|={E}=> Φ v) ⊢ WP e @ s; 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 s E e Φ R : R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
+Proof. iIntros "[??]". iApply (wp_strong_mono s E E _ Φ); try iFrame; eauto. Qed.
+Lemma wp_frame_r s E e Φ R : WP e @ s; E {{ Φ }} ∗ R ⊢ WP e @ s; E {{ v, Φ v ∗ R }}.
+Proof. iIntros "[??]". iApply (wp_strong_mono s E E _ Φ); try iFrame; eauto. Qed.
 
-Lemma wp_frame_step_l E1 E2 e Φ R :
+Lemma wp_frame_step_l s 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 @ 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 E1 E2 e Φ R :
+Lemma wp_frame_step_r s E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
-  WP e @ E2 {{ Φ }} ∗ (|={E1,E2}▷=> R) ⊢ WP e @ 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).
+  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_wand E e Φ Ψ :
-  WP e @ E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ E {{ Ψ }}.
+Lemma wp_frame_step_l' s E e Φ R :
+  to_val e = None → ▷ R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
+Proof. iIntros (?) "[??]". iApply (wp_frame_step_l s E E); try iFrame; eauto. Qed.
+Lemma wp_frame_step_r' s E e Φ R :
+  to_val e = None → WP e @ s; E {{ Φ }} ∗ ▷ R ⊢ WP e @ s; E {{ v, Φ v ∗ R }}.
+Proof. iIntros (?) "[??]". iApply (wp_frame_step_r s E E); try iFrame; eauto. Qed.
+
+Lemma wp_wand s E e Φ Ψ :
+  WP e @ s; E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E {{ Ψ }}.
 Proof.
-  iIntros "Hwp H". iApply (wp_strong_mono E); auto.
+  iIntros "Hwp H". iApply (wp_strong_mono s 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 s E e Φ Ψ :
+  (∀ v, Φ v -∗ Ψ v) ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; 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 s E e Φ Ψ :
+  WP e @ s; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ s; E {{ Ψ }}.
 Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
 End wp.
 
@@ -268,25 +378,26 @@ 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 s E e R Φ Ψ :
+    (∀ v, Frame p R (Φ v) (Ψ v)) → Frame p R (WP e @ s; E {{ Φ }}) (WP e @ s; 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 s E e Φ : IsExcept0 (WP e @ s; 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 s E e P Φ :
+    ElimModal (|==> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; 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 s E e P Φ :
+    ElimModal (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; 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 →
+  Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
+    Atomic (stuckness_to_atomicity s) e →
     ElimModal (|={E1,E2}=> P) P
-            (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
+            (WP e @ s; E1 {{ Φ }}) (WP e @ s; 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 b1a162b23ab1b33340186974125d34951fdb9d7b..48414dd253f6f0c7188c6a22d01d5c1948fc9311 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -105,5 +105,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 NotStuck 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..38ad33dc6008a9b944c4cbde62ae79efa1be00d9 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 → Atomic WeaklyAtomic e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".