From 25ed5c9c0d6d0b2912c1ecb6afecd08f982c0df9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 18 Oct 2018 11:10:41 +0200
Subject: [PATCH] generalize to lists of observations per program step

---
 theories/heap_lang/lang.v                   | 43 +++++++++++----------
 theories/heap_lang/lifting.v                |  1 -
 theories/program_logic/adequacy.v           |  8 ++--
 theories/program_logic/ectx_language.v      | 10 ++---
 theories/program_logic/ectx_lifting.v       | 20 +++++-----
 theories/program_logic/ectxi_language.v     |  4 +-
 theories/program_logic/language.v           | 16 +++-----
 theories/program_logic/lifting.v            | 12 +++---
 theories/program_logic/ownp.v               | 28 +++++++-------
 theories/program_logic/total_adequacy.v     |  2 +-
 theories/program_logic/total_ectx_lifting.v | 12 +++---
 theories/program_logic/total_lifting.v      |  8 ++--
 theories/program_logic/total_weakestpre.v   |  2 +-
 theories/program_logic/weakestpre.v         |  4 +-
 14 files changed, 83 insertions(+), 87 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 168df6524..a206efb6f 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -448,82 +448,83 @@ Definition state_upd_used_proph (f: gset proph → gset proph) (σ: state) :=
   {| heap := σ.(heap); used_proph := f σ.(used_proph) |}.
 Arguments state_upd_used_proph _ !_ /.
 
-Inductive head_step : expr → state → option observation → expr → state → list (expr) → Prop :=
+Inductive head_step : expr → state → list 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) σ None e' σ []
+     head_step (App (Rec f x e1) e2) σ [] e' σ []
   | UnOpS op e v v' σ :
      to_val e = Some v →
      un_op_eval op v = Some v' →
-     head_step (UnOp op e) σ None (of_val v') σ []
+     head_step (UnOp op e) σ [] (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) σ None (of_val v') σ []
+     head_step (BinOp op e1 e2) σ [] (of_val v') σ []
   | IfTrueS e1 e2 σ :
-     head_step (If (Lit $ LitBool true) e1 e2) σ None e1 σ []
+     head_step (If (Lit $ LitBool true) e1 e2) σ [] e1 σ []
   | IfFalseS e1 e2 σ :
-     head_step (If (Lit $ LitBool false) e1 e2) σ None e2 σ []
+     head_step (If (Lit $ LitBool false) e1 e2) σ [] e2 σ []
   | FstS e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     head_step (Fst (Pair e1 e2)) σ None e1 σ []
+     head_step (Fst (Pair e1 e2)) σ [] e1 σ []
   | SndS e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
-     head_step (Snd (Pair e1 e2)) σ None e2 σ []
+     head_step (Snd (Pair e1 e2)) σ [] e2 σ []
   | CaseLS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
-     head_step (Case (InjL e0) e1 e2) σ None (App e1 e0) σ []
+     head_step (Case (InjL e0) e1 e2) σ [] (App e1 e0) σ []
   | CaseRS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
-     head_step (Case (InjR e0) e1 e2) σ None (App e2 e0) σ []
+     head_step (Case (InjR e0) e1 e2) σ [] (App e2 e0) σ []
   | ForkS e σ:
-     head_step (Fork e) σ None (Lit LitUnit) σ [e]
+     head_step (Fork e) σ [] (Lit LitUnit) σ [e]
   | AllocS e v σ l :
      to_val e = Some v → σ.(heap) !! l = None →
      head_step (Alloc e) σ
-               None (Lit $ LitLoc l) (state_upd_heap <[l:=v]> σ)
+               []
+               (Lit $ LitLoc l) (state_upd_heap <[l:=v]> σ)
                []
   | LoadS l v σ :
      σ.(heap) !! l = Some v →
-     head_step (Load (Lit $ LitLoc l)) σ None (of_val v) σ []
+     head_step (Load (Lit $ LitLoc l)) σ [] (of_val v) σ []
   | StoreS l e v σ :
      to_val e = Some v → is_Some (σ.(heap) !! l) →
      head_step (Store (Lit $ LitLoc l) e) σ
-               None
+               []
                (Lit LitUnit) (state_upd_heap <[l:=v]> σ)
                []
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ.(heap) !! l = Some vl → vl ≠ v1 →
      vals_cas_compare_safe vl v1 →
-     head_step (CAS (Lit $ LitLoc l) e1 e2) σ None (Lit $ LitBool false) σ []
+     head_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ LitBool false) σ []
   | CasSucS l e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ.(heap) !! l = Some v1 →
      vals_cas_compare_safe v1 v1 →
      head_step (CAS (Lit $ LitLoc l) e1 e2) σ
-               None
+               []
                (Lit $ LitBool true) (state_upd_heap <[l:=v2]> σ)
                []
   | FaaS l i1 e2 i2 σ :
      to_val e2 = Some (LitV (LitInt i2)) →
      σ.(heap) !! l = Some (LitV (LitInt i1)) →
      head_step (FAA (Lit $ LitLoc l) e2) σ
-               None
+               []
                (Lit $ LitInt i1) (state_upd_heap <[l:=LitV (LitInt (i1 + i2))]> σ)
                []
   | NewProphS σ p :
      p ∉ σ.(used_proph) →
      head_step NewProph σ
-               None
+               []
                (Lit $ LitProphecy p) (state_upd_used_proph ({[ p ]} ∪) σ)
                []
   | ResolveProphS e1 p e2 v σ :
      to_val e1 = Some (LitV $ LitProphecy p) →
      to_val e2 = Some v →
-     head_step (ResolveProph e1 e2) σ (Some (p, v)) (Lit LitUnit) σ [].
+     head_step (ResolveProph e1 e2) σ [(p, v)] (Lit LitUnit) σ [].
 
 (** Basic properties about the language *)
 Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
@@ -553,12 +554,12 @@ Qed.
 Lemma alloc_fresh e v σ :
   let l := fresh (dom (gset loc) σ.(heap)) in
   to_val e = Some v →
-  head_step (Alloc e) σ None (Lit (LitLoc l)) (state_upd_heap <[l:=v]> σ) [].
+  head_step (Alloc e) σ [] (Lit (LitLoc l)) (state_upd_heap <[l:=v]> σ) [].
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
 
 Lemma new_proph_fresh σ :
   let p := fresh σ.(used_proph) in
-  head_step NewProph σ None (Lit $ LitProphecy p) (state_upd_used_proph ({[ p ]} ∪) σ) [].
+  head_step NewProph σ [] (Lit $ LitProphecy p) (state_upd_used_proph ({[ p ]} ∪) σ) [].
 Proof. constructor. apply is_fresh. Qed.
 
 (* Misc *)
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 4b19908fa..bef2ebca3 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -292,7 +292,6 @@ Lemma wp_resolve_proph e1 e2 p v w:
   {{{ p ⥱ v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}.
 Proof.
   iIntros (<- <- Φ) "Hp HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
-  unfold cons_obs. simpl.
   iIntros (σ1 κ κs) "[Hσ HR] !>". iDestruct "HR" as (R [Hfr Hdom]) "HR".
   iDestruct (@proph_map_valid with "HR Hp") as %Hlookup.
   iSplit; first by eauto.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index ee2b5375b..095aa0c67 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -73,7 +73,7 @@ Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
 
 Lemma wp_step s E e1 σ1 κ κs e2 σ2 efs Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
-  world' E σ1 (cons_obs κ κs) ∗ WP e1 @ s; E {{ Φ }}
+  world' E σ1 (κ ++ κs) ∗ WP e1 @ s; E {{ Φ }}
   ==∗  ▷ |==> ◇ (world' E σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
@@ -85,7 +85,7 @@ Qed.
 
 Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
   step (e1 :: t1,σ1) κ (t2, σ2) →
-  world σ1 (cons_obs κ κs) ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
+  world σ1 (κ ++ κs) ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
   ==∗ ∃ e2 t2',
     ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 κs ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
@@ -107,7 +107,7 @@ Proof.
   revert e1 t1 κs κs' t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
   { inversion_clear 1; iIntros "?"; eauto 10. }
   iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
-  rewrite /cons_obs. rewrite <- app_assoc.
+  rewrite <- app_assoc.
   iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first by eauto; simplify_eq.
   subst. iModIntro; iNext; iMod "H" as ">H". by iApply IH.
 Qed.
@@ -145,7 +145,7 @@ Proof.
   rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
   destruct (to_val e) as [v|] eqn:?.
   { iIntros "!> !> !%". left. by exists v. }
-  rewrite uPred_fupd_eq. iMod ("H" $! _ None with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
+  rewrite uPred_fupd_eq. iMod ("H" $! _ [] with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
   iIntros "!> !> !%". by right.
 Qed.
 
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 45eaf1cc1..c591c3a65 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -16,7 +16,7 @@ Section ectx_language_mixin.
   Context (empty_ectx : ectx).
   Context (comp_ectx : ectx → ectx → ectx).
   Context (fill : ectx → expr → expr).
-  Context (head_step : expr → state → option observation → expr → state → list expr → Prop).
+  Context (head_step : expr → state → list observation → expr → state → list expr → Prop).
 
   Record EctxLanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
@@ -55,7 +55,7 @@ Structure ectxLanguage := EctxLanguage {
   empty_ectx : ectx;
   comp_ectx : ectx → ectx → ectx;
   fill : ectx → expr → expr;
-  head_step : expr → state → option observation → expr → state → list expr → Prop;
+  head_step : expr → state → list observation → expr → state → list expr → Prop;
 
   ectx_language_mixin :
     EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
@@ -100,7 +100,7 @@ Section ectx_language.
   Definition head_reducible (e : expr Λ) (σ : state Λ) :=
     ∃ κ e' σ' efs, head_step e σ κ e' σ' efs.
   Definition head_reducible_no_obs (e : expr Λ) (σ : state Λ) :=
-    ∃ e' σ' efs, head_step e σ None e' σ' efs.
+    ∃ e' σ' efs, head_step e σ [] e' σ' efs.
   Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ κ e' σ' efs, ¬head_step e σ κ e' σ' efs.
   Definition head_stuck (e : expr Λ) (σ : state Λ) :=
@@ -111,7 +111,7 @@ 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 Λ) (κ : option (observation Λ))
+  Inductive prim_step (e1 : expr Λ) (σ1 : state Λ) (κ : list (observation Λ))
       (e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
     Ectx_step K e1' e2' :
       e1 = fill K e1' → e2 = fill K e2' →
@@ -217,7 +217,7 @@ Section ectx_language.
   Record pure_head_step (e1 e2 : expr Λ) := {
     pure_head_step_safe σ1 : head_reducible_no_obs e1 σ1;
     pure_head_step_det σ1 κ e2' σ2 efs :
-      head_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []
+      head_step e1 σ1 κ e2' σ2 efs → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []
   }.
 
   Lemma pure_head_step_pure_step e1 e2 : pure_head_step e1 e2 → pure_step e1 e2.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 6b24aa902..080d39947 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -16,7 +16,7 @@ Hint Resolve head_stuck_stuck.
 
 Lemma wp_lift_head_step_fupd {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
+  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
       state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
@@ -30,7 +30,7 @@ Qed.
 
 Lemma wp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
+  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
@@ -52,7 +52,7 @@ 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 → κ = None ∧ σ1 = σ2) →
+  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ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 {{ Φ }}.
@@ -76,7 +76,7 @@ Qed.
 
 Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
+  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
       state_interp σ2 κs ∗
@@ -91,7 +91,7 @@ Qed.
 
 Lemma wp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
+  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 κs ∗
@@ -106,7 +106,7 @@ Qed.
 
 Lemma wp_lift_atomic__head_step_no_fork_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
+  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E1}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
       ⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
@@ -121,7 +121,7 @@ Qed.
 
 Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
+  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E}=∗
     ⌜head_reducible e1 σ1⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       ⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
@@ -136,7 +136,7 @@ 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' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ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.
@@ -148,7 +148,7 @@ 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' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ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.
@@ -159,7 +159,7 @@ 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' → κ = None ∧  σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧  σ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 727425b11..603d21651 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -31,7 +31,7 @@ Section ectxi_language_mixin.
   Context (of_val : val → expr).
   Context (to_val : expr → option val).
   Context (fill_item : ectx_item → expr → expr).
-  Context (head_step : expr → state → option observation → expr → state → list expr → Prop).
+  Context (head_step : expr → state → list observation → expr → state → list expr → Prop).
 
   Record EctxiLanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
@@ -59,7 +59,7 @@ Structure ectxiLanguage := EctxiLanguage {
   of_val : val → expr;
   to_val : expr → option val;
   fill_item : ectx_item → expr → expr;
-  head_step : expr → state → option observation → expr → state → list expr → Prop;
+  head_step : expr → state → list observation → expr → state → list expr → Prop;
 
   ectxi_language_mixin :
     EctxiLanguageMixin of_val to_val fill_item head_step
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index de88479fc..5512fb3f3 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -8,7 +8,7 @@ Section language_mixin.
   (** We annotate the reduction relation with observations [κ], which we will
      use in the definition of weakest preconditions to predict future
      observations and assert correctness of the predictions. *)
-  Context (prim_step : expr → state → option observation → expr → state → list expr → Prop).
+  Context (prim_step : expr → state → list observation → expr → state → list expr → Prop).
 
   Record LanguageMixin := {
     mixin_to_of_val v : to_val (of_val v) = Some v;
@@ -24,7 +24,7 @@ Structure language := Language {
   observation : Type;
   of_val : val → expr;
   to_val : expr → option val;
-  prim_step : expr → state → option observation → expr → state → list expr → Prop;
+  prim_step : expr → state → list observation → expr → state → list expr → Prop;
   language_mixin : LanguageMixin of_val to_val prim_step
 }.
 Delimit Scope expr_scope with E.
@@ -75,7 +75,7 @@ Section language.
     ∃ κ e' σ' efs, prim_step e σ κ e' σ' efs.
   (* Total WP only permits reductions without observations *)
   Definition reducible_no_obs (e : expr Λ) (σ : state Λ) :=
-    ∃ e' σ' efs, prim_step e σ None e' σ' efs.
+    ∃ e' σ' efs, prim_step e σ [] e' σ' efs.
   Definition irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ κ e' σ' efs, ¬prim_step e σ κ e' σ' efs.
   Definition stuck (e : expr Λ) (σ : state Λ) :=
@@ -97,7 +97,7 @@ Section language.
       prim_step e σ κ e' σ' efs →
       if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
 
-  Inductive step (ρ1 : cfg Λ) (κ : option (observation Λ)) (ρ2 : cfg Λ) : Prop :=
+  Inductive step (ρ1 : cfg Λ) (κ : list (observation Λ)) (ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
        ρ1 = (t1 ++ e1 :: t2, σ1) →
        ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2) →
@@ -105,17 +105,13 @@ Section language.
        step ρ1 κ ρ2.
   Hint Constructors step.
 
-  (* TODO (MR) introduce notation ::? for cons_obs and suggest for inclusion to stdpp? *)
-  Definition cons_obs {A} (x : option A) (xs : list A) :=
-    option_list x ++ xs.
-
   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 (cons_obs κ κs) ρ3.
+       nsteps (S n) ρ1 (κ ++ κs) ρ3.
   Hint Constructors nsteps.
 
   Definition erased_step (ρ1 ρ2 : cfg Λ) := ∃ κ, step ρ1 κ ρ2.
@@ -180,7 +176,7 @@ Section language.
   Record pure_step (e1 e2 : expr Λ) := {
     pure_step_safe σ1 : reducible_no_obs e1 σ1;
     pure_step_det σ1 κ e2' σ2 efs :
-      prim_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []
+      prim_step e1 σ1 κ e2' σ2 efs → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = []
   }.
 
   (* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 5b836d2bf..1185a506f 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -15,7 +15,7 @@ Hint Resolve reducible_no_obs_reducible.
 
 Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
+  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
       state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
@@ -39,7 +39,7 @@ Qed.
 (** Derived lifting lemmas. *)
 Lemma wp_lift_step s E Φ e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
+  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E,∅}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
@@ -51,7 +51,7 @@ 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 → κ = None ∧ σ1 = σ2) →
+  (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ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 {{ Φ }}.
@@ -82,7 +82,7 @@ Qed.
    use the generic lemmas here. *)
 Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E1}=∗
+  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E1}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E1,E2}▷=∗
       state_interp σ2 κs ∗
@@ -102,7 +102,7 @@ Qed.
 
 Lemma wp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
-  (∀ σ1 κ κs, state_interp σ1 (cons_obs κ κs) ={E}=∗
+  (∀ σ1 κ κs, state_interp σ1 (κ ++ κs) ={E}=∗
     ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 κs ∗
@@ -117,7 +117,7 @@ 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' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
+  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
   (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 27d605146..42455a4d1 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -118,7 +118,7 @@ Section lifting.
   Lemma ownP_lift_step s E Φ e1 :
     (|={E,∅}=> ∃ σ1 κs, ⌜if s is NotStuck then reducible e1 σ1 else to_val e1 = None⌝ ∗
       ▷ ownP_state σ1 ∗ ▷ ownP_obs κs ∗
-      ▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗
+      ▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = κ ++ κs'⌝ -∗
       ownP_state σ2 ∗ ownP_obs κs'
             ={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
@@ -158,7 +158,7 @@ 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 → κ = None ∧ σ1 = σ2) →
+    (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
     (▷ ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
       WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
@@ -176,7 +176,7 @@ Section lifting.
   Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 κs :
     (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (▷ (ownP_state σ1 ∗ ownP_obs κs) ∗
-       ▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗
+       ▷ ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = κ ++ κs'⌝ -∗
          ownP_state σ2 -∗ ownP_obs κs' -∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
@@ -194,7 +194,7 @@ Section lifting.
     (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (∀ κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' →
                      κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
-    ▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) ∗ ▷ (ownP_state σ2 -∗ ownP_obs κs -∗
+    ▷ (ownP_state σ1 ∗ ownP_obs (κ ++ κs)) ∗ ▷ (ownP_state σ2 -∗ ownP_obs κs -∗
       Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
@@ -208,7 +208,7 @@ Section lifting.
     (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (∀ κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' →
       κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
-    {{{ ▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ∗ ownP_obs κs}}}.
+    {{{ ▷ (ownP_state σ1 ∗ ownP_obs (κ ++ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ∗ ownP_obs κs}}}.
   Proof.
     intros. rewrite -(ownP_lift_atomic_det_step σ1 κ κs v2 σ2 []); [|done..].
     rewrite big_sepL_nil right_id. apply bi.wand_intro_r. iIntros "[Hs Hs']".
@@ -217,7 +217,7 @@ 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' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
+    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
     ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤{{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
@@ -227,7 +227,7 @@ Section lifting.
 
   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' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
     intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
@@ -246,7 +246,7 @@ Section ectx_lifting.
 
   Lemma ownP_lift_head_step s E Φ e1 :
     (|={E,∅}=> ∃ σ1 κs, ⌜head_reducible e1 σ1⌝ ∗ ▷ (ownP_state σ1  ∗ ownP_obs κs) ∗
-            ▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗
+            ▷ ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = κ ++ κs'⌝ -∗
             ownP_state σ2 -∗ ownP_obs κs'
             ={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
@@ -269,7 +269,7 @@ 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 → κ = None ∧ σ1 = σ2) →
+    (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ1 = σ2) →
     (▷ ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
       WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
@@ -282,7 +282,7 @@ Section ectx_lifting.
   Lemma ownP_lift_atomic_head_step {s E Φ} e1 σ1 κs :
     head_reducible e1 σ1 →
     ▷ (ownP_state σ1 ∗ ownP_obs κs) ∗ ▷ (∀ κ κs' e2 σ2 efs,
-    ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ -∗ ownP_state σ2 -∗ ownP_obs κs' -∗
+    ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = κ ++ κs'⌝ -∗ ownP_state σ2 -∗ ownP_obs κs' -∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
@@ -296,7 +296,7 @@ Section ectx_lifting.
     head_reducible e1 σ1 →
     (∀ κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' →
       κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
-    ▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) ∗ ▷ (ownP_state σ2 -∗ ownP_obs κs -∗
+    ▷ (ownP_state σ1 ∗ ownP_obs (κ ++ κs)) ∗ ▷ (ownP_state σ2 -∗ ownP_obs κs -∗
                                                     Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
@@ -307,7 +307,7 @@ Section ectx_lifting.
     head_reducible e1 σ1 →
     (∀ κ' e2' σ2' efs', head_step e1 σ1 κ' e2' σ2' efs' →
       κ = κ' ∧ σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
-    {{{ ▷ (ownP_state σ1 ∗ ownP_obs (cons_obs κ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ∗ ownP_obs κs }}}.
+    {{{ ▷ (ownP_state σ1 ∗ ownP_obs (κ ++ κs)) }}} e1 @ s; E {{{ RET v2; ownP_state σ2 ∗ ownP_obs κs }}}.
   Proof.
     intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
     by destruct s; eauto using reducible_not_val.
@@ -315,7 +315,7 @@ Section ectx_lifting.
 
   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' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
     ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
   Proof using Hinh.
@@ -325,7 +325,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' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    (∀ σ1 κ e2' σ2 efs', head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ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 ab7b110d2..186b282e4 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -13,7 +13,7 @@ Implicit Types e : expr Λ.
 Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
     (t1 : list (expr Λ)) : iProp Σ :=
   (∀ t2 σ1 κ κs σ2, ⌜step (t1,σ1) κ (t2,σ2)⌝ -∗
-    state_interp σ1 κs ={⊤}=∗ ⌜κ = None⌝ ∗ state_interp σ2 κs ∗ twptp t2)%I.
+    state_interp σ1 κs ={⊤}=∗ ⌜κ = []⌝ ∗ state_interp σ2 κs ∗ twptp t2)%I.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
   (<pers> (∀ t, twptp1 t -∗ twptp2 t) →
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
index 48130bafc..5e7748848 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -17,7 +17,7 @@ Lemma twp_lift_head_step {s E Φ} e1 :
   (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
     ⌜head_reducible_no_obs e1 σ1⌝ ∗
     ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      ⌜κ = None⌝ ∗ state_interp σ2 κs ∗
+      ⌜κ = []⌝ ∗ state_interp σ2 κs ∗
       WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
@@ -29,7 +29,7 @@ Qed.
 
 Lemma twp_lift_pure_head_step {s E Φ} e1 :
   (∀ σ1, head_reducible_no_obs e1 σ1) →
-  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
+  (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ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 [{ Φ }].
@@ -43,7 +43,7 @@ Lemma twp_lift_atomic_head_step {s E Φ} e1 :
   (∀ σ1 κs, state_interp σ1 κs ={E}=∗
     ⌜head_reducible_no_obs e1 σ1⌝ ∗
     ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜κ = None⌝ ∗ state_interp σ2 κs ∗
+      ⌜κ = []⌝ ∗ state_interp σ2 κs ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
@@ -57,7 +57,7 @@ Lemma twp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   (∀ σ1 κs, state_interp σ1 κs ={E}=∗
     ⌜head_reducible_no_obs e1 σ1⌝ ∗
     ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜κ = None⌝ ∗ ⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
+      ⌜κ = []⌝ ∗ ⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_head_step; eauto.
@@ -69,7 +69,7 @@ Qed.
 Lemma twp_lift_pure_det_head_step {s E Φ} e1 e2 efs :
   (∀ σ1, head_reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ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 10 using twp_lift_pure_det_step. Qed.
@@ -78,7 +78,7 @@ Lemma twp_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
   to_val e1 = None →
   (∀ σ1, head_reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
-    head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+    head_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ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 3a9a775ce..dc6f8e3ec 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -16,7 +16,7 @@ Lemma twp_lift_step s E Φ e1 :
   (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
     ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
     ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-      ⌜κ = None⌝ ∗ state_interp σ2 κs ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+      ⌜κ = []⌝ ∗ state_interp σ2 κs ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
 
@@ -24,7 +24,7 @@ Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
 
 Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
   (∀ σ1, reducible_no_obs e1 σ1) →
-  (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ1 = σ2) →
+  (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] /\ σ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 [{ Φ }].
@@ -46,7 +46,7 @@ Lemma twp_lift_atomic_step {s E Φ} e1 :
   (∀ σ1 κs, state_interp σ1 κs ={E}=∗
     ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
     ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
-      ⌜κ = None⌝ ∗ state_interp σ2 κs ∗
+      ⌜κ = []⌝ ∗ state_interp σ2 κs ∗
       from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
@@ -61,7 +61,7 @@ Qed.
 
 Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
   (∀ σ1, reducible_no_obs e1 σ1) →
-  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
+  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
   (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index c27629d3e..aa53b6716 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -12,7 +12,7 @@ Definition twp_pre `{irisG Λ Σ} (s : stuckness)
   | None => ∀ σ1 κs,
      state_interp σ1 κs ={E,∅}=∗ ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
      ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
-       ⌜κ = None⌝ ∗ state_interp σ2 κs ∗
+       ⌜κ = []⌝ ∗ state_interp σ2 κs ∗
        wp E e2 Φ ∗ [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
   end%I.
 
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 7ba7ec99e..bcaa16f44 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -18,7 +18,7 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
   match to_val e1 with
   | Some v => |={E}=> Φ v
   | None => ∀ σ1 κ κs,
-      state_interp σ1 (cons_obs κ κs) ={E,∅}=∗
+      state_interp σ1 (κ ++ κs) ={E,∅}=∗
         ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
         ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,∅,E}▷=∗
           state_interp σ2 κs ∗ wp E e2 Φ ∗ [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
@@ -109,7 +109,7 @@ Proof.
   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" $! _ None with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ? & ?).
+    + 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'.
-- 
GitLab