diff --git a/Iris/Iris/Algebra/COFESolver.lean b/Iris/Iris/Algebra/COFESolver.lean
index 5706bb01d..be95a29e9 100644
--- a/Iris/Iris/Algebra/COFESolver.lean
+++ b/Iris/Iris/Algebra/COFESolver.lean
@@ -278,14 +278,16 @@ def Tower.isoAux : OFE.Iso (F (Tower F) (Tower F)) (Tower F) where
     refine ((map_comp _ _ _ _ _).trans
       (congrArg (fun a => (map ..) a) (map_comp _ _ _ _ _))).symm.dist.trans ?_
     refine .trans (y := map (upN F n) (downN F n) (X (k+n+1))) ?_ ?_
-    · refine map_ne.ne (fun Y => ?_) (fun Y => ?_) _
-      · simp [Hom.comp, Tower.embed, Tower.proj, embed, (by omega : k ≤ k+n+1)]
+    · refine (map_ne.eqv (OFE.eq_dist.mpr fun m' Y => ?_) (OFE.eq_dist.mpr fun m' Y => ?_)).dist _
+      · show (down F (k+n)).f ((embed : A F k -n> A F (k+n+1)).f Y) ≡{m'}≡ (upN F n).f Y
+        simp only [embed, dif_pos (show k ≤ k+n+1 by omega), Hom.comp]
         have {a e} : down F (k + n) (eqToHom e (upN F a Y)) = upN F n Y := by
-          cases Nat.add_left_cancel (k := n+1) e; exact down_up _
+          cases Nat.add_left_cancel (k := n+1) e; exact (down_up _)
         exact this.dist
-      · simp [Hom.comp, Tower.embed, Tower.proj, embed, show ¬k+n+1 ≤ k by omega]
+      · show (embed : A F (k+n+1) -n> A F k).f ((up F (k+n)).f Y) ≡{m'}≡ (downN F n).f Y
+        simp only [embed, dif_neg (show ¬k+n+1 ≤ k by omega), Hom.comp, Function.comp_apply]
         have {a e} : downN F a (eqToHom e (up F (k + n) Y)) = downN F n Y := by
-          cases Nat.add_left_cancel (m := n+1) e; exact congrArg (fun a => (downN ..) a) (down_up _)
+          cases Nat.add_left_cancel (m := n+1) e; exact (downN ..).ne.eqv (down_up _)
         exact this.dist
     · have e : k+n+1 = k+1+n := by omega
       suffices ∀ x y, eqToHom e x = y → ∀ m, map (upN F n) (downN F n) x ≡{m}≡ downN F n y by
diff --git a/Iris/Iris/Algebra/OFE.lean b/Iris/Iris/Algebra/OFE.lean
index 82175557a..f1adc8f27 100644
--- a/Iris/Iris/Algebra/OFE.lean
+++ b/Iris/Iris/Algebra/OFE.lean
@@ -71,12 +71,20 @@ theorem NonExpansive.comp [OFE α] [OFE β] [OFE γ] {g : β → γ} {f : α →
 
 #rocq_ignore ne_proper "OFE is Leibniz; use equality"
 
+/-- A non-expansive function respects equivalence. As OFE is Leibniz, this is congruence. -/
+theorem NonExpansive.eqv [OFE α] [OFE β] {f : α → β} (_ : NonExpansive f) {x y : α}
+    (h : x = y) : f x = f y := h ▸ rfl
+
 /-- A function `f : α → β → γ` is non-expansive if it preserves `n`-equivalence in each argument. -/
 class NonExpansive₂ [OFE α] [OFE β] [OFE γ] (f : α → β → γ) where
   ne : ∀ ⦃n x₁ x₂⦄, x₁ ≡{n}≡ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → f x₁ y₁ ≡{n}≡ f x₂ y₂
 
 #rocq_ignore ne_proper_2 "OFE is Leibniz; use equality"
 
+/-- A binary non-expansive function respects equivalence. As OFE is Leibniz, this is congruence. -/
+theorem NonExpansive₂.eqv [OFE α] [OFE β] [OFE γ] {f : α → β → γ} (_ : NonExpansive₂ f)
+    {x₁ x₂ : α} (hx : x₁ = x₂) {y₁ y₂ : β} (hy : y₁ = y₂) : f x₁ y₁ = f x₂ y₂ := hx ▸ hy ▸ rfl
+
 /-- Note: Not an instance, for symmetry with NonExpansive₂.ne_left, which cannot be an instance. -/
 theorem NonExpansive₂.ne_right [OFE α] [OFE β] [OFE γ] (f : α → β → γ) [NonExpansive₂ f]
     (a : α) : NonExpansive (f a) :=
diff --git a/Iris/Iris/HeapLang/Nonbranching.lean b/Iris/Iris/HeapLang/Nonbranching.lean
new file mode 100644
index 000000000..08b5911ca
--- /dev/null
+++ b/Iris/Iris/HeapLang/Nonbranching.lean
@@ -0,0 +1,304 @@
+module
+
+public import Iris.HeapLang.Instances
+public import Iris.HeapLang.Completeness
+public import Iris.ProgramLogic.Adequacy
+public import Iris.ProgramLogic.Nonbranching
+public import Std.Internal.Do.WP.Basic
+
+@[expose] public section
+namespace Iris.HeapLang
+
+open ProgramLogic PrimStep Language Language.Notation Lean.Order
+
+/-! ## Nonbranching weakest precondition for Pure HeapLang
+
+This file constructs an alternative weakest precondition for the fork-free fragment of HeapLang.
+
+The weakest precondition satisfies two important properties:
+- It is an instance of the HeapLang axiomatic semantics (`AxSem.lean`)
+- It is proven sound: any proof of `wp` implies an analagous `AdequateNoFork` statement.
+
+This weakest precondition serves to connect the automated proofs carried out against the HeapLang
+axiomatic semantics to the manual proofs carried out in Iris.
+-/
+
+
+section Iris
+
+open Iris ProgramLogic Iris.BI Language Language.Notation PrimStep Iris.Std Nonbranching
+
+variable {hlc : HasLC} {GF : BundledGFunctors} [HeapLangGS hlc GF] [CInvG GF]
+variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] [GhostMapG GF Nat Exp H]
+
+include H in
+/-- Iris external proof rule for interfacing with `Std.do`.
+
+This rule discharges a proof obligation for a nonbranching HeapLang program stated with the
+nonbranching `wp` weakest precondition by turning it into a HeapLang Iris `WP`, via the HeapLang
+completeness endpoint `heap_lang_sem_completeness_nofork`. The initial `heapInv σ` is consumed
+as a premise (exactly as the completeness endpoint requires it).
+
+NOTE: This is not the most expressive rule possible. For example, both `wp` and the completeness
+theorem support state, however the formulation of stateful weakest preconditions is under active
+development in `Std.do` as of Lean 4.32.2.
+-/
+theorem wp_external_pure (e : Exp) (σ : State) (Φ : Val → Prop)
+    (hwp : Nonbranching.wp e σ (fun v _ => Φ v)) :
+    ⊢@{IProp GF} heapInv σ -∗
+      Wp.wp (PROP := IProp GF) Stuckness.NotStuck ⊤ e (fun v => BIBase.pure (Φ v)) := by
+  iintro Hheap
+  ihave Hcomplete := heap_lang_sem_completeness_nofork e σ (fun v _ => Φ v)
+    (wp_adequateNoFork hwp) $$ Hheap
+  iapply wp_wand $$ Hcomplete
+  iintro %v ⟨%_, _, _⟩
+  iframe
+
+end Iris
+
+/-! ## Axiomatic semantics instance for the nonbranching `wp`
+
+The pure value-level stepping rules for HeapLang (each an instance of the generic
+`Nonbranching.wp_lift_step` with the relevant `BaseStep` inverted), packaged into an
+instance of `HeapLangAxioms` (moved here from `AxSem.lean`). -/
+
+namespace Nonbranching
+
+open ProgramLogic EctxLanguage
+
+/-- The nonbranching weakest precondition, specialized (monomorphic) to HeapLang.
+Keeping the type arguments fixed lets dotted notation like `.if`/`.load` resolve. -/
+abbrev owp : Exp → State → (Val → State → Prop) → Prop := Nonbranching.wp
+
+/-! ### Pure value-level stepping rules -/
+
+/-- Bind over an evaluation context `fill K`. -/
+theorem wp_bind_fill (K : List ECtxItem) {e σ Q}
+    (hwp : owp e σ (fun v σ' => owp (ProgramLogic.fill K (Exp.ofVal v)) σ' Q)) :
+    owp (ProgramLogic.fill K e) σ Q :=
+  Nonbranching.wp_bind (K := ProgramLogic.fill K) hwp
+
+/-- `if #true then e₁ else e₂` reduces to `e₁`. -/
+theorem wp_if_true {e₁ e₂ : Exp} {σ Q} (hQ : owp e₁ σ Q) :
+    owp (.if (.ofVal (.lit (.bool true))) e₁ e₂) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.if (.ofVal (.lit (.bool true))) e₁ e₂, σ) :=
+    ⟨[], _, _, _, BaseStep.ifTrueS e₁ e₂ σ⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | ifTrueS => exact ⟨rfl, hQ⟩
+
+/-- `if #false then e₁ else e₂` reduces to `e₂`. -/
+theorem wp_if_false {e₁ e₂ : Exp} {σ Q} (hQ : owp e₂ σ Q) :
+    owp (.if (.ofVal (.lit (.bool false))) e₁ e₂) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.if (.ofVal (.lit (.bool false))) e₁ e₂, σ) :=
+    ⟨[], _, _, _, BaseStep.ifFalseS e₁ e₂ σ⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | ifFalseS => exact ⟨rfl, hQ⟩
+
+/-- β-reduction: applying a recursive closure substitutes both binders. -/
+theorem wp_beta {f x : Binder} {e1 : Exp} {v2 : Val} {σ Q}
+    (hQ : owp ((e1.subst f (.rec_ f x e1)).subst x v2) σ Q) :
+    owp (.app (.ofVal (.rec_ f x e1)) (.ofVal v2)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.app (.ofVal (.rec_ f x e1)) (.ofVal v2), σ) :=
+    ⟨[], _, _, _, BaseStep.betaS f x e1 v2 _ σ rfl⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | betaS _ _ _ _ _ _ heq => subst heq; exact ⟨rfl, hQ⟩
+
+/-- Recursive closures evaluate to themselves as values. -/
+theorem wp_rec {f x : Binder} {e : Exp} {σ Q}
+    (hQ : Q (.rec_ f x e) σ) : owp (.rec_ f x e) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.rec_ f x e, σ) := ⟨[], _, _, _, BaseStep.recS f x e σ⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | recS _ _ _ _ => exact ⟨rfl, Nonbranching.wp_val.mpr hQ⟩
+
+/-- Unary operator evaluation. -/
+theorem wp_unop {op : UnOp} {v v' : Val} {σ Q}
+    (hop : op.eval v = some v') (hQ : Q v' σ) : owp (.unop op (.ofVal v)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.unop op (.ofVal v), σ) :=
+    ⟨[], _, _, _, BaseStep.unOpS op v v' σ hop⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with
+  | unOpS _ _ v'' _ hop' => rw [hop'] at hop; cases hop; exact ⟨rfl, Nonbranching.wp_val.mpr hQ⟩
+
+/-- Binary operator evaluation. -/
+theorem wp_binop {op : BinOp} {v1 v2 v' : Val} {σ Q}
+    (hop : op.eval v1 v2 = some v') (hQ : Q v' σ) :
+    owp (.binop op (.ofVal v1) (.ofVal v2)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.binop op (.ofVal v1) (.ofVal v2), σ) :=
+    ⟨[], _, _, _, BaseStep.binOpS op v1 v2 v' σ hop⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with
+  | binOpS _ _ _ v'' _ hop' => rw [hop'] at hop; cases hop; exact ⟨rfl, Nonbranching.wp_val.mpr hQ⟩
+
+/-- Pairing two values. -/
+theorem wp_pair {v1 v2 : Val} {σ Q} (hQ : Q (.pair v1 v2) σ) :
+    owp (.pair (.ofVal v1) (.ofVal v2)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.pair (.ofVal v1) (.ofVal v2), σ) :=
+    ⟨[], _, _, _, BaseStep.pairS v1 v2 σ⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | pairS _ _ _ => exact ⟨rfl, Nonbranching.wp_val.mpr hQ⟩
+
+/-- First projection. -/
+theorem wp_fst {v1 v2 : Val} {σ Q} (hQ : Q v1 σ) :
+    owp (.fst (.ofVal (.pair v1 v2))) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.fst (.ofVal (.pair v1 v2)), σ) :=
+    ⟨[], _, _, _, BaseStep.fstS v1 v2 σ⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | fstS _ _ _ => exact ⟨rfl, Nonbranching.wp_val.mpr hQ⟩
+
+/-- Second projection. -/
+theorem wp_snd {v1 v2 : Val} {σ Q} (hQ : Q v2 σ) :
+    owp (.snd (.ofVal (.pair v1 v2))) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.snd (.ofVal (.pair v1 v2)), σ) :=
+    ⟨[], _, _, _, BaseStep.sndS v1 v2 σ⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | sndS _ _ _ => exact ⟨rfl, Nonbranching.wp_val.mpr hQ⟩
+
+/-- Left injection. -/
+theorem wp_injL {v : Val} {σ Q} (hQ : Q (.injL v) σ) : owp (.injL (.ofVal v)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.injL (.ofVal v), σ) := ⟨[], _, _, _, BaseStep.injLS v σ⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | injLS _ _ => exact ⟨rfl, Nonbranching.wp_val.mpr hQ⟩
+
+/-- Right injection. -/
+theorem wp_injR {v : Val} {σ Q} (hQ : Q (.injR v) σ) : owp (.injR (.ofVal v)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.injR (.ofVal v), σ) := ⟨[], _, _, _, BaseStep.injRS v σ⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | injRS _ _ => exact ⟨rfl, Nonbranching.wp_val.mpr hQ⟩
+
+/-- `case` on a left injection takes the left branch (applied to the payload). -/
+theorem wp_case_injL {v : Val} {e1 e2 σ Q} (hQ : owp (.app e1 (.ofVal v)) σ Q) :
+    owp (.case (.ofVal (.injL v)) e1 e2) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.case (.ofVal (.injL v)) e1 e2, σ) :=
+    ⟨[], _, _, _, BaseStep.caseLS v e1 e2 σ⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | caseLS _ _ _ _ => exact ⟨rfl, hQ⟩
+
+/-- `case` on a right injection takes the right branch (applied to the payload). -/
+theorem wp_case_injR {v : Val} {e1 e2 σ Q} (hQ : owp (.app e2 (.ofVal v)) σ Q) :
+    owp (.case (.ofVal (.injR v)) e1 e2) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.case (.ofVal (.injR v)) e1 e2, σ) :=
+    ⟨[], _, _, _, BaseStep.caseRS v e1 e2 σ⟩
+  refine Nonbranching.wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with | caseRS _ _ _ _ => exact ⟨rfl, hQ⟩
+
+end Nonbranching
+
+/-! ## The HeapLang axiomatic semantics (moved from `AxSem.lean`) -/
+
+namespace Ax
+
+/-- A state-passing weakest precondition `wp e σ Φ` (postcondition `Φ : Val → State → Prop`
+sees the reached state) modelling the pure fragment of HeapLang. The reached state threads
+through each rule's continuation, so no state quantification is needed. -/
+class HeapLangAxioms (wp : Exp → State → (Val → State → Prop) → Prop) where
+  wp_mono : (∀ v σ, Φ v σ → Ψ v σ) → wp e σ Φ → wp e σ Ψ
+  wp_val : Φ v σ → wp (Exp.ofVal v) σ Φ
+  wp_closure : Φ (.rec_ f x e) σ → wp (Exp.rec_ f x e) σ Φ
+  wp_app :
+    wp e₂ σ (fun v₂ σ' => wp e₁ σ' (fun vf σ'' => ∃ f x body, vf = Val.rec_ f x body ∧
+      wp ((body.subst f (.rec_ f x body)).subst x v₂) σ'' Φ)) →
+    wp (Exp.app e₁ e₂) σ Φ
+  wp_unop :
+    wp e σ (fun v σ' => ∃ v', op.eval v = some v' ∧ Φ v' σ') →
+    wp (Exp.unop op e) σ Φ
+  wp_binop :
+    wp e₂ σ (fun v₂ σ' => wp e₁ σ' (fun v₁ σ'' => ∃ v', op.eval v₁ v₂ = some v' ∧ Φ v' σ'')) →
+    wp (Exp.binop op e₁ e₂) σ Φ
+  wp_cond :
+    wp e₀ σ (fun vc σ' => ∃ b, vc = Val.lit (.bool b) ∧ wp (if b then e₁ else e₂) σ' Φ) →
+    wp (Exp.if e₀ e₁ e₂) σ Φ
+  wp_pair :
+    wp e₂ σ (fun v₂ σ' => wp e₁ σ' (fun v₁ σ'' => Φ (Val.pair v₁ v₂) σ'')) →
+    wp (Exp.pair e₁ e₂) σ Φ
+  wp_fst : wp e σ (fun v σ' => ∃ v₁ v₂, v = Val.pair v₁ v₂ ∧ Φ v₁ σ') → wp (Exp.fst e) σ Φ
+  wp_snd : wp e σ (fun v σ' => ∃ v₁ v₂, v = Val.pair v₁ v₂ ∧ Φ v₂ σ') → wp (Exp.snd e) σ Φ
+  wp_injL : wp e σ (fun v σ' => Φ (Val.injL v) σ') → wp (Exp.injL e) σ Φ
+  wp_injR : wp e σ (fun v σ' => Φ (Val.injR v) σ') → wp (Exp.injR e) σ Φ
+  wp_case :
+    wp e₀ σ (fun vc σ' =>
+      (∃ v, vc = Val.injL v ∧ wp (Exp.app e₁ (Exp.ofVal v)) σ' Φ) ∨
+      (∃ v, vc = Val.injR v ∧ wp (Exp.app e₂ (Exp.ofVal v)) σ' Φ)) →
+    wp (Exp.case e₀ e₁ e₂) σ Φ
+  wp_bind (K : ECtxItem) :
+    wp e σ (fun v σ' => wp (K.fill (Exp.ofVal v)) σ' Φ) → wp (K.fill e) σ Φ
+
+/-- The nonbranching `wp` is a model of the HeapLang axiomatic semantics: the state-passing
+postcondition lets the reached state thread through each rule directly, with no state
+quantification. -/
+instance : HeapLangAxioms Nonbranching.owp where
+  wp_mono h H := Nonbranching.wp_mono h H
+  wp_val h := Nonbranching.wp_val.mpr h
+  wp_closure h := Nonbranching.wp_rec h
+  wp_bind K H := Nonbranching.wp_bind_fill [K] H
+  wp_unop {e σ op Φ} H :=
+    Nonbranching.wp_bind_fill [.unOp op]
+      (Nonbranching.wp_mono (fun v σ' hv => hv.elim fun v' hop => Nonbranching.wp_unop hop.1 hop.2) H)
+  wp_binop {e₂ σ e₁ op Φ} H :=
+    Nonbranching.wp_bind_fill [.binOpR op e₁]
+      (Nonbranching.wp_mono (fun v₂ σ' H₂ =>
+        Nonbranching.wp_bind_fill [.binOpL op v₂]
+          (Nonbranching.wp_mono (fun v₁ σ'' hv => hv.elim fun v' hop =>
+            Nonbranching.wp_binop hop.1 hop.2) H₂)) H)
+  wp_pair {e₂ σ e₁ Φ} H :=
+    Nonbranching.wp_bind_fill [.pairR e₁]
+      (Nonbranching.wp_mono (fun v₂ σ' H₂ =>
+        Nonbranching.wp_bind_fill [.pairL v₂]
+          (Nonbranching.wp_mono (fun v₁ σ'' hΦ => Nonbranching.wp_pair hΦ) H₂)) H)
+  wp_app {e₂ σ e₁ Φ} H := by
+    refine Nonbranching.wp_bind_fill [.appR e₁] (Nonbranching.wp_mono (fun v₂ σ' H₂ => ?_) H)
+    refine Nonbranching.wp_bind_fill [.appL v₂] (Nonbranching.wp_mono (fun vf σ'' hvf => ?_) H₂)
+    obtain ⟨f, x, body, rfl, Hbody⟩ := hvf
+    exact Nonbranching.wp_beta Hbody
+  wp_cond {e₀ σ e₁ e₂ Φ} H := by
+    refine Nonbranching.wp_bind_fill [.if e₁ e₂] (Nonbranching.wp_mono (fun vc σ' hvc => ?_) H)
+    obtain ⟨b, rfl, Hb⟩ := hvc
+    cases b
+    · exact Nonbranching.wp_if_false Hb
+    · exact Nonbranching.wp_if_true Hb
+  wp_fst {e σ Φ} H := by
+    refine Nonbranching.wp_bind_fill [.fst] (Nonbranching.wp_mono (fun v σ' hv => ?_) H)
+    obtain ⟨v₁, v₂, rfl, hΦ⟩ := hv
+    exact Nonbranching.wp_fst hΦ
+  wp_snd {e σ Φ} H := by
+    refine Nonbranching.wp_bind_fill [.snd] (Nonbranching.wp_mono (fun v σ' hv => ?_) H)
+    obtain ⟨v₁, v₂, rfl, hΦ⟩ := hv
+    exact Nonbranching.wp_snd hΦ
+  wp_injL {e σ Φ} H :=
+    Nonbranching.wp_bind_fill [.injL] (Nonbranching.wp_mono (fun v σ' hΦ => Nonbranching.wp_injL hΦ) H)
+  wp_injR {e σ Φ} H :=
+    Nonbranching.wp_bind_fill [.injR] (Nonbranching.wp_mono (fun v σ' hΦ => Nonbranching.wp_injR hΦ) H)
+  wp_case {e₀ σ e₁ Φ e₂} H := by
+    refine Nonbranching.wp_bind_fill [.case e₁ e₂] (Nonbranching.wp_mono (fun vc σ' hvc => ?_) H)
+    rcases hvc with ⟨v, rfl, Hv⟩ | ⟨v, rfl, Hv⟩
+    · exact Nonbranching.wp_case_injL Hv
+    · exact Nonbranching.wp_case_injR Hv
+
+end Ax
+
+end Iris.HeapLang
diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean
index c70d83395..574c5c864 100644
--- a/Iris/Iris/Instances/IProp/Instance.lean
+++ b/Iris/Iris/Instances/IProp/Instance.lean
@@ -173,14 +173,16 @@ theorem IProp.unfoldi_foldi (x : FF.api τ (IPre FF)) : unfoldi (foldi x) = x :=
   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]
+  apply OFunctor.map_ne.ne <;> intro _ <;> simp only [IProp.unfold, IProp.fold] <;>
+    first | exact OFE.Iso.hom_inv_dist _ | exact OFE.Iso.inv_hom_dist _
 
 @[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]
+  apply OFunctor.map_ne.ne <;> intro _ <;> simp only [IProp.unfold, IProp.fold] <;>
+    first | exact OFE.Iso.hom_inv_dist _ | exact OFE.Iso.inv_hom_dist _
 
 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/Nonbranching.lean b/Iris/Iris/ProgramLogic/Nonbranching.lean
new file mode 100644
index 000000000..9ca8c8a6d
--- /dev/null
+++ b/Iris/Iris/ProgramLogic/Nonbranching.lean
@@ -0,0 +1,162 @@
+/-
+Copyright (c) 2026 Markus de Medeiros. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+module
+
+public import Iris.Std.GreatestFixpoint
+public import Iris.Std.PartialMap
+public import Iris.ProgramLogic.Language
+public import Iris.ProgramLogic.Adequacy
+public import Iris.ProgramLogic.AbstractLangCompleteness
+public import Std.Internal.Do.WP.Basic
+public import Std.Internal.Do.ExceptPost
+
+namespace Nonbranching
+
+section wp
+public section
+
+open Iris ProgramLogic Language.Notation PrimStep Lean.Order Std.Internal.Do
+
+variable {Exp Val State Obs : Type _} [Language Exp State Obs Val]
+
+abbrev WPArg := Exp → State → (Val → State → Prop) → Prop
+
+def wpF (r : @WPArg Exp Val State) : @WPArg Exp Val State := fun e σ Φ  =>
+  (∃ v : Val, ToVal.toVal e = some v ∧ Φ v σ) ∨
+  (Reducible (e, σ) ∧
+    ∀ κ e' σ' efs, (e, σ) -<κ>-> (e', σ', efs) → efs = [] ∧ r e' σ' Φ)
+
+/-- A weakest preconditinon for fork-free HeapLang. -/
+noncomputable def wp : @WPArg Exp Val State := gfp wpF
+
+theorem wpF_monotone : monotone (@wpF Exp Val State Obs _) := by
+  intro r1 r2 h e σ Φ hr
+  rcases hr with hv | ⟨hred, hstep⟩
+  · exact .inl hv
+  · refine .inr ⟨hred, fun κ e' σ' efs hs => ?_⟩
+    obtain ⟨hnil, h1⟩ := hstep κ e' σ' efs hs
+    exact ⟨hnil, h _ _ _ h1⟩
+
+theorem wp_unfold : @wp Exp Val State Obs _ = @wpF _ _ _ _ _ wp :=
+  gfp_fix wpF_monotone
+
+/-- Coinduction principle: an invariant closed under `wpF` is below `wp`. -/
+theorem wp_coind (I : WPArg) (h : ∀ e σ Φ, I e σ Φ → wpF I e σ Φ) :
+    ∀ (e : Exp) σ Φ,
+      I e σ Φ → wp e σ Φ := le_gfp (x := I) h
+
+/-- `wp` is monotone in its postcondition. -/
+theorem wp_mono {e : Exp} {σ} {Q Q' : Val → State → Prop}
+    (hQ : ∀ v σ, Q v σ → Q' v σ) (hwp : wp e σ Q) : wp e σ Q' := by
+  refine wp_coind (fun e σ R => ∃ Q, (∀ v σ, Q v σ → R v σ) ∧ wp e σ Q)
+    (fun e σ R ⟨Q, hQR, hwpQ⟩ => ?_) e σ Q' ⟨Q, hQ, hwp⟩
+  rw [wp_unfold] at hwpQ
+  rcases hwpQ with ⟨v, hv, hQv⟩ | ⟨hred, hstep⟩
+  · exact .inl ⟨v, hv, hQR v σ hQv⟩
+  · refine .inr ⟨hred, fun κ e' σ' efs hs => ?_⟩
+    obtain ⟨hnil, hwp'⟩ := hstep κ e' σ' efs hs
+    exact ⟨hnil, Q, hQR, hwp'⟩
+
+theorem wp_lift_step {e : Exp} {σ Q} (hred : Reducible (e, σ))
+    (hcont : ∀ κ e' σ' efs, (e, σ) -<κ>-> (e', σ', efs) → efs = [] ∧ wp e' σ' Q) :
+    wp e σ Q := by rw [wp_unfold]; exact .inr ⟨hred, hcont⟩
+
+theorem wp_bind {K : Exp → Exp} [Language.Context K] {e : Exp} {σ Q}
+    (hwp : wp e σ (fun v σ' => wp (K (ToVal.ofVal v)) σ' Q)) : wp (K e) σ Q := by
+  refine wp_coind
+    (fun a σ Q => wp a σ Q ∨ ∃ e, a = K e ∧ wp e σ (fun v σ' => wp (K (ToVal.ofVal v)) σ' Q))
+    (fun a σ Q hI => ?_) (K e) σ Q (.inr ⟨e, rfl, hwp⟩)
+  rcases hI with hwp | ⟨e, rfl, hwp⟩
+  · rw [wp_unfold] at hwp
+    rcases hwp with hv | ⟨hred, hstep⟩
+    · exact .inl hv
+    · exact .inr ⟨hred, fun κ e' σ' efs hs => (hstep κ e' σ' efs hs).imp id (.inl ·)⟩
+  · rw (occs := .pos [1]) [wp_unfold] at hwp
+    rcases hwp with ⟨v, hv, hcont⟩ | ⟨hred, hstep⟩
+    · obtain rfl : e = ToVal.ofVal v := (ToVal.coe_of_toVal_eq_some hv).symm
+      rw [wp_unfold] at hcont
+      exact hcont.imp id (fun ⟨hr, hs⟩ => ⟨hr, fun κ e' σ' efs hst =>
+        (hs κ e' σ' efs hst).imp id (.inl ·)⟩)
+    · let ⟨obs, e', σ', eₜ, hst⟩ := hred
+      have hKred : Reducible (K e, σ) := ⟨obs, K e', σ', eₜ, Language.Context.primStep_fill hst⟩
+      refine .inr ⟨hKred, fun κ Ke' σ' efs hs => ?_⟩
+      obtain ⟨e', rfl, hes⟩ := Language.Context.primStep_fill_inv
+        (Language.toVal_none_of_reducible hred) hs
+      obtain ⟨hnil, hwp'⟩ := hstep κ e' σ' efs hes
+      exact ⟨hnil, .inr ⟨e', rfl, hwp'⟩⟩
+
+@[simp] theorem wp_val {v : Val} {σ Q} : wp (ToVal.ofVal v : Exp) σ Q ↔ Q v σ := by
+  rw [wp_unfold]
+  constructor
+  · rintro (⟨v', hv', hQ⟩ | ⟨hred, _⟩)
+    · rw [ToVal.toVal_coe] at hv'; cases hv'; exact hQ
+    · grind [Language.toVal_none_of_reducible hred]
+  · exact fun hQ => .inl ⟨v, ToVal.toVal_coe v, hQ⟩
+
+/-- A primitive step without forks lifts to a weakest precondition. -/
+theorem wp_primStep {e : Exp} {σ Φ κ e' σ' efs} (hwp : wp e σ Φ)
+    (hstep : (e, σ) -<κ>-> (e', σ', efs)) : efs = [] ∧ wp e' σ' Φ := by
+  rcases @wp_unfold Exp Val State Obs _ ▸ hwp with (⟨_, hv, _⟩|⟨_, hwp⟩)
+  · simp [Language.val_stuck hstep] at hv
+  · exact hwp _ _ _ _ hstep
+
+theorem wp_notStuck {e : Exp} {σ Q} (hwp : wp e σ Q) : NotStuck (e, σ) := by
+  rcases @wp_unfold Exp Val State Obs _ ▸ hwp with (⟨_, hv, _⟩|⟨hred, _⟩)
+  · simp [NotStuck, hv]
+  · exact .inr hred
+
+theorem wp_erasedStep {e : Exp} {σ Q t' σ'} (hwp : wp e σ Q) (hstep : ([e], σ) -·->ₜₚ (t', σ')) :
+    ∃ e', t' = [e'] ∧ wp e' σ' Q := by
+  obtain ⟨κ, hs⟩ := hstep
+  generalize hρ : ([e], σ) = ρ at hs
+  cases hs with | @atomic e₀ _ _ e' _ efs hbase t₁ t₂ =>
+  obtain ⟨hpool, rfl⟩ := Prod.mk.injEq .. ▸ hρ
+  rcases List.append_eq_cons_iff.mp hpool.symm with ⟨rfl, heq⟩ | ⟨a, _, hcontra⟩
+  · rw [List.nil_append] at hpool
+    cases hpool
+    obtain ⟨rfl, h⟩ := wp_primStep hwp hbase
+    simpa
+  · simp at hcontra
+
+theorem wp_reach {e σ Q} (hwp : wp e σ Q) :
+    ∀ {p : List Exp × State}, ([e], σ) -·->ₜₚ* p → ∃ e', p.1 = [e'] ∧ wp e' p.2 Q := by
+  intro p hp
+  induction hp
+  next => simpa
+  next p' p'' hstep hp ih =>
+    obtain ⟨tq, σq⟩ := p'
+    obtain ⟨e₁, rfl, hwp₁⟩ := ih
+    obtain ⟨tr, σr⟩ := p''
+    exact wp_erasedStep hwp₁ hp
+
+/-- Adequacy: Any closed proof of `wp` implies `AdequateNoFork`. -/
+theorem wp_adequateNoFork {e : Exp} {σ : State} {Q : Val → State → Prop}
+    (hwp : wp e σ Q) : AdequateNoFork .NotStuck e σ Q where
+  no_fork hreach := by
+    obtain ⟨e', hq, _⟩ := wp_reach hwp hreach
+    grind
+  result hreach := by
+    obtain ⟨e', hq, hwp'⟩ := wp_reach hwp hreach
+    rw [wp_unfold] at hwp'
+    rcases hwp' with ⟨_, _, _⟩ | ⟨hred, _⟩
+    · grind
+    · grind [Language.toVal_none_of_reducible hred]
+  not_stuck _ hreach hmem := by
+    obtain ⟨e', hq, hwp'⟩ := wp_reach hwp hreach
+    simp only at hq
+    rw [hq, List.mem_singleton] at hmem
+    subst hmem
+    exact wp_notStuck hwp'
+
+scoped instance instWPPreExp : Std.Internal.Do.WP Exp Val (State → Prop) EPost.Nil where
+  wpTrans e := ⟨fun Q _ σ => wp e σ Q⟩
+  wp_trans_monotone e := by
+    intro post post' _ _ _ hpost
+    exact fun σ h => wp_mono (fun v s => hpost v s) h
+
+end
+end wp
+end Nonbranching
diff --git a/Iris/Iris/Std/GreatestFixpoint.lean b/Iris/Iris/Std/GreatestFixpoint.lean
new file mode 100644
index 000000000..4aba815ba
--- /dev/null
+++ b/Iris/Iris/Std/GreatestFixpoint.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2026 Markus de Medeiros. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus de Medeiros
+-/
+module
+
+@[expose] public section
+
+section gfp
+open Lean.Order PartialOrder CompleteLattice
+
+variable {α} [CompleteLattice α]
+
+noncomputable def gfp (f : α → α) : α := sup (fun x => x ⊑ f x)
+
+theorem le_gfp {f : α → α} {x : α} (h : x ⊑ f x) : x ⊑ gfp f := le_sup _ h
+
+theorem gfp_postfixed {f : α → α} (hm : monotone f) : gfp f ⊑ f (gfp f) := by
+  apply sup_le; intro y hy
+  exact rel_trans hy (hm _ _ (le_sup _ hy))
+
+theorem gfp_fix {f : α → α} (hm : monotone f) : gfp f = f (gfp f) :=
+  rel_antisymm (gfp_postfixed hm) (le_gfp (hm _ _ (gfp_postfixed hm)))
+
+end gfp
diff --git a/Iris/lake-manifest.json b/Iris/lake-manifest.json
index 8f17b358d..859755111 100644
--- a/Iris/lake-manifest.json
+++ b/Iris/lake-manifest.json
@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
+   "rev": "31a49105f960721073a9adfc82b261f5d0f2ce1e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.32.0",
+   "inputRev": "v4.33.0-rc1",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
+   "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.32.0",
+   "inputRev": "v4.33.0-rc1",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "iris",
diff --git a/Iris/lakefile.toml b/Iris/lakefile.toml
index 62ceb86ea..9271b0372 100644
--- a/Iris/lakefile.toml
+++ b/Iris/lakefile.toml
@@ -1,15 +1,18 @@
 name = "iris"
 defaultTargets = ["Iris", "IrisTest"]
 
+[leanOptions]
+linter.ambiguousOpen = false
+
 [[require]]
 name = "Qq"
 scope = "leanprover-community"
-rev = "v4.32.0"
+rev = "v4.33.0-rc1"
 
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-rev = "v4.32.0"
+rev = "v4.33.0-rc1"
 
 [[lean_lib]]
 name = "Iris"
diff --git a/Iris/lean-toolchain b/Iris/lean-toolchain
index 0ec5999cc..fd85b262b 100644
--- a/Iris/lean-toolchain
+++ b/Iris/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.32.2
+leanprover/lean4:v4.33.0-rc1