From 936eeb487ba918dcdd7d6fdeb6f242a7b09ede9c Mon Sep 17 00:00:00 2001
From: Marianna Rapoport <mrapoport@uwaterloo.ca>
Date: Tue, 10 Jul 2018 20:01:25 +0200
Subject: [PATCH] Adding initial support for observations to the definition of
 wp for later prophecy support

---
 theories/heap_lang/lang.v                   | 47 +++++-----
 theories/heap_lang/lifting.v                | 36 ++++----
 theories/heap_lang/total_adequacy.v         |  2 +-
 theories/program_logic/adequacy.v           | 58 ++++++------
 theories/program_logic/ectx_language.v      | 85 +++++++++---------
 theories/program_logic/ectx_lifting.v       | 48 +++++-----
 theories/program_logic/ectxi_language.v     | 29 +++---
 theories/program_logic/language.v           | 98 ++++++++++++++-------
 theories/program_logic/lifting.v            | 28 +++---
 theories/program_logic/ownp.v               | 61 ++++++-------
 theories/program_logic/total_adequacy.v     | 20 ++---
 theories/program_logic/total_ectx_lifting.v | 28 +++---
 theories/program_logic/total_lifting.v      | 22 ++---
 theories/program_logic/total_weakestpre.v   | 28 +++---
 theories/program_logic/weakestpre.v         | 30 +++----
 15 files changed, 331 insertions(+), 289 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index d23688a93..ad92c97ce 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -108,6 +108,8 @@ Inductive val :=
 
 Bind Scope val_scope with val.
 
+Inductive observation := prophecy_observation_todo.
+
 Fixpoint of_val (v : val) : expr :=
   match v with
   | RecV f x e => Rec f x e
@@ -199,7 +201,7 @@ Proof.
   end) (λ l, match l with
   | (inl (inl n), None) => LitInt n | (inl (inr b), None) => LitBool b
   | (inr (inl ()), None) => LitUnit | (inr (inr l), None) => LitLoc l
-  | (_, Some p) => LitProphecy p                                                                 
+  | (_, Some p) => LitProphecy p
   end) _); by intros [].
 Qed.
 Instance un_op_finite : Countable un_op.
@@ -415,62 +417,61 @@ Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
   val_is_unboxed vl ∨ val_is_unboxed v1.
 Arguments vals_cas_compare_safe !_ !_ /.
 
-Inductive head_step : expr → state → expr → state → list (expr) → Prop :=
+Inductive head_step : expr → state → option observation -> expr → state → list (expr) → Prop :=
   | BetaS f x e1 e2 v2 e' σ :
      to_val e2 = Some v2 →
      Closed (f :b: x :b: []) e1 →
      e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) →
-     head_step (App (Rec f x e1) e2) σ e' σ []
+     head_step (App (Rec f x e1) e2) σ None e' σ []
   | UnOpS op e v v' σ :
      to_val e = Some v →
      un_op_eval op v = Some v' →
-     head_step (UnOp op e) σ (of_val v') σ []
+     head_step (UnOp op e) σ None (of_val v') σ []
   | BinOpS op e1 e2 v1 v2 v' σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      bin_op_eval op v1 v2 = Some v' →
-     head_step (BinOp op e1 e2) σ (of_val v') σ []
+     head_step (BinOp op e1 e2) σ None (of_val v') σ []
   | IfTrueS e1 e2 σ :
-     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
+     head_step (If (Lit $ LitBool true) e1 e2) σ None e1 σ []
   | IfFalseS e1 e2 σ :
-     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ []
+     head_step (If (Lit $ LitBool false) e1 e2) σ None e2 σ []
   | FstS e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     head_step (Fst (Pair e1 e2)) σ e1 σ []
+     head_step (Fst (Pair e1 e2)) σ None e1 σ []
   | SndS e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     head_step (Snd (Pair e1 e2)) σ e2 σ []
+     head_step (Snd (Pair e1 e2)) σ None e2 σ []
   | CaseLS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
-     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ []
+     head_step (Case (InjL e0) e1 e2) σ None (App e1 e0) σ []
   | CaseRS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
-     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
+     head_step (Case (InjR e0) e1 e2) σ None (App e2 e0) σ []
   | ForkS e σ:
-     head_step (Fork e) σ (Lit LitUnit) σ [e]
+     head_step (Fork e) σ None (Lit LitUnit) σ [e]
   | AllocS e v σ l :
      to_val e = Some v → σ !! l = None →
-     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
+     head_step (Alloc e) σ None (Lit $ LitLoc l) (<[l:=v]>σ) []
   | LoadS l v σ :
      σ !! l = Some v →
-     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ []
+     head_step (Load (Lit $ LitLoc l)) σ None (of_val v) σ []
   | StoreS l e v σ :
      to_val e = Some v → is_Some (σ !! l) →
-     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) []
+     head_step (Store (Lit $ LitLoc l) e) σ None (Lit LitUnit) (<[l:=v]>σ) []
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some vl → vl ≠ v1 →
      vals_cas_compare_safe vl v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ []
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool false) σ []
   | CasSucS l e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some v1 →
      vals_cas_compare_safe v1 v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) []
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool true) (<[l:=v2]>σ) []
   | FaaS l i1 e2 i2 σ :
      to_val e2 = Some (LitV (LitInt i2)) →
      σ !! l = Some (LitV (LitInt i1)) →
-     head_step (FAA (Lit $ LitLoc l) e2) σ (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].
-
+     head_step (FAA (Lit $ LitLoc l) e2) σ None (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].
 
 (** Basic properties about the language *)
 Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
@@ -480,11 +481,11 @@ Lemma fill_item_val Ki e :
   is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
 Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
 
-Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
+Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs → to_val e1 = None.
 Proof. destruct 1; naive_solver. Qed.
 
-Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
-  head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e).
+Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 efs :
+  head_step (fill_item Ki e) σ1 κ e2 σ2 efs → is_Some (to_val e).
 Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
 
 Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
@@ -499,7 +500,7 @@ Qed.
 
 Lemma alloc_fresh e v σ :
   let l := fresh (dom (gset loc) σ) in
-  to_val e = Some v → head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
+  to_val e = Some v → head_step (Alloc e) σ None (Lit (LitLoc l)) (<[l:=v]>σ) [].
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
 
 (* Misc *)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 959d6fc5d..aed8e6002 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -35,7 +35,7 @@ Ltac inv_head_step :=
   repeat match goal with
   | _ => progress simplify_map_eq/= (* simplify memory stuff *)
   | H : to_val _ = Some _ |- _ => apply of_to_val in H
-  | H : head_step ?e _ _ _ _ |- _ =>
+  | H : head_step ?e _ _ _ _ _ |- _ =>
      try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
      and can thus better be avoided. *)
      inversion H; subst; clear H
@@ -48,7 +48,7 @@ Local Hint Constructors head_step.
 Local Hint Resolve alloc_fresh.
 Local Hint Resolve to_of_val.
 
-Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
+Local Ltac solve_exec_safe := intros; subst; do 4 eexists; econstructor; eauto.
 Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pure_exec :=
   unfold IntoVal in *;
@@ -109,14 +109,14 @@ Lemma wp_fork s E e Φ :
   ▷ WP e @ s; ⊤ {{ _, True }} -∗ ▷ Φ (LitV LitUnit) -∗ WP Fork e @ s; E {{ Φ }}.
 Proof.
   iIntros "He HΦ".
-  iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
+  iApply wp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
   iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
 Qed.
 Lemma twp_fork s E e Φ :
   WP e @ s; ⊤ [{ _, True }] -∗ Φ (LitV LitUnit) -∗ WP Fork e @ s; E [{ Φ }].
 Proof.
   iIntros "He HΦ".
-  iApply twp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
+  iApply twp_lift_pure_det_head_step; [eauto|intros; inv_head_step; eauto|].
   iIntros "!> /= {$He}". by iApply twp_value.
 Qed.
 
@@ -126,8 +126,8 @@ Lemma wp_alloc s E e v :
   {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
   iIntros (<- Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>"; iSplit; first by auto.
-  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iIntros (σ1) "Hσ !>"; iSplit; first by eauto.
+  iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
@@ -136,8 +136,8 @@ Lemma twp_alloc s E e v :
   [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
 Proof.
   iIntros (<- Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
-  iIntros (σ1) "Hσ !>"; iSplit; first by auto.
-  iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iIntros (σ1) "Hσ !>"; iSplit; first by eauto.
+  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
@@ -148,7 +148,7 @@ Proof.
   iIntros (Φ) ">Hl HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto.
-  iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_load s E l q v :
@@ -157,7 +157,7 @@ Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto.
-  iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
@@ -168,7 +168,7 @@ Proof.
   iIntros (<- Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto 6. iNext; iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
@@ -179,7 +179,7 @@ Proof.
   iIntros (<- Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto 6. iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
@@ -192,7 +192,7 @@ Proof.
   iIntros (<- [v2 <-] ?? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 Lemma twp_cas_fail s E l q v' e1 v1 e2 :
@@ -203,7 +203,7 @@ Proof.
   iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
@@ -215,7 +215,7 @@ Proof.
   iIntros (<- <- ? Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
@@ -227,7 +227,7 @@ Proof.
   iIntros (<- <- ? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
@@ -240,7 +240,7 @@ Proof.
   iIntros (<- Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto. iNext; iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
@@ -252,7 +252,7 @@ Proof.
   iIntros (<- Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 55e7f5f5e..838357376 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 
 Definition heap_total Σ `{heapPreG Σ} s e σ φ :
   (∀ `{heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]%I) →
-  sn step ([e], σ).
+  sn erased_step ([e], σ).
 Proof.
   intros Hwp; eapply (twp_total _ _); iIntros (?) "".
   iMod (gen_heap_init σ) as (?) "Hh".
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index b53adc80d..43d9dddf2 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -37,26 +37,26 @@ Qed.
 Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
     (φ : val Λ → state Λ → Prop) := {
   adequate_result t2 σ2 v2 :
-   rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2 σ2;
+   rtc erased_step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2 σ2;
   adequate_not_stuck t2 σ2 e2 :
    s = NotStuck →
-   rtc step ([e1], σ1) (t2, σ2) →
+   rtc erased_step ([e1], σ1) (t2, σ2) →
    e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2)
 }.
 
 Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
   adequate NotStuck e1 σ1 φ →
-  rtc step ([e1], σ1) (t2, σ2) →
-  Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
+  rtc erased_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_not_stuck NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
+  destruct (adequate_not_stuck NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(κ&e3&σ3&efs&?)];
     rewrite ?eq_None_not_Some; auto.
   { exfalso. eauto. }
   destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
-  right; exists (t2' ++ e3 :: t2'' ++ efs), σ3; econstructor; eauto.
+  right; exists κ, (t2' ++ e3 :: t2'' ++ efs), σ3; econstructor; eauto.
 Qed.
 
 Section adequacy.
@@ -71,39 +71,41 @@ Notation world σ := (world' ⊤ σ) (only parsing).
 
 Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
 
-Lemma wp_step s E e1 σ1 e2 σ2 efs Φ :
-  prim_step e1 σ1 e2 σ2 efs →
+Lemma wp_step s E e1 σ1 κ e2 σ2 efs Φ :
+  prim_step e1 σ1 κ e2 σ2 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) // uPred_fupd_eq.
+  rewrite (val_stuck e1 σ1 κ e2 σ2 efs) // uPred_fupd_eq.
   iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
-  iMod ("H" $! e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
+  iMod ("H" $! κ e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
   iIntros "!> !>". by iMod ("H" with "[$Hw $HE]") as ">($ & $ & $)".
 Qed.
 
-Lemma wptp_step s e1 t1 t2 σ1 σ2 Φ :
-  step (e1 :: t1,σ1) (t2, σ2) →
+(* should we be able to say that κs = κ :: κs'? *)
+Lemma wptp_step s e1 t1 t2 κ σ1 σ2 Φ :
+  step (e1 :: t1,σ1) κ (t2, σ2) →
   world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
-  ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
+  ==∗ ∃ 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/=.
-  - iExists e2', (t2' ++ efs); iSplitR; first eauto.
+  - iExists e2', (t2' ++ efs); iSplitR; first by eauto.
     iFrame "Ht". iApply wp_step; eauto with iFrame.
   - iExists e, (t1' ++ e2' :: t2' ++ efs); iSplitR; first eauto.
     iDestruct "Ht" as "($ & He' & $)". iFrame "He".
     iApply wp_step; eauto with iFrame.
 Qed.
 
-Lemma wptp_steps s n e1 t1 t2 σ1 σ2 Φ :
-  nsteps step n (e1 :: t1, σ1) (t2, σ2) →
+Lemma wptp_steps s n e1 t1 κs t2 σ1 σ2 Φ :
+  nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢
   Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 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 /=.
+  revert e1 t1 κs t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs t2 σ1 σ2 /=.
   { inversion_clear 1; iIntros "?"; eauto 10. }
   iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
   iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
@@ -123,8 +125,8 @@ Proof.
   by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
 Qed.
 
-Lemma wptp_result s n e1 t1 v2 t2 σ1 σ2 φ :
-  nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) →
+Lemma wptp_result s n e1 t1 κs v2 t2 σ1 σ2 φ :
+  nsteps n (e1 :: t1, σ1) κs (of_val v2 :: t2, σ2) →
   world σ1 ∗ WP e1 @ s; ⊤ {{ v, ∀ σ, state_interp σ ={⊤,∅}=∗ ⌜φ v σ⌝ }} ∗ wptp s t1
   ⊢ ▷^(S (S n)) ⌜φ v2 σ2⌝.
 Proof.
@@ -145,8 +147,8 @@ Proof.
   iIntros "!> !> !%". by right.
 Qed.
 
-Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
-  nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 →
+Lemma wptp_safe n e1 κs e2 t1 t2 σ1 σ2 Φ :
+  nsteps n (e1 :: t1, σ1) κs (t2, σ2) → e2 ∈ t2 →
   world σ1 ∗ WP e1 {{ Φ }} ∗ wptp NotStuck t1
   ⊢ ▷^(S (S n)) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
 Proof.
@@ -157,8 +159,8 @@ Proof.
   - iMod (wp_safe with "Hw [Htp]") as "$". by iApply (big_sepL_elem_of with "Htp").
 Qed.
 
-Lemma wptp_invariance s n e1 e2 t1 t2 σ1 σ2 φ Φ :
-  nsteps step n (e1 :: t1, σ1) (t2, σ2) →
+Lemma wptp_invariance s n e1 κs e2 t1 t2 σ1 σ2 φ Φ :
+  nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
   (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
   ⊢ ▷^(S (S n)) ⌜φ⌝.
 Proof.
@@ -178,13 +180,13 @@ Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
   adequate s e σ φ.
 Proof.
   intros Hwp; split.
-  - intros t2 σ2 v2 [n ?]%rtc_nsteps.
+  - intros t2 σ2 v2 [n [κs ?]]%erased_steps_nsteps.
     eapply (soundness (M:=iResUR Σ) _ (S (S n))).
     iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
     rewrite {1}uPred_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.
-  - destruct s; last done. intros t2 σ2 e2 _ [n ?]%rtc_nsteps ?.
+  - destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?.
     eapply (soundness (M:=iResUR Σ) _ (S (S n))).
     iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
     rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
@@ -210,10 +212,10 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
      (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
        stateI σ1 ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) →
-  rtc step ([e], σ1) (t2, σ2) →
+  rtc erased_step ([e], σ1) (t2, σ2) →
   φ.
 Proof.
-  intros Hwp [n ?]%rtc_nsteps.
+  intros Hwp [n [κs ?]]%erased_steps_nsteps.
   eapply (soundness (M:=iResUR Σ) _ (S (S n))).
   iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _).
   rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
@@ -228,7 +230,7 @@ Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
      (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
        stateI σ1 ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 -∗ ∃ E, |={⊤,E}=> ⌜φ⌝))%I) →
-  rtc step ([e], σ1) (t2, σ2) →
+  rtc erased_step ([e], σ1) (t2, σ2) →
   φ.
 Proof.
   intros Hwp. eapply wp_invariance; first done.
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 7055956f1..45741b260 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -10,19 +10,19 @@ structure. Use the coercion [LanguageOfEctx] as defined in the bottom of this
 file for doing that. *)
 
 Section ectx_language_mixin.
-  Context {expr val ectx state : Type}.
+  Context {expr val ectx state observation : Type}.
   Context (of_val : val → expr).
   Context (to_val : expr → option val).
   Context (empty_ectx : ectx).
   Context (comp_ectx : ectx → ectx → ectx).
   Context (fill : ectx → expr → expr).
-  Context (head_step : expr → state → expr → state → list expr → Prop).
+  Context (head_step : expr → state → option observation -> expr → state → list expr → Prop).
 
   Record EctxLanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
     mixin_of_to_val e v : to_val e = Some v → of_val v = e;
-    mixin_val_head_stuck e1 σ1 e2 σ2 efs :
-      head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
+    mixin_val_head_stuck e1 σ1 κ e2 σ2 efs :
+      head_step e1 σ1 κ e2 σ2 efs → to_val e1 = None;
 
     mixin_fill_empty e : fill empty_ectx e = e;
     mixin_fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
@@ -35,10 +35,10 @@ Section ectx_language_mixin.
     mixin_ectx_positive K1 K2 :
       comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx;
 
-    mixin_step_by_val K K' e1 e1' σ1 e2 σ2 efs :
+    mixin_step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
       fill K e1 = fill K' e1' →
       to_val e1 = None →
-      head_step e1' σ1 e2 σ2 efs →
+      head_step e1' σ1 κ e2 σ2 efs →
       ∃ K'', K' = comp_ectx K K'';
   }.
 End ectx_language_mixin.
@@ -48,25 +48,26 @@ Structure ectxLanguage := EctxLanguage {
   val : Type;
   ectx : Type;
   state : Type;
+  observation : Type;
 
   of_val : val → expr;
   to_val : expr → option val;
   empty_ectx : ectx;
   comp_ectx : ectx → ectx → ectx;
   fill : ectx → expr → expr;
-  head_step : expr → state → expr → state → list expr → Prop;
+  head_step : expr → state → option observation -> expr → state → list expr → Prop;
 
   ectx_language_mixin :
     EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
 }.
 
-Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _} _.
+Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _ _} _.
 Arguments of_val {_} _%V.
 Arguments to_val {_} _%E.
 Arguments empty_ectx {_}.
 Arguments comp_ectx {_} _ _.
 Arguments fill {_} _ _%E.
-Arguments head_step {_} _%E _ _%E _ _.
+Arguments head_step {_} _%E _ _ _%E _ _.
 
 (* From an ectx_language, we can construct a language. *)
 Section ectx_language.
@@ -76,7 +77,7 @@ Section ectx_language.
   Implicit Types K : ectx Λ.
 
   (* Only project stuff out of the mixin that is not also in language *)
-  Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
+  Lemma val_head_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs → to_val e1 = None.
   Proof. apply ectx_language_mixin. Qed.
   Lemma fill_empty e : fill empty_ectx e = e.
   Proof. apply ectx_language_mixin. Qed.
@@ -89,17 +90,17 @@ Section ectx_language.
   Lemma ectx_positive K1 K2 :
     comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx.
   Proof. apply ectx_language_mixin. Qed.
-  Lemma step_by_val K K' e1 e1' σ1 e2 σ2 efs :
+  Lemma step_by_val K K' e1 e1' σ1 κ e2 σ2 efs :
     fill K e1 = fill K' e1' →
     to_val e1 = None →
-    head_step e1' σ1 e2 σ2 efs →
+    head_step e1' σ1 κ e2 σ2 efs →
     ∃ K'', K' = comp_ectx K K''.
   Proof. apply ectx_language_mixin. Qed.
 
   Definition head_reducible (e : expr Λ) (σ : state Λ) :=
-    ∃ e' σ' efs, head_step e σ e' σ' efs.
+    ∃ κ e' σ' efs, head_step e σ κ e' σ' efs.
   Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
-    ∀ e' σ' efs, ¬head_step e σ e' σ' efs.
+    ∀ κ e' σ' efs, ¬head_step e σ κ e' σ' efs.
   Definition head_stuck (e : expr Λ) (σ : state Λ) :=
     to_val e = None ∧ head_irreducible e σ.
 
@@ -108,14 +109,14 @@ Section ectx_language.
   Definition sub_redexes_are_values (e : expr Λ) :=
     ∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx.
 
-  Inductive prim_step (e1 : expr Λ) (σ1 : state Λ)
+  Inductive prim_step (e1 : expr Λ) (σ1 : state Λ) (κ : option (observation Λ))
       (e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
     Ectx_step K e1' e2' :
       e1 = fill K e1' → e2 = fill K e2' →
-      head_step e1' σ1 e2' σ2 efs → prim_step e1 σ1 e2 σ2 efs.
+      head_step e1' σ1 κ e2' σ2 efs → prim_step e1 σ1 κ e2 σ2 efs.
 
-  Lemma Ectx_step' K e1 σ1 e2 σ2 efs :
-    head_step e1 σ1 e2 σ2 efs → prim_step (fill K e1) σ1 (fill K e2) σ2 efs.
+  Lemma Ectx_step' K e1 σ1 κ e2 σ2 efs :
+    head_step e1 σ1 κ e2 σ2 efs → prim_step (fill K e1) σ1 κ (fill K e2) σ2 efs.
   Proof. econstructor; eauto. Qed.
 
   Definition ectx_lang_mixin : LanguageMixin of_val to_val prim_step.
@@ -123,30 +124,30 @@ Section ectx_language.
     split.
     - apply ectx_language_mixin.
     - apply ectx_language_mixin.
-    - intros ????? [??? -> -> ?%val_head_stuck].
+    - intros ?????? [??? -> -> ?%val_head_stuck].
       apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
   Qed.
 
   Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
 
   Definition head_atomic (a : atomicity) (e : expr Λ) : Prop :=
-    ∀ σ e' σ' efs,
-      head_step e σ e' σ' efs →
+    ∀ σ κ e' σ' efs,
+      head_step e σ κ e' σ' efs →
       if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
 
   (* Some lemmas about this language *)
   Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
   Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
 
-  Lemma head_prim_step e1 σ1 e2 σ2 efs :
-    head_step e1 σ1 e2 σ2 efs → prim_step e1 σ1 e2 σ2 efs.
+  Lemma head_prim_step e1 σ1 κ e2 σ2 efs :
+    head_step e1 σ1 κ e2 σ2 efs → prim_step e1 σ1 κ e2 σ2 efs.
   Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
 
   Lemma not_head_reducible e σ : ¬head_reducible e σ ↔ head_irreducible e σ.
   Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.
 
   Lemma head_prim_reducible e σ : head_reducible e σ → reducible e σ.
-  Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
+  Proof. intros (κ&e'&σ'&efs&?). eexists κ, e', σ', efs. by apply head_prim_step. Qed.
   Lemma head_prim_irreducible e σ : irreducible e σ → head_irreducible e σ.
   Proof.
     rewrite -not_reducible -not_head_reducible. eauto using head_prim_reducible.
@@ -155,7 +156,7 @@ Section ectx_language.
   Lemma prim_head_reducible e σ :
     reducible e σ → sub_redexes_are_values e → head_reducible e σ.
   Proof.
-    intros (e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
+    intros (κ&e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
     assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
     rewrite fill_empty /head_reducible; eauto.
   Qed.
@@ -175,18 +176,18 @@ Section ectx_language.
   Lemma ectx_language_atomic a e :
     head_atomic a e → sub_redexes_are_values e → Atomic a e.
   Proof.
-    intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
+    intros Hatomic_step Hatomic_fill σ κ e' σ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
     rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
   Qed.
 
-  Lemma head_reducible_prim_step e1 σ1 e2 σ2 efs :
+  Lemma head_reducible_prim_step e1 σ1 κ e2 σ2 efs :
     head_reducible e1 σ1 →
-    prim_step e1 σ1 e2 σ2 efs →
-    head_step e1 σ1 e2 σ2 efs.
+    prim_step e1 σ1 κ e2 σ2 efs →
+    head_step e1 σ1 κ e2 σ2 efs.
   Proof.
-    intros (e2''&σ2''&efs''&?) [K e1' e2' -> -> Hstep].
-    destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 e2'' σ2'' efs'')
+    intros (κ'&e2''&σ2''&efs''&?) [K e1' e2' -> -> Hstep].
+    destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 κ' e2'' σ2'' efs'')
       as [K' [-> _]%symmetry%ectx_positive];
       eauto using fill_empty, fill_not_val, val_head_stuck.
     by rewrite !fill_empty.
@@ -197,10 +198,10 @@ Section ectx_language.
   Proof.
     split; simpl.
     - eauto using fill_not_val.
-    - intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
+    - intros ?????? [K' e1' e2' Heq1 Heq2 Hstep].
       by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
-    - intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
-      destruct (step_by_val K K'' e1 e1'' σ1 e2'' σ2 efs) as [K' ->]; eauto.
+    - intros e1 σ1 κ e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
+      destruct (step_by_val K K'' e1 e1'' σ1 κ e2'' σ2 efs) as [K' ->]; eauto.
       rewrite -fill_comp in Heq1; apply (inj (fill _)) in Heq1.
       exists (fill K' e2''); rewrite -fill_comp; split; auto.
       econstructor; eauto.
@@ -208,14 +209,14 @@ Section ectx_language.
 
   Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
     (∀ σ, P → head_reducible e1 σ) →
-    (∀ σ1 e2' σ2 efs,
-      P → head_step e1 σ1 e2' σ2 efs → σ1 = σ2 ∧ e2=e2' ∧ efs = []) →
+    (∀ σ1 κ e2' σ2 efs,
+      P → head_step e1 σ1 κ e2' σ2 efs → κ = None /\ σ1 = σ2 ∧ e2=e2' ∧ efs = []) →
     PureExec P e1 e2.
   Proof.
     intros Hp1 Hp2. split.
-    - intros σ ?. destruct (Hp1 σ) as (e2' & σ2 & efs & ?); first done.
-      eexists e2', σ2, efs. by apply head_prim_step.
-    - intros σ1 e2' σ2 efs ? ?%head_reducible_prim_step; eauto.
+    - intros σ ?. destruct (Hp1 σ) as (κ & e2' & σ2 & efs & ?); first done.
+      eexists κ, e2', σ2, efs. by apply head_prim_step.
+    - intros σ1 κ e2' σ2 efs ? ?%head_reducible_prim_step; eauto.
   Qed.
 
   Global Instance pure_exec_fill K e1 e2 φ :
@@ -236,6 +237,6 @@ work.
 Note that this trick no longer works when we switch to canonical projections
 because then the pattern match [let '...] will be desugared into projections. *)
 Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
-  let '@EctxLanguage E V C St of_val to_val empty comp fill head mix := Λ in
-  @Language E V St of_val to_val _
-    (@ectx_lang_mixin (@EctxLanguage E V C St of_val to_val empty comp fill head mix)).
+  let '@EctxLanguage E V C St K of_val to_val empty comp fill head mix := Λ in
+  @Language E V St K of_val to_val _
+    (@ectx_lang_mixin (@EctxLanguage E V C St K of_val to_val empty comp fill head mix)).
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 419f8365e..524741d60 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -18,13 +18,13 @@ Lemma wp_lift_head_step_fupd {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}▷=∗
+    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,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_fupd=>//. iIntros (σ1) "Hσ".
   iMod ("H" with "Hσ") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs) "%".
+  iSplit; first by destruct s; eauto. iIntros (κ e2 σ2 efs) "%".
   iApply "H"; eauto.
 Qed.
 
@@ -32,12 +32,12 @@ 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}=∗
+    ▷ ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,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_head_step_fupd; [done|]. iIntros (?) "?".
-  iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "!> !>". by iApply "H".
+  iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (κ e2 σ2 efs ?) "!> !>". by iApply "H".
 Qed.
 
 Lemma wp_lift_head_stuck E Φ e :
@@ -52,15 +52,15 @@ 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⌝ →
+  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+  (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
     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; [|by eauto|].
   { by destruct s; auto. }
   iApply (step_fupd_wand with "H"); iIntros "H".
-  iIntros (????). iApply "H"; eauto.
+  iIntros (?????). iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_pure_head_stuck E Φ e :
@@ -78,43 +78,43 @@ Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E1,E2}▷=∗
+    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
       state_interp σ2 ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
   iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; auto. iIntros (e2 σ2 efs) "%".
-  iApply "H"; auto.
+  iSplit; first by destruct s; auto. iIntros (κ e2 σ2 efs) "%".
+  iApply "H"; eauto.
 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}=∗
+    ▷ ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
       from_option Φ 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" with "Hσ1") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs) "%".
-  iApply "H"; auto.
+  iSplit; first by destruct s; auto. iNext. iIntros (κ e2 σ2 efs) "%".
+  iApply "H"; eauto.
 Qed.
 
 Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
-    ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E1,E2}▷=∗
+    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
       ⌜efs = []⌝ ∗ state_interp σ2 ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E1 {{ Φ }}.
 Proof.
   iIntros (?) "H". iApply wp_lift_atomic_head_step_fupd; [done|].
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
-  iIntros (v2 σ2 efs) "%". iMod ("H" $! v2 σ2 efs with "[# //]") as "H".
+  iIntros (κ v2 σ2 efs) "%". iMod ("H" $! κ v2 σ2 efs with "[# //]") as "H".
   iIntros "!> !>". iMod "H" as "(% & $ & $)"; subst; auto.
 Qed.
 
@@ -122,20 +122,20 @@ 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}=∗
+    ▷ ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       ⌜efs = []⌝ ∗ state_interp σ2 ∗ from_option Φ False (to_val e2))
   ⊢ 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.
-  iNext; iIntros (v2 σ2 efs) "%".
-  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
+  iNext; iIntros (κ v2 σ2 efs) "%".
+  iMod ("H" $! κ v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
 Qed.
 
 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') →
+  (∀ σ1 κ e2' σ2 efs',
+    head_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
@@ -146,8 +146,8 @@ Qed.
 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') →
+  (∀ σ1 κ e2' σ2 efs',
+    head_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   (|={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.
@@ -157,8 +157,8 @@ Qed.
 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',
-    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+  (∀ σ1 κ e2' σ2 efs',
+    head_step e1 σ1 κ e2' σ2 efs' → κ = None /\  σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
 Proof using Hinh.
   intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index bd73dfc65..fb932b863 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -27,16 +27,16 @@ Below you can find the relevant parts:
 *)
 
 Section ectxi_language_mixin.
-  Context {expr val ectx_item state : Type}.
+  Context {expr val ectx_item state observation : Type}.
   Context (of_val : val → expr).
   Context (to_val : expr → option val).
   Context (fill_item : ectx_item → expr → expr).
-  Context (head_step : expr → state → expr → state → list expr → Prop).
+  Context (head_step : expr → state → option observation -> expr → state → list expr → Prop).
 
   Record EctxiLanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
     mixin_of_to_val e v : to_val e = Some v → of_val v = e;
-    mixin_val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
+    mixin_val_stuck e1 σ1 κ e2 σ2 efs : head_step e1 σ1 κ e2 σ2 efs → to_val e1 = None;
 
     mixin_fill_item_inj Ki : Inj (=) (=) (fill_item Ki);
     mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
@@ -44,8 +44,8 @@ Section ectxi_language_mixin.
       to_val e1 = None → to_val e2 = None →
       fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2;
 
-    mixin_head_ctx_step_val Ki e σ1 e2 σ2 efs :
-      head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e);
+    mixin_head_ctx_step_val Ki e σ1 κ e2 σ2 efs :
+      head_step (fill_item Ki e) σ1 κ e2 σ2 efs → is_Some (to_val e);
   }.
 End ectxi_language_mixin.
 
@@ -54,21 +54,22 @@ Structure ectxiLanguage := EctxiLanguage {
   val : Type;
   ectx_item : Type;
   state : Type;
+  observation : Type;
 
   of_val : val → expr;
   to_val : expr → option val;
   fill_item : ectx_item → expr → expr;
-  head_step : expr → state → expr → state → list expr → Prop;
+  head_step : expr → state → option observation -> expr → state → list expr → Prop;
 
   ectxi_language_mixin :
     EctxiLanguageMixin of_val to_val fill_item head_step
 }.
 
-Arguments EctxiLanguage {_ _ _ _ _ _ _ _} _.
+Arguments EctxiLanguage {_ _ _ _ _ _ _ _ _} _.
 Arguments of_val {_} _%V.
 Arguments to_val {_} _%E.
 Arguments fill_item {_} _ _%E.
-Arguments head_step {_} _%E _ _%E _ _.
+Arguments head_step {_} _%E _ _ _%E _ _.
 
 Section ectxi_language.
   Context {Λ : ectxiLanguage}.
@@ -84,8 +85,8 @@ Section ectxi_language.
     to_val e1 = None → to_val e2 = None →
     fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
   Proof. apply ectxi_language_mixin. Qed.
-  Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
-    head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e).
+  Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 efs :
+    head_step (fill_item Ki e) σ1 κ e2 σ2 efs → is_Some (to_val e).
   Proof. apply ectxi_language_mixin. Qed.
 
   Definition fill (K : ectx) (e : expr Λ) : expr Λ := foldl (flip fill_item) e K.
@@ -109,7 +110,7 @@ Section ectxi_language.
     - intros K; induction K as [|Ki K IH]; rewrite /Inj; naive_solver.
     - done.
     - by intros [] [].
-    - intros K K' e1 e1' σ1 e2 σ2 efs Hfill Hred Hstep; revert K' Hfill.
+    - intros K K' e1 κ e1' σ1 e2 σ2 efs Hfill Hred Hstep; revert K' Hfill.
       induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
       destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
       { rewrite fill_app in Hstep. apply head_ctx_step_val in Hstep.
@@ -147,6 +148,6 @@ Coercion ectxi_lang_ectx : ectxiLanguage >-> ectxLanguage.
 Coercion ectxi_lang : ectxiLanguage >-> language.
 
 Definition EctxLanguageOfEctxi (Λ : ectxiLanguage) : ectxLanguage :=
-  let '@EctxiLanguage E V C St of_val to_val fill head mix := Λ in
-  @EctxLanguage E V (list C) St of_val to_val _ _ _ _
-    (@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St of_val to_val fill head mix)).
+  let '@EctxiLanguage E V C St K of_val to_val fill head mix := Λ in
+  @EctxLanguage E V (list C) St K of_val to_val _ _ _ _
+    (@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St K of_val to_val fill head mix)).
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index b067bb1eb..e08663e64 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -2,15 +2,17 @@ From iris.algebra Require Export ofe.
 Set Default Proof Using "Type".
 
 Section language_mixin.
-  Context {expr val state : Type}.
+  Context {expr val state observation : Type}.
   Context (of_val : val → expr).
   Context (to_val : expr → option val).
-  Context (prim_step : expr → state → expr → state → list expr → Prop).
+  (** We annotate the reduction relation with observations [k], which we will use in the definition
+     of weakest preconditions to keep track of creating and resolving prophecy variables. *)
+  Context (prim_step : expr → state → option observation → expr → state → list expr → Prop).
 
   Record LanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
     mixin_of_to_val e v : to_val e = Some v → of_val v = e;
-    mixin_val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs → to_val e = None
+    mixin_val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None
   }.
 End language_mixin.
 
@@ -18,9 +20,10 @@ Structure language := Language {
   expr : Type;
   val : Type;
   state : Type;
+  observation : Type;
   of_val : val → expr;
   to_val : expr → option val;
-  prim_step : expr → state → expr → state → list expr → Prop;
+  prim_step : expr → state → option observation → expr → state → list expr → Prop;
   language_mixin : LanguageMixin of_val to_val prim_step
 }.
 Delimit Scope expr_scope with E.
@@ -28,10 +31,10 @@ Delimit Scope val_scope with V.
 Bind Scope expr_scope with expr.
 Bind Scope val_scope with val.
 
-Arguments Language {_ _ _ _ _ _} _.
+Arguments Language {_ _ _ _ _ _ _} _.
 Arguments of_val {_} _.
 Arguments to_val {_} _.
-Arguments prim_step {_} _ _ _ _ _.
+Arguments prim_step {_} _ _ _ _ _ _.
 
 Canonical Structure stateC Λ := leibnizC (state Λ).
 Canonical Structure valC Λ := leibnizC (val Λ).
@@ -42,12 +45,12 @@ Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
 Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
   fill_not_val e :
     to_val e = None → to_val (K e) = None;
-  fill_step e1 σ1 e2 σ2 efs :
-    prim_step e1 σ1 e2 σ2 efs →
-    prim_step (K e1) σ1 (K e2) σ2 efs;
-  fill_step_inv e1' σ1 e2 σ2 efs :
-    to_val e1' = None → prim_step (K e1') σ1 e2 σ2 efs →
-    ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 efs
+  fill_step e1 σ1 κ e2 σ2 efs :
+    prim_step e1 σ1 κ e2 σ2 efs →
+    prim_step (K e1) σ1 κ (K e2) σ2 efs;
+  fill_step_inv e1' σ1 κ e2 σ2 efs :
+    to_val e1' = None → prim_step (K e1') σ1 κ e2 σ2 efs →
+    ∃ e2', e2 = K e2' ∧ prim_step e1' σ1 κ e2' σ2 efs
 }.
 
 Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
@@ -64,13 +67,13 @@ Section language.
   Proof. apply language_mixin. Qed.
   Lemma of_to_val e v : to_val e = Some v → of_val v = e.
   Proof. apply language_mixin. Qed.
-  Lemma val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs → to_val e = None.
+  Lemma val_stuck e σ κ e' σ' efs : prim_step e σ κ e' σ' efs → to_val e = None.
   Proof. apply language_mixin. Qed.
 
   Definition reducible (e : expr Λ) (σ : state Λ) :=
-    ∃ e' σ' efs, prim_step e σ e' σ' efs.
+    ∃ κ e' σ' efs, prim_step e σ κ e' σ' efs.
   Definition irreducible (e : expr Λ) (σ : state Λ) :=
-    ∀ e' σ' efs, ¬prim_step e σ e' σ' efs.
+    ∀ κ e' σ' efs, ¬prim_step e σ κ e' σ' efs.
   Definition stuck (e : expr Λ) (σ : state Λ) :=
     to_val e = None ∧ irreducible e σ.
 
@@ -86,16 +89,43 @@ Section language.
      in case `e` reduces to a stuck non-value, there is no proof that the
      invariants have been established again. *)
   Class Atomic (a : atomicity) (e : expr Λ) : Prop :=
-    atomic σ e' σ' efs :
-      prim_step e σ e' σ' efs →
+    atomic σ e' κ σ' efs :
+      prim_step e σ κ e' σ' efs →
       if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
 
-  Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
+  Inductive step (ρ1 : cfg Λ) (κ : option (observation Λ)) (ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
        ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) →
-       prim_step e1 σ1 e2 σ2 efs →
-       step ρ1 ρ2.
+       prim_step e1 σ1 κ e2 σ2 efs →
+       step ρ1 κ ρ2.
+
+  Inductive nsteps : nat -> cfg Λ → list (observation Λ) → cfg Λ → Prop :=
+  | nsteps_refl ρ :
+      nsteps 0 ρ [] ρ
+  | nsteps_l n ρ1 ρ2 ρ3 κ κs :
+      step ρ1 κ ρ2 →
+      nsteps n ρ2 κs ρ3 →
+      nsteps (S n) ρ1 (option_list κ ++ κs) ρ3.
+
+ (* Inductive steps : cfg Λ → list (observation Λ) → cfg Λ → Prop :=
+  | steps_refl ρ :
+      steps ρ [] ρ
+  | steps_l ρ1 ρ2 ρ3 κ κs :
+      step ρ1 κ ρ2 →
+      steps ρ2 κs ρ3 →
+      steps ρ1 (option_list κ ++ κs) ρ3. *)
+
+  Definition erased_step (ρ1 ρ2 : cfg Λ) := exists κ, step ρ1 κ ρ2.
+
+  Hint Constructors step nsteps.
+
+  Lemma erased_steps_nsteps ρ1 ρ2 :
+    rtc erased_step ρ1 ρ2 ->
+    ∃ n κs, nsteps n ρ1 κs ρ2.
+  Proof.
+    induction 1; firstorder; eauto.
+  Qed.
 
   Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
   Proof. intros <-. by rewrite to_of_val. Qed.
@@ -103,9 +133,9 @@ Section language.
   Lemma not_reducible e σ : ¬reducible e σ ↔ irreducible e σ.
   Proof. unfold reducible, irreducible. naive_solver. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
-  Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
+  Proof. intros (?&?&?&?&?); eauto using val_stuck. Qed.
   Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ.
-  Proof. intros [??] ??? ?%val_stuck. by destruct (to_val e). Qed.
+  Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
@@ -116,15 +146,15 @@ Section language.
   Lemma reducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.
   Proof.
-    intros ? (e'&σ'&efs&Hstep); unfold reducible.
+    intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
     apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
   Qed.
   Lemma irreducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → irreducible e σ → irreducible (K e) σ.
   Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
 
-  Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
-    t1 ≡ₚ t1' → step (t1,σ1) (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) (t2',σ2).
+  Lemma step_Permutation (t1 t1' t2 : list (expr Λ)) κ σ1 σ2 :
+    t1 ≡ₚ t1' → step (t1,σ1) κ (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ step (t1',σ1) κ (t2',σ2).
   Proof.
     intros Ht [e1 σ1' e2 σ2' efs tl tr ?? Hstep]; simplify_eq/=.
     move: Ht; rewrite -Permutation_middle (symmetry_iff (≡ₚ)).
@@ -133,11 +163,17 @@ Section language.
     by rewrite -!Permutation_middle !assoc_L Ht.
   Qed.
 
+  Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
+    t1 ≡ₚ t1' → erased_step (t1,σ1) (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ erased_step (t1',σ1) (t2',σ2).
+  Proof.
+    intros* Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
+  Qed.
+
   Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
     pure_exec_safe σ :
       P → reducible e1 σ;
-    pure_exec_puredet σ1 e2' σ2 efs :
-      P → prim_step e1 σ1 e2' σ2 efs → σ1 = σ2 ∧ e2 = e2' ∧ efs = [];
+    pure_exec_puredet σ1 κ e2' σ2 efs :
+      P → prim_step e1 σ1 κ e2' σ2 efs → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = [];
   }.
 
   Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
@@ -152,10 +188,10 @@ Section language.
   Proof.
     intros [Hred Hstep]. split.
     - unfold reducible in *. naive_solver eauto using fill_step.
-    - intros σ1 e2' σ2 efs ? Hpstep.
-      destruct (fill_step_inv e1 σ1 e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
-      + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
-      + edestruct (Hstep σ1 e2'' σ2 efs) as (-> & -> & ->); auto.
+    - intros σ1 κ e2' σ2 efs ? Hpstep.
+      destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
+      + destruct (Hred σ1) as (? & ? & ? & ? & ?); eauto using val_stuck.
+      + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
   Qed.
 
   (* This is a family of frequent assumptions for PureExec *)
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 8cc97b7e2..58595f0bf 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -15,7 +15,7 @@ Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,∅,E}▷=∗
+    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
       state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
@@ -30,7 +30,7 @@ Lemma wp_lift_stuck E Φ e :
 Proof.
   rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1) "Hσ".
   iMod ("H" with "Hσ") as %[? Hirr]. iModIntro. iSplit; first done.
-  iIntros (e2 σ2 efs) "% !> !>". by case: (Hirr e2 σ2 efs).
+  iIntros (κ e2 σ2 efs) "% !> !>". by case: (Hirr κ e2 σ2 efs).
 Qed.
 
 (** Derived lifting lemmas. *)
@@ -38,7 +38,7 @@ Lemma wp_lift_step s E Φ e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+    ▷ ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
@@ -48,8 +48,8 @@ Qed.
 
 Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-  (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
-  (|={E,E'}▷=> ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
+  (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+  (|={E,E'}▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
     WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
@@ -59,8 +59,8 @@ Proof.
   iIntros (σ1) "Hσ". iMod "H".
   iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
   { iPureIntro. destruct s; done. }
-  iNext. iIntros (e2 σ2 efs ?).
-  destruct (Hstep σ1 e2 σ2 efs); auto; subst.
+  iNext. iIntros (κ e2 σ2 efs ?).
+  destruct (Hstep κ σ1 e2 σ2 efs); auto; subst.
   iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
 Qed.
 
@@ -81,7 +81,7 @@ Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E1}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E1,E2}▷=∗
+    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
       state_interp σ2 ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E1 {{ Φ }}.
@@ -89,8 +89,8 @@ Proof.
   iIntros (?) "H". iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iMod (fupd_intro_mask' E1 ∅) as "Hclose"; first set_solver.
-  iIntros "!>" (e2 σ2 efs ?). iMod "Hclose" as "_".
-  iMod ("H" $! e2 σ2 efs with "[#]") as "H"; [done|].
+  iIntros "!>" (κ e2 σ2 efs ?). iMod "Hclose" as "_".
+  iMod ("H" $! κ e2 σ2 efs with "[#]") as "H"; [done|].
   iMod (fupd_intro_mask' E2 ∅) as "Hclose"; [set_solver|]. iIntros "!> !>".
   iMod "Hclose" as "_". iMod "H" as "($ & HΦ & $)".
   destruct (to_val e2) eqn:?; last by iExFalso.
@@ -101,7 +101,7 @@ Lemma wp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+    ▷ ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
@@ -113,14 +113,14 @@ Qed.
 
 Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
   (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-  (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
+  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
   (|={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 s E E'); try done.
-  { by intros; eapply Hpuredet. }
+  { by naive_solver. }
   iApply (step_fupd_wand with "H"); iIntros "H".
-  by iIntros (e' efs' σ (_&->&->)%Hpuredet).
+  by iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
 Qed.
 
 Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ Φ :
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 59f471673..a87b07f1d 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -53,7 +53,7 @@ Qed.
 Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
   (∀ `{ownPG Λ Σ},
     ownP σ1 ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗ |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
-  rtc step ([e], σ1) (t2, σ2) →
+  rtc erased_step ([e], σ1) (t2, σ2) →
   φ σ2.
 Proof.
   intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
@@ -87,7 +87,7 @@ Section lifting.
 
   Lemma ownP_lift_step s E Φ e1 :
     (|={E,∅}=> ∃ σ1, ⌜if s is NotStuck then reducible e1 σ1 else to_val e1 = None⌝ ∗ ▷ ownP σ1 ∗
-      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
+      ▷ ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ ownP σ2
             ={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
@@ -98,7 +98,7 @@ Section lifting.
       move: Hred; by rewrite to_of_val.
     - iApply wp_lift_step; [done|]; iIntros (σ1) "Hσ".
       iMod "H" as (σ1' ?) "[>Hσf H]". iDestruct (ownP_eq with "Hσ Hσf") as %->.
-      iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep).
+      iModIntro; iSplit; [by destruct s|]; iNext; iIntros (κ e2 σ2 efs Hstep).
       rewrite /ownP; iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
       { by apply auth_update, option_local_update,
           (exclusive_local_update _ (Excl σ2)). }
@@ -120,8 +120,8 @@ Section lifting.
 
   Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
     (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
-    (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
+    (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+    (▷ ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
       WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
@@ -129,43 +129,43 @@ Section lifting.
     { specialize (Hsafe inhabitant). destruct s; last done.
       by eapply reducible_not_val. }
     iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-    iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?).
-    destruct (Hstep σ1 e2 σ2 efs); auto; subst.
+    iModIntro; iSplit; [by destruct s|]; iNext; iIntros (κ e2 σ2 efs ?).
+    destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
     by iMod "Hclose"; iModIntro; iFrame; iApply "H".
   Qed.
 
   (** Derived lifting lemmas. *)
   Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
     (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (▷ ownP σ1 ∗ ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
+    (▷ ownP σ1 ∗ ▷ ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ ownP σ2 -∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
     iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
     iModIntro; iExists σ1; iFrame; iSplit; first by destruct s.
-    iNext; iIntros (e2 σ2 efs) "% Hσ".
-    iDestruct ("H" $! e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
+    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; last done. by apply of_to_val.
   Qed.
 
   Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :
     (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
+    (∀ κ 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 @ 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'".
+    iFrame; iNext; iIntros (κ e2' σ2' efs') "% Hσ2'".
     edestruct Hdet as (->&Hval&->). done. by rewrite Hval; iApply "Hσ2".
   Qed.
 
   Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
     (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
+    (∀ κ 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.
@@ -175,17 +175,17 @@ Section lifting.
 
   Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
     (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
+    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
     ▷ (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).
+    naive_solver. by iNext; iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
   Qed.
 
   Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
     (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
-    (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
@@ -204,14 +204,14 @@ Section ectx_lifting.
 
   Lemma ownP_lift_head_step s E Φ e1 :
     (|={E,∅}=> ∃ σ1, ⌜head_reducible e1 σ1⌝ ∗ ▷ ownP σ1 ∗
-      ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
+      ▷ ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ -∗ ownP σ2
             ={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros "H". iApply ownP_lift_step.
     iMod "H" as (σ1 ?) "[Hσ1 Hwp]". iModIntro. iExists σ1. iSplit.
     { destruct s; try by eauto using reducible_not_val. }
-    iFrame. iNext. iIntros (e2 σ2 efs) "% ?".
+    iFrame. iNext. iIntros (κ e2 σ2 efs) "% ?".
     iApply ("Hwp" with "[]"); eauto.
   Qed.
 
@@ -226,51 +226,52 @@ Section ectx_lifting.
 
   Lemma ownP_lift_pure_head_step s E Φ e1 :
     (∀ σ1, head_reducible e1 σ1) →
-    (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
-    (▷ ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
+    (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+    (▷ ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
       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.
     { by destruct s; auto. }
-    iNext. iIntros (????). iApply "H"; eauto.
+    iNext. iIntros (?????). iApply "H"; eauto.
   Qed.
 
   Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 :
     head_reducible e1 σ1 →
-    ▷ ownP σ1 ∗ ▷ (∀ e2 σ2 efs,
-    ⌜head_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
+    ▷ ownP σ1 ∗ ▷ (∀ κ e2 σ2 efs,
+    ⌜head_step e1 σ1 κ e2 σ2 efs⌝ -∗ ownP σ2 -∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     iIntros (?) "[? H]". iApply ownP_lift_atomic_step; eauto.
     { by destruct s; eauto using reducible_not_val. }
-    iFrame. iNext. iIntros (???) "% ?". iApply ("H" with "[]"); eauto.
+    iFrame. iNext. iIntros (????) "% ?". iApply ("H" with "[]"); eauto.
   Qed.
 
   Lemma ownP_lift_atomic_det_head_step {s E Φ e1} σ1 v2 σ2 efs :
     head_reducible e1 σ1 →
-    (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
+    (∀ κ 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 @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    by destruct s; eauto 10 using ownP_lift_atomic_det_step, reducible_not_val.
+    intros. destruct s; apply ownP_lift_atomic_det_step; try naive_solver.
+    eauto using reducible_not_val.
   Qed.
 
   Lemma ownP_lift_atomic_det_head_step_no_fork {s E e1} σ1 v2 σ2 :
     head_reducible e1 σ1 →
-    (∀ e2' σ2' efs', head_step e1 σ1 e2' σ2' efs' →
+    (∀ κ e2' σ2' efs', head_step e1 σ1 κ e2' σ2' efs' →
       σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
     {{{ ▷ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
   Proof.
-    intros ???; apply ownP_lift_atomic_det_step_no_fork; eauto.
+    intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
     by destruct s; eauto using reducible_not_val.
   Qed.
 
   Lemma ownP_lift_pure_det_head_step {s E Φ} e1 e2 efs :
     (∀ σ1, head_reducible e1 σ1) →
-    (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
     ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
@@ -280,7 +281,7 @@ Section ectx_lifting.
 
   Lemma ownP_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
     (∀ σ1, head_reducible e1 σ1) →
-    (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
     iIntros (??) "H". iApply ownP_lift_pure_det_step_no_fork; eauto.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index ebb8c9b0c..3757b771e 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -12,7 +12,7 @@ Implicit Types e : expr Λ.
 
 Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
     (t1 : list (expr Λ)) : iProp Σ :=
-  (∀ t2 σ1 σ2, ⌜step (t1,σ1) (t2,σ2)⌝ -∗
+  (∀ t2 σ1 σ2, ⌜erased_step (t1,σ1) (t2,σ2)⌝ -∗
     state_interp σ1 ={⊤}=∗ state_interp σ2 ∗ twptp t2)%I.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
@@ -51,7 +51,7 @@ Proof.
   iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
   iApply twptp_ind; iIntros "!#" (t1) "IH"; iIntros (t1' Ht).
   rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 σ2 Hstep) "Hσ".
-  destruct (step_Permutation t1' t1 t2 σ1 σ2) as (t2'&?&?); try done.
+  destruct (erased_step_Permutation t1' t1 t2 σ1 σ2) as (t2'&?&?); try done.
   iMod ("IH" $! t2' with "[% //] Hσ") as "[$ [IH _]]". by iApply "IH".
 Qed.
 
@@ -62,20 +62,20 @@ Proof.
   iRevert (t1) "IH1"; iRevert (t2) "H2".
   iApply twptp_ind; iIntros "!#" (t2) "IH2". iIntros (t1) "IH1".
   rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 σ2 Hstep) "Hσ1".
-  destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' ?? Hstep]; simplify_eq/=.
+  destruct Hstep as [κ [e1 σ1' e2 σ2' efs' t1' t2' ?? Hstep]]; simplify_eq/=.
   apply app_eq_inv in H as [(t&?&?)|(t&?&?)]; subst.
   - destruct t as [|e1' ?]; simplify_eq/=.
-    + iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]".
+    + iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]". eexists.
       { by eapply step_atomic with (t1:=[]). }
       iModIntro. rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
       by setoid_rewrite (right_id_L [] (++)).
-    + iMod ("IH1" with "[%] Hσ1") as "[$ [IH1 _]]"; first by econstructor.
+    + iMod ("IH1" with "[%] Hσ1") as "[$ [IH1 _]]"; first by eexists; econstructor.
       iAssert (twptp t2) with "[IH2]" as "Ht2".
       { rewrite twptp_unfold. iApply (twptp_pre_mono with "[] IH2").
         iIntros "!# * [_ ?] //". }
       iModIntro. rewrite -assoc_L (comm _ t2) !cons_middle !assoc_L.
       by iApply "IH1".
-  - iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]"; first by econstructor.
+  - iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]"; first by eexists; econstructor.
     iModIntro. rewrite -assoc. by iApply "IH2".
 Qed.
 
@@ -85,7 +85,7 @@ Proof.
   iRevert (HE). iRevert (e E Φ) "He". iApply twp_ind.
   iIntros "!#" (e E Φ); iIntros "IH" (->).
   rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' σ1' σ2' Hstep) "Hσ1".
-  destruct Hstep as [e1 σ1 e2 σ2 efs [|? t1] t2 ?? Hstep];
+  destruct Hstep as [κ [e1 σ1 e2 σ2 efs [|? t1] t2 ?? Hstep]];
     simplify_eq/=; try discriminate_list.
   destruct (to_val e1) as [v|] eqn:He1.
   { apply val_stuck in Hstep; naive_solver. }
@@ -93,7 +93,7 @@ Proof.
   iMod ("IH" with "[% //]") as "[$ [[IH _] IHfork]]"; iModIntro.
   iApply (twptp_app [_] with "[IH]"); first by iApply "IH".
   clear. iInduction efs as [|e efs] "IH"; simpl.
-  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 σ2 Hstep).
+  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 σ2 [κ Hstep]).
     destruct Hstep; simplify_eq/=; discriminate_list. }
   iDestruct "IHfork" as "[[IH' _] IHfork]".
   iApply (twptp_app [_] with "[IH']"); [by iApply "IH'"|by iApply "IH"].
@@ -101,7 +101,7 @@ Qed.
 
 Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ)%I.
 
-Lemma twptp_total σ t : world σ -∗ twptp t -∗ ▷ ⌜sn step (t, σ)⌝.
+Lemma twptp_total σ t : world σ -∗ twptp t -∗ ▷ ⌜sn erased_step (t, σ)⌝.
 Proof.
   iIntros "Hw Ht". iRevert (σ) "Hw". iRevert (t) "Ht".
   iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ) "(Hw&HE&Hσ)".
@@ -117,7 +117,7 @@ Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
      (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
        stateI σ ∗ WP e @ s; ⊤ [{ Φ }])%I) →
-  sn step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
+  sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp.
   eapply (soundness (M:=iResUR Σ) _ 1); iIntros "/=".
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
index e5d1af45e..7b8775d81 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -16,59 +16,59 @@ Lemma twp_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}=∗
+    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply (twp_lift_step _ E)=>//. iIntros (σ1) "Hσ".
   iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
-  iSplit; [destruct s; auto|]. iIntros (e2 σ2 efs) "%".
+  iSplit; [destruct s; auto|]. iIntros (κ e2 σ2 efs) "%".
   iApply "H". by eauto.
 Qed.
 
 Lemma twp_lift_pure_head_step {s E Φ} e1 :
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
-  (|={E}=> ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
+  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+  (|={E}=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
     WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof using Hinh.
   iIntros (??) ">H". iApply twp_lift_pure_step; eauto.
-  iIntros "!>" (????). iApply "H"; eauto.
+  iIntros "!>" (?????). iApply "H"; eauto.
 Qed.
 
 Lemma twp_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}=∗
+    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; auto. iIntros (e2 σ2 efs) "%". iApply "H"; auto.
+  iSplit; first by destruct s; auto. iIntros (κ e2 σ2 efs) "%". iApply "H"; eauto.
 Qed.
 
 Lemma twp_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}=∗
+    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       ⌜efs = []⌝ ∗ state_interp σ2 ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_head_step; eauto.
   iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
-  iIntros (v2 σ2 efs) "%".
-  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
+  iIntros (κ v2 σ2 efs) "%".
+  iMod ("H" $! κ v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
 Qed.
 
 Lemma twp_lift_pure_det_head_step {s E Φ} e1 e2 efs :
   (∀ σ1, head_reducible e1 σ1) →
-  (∀ σ1 e2' σ2 efs',
-    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+  (∀ σ1 κ e2' σ2 efs',
+    head_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof using Hinh. eauto using twp_lift_pure_det_step. Qed.
@@ -76,8 +76,8 @@ Proof using Hinh. eauto using twp_lift_pure_det_step. Qed.
 Lemma twp_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') →
+  (∀ σ1 κ e2' σ2 efs',
+    head_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
 Proof using Hinh.
   intros. rewrite -(twp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index 571179889..ad5d3a861 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -15,7 +15,7 @@ Lemma twp_lift_step s E Φ e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
@@ -23,8 +23,8 @@ Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
 (** Derived lifting lemmas. *)
 Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
   (∀ σ1, reducible e1 σ1) →
-  (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
-  (|={E}=> ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
+  (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+  (|={E}=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
     WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
@@ -32,8 +32,8 @@ Proof.
   { eapply reducible_not_val, (Hsafe inhabitant). }
   iIntros (σ1) "Hσ". iMod "H".
   iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
-  iSplit; [by destruct s|]; iIntros (e2 σ2 efs ?).
-  destruct (Hstep σ1 e2 σ2 efs); auto; subst.
+  iSplit; [by destruct s|]; iIntros (κ e2 σ2 efs ?).
+  destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
   iMod "Hclose" as "_". iFrame "Hσ". iApply "H"; auto.
 Qed.
 
@@ -43,7 +43,7 @@ Lemma twp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
@@ -51,21 +51,21 @@ Proof.
   iIntros (?) "H". iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-  iIntros "!>" (e2 σ2 efs) "%". iMod "Hclose" as "_".
-  iMod ("H" $! e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
+  iIntros "!>" (κ e2 σ2 efs) "%". iMod "Hclose" as "_".
+  iMod ("H" $! κ e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
   destruct (to_val e2) eqn:?; last by iExFalso.
   iApply twp_value; last done. by apply of_to_val.
 Qed.
 
 Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s 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')→
+  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
   (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (? Hpuredet) ">H". iApply (twp_lift_pure_step _ E); try done.
-  { by intros; eapply Hpuredet. }
-  by iIntros "!>" (e' efs' σ (_&->&->)%Hpuredet).
+  { by naive_solver. }
+  by iIntros "!>" (κ e' efs' σ (->&_&->&->)%Hpuredet).
 Qed.
 
 Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ Φ :
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 9e8cf93ef..fd96dd737 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -11,7 +11,7 @@ Definition twp_pre `{irisG Λ Σ} (s : stuckness)
   | Some v => |={E}=> Φ v
   | None => ∀ σ1,
      state_interp σ1 ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+     ∀ κ 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.
@@ -24,7 +24,7 @@ Proof.
   iIntros "#H"; iIntros (E e1 Φ) "Hwp". rewrite /twp_pre.
   destruct (to_val e1) as [v|]; first done.
   iIntros (σ1) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
-  iIntros (e2 σ2 efs) "Hstep".
+  iIntros (κ e2 σ2 efs) "Hstep".
   iMod ("Hwp" with "Hstep") as "($ & Hwp & Hfork)"; iModIntro; iSplitL "Hwp".
   - by iApply "H".
   - iApply (@big_sepL_impl with "[$Hfork]"); iIntros "!#" (k e _) "Hwp".
@@ -44,7 +44,7 @@ Proof.
     iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" $! (E,e,Φ)).
   - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
-    rewrite /uncurry3 /twp_pre. do 16 (f_equiv || done). by apply Hwp, pair_ne.
+    rewrite /uncurry3 /twp_pre. do 18 (f_equiv || done). by apply Hwp, pair_ne.
 Qed.
 
 Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
@@ -107,7 +107,7 @@ Proof.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
   iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
   iMod ("IH" with "[$]") as "[% IH]".
-  iModIntro; iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
+  iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
   iMod ("IH" with "[//]") as "($ & IH & IHefs)"; auto.
   iMod "Hclose" as "_"; iModIntro. iSplitR "IHefs".
   - iDestruct "IH" as "[IH _]". iApply ("IH" with "[//] HΦ").
@@ -131,13 +131,13 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
   iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
-  iModIntro. iIntros (e2 σ2 efs Hstep).
+  iModIntro. iIntros (κ e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "(Hphy & H & $)". destruct s.
   - rewrite !twp_unfold /twp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
-    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
-      by edestruct (atomic _ _ _ _ Hstep).
-  - destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
+    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
+      by edestruct (atomic _ _ _ _ _ Hstep).
+  - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
     iMod (twp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply twp_value'.
 Qed.
 
@@ -155,9 +155,9 @@ Proof.
   iIntros (σ1) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
   { iPureIntro. unfold reducible in *.
     destruct s; naive_solver eauto using fill_step. }
-  iIntros (e2 σ2 efs Hstep).
-  destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
-  iMod ("IH" $! e2' σ2 efs with "[//]") as "($ & IH & IHfork)".
+  iIntros (κ e2 σ2 efs Hstep).
+  destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
+  iMod ("IH" $! κ e2' σ2 efs with "[//]") as "($ & IH & IHfork)".
   iModIntro; iSplitR "IHfork".
   - iDestruct "IH" as "[IH _]". by iApply "IH".
   - by setoid_rewrite and_elim_r.
@@ -175,8 +175,8 @@ Proof.
   rewrite /twp_pre fill_not_val //.
   iIntros (σ1) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
   { destruct s; eauto using reducible_fill. }
-  iIntros (e2 σ2 efs Hstep).
-  iMod ("IH" $! (K e2) σ2 efs with "[]") as "($ & IH & IHfork)"; eauto using fill_step.
+  iIntros (κ e2 σ2 efs Hstep).
+  iMod ("IH" $! κ (K e2) σ2 efs with "[]") as "($ & IH & IHfork)"; eauto using fill_step.
   iModIntro; iSplitR "IHfork".
   - iDestruct "IH" as "[IH _]". by iApply "IH".
   - by setoid_rewrite and_elim_r.
@@ -187,7 +187,7 @@ Proof.
   iIntros "H". iLöb as "IH" forall (E e Φ).
   rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//.
   iIntros (σ1) "Hσ". iMod ("H" with "Hσ") as "[$ H]". iIntros "!>".
-  iIntros (e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as "($ & H & Hfork)".
+  iIntros (κ e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as "($ & H & Hfork)".
   iApply step_fupd_intro; [set_solver+|]. iNext.
   iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]").
   iIntros "!#" (k e' _) "H". by iApply "IH".
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 023966eb0..5bacf60b4 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -7,7 +7,7 @@ Import uPred.
 
 Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
   iris_invG :> invG Σ;
-  state_interp : Λstate → iProp Σ;
+  state_interp : Λstate -> (*list (option Λobservations) → *) iProp Σ;
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 Global Opaque iris_invG.
@@ -19,7 +19,7 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
   | Some v => |={E}=> Φ v
   | None => ∀ σ1,
      state_interp σ1 ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,∅,E}▷=∗
+     ∀ κ 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.
@@ -57,8 +57,8 @@ Proof.
   (* FIXME: figure out a way to properly automate this proof *)
   (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
   is very slow here *)
-  do 18 (f_contractive || f_equiv). apply IH; first lia.
-  intros v. eapply dist_le; eauto with lia.
+  do 20 (f_contractive || f_equiv). apply IH; first lia.
+  intros v. eapply dist_le; eauto with omega.
 Qed.
 Global Instance wp_proper s E e :
   Proper (pointwise_relation _ (≡) ==> (≡)) (wp (PROP:=iProp Σ) s E e).
@@ -81,7 +81,7 @@ Proof.
   { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
   iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
   iMod ("H" with "[$]") as "[% H]".
-  iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
+  iModIntro. iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "H". iIntros "!> !>". iMod "H" as "($ & H & Hefs)".
   iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
   - iApply ("IH" with "[//] H HΦ").
@@ -105,13 +105,13 @@ Proof.
   destruct (to_val e) as [v|] eqn:He.
   { by iDestruct "H" as ">>> $". }
   iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
-  iModIntro. iIntros (e2 σ2 efs Hstep).
+  iModIntro. iIntros (κ e2 σ2 efs Hstep).
   iMod ("H" with "[//]") as "H". iIntros "!>!>". iMod "H" as "(Hphy & H & $)". destruct s.
   - rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
     + iDestruct "H" as ">> $". by iFrame.
-    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
-      by edestruct (atomic _ _ _ _ Hstep).
-  - destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
+    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
+      by edestruct (atomic _ _ _ _ _ Hstep).
+  - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
     iMod (wp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply wp_value'.
 Qed.
 
@@ -121,7 +121,7 @@ Lemma wp_step_fupd s E1 E2 e P Φ :
 Proof.
   rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
   iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
-  iIntros "!>" (e2 σ2 efs Hstep). iMod ("H" $! e2 σ2 efs with "[% //]") as "H".
+  iIntros "!>" (κ e2 σ2 efs Hstep). iMod ("H" $! κ e2 σ2 efs with "[% //]") as "H".
   iIntros "!>!>". iMod "H" as "($ & H & $)".
   iMod "HR". iModIntro. iApply (wp_strong_mono s s E2 with "H"); [done..|].
   iIntros (v) "H". by iApply "H".
@@ -137,9 +137,9 @@ Proof.
   iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
   { iPureIntro. destruct s; last done.
     unfold reducible in *. naive_solver eauto using fill_step. }
-  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". iIntros "!>!>".
+  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". iIntros "!>!>".
   iMod "H" as "($ & H & $)". by iApply "IH".
 Qed.
 
@@ -152,8 +152,8 @@ Proof.
   rewrite fill_not_val //.
   iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
   { destruct s; eauto using reducible_fill. }
-  iIntros (e2 σ2 efs Hstep).
-  iMod ("H" $! (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
+  iIntros (κ e2 σ2 efs Hstep).
+  iMod ("H" $! κ (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
   iIntros "!>!>". iMod "H" as "($ & H & $)". by iApply "IH".
 Qed.
 
-- 
GitLab