diff --git a/Iris/Iris.lean b/Iris/Iris.lean
index 017e91885..f5b38cfe3 100644
--- a/Iris/Iris.lean
+++ b/Iris/Iris.lean
@@ -10,5 +10,7 @@ public import Iris.HeapLang.Lib
 public import Iris.Instances
 public import Iris.Instances.Lib
 public import Iris.ProofMode
+public import Iris.ProgramLogic.TotalAdequacy
+public import Iris.ProgramLogic.TotalEctxLifting
 public import Iris.Std
 public import Iris.Tests
diff --git a/Iris/Iris/Algebra/COFESolver.lean b/Iris/Iris/Algebra/COFESolver.lean
index 937c630a9..6a607e591 100644
--- a/Iris/Iris/Algebra/COFESolver.lean
+++ b/Iris/Iris/Algebra/COFESolver.lean
@@ -28,7 +28,7 @@ def A' : Nat → Σ α : Type u, COFE α
   | n+1 => let ⟨A, _⟩ := A' n; ⟨F A A, inferInstance⟩
 
 variable (F) in
-def A (n : Nat) : Type u := (A' F n).1
+abbrev A (n : Nat) : Type u := (A' F n).1
 
 instance instA' (n) : COFE (A' F n).1 := (A' F n).2
 instance instA (n) : COFE (A F n) := (A' F n).2
diff --git a/Iris/Iris/Algebra/IProp.lean b/Iris/Iris/Algebra/IProp.lean
index 9b79432a5..8cf998ac0 100644
--- a/Iris/Iris/Algebra/IProp.lean
+++ b/Iris/Iris/Algebra/IProp.lean
@@ -85,12 +85,12 @@ def IProp.fold : IPre GF -n> IProp GF :=
   OFE.Iso.inv <| OFunctor.Fix.iso (F := (UPredOF (IResF GF)))
 
 @[rocq_alias iProp_solution.iProp_fold_unfold]
-theorem IProp.fold_unfold (P : IProp GF) : IProp.fold GF (IProp.unfold GF P) = P := by
-  simp only [IProp.fold, IProp.unfold, OFE.Iso.inv_hom]
+theorem IProp.fold_unfold (P : IProp GF) : IProp.fold GF (IProp.unfold GF P) = P :=
+  OFunctor.Fix.iso (F := UPredOF (IResF GF)) |>.inv_hom
 
 @[rocq_alias iProp_solution.iProp_unfold_fold]
-theorem IProp.unfold_fold (P : IPre GF) : IProp.unfold GF (IProp.fold GF P) = P := by
-  simp only [IProp.unfold, IProp.fold, OFE.Iso.hom_inv]
+theorem IProp.unfold_fold (P : IPre GF) : IProp.unfold GF (IProp.fold GF P) = P :=
+  OFunctor.Fix.iso (F := UPredOF (IResF GF)) |>.hom_inv
 
 end IProp
 
diff --git a/Iris/Iris/BI/WeakestPre.lean b/Iris/Iris/BI/WeakestPre.lean
index 4a47e0bd2..aef4d25a5 100644
--- a/Iris/Iris/BI/WeakestPre.lean
+++ b/Iris/Iris/BI/WeakestPre.lean
@@ -55,6 +55,7 @@ syntax " [" noWs "{ " wpPostcondInner " }" noWs "] " : wpPostcond
 syntax (name := wp) "WP " wpExpr wpPostcond : term
 
 syntax texanPostcondInner := ((ppSpace (binderIdent <|> bracketedBinder))+ ", ")? " RET " term:min "; " term:min
+
 declare_syntax_cat texanPostcond
 syntax " {" noWs "{ " texanPostcondInner " }" noWs "} " : texanPostcond
 declare_syntax_cat texanPrecond
@@ -62,6 +63,14 @@ syntax " {" noWs "{ " term:min " }" noWs "} " : texanPrecond
 
 syntax (name := texanTriple) texanPrecond wpExpr texanPostcond : term
 
+
+declare_syntax_cat totalTexanPostcond
+syntax " [" noWs "{ " texanPostcondInner " }" noWs "] " : totalTexanPostcond
+declare_syntax_cat totalTexanPrecond
+syntax " [" noWs "{ " term:min " }" noWs "] " : totalTexanPrecond
+
+syntax (name := totalTexanTriple) totalTexanPrecond wpExpr totalTexanPostcond : term
+
 open Lean in
 meta def parseWpExpr : Lean.TSyntax ``wpExpr → Lean.MacroM (TSyntax `term × TSyntax `term × TSyntax `term) := fun
   | `(wpExpr| $e @ $s ; $E) =>
@@ -92,6 +101,16 @@ meta def parseWpPostcond (stx : TSyntax `wpPostcond) : MacroM (TSyntax `term ×
     return (←parseWpPostcondInner inner, true)
   | _ => Macro.throwUnsupported (α := TSyntax `term × Bool)
 
+open Lean in
+private meta def transformTexanBinders
+    (xs : Array (TSyntax [`Lean.binderIdent, `Lean.Parser.Term.bracketedBinder])) :
+    MacroM <| TSyntaxArray [`ident, `Lean.Parser.Term.hole,
+      `Lean.Parser.Term.bracketedBinder] :=
+  xs.mapM fun
+    | `(binderIdent|_) => `(hole|_)
+    | `(binderIdent|$i:ident) => `(ident|$i)
+    | `(bracketedBinder|$x) => `(bracketedBinder|$x)
+
 @[macro wp]
 meta def wpMacro : Lean.Macro := fun stx => do
   match stx with
@@ -106,18 +125,19 @@ meta def wpMacro : Lean.Macro := fun stx => do
 
 meta def parseTexanTriple : Syntax → MacroM Term
   | `({{ $P:term }} $wpExpr {{ $[$[$xs]* ,]? RET $pat ; $Q:term }}) => do
-    let transform (xs : Array (TSyntax [`Lean.binderIdent, `Lean.Parser.Term.bracketedBinder])) : MacroM <| TSyntaxArray [`ident, `Lean.Parser.Term.hole, `Lean.Parser.Term.bracketedBinder] :=
-      xs.mapM fun
-        | `(binderIdent|_) => `(hole|_)
-        | `(binderIdent|$i:ident) => `(ident|$i)
-        | `(bracketedBinder|$x) => `(bracketedBinder|$x)
-
     let k ← match xs with
             | some xs =>
-              let xs ← transform xs -- TSyntax cast
+              let xs ← transformTexanBinders xs
               `(iprop(∀ $xs*, $Q:term -∗ Φ $pat))
             | none => `($Q:term -∗ Φ $pat)
     `(∀ Φ, $P -∗ ▷ $k -∗ (WP $wpExpr {{ Φ }}))
+  | `([{ $P:term }] $wpExpr [{ $[$[$xs]* ,]? RET $pat ; $Q:term }]) => do
+    let k ← match xs with
+            | some xs =>
+              let xs ← transformTexanBinders xs
+              `(iprop(∀ $xs*, $Q:term -∗ Φ $pat))
+            | none => `($Q:term -∗ Φ $pat)
+    `(∀ Φ, $P -∗ $k -∗ (WP $wpExpr [{ Φ }]))
   | _ => Lean.Macro.throwUnsupported
 
 @[macro Iris.BI.iprop]
@@ -125,7 +145,7 @@ meta def wpTexanTriple : Lean.Macro
   | `(iprop($P)) => do `(iprop(□ $(← parseTexanTriple P)))
   | _ => Lean.Macro.throwUnsupported
 
-@[macro texanTriple]
+@[macro texanTriple, macro totalTexanTriple]
 meta def wpTexanTripleTerm : Lean.Macro
   | P => do `(⊢ $(← parseTexanTriple P))
 
diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean
index 1039ca5cb..dc98695e0 100644
--- a/Iris/Iris/Instances/IProp/Instance.lean
+++ b/Iris/Iris/Instances/IProp/Instance.lean
@@ -170,25 +170,19 @@ def IProp.foldi : FF.api τ (IPre FF) -n> FF.api τ (IProp FF) :=
 
 @[rocq_alias inG_unfold_fold]
 theorem IProp.unfoldi_foldi (x : FF.api τ (IPre FF)) : unfoldi (foldi x) = x := by
-  refine OFE.eq_dist.mpr fun n => ?_
-  refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm.dist ?_
-  refine .trans ?_ (OFunctor.map_id (F := FF τ |>.fst) x).dist
-  apply OFunctor.map_ne.ne <;> intro _ <;> simp [IProp.unfold, IProp.fold]
+  have h : (IProp.unfold FF).comp (IProp.fold FF) = OFE.Hom.id := OFE.Hom.ext <| funext (IProp.unfold_fold FF)
+  rw [unfoldi, foldi, ← OFunctor.map_comp, h, OFunctor.map_id]
 
 @[rocq_alias inG_fold_unfold]
 theorem IProp.foldi_unfoldi (x : FF.api τ (IProp FF)) : foldi (unfoldi x) = x := by
-  refine OFE.eq_dist.mpr fun n => ?_
-  refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm.dist ?_
-  refine .trans ?_ (OFunctor.map_id (F := FF τ |>.fst) x).dist
-  apply OFunctor.map_ne.ne <;> intro _ <;> simp [IProp.unfold, IProp.fold]
+  have h : (IProp.fold FF).comp (IProp.unfold FF) = OFE.Hom.id := OFE.Hom.ext <| funext (IProp.fold_unfold FF)
+  rw [unfoldi, foldi, ← OFunctor.map_comp, h, OFunctor.map_id]
 
 @[rocq_alias iProp_unfold_equivI]
 theorem IProp.unfold_equivI (P Q : IProp FF) :
     (IProp.unfold FF P ≡ IProp.unfold FF Q) ⊢@{IProp FF} P ≡ Q := by
-  have h := BI.internalEq.of_internalEquiv_ne (PROP := IProp FF) (IProp.fold FF)
+  simpa only [IProp.fold_unfold] using BI.internalEq.of_internalEquiv_ne (PROP := IProp FF) (IProp.fold FF)
     (x := IProp.unfold FF P) (y := IProp.unfold FF Q)
-  rw [IProp.fold_unfold, IProp.fold_unfold] at h
-  exact h
 
 theorem IProp.unfoldi_discreteE {v : FF.api τ (IProp FF)} (hv : OFE.DiscreteE v) :
     OFE.DiscreteE (unfoldi.f v) where
diff --git a/Iris/Iris/ProgramLogic/TotalAdequacy.lean b/Iris/Iris/ProgramLogic/TotalAdequacy.lean
new file mode 100644
index 000000000..6661f81d5
--- /dev/null
+++ b/Iris/Iris/ProgramLogic/TotalAdequacy.lean
@@ -0,0 +1,283 @@
+/-
+Copyright (c) 2026 Marcelo Fornet. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+module
+
+public import Iris.ProgramLogic.TotalWeakestPre
+public import Iris.ProgramLogic.Adequacy
+
+namespace Iris.ProgramLogic
+
+open Iris OFE COFE BI Iris.BI Iris.Algebra Std FromMathlib LawfulSet
+open Language Language.Notation
+
+@[expose] public section
+
+/-! ## Total adequacy -/
+
+/-- Strong normalization for `step`. -/
+def StronglyNormalizing {α : Type _} (step : α → α → Prop) (x : α) : Prop :=
+  Acc (flip step) x
+
+namespace StronglyNormalizing
+
+theorem intro {α : Type _} {step : α → α → Prop} {x : α}
+    (H : ∀ y, step x y → StronglyNormalizing step y) :
+    StronglyNormalizing step x := Acc.intro x H
+
+theorem map {α β : Type _} {stepα : α → α → Prop}
+    {stepβ : β → β → Prop} (f : β → α)
+    (Hlift : ∀ x y, stepβ x y → stepα (f x) (f y))
+    {x : β} (H : StronglyNormalizing stepα (f x)) :
+    StronglyNormalizing stepβ x :=
+  Subrelation.accessible (fun h => Hlift _ _ h) (InvImage.accessible f H)
+
+end StronglyNormalizing
+
+variable {Expr State Obs Val : Type _} [Λ : Language Expr State Obs Val]
+
+section ThreadPool
+
+variable {hlc : HasLC} {GF : BundledGFunctors}
+variable [ι : IrisGS_gen hlc Expr GF]
+
+local instance : OFE (List Expr) := OFE.ofDiscrete _
+
+local instance list_nonexpansive (Ψ : List Expr → IProp GF) : NonExpansive Ψ :=
+  ⟨fun _ _ _ hxy => hxy ▸ .rfl⟩
+
+namespace twptp
+
+local instance : OFE CoPset := OFE.ofDiscrete _
+local instance : OFE Expr := OFE.ofDiscrete _
+local instance : OFE Val := OFE.ofDiscrete _
+
+private theorem step_append_inv (r₁ r₂ : List Expr) {t' : List Expr} {σ₁ σ₂ : State} {κ : List Obs} :
+    (r₁ ++ r₂, σ₁) -<κ>->ₜₚ (t', σ₂) →
+      (∃ r₁', (r₁, σ₁) -<κ>->ₜₚ (r₁', σ₂) ∧
+        t'.Perm (r₁' ++ r₂)) ∨
+      (∃ r₂', (r₂, σ₁) -<κ>->ₜₚ (r₂', σ₂) ∧
+        t'.Perm (r₁ ++ r₂')) := fun H => by
+  generalize hsrc : r₁ ++ r₂ = src at H
+  rcases H with @⟨e, _, _, e', _, efs, Hprim, p, q⟩
+  rcases List.append_eq_append_iff.mp hsrc.symm with (⟨(_ | ⟨a, tail⟩), hr₁, heq⟩ | ⟨bs, hp, hr₂⟩)
+  · exact .inr ⟨e' :: q ++ efs, (heq.trans (List.nil_append r₂)) ▸ .atomic Hprim [] q, by simp [hr₁]⟩
+  · simp_all only [List.cons_append, List.cons.injEq]
+    refine .inl ⟨p ++ e' :: tail ++ efs, .atomic Hprim p tail, ?_⟩
+    simpa [List.append_assoc] using List.perm_append_comm.append_left (p ++ e' :: tail)
+  · exact .inr ⟨bs ++ e' :: q ++ efs, hr₂ ▸ .atomic Hprim bs q, by simp [hp, List.append_assoc]⟩
+
+/-- One unfolding of the total thread-pool predicate. -/
+@[rocq_alias twptp_pre]
+def pre (X : List Expr → IProp GF) (t₁ : List Expr) : IProp GF := iprop(
+  ∀ (t₂ : List Expr) (σ₁ : State) (ns : Nat) (κ κs : List Obs)
+      (σ₂ : State) (nt : Nat),
+    ⌜(t₁, σ₁) -<κ>->ₜₚ (t₂, σ₂)⌝ -∗
+    stateInterp σ₁ ns κs nt ={⊤}=∗
+      ∃ nt', ⌜κ = []⌝ ∗ stateInterp σ₂ (ns + 1) κs nt' ∗ X t₂)
+
+instance pre_mono_inst : BIMonoPred (pre (ι := ι)) where
+  mono_pred := by
+    intro X Y _ _
+    iintro #HXY %t₁ Hpre
+    unfold pre
+    iintro %t₂ %σ₁ %ns %κ %κs %σ₂ %nt %Hstep Hσ
+    imod Hpre $$ %_ %_ %_ %_ %_ %_ %_ %Hstep Hσ with ⟨%nt', %hκ, Hσ, HX⟩
+    iframe %hκ Hσ
+    iapply HXY $$ HX
+  mono_pred_ne.ne {X} _ _ ht := ht ▸ .rfl
+
+@[rocq_alias twptp_pre_mono]
+theorem pre_mono (X Y : List Expr → IProp GF) :
+    ⊢ □ (∀ t, X t -∗ Y t) -∗
+      ∀ t, pre (ι := ι) X t -∗ pre (ι := ι) Y t :=
+  mono_pred (F := pre (ι := ι))
+
+/-- Total weakest precondition for a thread pool. -/
+@[rocq_alias twptp]
+def get (t : List Expr) : IProp GF :=
+  bi_least_fixpoint (pre (ι := ι)) t
+
+instance get_ne : NonExpansive (get (ι := ι)) :=
+  list_nonexpansive _
+
+@[rocq_alias twptp_unfold]
+theorem unfold (t : List Expr) :
+    get (ι := ι) t ⊣⊢ pre (ι := ι) (get (ι := ι)) t :=
+  BI.equiv_iff.1 (least_fixpoint_unfold (pre (ι := ι)))
+
+@[rocq_alias twptp_ind]
+theorem induction (Ψ : List Expr → IProp GF) :
+    (⊢ □ ∀ t, pre (ι := ι) (fun t => iprop(Ψ t ∧ get (ι := ι) t)) t -∗ Ψ t) →
+    ⊢ ∀ t, get (ι := ι) t -∗ Ψ t := fun H => by
+  simpa [get, BIBase.EmpValid] using H.trans (BI.wand_entails (least_fixpoint_ind (F := pre (ι := ι)) (Φ := Ψ)))
+
+@[rocq_alias twptp_Permutation]
+theorem permutation {t₁ t₁' : List Expr} (Hp : t₁.Perm t₁') :
+    get (ι := ι) t₁ ⊢ get (ι := ι) t₁' := by
+  iintro Ht
+  iapply induction (fun t : List Expr => iprop(∀ t', ⌜t.Perm t'⌝ -∗ get (ι := ι) t'))
+    (ι := ι) ?_ $$ %t₁ Ht %t₁' %Hp
+  iintro !> %t Hpre %t' %Htt'
+  simp only [(twptp.unfold (ι := ι) t').to_eq, pre]
+  iintro %t₂ %σ₁ %ns %κ %κs %σ₂ %nt %Hstep Hσ
+  obtain ⟨t₂', H₂perm, Hstep'⟩ := Language.perm_of_step Htt'.symm Hstep
+  imod Hpre $$ %_ %_ %_ %_ %_ %_ %_ %Hstep' Hσ with ⟨%nt', %hκ, Hσ, ⟨HIH, -⟩⟩
+  iframe %hκ Hσ
+  iapply HIH $$ %t₂ %H₂perm.symm
+
+@[rocq_alias twptp_app]
+theorem app (t₁ t₂ : List Expr) :
+    get (ι := ι) t₁ -∗ get (ι := ι) t₂ -∗ get (ι := ι) (t₁ ++ t₂) := by
+  let Ψ₁ := fun t₁ : List Expr => iprop(
+    ∀ t₂, get (ι := ι) t₂ -∗ get (ι := ι) (t₁ ++ t₂))
+  iintro H₁
+  iapply induction Ψ₁ (ι := ι) ?_ $$ %t₁ H₁ %t₂
+  let Ψ₂ := fun t₂ : List Expr => iprop(
+    ∀ t₁, pre (ι := ι)
+      (fun t => iprop(Ψ₁ t ∧ get (ι := ι) t)) t₁ -∗
+      get (ι := ι) (t₁ ++ t₂))
+  iintro !> %u₁ Hu₁ %u₂ Hu₂
+  iapply induction Ψ₂ (ι := ι) ?_ $$ %u₂ Hu₂ %u₁ Hu₁
+  iintro !> %r₂ Hr₂ %r₁ Hr₁
+  simp only [(twptp.unfold (ι := ι) (r₁ ++ r₂)).to_eq, pre]
+  iintro %t' %σ₁ %ns %κ %κs %σ₂ %nt %Hstep Hσ
+  rcases step_append_inv r₁ r₂ Hstep with (⟨r₁', Hstep₁, Hperm⟩ | ⟨r₂', Hstep₂, Hperm⟩)
+  · imod Hr₁ $$ %_ %_ %_ %_ %_ %_ %_ %Hstep₁ Hσ with ⟨%nt', %hκ, Hσ, ⟨IH₁, -⟩⟩
+    imodintro
+    iframe %hκ Hσ
+    iapply permutation Hperm.symm
+    iapply IH₁ $$ %r₂
+    rw [(twptp.unfold (ι := ι) r₂).to_eq]
+    iapply pre_mono (fun t => iprop(Ψ₂ t ∧ get (ι := ι) t)) _ $$ [] %r₂
+    iintro !> %u ⟨-, $⟩
+    unfold pre
+    iassumption
+  · imod Hr₂ $$ %_ %_ %_ %_ %_ %_ %_ %Hstep₂ Hσ with ⟨%nt', %hκ, Hσ, ⟨IH₂, -⟩⟩
+    iframe %hκ Hσ
+    iunfold Ψ₂, pre at IH₂
+    iapply permutation Hperm.symm $$ (IH₂ $$ %r₁ Hr₁)
+
+private theorem get_nil : ⊢ get (ι := ι) ([] : List Expr) := by
+  simp only [(twptp.unfold (ι := ι) []).to_eq, pre]
+  iintro %t₂ %σ₁ %ns %κ %κs %σ₂ %nt %Hstep
+  grind [List.append_eq_nil_iff]
+
+private theorem bigSepL_get_singleton (es : List Expr) :
+    ([∗list] e ∈ es, get (ι := ι) [e]) ⊢ get (ι := ι) es :=
+  List.rec (get_nil (ι := ι)) (fun e es IH =>
+    (BI.sep_mono_right IH).trans (BI.wand_elim (BI.wand_entails (app [e] es (ι := ι))))) es
+
+@[rocq_alias twp_twptp]
+theorem of_twp (s : Stuckness) (e : Expr) (Φ : Val → IProp GF) :
+    WP e @ s ; ⊤ [{ Φ }] ⊢ get (ι := ι) [e] := by
+  let Ψ := fun (E : CoPset) (e : Expr) (_ : Val → IProp GF) => iprop(
+    ⌜E = ⊤⌝ -∗ get (ι := ι) [e])
+  letI : NonExpansive
+      (fun x : twp.Internal.Args Expr Val GF => Ψ x.1 x.2.1 x.2.2) :=
+    ⟨fun _ _ _ ⟨hE, he, _⟩ => hE ▸ he ▸ .rfl⟩
+  iintro He
+  iapply twp.induction s Ψ (ι := ι) ?_ $$ He %rfl
+  iintro !> %E %e %Φ
+  cases he : toVal e
+  all_goals
+    simp only [twp.pre, he]
+    iintro Hpre %hE
+    simp only [hE, (twptp.unfold (ι := ι) [e]).to_eq, pre]
+    iintro %t₂ %σ₁ %ns %κ %κs %σ₂ %nt %Hstep
+    obtain ⟨e₂, efs, Hprim, rfl⟩ :
+        ∃ e₂ efs, (e, σ₁) -<κ>-> (e₂, σ₂, efs) ∧ t₂ = e₂ :: efs := by
+      grind [List.append_eq_singleton_iff]
+  next =>
+    iintro Hσ
+    imod Hpre $$ Hσ with ⟨%_, Hpre⟩
+    imod Hpre $$ %κ %e₂ %σ₂ %efs %Hprim with ⟨%hκ, Hσ, ⟨IH₂, -⟩, Hefs⟩
+    iframe %hκ Hσ
+    rw [show e₂ :: efs = [e₂] ++ efs by simp]
+    iapply app [e₂] efs (ι := ι) $$ (IH₂ $$ %rfl)
+    iapply (BigSepL.bigSepL_mono_of_forall ((sep_intro_emp_valid_left (pure_intro rfl) and_elim_l).trans
+      (wand_elim_swap .rfl))).trans (bigSepL_get_singleton efs (ι := ι)) $$ Hefs
+  next => simpa [he] using Language.val_stuck Hprim
+
+end twptp
+
+@[rocq_alias twptp_total]
+theorem twptp_total (t : List Expr) (σ : State) (ns nt : Nat) :
+    stateInterp σ ns ([] : List Obs) nt -∗ twptp.get (ι := ι) t
+      ={⊤|}=∗ ⌜StronglyNormalizing
+        (Language.ErasedStep (Expr := Expr) (State := State) (Obs := Obs))
+        (t, σ)⌝ := by
+  let Ψ := fun t : List Expr => iprop(
+    ∀ (σ : State) (ns nt : Nat),
+      StateInterp.stateInterp (GF := GF) σ ns ([] : List Obs) nt -∗
+      |={⊤|}=> ⌜StronglyNormalizing
+        (Language.ErasedStep (Expr := Expr) (State := State) (Obs := Obs))
+        (t, σ)⌝)
+  iintro Hσ Ht
+  iapply twptp.induction Ψ (ι := ι) ?_ $$ %t Ht %σ %ns %nt Hσ
+  iintro !> %t
+  unfold twptp.pre
+  iintro Hpre %σ %ns %nt Hσ
+  iapply fupd_finally_mono (pure_mono StronglyNormalizing.intro)
+  iintro %⟨t₂, σ₂⟩ %⟨κ, Hstep⟩
+  imod Hpre $$ %_ %_ %_ %_ %_ %_ %_ %Hstep Hσ with ⟨%nt', %hκ, Hσ, ⟨IH, -⟩⟩
+  iapply IH $$ %σ₂ %(ns + 1) %nt' Hσ
+
+end ThreadPool
+
+omit Λ in
+/-- Total adequacy for thread-pool reduction. -/
+@[rocq_alias twp_total]
+theorem twp_total {hlc : HasLC} {GF : BundledGFunctors}
+    [InvGpreS GF] [Language Expr State Obs Val]
+    (s : Stuckness) (e : Expr) (σ : State)
+    (Φ : Val → IProp GF) (n m : Nat)
+    (Hwp : ∀ [InvGS_gen hlc GF],
+      ⊢ |={⊤}=>
+        ∃ (stateI : State → Nat → List Obs → Nat → IProp GF)
+          (numLatersPerStep : Nat → Nat)
+          (forkPost : Val → IProp GF)
+          (mono : ∀ σ ns obs nt,
+            stateI σ ns obs nt ⊢ |={∅}=> stateI σ (ns + 1) obs nt),
+        let _ : IrisGS_gen hlc Expr GF :=
+          .mk (toStateInterp := ⟨stateI⟩) numLatersPerStep forkPost mono
+        iprop(stateI σ n [] 0 ∗
+          (£ m -∗ WP e @ s ; ⊤ [{ Φ }]))) :
+    StronglyNormalizing
+      (Language.ErasedStep (Expr := Expr) (State := State) (Obs := Obs))
+      ([e], σ) := by
+  refine pure_soundness (PROP := IProp GF) (fupd_finally_soundness hlc m ⊤ _ ?_)
+  iintro %Hinv Hcred
+  imod Hwp with
+    ⟨%stateI, %numLatersPerStep, %forkPost, %mono, Hσ, Htwp⟩
+  letI iG : IrisGS_gen hlc Expr GF :=
+    .mk (toStateInterp := ⟨stateI⟩) numLatersPerStep forkPost mono
+  iapply twptp_total [e] σ n 0 (ι := iG) $$ Hσ
+  iapply twptp.of_twp s e Φ (ι := iG) $$ (Htwp $$ Hcred)
+
+/-- Erased single-expression reduction. -/
+def ExprErasedStep : Expr × State → Expr × State → Prop
+  | (e₁, σ₁), (e₂, σ₂) =>
+      ∃ (κ : List Obs) (efs : List Expr), (e₁, σ₁) -<κ>-> (e₂, σ₂, efs)
+
+/-- A language whose primitive steps do not fork. -/
+class LanguageNoFork (Expr State Obs Val : Type _)
+    [Language Expr State Obs Val] : Prop where
+  no_fork {e₁ e₂ : Expr} {σ₁ σ₂ : State} {κ : List Obs} {efs : List Expr} :
+    (e₁, σ₁) -<κ>-> (e₂, σ₂, efs) → efs = []
+
+/-- Derive single-expression normalization from thread-pool normalization. -/
+theorem stronglyNormalizing_expr_of_threadPool
+    [LanguageNoFork Expr State Obs Val] {e : Expr} {σ : State}
+    (H : StronglyNormalizing
+      (Language.ErasedStep (Expr := Expr) (State := State) (Obs := Obs))
+      ([e], σ)) :
+    StronglyNormalizing
+      (ExprErasedStep (Expr := Expr) (State := State) (Obs := Obs))
+      (e, σ) :=
+  StronglyNormalizing.map (fun ρ : Expr × State => ([ρ.1], ρ.2))
+    (fun _ _ ⟨κ, efs, Hstep⟩ => ⟨κ, by simpa [LanguageNoFork.no_fork Hstep] using Step.atomic Hstep [] []⟩) H
+
+end
+end Iris.ProgramLogic
diff --git a/Iris/Iris/ProgramLogic/TotalEctxLifting.lean b/Iris/Iris/ProgramLogic/TotalEctxLifting.lean
new file mode 100644
index 000000000..c62fa9cb5
--- /dev/null
+++ b/Iris/Iris/ProgramLogic/TotalEctxLifting.lean
@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2026 Marcelo Fornet. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+module
+
+public import Iris.ProgramLogic.TotalLifting
+public import Iris.ProgramLogic.EctxiLanguage
+
+namespace Iris.ProgramLogic
+
+open Iris BI Language.Notation EctxLanguage EctxLanguage.Notation
+
+@[expose] public section
+
+/-! ## Total lifting rules for evaluation-context languages -/
+
+variable {hlc : outParam HasLC} {Expr Ectx State Obs Val}
+variable [Λ : EctxLanguage Expr Ectx State Obs Val]
+variable {GF : BundledGFunctors} [ι : IrisGS_gen hlc Expr GF]
+variable {s : Stuckness} {E : CoPset} {e₁ e₂ : Expr}
+variable {Φ : Val → IProp GF}
+
+private theorem baseStep_of_primStep {e₂' σ₁ σ₂ κ eₜ}
+    (Hred : BaseStep.ReducibleNoObs (e₁, σ₁))
+    (Hstep : (e₁, σ₁) -<κ>-> (e₂', σ₂, eₜ)) :
+    (e₁, σ₁) -<κ>->ᵇ (e₂', σ₂, eₜ) :=
+  baseStep_of_primStep_of_baseStep_reducible (BaseStep.reducible_of_reducibleNoObs Hred) Hstep
+
+private theorem baseStep_mono {E₁ E₂ : CoPset}
+    {Q : Nat → List Obs → Nat → List Obs → Expr → State → List Expr → IProp GF} :
+    (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E₁,E₂}=∗
+      ⌜BaseStep.ReducibleNoObs (e₁, σ₁)⌝ ∗
+      ∀ κ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<κ>->ᵇ (e₂, σ₂, eₜ)⌝ ={E₂,E₁}=∗
+        Q ns obs nt κ e₂ σ₂ eₜ) ⊢
+    ∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E₁,E₂}=∗
+      ⌜s.MaybeReducibleNoObs (e₁, σ₁)⌝ ∗
+      ∀ κ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<κ>-> (e₂, σ₂, eₜ)⌝ ={E₂,E₁}=∗
+        Q ns obs nt κ e₂ σ₂ eₜ := by
+  iintro H %σ₁ %ns %obs %nt Hσ
+  imod H $$ Hσ with ⟨%Hred, H⟩
+  have Hred' : s.MaybeReducibleNoObs (e₁, σ₁) := by grind [primStep_reducibleNoObs_of_baseStep_reducibleNoObs]
+  iframe %Hred'
+  iintro !> %κ %e₂ %σ₂ %eₜ %Hstep
+  iapply H $$ %κ %e₂ %σ₂ %eₜ %(baseStep_of_primStep Hred Hstep)
+
+@[rocq_alias twp_lift_base_step]
+theorem twp_lift_base_step (h : toVal e₁ = none) :
+    (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E,∅}=∗
+      ⌜BaseStep.ReducibleNoObs (e₁, σ₁)⌝ ∗
+      ∀ κ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<κ>->ᵇ (e₂, σ₂, eₜ)⌝ ={∅,E}=∗
+        ⌜κ = []⌝ ∗
+        stateInterp σ₂ (ns + 1) obs (nt + eₜ.length) ∗
+        WP e₂ @ s; E [{ Φ }] ∗
+        [∗list] ef ∈ eₜ, WP ef @ s; ⊤ [{ ι.forkPost }])
+    ⊢ WP e₁ @ s; E [{ Φ }] :=
+  baseStep_mono.trans (twp_lift_step h)
+
+theorem twp_lift_base_step_no_fork (h : toVal e₁ = none) :
+    (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E,∅}=∗
+      ⌜BaseStep.ReducibleNoObs (e₁, σ₁)⌝ ∗
+      ∀ κ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<κ>->ᵇ (e₂, σ₂, eₜ)⌝ ={∅,E}=∗
+        ⌜κ = []⌝ ∗ ⌜eₜ = []⌝ ∗
+        stateInterp σ₂ (ns + 1) obs nt ∗
+        WP e₂ @ s; E [{ Φ }])
+    ⊢ WP e₁ @ s; E [{ Φ }] :=
+  baseStep_mono.trans (twp_lift_step_no_fork h)
+
+@[rocq_alias twp_lift_pure_base_step_no_fork]
+theorem twp_lift_pure_base_step_no_fork [Inhabited State]
+    (Hred : ∀ σ, BaseStep.ReducibleNoObs (e₁, σ))
+    (Hpure : ∀ σ₁ κ e₂' σ₂ eₜ,
+      (e₁, σ₁) -<κ>->ᵇ (e₂', σ₂, eₜ) →
+      κ = [] ∧ σ₂ = σ₁ ∧ eₜ = []) :
+    (|={E}=> ∀ κ e₂' eₜ σ,
+      ⌜(e₁, σ) -<κ>->ᵇ (e₂', σ, eₜ)⌝ -∗
+      WP e₂' @ s; E [{ Φ }])
+    ⊢ WP e₁ @ s; E [{ Φ }] := by
+  refine (BIFUpdate.mono (forall_mono fun _ => forall_mono fun _ => forall_mono fun _ => forall_mono fun σ =>
+    wand_mono_left <| pure_mono fun Hstep => baseStep_of_primStep (Hred σ) Hstep)).trans <| twp_lift_pure_step_no_fork
+    (by grind [primStep_reducibleNoObs_of_baseStep_reducibleNoObs]) (by grind only [→ baseStep_of_primStep])
+
+@[rocq_alias twp_lift_atomic_base_step]
+theorem twp_lift_atomic_base_step (h : toVal e₁ = none) :
+    (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E}=∗
+      ⌜BaseStep.ReducibleNoObs (e₁, σ₁)⌝ ∗
+      ∀ κ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<κ>->ᵇ (e₂, σ₂, eₜ)⌝ ={E}=∗
+        ⌜κ = []⌝ ∗
+        stateInterp σ₂ (ns + 1) obs (nt + eₜ.length) ∗
+        (∃ v, ⌜toVal e₂ = some v⌝ ∧ Φ v) ∗
+        [∗list] ef ∈ eₜ, WP ef @ s; ⊤ [{ ι.forkPost }])
+    ⊢ WP e₁ @ s; E [{ Φ }] :=
+  baseStep_mono.trans (twp_lift_atomic_step h)
+
+@[rocq_alias twp_lift_atomic_base_step_no_fork]
+theorem twp_lift_atomic_base_step_no_fork (h : toVal e₁ = none) :
+    (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E}=∗
+      ⌜BaseStep.ReducibleNoObs (e₁, σ₁)⌝ ∗
+      ∀ κ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<κ>->ᵇ (e₂, σ₂, eₜ)⌝ ={E}=∗
+        ⌜κ = []⌝ ∗ ⌜eₜ = []⌝ ∗
+        stateInterp σ₂ (ns + 1) obs nt ∗
+        ∃ v, ⌜toVal e₂ = some v⌝ ∧ Φ v)
+    ⊢ WP e₁ @ s; E [{ Φ }] :=
+  baseStep_mono.trans (twp_lift_atomic_step_no_fork h)
+
+@[rocq_alias twp_lift_pure_det_base_step_no_fork]
+theorem twp_lift_pure_det_base_step_no_fork [Inhabited State]
+    (_h : toVal e₁ = none)
+    (Hred : ∀ σ, BaseStep.ReducibleNoObs (e₁, σ))
+    (Hpure : ∀ σ κ e₂' σ₂ eₜ,
+      (e₁, σ) -<κ>->ᵇ (e₂', σ₂, eₜ) →
+      κ = [] ∧ σ₂ = σ ∧ e₂' = e₂ ∧ eₜ = []) :
+    WP e₂ @ s; E [{ Φ }] ⊢ WP e₁ @ s; E [{ Φ }] :=
+  fupd_intro.trans <| twp_lift_pure_det_step_no_fork (e₂ := e₂)
+    (by grind [primStep_reducibleNoObs_of_baseStep_reducibleNoObs]) (by grind only [→ baseStep_of_primStep])
+
+end
+end Iris.ProgramLogic
diff --git a/Iris/Iris/ProgramLogic/TotalLifting.lean b/Iris/Iris/ProgramLogic/TotalLifting.lean
new file mode 100644
index 000000000..be76b4757
--- /dev/null
+++ b/Iris/Iris/ProgramLogic/TotalLifting.lean
@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2026 Marcelo Fornet. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+module
+
+public import Iris.ProgramLogic.TotalWeakestPre
+
+namespace Iris.ProgramLogic
+
+open Iris Language Language.Notation BI
+
+@[expose] public section
+
+/-! ## Total lifting rules -/
+
+variable {hlc : outParam HasLC} {Expr State Obs Val}
+variable [Λ : Language Expr State Obs Val]
+variable {GF : BundledGFunctors} [ι : IrisGS_gen hlc Expr GF]
+variable {s : Stuckness} {E E₁ E₂ : CoPset}
+variable {e e₁ e₂ : Expr} {Φ : Val → IProp GF}
+
+@[rocq_alias twp_lift_step]
+theorem twp_lift_step (h : toVal e₁ = none) :
+    (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E,∅}=∗
+      ⌜s.MaybeReducibleNoObs (e₁, σ₁)⌝ ∗
+      ∀ κ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<κ>-> (e₂, σ₂, eₜ)⌝ ={∅,E}=∗
+        ⌜κ = []⌝ ∗
+        stateInterp σ₂ (ns + 1) obs (nt + eₜ.length) ∗
+        WP e₂ @ s; E [{ Φ }] ∗
+        [∗list] ef ∈ eₜ, WP ef @ s; ⊤ [{ ι.forkPost }])
+    ⊢ WP e₁ @ s; E [{ Φ }] := by rw [twp.unfold.to_eq, twp.pre, h]
+
+theorem twp_lift_step_no_fork (h : toVal e₁ = none) :
+    (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E,∅}=∗
+      ⌜s.MaybeReducibleNoObs (e₁, σ₁)⌝ ∗
+      ∀ κ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<κ>-> (e₂, σ₂, eₜ)⌝ ={∅,E}=∗
+        ⌜κ = []⌝ ∗ ⌜eₜ = []⌝ ∗
+        stateInterp σ₂ (ns + 1) obs nt ∗
+        WP e₂ @ s; E [{ Φ }])
+    ⊢ WP e₁ @ s; E [{ Φ }] := by
+  refine .trans ?_ <| twp_lift_step h
+  iintro H %σ₁ %ns %obs %nt Hσ
+  imod H $$ Hσ with ⟨%Hred, H⟩
+  iframe %Hred
+  iintro !> %κ %e₂ %σ₂ %eₜ Hstep
+  imod H $$ Hstep with ⟨%hκ, %heₜ, Hσ, Hwp⟩
+  simp only [heₜ, List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil, BI.sep_emp.to_eq]
+  iframe %hκ Hσ Hwp
+
+@[rocq_alias twp_lift_atomic_step]
+theorem twp_lift_atomic_step (h : toVal e₁ = none) :
+    (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E}=∗
+      ⌜s.MaybeReducibleNoObs (e₁, σ₁)⌝ ∗
+      ∀ κ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<κ>-> (e₂, σ₂, eₜ)⌝ ={E}=∗
+        ⌜κ = []⌝ ∗
+        stateInterp σ₂ (ns + 1) obs (nt + eₜ.length) ∗
+        (∃ v, ⌜toVal e₂ = some v⌝ ∧ Φ v) ∗
+        [∗list] ef ∈ eₜ, WP ef @ s; ⊤ [{ ι.forkPost }])
+    ⊢ WP e₁ @ s; E [{ Φ }] := by
+  refine .trans ?_ <| twp_lift_step h
+  iintro H %σ₁ %ns %obs %nt Hσ
+  imod H $$ Hσ with ⟨%Hred, H⟩
+  iapply fupd_mask_intro Std.LawfulSet.empty_subset
+  iintro Hclose
+  iframe %Hred
+  iintro %κ %e₂ %σ₂ %eₜ Hstep
+  imod Hclose with -
+  imod H $$ Hstep with ⟨%hκ, Hσ, ⟨%v, %hval, HΦ⟩, Hefs⟩
+  iframe %hκ Hσ Hefs
+  iapply twp.value (ToVal.coe_of_toVal_eq_some hval).symm $$ HΦ
+
+theorem twp_lift_atomic_step_no_fork (h : toVal e₁ = none) :
+    (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E}=∗
+      ⌜s.MaybeReducibleNoObs (e₁, σ₁)⌝ ∗
+      ∀ κ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<κ>-> (e₂, σ₂, eₜ)⌝ ={E}=∗
+        ⌜κ = []⌝ ∗ ⌜eₜ = []⌝ ∗
+        stateInterp σ₂ (ns + 1) obs nt ∗
+        ∃ v, ⌜toVal e₂ = some v⌝ ∧ Φ v)
+    ⊢ WP e₁ @ s; E [{ Φ }] := by
+  refine .trans ?_ <| twp_lift_atomic_step h
+  iintro H %σ₁ %ns %obs %nt Hσ
+  imod H $$ Hσ with ⟨%Hred, H⟩
+  iframe %Hred
+  iintro !> %κ %e₂ %σ₂ %eₜ Hstep
+  imod H $$ Hstep with ⟨%hκ, %heₜ, Hσ, Hval⟩
+  simp only [heₜ, List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil, BI.sep_emp.to_eq]
+  iframe %hκ Hσ Hval
+
+@[rocq_alias twp_lift_pure_step_no_fork]
+theorem twp_lift_pure_step_no_fork [Inhabited State]
+    (Hsafe : ∀ σ₁, PrimStep.ReducibleNoObs (e₁, σ₁))
+    (Hpure : ∀ σ₁ κ e₂' σ₂ eₜ,
+      (e₁, σ₁) -<κ>-> (e₂', σ₂, eₜ) →
+      κ = [] ∧ σ₂ = σ₁ ∧ eₜ = []) :
+    (|={E}=> ∀ κ e₂' eₜ σ,
+      ⌜(e₁, σ) -<κ>-> (e₂', σ, eₜ)⌝ -∗
+      WP e₂' @ s; E [{ Φ }])
+    ⊢ WP e₁ @ s; E [{ Φ }] := by
+  refine .trans ?_ <| twp_lift_step_no_fork (toVal_none_of_reducible <| reducible_of_reducibleNoObs (Hsafe default))
+  iintro H %σ₁ %ns %obs %nt Hσ
+  imod H
+  iapply fupd_mask_intro Std.LawfulSet.empty_subset
+  iintro Hclose
+  isplitr
+  · exact BI.pure_intro (by grind [cases Stuckness])
+  · iintro %κ %e₂' %σ₂ %eₜ %Hstep
+    obtain ⟨hκ, rfl, heₜ⟩ := Hpure _ _ _ _ _ Hstep
+    imod ι.stateInterp_mono σ₂ ns obs nt $$ Hσ with Hσ
+    imod Hclose
+    iframe %hκ %heₜ Hσ
+    iapply H $$ %κ %e₂' %eₜ %σ₂ %Hstep
+
+@[rocq_alias twp_lift_pure_det_step_no_fork]
+theorem twp_lift_pure_det_step_no_fork [Inhabited State]
+    (Hsafe : ∀ σ₁, PrimStep.ReducibleNoObs (e₁, σ₁))
+    (Hpure : ∀ σ₁ κ e₂' σ₂ eₜ,
+      (e₁, σ₁) -<κ>-> (e₂', σ₂, eₜ) →
+      κ = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ = []) :
+    (|={E}=> WP e₂ @ s; E [{ Φ }]) ⊢ WP e₁ @ s; E [{ Φ }] := by
+  refine (BIFUpdate.mono ?_).trans <| twp_lift_pure_step_no_fork Hsafe (by grind only)
+  iintro Hwp %κ %e₂' %eₜ %σ %Hstep
+  exact (Hpure _ _ _ _ _ Hstep).2.2.1 ▸ .rfl
+
+@[rocq_alias twp_pure_step]
+theorem twp_pure_step [Inhabited State]
+    (Hexec : PureExec φ n e₁ e₂) (Hφ : φ) :
+    WP e₂ @ s; E [{ Φ }] ⊢ WP e₁ @ s; E [{ Φ }] := (Hexec.pureExec Hφ).head_induction_on
+      (motive := fun _ e _ => WP e₂ @ s; E [{ Φ }] ⊢ WP e @ s; E [{ Φ }]) .rfl fun e₃ Hstep _ IH =>
+    (IH.trans fupd_intro).trans <| twp_lift_pure_det_step_no_fork (e₂ := e₃) Hstep.1 (by grind only [Hstep.2])
+
+end
+end Iris.ProgramLogic
diff --git a/Iris/Iris/ProgramLogic/TotalWeakestPre.lean b/Iris/Iris/ProgramLogic/TotalWeakestPre.lean
new file mode 100644
index 000000000..28c034946
--- /dev/null
+++ b/Iris/Iris/ProgramLogic/TotalWeakestPre.lean
@@ -0,0 +1,458 @@
+/-
+Copyright (c) 2026 Marcelo Fornet. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+module
+
+public import Iris.BI.Lib.Fixpoint
+public import Iris.ProgramLogic.WeakestPre
+public import Iris.ProofMode
+
+namespace Iris
+
+open ProgramLogic Language Language.Notation Std OFE BI
+
+@[expose] public section
+
+/-!
+# Total weakest preconditions
+
+This file provides the core definition and selected rules for total WP. Total WP
+uses a least fixed point without a later modality and permits only
+observation-free reductions. Further Iris-Rocq rules can be ported separately.
+-/
+
+variable {hlc : outParam HasLC} {Expr State Obs Val}
+variable [Λ : Language Expr State Obs Val]
+variable {GF : BundledGFunctors} [ι : IrisGS_gen hlc Expr GF]
+
+/-- The stuckness-dependent reducibility condition for total WP. -/
+abbrev Stuckness.MaybeReducibleNoObs : Stuckness → Expr × State → Prop
+  | .NotStuck, ρ => PrimStep.ReducibleNoObs ρ
+  | .MaybeStuck, _ => True
+
+namespace twp
+
+local instance : OFE CoPset := OFE.ofDiscrete _
+local instance : OFE Expr := OFE.ofDiscrete _
+local instance : OFE Val := OFE.ofDiscrete _
+
+namespace Internal
+
+abbrev Args (Expr Val : Type _) (GF : BundledGFunctors) :=
+  CoPset × Expr × (Val → IProp GF)
+
+end Internal
+
+@[rocq_alias twp_pre]
+def pre (s : Stuckness) (twp : CoPset → Expr → (Val → IProp GF) → IProp GF) (E : CoPset)
+    (e₁ : Expr) (Φ : Val → IProp GF) : IProp GF :=
+  match toVal e₁ with
+  | some v => iprop% |={E}=> Φ v
+  | none => iprop% ∀ (σ₁ : State) (ns : Nat) (obs : List Obs) (nt : Nat),
+    stateInterp σ₁ ns obs nt ={E,∅}=∗
+    ⌜s.MaybeReducibleNoObs (e₁, σ₁)⌝ ∗
+    ∀ (κ : List Obs) e₂ σ₂ eₜ,
+      ⌜(e₁, σ₁) -<κ>-> (e₂, σ₂, eₜ)⌝ ={∅,E}=∗
+      ⌜κ = []⌝ ∗
+      stateInterp σ₂ (ns + 1) obs (nt + eₜ.length) ∗
+      twp E e₂ Φ ∗
+      [∗list] e' ∈ eₜ, twp ⊤ e' ι.forkPost
+
+namespace Internal
+
+def pre' (s : Stuckness) (X : Args Expr Val GF → IProp GF) : Args Expr Val GF → IProp GF
+  | (E, e, Φ) => pre s (fun E e Φ => X (E, e, Φ)) E e Φ
+
+end Internal
+
+@[rocq_alias twp_pre_mono]
+theorem pre_mono (s : Stuckness) (X Y : CoPset → Expr → (Val → IProp GF) → IProp GF) :
+    ⊢ □ (∀ E e Φ, X E e Φ -∗ Y E e Φ) -∗
+      ∀ E e Φ, pre s X E e Φ -∗ pre s Y E e Φ := by
+  iintro #H %E %e %Φ Hpre
+  unfold pre
+  cases toVal e with
+  | some => itrivial
+  | none =>
+      iintro %σ₁ %ns %obs %nt Hσ
+      imod Hpre $$ Hσ with ⟨%Hred, Hstep⟩
+      iframe %Hred
+      iintro !> %κ %e₂ %σ₂ %eₜ Hprim
+      imod Hstep $$ Hprim with ⟨%hκ, Hσ, He₂, Hefs⟩
+      iframe %hκ Hσ
+      isplitl [He₂]
+      · iapply H $$ He₂
+      · iapply BI.BigSepL.bigSepL_impl $$ Hefs
+        iintro !> !> %k %ef %Hef Hef
+        iapply H $$ Hef
+
+namespace Internal
+
+instance pre'_mono (s : Stuckness) : BIMonoPred (pre' (ι := ι) s) where
+  mono_pred := by
+    intro X Y _ _
+    iintro #HXY %⟨E, e, Φ⟩ HX
+    unfold pre'
+    iapply pre_mono s (fun E e Φ => X (E, e, Φ)) (fun E e Φ => Y (E, e, Φ)) $$ [] [$]
+    iintro !> %E %e %Φ H
+    iapply HXY $$ H
+  mono_pred_ne.ne {n} := fun ⟨E₁, e₁, Φ₁⟩ ⟨E₂, e₂, Φ₂⟩ ⟨hE, he, hΦ⟩ =>
+    (show E₁ = E₂ from hE) ▸ (show e₁ = e₂ from he) ▸ by
+    simp only [pre', pre]
+    match toVal e₁ with
+    | some v => exact BIFUpdate.ne.ne (hΦ v)
+    | none =>
+      refine forall_ne fun _ => forall_ne fun _ => forall_ne fun _ => forall_ne fun _ =>
+        wand_ne.ne .rfl <| BIFUpdate.ne.ne <| sep_ne.ne .rfl <| forall_ne fun _ => forall_ne fun e =>
+        forall_ne fun _ => forall_ne fun _ => wand_ne.ne .rfl <| BIFUpdate.ne.ne <|
+        sep_ne.ne .rfl <| sep_ne.ne .rfl <| sep_ne.ne ?_ .rfl
+      exact NonExpansive.ne (show (E₁, e, Φ₁) ≡{n}≡ (E₁, e, Φ₂) from ⟨.rfl, .rfl, hΦ⟩)
+
+def get (s : Stuckness) (E : CoPset) (e : Expr) (Φ : Val → IProp GF) : IProp GF :=
+  bi_least_fixpoint (pre' s) (E, e, Φ)
+
+end Internal
+
+instance instTotalWp : TotalWp (IProp GF) Expr Val Stuckness where
+  totalWp := Internal.get
+
+section Rules
+
+@[rocq_alias twp_unfold]
+theorem unfold {s E} {e : Expr} {Φ : Val → IProp GF} :
+    WP e @ s ; E [{ Φ }] ⊣⊢ pre s (TotalWp.totalWp s) E e Φ :=
+  BI.equiv_iff.1 (least_fixpoint_unfold (Internal.pre' s))
+
+@[rocq_alias twp_ind]
+theorem induction (s : Stuckness) (Ψ : CoPset → Expr → (Val → IProp GF) → IProp GF)
+    [HΨ : NonExpansive (fun x : Internal.Args Expr Val GF => Ψ x.1 x.2.1 x.2.2)] :
+    (⊢ □ (∀ E e Φ, pre s (fun E e Φ => iprop(Ψ E e Φ ∧ WP e @ s ; E [{ Φ }])) E e Φ -∗ Ψ E e Φ)) →
+    ⊢ ∀ E e Φ, WP e @ s ; E [{ Φ }] -∗ Ψ E e Φ := fun H => by
+  iintro %E %e %Φ
+  change ⊢ bi_least_fixpoint (Internal.pre' s) (E, e, Φ) -∗ Ψ E e Φ
+  iapply least_fixpoint_ind (F := Internal.pre' s) (Φ := fun x => Ψ x.1 x.2.1 x.2.2) $$ []
+  iintro !> %⟨E, e, Φ⟩
+  simp only [Internal.pre', TotalWp.totalWp, Internal.get] at H ⊢
+  iapply H
+
+@[rocq_alias twp_ne]
+instance ne {s : Stuckness} {E} {e : Expr} :
+    NonExpansive (TotalWp.totalWp (PROP := IProp GF) s E e) where
+  ne {n Φ₁ Φ₂} HΦ := NonExpansive.ne (f := bi_least_fixpoint (Internal.pre' s))
+    (show (E, e, Φ₁) ≡{n}≡ (E, e, Φ₂) from ⟨.rfl, .rfl, HΦ⟩)
+
+@[rocq_alias twp_value_fupd']
+theorem value_fupd' {s : Stuckness} {E} {Φ : Val → IProp GF} {v : Val} :
+    WP (v : Expr) @ s ; E [{ Φ }] ⊣⊢ |={E}=> Φ v := by
+  simp [unfold.to_eq, pre, toVal_coe]
+
+@[rocq_alias twp_value_fupd]
+theorem value_fupd {s : Stuckness} {E} {e : Expr} {v : Val} {Φ : Val → IProp GF} (h : e = v) :
+    WP e @ s ; E [{ Φ }] ⊣⊢ |={E}=> Φ v := h ▸ value_fupd'
+
+@[rocq_alias twp_strong_mono]
+theorem strong_mono {s₁ s₂ : Stuckness} {E₁ E₂} {e : Expr}
+    {Φ Ψ : Val → IProp GF} (hs : s₁ ≤ s₂) (hE : E₁ ⊆ E₂) :
+    ⊢ WP e @ s₁ ; E₁ [{ Φ }] -∗
+      (∀ v, Φ v ={E₂}=∗ Ψ v) -∗ WP e @ s₂ ; E₂ [{ Ψ }] := by
+  let Pred := fun (E : CoPset) (e : Expr) (Φ : Val → IProp GF) => iprop%
+    ∀ E₂ Ψ, ⌜E ⊆ E₂⌝ -∗ (∀ v, Φ v ={E₂}=∗ Ψ v) -∗ WP e @ s₂ ; E₂ [{ Ψ }]
+  have hPred : NonExpansive (fun x : Internal.Args Expr Val GF => Pred x.1 x.2.1 x.2.2) :=
+    ⟨fun _ _ _ ⟨hE, he, hΦ⟩ => hE ▸ he ▸ forall_ne fun _ => forall_ne fun _ => wand_ne.ne .rfl <|
+      wand_ne.ne (forall_ne fun v => wand_ne.ne (hΦ v) .rfl) .rfl⟩
+  iintro H HΦ
+  iapply induction s₁ Pred $$ H [//] [$]
+  · iintro !> %E %e₁ %Φ₁ IH %E' %Ψ' %hE'
+    simp only [(unfold (s := s₂) (E := E') (e := e₁) (Φ := Ψ')).to_eq, pre]
+    cases hval : toVal e₁
+    all_goals iintro Hpost
+    next =>
+      iintro %σ₁ %ns %obs %nt Hσ
+      imod fupd_mask_subseteq hE' with Hclose
+      imod IH $$ Hσ with ⟨%Hred, Hstep⟩
+      have Hred' : s₂.MaybeReducibleNoObs (e₁, σ₁) := by
+        simp only [LE.le] at hs
+        grind [cases Stuckness]
+      iframe %Hred'
+      iintro !> %κ %e₂ %σ₂ %eₜ Hprim
+      imod Hstep $$ Hprim with ⟨%hκ, Hσ, ⟨IH₂, -⟩, Hefs⟩
+      imod Hclose
+      iframe %hκ Hσ
+      isplitl [IH₂ Hpost]
+      · iapply IH₂ $$ [//] Hpost
+      · iapply BI.BigSepL.bigSepL_impl $$ Hefs
+        iintro !> !> %k %ef %Hef ⟨IHef, -⟩
+        iapply IHef $$ %⊤ %ι.forkPost %LawfulSet.subset_refl
+        iintro %v $
+    next =>
+      imod fupd_mask_mono hE' $$ IH with HΦv
+      iapply Hpost $$ HΦv
+
+private theorem strong_mono_with {s₁ s₂ : Stuckness} {E₁ E₂} {e : Expr} {Φ Ψ : Val → IProp GF}
+    (hs : s₁ ≤ s₂) (hE : E₁ ⊆ E₂) (H : ∀ v, ⊢ Φ v ={E₂}=∗ Ψ v) :
+    WP e @ s₁ ; E₁ [{ Φ }] ⊢ WP e @ s₂ ; E₂ [{ Ψ }] :=
+  sep_elim_emp_valid_right (forall_intro H) (wand_elim (wand_entails (strong_mono hs hE)))
+
+@[rocq_alias fupd_twp]
+theorem fupd_twp {s : Stuckness} {E} {e : Expr} {Φ : Val → IProp GF} :
+    (|={E}=> WP e @ s ; E [{ Φ }]) ⊢ WP e @ s ; E [{ Φ }] := by
+  simp only [(unfold (e := e)).to_eq, pre]
+  iintro H
+  cases toVal e
+  · iintro %σ %ns %obs %nt Hσ
+    imod H $$ Hσ with $
+  · imod H with $
+
+@[rocq_alias twp_fupd]
+theorem twp_fupd {s : Stuckness} {E} {e : Expr} {Φ : Val → IProp GF} :
+    WP e @ s ; E [{ v, |={E}=> Φ v }] ⊢ WP e @ s ; E [{ Φ }] :=
+  strong_mono_with (Std.IsPreorder.le_refl _) LawfulSet.subset_refl fun _ => BI.wand_rfl
+
+@[rocq_alias twp_atomic]
+theorem atomic {s : Stuckness} {E₁ E₂ : CoPset} {e : Expr}
+    {Φ : Val → IProp GF} [hatom : Language.Atomic ↑s e] :
+    (|={E₁,E₂}=> WP e @ s ; E₂ [{ v, |={E₂,E₁}=> Φ v }]) ⊢ WP e @ s ; E₁ [{ Φ }] := by
+  simp only [(unfold (e := e)).to_eq, pre]
+  iintro H
+  cases he : toVal e with
+  | some v => icases H with > >$
+  | none =>
+    iintro %σ₁ %ns %obs %nt Hσ
+    imod H $$ Hσ with >⟨$, Hstep⟩
+    iintro !> %κ %e₂ %σ₂ %eₜ %Hprim
+    cases s
+    · imod Hstep $$ %κ %e₂ %σ₂ %eₜ %Hprim with ⟨%hκ, Hσ, He₂, Hefs⟩
+      cases he₂ : toVal e₂ with
+      | some v₂ =>
+        imod (value_fupd (ToVal.coe_of_toVal_eq_some he₂).symm).mp $$ He₂ with >He₂
+        iframe %hκ Hσ Hefs
+        iapply (value_fupd (ToVal.coe_of_toVal_eq_some he₂).symm).mpr $$ He₂
+      | none =>
+        simp only [(unfold (e := e₂)).to_eq, pre, he₂]
+        imod He₂ $$ %σ₂ %(ns + 1) %obs %(nt + eₜ.length) Hσ with ⟨%Hred₂, _⟩
+        exact ((not_reducible_iff_irreducible.mpr (hatom.atomic Hprim)) (reducible_of_reducibleNoObs Hred₂)).elim
+    · imod Hstep $$ [//] with ⟨%hκ, Hσ, He₂, Hefs⟩
+      have ⟨v₂, hv₂⟩ := Option.isSome_iff_exists.mp (hatom.atomic Hprim)
+      imod (value_fupd (ToVal.coe_of_toVal_eq_some hv₂).symm).mp $$ He₂ with >He₂
+      iframe %hκ Hσ Hefs
+      iapply (value_fupd (ToVal.coe_of_toVal_eq_some hv₂).symm).mpr $$ He₂
+
+@[rocq_alias twp_bind]
+theorem bind (K : Expr → Expr) [ctx : Language.Context K]
+    {s : Stuckness} {E : CoPset} {e : Expr} {Φ : Val → IProp GF} :
+    TotalWp.totalWp s E e
+      (fun v : Val => iprop(WP (K v) @ s ; E [{ Φ }])) ⊢ WP (K e) @ s ; E [{ Φ }] := by
+  let Pred := fun (E : CoPset) (e : Expr) (Ψ : Val → IProp GF) => iprop%
+    ∀ Φ, (∀ v, Ψ v -∗ WP (K v) @ s ; E [{ Φ }]) -∗
+      WP (K e) @ s ; E [{ Φ }]
+  letI : NonExpansive (fun x : Internal.Args Expr Val GF => Pred x.1 x.2.1 x.2.2) :=
+    ⟨fun _ _ _ ⟨hE, he, hΨ⟩ => hE ▸ he ▸ BI.forall_ne fun _ =>
+      BI.wand_ne.ne (BI.forall_ne fun v => BI.wand_ne.ne (hΨ v) .rfl) .rfl⟩
+  iintro H
+  iapply induction s Pred $$ H
+  · iintro !> %E %e %Ψ
+    cases he : toVal e
+    all_goals
+      simp only [pre, he]
+      iintro Hpre %Φ Hcont
+    next =>
+      simp only [(unfold (e := K e)).to_eq, pre, ctx.toVal_eq_none_fill he]
+      iintro %σ₁ %ns %obs %nt Hσ
+      imod Hpre $$ Hσ with ⟨%Hred, Hstep⟩
+      have Hred' : s.MaybeReducibleNoObs (K e, σ₁) := by grind [Language.Context.reducibleNoObs_fill]
+      iframe %Hred'
+      iintro !> %κ %e₂ %σ₂ %eₜ %HKstep
+      obtain ⟨e₂', rfl, Hprim⟩ := ctx.primStep_fill_inv he HKstep
+      imod Hstep $$ [//] with ⟨%hκ, Hσ, ⟨IH, -⟩, Hefs⟩
+      iframe %hκ Hσ
+      isplitl [IH Hcont]
+      · iapply IH $$ Hcont
+      · iapply BI.BigSepL.bigSepL_mono_of_forall BI.and_elim_r $$ Hefs
+    next v =>
+      rw [← (ToVal.coe_of_toVal_eq_some he)]
+      ispecialize Hcont $$ %v
+      iapply (fupd_wand_left (P := Ψ v)).trans fupd_twp $$ [$]
+  · iintro %_ $
+
+@[rocq_alias twp_bind_inv]
+theorem bind_inv (K : Expr → Expr) [ctx : Language.Context K]
+    {s : Stuckness} {E : CoPset} {e : Expr} {Φ : Val → IProp GF} :
+    WP (K e) @ s ; E [{ Φ }] ⊢
+      TotalWp.totalWp s E e (fun v : Val => iprop(WP (K v) @ s ; E [{ Φ }])) := by
+  let Pred := fun (E : CoPset) (e' : Expr) (Φ : Val → IProp GF) => iprop%
+    ∀ e, ⌜e' = K e⌝ -∗
+      TotalWp.totalWp s E e (fun v : Val => iprop(WP (K v) @ s ; E [{ Φ }]))
+  letI : NonExpansive (fun x : Internal.Args Expr Val GF => Pred x.1 x.2.1 x.2.2) :=
+    ⟨fun _ _ _ ⟨hE, he, hΦ⟩ => hE ▸ he ▸ BI.forall_ne fun _ =>
+      BI.wand_ne.ne .rfl (NonExpansive.ne fun _ => NonExpansive.ne hΦ)⟩
+  iintro H
+  iapply induction s Pred $$ H %e %rfl
+  iintro !> %E %e' %Φ IH %e %heq
+  rw [heq, unfold.to_eq]
+  cases he : toVal e with
+  | some v =>
+      ihave IHfold : iprop(WP (K e) @ s ; E [{ Φ }]) $$ [IH]
+      · rw [unfold.to_eq]
+        iapply pre_mono s (fun E e Φ => iprop(Pred E e Φ ∧ WP e @ s ; E [{ Φ }])) $$ [] %E %(K e) %Φ IH
+        iintro !> %E %e %Φ ⟨-, $⟩
+      simp only [pre, ← ToVal.coe_of_toVal_eq_some he, toVal_coe]
+      itrivial
+  | none =>
+      simp only [pre, he, ctx.toVal_eq_none_fill he]
+      iintro %σ₁ %ns %obs %nt Hσ
+      imod IH $$ Hσ with ⟨%Hred, Hstep⟩
+      have Hred' : s.MaybeReducibleNoObs (e, σ₁) := by grind [Language.Context.reducibleNoObs_fill_inv]
+      iframe %Hred'
+      iintro !> %κ %e₂ %σ₂ %eₜ %Hprim
+      imod Hstep $$ %_ %_ %_ %_ %(ctx.primStep_fill Hprim) with ⟨$, $, ⟨IH₂, -⟩, Hefs⟩
+      isplitl [IH₂]
+      · iapply IH₂ $$ %e₂ %rfl
+      · iapply BI.BigSepL.bigSepL_mono_of_forall BI.and_elim_r $$ Hefs
+
+@[rocq_alias twp_mono]
+theorem mono {s : Stuckness} {E} {e : Expr} {Φ Ψ : Val → IProp GF}
+    (H : ∀ v, Φ v ⊢ Ψ v) :
+    WP e @ s ; E [{ Φ }] ⊢ WP e @ s ; E [{ Ψ }] :=
+  strong_mono_with (Std.IsPreorder.le_refl _) LawfulSet.subset_refl fun v => entails_wand ((H v).trans fupd_intro)
+
+@[rocq_alias twp_stuck_mono]
+theorem stuck_mono {s₁ s₂ : Stuckness} {E} {e : Expr} {Φ : Val → IProp GF} (H : s₁ ≤ s₂) :
+    WP e @ s₁ ; E [{ Φ }] ⊢ WP e @ s₂ ; E [{ Φ }] :=
+  strong_mono_with H LawfulSet.subset_refl fun _ => BI.entails_wand fupd_intro
+
+@[rocq_alias twp_stuck_weaken]
+theorem stuck_weaken {s : Stuckness} {E} {e : Expr} {Φ : Val → IProp GF} :
+    WP e @ s ; E [{ Φ }] ⊢ WP e @ E ? [{ Φ }] :=
+  stuck_mono Stuckness.le_MaybeStuck
+
+@[rocq_alias twp_mask_mono]
+theorem mask_mono {s : Stuckness} {E₁ E₂} {e : Expr} {Φ : Val → IProp GF}
+    (H : E₁ ⊆ E₂) :
+    WP e @ s ; E₁ [{ Φ }] ⊢ WP e @ s ; E₂ [{ Φ }] :=
+  strong_mono_with (Std.IsPreorder.le_refl _) H fun _ => BI.entails_wand fupd_intro
+
+@[rocq_alias twp_value']
+theorem value' {s : Stuckness} {E} {v : Val} {Φ : Val → IProp GF} :
+    Φ v ⊢ WP (v : Expr) @ s ; E [{ Φ }] := fupd_intro.trans value_fupd'.mpr
+
+@[rocq_alias twp_value]
+theorem value {s : Stuckness} {E} {e : Expr} {v : Val} {Φ : Val → IProp GF} (h : e = v) :
+    Φ v ⊢ WP e @ s ; E [{ Φ }] := h ▸ value'
+
+@[rocq_alias twp_frame_l]
+theorem frame_l {s : Stuckness} {E} {e : Expr} {Φ : Val → IProp GF}
+    {R : IProp GF} :
+    R ∗ WP e @ s ; E [{ Φ }] ⊢ WP e @ s ; E [{ v, R ∗ Φ v }] :=
+  (BI.sep_mono_left (BI.forall_intro fun _ => BI.wand_intro fupd_intro)).trans <|
+    BI.wand_elim_swap (BI.wand_entails (strong_mono (Std.IsPreorder.le_refl _) LawfulSet.subset_refl))
+
+@[rocq_alias twp_frame_r]
+theorem frame_r {s : Stuckness} {E} {e : Expr} {Φ : Val → IProp GF} {R : IProp GF} :
+    WP e @ s ; E [{ Φ }] ∗ R ⊢ WP e @ s ; E [{ v, Φ v ∗ R }] :=
+  BI.sep_comm.mp.trans (frame_l.trans (mono fun _ => BI.sep_comm.mp))
+
+@[rocq_alias twp_wand]
+theorem wand {s : Stuckness} {E} {e : Expr} {Φ Ψ : Val → IProp GF} :
+    WP e @ s ; E [{ Φ }] ⊢
+      (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s ; E [{ Ψ }] :=
+  BI.wand_intro <| frame_r.trans <| mono fun v => (BI.sep_mono_right (BI.forall_elim v)).trans BI.wand_elim_right
+
+@[rocq_alias twp_wand_l]
+theorem wand_l {s : Stuckness} {E} {e : Expr} {Φ Ψ : Val → IProp GF} :
+    (∀ v, Φ v -∗ Ψ v) ∗ WP e @ s ; E [{ Φ }] ⊢ WP e @ s ; E [{ Ψ }] :=
+  BI.wand_elim_swap wand
+
+@[rocq_alias twp_wand_r]
+theorem wand_r {s : Stuckness} {E} {e : Expr} {Φ Ψ : Val → IProp GF} :
+    WP e @ s ; E [{ Φ }] ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ s ; E [{ Ψ }] :=
+  BI.wand_elim wand
+
+@[rocq_alias twp_frame_wand]
+theorem frame_wand {s : Stuckness} {E} {e : Expr} {Φ : Val → IProp GF} {R : IProp GF} :
+    R ⊢ (WP e @ s ; E [{ v, R -∗ Φ v }]) -∗ WP e @ s ; E [{ Φ }] :=
+  BI.wand_intro_left (frame_r.trans (mono fun _ => BI.wand_elim_left))
+
+@[rocq_alias twp_wp]
+theorem to_wp {s : Stuckness} {E} {e : Expr} {Φ : Val → IProp GF} :
+    WP e @ s ; E [{ Φ }] ⊢ WP e @ s ; E {{ Φ }} := by
+  iloeb as IH generalizing %E %e %Φ
+  simp only [(wp_unfold (e := e)).to_eq, (unfold (e := e)).to_eq, wp.pre, pre]
+  cases hval : toVal e
+  case some v => iintro $
+  case none =>
+    iintro H %σ %ns %κ %κs %nt Hσ
+    imod H $$ Hσ with ⟨%Hred, H⟩
+    have Hred' : s.MaybeReducible (e, σ) := by grind
+    iframe %Hred'
+    iintro !> %e₂ %σ₂ %eₜ %Hstep _
+    iapply step_fupdN_intro Std.LawfulSet.empty_subset
+    iintro !>
+    imod H $$ %κ %e₂ %σ₂ %eₜ %Hstep with ⟨%⟨⟩, Hσ, He₂, Hefs⟩
+    simp only [List.nil_append]
+    iframe Hσ
+    isplitl [He₂]
+    · iapply IH $$ He₂
+    · iapply BI.BigSepL.bigSepL_impl $$ Hefs
+      iintro !> %k %ef %Hef !>Hef
+      iapply IH $$ Hef
+
+section ProofMode
+
+open ProofMode
+
+variable {s : Stuckness} {E E₁ E₂ : CoPset} {e : Expr}
+variable {Φ Ψ : Val → IProp GF} {P R : IProp GF}
+
+@[rocq_alias frame_twp]
+instance frameTwp {p : Bool} [H : ∀ v, FrameInstantiateExistDisabled p R (Φ v) (Ψ v)] :
+    Frame p R (WP e @ s ; E [{ Φ }]) (WP e @ s ; E [{ Ψ }]) where
+  frame := frame_l.trans (mono fun v => (H v).frame_instantiatiate_exist_disabled.frame)
+
+-- Iris-Rocq reuses the module-qualified name `is_except_0_wp` here; that alias
+-- is already assigned to partial WP in Lean, so this instance is left unaliased.
+instance isExcept0Twp : IsExcept0 (WP e @ s ; E [{ Φ }]) where
+  is_except0 := (BI.except0_mono fupd_intro).trans (BIFUpdate.except0.trans fupd_twp)
+
+@[rocq_alias elim_modal_fupd_twp]
+instance (priority := default + 10) elimModalFupdTwp p :
+    ElimModal True p io false iprop(|={E}=> P) P (WP e @ s ; E [{ Φ }]) (WP e @ s ; E [{ Φ }]) where
+  elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans (fupd_wand_right.trans fupd_twp)
+
+@[rocq_alias elim_modal_bupd_twp]
+instance elimModalBupdTwp p :
+    ElimModal True p io false iprop(|==> P) P (WP e @ s ; E [{ Φ }]) (WP e @ s ; E [{ Φ }]) where
+  elim_modal := fun ⟨⟩ =>
+    (BI.sep_mono_left (BI.intuitionisticallyIf_mono (BIUpdateFUpdate.fupd_of_bupd (E := E)))).trans
+      (elimModalFupdTwp _ |>.elim_modal ⟨⟩ (io := io))
+
+/-- The same diagnostic as partial WP: changing masks through a non-atomic
+TWP goal requires an explicit leading update. -/
+@[rocq_alias elim_modal_fupd_twp_wrong_mask]
+instance elimModalFupdTwp_wrongMask :
+    ElimModal (PMError "Goal and eliminated modality must have the same mask.
+    Use `iapply twp.fupd_twp; imod (fupd_mask_subseteq E₂)` to adjust the mask of your goal to `E₂`")
+      p io false iprop(|={E₂}=> P) iprop(False)
+      (WP e @ s ; E₁ [{ Φ }]) iprop(False) where
+  elim_modal := nofun
+
+@[rocq_alias elim_modal_fupd_twp_atomic]
+instance elimModalFupdTwpAtomic :
+    ElimModal (Language.Atomic ↑s e) p io false iprop(|={E₁,E₂}=> P) P
+      (WP e @ s ; E₁ [{ Φ }]) (WP e @ s ; E₂ [{ v, |={E₂,E₁}=> Φ v }]) where
+  elim_modal _ := (sep_mono_left intuitionisticallyIf_elim).trans (fupd_wand_right.trans atomic)
+
+@[rocq_alias elim_modal_fupd_twp_atomic_wrong_mask]
+instance elimModalFupdTwpAtomic_wrongMask :
+    ElimModal (PMError "Goal and eliminated modality must have the same mask.
+    Use `iapply twp.fupd_twp; imod (fupd_mask_subseteq E₂)` to adjust the mask of your goal to `E₂`")
+      p io false iprop(|={E₁,E₂}=> P) iprop(False)
+      (WP e @ s ; E₁ [{ Φ }]) iprop(False) where
+  elim_modal := nofun
+
+end ProofMode
+
+end Rules
+end twp
+end
+end Iris
diff --git a/Iris/Iris/Tests.lean b/Iris/Iris/Tests.lean
index ee60cdaff..1e2a4a848 100644
--- a/Iris/Iris/Tests.lean
+++ b/Iris/Iris/Tests.lean
@@ -7,5 +7,6 @@ public import Iris.Tests.InstancesImport
 public import Iris.Tests.Language
 public import Iris.Tests.Notation
 public import Iris.Tests.Tactics
+public import Iris.Tests.TotalWeakestPre
 public import Iris.Tests.Updates
 public import Iris.Tests.WeakestPre
diff --git a/Iris/Iris/Tests/TotalWeakestPre.lean b/Iris/Iris/Tests/TotalWeakestPre.lean
new file mode 100644
index 000000000..25cd8710f
--- /dev/null
+++ b/Iris/Iris/Tests/TotalWeakestPre.lean
@@ -0,0 +1,285 @@
+/-
+Copyright (c) 2026 Marcelo Fornet. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+module
+
+public import Iris.ProgramLogic.TotalAdequacy
+public import Iris.ProgramLogic.TotalEctxLifting
+public import Iris.ProgramLogic.TotalLifting
+public import Iris.Examples.ClosedProofs
+public import Iris.HeapLang.Instances
+
+namespace Iris.Tests.TotalWeakestPre
+
+open Iris BI ProgramLogic ProgramLogic.Language ProgramLogic.Language.Notation
+open Std LawfulSet
+
+/-! A small language for total-correctness tests. -/
+
+inductive Expr where
+  | val : Nat → Expr
+  | tick : Nat → Expr
+  | put : Nat → Expr
+  | branch : Nat → Expr
+  | observe : Expr
+  | stuck : Expr
+deriving DecidableEq, Repr
+
+abbrev Val := Nat
+abbrev State := Nat
+abbrev Obs := Unit
+
+instance : ToVal Expr Val where
+  toVal
+    | .val n => some n
+    | _ => none
+  ofVal := .val
+  coe_of_toVal_eq_some := by grind
+  toVal_coe := by simp
+
+inductive Step : Expr → State → List Obs → Expr → State → List Expr → Prop
+  | tickSucc (n σ) : Step (.tick (n + 1)) σ [] (.tick n) σ []
+  | tickZero (σ) : Step (.tick 0) σ [] (.val 0) σ []
+  | put (n σ) : Step (.put n) σ [] (.val n) n []
+  | branchLeft (n σ) : Step (.branch (n + 1)) σ [] (.branch n) σ []
+  | branchRight (n σ) : Step (.branch (n + 1)) σ [] (.tick n) σ []
+  | branchZero (σ) : Step (.branch 0) σ [] (.val 0) σ []
+  | observe (σ) : Step .observe σ [()] (.val 0) σ []
+
+instance : PrimStep Expr State (List Obs) where
+  primStep
+    | (e₁, σ₁), κ, (e₂, σ₂, efs) => Step e₁ σ₁ κ e₂ σ₂ efs
+
+instance : Language Expr State Obs Val where
+  val_stuck H := by
+    cases H <;> rfl
+
+instance : LanguageNoFork Expr State Obs Val where
+  no_fork H := by
+    cases H <;> rfl
+
+section Proofs
+
+noncomputable abbrev GF := Iris.Examples.ClosedProofs.GF
+
+noncomputable abbrev trivialIrisGS {Expr State Obs Val}
+    [Language Expr State Obs Val] [InvGS_gen .hasNoLC GF] : IrisGS_gen .hasNoLC Expr GF where
+  toStateInterp := ⟨fun _ _ _ _ => iprop(True)⟩
+  numLatersPerStep := fun _ => 0
+  forkPost := fun _ => iprop(True)
+  stateInterp_mono := fun _ _ _ _ => fupd_intro
+
+theorem tick_pureExec (n : Nat) :
+    PureExec True (n + 1) (Expr.tick n) (Expr.val 0) where
+  pureExec _ := Nat.rec (.once {
+      safe σ := ⟨.val 0, σ, [], Step.tickZero σ⟩
+      deterministic | .tickZero _ => ⟨rfl, rfl, rfl, rfl⟩ })
+    (fun n IH => .head {
+      safe σ := ⟨.tick n, σ, [], Step.tickSucc n σ⟩
+      deterministic | .tickSucc _ _ => ⟨rfl, rfl, rfl, rfl⟩ } IH) n
+
+variable [InvGS_gen .hasNoLC GF]
+
+noncomputable local instance testIrisGS : IrisGS_gen .hasNoLC Expr GF :=
+  trivialIrisGS (State := State) (Obs := Obs) (Val := Val)
+
+private noncomputable abbrev eqPost (n : Nat) : Val → IProp GF := fun v => iprop(⌜v = n⌝)
+private abbrev zeroTwpSpec (e : Expr) : Prop := ⊢ WP e @ Stuckness.NotStuck ; ⊤ [{ eqPost 0 }]
+
+theorem tick_twp (n : Nat) : zeroTwpSpec (.tick n) :=
+  (pure_intro rfl).trans (twp.value' (v := 0) (Φ := eqPost 0)) |>.trans (twp_pure_step (tick_pureExec n) trivial)
+
+theorem put_twp (n : Nat) : ⊢ WP (Expr.put n) @ Stuckness.NotStuck ; ⊤ [{ eqPost n }] := by
+  iapply twp_lift_atomic_step_no_fork (e₁ := Expr.put n) rfl
+  iintro %σ %ns %obs %nt _ !>
+  isplit
+  · exact BI.pure_intro ⟨.val n, n, [], Step.put n σ⟩
+  · iintro %κ %e₂ %σ₂ %efs %⟨⟩
+    exact (sep_intro_emp_valid_left (by itrivial) <| sep_intro_emp_valid_left (by itrivial) <| sep_intro_emp_valid_right
+      .rfl (exists_intro_trans n <| (pure_intro ⟨rfl, rfl⟩).trans pure_and.2)).trans fupd_intro
+
+theorem branch_twp (n : Nat) : zeroTwpSpec (.branch n) := by
+  induction n with
+  | zero =>
+      exact (pure_intro rfl).trans (twp.value (Φ := eqPost 0) rfl) |>.trans fupd_intro |>.trans <|
+        twp_lift_pure_det_step_no_fork (e₂ := Expr.val 0) (fun σ => ⟨.val 0, σ, [], Step.branchZero σ⟩)
+          (fun _ _ _ _ _ (.branchZero _) => ⟨rfl, rfl, rfl, rfl⟩)
+  | succ n IH =>
+      iapply twp_lift_step_no_fork (e₁ := Expr.branch (n + 1)) rfl
+      iintro %σ %ns %obs %nt _
+      iapply fupd_mask_intro empty_subset
+      iintro Hclose
+      isplit
+      · exact BI.pure_intro ⟨.branch n, σ, [], Step.branchLeft n σ⟩
+      · iintro %κ %e₂ %σ₂ %efs %⟨⟩
+        all_goals
+          imod Hclose with -
+          exact (BI.sep_intro_emp_valid_left (BI.pure_intro rfl) <| BI.sep_intro_emp_valid_left (BI.pure_intro rfl) <|
+            BI.sep_intro_emp_valid_right .rfl (by first | exact IH | exact tick_twp n)).trans fupd_intro
+
+omit [InvGS_gen .hasNoLC GF] in
+private theorem stronglyNormalizing_of_twp {Expr State Obs Val}
+    [Language Expr State Obs Val] {e : Expr} {initialState : State} {Φ : Val → IProp GF}
+    (Hwp : ∀ [InvGS_gen .hasNoLC GF],
+      let _ : IrisGS_gen .hasNoLC Expr GF :=
+        trivialIrisGS (State := State) (Obs := Obs) (Val := Val);
+      ⊢ WP e @ Stuckness.NotStuck ; ⊤ [{ Φ }]) :
+    StronglyNormalizing
+      (Language.ErasedStep (Expr := Expr) (State := State) (Obs := Obs))
+      ([e], initialState) := by
+  apply twp_total (hlc := .hasNoLC) (GF := GF) Stuckness.NotStuck e initialState Φ 0 0
+  iintro %Hinv !>
+  iexists (fun _ _ _ _ => iprop(True)), (fun _ => 0), (fun _ => iprop(True)), fun _ _ _ _ => fupd_intro
+  exact BI.sep_intro_emp_valid_left BI.true_intro <| BI.wand_intro_left (BI.true_intro.trans Hwp)
+
+end Proofs
+
+section CoreRuleChecks
+
+variable {E : CoPset} {e : Expr} {v : Val}
+variable {Φ : Val → IProp GF} {P Q : IProp GF}
+variable [IrisGS_gen .hasNoLC Expr GF]
+
+example :
+    WP e @ Stuckness.NotStuck ; ⊤ [{ Φ }] ⊢
+      WP e @ Stuckness.NotStuck ; ⊤ {{ Φ }} :=
+  twp.to_wp
+
+example :
+    P ∗ WP e @ Stuckness.NotStuck ; ⊤ [{ Φ }] ⊢
+      WP e @ Stuckness.NotStuck ; ⊤ [{ v, P ∗ Φ v }] :=
+  twp.frame_l
+
+example :
+    WP (id e) @ Stuckness.NotStuck ; ⊤ [{ Φ }] ⊢
+      TotalWp.totalWp Stuckness.NotStuck ⊤ e
+        (fun v : Val => iprop(
+          WP (id (v : Expr)) @ Stuckness.NotStuck ; ⊤ [{ Φ }])) :=
+  twp.bind_inv id
+
+example :
+    TotalWp.totalWp Stuckness.NotStuck ⊤ e
+      (fun v : Val => iprop(
+        WP (id (v : Expr)) @ Stuckness.NotStuck ; ⊤ [{ Φ }])) ⊢
+      WP (id e) @ Stuckness.NotStuck ; ⊤ [{ Φ }] :=
+  twp.bind id
+
+example [inst : Language.IntoVal e v] :
+    P ∗ Φ v ⊢ WP e @ Stuckness.NotStuck ; ⊤ [{ w, P ∗ Φ w }] :=
+  twp.value (Φ := fun w => iprop(P ∗ Φ w)) inst.into_val.symm
+
+/-- error: iframe: cannot frame R 0 -/
+#guard_msgs in
+example (R : Nat → IProp GF) :
+    R 0 ∗ WP e @ Stuckness.NotStuck ; E [{ fun _ => emp }] ⊢
+      WP e @ Stuckness.NotStuck ; E [{ fun _ => iprop(∃ n, R n) }] := by
+  iintro ⟨HR, Hwp⟩
+  iframe HR
+
+example :
+    (|={E}=> P) ∗ (P -∗ WP e @ Stuckness.NotStuck ; E [{ Φ }]) ⊢
+      WP e @ Stuckness.NotStuck ; E [{ Φ }] :=
+  fupd_wand_right.trans twp.fupd_twp
+
+example :
+    (|==> Q) ∗ (Q -∗ WP e @ Stuckness.NotStuck ; E [{ Φ }]) ⊢
+      WP e @ Stuckness.NotStuck ; E [{ Φ }] :=
+  bupd_wand_right.trans (BIUpdateFUpdate.fupd_of_bupd.trans twp.fupd_twp)
+
+end CoreRuleChecks
+
+section HeapLangPureSmoke
+
+open Iris.HeapLang
+
+variable [InvGS_gen .hasNoLC GF]
+
+noncomputable local instance heapIrisGS : IrisGS_gen .hasNoLC Iris.HeapLang.Exp GF :=
+  trivialIrisGS (State := Iris.HeapLang.State) (Obs := Iris.HeapLang.Observation)
+    (Val := Iris.HeapLang.Val)
+
+private noncomputable abbrev addPost : Iris.HeapLang.Val → IProp GF := fun v => iprop(⌜v = hl_val(#3)⌝)
+
+theorem heapLang_add_twp : ⊢ WP hl(#1 + #2) @ Stuckness.NotStuck ; ⊤ [{ addPost }] :=
+  (pure_intro rfl).trans (twp.value' (v := hl_val(#3)) (Φ := addPost)) |>.trans
+    (twp_pure_step Iris.HeapLang.instPureExecBinOp rfl)
+
+end HeapLangPureSmoke
+
+namespace Forking
+
+inductive Expr where
+  | done
+  | fork
+
+abbrev Val := Unit
+abbrev State := Unit
+abbrev Obs := Unit
+
+instance : ToVal Expr Val where
+  toVal
+    | .done => some ()
+    | .fork => none
+  ofVal _ := .done
+  coe_of_toVal_eq_some := by grind
+  toVal_coe := by simp
+
+inductive Step : Expr → State → List Obs → Expr → State → List Expr → Prop
+  | fork : Step .fork () [] .done () [.done]
+
+instance : PrimStep Expr State (List Obs) where
+  primStep
+    | (e₁, σ₁), κ, (e₂, σ₂, efs) => Step e₁ σ₁ κ e₂ σ₂ efs
+
+instance : Language Expr State Obs Val where
+  val_stuck | .fork => rfl
+
+section
+
+variable [InvGS_gen .hasNoLC GF]
+
+noncomputable local instance forkIrisGS : IrisGS_gen .hasNoLC Expr GF :=
+  trivialIrisGS (State := State) (Obs := Obs) (Val := Val)
+
+theorem fork_twp :
+    ⊢ WP Expr.fork @ Stuckness.NotStuck ; ⊤ [{
+      fun _ : Val => (iprop(True) : IProp GF) }] := by
+  iapply twp_lift_atomic_step (e₁ := Expr.fork) rfl
+  iintro %⟨⟩ %ns %obs %nt _ !>
+  isplit
+  · exact BI.pure_intro ⟨.done, (), [.done], Step.fork⟩
+  · iintro %κ %e₂ %σ₂ %efs %⟨⟩
+    exact (sep_intro_emp_valid_left (PROP := IProp GF) (pure_intro rfl) <| sep_intro_emp_valid_right .rfl <|
+      sep_intro_emp_valid_left (exists_intro_trans () <| and_intro (pure_intro rfl) true_intro)
+      ((true_intro.trans (twp.value' (v := ()) (Φ := fun _ => iprop(True)))).trans sep_emp.mpr)).trans fupd_intro
+
+end
+
+theorem fork_stronglyNormalizing :
+    StronglyNormalizing
+      (Language.ErasedStep (Expr := Expr) (State := State) (Obs := Obs))
+      ([Expr.fork], ()) :=
+  stronglyNormalizing_of_twp (fun [_] => fork_twp)
+
+end Forking
+
+theorem branch_stronglyNormalizing (n initialState : Nat) :
+    StronglyNormalizing
+      (Language.ErasedStep (Expr := Expr) (State := State) (Obs := Obs))
+      ([Expr.branch n], initialState) :=
+  stronglyNormalizing_of_twp (fun [_] => branch_twp n)
+
+theorem branch_singleMachine_stronglyNormalizing (n initialState : Nat) :
+    StronglyNormalizing
+      (ExprErasedStep (Expr := Expr) (State := State) (Obs := Obs))
+      (Expr.branch n, initialState) :=
+  stronglyNormalizing_expr_of_threadPool (branch_stronglyNormalizing n initialState)
+
+theorem put_stronglyNormalizing (n initialState : Nat) :
+    StronglyNormalizing
+      (Language.ErasedStep (Expr := Expr) (State := State) (Obs := Obs))
+      ([Expr.put n], initialState) :=
+  stronglyNormalizing_of_twp (fun [_] => put_twp n)
+
+end Iris.Tests.TotalWeakestPre
diff --git a/Iris/Iris/Tests/WeakestPre.lean b/Iris/Iris/Tests/WeakestPre.lean
index f4c06e08d..71003436c 100644
--- a/Iris/Iris/Tests/WeakestPre.lean
+++ b/Iris/Iris/Tests/WeakestPre.lean
@@ -192,6 +192,56 @@ variable (P Q : PROP)
 
 end TestTexanTriple
 
+section TestTotalTexanTriple
+
+variable (PROP Expr Val A : Type _) [BI PROP]
+variable [TotalWp PROP Expr Val A] [TotalWp PROP Expr Val Stuckness]
+variable (e : Expr) (s : A) (E : CoPset) (P Q : PROP) (v : Val)
+
+/-- info: ⊢ ∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e @ s ; E [{ Φ }] : Prop -/
+#guard_msgs in #check [{ P }] e @ s ; E [{ RET v; Q }]
+
+/-- info: ⊢ ∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e @ E [{ Φ }] : Prop -/
+#guard_msgs in #check [{ P }] e @ E [{ RET v; Q }]
+
+/-- info: ⊢ ∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e @ E ? [{ Φ }] : Prop -/
+#guard_msgs in #check [{ P }] e @ E ? [{ RET v; Q }]
+
+/-- info: ⊢ ∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e [{ Φ }] : Prop -/
+#guard_msgs in #check [{ P }] e [{ RET v; Q }]
+
+/-- info: ⊢ ∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e ? [{ Φ }] : Prop -/
+#guard_msgs in #check [{ P }] e ? [{ RET v; Q }]
+
+/-- info: ⊢ ∀ Φ, P -∗ (∀ x, Q -∗ Φ x) -∗ WP e [{ Φ }] : Prop -/
+#guard_msgs in #check [{ P }] e [{ (x : Val), RET x; Q }]
+
+/-- info: ⊢ ∀ Φ, P -∗ (∀ x, Q -∗ Φ v) -∗ WP e [{ Φ }] : Prop -/
+#guard_msgs in #check [{ P }] e [{ _, RET v; Q }]
+
+/-- info: iprop(□ ∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e @ s ; E [{ Φ }] ) : PROP -/
+#guard_msgs in #check iprop([{ P }] e @ s ; E [{ RET v; Q }])
+
+/-- info: iprop(□ ∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e @ E [{ Φ }] ) : PROP -/
+#guard_msgs in #check iprop([{ P }] e @ E [{ RET v; Q }])
+
+/-- info: iprop(□ ∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e @ E ? [{ Φ }] ) : PROP -/
+#guard_msgs in #check iprop([{ P }] e @ E ? [{ RET v; Q }])
+
+/-- info: iprop(□ ∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e [{ Φ }] ) : PROP -/
+#guard_msgs in #check iprop([{ P }] e [{ RET v; Q }])
+
+/-- info: iprop(□ ∀ Φ, P -∗ (Q -∗ Φ v) -∗ WP e ? [{ Φ }] ) : PROP -/
+#guard_msgs in #check iprop([{ P }] e ? [{ RET v; Q }])
+
+/-- info: iprop(□ ∀ Φ, P -∗ (∀ x, Q -∗ Φ x) -∗ WP e [{ Φ }] ) : PROP -/
+#guard_msgs in #check iprop([{ P }] e [{ (x : Val), RET x; Q }])
+
+/-- info: iprop(□ ∀ Φ, P -∗ (∀ x, Q -∗ Φ v) -∗ WP e [{ Φ }] ) : PROP -/
+#guard_msgs in #check iprop([{ P }] e [{ _, RET v; Q }])
+
+end TestTotalTexanTriple
+
 section HeapLangTestWP
 set_option linter.unusedVariables false
 
@@ -287,4 +337,3 @@ info: iprop(□ ∀ Φ, P -∗ (▷ ∀ x, Q -∗ Φ x) -∗ WP hl(if (#1 < #2)
 #guard_msgs in #check iprop({{ P }} hl(#1) {{ v, RET v; ⌜v = hl_val(#1)⌝ }} : PROP)
 
 end HeapLangTestTexanTriple
-