Adjust lifting lemmas for progress bits.

3742f4c2 · David Swasey · 3803dc19 · 3742f4c2 · 3742f4c2 · 3742f4c2
Commit 3742f4c2 authored Dec 18, 2016 by David Swasey
5 changed files
--- 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;

--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -6,11 +6,13 @@ 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 p : bool.
 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).

 Definition head_progressive (e : expr) (σ : state) :=
  is_Some(to_val e) ∨ ∃ K e', e = fill K e' ∧ head_reducible e' σ.
@@ -25,11 +27,13 @@ Qed.
 Hint Resolve progressive_head_progressive.

 Lemma wp_ectx_bind {p E e} K Φ :
-  WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }} ⊢ WP fill K e @ p; E {{ Φ }}.
+  WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }}
+  ⊢ WP fill K e @ p; E {{ Φ }}.
 Proof. apply: weakestpre.wp_bind. Qed.

 Lemma wp_ectx_bind_inv {p E Φ} K e :
-  WP fill K e @ p; E {{ Φ }} ⊢ WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }}.
+  WP fill K e @ p; E {{ Φ }}
+  ⊢ WP e @ p; E {{ v, WP fill K (of_val v) @ p; E {{ Φ }} }}.
 Proof. apply: weakestpre.wp_bind_inv. Qed.

 Lemma wp_lift_head_step {p E Φ} e1 :
@@ -41,9 +45,28 @@ Lemma wp_lift_head_step {p E Φ} e1 :
  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
  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.
+  iMod ("H" with "Hσ") as "[% H]"; iModIntro.
+  iSplit; first by destruct p; eauto. iNext. iIntros (e2 σ2 efs) "%".
+  iApply "H"; eauto.
+Qed.
+
+(*
+  PDS: Discard. It's confusing. In practice, we just need rules
+  like wp_lift_head_{step,stuck}.
+*)
+Lemma wp_strong_lift_head_step p E Φ e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E,∅}=∗
+    ⌜if p then head_reducible e1 σ1 else True⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+      state_interp σ2 ∗ WP e2 @ p; E {{ Φ }}
+      ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof.
+  iIntros (?) "H". iApply wp_lift_step=>//. iIntros (σ1) "Hσ".
+  iMod ("H" with "Hσ") as "[% H]"; iModIntro.
+  iSplit; first by destruct p; eauto. iNext. iIntros (e2 σ2 efs) "%".
+  iApply "H"; eauto.
 Qed.

 Lemma wp_lift_head_stuck E Φ e :
@@ -52,7 +75,7 @@ Lemma wp_lift_head_stuck E Φ e :
  ⊢ WP e @ E ?{{ Φ }}.
 Proof.
  iIntros (?) "H". iApply wp_lift_stuck; first done.
-  iIntros (σ) "Hσ". iMod ("H" $! _ with "Hσ") as "%". iModIntro. by auto.
+  iIntros (σ) "Hσ". iMod ("H" with "Hσ") as "%". by auto. 
 Qed.

 Lemma wp_lift_pure_head_step {p E E' Φ} e1 :
@@ -63,42 +86,71 @@ Lemma wp_lift_pure_head_step {p E E' Φ} e1 :
  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof using Hinh.
  iIntros (??) "H". iApply wp_lift_pure_step; eauto.
+  { by destruct p; auto. }
  iApply (step_fupd_wand with "H"); iIntros "H".
  iIntros (????). iApply "H"; eauto.
 Qed.

-Lemma wp_lift_pure_head_stuck `{Inhabited state} E Φ e :
+(* PDS: Discard. *)
+Lemma wp_strong_lift_pure_head_step p E Φ e1 :
+  to_val e1 = None →
+  (∀ σ1, if p then head_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 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof using Hinh.
+  iIntros (???) "H". iApply wp_lift_pure_step; eauto. by destruct p; auto.
+Qed.
+
+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.
+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 {p E Φ} e1 :
+Lemma wp_lift_atomic_head_step {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 @ p; ⊤ {{ _, True }})
-  ⊢ WP e1 @ p; E {{ Φ }}.
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+  ⊢ WP e1 @ 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 {p E Φ} e1 :
+(* PDS: Discard. *)
+Lemma wp_strong_lift_atomic_head_step {p E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜if p then head_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 @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof.
+  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
+  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct p; eauto.
+  by iNext; iIntros (e2 σ2 efs ?); iApply "H"; eauto.
+Qed.
+
+Lemma wp_lift_atomic_head_step_no_fork {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 @ p; E {{ Φ }}.
+  ⊢ WP e1 @ E {{ Φ }}.
 Proof.
  iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
@@ -106,13 +158,45 @@ Proof.
  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
 Qed.

+(* PDS: Discard. *)
+Lemma wp_strong_lift_atomic_head_step_no_fork {p E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜if p then head_reducible e1 σ1 else True⌝ ∗
+    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      ⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof.
+  iIntros (?) "H". iApply wp_strong_lift_atomic_head_step; eauto.
+  iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[$ H]"; iModIntro.
+  iNext; iIntros (v2 σ2 efs) "%".
+  iMod ("H" with "[#]") as "(% & $ & $)"=>//; subst.
+  by iApply big_sepL_nil.
+Qed.
+
 Lemma wp_lift_pure_det_head_step {p E E' Φ} e1 e2 efs :
  (∀ σ1, head_reducible e1 σ1) →
  (∀ σ1 e2' σ2 efs',
    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
  (|={E,E'}▷=> WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
  ⊢ WP e1 @ p; E {{ Φ }}.
-Proof using Hinh. eauto using wp_lift_pure_det_step. Qed.
+Proof using Hinh.
+  intros. rewrite -(wp_lift_pure_det_step e1 e2 efs); eauto.
+  destruct p; by auto.
+Qed.
+
+(* PDS: Discard. *)
+Lemma wp_strong_lift_pure_det_head_step {p E Φ} e1 e2 efs :
+  to_val e1 = None →
+  (∀ σ1, if p then head_reducible e1 σ1 else True) →
+  (∀ σ1 e2' σ2 efs',
+    prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+  ▷ (WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
+  ⊢ WP e1 @ p; E {{ Φ }}.
+Proof using Hinh.
+  iIntros (???) "H"; iApply wp_lift_pure_det_step; eauto.
+  by destruct p; eauto.
+Qed.

 Lemma wp_lift_pure_det_head_step_no_fork {p E E' Φ} e1 e2 :
  to_val e1 = None →
@@ -122,6 +206,7 @@ Lemma wp_lift_pure_det_head_step_no_fork {p E E' Φ} e1 e2 :
  (|={E,E'}▷=> WP e2 @ p; E {{ Φ }}) ⊢ WP e1 @ p; E {{ Φ }}.
 Proof using Hinh.
  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
+  destruct p; by auto.
 Qed.

 Lemma wp_lift_pure_det_head_step_no_fork' {p E Φ} e1 e2 :
@@ -129,9 +214,21 @@ Lemma wp_lift_pure_det_head_step_no_fork' {p E Φ} e1 e2 :
  (∀ σ1, head_reducible e1 σ1) →
  (∀ σ1 e2' σ2 efs',
    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
-  ▷ WP e2 @ p; E {{ Φ }} ⊢ WP e1 @ p; E {{ Φ }}.
+  ▷ WP e2 @ E {{ Φ }} ⊢ WP e1 @ E {{ Φ }}.
 Proof using Hinh.
-  intros. rewrite -[(WP e1 @ _; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
+  intros. rewrite -[(WP e1 @ _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
  rewrite -step_fupd_intro //.
 Qed.
+
+(* PDS: Discard. *)
+Lemma wp_strong_lift_pure_det_head_step_no_fork {p E Φ} e1 e2 :
+  to_val e1 = None →
+  (∀ σ1, if p then head_reducible e1 σ1 else True) →
+  (∀ σ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 using Hinh.
+  intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
+  by destruct p; eauto.
+Qed.
 End wp.
--- 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;

--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -5,6 +5,7 @@ Set Default Proof Using "Type".

 Section lifting.
 Context `{irisG Λ Σ}.
+Implicit Types p : bool.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 Implicit Types σ : state Λ.
@@ -14,7 +15,7 @@ Implicit Types Φ : val Λ → iProp Σ.
 Lemma wp_lift_step p E Φ e1 :
  to_val e1 = None →
  (∀ σ1, state_interp σ1 ={E,∅}=∗
-    ⌜reducible e1 σ1⌝ ∗
+    ⌜if p then reducible e1 σ1 else True⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
      state_interp σ2 ∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
  ⊢ WP e1 @ p; E {{ Φ }}.
@@ -36,17 +37,17 @@ Qed.

 (** Derived lifting lemmas. *)
 Lemma wp_lift_pure_step `{Inhabited (state Λ)} p E E' Φ e1 :
-  (∀ σ1, reducible e1 σ1) →
+  to_val e1 = None →
+  (∀ σ1, if p 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 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
-  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
-  { eapply reducible_not_val, (Hsafe inhabitant). }
+  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.
@@ -67,7 +68,7 @@ Qed.
 Lemma wp_lift_atomic_step {p E Φ} e1 :
  to_val e1 = None →
  (∀ σ1, state_interp σ1 ={E}=∗
-    ⌜reducible e1 σ1⌝ ∗
+    ⌜if p 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 @ p; ⊤ {{ _, True }})
@@ -83,12 +84,13 @@ Proof.
 Qed.

 Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {p E E' Φ} e1 e2 efs :
-  (∀ σ1, reducible e1 σ1) →
+  to_val e1 = None →
+  (∀ σ1, if p 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 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
  ⊢ WP e1 @ p; E {{ Φ }}.
 Proof.
-  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step p E); try done.
+  iIntros (?? Hpuredet) "H". iApply (wp_lift_pure_step p E E'); try done.
  { by intros; eapply Hpuredet. }
  iApply (step_fupd_wand with "H"); iIntros "H".
  by iIntros (e' efs' σ (_&->&->)%Hpuredet).
@@ -100,8 +102,9 @@ Lemma wp_pure_step_fupd `{Inhabited (state Λ)} E E' e1 e2 φ Φ :
  (|={E,E'}▷=> WP e2 @ E {{ Φ }}) ⊢ WP e1 @ 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]"); [|naive_solver|naive_solver|].
+  - apply (reducible_not_val _ inhabitant). by auto.
+  - by rewrite big_sepL_nil right_id.
 Qed.

 Lemma wp_pure_step_later `{Inhabited (state Λ)} E e1 e2 φ Φ :

--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -61,7 +61,7 @@ Proof.
    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,33 +70,36 @@ Qed.
 (** Lifting *)
 Section lifting.
  Context `{ownPG Λ Σ}.
+  Implicit Types p : bool.
  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 p E Φ e1 :
-    (|={E,∅}=> ∃ σ1, ⌜reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
+    to_val e1 = None →
+    (|={E,∅}=> ∃ σ1, ⌜if p then reducible e1 σ1 else True⌝ ∗ ▷ ownP σ1 ∗
      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
            ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
-    iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
-    - apply of_to_val in EQe1 as <-. iApply fupd_wp.
-      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.
+    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 :
@@ -108,57 +111,59 @@ Section lifting.
      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.
+      iMod "H" as (σ1') "(% & >Hσf)".
+      by iDestruct (ownP_eq with "Hσ Hσf") as %->.
  Qed.

-  Lemma ownP_lift_pure_step `{Inhabited (state Λ)} p E Φ e1 :
-    (∀ σ1, reducible e1 σ1) →
+  Lemma ownP_lift_pure_step p E Φ e1 :
+    to_val e1 = None →
+    (∀ σ1, if p 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 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤ {{ _, True }})
    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
-    iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
-    { eapply reducible_not_val, (Hsafe inhabitant). }
+    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 p|]; 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 {p E Φ} e1 σ1 :
-    reducible e1 σ1 →
+    to_val e1 = None →
+    (if p 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 @ p; ⊤ {{ _, True }})
    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
-    iIntros (?) "[Hσ H]". iApply ownP_lift_step.
-    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 p.
    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 {p E Φ e1} σ1 v2 σ2 efs :
-    reducible e1 σ1 →
+    to_val e1 = None →
+    (if p 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 @ p; ⊤ {{ _, True }})
    ⊢ WP e1 @ p; 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. rewrite Hval. by iApply "Hσ2".
+    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 {p E e1} σ1 v2 σ2 :
-    reducible e1 σ1 →
+    to_val e1 = None →
+    (if p 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 @ p; E {{{ RET v2; ownP σ2 }}}.
@@ -167,19 +172,20 @@ Section lifting.
    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) →
+  Lemma ownP_lift_pure_det_step {p E Φ} e1 e2 efs :
+    to_val e1 = None →
+    (∀ σ1, if p 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 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
    ⊢ WP e1 @ p; E {{ Φ }}.
  Proof.
-    iIntros (? Hpuredet) "?". iApply ownP_lift_pure_step; try done.
-    by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
+    iIntros (?? Hpuredet) "?"; iApply ownP_lift_pure_step=>//.
+    by apply Hpuredet. by iNext; iIntros (e' efs' σ (_&->&->)%Hpuredet).
  Qed.

  Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {p E Φ} e1 e2 :
    to_val e1 = None →
-    (∀ σ1, reducible e1 σ1) →
+    (∀ σ1, if p then reducible e1 σ1 else True) →
    (∀ σ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.
@@ -191,70 +197,166 @@ 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 p : bool.
  Implicit Types Φ : val → iProp Σ.
  Implicit Types e : expr.
  Hint Resolve head_prim_reducible head_reducible_prim_step.

-  Lemma ownP_lift_head_step p E Φ e1 :
+  Lemma ownP_lift_head_step 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 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
-    ⊢ WP e1 @ p; E {{ Φ }}.
+            ={∅,E}=∗ WP e2 @ E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef {{ _, True }})
+    ⊢ WP e1 @ E {{ Φ }}.
  Proof.
-    iIntros "H". iApply (ownP_lift_step p 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) "% ?".
    iApply ("Hwp" with "[]"); eauto.
  Qed.

-  Lemma ownP_lift_pure_head_step p E Φ e1 :
+  (* PDS: Discard *)
+  Lemma ownP_strong_lift_head_step p E Φ e1 :
+    to_val e1 = None →
+    (|={E,∅}=> ∃ σ1, ⌜if p then head_reducible e1 σ1 else True⌝ ∗ ▷ ownP σ1 ∗
+      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
+            ={∅,E}=∗ WP e2 @ p; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ p; ⊤{{ _, True }})
+    ⊢ WP e1 @ p; E {{ Φ }}.
+  Proof.
+    iIntros (?) "H"; iApply ownP_lift_step; first done.
+    iMod "H" as (σ1) "(%&Hσ1&Hwp)". iModIntro. iExists σ1.
+    iSplit; first by destruct p; eauto. by iFrame.
+  Qed.
+
+  Lemma ownP_lift_pure_head_step 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 }})