diff --git a/_CoqProject b/_CoqProject
index 13c296354ff16a778c455e79595df5e381685a62..338f805ac4ddffc70a792ce2f7abc285585a3ba9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -56,12 +56,16 @@ theories/base_logic/lib/fancy_updates_from_vs.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
 theories/program_logic/weakestpre.v
+theories/program_logic/total_weakestpre.v
+theories/program_logic/total_adequacy.v
 theories/program_logic/hoare.v
 theories/program_logic/language.v
 theories/program_logic/ectx_language.v
 theories/program_logic/ectxi_language.v
 theories/program_logic/ectx_lifting.v
 theories/program_logic/ownp.v
+theories/program_logic/total_lifting.v
+theories/program_logic/total_ectx_lifting.v
 theories/heap_lang/lang.v
 theories/heap_lang/tactics.v
 theories/heap_lang/lifting.v
@@ -75,6 +79,7 @@ theories/heap_lang/lib/ticket_lock.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v
+theories/heap_lang/total_adequacy.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
diff --git a/theories/heap_lang/lib/assert.v b/theories/heap_lang/lib/assert.v
index e111f3c831d7d8b69cf89580fc9258142258878d..ce10822a07640763dedaa3c9e61b88f705015d9f 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/theories/heap_lang/lib/assert.v
@@ -9,6 +9,13 @@ Definition assert : val :=
 (* just below ;; *)
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 
+Lemma twp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
+  WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗ WP assert: e @ E [{ Φ }].
+Proof.
+  iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
+  wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
+Qed.
+
 Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
 Proof.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 5369e0a9a0fbe09ab14145d2509104ecdc74a679..94c8b1e8942243bc0bba771d1498ed8eb2e8d1b1 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,14 +1,11 @@
 From iris.base_logic Require Export gen_heap.
-From iris.program_logic Require Export weakestpre lifting.
-From iris.program_logic Require Import ectx_lifting.
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
 From stdpp Require Import fin_maps.
 Set Default Proof Using "Type".
-Import uPred.
-
-(** Basic rules for language operations. *)
 
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
@@ -39,8 +36,6 @@ 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 : _ = of_val ?v |- _ =>
-     is_var v; destruct v; first[discriminate H|injection H as H]
   | 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. *)
@@ -54,22 +49,6 @@ Local Hint Constructors head_step.
 Local Hint Resolve alloc_fresh.
 Local Hint Resolve to_of_val.
 
-Section lifting.
-Context `{heapG Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-Implicit Types efs : list expr.
-Implicit Types σ : state.
-
-(** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork s E e Φ :
-  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}.
-Proof.
-  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ _ (Lit _)) // right_id.
-  - intros; inv_head_step; eauto.
-Qed.
-
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
 Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pure_exec :=
@@ -79,48 +58,69 @@ Local Ltac solve_pure_exec :=
 
 Class AsRec (e : expr) (f x : binder) (erec : expr) :=
   as_rec : e = Rec f x erec.
-Global Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
-Global Instance AsRec_rec_locked_val v f x e :
+Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
+Instance AsRec_rec_locked_val v f x e :
   AsRec (of_val v) f x e → AsRec (of_val (locked v)) f x e.
 Proof. by unlock. Qed.
 
-Global Instance pure_rec f x (erec e1 e2 : expr)
+Instance pure_rec f x (erec e1 e2 : expr)
     `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
   PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
 Proof. unfold AsRec in *; solve_pure_exec. Qed.
 
-Global Instance pure_unop op e v v' `{!IntoVal e v} :
+Instance pure_unop op e v v' `{!IntoVal e v} :
   PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
+Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
   PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_if_true e1 e2 :
-  PureExec True (If (Lit (LitBool true)) e1 e2) e1.
+Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_if_false e1 e2 :
-  PureExec True (If (Lit (LitBool false)) e1 e2) e2.
+Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
+Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
   PureExec True (Fst (Pair e1 e2)) e1.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
+Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
   PureExec True (Snd (Pair e1 e2)) e2.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
+Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
   PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
+Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
   PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
 Proof. solve_pure_exec. Qed.
 
+Section lifting.
+Context `{heapG Σ}.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val → iProp Σ.
+Implicit Types efs : list expr.
+Implicit Types σ : state.
+
+(** Base axioms for core primitives of the language: Stateless reductions *)
+Lemma wp_fork s E e Φ :
+  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}.
+Proof.
+  iIntros "[HΦ He]".
+  iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
+  iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
+Qed.
+Lemma twp_fork s E e Φ :
+  Φ (LitV LitUnit) ∗ WP e @ s; ⊤ [{ _, True }] ⊢ WP Fork e @ s; E [{ Φ }].
+Proof.
+  iIntros "[HΦ He]".
+  iApply twp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
+  iIntros "!> /= {$He}". by iApply twp_value.
+Qed.
+
 (** Heap *)
 Lemma wp_alloc s E e v :
   IntoVal e v →
@@ -132,6 +132,16 @@ Proof.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
+Lemma twp_alloc s E e v :
+  IntoVal e v →
+  [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
+Proof.
+  iIntros (<-%of_to_val Φ) "_ 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.
+  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
 
 Lemma wp_load s E l q v :
   {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}.
@@ -142,6 +152,15 @@ Proof.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
+Lemma twp_load s E l q v :
+  [[{ l ↦{q} v }]] Load (Lit (LitLoc l)) @ s; E [[{ RET v; l ↦{q} v }]].
+Proof.
+  iIntros (Φ) "Hl HΦ". iApply 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.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
 
 Lemma wp_store s E l v' e v :
   IntoVal e v →
@@ -154,6 +173,17 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
+Lemma twp_store s E l v' e v :
+  IntoVal e v →
+  [[{ l ↦ v' }]] Store (Lit (LitLoc l)) e @ s; E [[{ RET LitV LitUnit; l ↦ v }]].
+Proof.
+  iIntros (<-%of_to_val Φ) "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.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
 
 Lemma wp_cas_fail s E l q v' e1 v1 e2 :
   IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
@@ -166,6 +196,17 @@ Proof.
   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 :
+  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
+  [[{ l ↦{q} v' }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
+  [[{ RET LitV (LitBool false); l ↦{q} v' }]].
+Proof.
+  iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) "Hl HΦ".
+  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.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
 
 Lemma wp_cas_suc s E l e1 v1 e2 v2 :
   IntoVal e1 v1 → IntoVal e2 v2 →
@@ -179,6 +220,18 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
+Lemma twp_cas_suc s E l e1 v1 e2 v2 :
+  IntoVal e1 v1 → IntoVal e2 v2 →
+  [[{ l ↦ v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
+  [[{ RET LitV (LitBool true); l ↦ v2 }]].
+Proof.
+  iIntros (<-%of_to_val <-%of_to_val Φ) "Hl HΦ".
+  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.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
 
 Lemma wp_faa s E l i1 e2 i2 :
   IntoVal e2 (LitV (LitInt i2)) →
@@ -192,4 +245,16 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
+Lemma twp_faa s E l i1 e2 i2 :
+  IntoVal e2 (LitV (LitInt i2)) →
+  [[{ l ↦ LitV (LitInt i1) }]] FAA (Lit (LitLoc l)) e2 @ s; E
+  [[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]].
+Proof.
+  iIntros (<-%of_to_val Φ) "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.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
 End lifting.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index a88e475599768ff8011cbae9d866974efac59eb6..24a22025c75200f80494f1ad9b14b2c6c811a297 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics lifting.
@@ -9,10 +9,15 @@ Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
   e = e' →
   envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
+Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
+  e = e' →
+  envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
+Proof. by intros ->. Qed.
 
 Tactic Notation "wp_expr_eval" tactic(t) :=
   try iStartProof;
-  try (eapply tac_wp_expr_eval; [t; reflexivity|]).
+  try (first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
+       [t; reflexivity|]).
 
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
@@ -25,16 +30,28 @@ Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
   envs_entails Δ (WP e1 @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
-  rewrite HΔ' -wp_pure_step_later //.
+  rewrite HΔ' -lifting.wp_pure_step_later //.
+Qed.
+Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ Φ :
+  PureExec φ e1 e2 →
+  φ →
+  envs_entails Δ (WP e2 @ s; E [{ Φ }]) →
+  envs_entails Δ (WP e1 @ s; E [{ Φ }]).
+Proof.
+  rewrite /envs_entails=> ?? ->. rewrite -total_lifting.twp_pure_step //.
 Qed.
 
 Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
   IntoVal e v →
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
+Lemma tac_twp_value `{heapG Σ} Δ s E Φ e v :
+  IntoVal e v →
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E [{ Φ }]).
+Proof. rewrite /envs_entails=> ? ->. by apply twp_value. Qed.
 
 Ltac wp_value_head :=
-  eapply tac_wp_value;
+  first [eapply tac_wp_value || eapply tac_twp_value];
     [apply _
     |iEval (lazy beta; simpl of_val)].
 
@@ -51,7 +68,17 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       |apply _                        (* IntoLaters *)
       |wp_expr_simpl_subst; try wp_value_head (* new goal *)
       ])
-   || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
+    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    let e := eval simpl in e in
+    reshape_expr e ltac:(fun K e' =>
+      unify e' efoc;
+      eapply (tac_twp_pure _ _ _ (fill K e'));
+      [apply _                        (* PureExec *)
+      |try fast_done                  (* The pure condition for PureExec *)
+      |wp_expr_simpl_subst; try wp_value_head (* new goal *)
+      ])
+    || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
   | _ => fail "wp_pure: not a 'wp'"
   end.
 
@@ -74,12 +101,22 @@ Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
   envs_entails Δ (WP e @ s; E {{ v, WP f (of_val v) @ s; E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> -> ->. by apply: wp_bind. Qed.
+Lemma tac_twp_bind `{heapG Σ} K Δ s E Φ e f :
+  f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
+  envs_entails Δ (WP e @ s; E [{ v, WP f (of_val v) @ s; E [{ Φ }] }])%I →
+  envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
+Proof. rewrite /envs_entails=> -> ->. by apply: twp_bind. Qed.
 
 Ltac wp_bind_core K :=
   lazymatch eval hnf in K with
   | [] => idtac
   | _ => eapply (tac_wp_bind K); [simpl; reflexivity|lazy beta]
   end.
+Ltac twp_bind_core K :=
+  lazymatch eval hnf in K with
+  | [] => idtac
+  | _ => eapply (tac_twp_bind K); [simpl; reflexivity|lazy beta]
+  end.
 
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
@@ -87,6 +124,9 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
     || fail "wp_bind: cannot find" efoc "in" e
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    reshape_expr e ltac:(fun K e' => unify e' efoc; twp_bind_core K)
+    || fail "wp_bind: cannot find" efoc "in" e
   | _ => fail "wp_bind: not a 'wp'"
   end.
 
@@ -111,6 +151,19 @@ Proof.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
 Qed.
+Lemma tac_twp_alloc Δ s E j K e v Φ :
+  IntoVal e v →
+  (∀ l, ∃ Δ',
+    envs_app false (Esnoc Enil j (l ↦ v)) Δ = Some Δ' ∧
+    envs_entails Δ' (WP fill K (Lit (LitLoc l)) @ s; E [{ Φ }])) →
+  envs_entails Δ (WP fill K (Alloc e) @ s; E [{ Φ }]).
+Proof.
+  rewrite /envs_entails=> ? HΔ.
+  rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
+  rewrite left_id. apply forall_intro=> l.
+  destruct (HΔ l) as (Δ'&?&HΔ'). rewrite envs_app_sound //; simpl.
+  by rewrite right_id HΔ'.
+Qed.
 
 Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
@@ -123,6 +176,16 @@ Proof.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
+Lemma tac_twp_load Δ s E i K l q v Φ :
+  envs_lookup i Δ = Some (false, l ↦{q} v)%I →
+  envs_entails Δ (WP fill K (of_val v) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E [{ Φ }]).
+Proof.
+  rewrite /envs_entails=> ??.
+  rewrite -twp_bind. eapply wand_apply; first exact: twp_load.
+  rewrite envs_lookup_split //; simpl.
+  by apply sep_mono_r, wand_mono.
+Qed.
 
 Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
   IntoVal e v' →
@@ -137,6 +200,17 @@ Proof.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
+Lemma tac_twp_store Δ Δ' s E i K l v e v' Φ :
+  IntoVal e v' →
+  envs_lookup i Δ = Some (false, l ↦ v)%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ = Some Δ' →
+  envs_entails Δ' (WP fill K (Lit LitUnit) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ s; E [{ Φ }]).
+Proof.
+  intros. rewrite -twp_bind. eapply wand_apply; first by eapply twp_store.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id. by apply sep_mono_r, wand_mono.
+Qed.
 
 Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
@@ -150,6 +224,15 @@ Proof.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
+Lemma tac_twp_cas_fail Δ s E i K l q v e1 v1 e2 Φ :
+  IntoVal e1 v1 → AsVal e2 →
+  envs_lookup i Δ = Some (false, l ↦{q} v)%I → v ≠ v1 →
+  envs_entails Δ (WP fill K (Lit (LitBool false)) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
+Proof.
+  intros. rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_fail.
+  rewrite envs_lookup_split //; simpl. by apply sep_mono_r, wand_mono.
+Qed.
 
 Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
   IntoVal e1 v1 → IntoVal e2 v2 →
@@ -164,6 +247,17 @@ Proof.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
+Lemma tac_twp_cas_suc Δ Δ' s E i K l v e1 v1 e2 v2 Φ :
+  IntoVal e1 v1 → IntoVal e2 v2 →
+  envs_lookup i Δ = Some (false, l ↦ v)%I → v = v1 →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ = Some Δ' →
+  envs_entails Δ' (WP fill K (Lit (LitBool true)) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E [{ Φ }]).
+Proof.
+  intros; subst. rewrite -twp_bind. eapply wand_apply; first exact: twp_cas_suc.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id. by apply sep_mono_r, wand_mono.
+Qed.
 
 Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
   IntoVal e2 (LitV (LitInt i2)) →
@@ -178,6 +272,18 @@ Proof.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
+Lemma tac_twp_faa Δ Δ' s E i K l i1 e2 i2 Φ :
+  IntoVal e2 (LitV (LitInt i2)) →
+  envs_lookup i Δ = Some (false, l ↦ LitV (LitInt i1))%I →
+  envs_simple_replace i false (Esnoc Enil i (l ↦ LitV (LitInt (i1 + i2)))) Δ = Some Δ' →
+  envs_entails Δ' (WP fill K (Lit (LitInt i1)) @ s; E [{ Φ }]) →
+  envs_entails Δ (WP fill K (FAA (Lit (LitLoc l)) e2) @ s; E [{ Φ }]).
+Proof.
+  rewrite /envs_entails=> ????; subst.
+  rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ i1 _ i2).
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id. by apply sep_mono_r, wand_mono.
+Qed.
 End heap.
 
 Tactic Notation "wp_apply" open_constr(lem) :=
@@ -189,10 +295,21 @@ Tactic Notation "wp_apply" open_constr(lem) :=
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end
+    | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+      reshape_expr e ltac:(fun K e' =>
+        twp_bind_core K; iApplyHyp H; wp_expr_simpl) ||
+      lazymatch iTypeOf H with
+      | Some (_,?P) => fail "wp_apply: cannot apply" P
+      end
     | _ => fail "wp_apply: not a 'wp'"
     end).
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
+  let finish _ :=
+    first [intros l | fail 1 "wp_alloc:" l "not fresh"];
+      eexists; split;
+        [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
+        |wp_expr_simpl; try wp_value_head] in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -201,10 +318,13 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
          eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..])
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
     [apply _
-    |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
-      eexists; split;
-        [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
-        |wp_expr_simpl; try wp_value_head]]
+    |finish ()]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_alloc _ _ _ H K); [apply _|..])
+      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
+    finish ()
   | _ => fail "wp_alloc: not a 'wp'"
   end.
 
@@ -212,6 +332,9 @@ Tactic Notation "wp_alloc" ident(l) :=
   let H := iFresh in wp_alloc l as H.
 
 Tactic Notation "wp_load" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_load: cannot find" l "↦ ?" in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -219,13 +342,23 @@ Tactic Notation "wp_load" :=
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
       |fail 1 "wp_load: cannot find 'Load' in" e];
     [apply _
-    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-     iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
+    |solve_mapsto ()
+    |wp_expr_simpl; try wp_value_head]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' => eapply (tac_twp_load _ _ _ _ K))
+      |fail 1 "wp_load: cannot find 'Load' in" e];
+    [solve_mapsto ()
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_load: not a 'wp'"
   end.
 
 Tactic Notation "wp_store" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_store: cannot find" l "↦ ?" in
+  let finish _ :=
+    wp_expr_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head] in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -234,14 +367,24 @@ Tactic Notation "wp_store" :=
          eapply (tac_wp_store _ _ _ _ _ _ K); [apply _|..])
       |fail 1 "wp_store: cannot find 'Store' in" e];
     [apply _
-    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-     iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
+    |solve_mapsto ()
+    |env_cbv; reflexivity
+    |finish ()]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_store _ _ _ _ _ K); [apply _|..])
+      |fail 1 "wp_store: cannot find 'Store' in" e];
+    [solve_mapsto ()
     |env_cbv; reflexivity
-    |wp_expr_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
+    |finish ()]
   | _ => fail "wp_store: not a 'wp'"
   end.
 
 Tactic Notation "wp_cas_fail" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?" in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -250,14 +393,24 @@ Tactic Notation "wp_cas_fail" :=
          eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..])
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [apply _
-    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-     iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
+    |solve_mapsto ()
+    |try congruence
+    |simpl; try wp_value_head]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_cas_fail _ _ _ _ K); [apply _|apply _|..])
+      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
+    [solve_mapsto ()
     |try congruence
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_fail: not a 'wp'"
   end.
 
 Tactic Notation "wp_cas_suc" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -266,8 +419,16 @@ Tactic Notation "wp_cas_suc" :=
          eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [apply _|apply _|..])
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [apply _
-    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-     iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
+    |solve_mapsto ()
+    |try congruence
+    |env_cbv; reflexivity
+    |simpl; try wp_value_head]
+  | |- envs_entails _ (twp ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
+      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
+    [solve_mapsto ()
     |try congruence
     |env_cbv; reflexivity
     |wp_expr_simpl; try wp_value_head]
@@ -275,6 +436,9 @@ Tactic Notation "wp_cas_suc" :=
   end.
 
 Tactic Notation "wp_faa" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
+    iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?" in
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
@@ -283,8 +447,15 @@ Tactic Notation "wp_faa" :=
          eapply (tac_wp_faa _ _ _ _ _ _ K); [apply _|..])
       |fail 1 "wp_faa: cannot find 'CAS' in" e];
     [apply _
-    |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
-     iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
+    |solve_mapsto ()
+    |env_cbv; reflexivity
+    |wp_expr_simpl; try wp_value_head]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    first
+      [reshape_expr e ltac:(fun K e' =>
+         eapply (tac_twp_faa _ _ _ _ _ K); [apply _|..])
+      |fail 1 "wp_faa: cannot find 'CAS' in" e];
+    [solve_mapsto ()
     |env_cbv; reflexivity
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_faa: not a 'wp'"
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
new file mode 100644
index 0000000000000000000000000000000000000000..55e7f5f5e41fbce3c9df3f0ed829461dc29c3d8c
--- /dev/null
+++ b/theories/heap_lang/total_adequacy.v
@@ -0,0 +1,15 @@
+From iris.program_logic Require Export total_adequacy.
+From iris.heap_lang Require Export adequacy.
+From iris.heap_lang Require Import proofmode notation.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+Definition heap_total Σ `{heapPreG Σ} s e σ φ :
+  (∀ `{heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]%I) →
+  sn step ([e], σ).
+Proof.
+  intros Hwp; eapply (twp_total _ _); iIntros (?) "".
+  iMod (gen_heap_init σ) as (?) "Hh".
+  iModIntro. iExists gen_heap_ctx; iFrame.
+  iApply (Hwp (HeapG _ _ _)).
+Qed.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
new file mode 100644
index 0000000000000000000000000000000000000000..648d934571fd8d628932554a45737a2c2c2040ec
--- /dev/null
+++ b/theories/program_logic/total_adequacy.v
@@ -0,0 +1,129 @@
+From iris.program_logic Require Export total_weakestpre adequacy.
+From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.base_logic Require Import big_op soundness fixpoint.
+From iris.base_logic.lib Require Import wsat.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+Import uPred.
+
+Section adequacy.
+Context `{irisG Λ Σ}.
+Implicit Types e : expr Λ.
+
+Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
+    (t1 : list (expr Λ)) : iProp Σ :=
+  (∀ t2 σ1 σ2, ⌜step (t1,σ1) (t2,σ2)⌝ -∗
+    state_interp σ1 ={⊤}=∗ state_interp σ2 ∗ twptp t2)%I.
+
+Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
+  ((□ ∀ t, twptp1 t -∗ twptp2 t) →
+  ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t)%I.
+Proof.
+  iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
+  iIntros (t2 σ1 σ2) "Hstep Hσ". iMod ("Hwp" with "[$] [$]") as "[$ ?]".
+  by iApply "H".
+Qed.
+
+Local Instance twptp_pre_mono' : BIMonoPred twptp_pre.
+Proof.
+  constructor; first apply twptp_pre_mono.
+  intros wp Hwp n t1 t2 ?%(discrete_iff _ _)%leibniz_equiv; solve_proper.
+Qed.
+
+Definition twptp (t : list (expr Λ)) : iProp Σ :=
+  uPred_least_fixpoint twptp_pre t.
+
+Lemma twptp_unfold t : twptp t ⊣⊢ twptp_pre twptp t.
+Proof. by rewrite /twptp least_fixpoint_unfold. Qed.
+
+Lemma twptp_ind Ψ :
+  ((□ ∀ t, twptp_pre (λ t, Ψ t ∧ twptp t) t -∗ Ψ t) → ∀ t, twptp t -∗ Ψ t)%I.
+Proof.
+  iIntros "#IH" (t) "H".
+  assert (NonExpansive Ψ).
+  { by intros n ?? ->%(discrete_iff _ _)%leibniz_equiv. }
+  iApply (least_fixpoint_strong_ind _ Ψ with "[] H").
+  iIntros "!#" (t') "H". by iApply "IH".
+Qed.
+
+Instance twptp_Permutation : Proper ((≡ₚ) ==> (⊢)) twptp.
+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.
+  iMod ("IH" $! t2' with "[% //] Hσ") as "[$ [IH _]]". by iApply "IH".
+Qed.
+
+Lemma twptp_app t1 t2 : twptp t1 -∗ twptp t2 -∗ twptp (t1 ++ t2).
+Proof.
+  iIntros "H1". iRevert (t2). iRevert (t1) "H1".
+  iApply twptp_ind; iIntros "!#" (t1) "IH1". iIntros (t2) "H2".
+  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/=.
+  apply app_eq_inv in H as [(t&?&?)|(t&?&?)]; subst.
+  - destruct t as [|e1' ?]; simplify_eq/=.
+    + iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]".
+      { 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.
+      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.
+    iModIntro. rewrite -assoc. by iApply "IH2".
+Qed.
+
+Lemma twp_twptp s Φ e : WP e @ s; ⊤ [{ Φ }] -∗ twptp [e].
+Proof.
+  iIntros "He". remember (⊤ : coPset) as E eqn:HE.
+  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];
+    simplify_eq/=; try discriminate_list.
+  destruct (to_val e1) as [v|] eqn:He1.
+  { apply val_stuck in Hstep; naive_solver. }
+  iMod ("IH" with "Hσ1") as "[_ IH]".
+  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).
+    destruct Hstep; simplify_eq/=; discriminate_list. }
+  iDestruct "IHfork" as "[[IH' _] IHfork]".
+  iApply (twptp_app [_] with "[IH']"); [by iApply "IH'"|by iApply "IH"].
+Qed.
+
+Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ)%I.
+
+Lemma twptp_total σ t : world σ -∗ twptp t -∗ ▷ ⌜sn step (t, σ)⌝.
+Proof.
+  iIntros "Hw Ht". iRevert (σ) "Hw". iRevert (t) "Ht".
+  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ) "(Hw&HE&Hσ)".
+  iApply (pure_mono _ _ (Acc_intro _)). iIntros ([t' σ'] Hstep).
+  rewrite /twptp_pre fupd_eq /fupd_def.
+  iMod ("IH" with "[% //] Hσ [$Hw $HE]") as ">(Hw & HE & Hσ & [IH _])".
+  iApply "IH". by iFrame.
+Qed.
+End adequacy.
+
+Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
+  (∀ `{Hinv : invG Σ},
+     (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
+       stateI σ ∗ WP e @ s; ⊤ [{ Φ }])%I) →
+  sn step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
+Proof.
+  intros Hwp.
+  eapply (soundness (M:=iResUR Σ) _ 1); iIntros "/=".
+  iMod wsat_alloc as (Hinv) "[Hw HE]".
+  rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+  iDestruct "Hwp" as (Istate) "[HI Hwp]".
+  iApply (@twptp_total _ _ (IrisG _ _ Hinv Istate) with "[$Hw $HE $HI]").
+  by iApply (@twp_twptp _ _ (IrisG _ _ Hinv Istate)).
+Qed.
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
new file mode 100644
index 0000000000000000000000000000000000000000..a78740646b2970d56b138c81114236f3251a4c26
--- /dev/null
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -0,0 +1,85 @@
+(** Some derived lemmas for ectx-based languages *)
+From iris.program_logic Require Export ectx_language.
+From iris.program_logic Require Export total_weakestpre total_lifting.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+Section wp.
+Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
+Implicit Types P : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+Hint Resolve head_prim_reducible head_reducible_prim_step.
+
+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}=∗
+      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) "%".
+  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⌝ →
+    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.
+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}=∗
+      state_interp σ2 ∗
+      default 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.
+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}=∗
+      ⌜efs = []⌝ ∗ state_interp σ2 ∗ default 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.
+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') →
+  (|={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.
+
+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') →
+  WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
+Proof using Hinh.
+  intros. rewrite -(twp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
+Qed.
+End wp.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
new file mode 100644
index 0000000000000000000000000000000000000000..fe690efd28a84f22cad9044be7714b72467debb2
--- /dev/null
+++ b/theories/program_logic/total_lifting.v
@@ -0,0 +1,79 @@
+From iris.program_logic Require Export total_weakestpre.
+From iris.base_logic Require Export big_op.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+Section lifting.
+Context `{irisG Λ Σ}.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+Implicit Types σ : state Λ.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+
+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}=∗
+      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.
+
+(** 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⌝ →
+    WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros (Hsafe Hstep) "H". iApply twp_lift_step.
+  { 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.
+  iMod "Hclose" as "_". iFrame "Hσ". iApply "H"; auto.
+Qed.
+
+(* Atomic steps don't need any mask-changing business here, one can
+   use the generic lemmas here. *)
+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}=∗
+      state_interp σ2 ∗
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+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.
+  destruct (to_val e2) eqn:?; last by iExFalso.
+  by iApply twp_value.
+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')→
+  (|={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).
+Qed.
+
+Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ Φ :
+  PureExec φ e1 e2 →
+  φ →
+  WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros ([??] Hφ) "HWP".
+  iApply (twp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|auto].
+Qed.
+End lifting.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
new file mode 100644
index 0000000000000000000000000000000000000000..9548bba4b6c0d98447dbdf2a99611eb07cd36b8c
--- /dev/null
+++ b/theories/program_logic/total_weakestpre.v
@@ -0,0 +1,401 @@
+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import fixpoint big_op.
+Set Default Proof Using "Type".
+Import uPred.
+
+Definition twp_pre `{irisG Λ Σ} (s : stuckness)
+      (wp : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
+    coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := λ E e1 Φ,
+  match to_val e1 with
+  | 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}=∗
+       state_interp σ2 ∗ wp E e2 Φ ∗
+       [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
+  end%I.
+
+Lemma twp_pre_mono `{irisG Λ Σ} s
+    (wp1 wp2 : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
+  ((□ ∀ E e Φ, wp1 E e Φ -∗ wp2 E e Φ) →
+  ∀ E e Φ, twp_pre s wp1 E e Φ -∗ twp_pre s wp2 E e Φ)%I.
+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".
+  iMod ("Hwp" with "Hstep") as "($ & Hwp & Hfork)"; iModIntro; iSplitL "Hwp".
+  - by iApply "H".
+  - iApply (@big_sepL_impl with "[$Hfork]"); iIntros "!#" (k e _) "Hwp".
+    by iApply "H".
+Qed.
+
+(* Uncurry [twp_pre] and equip its type with an OFE structure *)
+Definition twp_pre' `{irisG Λ Σ} (s : stuckness) :
+  (prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ) →
+  prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ :=
+    curry3 ∘ twp_pre s ∘ uncurry3.
+
+Local Instance twp_pre_mono' `{irisG Λ Σ} s : BIMonoPred (twp_pre' s).
+Proof.
+  constructor.
+  - iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
+    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.
+Qed.
+
+Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
+    (e : expr Λ) (Φ : val Λ → iProp Σ) :
+  iProp Σ := uPred_least_fixpoint (twp_pre' s) (E,e,Φ).
+Definition twp_aux : seal (@twp_def). by eexists. Qed.
+Definition twp := unseal twp_aux.
+Definition twp_eq : @twp = @twp_def := seal_eq twp_aux.
+
+Arguments twp {_ _ _} _ _ _%E _.
+Instance: Params (@twp) 6.
+
+(* Note that using '[[' instead of '[{' results in conflicts with the list
+notations. *)
+Notation "'WP' e @ s ; E [{ Φ } ]" := (twp s E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  s ;  E  [{  Φ  } ] ']'") : uPred_scope.
+Notation "'WP' e @ E [{ Φ } ]" := (twp NotStuck E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  E  [{  Φ  } ] ']'") : uPred_scope.
+Notation "'WP' e @ E ? [{ Φ } ]" := (twp MaybeStuck E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  E  ? [{  Φ  } ] ']'") : uPred_scope.
+Notation "'WP' e [{ Φ } ]" := (twp NotStuck ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' [{  Φ  } ] ']'") : uPred_scope.
+Notation "'WP' e ? [{ Φ } ]" := (twp MaybeStuck ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' ? [{  Φ  } ] ']'") : uPred_scope.
+
+Notation "'WP' e @ s ; E [{ v , Q } ]" := (twp s E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' @  s ;  E  [{  v ,  Q  } ] ']'") : uPred_scope.
+Notation "'WP' e @ E [{ v , Q } ]" := (twp NotStuck E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' @  E  [{  v ,  Q  } ] ']'") : uPred_scope.
+Notation "'WP' e @ E ? [{ v , Q } ]" := (twp MaybeStuck E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' @  E  ? [{  v ,  Q  } ] ']'") : uPred_scope.
+Notation "'WP' e [{ v , Q } ]" := (twp NotStuck ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' [{  v ,  Q  } ] ']'") : uPred_scope.
+Notation "'WP' e ? [{ v , Q } ]" := (twp MaybeStuck ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' ? [{  v ,  Q  } ] ']'") : uPred_scope.
+
+(* Texan triples *)
+Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  s ;  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  E  ? [[{  x .. y ,  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  [[{  x .. y ,   RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  ? [[{  x .. y ,   RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])%I
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  s ;  E  [[{  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])%I
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  E  [[{  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])%I
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  E  ? [[{  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])%I
+    (at level 20,
+     format "[[{  P  } ] ]  e  [[{  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])%I
+    (at level 20,
+     format "[[{  P  } ] ]  e  ? [[{  RET  pat ;  Q } ] ]") : uPred_scope.
+
+Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  s ;  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  E  ? [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  ? [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  s ;  E  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  E  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  E  ? [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])
+    (at level 20,
+     format "[[{  P  } ] ]  e  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])
+    (at level 20,
+     format "[[{  P  } ] ]  e  ? [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+
+Section twp.
+Context `{irisG Λ Σ}.
+Implicit Types P : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+
+(* Weakest pre *)
+Lemma twp_unfold s E e Φ : WP e @ s; E [{ Φ }] ⊣⊢ twp_pre s (twp s) E e Φ.
+Proof. by rewrite twp_eq /twp_def least_fixpoint_unfold. Qed.
+Lemma twp_ind s Ψ :
+  (∀ n E e, Proper (pointwise_relation _ (dist n) ==> dist n) (Ψ E e)) →
+  (□ (∀ e E Φ, twp_pre s (λ E e Φ, Ψ E e Φ ∧ WP e @ s; E [{ Φ }]) E e Φ -∗ Ψ E e Φ) →
+  ∀ e E Φ, WP e @ s; E [{ Φ }] -∗ Ψ E e Φ)%I.
+Proof.
+  iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_eq.
+  set (Ψ' := curry3 Ψ :
+    prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ).
+  assert (NonExpansive Ψ').
+  { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
+      [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
+  iApply (least_fixpoint_strong_ind _ Ψ' with "[] H").
+  iIntros "!#" ([[??] ?]) "H". by iApply "IH".
+Qed.
+
+Global Instance twp_ne s E e n :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@twp Λ Σ _ s E e).
+Proof.
+  intros Φ1 Φ2 HΦ. rewrite !twp_eq. by apply (least_fixpoint_ne _), pair_ne, HΦ.
+Qed.
+Global Instance twp_proper s E e :
+  Proper (pointwise_relation _ (≡) ==> (≡)) (@twp Λ Σ _ s E e).
+Proof.
+  by intros Φ Φ' ?; apply equiv_dist=>n; apply twp_ne=>v; apply equiv_dist.
+Qed.
+
+Lemma twp_value' s E Φ v : Φ v -∗ WP of_val v @ s; E [{ Φ }].
+Proof. iIntros "HΦ". rewrite twp_unfold /twp_pre to_of_val. auto. Qed.
+Lemma twp_value_inv s E Φ v : WP of_val v @ s; E [{ Φ }] ={E}=∗ Φ v.
+Proof. by rewrite twp_unfold /twp_pre to_of_val. Qed.
+
+Lemma twp_strong_mono s1 s2 E1 E2 e Φ Ψ :
+  s1 ⊑ s2 → E1 ⊆ E2 →
+  WP e @ s1; E1 [{ Φ }] -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s2; E2 [{ Ψ }].
+Proof.
+  iIntros (? HE) "H HΦ". iRevert (E2 Ψ HE) "HΦ"; iRevert (e E1 Φ) "H".
+  iApply twp_ind; first solve_proper.
+  iIntros "!#" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
+  rewrite !twp_unfold /twp_pre. destruct (to_val e) as [v|] eqn:?.
+  { 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).
+  iMod ("IH" with "[//]") as "($ & IH & IHefs)"; auto.
+  iMod "Hclose" as "_"; iModIntro. iSplitR "IHefs".
+  - iDestruct "IH" as "[IH _]". iApply ("IH" with "[//] HΦ").
+  - iApply (big_sepL_impl with "[$IHefs]"); iIntros "!#" (k ef _) "[IH _]".
+    by iApply "IH".
+Qed.
+
+Lemma fupd_twp s E e Φ : (|={E}=> WP e @ s; E [{ Φ }]) -∗ WP e @ s; E [{ Φ }].
+Proof.
+  rewrite twp_unfold /twp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
+  { by iMod "H". }
+  iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
+Qed.
+Lemma twp_fupd s E e Φ : WP e @ s; E [{ v, |={E}=> Φ v }] -∗ WP e @ s; E [{ Φ }].
+Proof. iIntros "H". iApply (twp_strong_mono with "H"); auto. Qed.
+
+Lemma twp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
+  (|={E1,E2}=> WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }]) -∗ WP e @ s; E1 [{ Φ }].
+Proof.
+  iIntros "H". rewrite !twp_unfold /twp_pre /=.
+  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).
+  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 (twp_value_inv with "H") as ">H". iFrame "Hphy". by iApply twp_value'.
+Qed.
+
+Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
+  WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }] -∗ WP K e @ s; E [{ Φ }].
+Proof.
+  revert Φ. cut (∀ Φ', WP e @ s; E [{ Φ' }] -∗ ∀ Φ,
+    (∀ v, Φ' v -∗ WP K (of_val v) @ s; E [{ Φ }]) -∗ WP K e @ s; E [{ Φ }]).
+  { iIntros (help Φ) "H". iApply (help with "H"); auto. }
+  iIntros (Φ') "H". iRevert (e E Φ') "H". iApply twp_ind; first solve_proper.
+  iIntros "!#" (e E1 Φ') "IH". iIntros (Φ) "HΦ".
+  rewrite /twp_pre. destruct (to_val e) as [v|] eqn:He.
+  { apply of_to_val in He as <-. iApply fupd_twp. by iApply "HΦ". }
+  rewrite twp_unfold /twp_pre fill_not_val //.
+  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)".
+  iModIntro; iSplitR "IHfork".
+  - iDestruct "IH" as "[IH _]". by iApply "IH".
+  - by setoid_rewrite and_elim_r.
+Qed.
+
+Lemma twp_bind_inv K `{!LanguageCtx K} s E e Φ :
+  WP K e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }].
+Proof.
+  iIntros "H". remember (K e) as e' eqn:He'.
+  iRevert (e He'). iRevert (e' E Φ) "H". iApply twp_ind; first solve_proper.
+  iIntros "!#" (e' E1 Φ) "IH". iIntros (e ->).
+  rewrite !twp_unfold {2}/twp_pre. destruct (to_val e) as [v|] eqn:He.
+  { iModIntro. apply of_to_val in He as <-. rewrite !twp_unfold.
+    iApply (twp_pre_mono with "[] IH"). by iIntros "!#" (E e Φ') "[_ ?]". }
+  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.
+  iModIntro; iSplitR "IHfork".
+  - iDestruct "IH" as "[IH _]". by iApply "IH".
+  - by setoid_rewrite and_elim_r.
+Qed.
+
+Lemma twp_wp s E e Φ : WP e @ s; E [{ Φ }] -∗ WP e @ s; E {{ Φ }}.
+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]". iModIntro; iNext.
+  iIntros (e2 σ2 efs) "Hstep".
+  iMod ("H" with "Hstep") as "($ & H & Hfork)"; iModIntro.
+  iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]").
+  iIntros "!#" (k e' _) "H". by iApply "IH".
+Qed.
+
+(** * Derived rules *)
+Lemma twp_mono s E e Φ Ψ :
+  (∀ v, Φ v -∗ Ψ v) → WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ Ψ }].
+Proof.
+  iIntros (HΦ) "H"; iApply (twp_strong_mono with "H"); auto.
+  iIntros (v) "?". by iApply HΦ.
+Qed.
+Lemma twp_stuck_mono s1 s2 E e Φ :
+  s1 ⊑ s2 → WP e @ s1; E [{ Φ }] ⊢ WP e @ s2; E [{ Φ }].
+Proof. iIntros (?) "H". iApply (twp_strong_mono with "H"); auto. Qed.
+Lemma twp_stuck_weaken s E e Φ :
+  WP e @ s; E [{ Φ }] ⊢ WP e @ E ?[{ Φ }].
+Proof. apply twp_stuck_mono. by destruct s. Qed.
+Lemma twp_mask_mono s E1 E2 e Φ :
+  E1 ⊆ E2 → WP e @ s; E1 [{ Φ }] -∗ WP e @ s; E2 [{ Φ }].
+Proof. iIntros (?) "H"; iApply (twp_strong_mono with "H"); auto. Qed.
+Global Instance twp_mono' s E e :
+  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@twp Λ Σ _ s E e).
+Proof. by intros Φ Φ' ?; apply twp_mono. Qed.
+
+Lemma twp_value s E Φ e v `{!IntoVal e v} : Φ v -∗ WP e @ s; E [{ Φ }].
+Proof. intros; rewrite -(of_to_val e v) //; by apply twp_value'. Qed.
+Lemma twp_value_fupd' s E Φ v : (|={E}=> Φ v) -∗ WP of_val v @ s; E [{ Φ }].
+Proof. intros. by rewrite -twp_fupd -twp_value'. Qed.
+Lemma twp_value_fupd s E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) -∗ WP e @ s; E [{ Φ }].
+Proof. intros. rewrite -twp_fupd -twp_value //. Qed.
+
+Lemma twp_frame_l s E e Φ R : R ∗ WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, R ∗ Φ v }].
+Proof. iIntros "[? H]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.
+Lemma twp_frame_r s E e Φ R : WP e @ s; E [{ Φ }] ∗ R -∗ WP e @ s; E [{ v, Φ v ∗ R }].
+Proof. iIntros "[H ?]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.
+
+Lemma twp_wand s E e Φ Ψ :
+  WP e @ s; E [{ Φ }] -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E [{ Ψ }].
+Proof.
+  iIntros "H HΦ". iApply (twp_strong_mono with "H"); auto.
+  iIntros (?) "?". by iApply "HΦ".
+Qed.
+Lemma twp_wand_l s E e Φ Ψ :
+  (∀ v, Φ v -∗ Ψ v) ∗ WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ Ψ }].
+Proof. iIntros "[H Hwp]". iApply (twp_wand with "Hwp H"). Qed.
+Lemma twp_wand_r s E e Φ Ψ :
+  WP e @ s; E [{ Φ }] ∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E [{ Ψ }].
+Proof. iIntros "[Hwp H]". iApply (twp_wand with "Hwp H"). Qed.
+End twp.
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+  Context `{irisG Λ Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types Φ : val Λ → iProp Σ.
+
+  Global Instance frame_twp p s E e R Φ Ψ :
+    (∀ v, Frame p R (Φ v) (Ψ v)) → Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
+  Proof. rewrite /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
+
+  Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).
+  Proof. by rewrite /IsExcept0 -{2}fupd_twp -except_0_fupd -fupd_intro. Qed.
+
+  Global Instance elim_modal_bupd_twp s E e P Φ :
+    ElimModal (|==> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+  Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_twp. Qed.
+
+  Global Instance elim_modal_fupd_twp s E e P Φ :
+    ElimModal (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_twp. Qed.
+
+  Global Instance elim_modal_fupd_twp_atomic s E1 E2 e P Φ :
+    Atomic (stuckness_to_atomicity s) e →
+    ElimModal (|={E1,E2}=> P) P
+            (WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I.
+  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r twp_atomic. Qed.
+
+  Global Instance add_modal_fupd_twp s E e P Φ :
+    AddModal (|={E}=> P) P (WP e @ s; E [{ Φ }]).
+  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_twp. Qed.
+End proofmode_classes.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 049ac577d77fae5093136b96081b0bc24a1bf254..15473de95e7ff3462ae739e17ca8a38909bf789e 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -13,16 +13,14 @@ Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
 Inductive stuckness := NotStuck | MaybeStuck.
 
-Definition stuckness_le (s1 s2 : stuckness) : bool :=
+Definition stuckness_leb (s1 s2 : stuckness) : bool :=
   match s1, s2 with
   | MaybeStuck, NotStuck => false
   | _, _ => true
   end.
-Instance: PreOrder stuckness_le.
-Proof.
-  split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
-Qed.
-Instance: SqSubsetEq stuckness := stuckness_le.
+Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
+Instance stuckness_le_po : PreOrder stuckness_le.
+Proof. split; by repeat intros []. Qed.
 
 Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
   if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
@@ -45,7 +43,7 @@ Proof.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
-Definition wp_def `{irisG Λ Σ} s :
+Definition wp_def `{irisG Λ Σ} (s : stuckness) :
   coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
 Definition wp_aux : seal (@wp_def). by eexists. Qed.
 Definition wp := unseal wp_aux.
@@ -213,31 +211,22 @@ Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
 Lemma wp_value_inv s E Φ v : WP of_val v @ s; E {{ Φ }} ={E}=∗ Φ v.
 Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
 
-Lemma wp_strong_mono s E1 E2 e Φ Ψ :
-  E1 ⊆ E2 → (∀ v, Φ v ={E2}=∗ Ψ v) ∗ WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Ψ }}.
+Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
+  s1 ⊑ s2 → E1 ⊆ E2 →
+  WP e @ s1; E1 {{ Φ }} -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s2; E2 {{ Ψ }}.
 Proof.
-  iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
+  iIntros (? HE) "H HΦ". iLöb as "IH" forall (e E1 E2 HE Φ Ψ).
+  rewrite !wp_unfold /wp_pre.
   destruct (to_val e) as [v|] eqn:?.
   { 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. iNext. iIntros (e2 σ2 efs Hstep).
-  iMod ("H" with "[//]") as "($ & H & $)"; auto.
-  iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
-Qed.
-
-Lemma wp_stuck_weaken s E e Φ :
-  WP e @ s; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
-Proof.
-  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
-  destruct (to_val e) as [v|]; first iExact "H".
-  iIntros (σ1) "Hσ". iMod ("H" with "Hσ") as "[#Hred H]". iModIntro.
-  iSplit; first done. iNext. iIntros (e2 σ2 efs) "#Hstep".
-  iMod ("H" with "Hstep") as "($ & He2 & Hefs)". iModIntro.
-  iSplitL "He2"; first by iApply ("IH" with "He2"). iClear "Hred Hstep".
-  induction efs as [|ef efs IH]; first by iApply big_sepL_nil.
-  rewrite !big_sepL_cons. iDestruct "Hefs" as "(Hef & Hefs)".
-  iSplitL "Hef". by iApply ("IH" with "Hef"). exact: IH.
+  iMod ("H" with "[$]") as "[% H]".
+  iModIntro. iSplit; [by destruct s1, s2|]. iNext. iIntros (e2 σ2 efs Hstep).
+  iMod ("H" with "[//]") as "($ & H & Hefs)".
+  iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
+  - iApply ("IH" with "[//] H HΦ").
+  - iApply (big_sepL_impl with "[$Hefs]"); iIntros "!#" (k ef _) "H".
+    by iApply ("IH" with "[] H").
 Qed.
 
 Lemma fupd_wp s E e Φ : (|={E}=> WP e @ s; E {{ Φ }}) ⊢ WP e @ s; E {{ Φ }}.
@@ -247,7 +236,7 @@ Proof.
   iIntros (σ1) "Hσ1". iMod "H". by iApply "H".
 Qed.
 Lemma wp_fupd s E e Φ : WP e @ s; E {{ v, |={E}=> Φ v }} ⊢ WP e @ s; E {{ Φ }}.
-Proof. iIntros "H". iApply (wp_strong_mono s E); try iFrame; auto. Qed.
+Proof. iIntros "H". iApply (wp_strong_mono s s E with "H"); auto. Qed.
 
 Lemma wp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
   (|={E1,E2}=> WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ s; E1 {{ Φ }}.
@@ -256,15 +245,14 @@ 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. iNext. iIntros (e2 σ2 efs Hstep). destruct s.
-  - iMod ("H" with "[//]") as "(Hphy & H & $)".
-    rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
+  iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
+  iMod ("H" with "[//]") 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 & $)"; first done.
-    iMod (wp_value_inv with "H") as ">H". by iApply wp_value'.
+    iMod (wp_value_inv with "H") as ">H". iFrame "Hphy". by iApply wp_value'.
 Qed.
 
 Lemma wp_step_fupd s E1 E2 e P Φ :
@@ -275,8 +263,8 @@ Proof.
   iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
   iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
   iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
-  iMod "HR". iModIntro. iApply (wp_strong_mono s E2); first done.
-  iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
+  iMod "HR". iModIntro. iApply (wp_strong_mono s s E2 with "H"); [done..|].
+  iIntros (v) "H". by iApply "H".
 Qed.
 
 Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
@@ -312,14 +300,17 @@ Qed.
 (** * Derived rules *)
 Lemma wp_mono s E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ Ψ }}.
 Proof.
-  iIntros (HΦ) "H"; iApply (wp_strong_mono s E E); auto.
-  iIntros "{$H}" (v) "?". by iApply HΦ.
+  iIntros (HΦ) "H"; iApply (wp_strong_mono with "H"); auto.
+  iIntros (v) "?". by iApply HΦ.
 Qed.
 Lemma wp_stuck_mono s1 s2 E e Φ :
   s1 ⊑ s2 → WP e @ s1; E {{ Φ }} ⊢ WP e @ s2; E {{ Φ }}.
-Proof. case: s1; case: s2 => // _. exact: wp_stuck_weaken. Qed.
+Proof. iIntros (?) "H". iApply (wp_strong_mono with "H"); auto. Qed.
+Lemma wp_stuck_weaken s E e Φ :
+  WP e @ s; E {{ Φ }} ⊢ WP e @ E ?{{ Φ }}.
+Proof. apply wp_stuck_mono. by destruct s. Qed.
 Lemma wp_mask_mono s E1 E2 e Φ : E1 ⊆ E2 → WP e @ s; E1 {{ Φ }} ⊢ WP e @ s; E2 {{ Φ }}.
-Proof. iIntros (?) "H"; iApply (wp_strong_mono s E1 E2); auto. iFrame; eauto. Qed.
+Proof. iIntros (?) "H"; iApply (wp_strong_mono with "H"); auto. Qed.
 Global Instance wp_mono' s E e :
   Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ s E e).
 Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
@@ -333,9 +324,9 @@ Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
 Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
 
 Lemma wp_frame_l s E e Φ R : R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}.
-Proof. iIntros "[??]". iApply (wp_strong_mono s E E _ Φ); try iFrame; eauto. Qed.
+Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
 Lemma wp_frame_r s E e Φ R : WP e @ s; E {{ Φ }} ∗ R ⊢ WP e @ s; E {{ v, Φ v ∗ R }}.
-Proof. iIntros "[??]". iApply (wp_strong_mono s E E _ Φ); try iFrame; eauto. Qed.
+Proof. iIntros "[H ?]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
 
 Lemma wp_frame_step_l s E1 E2 e Φ R :
   to_val e = None → E2 ⊆ E1 →
@@ -361,8 +352,8 @@ Proof. iIntros (?) "[??]". iApply (wp_frame_step_r s E E); try iFrame; eauto. Qe
 Lemma wp_wand s E e Φ Ψ :
   WP e @ s; E {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E {{ Ψ }}.
 Proof.
-  iIntros "Hwp H". iApply (wp_strong_mono s E); auto.
-  iIntros "{$Hwp}" (?) "?". by iApply "H".
+  iIntros "Hwp H". iApply (wp_strong_mono with "Hwp"); auto.
+  iIntros (?) "?". by iApply "H".
 Qed.
 Lemma wp_wand_l s E e Φ Ψ :
   (∀ v, Φ v -∗ Ψ v) ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ Ψ }}.
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 48414dd253f6f0c7188c6a22d01d5c1948fc9311..87ed6c41f1e3ff5acbe6467b6acfb0cc69ea0eed 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -1,5 +1,5 @@
 (** This file is essentially a bunch of testcases. *)
-From iris.program_logic Require Export weakestpre hoare.
+From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import adequacy.
 From iris.heap_lang Require Import proofmode notation.
@@ -34,7 +34,7 @@ Section LiftingTests.
     let: "y" := ref #1 in
     "x" <- !"x" + #1 ;; !"x".
 
-  Lemma heap_e2_spec E : WP heap_e2 @ E {{ v, ⌜v = #2⌝ }}%I.
+  Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, ⌜v = #2⌝ }]%I.
   Proof.
     iIntros "". rewrite /heap_e2.
     wp_alloc l. wp_let. wp_alloc l'. wp_let.
@@ -46,7 +46,7 @@ Section LiftingTests.
     let: "f" := λ: "z", "z" + #1 in
     if: "x" then "f" #0 else "f" #1.
 
-  Lemma heap_e3_spec E : WP heap_e3 @ E {{ v, ⌜v = #1⌝ }}%I.
+  Lemma heap_e3_spec E : WP heap_e3 @ E [{ v, ⌜v = #1⌝ }]%I.
   Proof.
     iIntros "". rewrite /heap_e3.
     by repeat (wp_pure _).
@@ -56,7 +56,7 @@ Section LiftingTests.
     let: "x" := (let: "y" := ref (ref #1) in ref "y") in
     ! ! !"x".
 
-  Lemma heap_e4_spec : WP heap_e4 {{ v, ⌜ v = #1 ⌝ }}%I.
+  Lemma heap_e4_spec : WP heap_e4 [{ v, ⌜ v = #1 ⌝ }]%I.
   Proof.
     rewrite /heap_e4. wp_alloc l. wp_alloc l'. wp_let.
     wp_alloc l''. wp_let. by repeat wp_load.
@@ -65,7 +65,7 @@ Section LiftingTests.
   Definition heap_e5 : expr :=
     let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x".
 
-  Lemma heap_e5_spec E : WP heap_e5 @ E {{ v, ⌜v = #13⌝ }}%I.
+  Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, ⌜v = #13⌝ }]%I.
   Proof.
     rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
     wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
@@ -81,16 +81,17 @@ Section LiftingTests.
 
   Lemma FindPred_spec n1 n2 E Φ :
     n1 < n2 →
-    Φ #(n2 - 1) -∗ WP FindPred #n2 #n1 @ E {{ Φ }}.
+    Φ #(n2 - 1) -∗ WP FindPred #n2 #n1 @ E [{ Φ }].
   Proof.
-    iIntros (Hn) "HΦ". iLöb as "IH" forall (n1 Hn).
+    iIntros (Hn) "HΦ".
+    iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
     wp_rec. wp_let. wp_op. wp_let.
     wp_op; case_bool_decide; wp_if.
-    - iApply ("IH" with "[%] HΦ"). omega.
-    - by assert (n1 = n2 - 1) as -> by omega.
+    - iApply ("IH" with "[%] [%] HΦ"); omega.
+    - by assert (n1' = n2 - 1) as -> by omega.
   Qed.
 
-  Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) -∗ WP Pred #n @ E {{ Φ }}.
+  Lemma Pred_spec n E Φ : Φ #(n - 1) -∗ WP Pred #n @ E [{ Φ }].
   Proof.
     iIntros "HΦ". wp_lam.
     wp_op. case_bool_decide; wp_if.
@@ -101,7 +102,7 @@ Section LiftingTests.
   Qed.
 
   Lemma Pred_user E :
-    (WP let: "x" := Pred #42 in Pred "x" @ E {{ v, ⌜v = #40⌝ }})%I.
+    WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌝ }]%I.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
diff --git a/theories/tests/list_reverse.v b/theories/tests/list_reverse.v
index 3db301080833099ce44d0e45b3949c0072e139a4..d5388c0e156e86b880197c0b57ad24addb2f9c75 100644
--- a/theories/tests/list_reverse.v
+++ b/theories/tests/list_reverse.v
@@ -1,5 +1,5 @@
 (** Correctness of in-place list reversal *)
-From iris.program_logic Require Export weakestpre hoare.
+From iris.program_logic Require Export total_weakestpre weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
@@ -27,26 +27,26 @@ Definition rev : val :=
     end.
 
 Lemma rev_acc_wp hd acc xs ys :
-  {{{ is_list hd xs ∗ is_list acc ys }}}
+  [[{ is_list hd xs ∗ is_list acc ys }]]
     rev hd acc
-  {{{ w, RET w; is_list w (reverse xs ++ ys) }}}.
+  [[{ w, RET w; is_list w (reverse xs ++ ys) }]].
 Proof.
   iIntros (Φ) "[Hxs Hys] HΦ".
-  iLöb as "IH" forall (hd acc xs ys Φ). wp_rec. wp_let.
-  destruct xs as [|x xs]; iSimplifyEq.
+  iInduction xs as [|x xs] "IH" forall (hd acc ys Φ);
+    iSimplifyEq; wp_rec; wp_let.
   - wp_match. by iApply "HΦ".
   - iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
     wp_match. wp_load. wp_proj. wp_let. wp_load. wp_proj. wp_let. wp_store.
-    iApply ("IH" $! hd' (SOMEV #l) xs (x :: ys) with "Hxs [Hx Hys]"); simpl.
+    iApply ("IH" $! hd' (SOMEV #l) (x :: ys) with "Hxs [Hx Hys]"); simpl.
     { iExists l, acc; by iFrame. }
-    iNext. iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
+    iIntros (w). rewrite cons_middle assoc -reverse_cons. iApply "HΦ".
 Qed.
 
 Lemma rev_wp hd xs :
-  {{{ is_list hd xs }}} rev hd (InjL #()) {{{ w, RET w; is_list w (reverse xs) }}}.
+  [[{ is_list hd xs }]] rev hd NONE [[{ w, RET w; is_list w (reverse xs) }]].
 Proof.
   iIntros (Φ) "Hxs HΦ".
   iApply (rev_acc_wp hd NONEV xs [] with "[$Hxs //]").
-  iNext; iIntros (w). rewrite right_id_L. iApply "HΦ".
+  iIntros (w). rewrite right_id_L. iApply "HΦ".
 Qed.
 End list_reverse.
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index 01441c800708b8ba694685b2b7bfc5ddf8646215..2e91d34175262e978b5d2ceaa04260032fd29f60 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Import proofmode notation.
@@ -35,9 +35,9 @@ Definition sum' : val := λ: "t",
   !"l".
 
 Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
-  {{{ l ↦ #n ∗ is_tree v t }}}
+  [[{ l ↦ #n ∗ is_tree v t }]]
     sum_loop v #l
-  {{{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }}}.
+  [[{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }]].
 Proof.
   iIntros (Φ) "[Hl Ht] HΦ".
   iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
@@ -55,7 +55,7 @@ Proof.
 Qed.
 
 Lemma sum_wp `{!heapG Σ} v t :
-  {{{ is_tree v t }}} sum' v {{{ RET #(sum t); is_tree v t }}}.
+  [[{ is_tree v t }]] sum' v [[{ RET #(sum t); is_tree v t }]].
 Proof.
   iIntros (Φ) "Ht HΦ". rewrite /sum' /=.
   wp_let. wp_alloc l as "Hl". wp_let.