Add progress bit to wp (and slightly generalize wp_step, wp_safe).

569c559f · David Swasey · 13c21cb7 · 569c559f · 569c559f · 569c559f
Commit 569c559f authored 8 years ago by David Swasey
--- a/naming.txt
+++ b/naming.txt
@@ -14,7 +14,7 @@ l
 m : iGst = ghost state
 n
 o
-p
+p : progress bits
 q
 r : iRes = resources
 s : state (STSs)

--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -15,7 +15,7 @@ Proof. intros [? ?]%subG_inv; split; apply _. Qed.
 Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
  (∀ `{heapG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
-  adequate e σ φ.
+  adequate true e σ φ.
 Proof.
  intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
  iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".

--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -74,7 +74,7 @@ Lemma wp_fork E e Φ :
  ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
 Proof.
  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite later_sep -(wp_value _ _ (Lit _)) // big_sepL_singleton.
+  - by rewrite later_sep -(wp_value _ _ _ (Lit _)) // big_sepL_singleton.
  - intros; inv_head_step; eauto.
 Qed.

--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -25,7 +25,7 @@ Ltac wp_value_head := etrans; [|eapply wp_value; wp_done]; lazy beta.
 Ltac wp_seq_head :=
  lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
+  | |- _ ⊢ wp true ?E (Seq _ _) ?Q =>
    etrans; [|eapply wp_seq; wp_done]; iNext
  end.
@@ -33,15 +33,15 @@ Ltac wp_finish := intros_revert ltac:(
  rewrite /= ?to_of_val;
  try iNext;
  repeat lazymatch goal with
-  | |- _ ⊢ wp ?E (Seq _ _) ?Q =>
+  | |- _ ⊢ wp true ?E (Seq _ _) ?Q =>
     etrans; [|eapply wp_seq; wp_done]; iNext
-  | |- _ ⊢ wp ?E _ ?Q => wp_value_head
+  | |- _ ⊢ wp true ?E _ ?Q => wp_value_head
  end).
 Tactic Notation "wp_value" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- _ ⊢ wp true ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    wp_bind_core K; wp_value_head) || fail "wp_value: cannot find value in" e
  | _ => fail "wp_value: not a wp"
  end.
@@ -56,7 +56,7 @@ Ltac solve_of_val_unlock := try apply of_val_unlock; reflexivity.
 Tactic Notation "wp_rec" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- _ ⊢ wp true ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with App ?e1 _ =>
 (* hnf does not reduce through an of_val *)
 (*      match eval hnf in e1 with Rec _ _ _ => *)
@@ -69,7 +69,7 @@ Tactic Notation "wp_rec" :=
 Tactic Notation "wp_lam" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- _ ⊢ wp true ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with App ?e1 _ =>
 (*    match eval hnf in e1 with Rec BAnon _ _ => *)
    wp_bind_core K; etrans;
@@ -84,7 +84,7 @@ Tactic Notation "wp_seq" := wp_let.
 Tactic Notation "wp_op" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- _ ⊢ wp true ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    lazymatch eval hnf in e' with
    | BinOp LtOp _ _ => wp_bind_core K; apply wp_lt; wp_finish
    | BinOp LeOp _ _ => wp_bind_core K; apply wp_le; wp_finish
@@ -103,7 +103,7 @@ Tactic Notation "wp_op" :=
 Tactic Notation "wp_proj" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- _ ⊢ wp true ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | Fst _ => wp_bind_core K; etrans; [|eapply wp_fst; wp_done]; wp_finish
    | Snd _ => wp_bind_core K; etrans; [|eapply wp_snd; wp_done]; wp_finish
@@ -114,7 +114,7 @@ Tactic Notation "wp_proj" :=
 Tactic Notation "wp_if" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- _ ⊢ wp true ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | If _ _ _ =>
      wp_bind_core K;
@@ -126,7 +126,7 @@ Tactic Notation "wp_if" :=
 Tactic Notation "wp_match" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- _ ⊢ wp true ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match eval hnf in e' with
    | Case _ _ _ =>
      wp_bind_core K;
@@ -139,7 +139,7 @@ Tactic Notation "wp_match" :=
 Tactic Notation "wp_bind" open_constr(efoc) :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- _ ⊢ wp true ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    match e' with
    | efoc => unify e' efoc; wp_bind_core K
    end) || fail "wp_bind: cannot find" efoc "in" e
@@ -220,7 +220,7 @@ End heap.
 Tactic Notation "wp_apply" open_constr(lem) :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- _ ⊢ wp true ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    wp_bind_core K; iApply lem; try iNext)
  | _ => fail "wp_apply: not a 'wp'"
  end.
@@ -228,7 +228,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- _ ⊢ wp true ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
         match eval hnf in e' with Alloc _ => wp_bind_core K end)
@@ -250,7 +250,7 @@ Tactic Notation "wp_alloc" ident(l) :=
 Tactic Notation "wp_load" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- _ ⊢ wp true ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
         match eval hnf in e' with Load _ => wp_bind_core K end)
@@ -266,7 +266,7 @@ Tactic Notation "wp_load" :=
 Tactic Notation "wp_store" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- _ ⊢ wp true ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
         match eval hnf in e' with Store _ _ => wp_bind_core K end)
@@ -285,7 +285,7 @@ Tactic Notation "wp_store" :=
 Tactic Notation "wp_cas_fail" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- _ ⊢ wp true ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
@@ -306,7 +306,7 @@ Tactic Notation "wp_cas_fail" :=
 Tactic Notation "wp_cas_suc" :=
  iStartProof;
  lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- _ ⊢ wp true ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
         match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)

--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -35,23 +35,24 @@ Proof.
 Qed.
 (* Program logic adequacy *)
-Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
+Record adequate {Λ} (p : bool) (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
  adequate_result t2 σ2 v2 :
   rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2;
  adequate_safe t2 σ2 e2 :
+   p →
   rtc step ([e1], σ1) (t2, σ2) →
-   e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2)
+   e2 ∈ t2 → progress e2 σ2
 }.
 Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
-  adequate e1 σ1 φ →
+  adequate true e1 σ1 φ →
  rtc step ([e1], σ1) (t2, σ2) →
  Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
 Proof.
  intros Had ?.
  destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
  apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
-  destruct (adequate_safe e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
+  destruct (adequate_safe true e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
    rewrite ?eq_None_not_Some; auto.
  { exfalso. eauto. }
  destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
@@ -59,19 +60,22 @@ Proof.
 Qed.
 Section adequacy.
-Context `{irisG Λ Σ}.
+Context `{irisG Λ Σ} (p : bool).
 Implicit Types e : expr Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
-Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ)%I.
+Notation world' E σ := (wsat ∗ ownE E ∗ state_interp σ)%I.
+Notation world σ := (world' ⊤ σ).
-Notation wptp t := ([∗ list] ef ∈ t, WP ef {{ _, True }})%I.
+Notation wp' E e Φ := (WP e @ p; E {{ Φ }})%I.
+Notation wp e Φ := (wp' ⊤ e Φ).
+Notation wptp t := ([∗ list] ef ∈ t, WP ef @ p; ⊤ {{ _, True }})%I.
-Lemma wp_step e1 σ1 e2 σ2 efs Φ :
+Lemma wp_step E e1 σ1 e2 σ2 efs Φ :
  prim_step e1 σ1 e2 σ2 efs →
-  world σ1 ∗ WP e1 {{ Φ }} ==∗ ▷ |==> ◇ (world σ2 ∗ WP e2 {{ Φ }} ∗ wptp efs).
+  world' E σ1 ∗ wp' E e1 Φ ==∗ ▷ |==> ◇ (world' E σ2 ∗ wp' E e2 Φ ∗ wptp efs).
 Proof.
  rewrite {1}wp_unfold /wp_pre. iIntros (Hstep) "[(Hw & HE & Hσ) [H|[_ H]]]".
  { iDestruct "H" as (v) "[% _]". apply val_stuck in Hstep; simplify_eq. }
@@ -83,8 +87,8 @@ Qed.
 Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
  step (e1 :: t1,σ1) (t2, σ2) →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1
+  world σ1 ∗ wp e1 Φ ∗ wptp t1
-  ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 {{ Φ }} ∗ wptp t2').
+  ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ wp e2 Φ ∗ wptp t2').
 Proof.
  iIntros (Hstep) "(HW & He & Ht)".
  destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
@@ -98,9 +102,9 @@ Qed.
 Lemma wptp_steps n e1 t1 t2 σ1 σ2 Φ :
  nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢
+  world σ1 ∗ wp e1 Φ ∗ wptp t1 ⊢
  Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ WP e2 {{ Φ }} ∗ wptp t2').
+    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ wp e2 Φ ∗ wptp t2').
 Proof.
  revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=.
  { inversion_clear 1; iIntros "?"; eauto 10. }
@@ -121,7 +125,7 @@ Qed.
 Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
  nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) →
-  world σ1 ∗ WP e1 {{ v, ⌜φ v⌝ }} ∗ wptp t1 ⊢
+  world σ1 ∗ wp e1 (λ v, ⌜φ v⌝) ∗ wptp t1 ⊢
  Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜φ v2⌝.
 Proof.
  intros. rewrite wptp_steps //.
@@ -131,19 +135,19 @@ Proof.
  iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
 Qed.
-Lemma wp_safe e σ Φ :
+Lemma wp_safe E e σ Φ :
-  world σ ∗ WP e {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
+  world' E σ ∗ wp' E e Φ ==∗ ▷ ⌜if p then progress e σ else True⌝.
 Proof.
-  rewrite wp_unfold /wp_pre. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]".
+  rewrite wp_unfold /wp_pre /progress. iIntros "[(Hw&HE&Hσ) [H|[_ H]]]".
-  { iDestruct "H" as (v) "[% _]"; eauto 10. }
+  { iDestruct "H" as (v) "[% _]"; destruct p; eauto 10. }
  rewrite fupd_eq. iMod ("H" with "* Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
-  eauto 10.
+  destruct p; eauto 10.
 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 ⊢
+  world σ1 ∗ wp e1 Φ ∗ wptp t1 ⊢
-  Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
+  Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜if p then progress e2 σ2 else True⌝.
 Proof.
  intros ? He2. rewrite wptp_steps //; rewrite (Nat_iter_S_r (S n)). apply bupd_iter_mono.
  iDestruct 1 as (e2' t2') "(% & Hw & H & Htp)"; simplify_eq.
@@ -153,7 +157,7 @@ Qed.
 Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 φ Φ :
  nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1
+  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ wp e1 Φ ∗ wptp t1
  ⊢ Nat.iter (S (S n)) (λ P, |==> ▷ P) ⌜φ⌝.
 Proof.
  intros ?. rewrite wptp_steps //.
@@ -165,12 +169,12 @@ Proof.
 Qed.
 End adequacy.
-Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ :
+Theorem wp_adequacy Σ Λ `{invPreG Σ} p e σ φ :
  (∀ `{Hinv : invG Σ},
     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ ∗ WP e {{ v, ⌜φ v⌝ }}) →
+       stateI σ ∗ WP e @ p; ⊤ {{ v, ⌜φ v⌝ }}) →
-  adequate e σ φ.
+  adequate p e σ φ.
 Proof.
  intros Hwp; split.
  - intros t2 σ2 v2 [n ?]%rtc_nsteps.
@@ -180,20 +184,20 @@ Proof.
    iDestruct "Hwp" as (Istate) "[HI Hwp]".
    iModIntro. iNext. iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto.
    iFrame. by iApply big_sepL_nil.
-  - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
+  - destruct p; last done. intros t2 σ2 e2 Hp [n ?]%rtc_nsteps ?.
    eapply (soundness (M:=iResUR Σ) _ (S (S (S n)))); iIntros "".
    rewrite Nat_iter_S. iMod wsat_alloc as (Hinv) "[Hw HE]".
    rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
    iDestruct "Hwp" as (Istate) "[HI Hwp]".
-    iModIntro. iNext. iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto.
+    iModIntro. iNext. iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate) true); eauto.
    iFrame. by iApply big_sepL_nil.
 Qed.
-Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ Φ :
+Theorem wp_invariance Σ Λ `{invPreG Σ} p e σ1 t2 σ2 φ Φ :
  (∀ `{Hinv : invG Σ},
     True ={⊤}=∗ ∃ stateI : state Λ → iProp Σ,
       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ1 ∗ WP e {{ Φ }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝)) →
+       stateI σ1 ∗ WP e @ p; ⊤ {{ Φ }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝)) →
  rtc step ([e], σ1) (t2, σ2) →
  φ.
 Proof.

--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -11,56 +11,56 @@ Implicit Types v : val.
 Implicit Types e : expr.
 Hint Resolve head_prim_reducible head_reducible_prim_step.
-Lemma wp_ectx_bind {E e} K Φ :
+Lemma wp_ectx_bind {p E e} K Φ :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+  WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }} ⊢ WP fill K e @ p; E {{ Φ }}.
 Proof. apply: weakestpre.wp_bind. Qed.
-Lemma wp_lift_head_step E Φ e1 :
+Lemma wp_lift_head_step p E Φ e1 :
  to_val e1 = None →
  (∀ σ1, state_interp σ1 ={E,∅}=∗
    ⌜head_reducible e1 σ1⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+      state_interp σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step E)=>//. iIntros (σ1) "Hσ".
+  iIntros (?) "H". iApply wp_lift_step=>//. iIntros (σ1) "Hσ".
  iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
  iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%".
  iApply "H". by eauto.
 Qed.
-Lemma wp_lift_pure_head_step E Φ e1 :
+Lemma wp_lift_pure_head_step p E Φ e1 :
  (∀ σ1, head_reducible e1 σ1) →
  (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
  (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
-    WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
  iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext.
  iIntros (????). iApply "H". eauto.
 Qed.
-Lemma wp_lift_atomic_head_step {E Φ} e1 :
+Lemma wp_lift_atomic_head_step {p E Φ} e1 :
  to_val e1 = None →
  (∀ σ1, state_interp σ1 ={E}=∗
    ⌜head_reducible e1 σ1⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
      state_interp σ2 ∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
  iSplit; first by eauto. iNext. iIntros (e2 σ2 efs) "%". iApply "H"; auto.
 Qed.
-Lemma wp_lift_atomic_head_step_no_fork {E Φ} e1 :
+Lemma wp_lift_atomic_head_step_no_fork {p E Φ} e1 :
  to_val e1 = None →
  (∀ σ1, state_interp σ1 ={E}=∗
    ⌜head_reducible e1 σ1⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
      ⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
-  ⊢ WP e1 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
  iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
@@ -69,20 +69,20 @@ Proof.
  by iApply big_sepL_nil.
 Qed.
-Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
+Lemma wp_lift_pure_det_head_step {p E Φ} e1 e2 efs :
  (∀ σ1, head_reducible e1 σ1) →
  (∀ σ1 e2' σ2 efs',
    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-  ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof. eauto using wp_lift_pure_det_step. Qed.
-Lemma wp_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
+Lemma wp_lift_pure_det_head_step_no_fork {p E Φ} e1 e2 :
  to_val e1 = None →
  (∀ σ1, head_reducible e1 σ1) →
  (∀ σ1 e2' σ2 efs',
    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
-  ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+  ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
 Qed.

--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -2,24 +2,42 @@ From iris.program_logic Require Export weakestpre.
 From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
-Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
+Definition ht `{irisG Λ Σ} (p : bool) (E : coPset) (P : iProp Σ)
    (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
-  (□ (P -∗ WP e @ E {{ Φ }}))%I.
+  (□ (P -∗ WP e @ p; E {{ Φ }}))%I.
-Instance: Params (@ht) 4.
+Instance: Params (@ht) 5.
-Notation "{{ P } } e @ E {{ Φ } }" := (ht E P%I e%E Φ%I)
+Notation "{{ P } } e @ p ; E {{ Φ } }" := (ht p E P%I e%E Φ%I)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  p ;  E  {{  Φ  } }") : C_scope.
+Notation "{{ P } } e @ E {{ Φ } }" := (ht true E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
-Notation "{{ P } } e {{ Φ } }" := (ht ⊤ P%I e%E Φ%I)
+Notation "{{ P } } e @ E ? {{ Φ } }" := (ht false E P%I e%E Φ%I)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  @  E  ? {{  Φ  } }") : C_scope.
+Notation "{{ P } } e {{ Φ } }" := (ht true ⊤ P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  {{  Φ  } }") : C_scope.
+Notation "{{ P } } e ? {{ Φ } }" := (ht false ⊤ P%I e%E Φ%I)
+  (at level 20, P, e, Φ at level 200,
+   format "{{  P  } }  e  ? {{  Φ  } }") : C_scope.
-Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e @ p ; E {{ v , Q } }" := (ht p E P%I e%E (λ v, Q)%I)
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  @  p ;  E  {{  v ,  Q  } }") : C_scope.
+Notation "{{ P } } e @ E {{ v , Q } }" := (ht true E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
-Notation "{{ P } } e {{ v , Q } }" := (ht ⊤ P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht false E P%I e%E (λ v, Q)%I)
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  @  E  ? {{  v ,  Q  } }") : C_scope.
+Notation "{{ P } } e {{ v , Q } }" := (ht true ⊤ P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.
+Notation "{{ P } } e ? {{ v , Q } }" := (ht false ⊤ P%I e%E (λ v, Q)%I)
+  (at level 20, P, e, Q at level 200,
+   format "{{  P  } }  e  ? {{  v ,  Q  } }") : C_scope.
 Section hoare.
 Context `{irisG Λ Σ}.
@@ -28,100 +46,106 @@ Implicit Types Φ Ψ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Import uPred.
-Global Instance ht_ne E n :
+Global Instance ht_ne p E n :
-  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (ht E).
+  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (ht p E).
 Proof. solve_proper. Qed.
-Global Instance ht_proper E :
+Global Instance ht_proper p E :
-  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht E).
+  Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht p E).
 Proof. solve_proper. Qed.
-Lemma ht_mono E P P' Φ Φ' e :
+Lemma ht_mono p E P P' Φ Φ' e :
-  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ E {{ Φ' }} ⊢ {{ P }} e @ E {{ Φ }}.
+  (P ⊢ P') → (∀ v, Φ' v ⊢ Φ v) → {{ P' }} e @ p; E {{ Φ' }} ⊢ {{ P }} e @ p; E {{ Φ }}.
 Proof. by intros; apply always_mono, wand_mono, wp_mono. Qed.
-Global Instance ht_mono' E :
+Global Instance ht_mono' p E :
-  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht E).
+  Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht p E).
 Proof. solve_proper. Qed.
-Lemma ht_alt E P Φ e : (P ⊢ WP e @ E {{ Φ }}) → {{ P }} e @ E {{ Φ }}.
+Lemma ht_alt p E P Φ e : (P ⊢ WP e @ p; E {{ Φ }}) → {{ P }} e @ p; E {{ Φ }}.
 Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.
-Lemma ht_val E v : {{ True }} of_val v @ E {{ v', ⌜v = v'⌝ }}.
+Lemma ht_val p E v : {{ True }} of_val v @ p; E {{ v', ⌜v = v'⌝ }}.
 Proof. iIntros "!# _". by iApply wp_value'. Qed.
-Lemma ht_vs E P P' Φ Φ' e :
+Lemma ht_vs p E P P' Φ Φ' e :
-  (P ={E}=> P') ∧ {{ P' }} e @ E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
+  (P ={E}=> P') ∧ {{ P' }} e @ p; E {{ Φ' }} ∧ (∀ v, Φ' v ={E}=> Φ v)
-  ⊢ {{ P }} e @ E {{ Φ }}.
+  ⊢ {{ P }} e @ p; E {{ Φ }}.
 Proof.
  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
  iApply wp_fupd. iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
  iIntros (v) "Hv". by iApply "HΦ".
 Qed.
-Lemma ht_atomic E1 E2 P P' Φ Φ' e :
+Lemma ht_atomic p E1 E2 P P' Φ Φ' e :
  atomic e →
-  (P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
+  (P ={E1,E2}=> P') ∧ {{ P' }} e @ p; E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
-  ⊢ {{ P }} e @ E1 {{ Φ }}.
+  ⊢ {{ P }} e @ p; E1 {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ E2); auto.
+  iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ _ E2); auto.
  iMod ("Hvs" with "HP") as "HP". iModIntro.
  iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
  iIntros (v) "Hv". by iApply "HΦ".
 Qed.
-Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
+Lemma ht_bind `{LanguageCtx Λ K} p E P Φ Φ' e :
-  {{ P }} e @ E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
+  {{ P }} e @ p; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ p; E {{ Φ' }})
-  ⊢ {{ P }} K e @ E {{ Φ' }}.
+  ⊢ {{ P }} K e @ p; E {{ Φ' }}.
 Proof.
  iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
  iApply (wp_wand with "[HP]"); [by iApply "Hwpe"|].
  iIntros (v) "Hv". by iApply "HwpK".
 Qed.
-Lemma ht_mask_weaken E1 E2 P Φ e :
+Lemma ht_forget_progress E P Φ e :
-  E1 ⊆ E2 → {{ P }} e @ E1 {{ Φ }} ⊢ {{ P }} e @ E2 {{ Φ }}.
+  {{ P }} e @ E {{ Φ }} ⊢ {{ P }} e @ E ?{{ Φ }}.
+Proof.
+  by iIntros "#Hwp !# ?"; iApply wp_forget_progress; iApply "Hwp".
+Qed.
+Lemma ht_mask_weaken p E1 E2 P Φ e :
+  E1 ⊆ E2 → {{ P }} e @ p; E1 {{ Φ }} ⊢ {{ P }} e @ p; E2 {{ Φ }}.
 Proof.
-  iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono E1 E2); try done.
+  iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono _ E1 E2); try done.
  by iApply "Hwp".
 Qed.
-Lemma ht_frame_l E P Φ R e :
+Lemma ht_frame_l p E P Φ R e :
-  {{ P }} e @ E {{ Φ }} ⊢ {{ R ∗ P }} e @ E {{ v, R ∗ Φ v }}.
+  {{ P }} e @ p; E {{ Φ }} ⊢ {{ R ∗ P }} e @ p; E {{ v, R ∗ Φ v }}.
 Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.
-Lemma ht_frame_r E P Φ R e :
+Lemma ht_frame_r p E P Φ R e :
-  {{ P }} e @ E {{ Φ }} ⊢ {{ P ∗ R }} e @ E {{ v, Φ v ∗ R }}.
+  {{ P }} e @ p; E {{ Φ }} ⊢ {{ P ∗ R }} e @ p; E {{ v, Φ v ∗ R }}.
 Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
-Lemma ht_frame_step_l E1 E2 P R1 R2 e Φ :
+Lemma ht_frame_step_l p E1 E2 P R1 R2 e Φ :
  to_val e = None → E2 ⊆ E1 →
-  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }}
+  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ p; E2 {{ Φ }}
-  ⊢ {{ R1 ∗ P }} e @ E1 {{ λ v, R2 ∗ Φ v }}.
+  ⊢ {{ R1 ∗ P }} e @ p; E1 {{ λ v, R2 ∗ Φ v }}.
 Proof.
  iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
-  iApply (wp_frame_step_l E1 E2); try done.
+  iApply (wp_frame_step_l _ E1 E2); try done.
  iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
 Qed.
-Lemma ht_frame_step_r E1 E2 P R1 R2 e Φ :
+Lemma ht_frame_step_r p E1 E2 P R1 R2 e Φ :
  to_val e = None → E2 ⊆ E1 →
-  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ E2 {{ Φ }}
+  (R1 ={E1,E2}=> ▷ |={E2,E1}=> R2) ∧ {{ P }} e @ p; E2 {{ Φ }}
-  ⊢ {{ P ∗ R1 }} e @ E1 {{ λ v, Φ v ∗ R2 }}.
+  ⊢ {{ P ∗ R1 }} e @ p; E1 {{ λ v, Φ v ∗ R2 }}.
 Proof.
  iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
-  iApply (wp_frame_step_r E1 E2); try done.
+  iApply (wp_frame_step_r _ E1 E2); try done.
  iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
 Qed.
-Lemma ht_frame_step_l' E P R e Φ :
+Lemma ht_frame_step_l' p E P R e Φ :
  to_val e = None →
-  {{ P }} e @ E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ E {{ v, R ∗ Φ v }}.
+  {{ P }} e @ p; E {{ Φ }} ⊢ {{ ▷ R ∗ P }} e @ p; E {{ v, R ∗ Φ v }}.
 Proof.
  iIntros (?) "#Hwp !# [HR HP]".
  iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
 Qed.
-Lemma ht_frame_step_r' E P Φ R e :
+Lemma ht_frame_step_r' p E P Φ R e :
  to_val e = None →
-  {{ P }} e @ E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ E {{ v, Φ v ∗ R }}.
+  {{ P }} e @ p; E {{ Φ }} ⊢ {{ P ∗ ▷ R }} e @ p; E {{ v, Φ v ∗ R }}.
 Proof.
  iIntros (?) "#Hwp !# [HP HR]".
  iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".

--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -36,6 +36,8 @@ Section language.
    ∃ e' σ' efs, prim_step e σ e' σ' efs.
  Definition atomic (e : expr Λ) : Prop :=
    ∀ σ e' σ' efs, prim_step e σ e' σ' efs → is_Some (to_val e').
+  Definition progress (e : expr Λ) (σ : state Λ) :=
+    is_Some (to_val e) ∨ reducible e σ.
  Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
    | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
       ρ1 = (t1 ++ e1 :: t2, σ1) →

--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -10,22 +10,36 @@ Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
-Lemma wp_lift_step E Φ e1 :
+Lemma wp_lift_step p E Φ e1 :
  to_val e1 = None →
  (∀ σ1, state_interp σ1 ={E,∅}=∗
    ⌜reducible e1 σ1⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
-      state_interp σ2 ∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+      state_interp σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
-Proof. iIntros (?) "H". rewrite wp_unfold /wp_pre; auto. Qed.
+Proof.
+  iIntros (?) "H". rewrite wp_unfold /wp_pre. destruct p; first by auto.
+  iRight; iSplit; first done. iIntros (?) "Hσ"; iMod ("H" $! _ with "Hσ") as "(_&?)"; by auto.
+Qed.
+Lemma wp_lift_stuck E Φ e :
+  to_val e = None →
+  (∀ σ, state_interp σ ={E,∅}=∗ ⌜¬ progress e σ⌝)
+  ⊢ WP e @ E ?{{ Φ }}.
+Proof.
+  iIntros (?) "H"; rewrite wp_unfold /wp_pre; iRight; iSplit; first done.
+  iIntros (σ) "Hσ"; iMod ("H" $! _ with "Hσ") as "#H"; iDestruct "H" as % Hstuck.
+  iModIntro; iSplit; first done; iNext; iIntros (e' σ' efs Hstep); exfalso.
+  by apply Hstuck; right; exists e', σ', efs.
+Qed.
 (** Derived lifting lemmas. *)
-Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
+Lemma wp_lift_pure_step `{Inhabited (state Λ)} p E Φ e1 :
  (∀ σ1, reducible e1 σ1) →
  (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
  (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
-    WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
  { eapply reducible_not_val, (Hsafe inhabitant). }
@@ -35,16 +49,27 @@ Proof.
  iMod "Hclose"; iModIntro. iFrame "Hσ". iApply "H"; auto.
 Qed.
-Lemma wp_lift_atomic_step {E Φ} e1 :
+Lemma wp_lift_pure_stuck `{Inhabited (state Λ)} E Φ e :
+  (∀ σ, ¬ progress e σ) →
+  True ⊢ WP e @ E ?{{ Φ }}.
+Proof.
+  iIntros (Hstuck) "". iApply wp_lift_stuck.
+  - destruct(to_val e) as [v|] eqn:He; last done.
+    by exfalso; apply (Hstuck inhabitant); left; exists v.
+  - iIntros (σ) "_"; iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
+    by iModIntro; iPureIntro; apply Hstuck.
+Qed.
+Lemma wp_lift_atomic_step {p E Φ} e1 :
  to_val e1 = None →
  (∀ σ1, state_interp σ1 ={E}=∗
    ⌜reducible e1 σ1⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
      state_interp σ2 ∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step E _ e1)=>//; iIntros (σ1) "Hσ1".
+  iIntros (?) "H". iApply (wp_lift_step p E _ e1)=>//; iIntros (σ1) "Hσ1".
  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
  iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
  iModIntro; iNext; iIntros (e2 σ2 efs) "%". iMod "Hclose" as "_".
@@ -53,13 +78,13 @@ Proof.
  by iApply wp_value.
 Qed.
-Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
+Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {p E Φ} e1 e2 efs :
  (∀ σ1, reducible e1 σ1) →
  (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-  ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ E {{ Φ }}.
+  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
-  iIntros (? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
+  iIntros (? Hpuredet) "?". iApply (wp_lift_pure_step p E); try done.
  by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 End lifting.
--- 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 σ φ :
+Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} p e σ φ :
-  (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e {{ v, ⌜φ v⌝ }}) →
+  (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e @ p; ⊤ {{ v, ⌜φ v⌝ }}) →
-  adequate e σ φ.
+  adequate p e σ φ.
 Proof.
  intros Hwp. apply (wp_adequacy Σ _).
  iIntros (?) "". iMod (own_alloc (● (Excl' (σ : leibnizC _)) ⋅ ◯ (Excl' σ)))
@@ -50,13 +50,13 @@ Proof.
  iApply (Hwp (OwnPG _ _ _ _ γσ)). by rewrite /ownP.
 Qed.
-Theorem ownP_invariance Σ `{ownPPreG Λ Σ} e σ1 t2 σ2 φ Φ :
+Theorem ownP_invariance Σ `{ownPPreG Λ Σ} p e σ1 t2 σ2 φ Φ :
  (∀ `{ownPG Λ Σ},
-    ownP σ1 ={⊤}=∗ WP e {{ Φ }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
+    ownP σ1 ={⊤}=∗ WP e @ p; ⊤ {{ Φ }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
  rtc step ([e], σ1) (t2, σ2) →
  φ σ2.
 Proof.
-  intros Hwp Hsteps. eapply (wp_invariance Σ Λ e σ1 t2 σ2 _ Φ)=> //.
+  intros Hwp Hsteps. eapply (wp_invariance Σ Λ p e σ1 t2 σ2 _ Φ)=> //.
  iIntros (?) "". iMod (own_alloc (● (Excl' (σ1 : leibnizC _)) ⋅ ◯ (Excl' σ1)))
    as (γσ) "[Hσ Hσf]"; first done.
  iExists (λ σ, own γσ (● (Excl' (σ:leibnizC _)))). iFrame "Hσ".
@@ -78,11 +78,11 @@ Section lifting.
  Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
  Proof. rewrite /ownP; apply _. Qed.
-  Lemma ownP_lift_step E Φ e1 :
+  Lemma ownP_lift_step p E Φ e1 :
    (|={E,∅}=> ∃ σ1, ⌜reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-            ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+            ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
    iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
    - apply of_to_val in EQe1 as <-. iApply fupd_wp.
@@ -99,12 +99,26 @@ Section lifting.
      iFrame "Hσ". iApply ("H" with "* []"); eauto.
  Qed.
-  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
+  Lemma ownP_lift_stuck E Φ e :
+    (|={E,∅}=> ∃ σ, ⌜¬ progress e σ⌝ ∗ ▷ ownP σ)
+    ⊢ WP e @ E ?{{ Φ }}.
+  Proof.
+    iIntros "H". destruct (to_val e) as [v|] eqn:EQe.
+    - apply of_to_val in EQe as <-; iApply fupd_wp.
+      iMod "H" as (σ1) "[#H _]"; iDestruct "H" as %Hstuck; exfalso.
+      by apply Hstuck; left; rewrite to_of_val; exists v.
+    - iApply wp_lift_stuck; [done|]; iIntros (σ1) "Hσ".
+      iMod "H" as (σ1') "(% & >Hσf)"; rewrite /ownP.
+      by iDestruct (own_valid_2 with "Hσ Hσf")
+        as %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+  Qed.
+  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} p E Φ e1 :
    (∀ σ1, reducible e1 σ1) →
    (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
    (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
-      WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+      WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
    iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
    { eapply reducible_not_val, (Hsafe inhabitant). }
@@ -115,13 +129,13 @@ Section lifting.
  Qed.
  (** Derived lifting lemmas. *)
-  Lemma ownP_lift_atomic_step {E Φ} e1 σ1 :
+  Lemma ownP_lift_atomic_step {p E Φ} e1 σ1 :
    reducible e1 σ1 →
    (▷ ownP σ1 ∗ ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
-    iIntros (?) "[Hσ H]". iApply (ownP_lift_step E _ e1).
+    iIntros (?) "[Hσ H]". iApply ownP_lift_step.
    iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver. iModIntro.
    iExists σ1. iFrame "Hσ"; iSplit; eauto.
    iNext; iIntros (e2 σ2 efs) "% Hσ".
@@ -130,28 +144,49 @@ Section lifting.
    iMod "Hclose". iApply wp_value; auto using to_of_val. done.
  Qed.
-  Lemma ownP_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
+  Lemma ownP_lift_atomic_det_step {p E Φ e1} σ1 v2 σ2 efs :
    reducible e1 σ1 →
    (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
                     σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
-      Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+      Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
-    iIntros (? Hdet) "[Hσ1 Hσ2]". iApply (ownP_lift_atomic_step _ σ1); try done.
+    iIntros (? Hdet) "[Hσ1 Hσ2]". iApply ownP_lift_atomic_step; try done.
    iFrame. iNext. iIntros (e2' σ2' efs') "% Hσ2'".
    edestruct Hdet as (->&Hval&->). done. rewrite Hval. by iApply "Hσ2".
  Qed.
-  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
+  (* PDS: Does anyone use this? Why had it only been proved for ectx languages? *)
+  Lemma ownP_lift_atomic_det_step_no_fork {p E e1} σ1 v2 σ2 :
+    reducible e1 σ1 →
+    (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
+      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
+    {{{ ▷ ownP σ1 }}} e1 @ p; E {{{ RET v2; ownP σ2 }}}.
+  Proof.
+    intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
+    rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
+  Qed.
+  Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {p E Φ} e1 e2 efs :
    (∀ σ1, reducible e1 σ1) →
    (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
-    ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
-    iIntros (? Hpuredet) "?". iApply (ownP_lift_pure_step E); try done.
+    iIntros (? Hpuredet) "?". iApply ownP_lift_pure_step; try done.
    by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
  Qed.
+  (* PDS: Does anyone use this? Why had it only been proved for ectx languages? *)
+  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {p E Φ} e1 e2 :
+    to_val e1 = None →
+    (∀ σ1, reducible e1 σ1) →
+    (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
+  Proof.
+    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
+  Qed.
 End lifting.
 Section ectx_lifting.
@@ -162,71 +197,66 @@ Section ectx_lifting.
  Implicit Types e : expr.
  Hint Resolve head_prim_reducible head_reducible_prim_step.
-  Lemma ownP_lift_head_step E Φ e1 :
+  Lemma ownP_lift_head_step p E Φ e1 :
    (|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
      ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
-            ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+            ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
-    iIntros "H". iApply (ownP_lift_step E); try done.
+    iIntros "H". iApply ownP_lift_step.
    iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
    iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
    iApply ("Hwp" with "* []"); by eauto.
  Qed.
-  Lemma ownP_lift_pure_head_step E Φ e1 :
+  Lemma ownP_lift_pure_head_step p E Φ e1 :
    (∀ σ1, head_reducible e1 σ1) →
    (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
    (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
-      WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+      WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
    iIntros (??) "H". iApply ownP_lift_pure_step; eauto. iNext.
    iIntros (????). iApply "H". eauto.
  Qed.
-  Lemma ownP_lift_atomic_head_step {E Φ} e1 σ1 :
+  Lemma ownP_lift_atomic_head_step {p E Φ} e1 σ1 :
    head_reducible e1 σ1 →
    ▷ ownP σ1 ∗ ▷ (∀ e2 σ2 efs,
    ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
-      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
    iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto. iFrame. iNext.
    iIntros (???) "% ?". iApply ("H" with "* []"); eauto.
  Qed.
-  Lemma ownP_lift_atomic_det_head_step {E Φ e1} σ1 v2 σ2 efs :
+  Lemma ownP_lift_atomic_det_head_step {p E Φ e1} σ1 v2 σ2 efs :
    head_reducible e1 σ1 →
    (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
-    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗ Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof. eauto using ownP_lift_atomic_det_step. Qed.
-  Lemma ownP_lift_atomic_det_head_step_no_fork {E e1} σ1 v2 σ2 :
+  Lemma ownP_lift_atomic_det_head_step_no_fork {p E e1} σ1 v2 σ2 :
    head_reducible e1 σ1 →
    (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
-    {{{ ▷ ownP σ1 }}} e1 @ E {{{ RET v2; ownP σ2 }}}.
+    {{{ ▷ ownP σ1 }}} e1 @ p; E {{{ RET v2; ownP σ2 }}}.
-  Proof.
+  Proof. eauto using ownP_lift_atomic_det_step_no_fork.  Qed.
-    intros. rewrite -(ownP_lift_atomic_det_head_step σ1 v2 σ2 []); [|done..].
-    rewrite big_sepL_nil right_id. by apply uPred.wand_intro_r.
-  Qed.
-  Lemma ownP_lift_pure_det_head_step {E Φ} e1 e2 efs :
+  Lemma ownP_lift_pure_det_head_step {p E Φ} e1 e2 efs :
    (∀ σ1, head_reducible e1 σ1) →
    (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
-    ▷ (WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
-    ⊢ WP e1 @ E {{ Φ }}.
+    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof. eauto using wp_lift_pure_det_step. Qed.
-  Lemma ownP_lift_pure_det_head_step_no_fork {E Φ} e1 e2 :
+  Lemma ownP_lift_pure_det_head_step_no_fork {p E Φ} e1 e2 :
    to_val e1 = None →
    (∀ σ1, head_reducible e1 σ1) →
    (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
-    ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
+    ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
-  Proof.
+  Proof. eauto using ownP_lift_pure_det_step_no_fork. Qed.
-    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
-  Qed.
 End ectx_lifting.
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
--- a/theories/tests/barrier_client.v
+++ b/theories/tests/barrier_client.v
@@ -59,7 +59,7 @@ Section ClosedProofs.
 Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
-Lemma client_adequate σ : adequate client σ (λ _, True).
+Lemma client_adequate σ : adequate true client σ (λ _, True).
 Proof. apply (heap_adequacy Σ)=> ?. apply client_safe. Qed.
 End ClosedProofs.

--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -62,5 +62,5 @@ Section LiftingTests.
  Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
-Lemma heap_e_adequate σ : adequate heap_e σ (= #2).
+Lemma heap_e_adequate σ : adequate true heap_e σ (= #2).
 Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.