From 018cf38c29375566a26c99b9137ed3f67e452745 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Thu, 9 Nov 2017 20:52:14 +0100
Subject: [PATCH] Revert "Revert "Merge branch 'swasey/progress' into
 'master'""

This reverts commit 913059d27af6779586272ee4c870bf5d558210a9.
---
 CHANGELOG.md                            |  14 ++
 naming.txt                              |   2 +-
 theories/heap_lang/adequacy.v           |   6 +-
 theories/heap_lang/lifting.v            |  38 ++--
 theories/heap_lang/proofmode.v          |  72 +++----
 theories/heap_lang/tactics.v            |  13 +-
 theories/program_logic/adequacy.v       |  65 +++---
 theories/program_logic/ectx_language.v  |  23 +-
 theories/program_logic/ectx_lifting.v   |  87 +++++---
 theories/program_logic/ectxi_language.v |   2 +-
 theories/program_logic/hoare.v          | 121 ++++++-----
 theories/program_logic/language.v       |  34 ++-
 theories/program_logic/lifting.v        |  88 +++++---
 theories/program_logic/ownp.v           | 232 +++++++++++++--------
 theories/program_logic/weakestpre.v     | 266 +++++++++++++++++-------
 theories/tests/heap_lang.v              |   2 +-
 theories/tests/ipm_paper.v              |   2 +-
 17 files changed, 688 insertions(+), 379 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a3305d696..71bcaac71 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,13 @@ 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
+  "progressive" vs. "non-progressive" weakest preconditions. (See
+  [Swasey et al. OOPSLA '17] for examples.) The progressive `WP e @ E
+  {{ Φ }}` ensures that, as `e` runs, it does not get stuck. The
+  non-progressive `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.
 
 Changes in Coq:
 
@@ -88,6 +95,13 @@ 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.
+* Use *stuckness bits* `s` to define progressive vs. non-progressive
+  WP. The full judgment is `WP e @ s; E {{ Φ }}`; progressive WP uses
+  `s = not_stuck` while non-progressive WP uses `s = maybe_stuck`.
+* Restore the original, stronger notion of atomicity alongside the
+  weaker notion. These are `Atomic s e` where the stuckness bit `s`
+  indicates whether expression `e` is weakly (`s = not_stuck`) or
+  strongly (`s = maybe_stuck`) atomic.
 
 ## Iris 3.0.0 (released 2017-01-11)
 
diff --git a/naming.txt b/naming.txt
index 191c1664e..ed87ef4c3 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 fa3bc513f..d712d79fd 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 (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 46c2aeb8b..2251d52c2 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,21 +62,21 @@ Implicit Types efs : list expr.
 Implicit Types σ : state.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
-Lemma wp_bind {E e} K Φ :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+Lemma wp_bind {s E e} K Φ :
+  WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }} ⊢ WP fill K e @ s; E {{ Φ }}.
 Proof. exact: wp_ectx_bind. Qed.
 
-Lemma wp_bindi {E e} Ki Φ :
-  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
-     WP fill_item Ki e @ E {{ Φ }}.
+Lemma wp_bindi {s E e} Ki Φ :
+  WP e @ s; E {{ v, WP fill_item Ki (of_val v) @ s; E {{ Φ }} }} ⊢
+     WP fill_item Ki e @ s; E {{ Φ }}.
 Proof. exact: weakestpre.wp_bind. Qed.
 
 (** 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.
 
@@ -132,9 +132,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.
@@ -143,8 +143,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 %?.
@@ -153,9 +153,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.
@@ -165,9 +165,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Φ".
@@ -177,9 +177,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 677aa6063..0f95f3b9f 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -5,21 +5,21 @@ From iris.heap_lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
+Lemma tac_wp_pure `{heapG Σ} K Δ Δ' s E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
   IntoLaterNEnvs 1 Δ Δ' →
-  envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
+  envs_entails Δ' (WP fill K e2 @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K e1 @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
   by rewrite -ectx_lifting.wp_ectx_bind_inv.
 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].
@@ -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 ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
     [simpl; apply _                 (* PureExec *)
@@ -52,9 +52,9 @@ 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 :
-  envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
-  envs_entails Δ (WP fill K e @ E {{ Φ }}).
+Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e :
+  envs_entails Δ (WP e @ s; E {{ v, WP fill K (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 :=
@@ -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 ?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'"
@@ -79,13 +79,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.
@@ -94,11 +94,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.
@@ -106,13 +106,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.
@@ -120,12 +120,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.
@@ -133,13 +133,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.
@@ -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 ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
         wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
       lazymatch iTypeOf H with
@@ -163,10 +163,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"];
@@ -182,9 +182,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
@@ -196,10 +196,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
@@ -212,10 +212,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
@@ -228,10 +228,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 1198fb520..fd3fcd635 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -187,11 +187,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 maybe_stuck (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.
@@ -227,11 +228,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 8d6f9a85b..a7f1bdd1d 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 = not_stuck →
    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 not_stuck 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 not_stuck 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 {{ Φ }} ==∗ ▷ ⌜progressive 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 not_stuck t1
+  ⊢ ▷^(S (S n)) ⌜progressive 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 d8330354d..8d7dbf1ee 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -4,7 +4,7 @@ From iris.algebra Require Export base.
 From iris.program_logic Require Import language.
 Set Default Proof Using "Type".
 
-(* We need to make thos arguments indices that we want canonical structure
+(* We need to make those arguments indices that we want canonical structure
    inference to use a keys. *)
 Class EctxLanguage (expr val ectx state : Type) := {
   of_val : val → expr;
@@ -61,6 +61,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_progressive (e : expr) (σ : state) :=
+    is_Some(to_val e) ∨ ∃ K e', e = fill K e' ∧ head_reducible e' σ.
 
   (* All non-value redexes are at the root.  In other words, all sub-redexes are
      values. *)
@@ -89,6 +91,11 @@ Section ectx_language.
     language.val_stuck := val_prim_stuck;
   |}.
 
+  Class HeadAtomic (s : stuckness) (e : expr) : Prop :=
+    head_atomic σ e' σ' efs :
+      head_step e σ e' σ' efs →
+      if s is not_stuck then irreducible e' σ' else is_Some (to_val e').
+
   (* Some lemmas about this language *)
   Lemma head_prim_step e1 σ1 e2 σ2 efs :
     head_step e1 σ1 e2 σ2 efs → prim_step e1 σ1 e2 σ2 efs.
@@ -117,10 +124,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 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.
+
+  Lemma ectx_language_atomic s e :
+    HeadAtomic s e → sub_redexes_are_values e → Atomic s e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 82275d0f3..a3d0cb768 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -6,67 +6,94 @@ Set Default Proof Using "Type".
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
 Context `{irisG (ectx_lang expr) Σ} {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 progressive_head_progressive.
 
-Lemma wp_ectx_bind {E Φ} K e :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+Lemma wp_ectx_bind {s E e} K Φ :
+  WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }}
+  ⊢ WP fill K e @ s; 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 {s E Φ} K e :
+  WP fill K e @ s; E {{ Φ }}
+  ⊢ WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }}.
 Proof. apply: weakestpre.wp_bind_inv. Qed.
 
-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 →
+  (∀ σ, 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 "%". 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 →
+  (∀ K e1 σ1 e2 σ2 efs, e = fill K e1 → ¬ head_step e1 σ1 e2 σ2 efs) →
+  WP e @ E ?{{ Φ }}%I.
+Proof using Hinh.
+  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 {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.
@@ -74,25 +101,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/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 6475a921d..0e6d4f2e0 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -4,7 +4,7 @@ From iris.algebra Require Export base.
 From iris.program_logic Require Import language ectx_language.
 Set Default Proof Using "Type".
 
-(* We need to make thos arguments indices that we want canonical structure
+(* We need to make those arguments indices that we want canonical structure
    inference to use a keys. *)
 Class EctxiLanguage (expr val ectx_item state : Type) := {
   of_val : val → expr;
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index cb110957a..629e50a99 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  {{  Φ  } }") : C_scope.
+Notation "{{ P } } e @ E {{ Φ } }" := (ht not_stuck 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 maybe_stuck E P%I e%E Φ%I)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  E  ? {{  Φ  } }") : C_scope.
+Notation "{{ P } } e {{ Φ } }" := (ht not_stuck ⊤ P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : C_scope.
+Notation "{{ P } } e ? {{ Φ } }" := (ht maybe_stuck ⊤ 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 @ 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  } }") : C_scope.
+Notation "{{ P } } e @ E {{ v , Q } }" := (ht not_stuck 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 maybe_stuck 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 not_stuck ⊤ 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 maybe_stuck ⊤ 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 Λ Σ}.
+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_stuckness_mono s1 s2 E P Φ e :
+  (s1 ≤ s2)%stuckness → {{ P }} e @ s1; E {{ Φ }} ⊢ {{ P }} e @ s2; E {{ Φ }}.
+Proof. by intros; apply persistently_mono, wand_mono, wp_stuckness_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 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_forget_not_stuck s E P Φ e :
+  {{ P }} e @ s; E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
+Proof.
+  by iIntros "#Hwp !# ?"; iApply wp_forget_not_stuck; 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 8189151d5..0d2f2bbbf 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -43,6 +43,20 @@ Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
 Instance language_ctx_id Λ : LanguageCtx Λ id.
 Proof. constructor; naive_solver. Qed.
 
+Variant stuckness := not_stuck | maybe_stuck.
+Definition stuckness_le (s1 s2 : stuckness) : bool :=
+  match s1, s2 with
+  | maybe_stuck, not_stuck => false
+  | _, _ => true
+  end.
+Instance: @PreOrder stuckness stuckness_le.
+Proof.
+  split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
+Qed.
+Bind Scope stuckness_scope with stuckness.
+Delimit Scope stuckness_scope with stuckness.
+Infix "≤" := stuckness_le : stuckness_scope.
+
 Section language.
   Context {Λ : language}.
   Implicit Types v : val Λ.
@@ -51,22 +65,24 @@ 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
+  (* [Atomic not_stuck]: 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' σ'.
+     [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v).
 
-  (* To open invariants with a WP that does not ensure safety, we need a
+     [Atomic maybe_stuck]: 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').
+  Class Atomic (s : stuckness) (e : expr Λ) : Prop :=
+    atomic σ e' σ' efs :
+      prim_step e σ e' σ' efs →
+      if s is not_stuck then irreducible e' σ' else is_Some (to_val e').
 
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
@@ -87,8 +103,8 @@ 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 maybe_stuck e → Atomic not_stuck 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 41edd498d..f69906141 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -5,50 +5,76 @@ 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 not_stuck 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,∅}=∗ ⌜¬ 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 :
-  (∀ σ1, reducible e1 σ1) →
+Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
+  to_val e1 = None →
+  (∀ σ1, if s is not_stuck then reducible e1 σ1 else True) →
   (∀ σ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). }
+  iIntros (? Hsafe Hstep) "H". iApply wp_lift_step; first done.
   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; first by iPureIntro; apply Hsafe. 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 :
+  (∀ σ, ¬ 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 {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
-    ⌜reducible e1 σ1⌝ ∗
+    ⌜if s is not_stuck 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 +83,36 @@ 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 :
+  to_val e1 = None →
+  (∀ σ1, if s is not_stuck then reducible e1 σ1 else true) →
   (∀ σ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]").
+  - apply (reducible_not_val _ inhabitant). by auto.
+  - destruct s; naive_solver.
+  - 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 1c3a8d3e3..a7c51e14e 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,87 +70,126 @@ 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 :
+    to_val e1 = None →
+    (|={E,∅}=> ∃ σ1, ⌜if s is not_stuck then reducible e1 σ1 else True⌝ ∗ ▷ 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.
-      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]".
-      { 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) →
+    iIntros (?) "H". iApply wp_lift_step; first done.
+    iIntros (σ1) "Hσ"; iMod "H" as (σ1') "(% & >Hσf & H)".
+    iDestruct (ownP_eq with "Hσ Hσf") as %->.
+    iModIntro. iSplit; first done. 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σ". by iApply ("H" with "[]"); eauto.
+  Qed.
+
+  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)".
+      by iDestruct (ownP_eq with "Hσ Hσf") as %->.
+  Qed.
+
+  Lemma ownP_lift_pure_step s E Φ e1 :
+    to_val e1 = None →
+    (∀ σ1, if s is not_stuck then reducible e1 σ1 else True) →
     (∀ σ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; first done.
     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 :
+    to_val e1 = None →
+    (if s is not_stuck then reducible e1 σ1 else True) →
     (▷ 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; first done.
+    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 :
+    to_val e1 = None →
+    (if s is not_stuck then reducible e1 σ1 else True) →
     (∀ 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 :
+    to_val e1 = None →
+    (if s is not_stuck then reducible e1 σ1 else True) →
+    (∀ 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 {s E Φ} e1 e2 efs :
+    to_val e1 = None →
+    (∀ σ1, if s is not_stuck then reducible e1 σ1 else True) →
     (∀ σ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=>//.
+    by apply Hpuredet. by iNext; iIntros (e' efs' σ (_&->&->)%Hpuredet).
+  Qed.
+
+  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
+    to_val e1 = None →
+    (∀ σ1, if s is not_stuck then reducible e1 σ1 else True) →
+    (∀ σ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.
-    iIntros (? Hpuredet) "?". iApply (ownP_lift_pure_step E); try done.
-    by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
+    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
   Qed.
 End lifting.
 
@@ -158,77 +197,100 @@ Section ectx_lifting.
   Import ectx_language.
   Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
   Context `{ownPG (ectx_lang expr) Σ} {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 progressive_head_progressive.
 
-  Lemma ownP_lift_head_step E Φ e1 :
+  Lemma ownP_lift_head_step s E Φ e1 :
+    to_val e1 = None →
     (|={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.
+    iIntros (?) "H". iApply ownP_lift_step; first done.
     iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1.
-    iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
+    iSplit; first by destruct s; eauto. 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 :
+    (|={E,∅}=> ∃ σ, ⌜¬ head_progressive e σ⌝ ∗ ▷ ownP σ)
+    ⊢ WP e @ E ?{{ Φ }}.
+  Proof.
+    iIntros "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]".
+    iModIntro. iExists σ. iFrame "Hσ". by eauto.
+  Qed.
+
+  Lemma ownP_lift_pure_head_step s E Φ e1 :
+    to_val e1 = None →
     (∀ σ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 :
+    to_val e1 = None →
     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. }
+    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 :
+    to_val e1 = None →
     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.
+  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 :
+    to_val e1 = None →
     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.
   Qed.
 
-  Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
+  Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
+    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 = 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.
   Qed.
 
-  Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
+  Lemma ownP_lift_pure_det_head_step_no_fork {s 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 @ 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.
   Qed.
 End ectx_lifting.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 32b98d8ff..efa2340a5 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -11,99 +11,172 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
-Definition wp_pre `{irisG Λ Σ}
+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 not_stuck 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 not_stuck 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 maybe_stuck E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  E  ? {{  Φ  } } ']'") : uPred_scope.
+Notation "'WP' e {{ Φ } }" := (wp not_stuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : uPred_scope.
+Notation "'WP' e ? {{ Φ } }" := (wp maybe_stuck ⊤ 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 not_stuck 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 maybe_stuck 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 not_stuck ⊤ 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 maybe_stuck ⊤ 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 } } }") : 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 @ 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 } } }") : 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 Λ Σ}.
+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 +186,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,17 +210,45 @@ 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_not_stuck 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 →
+Lemma wp_strong_atomic s E1 E2 e Φ :
+  Atomic maybe_stuck e →
+  (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
+Proof.
+  iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
+  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).
+  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_weak_atomic E1 E2 e Φ :
+  Atomic not_stuck e →
   (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
 Proof.
   iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
@@ -157,108 +258,117 @@ Proof.
   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.
+  - iDestruct "H" as ">> $". by iFrame.
   - iMod ("H" with "[$]") as "[H _]".
     iDestruct "H" as %(? & ? & ? & ?). by edestruct (Hatomic _ _ _ _ Hstep).
 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_stuckness_mono s1 s2 E e Φ :
+  (s1 ≤ s2)%stuckness → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
+Proof. case: s1; case: s2 => // _. exact: wp_forget_not_stuck. 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_atomic s E1 E2 e Φ `{!Atomic s e} :
+  (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
+Proof. destruct s. exact: wp_weak_atomic. exact: wp_strong_atomic. Qed.
 
-Lemma wp_frame_step_l E1 E2 e Φ R :
+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 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,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 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 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 51681a365..2771e3101 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 not_stuck 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 6834c5c5e..b6189d309 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 not_stuck e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".
-- 
GitLab