diff --git a/Iris/Iris/Algebra/COFESolver.lean b/Iris/Iris/Algebra/COFESolver.lean
index 4a3517f8f..726d99df1 100644
--- a/Iris/Iris/Algebra/COFESolver.lean
+++ b/Iris/Iris/Algebra/COFESolver.lean
@@ -276,11 +276,13 @@ def Tower.isoAux : OFE.Iso (F (Tower F) (Tower F)) (Tower F) where
     refine ((map_comp _ _ _ _ _).trans <| (map ..).ne.eqv (map_comp _ _ _ _ _)).symm.trans ?_
     refine .trans (y := map (upN F n) (downN F n) (X (k+n+1))) ?_ ?_
     · refine fun m => map_ne.eqv (fun m' Y => ?_) (fun m' Y => ?_) m _
-      · simp [Hom.comp, Tower.embed, Tower.proj, embed, (by omega : k ≤ k+n+1)]
+      · 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 _)
         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 (downN ..).ne.eqv (down_up _)
         exact this.dist
diff --git a/Iris/Iris/HeapLang/AxSem.lean b/Iris/Iris/HeapLang/AxSem.lean
new file mode 100644
index 000000000..507647800
--- /dev/null
+++ b/Iris/Iris/HeapLang/AxSem.lean
@@ -0,0 +1,193 @@
+module
+
+import Iris.HeapLang.Semantics
+import Std.Tactic.Do
+import Std.Internal.Do
+
+/-! # Axiomatic Semantics for HeapLang -/
+
+set_option mvcgen.warning false
+
+open Lean.Order
+
+namespace Iris.HeapLang.Ax
+
+/-- A predicate `wp` imbues a fragment of HeapLang with the correct axiomatic semantics.
+In particular, `wp` admits proof rules that obey the evaluation order and effects of HeapLang. -/
+class HeapLangAxioms (wp : Exp → (Val → 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₂) Φ
+
+open HeapLangAxioms Std.Internal.Do
+
+/-- Local notation for a Std.Do weakest precondition. -/
+scoped syntax:max "wp⟦" term:min "⟧" ppSpace term:max : term
+scoped macro_rules
+  | `(wp⟦ $e ⟧ $Φ) => `(Std.Internal.Do.wp $e $Φ Std.Internal.Do.EPost.Nil.mk)
+
+set_option synthInstance.checkSynthOrder false in
+instance instWP_HeapLangAxioms {wp} [HeapLangAxioms wp] :
+    Std.Internal.Do.WP Exp Val Prop EPost.Nil where
+  wpTrans e := ⟨fun Φ _ => wp e Φ⟩
+  wp_trans_monotone _ _ _ _ _ _ := wp_mono
+
+section laws
+
+variable {wp} [HeapLangAxioms wp]
+
+@[spec] theorem spec_val {v : Val} {Φ : Val → Prop} :
+    Φ v ⊑ wp⟦(Exp.ofVal v : Exp)⟧ Φ := by
+  intro h; exact wp_val h
+
+@[spec] theorem spec_rec {f x : Binder} {e : Exp} {Φ : Val → Prop} :
+    Φ (.rec_ f x e) ⊑ wp⟦Exp.rec_ f x e⟧ Φ := by
+  intro h; exact wp_closure h
+
+@[spec] theorem spec_app {e₁ e₂ : Exp} {Φ : Val → Prop} :
+    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₂⟧ Φ := by
+  intro h; exact wp_app h
+
+@[spec] theorem spec_unop {op : UnOp} {e : Exp} {Φ : Val → Prop} :
+    wp⟦e⟧ (fun v => ∃ v', op.eval v = some v' ∧ Φ v')
+      ⊑ wp⟦Exp.unop op e⟧ Φ := by
+  intro h; exact wp_unop h
+
+@[spec] theorem spec_binop {op : BinOp} {e₁ e₂ : Exp} {Φ : Val → Prop} :
+    wp⟦e₂⟧ (fun v₂ => wp⟦e₁⟧ (fun v₁ => ∃ v', op.eval v₁ v₂ = some v' ∧ Φ v'))
+      ⊑ wp⟦Exp.binop op e₁ e₂⟧ Φ := by
+  intro h; exact wp_binop h
+
+@[spec] theorem spec_if {e₀ e₁ e₂ : Exp} {Φ : Val → Prop} :
+    wp⟦e₀⟧ (fun vc => ∃ b, vc = Val.lit (.bool b) ∧ wp⟦if b then e₁ else e₂⟧ Φ)
+      ⊑ wp⟦Exp.if e₀ e₁ e₂⟧ Φ := by
+  intro h; exact wp_cond h
+
+@[spec] theorem spec_pair {e₁ e₂ : Exp} {Φ : Val → Prop} :
+    wp⟦e₂⟧ (fun v₂ => wp⟦e₁⟧ (fun v₁ => Φ (Val.pair v₁ v₂)))
+      ⊑ wp⟦Exp.pair e₁ e₂⟧ Φ := by
+  intro h; exact wp_pair h
+
+@[spec] theorem spec_fst {e : Exp} {Φ : Val → Prop} :
+    wp⟦e⟧ (fun v => ∃ v₁ v₂, v = Val.pair v₁ v₂ ∧ Φ v₁)
+      ⊑ wp⟦Exp.fst e⟧ Φ := by
+  intro h; exact wp_fst h
+
+@[spec] theorem spec_snd {e : Exp} {Φ : Val → Prop} :
+    wp⟦e⟧ (fun v => ∃ v₁ v₂, v = Val.pair v₁ v₂ ∧ Φ v₂)
+      ⊑ wp⟦Exp.snd e⟧ Φ := by
+  intro h; exact wp_snd h
+
+@[spec] theorem spec_injL {e : Exp} {Φ : Val → Prop} :
+    wp⟦e⟧ (fun v => Φ (Val.injL v)) ⊑ wp⟦Exp.injL e⟧ Φ := by
+  intro h; exact wp_injL h
+
+@[spec] theorem spec_injR {e : Exp} {Φ : Val → Prop} :
+    wp⟦e⟧ (fun v => Φ (Val.injR v)) ⊑ wp⟦Exp.injR e⟧ Φ := by
+  intro h; exact wp_injR h
+
+@[spec] theorem spec_case {e₀ e₁ e₂ : Exp} {Φ : Val → Prop} :
+    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₂⟧ Φ := by
+  intro h; exact wp_case h
+
+end laws
+
+
+section demos
+
+variable {wp} [HeapLangAxioms wp]
+
+private def lit (n : Int) : Exp := .ofVal (.lit (.int n))
+private def bool (b : Bool) : Exp := .ofVal (.lit (.bool b))
+private def lam (x : String) (e : Exp) : Exp := .rec_ .anon (.named x) e
+private def add (a b : Exp) : Exp := .binop .plus a b
+
+/-- Substituting into a value-expression is the identity. Needed because the
+default simp set normalises `.val` to `.ofVal` (`val_to_ofVal`), so `substStr`'s
+`.val` case cannot fire on a `.ofVal` leaf; this `rfl` lemma bridges the gap while
+keeping the `vcgen`-friendly `.ofVal` form. -/
+@[local simp] private theorem substStr_ofVal (x : String) (v w : Val) :
+    Exp.substStr x v (Exp.ofVal w) = Exp.ofVal w := rfl
+
+/-! ### Values and pure arithmetic -/
+
+example : True ⊑ wp⟦lit 0⟧ (fun _v => True) := by
+  unfold lit; vcgen
+
+example : True ⊑ wp⟦lit 0⟧ (fun v => v = Val.lit (.int 0)) := by
+  unfold lit; vcgen with finish
+
+/-- `(1 + 2) + (3 + 4) = 10`, nested redexes. -/
+example : True ⊑ wp⟦add (add (lit 1) (lit 2)) (add (lit 3) (lit 4))⟧ (fun v => v = Val.lit (.int 10)) := by
+  unfold add lit
+  vcgen <;> (try simp [BinOp.eval]) <;> (try vcgen) <;> (try simp [BinOp.eval])
+
+/-! ### Computed conditions -/
+
+/-- The guard is a comparison, not a literal: `if 1 < 2 then 1 else 2 = 1`. -/
+example : True ⊑ wp⟦Exp.if (.binop .lt (lit 1) (lit 2)) (lit 1) (lit 2)⟧ (fun v => v = Val.lit (.int 1)) := by
+  unfold lit
+  vcgen <;> (try simp [BinOp.eval]) <;> (try vcgen) <;> (try simp [BinOp.eval]) <;>
+    (try vcgen) <;> (try simp [BinOp.eval])
+
+/-! ### Binders (β-reduction)
+
+The workflow: `vcgen until Exp.subst _ _ _` symbolically executes up to the
+substitution redex, `simp [Exp.subst, Exp.substStr]` computes it, then `vcgen`
+resumes on the concrete substituted program. -/
+
+/-- Identity applied to a literal: `(λx. x) 0`. -/
+example : True ⊑ wp⟦Exp.app (lam "x" (.var "x")) (lit 0)⟧ (fun _v => True) := by
+  unfold lam lit
+  vcgen until Exp.subst _ _ _
+  refine ⟨_, _, _, rfl, ?_⟩
+  simp [Exp.subst, Exp.substStr]
+  vcgen
+
+/-- The bound variable is used in an arithmetic context: `(λx. x + 1) 5 = 6`. -/
+example : True ⊑ wp⟦Exp.app (lam "x" (add (.var "x") (lit 1))) (lit 5)⟧ (fun v => v = Val.lit (.int 6)) := by
+  unfold lam add lit
+  vcgen until Exp.subst _ _ _
+  refine ⟨_, _, _, rfl, ?_⟩
+  simp [Exp.subst, Exp.substStr]
+  vcgen <;> (try simp [BinOp.eval]) <;> (try vcgen) <;> (try simp [BinOp.eval])
+
+/-! ### Products and sums -/
+
+/-- `fst (1 + 2, 3 + 4) = 3`. -/
+example : True ⊑ wp⟦Exp.fst (Exp.pair (add (lit 1) (lit 2)) (add (lit 3) (lit 4)))⟧ (fun v => v = Val.lit (.int 3)) := by
+  unfold add lit
+  vcgen <;> (try simp [BinOp.eval]) <;> (try vcgen) <;> (try simp [BinOp.eval])
+
+end demos
+end Iris.HeapLang.Ax
diff --git a/Iris/Iris/HeapLang/Completeness.lean b/Iris/Iris/HeapLang/Completeness.lean
new file mode 100644
index 000000000..7bac3ec41
--- /dev/null
+++ b/Iris/Iris/HeapLang/Completeness.lean
@@ -0,0 +1,668 @@
+/-
+Copyright (c) 2026 Markus de Medeiros. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+module
+
+public import Iris.HeapLang.PrimitiveLaws
+public import Iris.BI.BigOp.BigSepSet
+public import Iris.ProgramLogic.ThreadPool
+public import Iris.ProgramLogic.AbstractWeakestPre
+public import Iris.ProgramLogic.AbstractLangCompleteness
+public import Iris.ProgramLogic.AbstractEctxLangCompleteness
+public import Iris.Instances.Lib.CInvariants
+public import Iris.Instances.Lib.GhostMap
+public import Iris.ProofMode
+
+/-! # HeapLang completeness -/
+
+@[expose] public section
+namespace Iris.HeapLang
+
+open Iris ProgramLogic Iris.BI Language Language.Notation Std
+
+variable {hlc : HasLC} {GF : BundledGFunctors} [HeapLangGS hlc GF]
+
+@[reducible] def heapCellPts (l : Loc) (vo : Option Val) : IProp GF :=
+  match vo with
+  | some _ => iprop(l ↦ vo)
+  | none => iprop(emp)
+
+instance instTimeless_heapCellPts (l : Loc) (vo : Option Val) :
+    Timeless (heapCellPts (GF := GF) l vo) := by
+  cases vo <;> (unfold heapCellPts; infer_instance)
+
+@[reducible] def cellInv (k : Loc) (vo : Option Val) : IProp GF :=
+  iprop(heapCellPts k vo ∗ metaToken k ⊤)
+
+theorem pointsTo_heapCellPts (l : Loc) (vo : Option Val) :
+    (l ↦ vo) ⊢ heapCellPts (GF := GF) l vo := by
+  cases vo with
+  | some v => exact .rfl
+  | none => exact Affine.affine
+
+/-- Predicate which asserts ownership over a complete HeapLang state -/
+@[reducible] def heapInv (σ : State) : IProp GF := iprop%
+    (bigSepM (M := HeapF) (fun l vo => iprop% heapCellPts l vo ∗ metaToken l ⊤) σ.heap) ∗
+    ([∗set] p ∈ σ.usedProphId, ∃ pvs, proph p pvs)
+
+instance instTimeless_heapInv (σ : State) : Timeless (heapInv (GF := GF) σ) := by
+  unfold heapInv; infer_instance
+
+abbrev baseCompletenessGoal (e₁ : Exp) (σ : State) (E : CoPset) : IProp GF := iprop%
+  ((⌜Atomic Atomicity.StronglyAtomic e₁⌝ ∗
+      ∀ (Φ : Val → IProp GF),
+        (▷ ∀ κ v₂ σ' efs, ⌜PrimStep.primStep (e₁, σ) κ (ToVal.ofVal v₂, σ', efs)⌝ ==∗
+          ((heapInv σ' -∗ Φ v₂) ∗
+            [∗list] _i ↦ etp ∈ efs, WP etp @ Stuckness.NotStuck; ⊤ {{ _v, True }})) -∗
+        WP e₁ @ Stuckness.NotStuck; E {{ v, Φ v }}) ∨
+   (heapInv σ ∗
+      ∀ (Φ : Val → IProp GF) (E₂ : CoPset),
+        (▷ ∀ e₂ efs, (∀ σ₁, heapInv σ₁ ={E}=∗
+            ∃ κ σ₁', ⌜PrimSteps e₁ σ₁ κ e₂ σ₁' efs⌝ ∗ heapInv σ₁') ={E₂}=∗
+          WP e₂ @ Stuckness.NotStuck; E₂ {{ v, Φ v }} ∗
+          [∗list] _i ↦ etp ∈ efs, WP etp @ Stuckness.NotStuck; ⊤ {{ _v, True }}) -∗
+        WP e₁ @ Stuckness.NotStuck; E₂ {{ v, Φ v }}))
+
+theorem wp_base_pure {e₁ e₂ : Exp} {φ : Prop} [hpe : Language.PureExec φ 1 e₁ e₂] (hφ : φ)
+    (σ : State) (E : CoPset)
+    (hbase : ∀ σ' : State, BaseStep e₁ σ' [] e₂ σ' []) :
+    heapInv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e₁ σ E) := by
+  iintro Hinv
+  imodintro
+  iright
+  iframe Hinv
+  iintro %Φ %E₂ H
+  iapply wp_pure_step_later (Hexec := hpe) (Hφ := hφ)
+  iintro !> -
+  ihave Htraj : iprop(∀ σ₁, heapInv σ₁ ={E}=∗
+      ∃ κ σ₁', ⌜PrimSteps e₁ σ₁ κ e₂ σ₁' []⌝ ∗ heapInv σ₁') $$ []
+  · iintro %σ₁ Hinv₁
+    imodintro
+    iexists [], σ₁
+    iframe Hinv₁
+    ipureintro
+    exact PrimSteps.once (EctxLanguage.primStep_of_baseStep (hbase σ₁))
+  iapply fupd_wp
+  imod H $$ Htraj with ⟨Hwp, _⟩
+  imodintro
+  iexact Hwp
+
+theorem wp_base_atomic {e₁ : Exp} {v₂ : Val} (l : Loc) (vlive : Val) (vnew : Option Val)
+    (σ : State) (E : CoPset)
+    (hatom : Atomic Atomicity.StronglyAtomic e₁)
+    (hcell : get? (M := HeapF) σ.heap l = some (some vlive))
+    (hbase : ∀ σ'' : State, get? (M := HeapF) σ''.heap l = some (some vlive) →
+        BaseStep e₁ σ'' [] (ToVal.ofVal v₂) (σ''.initHeap l 1 vnew) [])
+    (hdet : ∀ {σ'' : State} {obs e' σ''' efs},
+        get? (M := HeapF) σ''.heap l = some (some vlive) →
+        BaseStep e₁ σ'' obs e' σ''' efs →
+        obs = [] ∧ e' = (ToVal.ofVal v₂ : Exp) ∧ σ''' = σ''.initHeap l 1 vnew ∧ efs = []) :
+    heapInv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e₁ σ E) := by
+  iintro ⟨Hmap, Hproph_inv⟩
+  unfold baseCompletenessGoal
+  imodintro
+  ileft
+  iframe %hatom
+  iintro %Φ Hstep
+  icases (BigSepM.bigSepM_insert_acc (M := HeapF) (Φ := cellInv) hcell) $$ Hmap
+    with ⟨⟨Hpt, Hmeta⟩, Hclose⟩
+  iapply wp_lift_atomic_step (EctxLanguage.val_stuck (hbase σ hcell))
+  iintro %σ₁ %ns %obs %obs' %nt Hσ !>
+  icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩
+  ihave %hcell1 : ⌜get? (M := HeapF) σ₁.heap l = some (some vlive)⌝ $$ [Hσ Hpt]
+  · icases genHeap_valid $$ [$Hσ $Hpt] with >%hh
+    itrivial
+  isplitr
+  · ipureintro
+    simp only [Stuckness.MaybeReducible]
+    exact EctxLanguage.primStep_reducible_of_baseStep_reducible
+      ⟨[], _, _, [], hbase σ₁ hcell1⟩
+  iintro !> %e₂ %σ₂ %eₜ %Hprim Hcr
+  obtain ⟨rfl, rfl, rfl, rfl⟩ :=
+    hdet hcell1 (EctxLanguage.baseStep_of_primStep_of_baseStep_reducible
+      ⟨[], _, _, [], hbase σ₁ hcell1⟩ Hprim)
+  imod genHeap_update (v₂ := vnew) $$ [$Hσ $Hpt] with ⟨Hσ, Hpt⟩
+  imod Hstep $$ [] with ⟨Hpost, _⟩
+  · ipureintro
+    exact EctxLanguage.primStep_of_baseStep (hbase σ hcell)
+  imodintro
+  ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph
+  have hl0 : l + (0 : Int) = l := by
+    cases l
+    simp only [HAdd.hAdd, Loc.mk.injEq]
+    grind
+  simp only [stateInterp, State.initHeap, Int.toNat_one, List.range_one, List.foldl_cons,
+    Int.cast_ofNat_Int, List.foldl_nil, hl0,
+    Algebra.BigOpL.bigOpL_nil]
+  iframe
+  iexists v₂
+  isplit; ipureintro; simp [toVal]; rfl
+  iapply Hpost
+  simp only [heapInv]
+  iframe
+  iapply Hclose
+  unfold cellInv
+  iframe
+  iapply (pointsTo_heapCellPts l vnew); iexact Hpt
+
+theorem wp_base_atomic_nochange {e₁ : Exp} {v₂ : Val} (l : Loc) (vlive : Val)
+    (σ : State) (E : CoPset)
+    (hatom : Atomic Atomicity.StronglyAtomic e₁)
+    (hcell : get? (M := HeapF) σ.heap l = some (some vlive))
+    (hbase : ∀ σ'' : State, get? (M := HeapF) σ''.heap l = some (some vlive) →
+        BaseStep e₁ σ'' [] (ToVal.ofVal v₂) σ'' [])
+    (hdet : ∀ {σ'' : State} {obs e' σ''' efs},
+        get? (M := HeapF) σ''.heap l = some (some vlive) →
+        BaseStep e₁ σ'' obs e' σ''' efs →
+        obs = [] ∧ e' = (ToVal.ofVal v₂ : Exp) ∧ σ''' = σ'' ∧ efs = []) :
+    heapInv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e₁ σ E) := by
+  iintro ⟨Hmap, Hproph_inv⟩
+  unfold baseCompletenessGoal
+  imodintro
+  ileft
+  iframe %hatom
+  iintro %Φ Hstep
+  iapply wp_lift_atomic_step (EctxLanguage.val_stuck (hbase σ hcell))
+  iintro %σ₁ %ns %obs %obs' %nt Hσ !>
+  icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩
+  ihave %hcell1 : ⌜get? (M := HeapF) σ₁.heap l = some (some vlive)⌝ $$ [Hσ Hmap]
+  · icases (BigSepM.bigSepM_lookup_acc (M := HeapF) (Φ := cellInv) hcell).1 $$ Hmap
+      with ⟨⟨Hpt, _⟩, _⟩
+    icases genHeap_valid $$ [$Hσ $Hpt] with >%hh
+    itrivial
+  isplitr
+  · ipureintro
+    simp only [Stuckness.MaybeReducible]
+    exact EctxLanguage.primStep_reducible_of_baseStep_reducible
+      ⟨[], _, _, [], hbase σ₁ hcell1⟩
+  iintro !> %e₂ %σ₂ %eₜ %Hprim Hcr
+  obtain ⟨rfl, rfl, rfl, rfl⟩ :=
+    hdet hcell1 (EctxLanguage.baseStep_of_primStep_of_baseStep_reducible
+      ⟨[], _, _, [], hbase σ₁ hcell1⟩ Hprim)
+  imod Hstep $$ [] with ⟨Hpost, _⟩
+  · ipureintro
+    exact EctxLanguage.primStep_of_baseStep (hbase σ hcell)
+  imodintro
+  ihave Hproph := (prophMapInterp_nil_append obs' σ₂.usedProphId).mp $$ Hproph
+  simp only [stateInterp]
+  iframe
+  iexists v₂
+  isplit; ipureintro; simp [toVal]; rfl
+  iapply Hpost
+  simp only [heapInv]
+  iframe
+
+/-! ### Per-operation determinism facts -/
+
+theorem loadS_det {l : Loc} {v : Val} {σ : State} {obs e' σ' efs}
+    (h : get? (M := HeapF) σ.heap l = some (some v))
+    (hs : BaseStep (.load (.val (.lit (.loc l)))) σ obs e' σ' efs) :
+    obs = [] ∧ e' = (ToVal.ofVal v : Exp) ∧ σ' = σ ∧ efs = [] := by
+  cases hs with | loadS => grind
+
+theorem storeS_det {l : Loc} {w : Val} {σ : State} {obs e' σ' efs}
+    (hs : BaseStep (.store (.val (.lit (.loc l))) (.val w)) σ obs e' σ' efs) :
+    obs = [] ∧ e' = (ToVal.ofVal (Val.lit .unit) : Exp) ∧
+      σ' = σ.initHeap l 1 (some w) ∧ efs = [] := by
+  cases hs with | storeS => grind
+
+theorem freeS_det {l : Loc} {σ : State} {obs e' σ' efs}
+    (hs : BaseStep (.free (.val (.lit (.loc l)))) σ obs e' σ' efs) :
+    obs = [] ∧ e' = (ToVal.ofVal (Val.lit .unit) : Exp) ∧
+      σ' = σ.initHeap l 1 none ∧ efs = [] := by
+  cases hs with | freeS => grind
+
+theorem xchgS_det {l : Loc} {v1 v2 : Val} {σ : State} {obs e' σ' efs}
+    (h : get? (M := HeapF) σ.heap l = some (some v1))
+    (hs : BaseStep (.xchg (.val (.lit (.loc l))) (.val v2)) σ obs e' σ' efs) :
+    obs = [] ∧ e' = (ToVal.ofVal v1 : Exp) ∧ σ' = σ.initHeap l 1 (some v2) ∧ efs = [] := by
+  cases hs with | xchgS => grind
+
+theorem faaS_det {l : Loc} {i1 i2 : Int} {σ : State} {obs e' σ' efs}
+    (h : get? (M := HeapF) σ.heap l = some (some (Val.lit (.int i1))))
+    (hs : BaseStep (.faa (.val (.lit (.loc l))) (.val (.lit (.int i2)))) σ obs e' σ' efs) :
+    obs = [] ∧ e' = (ToVal.ofVal (Val.lit (.int i1)) : Exp) ∧
+      σ' = σ.initHeap l 1 (some (Val.lit (.int (i1 + i2)))) ∧ efs = [] := by
+  cases hs with | faaS => grind
+
+theorem cmpXchgS_det_true {l : Loc} {v1 v2 vl : Val} {σ : State} {obs e' σ' efs}
+    (h : get? (M := HeapF) σ.heap l = some (some vl)) (htrue : decide (vl = v1) = true)
+    (hs : BaseStep (.cmpXchg (.val (.lit (.loc l))) (.val v1) (.val v2)) σ obs e' σ' efs) :
+    obs = [] ∧ e' = (ToVal.ofVal (Val.pair vl (.lit (.bool true))) : Exp) ∧
+      σ' = σ.initHeap l 1 (some v2) ∧ efs = [] := by
+  cases hs with | cmpXchgS => grind
+
+theorem cmpXchgS_det_false {l : Loc} {v1 v2 vl : Val} {σ : State} {obs e' σ' efs}
+    (h : get? (M := HeapF) σ.heap l = some (some vl)) (hfalse : decide (vl = v1) = false)
+    (hs : BaseStep (.cmpXchg (.val (.lit (.loc l))) (.val v1) (.val v2)) σ obs e' σ' efs) :
+    obs = [] ∧ e' = (ToVal.ofVal (Val.pair vl (.lit (.bool false))) : Exp) ∧
+      σ' = σ ∧ efs = [] := by
+  cases hs with | cmpXchgS => grind
+
+/-! ### Multi-cell allocation helpers -/
+
+def allocCells (l : Loc) (n : Nat) (v : Option Val) : HeapF (Option Val) :=
+  (List.range n).foldl (fun h (i : Nat) => Std.insert (M := HeapF) h (l + (i : Int)) v) ∅
+
+theorem get?_foldl_insert (l : Loc) (v : Option Val) (m : HeapF (Option Val)) (n : Nat) (k : Loc) :
+    get? (M := HeapF) ((List.range n).foldl
+        (fun h (i : Nat) => Std.insert (M := HeapF) h (l + (i : Int)) v) m) k
+      = if (∃ i, i < n ∧ k = l + (i : Int)) then some v else get? (M := HeapF) m k := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    rw [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil,
+      Std.LawfulPartialMap.get?_insert, ih]
+    by_cases hk : (l + (n : Int)) = k
+    · rw [if_pos hk, if_pos ⟨n, Nat.lt_succ_self n, hk.symm⟩]
+    · rw [if_neg hk]
+      by_cases hex : ∃ i, i < n ∧ k = l + (i : Int)
+      · obtain ⟨i, hi, hki⟩ := hex
+        rw [if_pos ⟨i, hi, hki⟩, if_pos ⟨i, Nat.lt_succ_of_lt hi, hki⟩]
+      · grind
+
+theorem get?_allocCells {l : Loc} {n : Nat} {v : Option Val} {k : Loc} :
+    get? (M := HeapF) (allocCells l n v) k
+      = if (∃ i, i < n ∧ k = l + (i : Int)) then some v else none := by
+  simp [allocCells, get?_foldl_insert, LawfulPartialMap.get?_empty]
+
+theorem initHeap_heap_eq {σ : State} {l : Loc} {n : Int} {v : Option Val} :
+    Std.PartialMap.equiv (M := HeapF) (σ.initHeap l n v).heap
+      (Std.PartialMap.union (allocCells l n.toNat v) σ.heap) := by
+  intro k
+  show get? (M := HeapF) ((List.range n.toNat).foldl
+      (fun h (i : Nat) => Std.insert (M := HeapF) h (l + (i : Int)) v) σ.heap) k = _
+  rw [get?_foldl_insert, Std.PartialMap.union, Std.LawfulPartialMap.get?_merge, get?_allocCells]
+  by_cases hex : ∃ i, i < n.toNat ∧ k = l + (i : Int)
+  · simp only [if_pos hex]; cases get? (M := HeapF) σ.heap k <;> rfl
+  · simp only [if_neg hex]; cases get? (M := HeapF) σ.heap k <;> rfl
+
+theorem allocCells_disjoint {l : Loc} {n : Int} {v : Val} {m : HeapF (Option Val)}
+    (hf : ∀ i : Int, 0 ≤ i → i < n → get? (M := HeapF) m (l + i) = none) :
+    Std.PartialMap.disjoint (M := HeapF) (allocCells l n.toNat (some v)) m := by
+  intro k ⟨h1, h2⟩
+  rw [get?_allocCells] at h1
+  split at h1 <;> rename_i hcond
+  · obtain ⟨i, hi, hki⟩ := hcond
+    rw [hki, hf (i : Int) (Int.natCast_nonneg i) (by omega)] at h2
+    simp at h2
+  · simp at h1
+
+theorem mem_le_foldr_max (x : Int) (L : List Int) (h : x ∈ L) :
+    x ≤ L.foldr max 0 := by induction L <;> grind
+
+theorem exists_fresh_block (m : HeapF (Option Val)) (n : Int) :
+    ∃ l : Loc, ∀ i : Int, 0 ≤ i → i < n → get? (M := HeapF) m (l + i) = none := by
+  refine ⟨Loc.mk ((m.keys.map Loc.n).foldr max 0 + 1), fun i hi0 hin => ?_⟩
+  simp only [get?, getElem?_eq_none_iff, ← Std.ExtTreeMap.mem_keys]
+  intro hmem
+  have hle : (Loc.mk ((m.keys.map Loc.n).foldr max 0 + 1) + i).n ≤ (m.keys.map Loc.n).foldr max 0 :=
+    mem_le_foldr_max _ _ (List.mem_map_of_mem hmem)
+  simp only [loc_add_n] at hle
+  grind
+
+theorem coPset_top_ne_empty : (⊤ : CoPset) ≠ ∅ := by
+  intro h
+  refine CoPset.mem_empty (p := Pos.xH) ?_
+  cases h
+
+theorem usedProph_insert_eq {ps : Std.ExtTreeSet ProphId compare} {p : ProphId} :
+    ps.insert p = ({p} ∪ ps : Std.ExtTreeSet ProphId compare) := by
+  refine Std.ExtTreeSet.ext_mem fun x => ?_
+  rw [Std.ExtTreeSet.mem_union_iff, Std.ExtTreeSet.mem_insert,
+    Std.mem_singleton_extTreeSet, Std.LawfulEqCmp.compare_eq_iff_eq]
+  grind
+
+theorem wp_baseCompletenessGoal (e₁ : Exp) (σ : State) (E : CoPset)
+    (Hred : BaseStep.Reducible (e₁, σ)) :
+    heapInv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e₁ σ E) := by
+  iintro Hinv
+  obtain ⟨κ, e', σ', efs, Hstep⟩ := Hred
+  cases Hstep with
+  | recS f x e σ =>
+      iapply (wp_base_pure trivial σ E (.recS f x e)) $$ Hinv
+  | pairS v1 v2 σ =>
+      iapply (wp_base_pure trivial σ E (.pairS v1 v2)) $$ Hinv
+  | injLS v σ =>
+      iapply (wp_base_pure trivial σ E (.injLS v)) $$ Hinv
+  | injRS v σ =>
+      iapply (wp_base_pure trivial σ E (.injRS v)) $$ Hinv
+  | betaS f x eb v2 e' σ h =>
+      iapply (wp_base_pure trivial σ E (.betaS f x eb v2 _ · rfl)) $$ Hinv
+  | unOpS op v v' σ h =>
+      iapply (wp_base_pure (hpe := instPureExecUnOp) h σ E (.unOpS op v v' · h)) $$ Hinv
+  | binOpS op v1 v2 v' σ h =>
+      iapply (wp_base_pure (hpe := instPureExecBinOp) h σ E (.binOpS op v1 v2 v' · h)) $$ Hinv
+  | ifTrueS et ee σ =>
+      iapply (wp_base_pure trivial σ E (.ifTrueS e' ee)) $$ Hinv
+  | ifFalseS et ee σ =>
+      iapply (wp_base_pure trivial σ E (.ifFalseS et e')) $$ Hinv
+  | fstS v1 v2 σ =>
+      iapply (wp_base_pure trivial σ E (.fstS v1 v2)) $$ Hinv
+  | sndS v1 v2 σ =>
+      iapply (wp_base_pure trivial σ E (.sndS v1 v2)) $$ Hinv
+  | caseLS v et ee σ =>
+      iapply (wp_base_pure trivial σ E (.caseLS v et ee)) $$ Hinv
+  | caseRS v et ee σ =>
+      iapply (wp_base_pure trivial σ E (.caseRS v et ee)) $$ Hinv
+  | loadS l v σ hl =>
+      iapply (wp_base_atomic_nochange l v σ E
+        (base_step_to_val_atomic .StronglyAtomic (.loadS l v σ hl)) hl
+        (.loadS l v) loadS_det) $$ Hinv
+  | storeS l v w σ hl =>
+      iapply (wp_base_atomic l v (some w) σ E
+        (base_step_to_val_atomic .StronglyAtomic (.storeS l v w σ hl)) hl
+        (.storeS l v w) (fun _ => storeS_det)) $$ Hinv
+  | freeS l v σ hl =>
+      iapply (wp_base_atomic l v none σ E
+        (base_step_to_val_atomic .StronglyAtomic (.freeS l v σ hl)) hl
+        (.freeS l v) (fun _ => freeS_det)) $$ Hinv
+  | xchgS l v1 v2 σ hl =>
+      iapply (wp_base_atomic l v1 (some v2) σ E
+        (base_step_to_val_atomic .StronglyAtomic (.xchgS l v1 v2 σ hl)) hl
+        (.xchgS l v1 v2) xchgS_det) $$ Hinv
+  | faaS l i1 i2 σ hl =>
+      iapply (wp_base_atomic l (.lit (.int i1))
+        (some (.lit (.int (i1 + i2)))) σ E
+        (base_step_to_val_atomic .StronglyAtomic (.faaS l i1 i2 σ hl)) hl
+        (.faaS l i1 i2) faaS_det) $$ Hinv
+  | cmpXchgS l v1 v2 vl σ b hl hcs hb =>
+      cases hb1 : decide (vl = v1) with
+      | true =>
+          have Hx σ'' h := BaseStep.cmpXchgS l v1 v2 vl σ'' true h hcs (by rw [hb1])
+          iapply (wp_base_atomic l vl (some v2) σ E
+            (base_step_to_val_atomic .StronglyAtomic (Hx σ hl))
+              hl Hx (cmpXchgS_det_true · hb1)) $$ Hinv
+      | false =>
+          have Hx σ'' h := BaseStep.cmpXchgS l v1 v2 vl σ'' false h hcs (by rw [hb1])
+          iapply (wp_base_atomic_nochange l vl σ E
+            (base_step_to_val_atomic Atomicity.StronglyAtomic (Hx σ hl))
+            hl Hx (cmpXchgS_det_false · hb1)) $$ Hinv
+  | forkS e σ =>
+      imodintro
+      iright
+      iframe Hinv
+      iintro %Φ %E₂ H
+      iapply wp_fork_fupd
+      iintro !>
+      ihave Htraj : iprop(∀ σ₁, heapInv σ₁ ={E}=∗
+          ∃ κ σ₁', ⌜PrimSteps (.fork e) σ₁ κ (.val (.lit .unit)) σ₁' [e]⌝ ∗ heapInv σ₁') $$ []
+      · iintro %σ₁ Hheap
+        imodintro
+        iexists [], σ₁
+        iframe Hheap
+        ipureintro
+        exact .once (EctxLanguage.primStep_of_baseStep (.forkS e σ₁))
+      imod H $$ Htraj with ⟨HwpUnit, Hefs⟩
+      isplitl [Hefs]
+      · iapply (BigSepL.bigSepL_singleton (PROP := IProp GF)).1 $$ Hefs
+      · iapply (wp_value_fupd' (v := .lit .unit)).1 $$ HwpUnit
+  | allocNS n v σ l hn hfresh =>
+      imodintro
+      ileft
+      have hatom : Atomic .StronglyAtomic (Exp.allocN (.val (.lit (.int n))) (.val v)) :=
+        base_step_to_val_atomic Atomicity.StronglyAtomic (BaseStep.allocNS n v σ l hn hfresh)
+      iframe %hatom
+      iintro %Φ Hstep
+      iapply wp_lift_atomic_step (EctxLanguage.val_stuck (BaseStep.allocNS n v σ l hn hfresh))
+      iintro %σ₁ %ns %obs %obs' %nt Hσ !>
+      icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩
+      obtain ⟨lf, hlf⟩ := exists_fresh_block σ₁.heap n
+      have Hred₁ : BaseStep.Reducible (Exp.allocN (.val (.lit (.int n))) (.val v), σ₁) :=
+        ⟨[], _, _, [], BaseStep.allocNS n v σ₁ lf hn hlf⟩
+      isplit
+      · ipureintro
+        simp only [Stuckness.MaybeReducible]
+        exact EctxLanguage.primStep_reducible_of_baseStep_reducible Hred₁
+      iintro !> %e₂ %σ₂ %eₜ %Hprim Hcr
+      rcases EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hred₁ Hprim
+      rename_i l' Hpo Hi
+      ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph
+      icases Hinv with ⟨Hmap, Hproph_inv⟩
+      imod (genHeap_alloc_big (allocCells l' n.toNat (some v)) σ₁.heap (allocCells_disjoint Hi))
+        $$ Hσ with ⟨Hσ', Hnewpts, Hnewmeta⟩
+      ihave %hfreshσ : ⌜∀ i : Int, 0 ≤ i → i < n → get? (M := HeapF) σ.heap (l' + i) = none⌝
+          $$ [Hmap Hnewmeta]
+      · iintro %i %hi0 %hin
+        rcases hgc : get? (M := HeapF) σ.heap (l' + i) with _ | vo
+        · itrivial
+        · icases (BigSepM.bigSepM_lookup_acc hgc).1 $$ Hmap with ⟨⟨_, Hmeta1⟩, _⟩
+          have hcell_new : get? (allocCells l' n.toNat (some v)) (l' + i) = some (some v) := by
+            rw [get?_allocCells, if_pos ⟨i.toNat, by omega, by rw [Int.toNat_of_nonneg hi0]⟩]
+          icases (BigSepM.bigSepM_lookup_acc hcell_new).1 $$ Hnewmeta with ⟨Hmeta2, _⟩
+          icases metaToken_ne coPset_top_ne_empty $$ Hmeta1 Hmeta2 with %hne
+          exact absurd rfl hne
+      imod Hstep $$ [] with ⟨Hpost, _⟩
+      · ipureintro
+        exact EctxLanguage.primStep_of_baseStep (BaseStep.allocNS n v σ l' hn hfreshσ)
+      imodintro
+      iframe
+      isplitl [Hσ' Hproph]
+      · simp only [stateInterp]
+        iframe
+        iapply genHeapInterp_eqv (Std.PartialMap.equiv.symm _ _ initHeap_heap_eq)
+        iexact Hσ'
+      iexists (.lit (.loc l'))
+      isplit; ipureintro; simp [toVal]; rfl
+      iapply Hpost
+      simp only [heapInv]
+      iframe
+      iapply (BigSepM.bigSepM_eqv_of_perm initHeap_heap_eq).2
+      iapply (BigSepM.bigSepM_union (allocCells_disjoint hfreshσ)).2
+      iframe
+      iapply (equiv_iff.mp BigSepM.bigSepM_sep_eqv).2
+      iframe
+      iapply (BigSepM.bigSepM_mono_of_forall (fun {k vo} => pointsTo_heapCellPts k vo)) $$ Hnewpts
+  | newProphS σ p hp =>
+      imodintro
+      ileft
+      isplit
+      · ipureintro
+        exact base_step_to_val_atomic Atomicity.StronglyAtomic (BaseStep.newProphS σ p hp)
+      iintro %Φ Hstep
+      iapply wp_lift_atomic_step (EctxLanguage.val_stuck (BaseStep.newProphS σ p hp))
+      iintro %σ₁ %ns %obs %obs' %nt Hσ !>
+      icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩
+      obtain ⟨pf, Hpf⟩ := Std.List.fresh σ₁.usedProphId.toList
+      have Hpf_contains : ¬ σ₁.usedProphId.contains pf := by
+        intro hc; exact Hpf (Std.ExtTreeSet.mem_toList.mpr hc)
+      have Hred₁ : BaseStep.Reducible (Exp.newProph, σ₁) :=
+        ⟨[], _, _, [], BaseStep.newProphS σ₁ pf Hpf_contains⟩
+      isplitr
+      · ipureintro
+        simp only [Stuckness.MaybeReducible]
+        exact EctxLanguage.primStep_reducible_of_baseStep_reducible Hred₁
+      iintro !> %e₂ %σ₂ %eₜ %Hprim Hcr
+      cases EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hred₁ Hprim
+      rename_i p' Hp'
+      ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph
+      have Hp'_mem : p' ∉ σ₁.usedProphId :=
+        fun hmem => Hp' (Std.ExtTreeSet.mem_iff_contains.symm.mp hmem)
+      imod (ProphMap.new_proph p' σ₁.usedProphId obs' Hp'_mem) $$ Hproph
+        with ⟨Hproph', Htok⟩
+      icases Hinv with ⟨Hmap, Hproph_inv⟩
+      ihave %Hfresh_σ : ⌜p' ∉ σ.usedProphId⌝ $$ [Hproph_inv Htok]
+      · iintro %hmem
+        icases BigSepS.bigSepS_elem_of_acc hmem $$ Hproph_inv with ⟨⟨%pvs', Htok'⟩, _⟩
+        iapply proph_exclusive $$ Htok Htok'
+      have Hfresh_σ_contains : ¬ σ.usedProphId.contains p' := fun hc =>
+        Hfresh_σ (Std.ExtTreeSet.mem_iff_contains.symm.mpr hc)
+      imod Hstep $$ [] with ⟨Hpost, _⟩
+      · ipureintro
+        exact EctxLanguage.primStep_of_baseStep (BaseStep.newProphS σ p' Hfresh_σ_contains)
+      imodintro
+      isplitl [Hσ Hproph']
+      · simp only [stateInterp]
+        iframe Hσ
+        rw [show ({p'} ∪ σ₁.usedProphId : Std.ExtTreeSet ProphId compare)
+            = σ₁.usedProphId.insert p' from usedProph_insert_eq.symm]
+        iexact Hproph'
+      iframe
+      iexists (.lit (.prophecy p'))
+      isplit; ipureintro; simp [toVal]; rfl
+      iapply Hpost
+      simp only [heapInv]
+      iframe
+      rw [usedProph_insert_eq (ps := σ.usedProphId) (p := p')]
+      have hdisj : ({p'} : Std.ExtTreeSet ProphId compare) ## σ.usedProphId := by
+        intro x ⟨h1, h2⟩
+        rw [Std.LawfulSet.mem_singleton] at h1
+        subst h1
+        exact Hfresh_σ h2
+      iapply (BigSepS.bigSepS_union hdisj).mpr
+      iframe
+      iapply BigSepS.bigSepS_singleton.mpr
+      iexists (prophListResolves obs' p')
+      iexact Htok
+  | resolveS p v e σ w σ' κs ts hbase hp =>
+      have IH : heapInv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e σ E) :=
+        wp_baseCompletenessGoal e σ E ⟨κs, _, _, _, hbase⟩
+      have hatom : Atomic Atomicity.StronglyAtomic
+          (Exp.resolve e (.val (.lit (.prophecy p))) (.val w)) :=
+        base_step_to_val_atomic Atomicity.StronglyAtomic
+          (BaseStep.resolveS p v e σ w σ' κs efs hbase hp)
+      have hatom_e : Atomic Atomicity.StronglyAtomic e :=
+        base_step_to_val_atomic Atomicity.StronglyAtomic hbase
+      have hne_e : toVal e = none := EctxLanguage.val_stuck hbase
+      have hp_mem : p ∈ σ.usedProphId := Std.ExtTreeSet.mem_iff_contains.symm.mpr hp
+      imodintro
+      ileft
+      iframe %hatom; clear hatom
+      iintro %Φ Hstep
+      icases Hinv with ⟨Hmap, Hproph_inv⟩
+      icases BigSepS.bigSepS_elem_of_acc hp_mem $$ Hproph_inv with ⟨⟨%pvs, Htok⟩, HcloseProph⟩
+      iapply (wp_resolve_strong hatom_e hne_e) $$ Htok
+      iintro Hele
+      ihave Hinv_full : heapInv σ $$ [Hmap HcloseProph Hele]
+      · unfold heapInv
+        iframe
+        iapply HcloseProph
+        iexists pvs; iexact Hele
+      ihave Hinner : iprop(|={E}=> baseCompletenessGoal e σ E) $$ [Hinv_full]
+      · iapply IH $$ [$]
+      iapply fupd_wp
+      imod Hinner with H
+      imodintro
+      icases H with (⟨-, Hrst⟩ | ⟨Hinv_back, Hrst_nonatom⟩)
+      · iapply Hrst
+        iintro !> %κ_e %v_e %σ_e %efs_e %Hprim_e
+        have Hbase_e : BaseStep e σ κ_e (.val v_e) σ_e efs_e := primStep_val_baseStep Hprim_e
+        imod Hstep $$ %_ %_ %_ %_ %(prim_step_resolve_of_inner (w := w) Hbase_e hp)
+          with ⟨Hwp_outer, Hefs⟩
+        imodintro
+        iframe Hefs
+        iintro ⟨Hmap_e, Hproph_inv_e⟩
+        have hp_mem_e : p ∈ σ_e.usedProphId := base_step_more_proph_ids Hbase_e p hp_mem
+        icases BigSepS.bigSepS_elem_of_acc hp_mem_e $$ Hproph_inv_e
+          with ⟨⟨%pvs2, Hele2⟩, HcloseProph_e⟩
+        iexists pvs2
+        iframe Hele2
+        iintro %pvs'' %heq Hele2'
+        subst heq
+        iapply Hwp_outer
+        unfold heapInv
+        iframe Hmap_e
+        iapply HcloseProph_e
+        iexists pvs''; iexact Hele2'
+      · iapply Hrst_nonatom
+        iintro !> %e₂_e %efs_e Htraj_e
+        imod Htraj_e $$ %_ Hinv_back with ⟨%κ_e, %σ_e, %Hprims, ⟨Hmap_e, Hproph_inv_e⟩⟩
+        obtain ⟨Hprim_e, hval_e⟩ := primSteps_atomic (e := e) hatom_e Hprims
+        obtain ⟨v_e, rfl⟩ : ∃ v_e, e₂_e = Exp.val v_e := by
+          match e₂_e, hval_e with | .val v_e, _ => exact ⟨v_e, rfl⟩
+        have Hbase_e : BaseStep e σ κ_e (.val v_e) σ_e efs_e := primStep_val_baseStep Hprim_e
+        imod Hstep $$ %_ %_ %_ %_ %(prim_step_resolve_of_inner (w := w) Hbase_e hp)
+          with ⟨Hwp_outer, Hefs⟩
+        imodintro
+        have hp_mem_e : p ∈ σ_e.usedProphId := base_step_more_proph_ids Hbase_e p hp_mem
+        icases BigSepS.bigSepS_elem_of_acc hp_mem_e $$ Hproph_inv_e
+          with ⟨⟨%pvs2, Hele2⟩, HcloseProph_e⟩
+        iframe
+        iapply wp_value'
+        iexists pvs2
+        iframe Hele2
+        iintro %pvs'' %heq Hele2'
+        subst heq
+        iapply Hwp_outer
+        unfold heapInv
+        iframe Hmap_e
+        iapply HcloseProph_e
+        iexists pvs''
+        iexact Hele2'
+termination_by e₁
+
+section Framework
+
+variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] [TpinvGS GF Exp H]
+
+theorem wp_base_completeness {n C e₁ σ K E} :
+  ⊢@{IProp GF} ectxLangCompletenessStmt (Wp.wp Stuckness.NotStuck)
+        (fun (_ : List Exp) (σ : State) => heapInv σ) n C e₁ σ K E := by
+  unfold ectxLangCompletenessStmt
+  iintro %Hred Htok ⟨Hheap, Htp, %Hsafe⟩
+  imod (wp_baseCompletenessGoal e₁ σ E Hred) $$ Hheap with (⟨%Hatom, H⟩ | ⟨Hheap, H⟩)
+  · -- Atomic redex.
+    imodintro
+    ileft
+    have Hwa : Atomic Atomicity.WeaklyAtomic e₁ := stronglyAtomic_atomic Hatom
+    iframe %Hwa
+    iintro %Φ Hx
+    iapply H
+    iintro !> %κ %v₂ %σ' %efs %Hprim
+    iapply Hx $$ [] Htok Htp
+    ipureintro; exact Hprim
+  · -- Non-atomic redex.
+    imodintro
+    iright
+    iframe Hheap Htp
+    iintro %Φ Hx
+    iapply H
+    iintro !> %e₂ %efs HH
+    iapply Hx
+    iintro %σ₁ %C₁ ⟨Hsi, Htp, %_Hs⟩
+    imod HH $$ Hsi with ⟨%κ, %σ₁', %Hprims, Hhp⟩
+    imodintro
+    iexists κ, σ₁'
+    iframe Htok Htp Hhp
+    ipureintro
+    exact Hprims
+
+instance heap_lang_completeness :
+    AbstractEctxLangCompletenessGen (Expr := Exp) (Ectx := List ECtxItem)
+      (Wp.wp (PROP := IProp GF) Stuckness.NotStuck) where
+  heap_inv _ := heapInv
+  heap_inv_timeless _ := instTimeless_heapInv
+  ectx_lang_completeness _ _ _ _ _ _ := wp_base_completeness
+
+end Framework
+
+section Endpoint
+
+variable {H : Type _ → Type _} [LawfulFiniteMap H Nat] [GhostMapG GF Nat Exp H] [CInvG GF]
+include H
+
+theorem heap_lang_sem_completeness (e : Exp) (σ : State) (φ : Val → Prop)
+    (Hade : adequate Stuckness.NotStuck e σ (fun v _ => φ v)) :
+    ⊢ heapInv (GF := GF) σ -∗ WP e @ Stuckness.NotStuck; ⊤ {{ v, ⌜φ v⌝ }} := by
+  iintro Hheap
+  imod (tpInv_alloc (GF := GF) (Expr := Exp) (H := H)) with ⟨%γ, Hini⟩
+  letI TI : TpinvGS GF Exp H := { toGhostMapG := inferInstance, tp_name := γ }
+  ihave Hwp := weakestpre_sem_completeness
+    (wp := Wp.wp (PROP := IProp GF) Stuckness.NotStuck) e σ φ Hade $$ Hini Hheap
+  iexact Hwp
+
+theorem heap_lang_sem_completeness_nofork (e : Exp) (σ : State) (φ : Val → State → Prop)
+    (Hade : AdequateNoFork Stuckness.NotStuck e σ (fun v σ' => φ v σ')) :
+    ⊢ heapInv (GF := GF) σ -∗
+      WP e @ Stuckness.NotStuck; ⊤ {{ v, ∃ σ' : State, heapInv σ' ∗ ⌜φ v σ'⌝ }} := by
+  iintro Hheap
+  imod (tpInv_alloc (GF := GF) (Expr := Exp) (H := H)) with ⟨%γ, Hini⟩
+  letI TI : TpinvGS GF Exp H := { toGhostMapG := inferInstance, tp_name := γ }
+  ihave Hwp := weakestpre_sem_completeness_nofork
+    (wp := Wp.wp (PROP := IProp GF) Stuckness.NotStuck) e σ φ Hade $$ Hini Hheap
+  iexact Hwp
+
+end Endpoint
+
+end Iris.HeapLang
diff --git a/Iris/Iris/HeapLang/Omni.lean b/Iris/Iris/HeapLang/Omni.lean
new file mode 100644
index 000000000..9c205ddb7
--- /dev/null
+++ b/Iris/Iris/HeapLang/Omni.lean
@@ -0,0 +1,523 @@
+module
+
+public import Iris.HeapLang.Instances
+public import Iris.ProgramLogic.Adequacy
+public import Std.Internal.Do.WP.Basic
+
+@[expose] public section
+namespace Iris.HeapLang
+
+open ProgramLogic PrimStep Language Language.Notation Lean.Order
+
+/-! ## Greatest fixpoint (dual of `Lean.Order.lfp`) -/
+
+section gfp
+open Lean.Order.PartialOrder Lean.Order.CompleteLattice
+variable {α : Sort u} [Lean.Order.CompleteLattice α]
+
+/-- Greatest fixpoint: the largest post-fixed point `x ⊑ f x`. -/
+noncomputable def gfp (f : α → α) : α := sup (fun x => x ⊑ f x)
+
+/-- Coinduction: any post-fixed point is below `gfp f`. -/
+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_prefixed {f : α → α} (hm : monotone f) : f (gfp f) ⊑ gfp f :=
+  le_gfp (hm _ _ (gfp_postfixed hm))
+
+theorem gfp_fix {f : α → α} (hm : monotone f) : gfp f = f (gfp f) :=
+  rel_antisymm (gfp_postfixed hm) (gfp_prefixed hm)
+
+end gfp
+
+/-! ## The omni-WP for HeapLang -/
+
+abbrev WPArg := Exp → State → (Val → State → Prop) → Prop
+
+/-- Weakest precondition functor
+This wp forbids forks. -/
+def wpF (r : WPArg) : WPArg := fun e σ Q =>
+  (∃ v, ToVal.toVal e = some v ∧ Q v σ) ∨
+  (Reducible (e, σ) ∧
+    ∀ κ e' σ' efs, (e, σ) -<κ>-> (e', σ', efs) → efs = [] ∧ r e' σ' Q)
+
+noncomputable def wp : WPArg := gfp wpF
+
+theorem wpF_monotone : monotone wpF := by
+  intro r1 r2 h e σ Q 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 e' σ' Q h1⟩
+
+/-- The defining fixpoint equation for `wp`. -/
+theorem wp_unfold : wp = wpF wp := gfp_fix wpF_monotone
+
+theorem wp_unfold_apply {e σ Q} : wp e σ Q ↔ wpF wp e σ Q := by rw [← wp_unfold]
+
+/-- Coinduction principle: an invariant closed under `wpF` is below `wp`. -/
+theorem wp_coind (I : WPArg) (h : ∀ e σ Q, I e σ Q → wpF I e σ Q) :
+    ∀ e σ Q, I e σ Q → wp e σ Q := le_gfp (x := I) h
+
+/-! ## Adequacy (fork-free fragment) -/
+
+theorem wp_primStep {e σ Q κ e' σ' efs}
+    (hwp : wp e σ Q) (hstep : (e, σ) -<κ>-> (e', σ', efs)) :
+    efs = [] ∧ wp e' σ' Q := by
+  rw [wp_unfold_apply] at hwp
+  rcases hwp with ⟨v, hv, _⟩ | ⟨_, hk⟩
+  · exact absurd (Language.val_stuck hstep) (by rw [hv]; exact Option.some_ne_none v)
+  · exact hk κ e' σ' efs hstep
+
+theorem wp_notStuck {e σ Q} (hwp : wp e σ Q) : NotStuck (e, σ) := by
+  rw [wp_unfold_apply] at hwp
+  rcases hwp with ⟨v, hv, _⟩ | ⟨hred, _⟩
+  · exact .inl (by rw [hv]; exact rfl)
+  · exact .inr hred
+
+theorem wp_erasedStep {e σ Q t' σ'} (hwp : wp e σ Q)
+    (hstep : ([e], σ) -·->ₜₚ (t', σ')) : ∃ e', t' = [e'] ∧ wp e' σ' Q := by
+  obtain ⟨κ, hstep⟩ := hstep
+  generalize hsrc : ([e], σ) = src at hstep
+  cases hstep with
+  | @atomic e₀ _ _ e' _ efs hbase t₁ t₂ =>
+    obtain ⟨hpool, rfl⟩ := Prod.mk.injEq .. ▸ hsrc
+    rcases List.append_eq_cons_iff.mp hpool.symm with ⟨rfl, heq⟩ | ⟨a, _, hcontra⟩
+    · obtain ⟨rfl, rfl⟩ := List.cons_eq_cons.mp heq
+      obtain ⟨rfl, hwp'⟩ := wp_primStep hwp hbase
+      exact ⟨e', by simp, hwp'⟩
+    · exact absurd hcontra (by simp)
+
+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 hreach
+  induction hreach with
+  | refl => exact ⟨e, rfl, hwp⟩
+  | @tail q r _ hstep ih =>
+    obtain ⟨e₁, hq, hwp₁⟩ := ih
+    obtain ⟨tq, σq⟩ := q; subst hq
+    obtain ⟨tr, σr⟩ := r
+    obtain ⟨e₂, rfl, hwp₂⟩ := wp_erasedStep hwp₁ hstep
+    exact ⟨e₂, rfl, hwp₂⟩
+
+/-- **Adequacy for the fork-free fragment**: the omni-`wp` yields an
+`AdequateNoFork` partial-correctness predicate. -/
+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; simp only at hq; rw [hq]; rfl
+  result hreach := by
+    obtain ⟨e', hq, hwp'⟩ := wp_reach hwp hreach; simp only at hq hwp'
+    -- hq : ofVal v :: t₂ = [e'], so the pool is exactly [ofVal v] and e' = ofVal v
+    obtain ⟨rfl, -⟩ := List.cons_eq_cons.mp hq
+    rw [wp_unfold_apply] at hwp'
+    rcases hwp' with ⟨v', hv', hQ⟩ | ⟨hred, _⟩
+    · rw [ToVal.toVal_coe] at hv'; cases hv'; exact hQ
+    · exact absurd (toVal_none_of_reducible hred) (by rw [ToVal.toVal_coe]; simp)
+  not_stuck _ hreach hmem := by
+    obtain ⟨e', hq, hwp'⟩ := wp_reach hwp hreach; simp only at hq hwp'
+    rw [hq, List.mem_singleton] at hmem; subst hmem
+    exact wp_notStuck hwp'
+
+/-! ## `WPPre` instance (wiring into the `Do.lean` framework)
+
+The omni-`wp` is the predicate transformer of the `WPPre` framework, with
+result type `Val`, precondition lattice `State → Prop`, and the trivial
+exceptional postcondition `EPost.nil` (the fragment is exception-free). -/
+
+/-- `wp` is monotone in its postcondition. -/
+theorem wp_mono {e σ} {Q Q' : Val → State → Prop}
+    (hQ : ∀ v σ, Q v σ → Q' v σ) (hwp : wp e σ Q) : wp e σ Q' := by
+  -- Coinduction: `fun e σ R => ∃ Q, (∀ v σ, Q v σ → R v σ) ∧ wp e σ Q` is `wpF`-closed.
+  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_apply] 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'⟩
+
+/-! ## Bind / evaluation-context rule
+
+`wp_bind` decomposes the wp of an expression sitting in an evaluation context:
+evaluate the focus `e` to a value `v`, then continue with `K (ofVal v)`. Stated
+for any `Language.Context K` (HeapLang provides `instContextFill` for
+`fill K`). -/
+
+theorem wp_bind {K : Exp → Exp} [Language.Context K] {e σ Q}
+    (hwp : wp e σ (fun v σ' => wp (K (Exp.ofVal v)) σ' Q)) : wp (K e) σ Q := by
+  -- Coinduct on: "already wp, or of the form `K e` with `e` running toward the
+  -- continuation". The left disjunct lets the invariant absorb `wp`.
+  refine wp_coind
+    (fun a σ Q => wp a σ Q ∨
+      ∃ e, a = K e ∧ wp e σ (fun v σ' => wp (K (Exp.ofVal v)) σ' Q))
+    (fun a σ Q hI => ?_) (K e) σ Q (.inr ⟨e, rfl, hwp⟩)
+  rcases hI with hwp | ⟨e, rfl, hwp⟩
+  · -- already `wp a σ Q`: unfold and weaken each recursive position into the invariant
+    rw [wp_unfold_apply] 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 ·)⟩
+  · -- `a = K e`: case on whether the focus `e` is already a value
+    rw [wp_unfold_apply] at hwp
+    rcases hwp with ⟨v, hv, hcont⟩ | ⟨hred, hstep⟩
+    · -- focus is `ofVal v`: `K e = K (ofVal v)`, continue with `wp (K (ofVal v))`
+      have : e = Exp.ofVal v := (ToVal.coe_of_toVal_eq_some hv).symm
+      subst this
+      -- `hcont : wp (K (ofVal v)) σ Q`; fold into the invariant via the left disjunct
+      rw [wp_unfold_apply] at hcont
+      exact hcont.imp id (fun ⟨hr, hs⟩ => ⟨hr, fun κ e' σ' efs hst =>
+        (hs κ e' σ' efs hst).imp id (.inl ·)⟩)
+    · -- focus reduces: `K e` is reducible, and successors stay in the invariant
+      have hKred : Reducible (K e, σ) :=
+        let ⟨obs, e', σ', eₜ, hst⟩ := hred
+        ⟨obs, K e', σ', eₜ, Language.Context.primStep_fill hst⟩
+      refine .inr ⟨hKred, fun κ Ke' σ' efs hs => ?_⟩
+      have hnv : ToVal.toVal e = none := toVal_none_of_reducible hred
+      obtain ⟨e', rfl, hes⟩ := Language.Context.primStep_fill_inv hnv hs
+      obtain ⟨hnil, hwp'⟩ := hstep κ e' σ' efs hes
+      exact ⟨hnil, .inr ⟨e', rfl, hwp'⟩⟩
+
+/-- HeapLang specialization: bind over an evaluation context `fill K`. -/
+theorem wp_bind_fill (K : List ECtxItem) {e σ Q}
+    (hwp : wp e σ (fun v σ' => wp (ProgramLogic.fill K (Exp.ofVal v)) σ' Q)) :
+    wp (ProgramLogic.fill K e) σ Q :=
+  wp_bind (K := ProgramLogic.fill K) hwp
+
+/-! ## Lifting base steps to `wp`
+
+Generic backward rule: to prove `wp e σ Q` it suffices that `e` is reducible and
+every (fork-free) successor is already `wp`-safe. Every primitive rule below is
+an instance of this with the relevant `BaseStep` inverted. -/
+
+/-- Backward step rule (the right disjunct of `wp_unfold`). -/
+theorem wp_lift_step {e σ Q} (hred : Reducible (e, σ))
+    (hcont : ∀ κ e' σ' efs, (e, σ) -<κ>-> (e', σ', efs) → efs = [] ∧ wp e' σ' Q) :
+    wp e σ Q := by
+  rw [wp_unfold_apply]; exact .inr ⟨hred, hcont⟩
+
+open ProgramLogic EctxLanguage in
+/-- A `load` of a bound location reduces to the stored value, leaving the state
+unchanged. -/
+theorem wp_load {l : Loc} {v : Val} {σ Q}
+    (hl : σ.get? l = some (some v)) (hQ : Q v σ) :
+    wp (.load (.ofVal (.lit (.loc l)))) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.load (.ofVal (.lit (.loc l))), σ) :=
+    ⟨[], _, _, _, BaseStep.loadS l v σ hl⟩
+  refine wp_lift_step (primStep_reducible_of_baseStep_reducible hbred)
+    (fun κ e' σ' efs hs => ?_)
+  -- the only base step of `load (loc l)` is `loadS`, giving `(ofVal v, σ, [])`
+  have hb := baseStep_of_primStep_of_baseStep_reducible hbred hs
+  cases hb with
+  | loadS _ v' _ hl' =>
+    rw [hl'] at hl; cases hl
+    exact ⟨rfl, by rw [wp_unfold_apply]; exact .inl ⟨v, ToVal.toVal_coe v, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- A `store` to a bound location updates it and returns unit. -/
+theorem wp_store {l : Loc} {v w : Val} {σ Q}
+    (hl : σ.get? l = some (some v)) (hQ : Q (.lit .unit) (σ.initHeap l 1 (some w))) :
+    wp (.store (.ofVal (.lit (.loc l))) (.ofVal w)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.store (.ofVal (.lit (.loc l))) (.ofVal w), σ) :=
+    ⟨[], _, _, _, BaseStep.storeS l v w σ hl⟩
+  refine 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
+  | storeS _ v' _ _ hl' =>
+    exact ⟨rfl, by rw [wp_unfold_apply]
+                   exact .inl ⟨.lit .unit, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- `if #true then e₁ else e₂` reduces to `e₁`. -/
+theorem wp_if_true {e₁ e₂ σ Q} (hQ : wp e₁ σ Q) :
+    wp (.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 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⟩
+
+open ProgramLogic EctxLanguage in
+/-- `if #false then e₁ else e₂` reduces to `e₂`. -/
+theorem wp_if_false {e₁ e₂ σ Q} (hQ : wp e₂ σ Q) :
+    wp (.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 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⟩
+
+open ProgramLogic EctxLanguage in
+/-- `free` of a bound location deallocates it and returns unit. -/
+theorem wp_free {l : Loc} {v : Val} {σ Q}
+    (hl : σ.get? l = some (some v)) (hQ : Q (.lit .unit) (σ.initHeap l 1 none)) :
+    wp (.free (.ofVal (.lit (.loc l)))) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.free (.ofVal (.lit (.loc l))), σ) :=
+    ⟨[], _, _, _, BaseStep.freeS l v σ hl⟩
+  refine 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
+  | freeS _ _ _ _ =>
+    exact ⟨rfl, by rw [wp_unfold_apply]; exact .inl ⟨.lit .unit, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- Atomic exchange `xchg l v2`: returns the old value, stores `v2`. -/
+theorem wp_xchg {l : Loc} {v1 v2 : Val} {σ Q}
+    (hl : σ.get? l = some (some v1)) (hQ : Q v1 (σ.initHeap l 1 (some v2))) :
+    wp (.xchg (.ofVal (.lit (.loc l))) (.ofVal v2)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.xchg (.ofVal (.lit (.loc l))) (.ofVal v2), σ) :=
+    ⟨[], _, _, _, BaseStep.xchgS l v1 v2 σ hl⟩
+  refine 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
+  | xchgS _ v1' _ _ hl' =>
+    rw [hl'] at hl; cases hl
+    exact ⟨rfl, by rw [wp_unfold_apply]; exact .inl ⟨v1, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- Compare-and-exchange. The stored value `vl` must be comparable to `v1`; the
+boolean result `b = (vl == v1)` decides whether the store happens. The
+continuation must cover both outcomes. -/
+theorem wp_cmpXchg {l : Loc} {v1 v2 vl : Val} {σ Q}
+    (hl : σ.get? l = some (some vl)) (hcmp : vl.compareSafe v1)
+    (hQ : ∀ b : Bool, decide (vl = v1) = b →
+      Q (.pair vl (.lit (.bool b))) (if b then σ.initHeap l 1 (some v2) else σ)) :
+    wp (.cmpXchg (.ofVal (.lit (.loc l))) (.ofVal v1) (.ofVal v2)) σ Q := by
+  have hbred : BaseStep.Reducible
+      (Exp.cmpXchg (.ofVal (.lit (.loc l))) (.ofVal v1) (.ofVal v2), σ) :=
+    ⟨[], _, _, _, BaseStep.cmpXchgS l v1 v2 vl σ _ hl hcmp rfl⟩
+  refine 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
+  | cmpXchgS _ _ _ vl' _ b hl' _ hb =>
+    rw [hl'] at hl; cases hl
+    exact ⟨rfl, by rw [wp_unfold_apply]
+                   exact .inl ⟨_, ToVal.toVal_coe _, hQ b hb⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- Fetch-and-add: atomically adds `i2` to the integer stored at `l`, returning
+the old value. -/
+theorem wp_faa {l : Loc} {i1 i2 : Int} {σ Q}
+    (hl : σ.get? l = some (some (.lit (.int i1))))
+    (hQ : Q (.lit (.int i1)) (σ.initHeap l 1 (some (.lit (.int (i1 + i2)))))) :
+    wp (.faa (.ofVal (.lit (.loc l))) (.ofVal (.lit (.int i2)))) σ Q := by
+  have hbred : BaseStep.Reducible
+      (Exp.faa (.ofVal (.lit (.loc l))) (.ofVal (.lit (.int i2))), σ) :=
+    ⟨[], _, _, _, BaseStep.faaS l i1 i2 σ hl⟩
+  refine 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
+  | faaS _ i1' _ _ hl' =>
+    rw [hl'] at hl; cases hl
+    exact ⟨rfl, by rw [wp_unfold_apply]; exact .inl ⟨_, ToVal.toVal_coe _, hQ⟩⟩
+
+open Std Iris.Std FromMathlib in
+/-- Heap finiteness + `Loc` infinitude: every state has a location absent from
+the heap. (Single cell; matches the freshness used by Iris's `wp_alloc`.) -/
+theorem State.exists_fresh (σ : State) : ∃ l : Loc, σ.get? l = none := by
+  refine ⟨(List.fresh σ.heap.keys).choose, ?_⟩
+  have h := (List.fresh σ.heap.keys).choose_spec
+  show σ.heap[_]? = none
+  exact Std.ExtTreeMap.getElem?_eq_none (fun hm => h (Std.ExtTreeMap.mem_keys.mpr hm))
+
+open ProgramLogic EctxLanguage in
+/-- `allocN n v` with `0 < n` allocates a fresh array. Allocation is
+nondeterministic in the base location, so the continuation must hold for **every**
+valid fresh `l`; the `hfresh` premise witnesses that at least one exists (needed
+for reducibility — discharge it from heap finiteness at the call site). -/
+theorem wp_allocN {n : Int} {v : Val} {σ Q} (hn : 0 < n)
+    (hfresh : ∃ l : Loc, ∀ i : Int, 0 ≤ i → i < n → σ.get? (l + i) = none)
+    (hQ : ∀ l : Loc, (∀ i : Int, 0 ≤ i → i < n → σ.get? (l + i) = none) →
+      Q (.lit (.loc l)) (σ.initHeap l n v)) :
+    wp (.allocN (.ofVal (.lit (.int n))) (.ofVal v)) σ Q := by
+  obtain ⟨l₀, hl₀⟩ := hfresh
+  have hbred : BaseStep.Reducible (Exp.allocN (.ofVal (.lit (.int n))) (.ofVal v), σ) :=
+    ⟨[], _, _, _, BaseStep.allocNS n v σ l₀ hn hl₀⟩
+  refine 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
+  | allocNS _ _ _ l _ hfr =>
+    exact ⟨rfl, by rw [wp_unfold_apply]
+                   exact .inl ⟨.lit (.loc l), ToVal.toVal_coe _, hQ l hfr⟩⟩
+
+/-- Single-cell allocation `ref v` (= `allocN 1 v`): premise-free, since a fresh
+location always exists. The result location is universally quantified. -/
+theorem wp_alloc {v : Val} {σ Q}
+    (hQ : ∀ l : Loc, σ.get? l = none → Q (.lit (.loc l)) (σ.initHeap l 1 v)) :
+    wp (.allocN (.ofVal (.lit (.int 1))) (.ofVal v)) σ Q := by
+  have hl0 : ∀ l : Loc, l + (0 : Int) = l := fun l => by ext; simp
+  refine wp_allocN (by decide) ?_ (fun l hfr => hQ l ?_)
+  · obtain ⟨l, hl⟩ := σ.exists_fresh
+    exact ⟨l, fun i _ h1 => by rw [show i = 0 by omega, hl0]; exact hl⟩
+  · rw [← hl0 l]; exact hfr 0 (by decide) (by decide)
+
+open ProgramLogic EctxLanguage in
+/-- β-reduction: applying a recursive closure substitutes both binders. -/
+theorem wp_beta {f x : Binder} {e1 : Exp} {v2 : Val} {σ Q}
+    (hQ : wp ((e1.subst f (.rec_ f x e1)).subst x v2) σ Q) :
+    wp (.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 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⟩
+
+open ProgramLogic EctxLanguage in
+/-- Recursive closures evaluate to themselves as values. -/
+theorem wp_rec {f x : Binder} {e : Exp} {σ Q}
+    (hQ : Q (.rec_ f x e) σ) : wp (.rec_ f x e) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.rec_ f x e, σ) := ⟨[], _, _, _, BaseStep.recS f x e σ⟩
+  refine 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, by rw [wp_unfold_apply]; exact .inl ⟨_, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- Unary operator evaluation. -/
+theorem wp_unop {op : UnOp} {v v' : Val} {σ Q}
+    (hop : op.eval v = some v') (hQ : Q v' σ) :
+    wp (.unop op (.ofVal v)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.unop op (.ofVal v), σ) :=
+    ⟨[], _, _, _, BaseStep.unOpS op v v' σ hop⟩
+  refine 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, by rw [wp_unfold_apply]; exact .inl ⟨_, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- Binary operator evaluation. -/
+theorem wp_binop {op : BinOp} {v1 v2 v' : Val} {σ Q}
+    (hop : op.eval v1 v2 = some v') (hQ : Q v' σ) :
+    wp (.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 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, by rw [wp_unfold_apply]; exact .inl ⟨_, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- Pairing two values. -/
+theorem wp_pair {v1 v2 : Val} {σ Q} (hQ : Q (.pair v1 v2) σ) :
+    wp (.pair (.ofVal v1) (.ofVal v2)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.pair (.ofVal v1) (.ofVal v2), σ) :=
+    ⟨[], _, _, _, BaseStep.pairS v1 v2 σ⟩
+  refine 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, by rw [wp_unfold_apply]; exact .inl ⟨_, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- First projection. -/
+theorem wp_fst {v1 v2 : Val} {σ Q} (hQ : Q v1 σ) :
+    wp (.fst (.ofVal (.pair v1 v2))) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.fst (.ofVal (.pair v1 v2)), σ) :=
+    ⟨[], _, _, _, BaseStep.fstS v1 v2 σ⟩
+  refine 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, by rw [wp_unfold_apply]; exact .inl ⟨_, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- Second projection. -/
+theorem wp_snd {v1 v2 : Val} {σ Q} (hQ : Q v2 σ) :
+    wp (.snd (.ofVal (.pair v1 v2))) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.snd (.ofVal (.pair v1 v2)), σ) :=
+    ⟨[], _, _, _, BaseStep.sndS v1 v2 σ⟩
+  refine 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, by rw [wp_unfold_apply]; exact .inl ⟨_, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- Left injection. -/
+theorem wp_injL {v : Val} {σ Q} (hQ : Q (.injL v) σ) :
+    wp (.injL (.ofVal v)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.injL (.ofVal v), σ) := ⟨[], _, _, _, BaseStep.injLS v σ⟩
+  refine 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, by rw [wp_unfold_apply]; exact .inl ⟨_, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- Right injection. -/
+theorem wp_injR {v : Val} {σ Q} (hQ : Q (.injR v) σ) :
+    wp (.injR (.ofVal v)) σ Q := by
+  have hbred : BaseStep.Reducible (Exp.injR (.ofVal v), σ) := ⟨[], _, _, _, BaseStep.injRS v σ⟩
+  refine 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, by rw [wp_unfold_apply]; exact .inl ⟨_, ToVal.toVal_coe _, hQ⟩⟩
+
+open ProgramLogic EctxLanguage in
+/-- `case` on a left injection takes the left branch (applied to the payload). -/
+theorem wp_case_injL {v : Val} {e1 e2 σ Q} (hQ : wp (.app e1 (.ofVal v)) σ Q) :
+    wp (.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 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⟩
+
+open ProgramLogic EctxLanguage in
+/-- `case` on a right injection takes the right branch (applied to the payload). -/
+theorem wp_case_injR {v : Val} {e1 e2 σ Q} (hQ : wp (.app e2 (.ofVal v)) σ Q) :
+    wp (.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 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⟩
+
+/-- The value rule: `wp (ofVal v) σ Q ↔ Q v σ`. -/
+@[simp] theorem wp_val {v : Val} {σ Q} : wp (.ofVal v) σ Q ↔ Q v σ := by
+  rw [wp_unfold_apply]
+  constructor
+  · rintro (⟨v', hv', hQ⟩ | ⟨hred, _⟩)
+    · rw [ToVal.toVal_coe] at hv'; cases hv'; exact hQ
+    · exact absurd (toVal_none_of_reducible hred) (by rw [ToVal.toVal_coe]; simp)
+  · exact fun hQ => .inl ⟨v, ToVal.toVal_coe v, hQ⟩
+
+open Lean.Order in
+instance instWPPreExp : Std.Internal.Do.WP Exp Val (State → Prop) Std.Internal.Do.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 Iris.HeapLang
diff --git a/Iris/Iris/HeapLang/VcgenSmokeTest.lean b/Iris/Iris/HeapLang/VcgenSmokeTest.lean
new file mode 100644
index 000000000..c7239e198
--- /dev/null
+++ b/Iris/Iris/HeapLang/VcgenSmokeTest.lean
@@ -0,0 +1,404 @@
+module
+
+import Iris.HeapLang.Omni
+import Iris.HeapLang.Notation
+import Std.Tactic.Do
+
+/-!
+# `@[spec]` lemmas driving `vcgen` over the HeapLang omni-WP
+
+This wires the omni-WP `wp` step rules from `Omni.lean` into the (internal)
+`Std.Internal.Do` verification-condition generator, following the
+"approach 1" recipe: for every syntactic form,
+
+* a **redex** spec, keyed on the fully-evaluated head (operands `.ofVal _`), and
+* one **focus** spec per sub-expression position, expressing HeapLang's
+  right-to-left evaluation order via `wp_bind_fill [ectxItem]`.
+
+All specs are in the engine's `pre ⊑ wp prog post epost` shape.
+
+**Priorities.** Redexes/values fire first (`high`); among the focus specs for a
+constructor the one requiring the *most* already-evaluated positions gets the
+higher priority (`L > M > R`), so `vcgen` never re-focuses a value and the tree
+is walked deterministically. Termination: each focus spec strictly shrinks the
+focused subterm; the value spec is the base case.
+-/
+
+open Iris.HeapLang Lean.Order Std.Internal.Do
+
+namespace Iris.HeapLang.VcgenSmoke
+
+/-! ## Values -/
+
+@[spec high] theorem val_spec (v : Val) (post : Val → State → Prop) (epost : EPost.Nil) :
+    post v ⊑ Std.Internal.Do.wp ((.ofVal v : Exp)) post epost := by
+  intro σ h; exact wp_val.mpr h
+
+/-- Recursive closures are values. -/
+@[spec high] theorem rec_spec (f x : Binder) (e : Exp) (post : Val → State → Prop) (epost : EPost.Nil) :
+    post (.rec_ f x e) ⊑ Std.Internal.Do.wp (Exp.rec_ f x e) post epost := by
+  intro σ h; exact wp_rec h
+
+/-! ## Unary operator -/
+
+@[spec high] theorem unop_redex_spec {op : UnOp} {v v' : Val} (hop : op.eval v = some v')
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    post v' ⊑ Std.Internal.Do.wp (Exp.unop op (.ofVal v)) post epost := by
+  intro σ h; exact wp_unop hop h
+
+@[spec 1000] theorem unop_focus_spec {op : UnOp} {e : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e (fun v => Std.Internal.Do.wp (Exp.unop op (.ofVal v)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.unop op e) post epost := by
+  intro σ h; exact wp_bind_fill [.unOp op] h
+
+/-! ## Binary operator -/
+
+@[spec high] theorem binop_redex_spec {op : BinOp} {v1 v2 v' : Val} (hop : op.eval v1 v2 = some v')
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    post v' ⊑ Std.Internal.Do.wp (Exp.binop op (.ofVal v1) (.ofVal v2)) post epost := by
+  intro σ h; exact wp_binop hop h
+
+@[spec 1200] theorem binop_focusL_spec {op : BinOp} {e1 : Exp} {v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e1 (fun v1 => Std.Internal.Do.wp (Exp.binop op (.ofVal v1) (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.binop op e1 (.ofVal v2)) post epost := by
+  intro σ h; exact wp_bind_fill [.binOpL op v2] h
+
+@[spec 1000] theorem binop_focusR_spec {op : BinOp} {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e2 (fun v2 => Std.Internal.Do.wp (Exp.binop op e1 (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.binop op e1 e2) post epost := by
+  intro σ h; exact wp_bind_fill [.binOpR op e1] h
+
+/-! ## Application (β-reduction) -/
+
+@[spec high] theorem beta_redex_spec {f x : Binder} {e1 : Exp} {v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp ((e1.subst f (.rec_ f x e1)).subst x v2) post epost
+      ⊑ Std.Internal.Do.wp (Exp.app (.ofVal (.rec_ f x e1)) (.ofVal v2)) post epost := by
+  intro σ h; exact wp_beta h
+
+@[spec 1200] theorem app_focusL_spec {e1 : Exp} {v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e1 (fun v1 => Std.Internal.Do.wp (Exp.app (.ofVal v1) (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.app e1 (.ofVal v2)) post epost := by
+  intro σ h; exact wp_bind_fill [.appL v2] h
+
+@[spec 1000] theorem app_focusR_spec {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e2 (fun v2 => Std.Internal.Do.wp (Exp.app e1 (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.app e1 e2) post epost := by
+  intro σ h; exact wp_bind_fill [.appR e1] h
+
+/-! ## Pairs -/
+
+@[spec high] theorem pair_redex_spec {v1 v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    post (.pair v1 v2) ⊑ Std.Internal.Do.wp (Exp.pair (.ofVal v1) (.ofVal v2)) post epost := by
+  intro σ h; exact wp_pair h
+
+@[spec 1200] theorem pair_focusL_spec {e1 : Exp} {v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e1 (fun v1 => Std.Internal.Do.wp (Exp.pair (.ofVal v1) (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.pair e1 (.ofVal v2)) post epost := by
+  intro σ h; exact wp_bind_fill [.pairL v2] h
+
+@[spec 1000] theorem pair_focusR_spec {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e2 (fun v2 => Std.Internal.Do.wp (Exp.pair e1 (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.pair e1 e2) post epost := by
+  intro σ h; exact wp_bind_fill [.pairR e1] h
+
+@[spec high] theorem fst_redex_spec {v1 v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    post v1 ⊑ Std.Internal.Do.wp (Exp.fst (.ofVal (.pair v1 v2))) post epost := by
+  intro σ h; exact wp_fst h
+
+@[spec 1000] theorem fst_focus_spec {e : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e (fun v => Std.Internal.Do.wp (Exp.fst (.ofVal v)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.fst e) post epost := by
+  intro σ h; exact wp_bind_fill [.fst] h
+
+@[spec high] theorem snd_redex_spec {v1 v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    post v2 ⊑ Std.Internal.Do.wp (Exp.snd (.ofVal (.pair v1 v2))) post epost := by
+  intro σ h; exact wp_snd h
+
+@[spec 1000] theorem snd_focus_spec {e : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e (fun v => Std.Internal.Do.wp (Exp.snd (.ofVal v)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.snd e) post epost := by
+  intro σ h; exact wp_bind_fill [.snd] h
+
+/-! ## Sum injections -/
+
+@[spec high] theorem injL_redex_spec {v : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    post (.injL v) ⊑ Std.Internal.Do.wp (Exp.injL (.ofVal v)) post epost := by
+  intro σ h; exact wp_injL h
+
+@[spec 1000] theorem injL_focus_spec {e : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e (fun v => Std.Internal.Do.wp (Exp.injL (.ofVal v)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.injL e) post epost := by
+  intro σ h; exact wp_bind_fill [.injL] h
+
+@[spec high] theorem injR_redex_spec {v : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    post (.injR v) ⊑ Std.Internal.Do.wp (Exp.injR (.ofVal v)) post epost := by
+  intro σ h; exact wp_injR h
+
+@[spec 1000] theorem injR_focus_spec {e : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e (fun v => Std.Internal.Do.wp (Exp.injR (.ofVal v)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.injR e) post epost := by
+  intro σ h; exact wp_bind_fill [.injR] h
+
+/-! ## Conditional (only the scrutinee is evaluated) -/
+
+@[spec high] theorem if_true_spec {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e1 post epost
+      ⊑ Std.Internal.Do.wp (Exp.if (.ofVal (.lit (.bool true))) e1 e2) post epost := by
+  intro σ h; exact wp_if_true h
+
+@[spec high] theorem if_false_spec {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e2 post epost
+      ⊑ Std.Internal.Do.wp (Exp.if (.ofVal (.lit (.bool false))) e1 e2) post epost := by
+  intro σ h; exact wp_if_false h
+
+@[spec 1000] theorem if_focus_spec {e e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e (fun v => Std.Internal.Do.wp (Exp.if (.ofVal v) e1 e2) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.if e e1 e2) post epost := by
+  intro σ h; exact wp_bind_fill [.if e1 e2] h
+
+/-! ## Case (only the scrutinee is evaluated) -/
+
+@[spec high] theorem case_injL_spec {v : Val} {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp (Exp.app e1 (.ofVal v)) post epost
+      ⊑ Std.Internal.Do.wp (Exp.case (.ofVal (.injL v)) e1 e2) post epost := by
+  intro σ h; exact wp_case_injL h
+
+@[spec high] theorem case_injR_spec {v : Val} {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp (Exp.app e2 (.ofVal v)) post epost
+      ⊑ Std.Internal.Do.wp (Exp.case (.ofVal (.injR v)) e1 e2) post epost := by
+  intro σ h; exact wp_case_injR h
+
+@[spec 1000] theorem case_focus_spec {e e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e (fun v => Std.Internal.Do.wp (Exp.case (.ofVal v) e1 e2) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.case e e1 e2) post epost := by
+  intro σ h; exact wp_bind_fill [.case e1 e2] h
+
+/-! ## Heap: allocation
+
+`ref v` (`allocN 1`) is premise-free; general `allocN n` carries `0 < n` and a
+freshness witness as VCs. -/
+
+@[spec high] theorem alloc_spec {v : Val} (post : Val → State → Prop) (epost : EPost.Nil) :
+    (fun σ => ∀ l : Loc, σ.get? l = none → post (.lit (.loc l)) (σ.initHeap l 1 v))
+      ⊑ Std.Internal.Do.wp (Exp.allocN (.ofVal (.lit (.int 1))) (.ofVal v)) post epost := by
+  intro σ h; exact wp_alloc h
+
+@[spec 1300] theorem allocN_spec {n : Int} {v : Val} (post : Val → State → Prop) (epost : EPost.Nil) :
+    (fun σ => 0 < n ∧ (∃ l : Loc, ∀ i : Int, 0 ≤ i → i < n → σ.get? (l + i) = none) ∧
+        ∀ l : Loc, (∀ i : Int, 0 ≤ i → i < n → σ.get? (l + i) = none) →
+          post (.lit (.loc l)) (σ.initHeap l n v))
+      ⊑ Std.Internal.Do.wp (Exp.allocN (.ofVal (.lit (.int n))) (.ofVal v)) post epost := by
+  intro σ h; obtain ⟨hn, hfresh, hQ⟩ := h; exact wp_allocN hn hfresh hQ
+
+@[spec 1200] theorem allocN_focusL_spec {e1 : Exp} {v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e1 (fun v1 => Std.Internal.Do.wp (Exp.allocN (.ofVal v1) (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.allocN e1 (.ofVal v2)) post epost := by
+  intro σ h; exact wp_bind_fill [.allocNL v2] h
+
+@[spec 1000] theorem allocN_focusR_spec {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e2 (fun v2 => Std.Internal.Do.wp (Exp.allocN e1 (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.allocN e1 e2) post epost := by
+  intro σ h; exact wp_bind_fill [.allocNR e1] h
+
+/-! ## Heap: load / free (unary) -/
+
+@[spec high] theorem load_spec {l : Loc} (post : Val → State → Prop) (epost : EPost.Nil) :
+    (fun σ => ∃ v : Val, σ.get? l = some (some v) ∧ post v σ)
+      ⊑ Std.Internal.Do.wp (Exp.load (.ofVal (.lit (.loc l)))) post epost := by
+  intro σ h; obtain ⟨v, hl, hq⟩ := h; exact wp_load hl hq
+
+@[spec 1000] theorem load_focus_spec {e : Exp} (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e (fun v => Std.Internal.Do.wp (Exp.load (.ofVal v)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.load e) post epost := by
+  intro σ h; exact wp_bind_fill [.load] h
+
+@[spec high] theorem free_spec {l : Loc} (post : Val → State → Prop) (epost : EPost.Nil) :
+    (fun σ => ∃ v : Val, σ.get? l = some (some v) ∧ post (.lit .unit) (σ.initHeap l 1 none))
+      ⊑ Std.Internal.Do.wp (Exp.free (.ofVal (.lit (.loc l)))) post epost := by
+  intro σ h; obtain ⟨v, hl, hq⟩ := h; exact wp_free hl hq
+
+@[spec 1000] theorem free_focus_spec {e : Exp} (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e (fun v => Std.Internal.Do.wp (Exp.free (.ofVal v)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.free e) post epost := by
+  intro σ h; exact wp_bind_fill [.free] h
+
+/-! ## Heap: store / xchg / faa (binary) -/
+
+@[spec high] theorem store_spec {l : Loc} {w : Val} (post : Val → State → Prop) (epost : EPost.Nil) :
+    (fun σ => ∃ v : Val, σ.get? l = some (some v) ∧ post (.lit .unit) (σ.initHeap l 1 (some w)))
+      ⊑ Std.Internal.Do.wp (Exp.store (.ofVal (.lit (.loc l))) (.ofVal w)) post epost := by
+  intro σ h; obtain ⟨v, hl, hq⟩ := h; exact wp_store hl hq
+
+@[spec 1200] theorem store_focusL_spec {e1 : Exp} {v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e1 (fun v1 => Std.Internal.Do.wp (Exp.store (.ofVal v1) (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.store e1 (.ofVal v2)) post epost := by
+  intro σ h; exact wp_bind_fill [.storeL v2] h
+
+@[spec 1000] theorem store_focusR_spec {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e2 (fun v2 => Std.Internal.Do.wp (Exp.store e1 (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.store e1 e2) post epost := by
+  intro σ h; exact wp_bind_fill [.storeR e1] h
+
+@[spec high] theorem xchg_spec {l : Loc} {v2 : Val} (post : Val → State → Prop) (epost : EPost.Nil) :
+    (fun σ => ∃ v1 : Val, σ.get? l = some (some v1) ∧ post v1 (σ.initHeap l 1 (some v2)))
+      ⊑ Std.Internal.Do.wp (Exp.xchg (.ofVal (.lit (.loc l))) (.ofVal v2)) post epost := by
+  intro σ h; obtain ⟨v1, hl, hq⟩ := h; exact wp_xchg hl hq
+
+@[spec 1200] theorem xchg_focusL_spec {e1 : Exp} {v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e1 (fun v1 => Std.Internal.Do.wp (Exp.xchg (.ofVal v1) (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.xchg e1 (.ofVal v2)) post epost := by
+  intro σ h; exact wp_bind_fill [.xchgL v2] h
+
+@[spec 1000] theorem xchg_focusR_spec {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e2 (fun v2 => Std.Internal.Do.wp (Exp.xchg e1 (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.xchg e1 e2) post epost := by
+  intro σ h; exact wp_bind_fill [.xchgR e1] h
+
+@[spec high] theorem faa_spec {l : Loc} {i2 : Int} (post : Val → State → Prop) (epost : EPost.Nil) :
+    (fun σ => ∃ i1 : Int, σ.get? l = some (some (.lit (.int i1))) ∧
+        post (.lit (.int i1)) (σ.initHeap l 1 (some (.lit (.int (i1 + i2))))))
+      ⊑ Std.Internal.Do.wp (Exp.faa (.ofVal (.lit (.loc l))) (.ofVal (.lit (.int i2)))) post epost := by
+  intro σ h; obtain ⟨i1, hl, hq⟩ := h; exact wp_faa hl hq
+
+@[spec 1200] theorem faa_focusL_spec {e1 : Exp} {v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e1 (fun v1 => Std.Internal.Do.wp (Exp.faa (.ofVal v1) (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.faa e1 (.ofVal v2)) post epost := by
+  intro σ h; exact wp_bind_fill [.faaL v2] h
+
+@[spec 1000] theorem faa_focusR_spec {e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e2 (fun v2 => Std.Internal.Do.wp (Exp.faa e1 (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.faa e1 e2) post epost := by
+  intro σ h; exact wp_bind_fill [.faaR e1] h
+
+/-! ## Heap: compare-and-exchange (ternary) -/
+
+@[spec high] theorem cmpXchg_spec {l : Loc} {v1 v2 : Val} (post : Val → State → Prop) (epost : EPost.Nil) :
+    (fun σ => ∃ vl : Val, σ.get? l = some (some vl) ∧ vl.compareSafe v1 ∧
+        ∀ b : Bool, decide (vl = v1) = b →
+          post (.pair vl (.lit (.bool b))) (if b then σ.initHeap l 1 (some v2) else σ))
+      ⊑ Std.Internal.Do.wp (Exp.cmpXchg (.ofVal (.lit (.loc l))) (.ofVal v1) (.ofVal v2)) post epost := by
+  intro σ h; obtain ⟨vl, hl, hcmp, hQ⟩ := h; exact wp_cmpXchg hl hcmp hQ
+
+@[spec 1200] theorem cmpXchg_focusL_spec {e0 : Exp} {v1 v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e0 (fun v0 => Std.Internal.Do.wp (Exp.cmpXchg (.ofVal v0) (.ofVal v1) (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.cmpXchg e0 (.ofVal v1) (.ofVal v2)) post epost := by
+  intro σ h; exact wp_bind_fill [.cmpXchgL v1 v2] h
+
+@[spec 1100] theorem cmpXchg_focusM_spec {e0 e1 : Exp} {v2 : Val}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e1 (fun v1 => Std.Internal.Do.wp (Exp.cmpXchg e0 (.ofVal v1) (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.cmpXchg e0 e1 (.ofVal v2)) post epost := by
+  intro σ h; exact wp_bind_fill [.cmpXchgM e0 v2] h
+
+@[spec 1000] theorem cmpXchg_focusR_spec {e0 e1 e2 : Exp}
+    (post : Val → State → Prop) (epost : EPost.Nil) :
+    Std.Internal.Do.wp e2 (fun v2 => Std.Internal.Do.wp (Exp.cmpXchg e0 e1 (.ofVal v2)) post epost) epost
+      ⊑ Std.Internal.Do.wp (Exp.cmpXchg e0 e1 e2) post epost := by
+  intro σ h; exact wp_bind_fill [.cmpXchgR e0 e1] h
+
+/-! ## Demos -/
+
+private def lit (n : Int) : Exp := .ofVal (.lit (.int n))
+private def add (a b : Exp) : Exp := Exp.binop .plus a b
+
+/-- Pure arithmetic, nested redexes: `(1 + 2) + (3 + 4) = 10`. -/
+example : (fun _ => True) ⊑
+    Std.Internal.Do.wp (add (add (lit 1) (lit 2)) (add (lit 3) (lit 4)))
+      (fun r _ => r = .lit (.int 10)) EPost.Nil.mk := by
+  unfold add lit
+  vcgen
+  -- Leftover VCs are the per-node `BinOp.eval` obligations. Each `rfl` also pins
+  -- the intermediate-value metavariable, so a couple of passes (inner nodes
+  -- before the outer one) discharge the whole chain regardless of goal order.
+  all_goals (try rfl)
+  all_goals (try rfl)
+
+/-- Mixing constructs: `fst ((1 + 2), (3 + 4)) = 3`, with a conditional wrapper. -/
+example : (fun _ => True) ⊑
+    Std.Internal.Do.wp
+      (Exp.if (.ofVal (.lit (.bool true)))
+        (Exp.fst (Exp.pair (add (lit 1) (lit 2)) (add (lit 3) (lit 4))))
+        (lit 0))
+      (fun r _ => r = .lit (.int 3)) EPost.Nil.mk := by
+  unfold add lit
+  vcgen
+  all_goals (try rfl)
+  all_goals (try rfl)
+
+/-! ### Larger programs in HeapLang surface syntax
+
+Written with the `hl(…)` notation; `vcgen` symbolically executes the whole
+expression, leaving only the primitive `BinOp.eval` obligations as VCs. -/
+
+/-- Deeper arithmetic, mixed operators: `(10 - 3) * (2 + 2)` ⟶ `28`. -/
+private def arith : Exp := hl((#10 - #3) * (#2 + #2))
+example : (fun _ => True) ⊑
+    Std.Internal.Do.wp arith (fun r _ => r = .lit (.int 28)) EPost.Nil.mk := by
+  unfold arith
+  vcgen
+  all_goals (try rfl)
+  all_goals (try rfl)
+
+/-- Build a nested tuple, then project into it (pairs/`fst`/`snd` bind nothing, so
+`vcgen` handles them fully): `fst (snd (1, (2 * 3, 4 + 5)))` ⟶ `6`. -/
+private def project : Exp := hl(fst(snd((#1, (#2 * #3, #4 + #5)))))
+example : (fun _ => True) ⊑
+    Std.Internal.Do.wp project (fun r _ => r = .lit (.int 6)) EPost.Nil.mk := by
+  unfold project
+  vcgen
+  all_goals (try rfl)
+  all_goals (try rfl)
+
+/-! ### The frontier
+
+`vcgen` here drives *substitution-free* evaluation: arithmetic, pairs/projections,
+injections, and control flow whose scrutinee is a **literal** (as in the `if true …`
+demo above — the dead branch is discarded untouched). Three things are out of reach
+with just these specs, all for the same underlying reason — a spec has to match the
+program **syntactically**:
+
+* **Binding — `let`, `λ`-application, recursion.** β-reduction (`beta_redex_spec`)
+  produces a metalevel `Exp.subst …` term; `vcgen` has no spec for a raw `subst`
+  call, and feeding `Exp.subst` to its simp set makes the substitution's binder
+  handling panic. Needs a normalizing substitution operation `vcgen` can compute.
+* **Control flow on a *computed* condition** (`if x < y then …`). The guard reduces
+  to `.lit (.bool (x < y))`, whose boolean does not syntactically match `if_true`'s
+  `true` / `if_false`'s `false`; `if_focus` then re-fires on the value scrutinee and
+  loops. Needs the comparison to normalize to a literal `true`/`false`.
+* **Mutable state end-to-end.** `ref`/`load`/`store` each step, but the heap
+  side-conditions (`σ.get? l = some …`) are left as VCs — there is no separation-logic
+  frame in this plain `State → Prop` lattice to discharge them automatically. -/
+
+end Iris.HeapLang.VcgenSmoke
diff --git a/Iris/Iris/Instances/IProp/Instance.lean b/Iris/Iris/Instances/IProp/Instance.lean
index 84506015a..5c9ba4831 100644
--- a/Iris/Iris/Instances/IProp/Instance.lean
+++ b/Iris/Iris/Instances/IProp/Instance.lean
@@ -174,14 +174,16 @@ theorem IProp.unfoldi_foldi (x : FF.api τ (IPre FF)) : unfoldi (foldi x) ≡ x
   refine OFE.equiv_dist.mpr fun n => ?_
   refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm ?_
   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 OFunctor.Fix.iso.hom_inv.dist | exact OFunctor.Fix.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.equiv_dist.mpr fun n => ?_
   refine .trans (OFunctor.map_comp (F := FF τ |>.fst) ..).symm ?_
   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 OFunctor.Fix.iso.hom_inv.dist | exact OFunctor.Fix.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/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..37d7e684e 100644
--- a/Iris/lakefile.toml
+++ b/Iris/lakefile.toml
@@ -4,12 +4,12 @@ defaultTargets = ["Iris", "IrisTest"]
 [[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 2544c30c5..b9371ec41 100644
--- a/Iris/lean-toolchain
+++ b/Iris/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.32.0
\ No newline at end of file
+leanprover/lean4:4.33.0-rc1
diff --git a/IrisDoNightly/.github/workflows/lean_action_ci.yml b/IrisDoNightly/.github/workflows/lean_action_ci.yml
new file mode 100644
index 000000000..c48bd6829
--- /dev/null
+++ b/IrisDoNightly/.github/workflows/lean_action_ci.yml
@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v5
+      - uses: leanprover/lean-action@v1
diff --git a/IrisDoNightly/.gitignore b/IrisDoNightly/.gitignore
new file mode 100644
index 000000000..bfb30ec8c
--- /dev/null
+++ b/IrisDoNightly/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/IrisDoNightly/IrisDoNightly.lean b/IrisDoNightly/IrisDoNightly.lean
new file mode 100644
index 000000000..24c6ff66d
--- /dev/null
+++ b/IrisDoNightly/IrisDoNightly.lean
@@ -0,0 +1 @@
+import IrisDoNightly.AxSem
diff --git a/IrisDoNightly/IrisDoNightly/AxSem.lean b/IrisDoNightly/IrisDoNightly/AxSem.lean
new file mode 100644
index 000000000..5e955515d
--- /dev/null
+++ b/IrisDoNightly/IrisDoNightly/AxSem.lean
@@ -0,0 +1,199 @@
+module
+
+public import IrisDoNightly.Semantics
+import Std.Tactic.Do
+import Std.Internal.Do
+
+/-! # Axiomatic Semantics for HeapLang -/
+
+set_option mvcgen.warning false
+
+open Lean.Order
+
+namespace Iris.HeapLang.Ax
+
+/-- A predicate `wp` imbues a fragment of HeapLang with the correct axiomatic semantics.
+In particular, `wp` admits proof rules that obey the evaluation order and effects of HeapLang. -/
+class HeapLangAxioms (wp : Exp → (Val → 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₂) Φ
+
+open HeapLangAxioms Std.Internal.Do
+
+/-- Local notation for a Std.Do weakest precondition. -/
+scoped syntax:max "wp⟦" term:min "⟧" ppSpace term:max : term
+scoped macro_rules
+  | `(wp⟦ $e ⟧ $Φ) => `(Std.Internal.Do.wp $e $Φ Std.Internal.Do.EPost.Nil.mk)
+
+set_option synthInstance.checkSynthOrder false in
+instance instWP_HeapLangAxioms {wp} [HeapLangAxioms wp] :
+    Std.Internal.Do.WP Exp Val Prop EPost.Nil where
+  wpTrans e := ⟨fun Φ _ => wp e Φ⟩
+  wp_trans_monotone _ _ _ _ _ _ := wp_mono
+
+section laws
+
+variable {wp} [HeapLangAxioms wp]
+
+@[spec] theorem spec_val {v : Val} {Φ : Val → Prop} :
+    Φ v ⊑ wp⟦(Exp.ofVal v : Exp)⟧ Φ := by
+  intro h; exact wp_val h
+
+@[spec] theorem spec_rec {f x : Binder} {e : Exp} {Φ : Val → Prop} :
+    Φ (.rec_ f x e) ⊑ wp⟦Exp.rec_ f x e⟧ Φ := by
+  intro h; exact wp_closure h
+
+@[spec] theorem spec_app {e₁ e₂ : Exp} {Φ : Val → Prop} :
+    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₂⟧ Φ := by
+  intro h; exact wp_app h
+
+@[spec] theorem spec_unop {op : UnOp} {e : Exp} {Φ : Val → Prop} :
+    wp⟦e⟧ (fun v => ∃ v', op.eval v = some v' ∧ Φ v')
+      ⊑ wp⟦Exp.unop op e⟧ Φ := by
+  intro h; exact wp_unop h
+
+@[spec] theorem spec_binop {op : BinOp} {e₁ e₂ : Exp} {Φ : Val → Prop} :
+    wp⟦e₂⟧ (fun v₂ => wp⟦e₁⟧ (fun v₁ => ∃ v', op.eval v₁ v₂ = some v' ∧ Φ v'))
+      ⊑ wp⟦Exp.binop op e₁ e₂⟧ Φ := by
+  intro h; exact wp_binop h
+
+@[spec] theorem spec_if {e₀ e₁ e₂ : Exp} {Φ : Val → Prop} :
+    wp⟦e₀⟧ (fun vc => ∃ b, vc = Val.lit (.bool b) ∧ wp⟦if b then e₁ else e₂⟧ Φ)
+      ⊑ wp⟦Exp.if e₀ e₁ e₂⟧ Φ := by
+  intro h; exact wp_cond h
+
+@[spec] theorem spec_pair {e₁ e₂ : Exp} {Φ : Val → Prop} :
+    wp⟦e₂⟧ (fun v₂ => wp⟦e₁⟧ (fun v₁ => Φ (Val.pair v₁ v₂)))
+      ⊑ wp⟦Exp.pair e₁ e₂⟧ Φ := by
+  intro h; exact wp_pair h
+
+@[spec] theorem spec_fst {e : Exp} {Φ : Val → Prop} :
+    wp⟦e⟧ (fun v => ∃ v₁ v₂, v = Val.pair v₁ v₂ ∧ Φ v₁)
+      ⊑ wp⟦Exp.fst e⟧ Φ := by
+  intro h; exact wp_fst h
+
+@[spec] theorem spec_snd {e : Exp} {Φ : Val → Prop} :
+    wp⟦e⟧ (fun v => ∃ v₁ v₂, v = Val.pair v₁ v₂ ∧ Φ v₂)
+      ⊑ wp⟦Exp.snd e⟧ Φ := by
+  intro h; exact wp_snd h
+
+@[spec] theorem spec_injL {e : Exp} {Φ : Val → Prop} :
+    wp⟦e⟧ (fun v => Φ (Val.injL v)) ⊑ wp⟦Exp.injL e⟧ Φ := by
+  intro h; exact wp_injL h
+
+@[spec] theorem spec_injR {e : Exp} {Φ : Val → Prop} :
+    wp⟦e⟧ (fun v => Φ (Val.injR v)) ⊑ wp⟦Exp.injR e⟧ Φ := by
+  intro h; exact wp_injR h
+
+@[spec] theorem spec_case {e₀ e₁ e₂ : Exp} {Φ : Val → Prop} :
+    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₂⟧ Φ := by
+  intro h; exact wp_case h
+
+end laws
+
+
+section demos
+
+variable {wp} [HeapLangAxioms wp]
+
+private def lit (n : Int) : Exp := .ofVal (.lit (.int n))
+private def bool (b : Bool) : Exp := .ofVal (.lit (.bool b))
+private def lam (x : String) (e : Exp) : Exp := .rec_ .anon (.named x) e
+private def add (a b : Exp) : Exp := .binop .plus a b
+
+/-- Substituting into a value-expression is the identity. Needed because the
+default simp set normalises `.val` to `.ofVal` (`val_to_ofVal`), so `substStr`'s
+`.val` case cannot fire on a `.ofVal` leaf; this `rfl` lemma bridges the gap while
+keeping the `vcgen`-friendly `.ofVal` form. -/
+@[local simp] private theorem substStr_ofVal (x : String) (v w : Val) :
+    Exp.substStr x v (Exp.ofVal w) = Exp.ofVal w := rfl
+
+/-! ### Values and pure arithmetic -/
+
+example : True ⊑ wp⟦lit 0⟧ (fun _v => True) := by
+  unfold lit; vcgen
+
+example : True ⊑ wp⟦lit 0⟧ (fun v => v = Val.lit (.int 0)) := by
+  unfold lit; vcgen with finish
+
+attribute [simp] BinOp.eval
+
+/-- `(1 + 2) + (3 + 4) = 10`, nested redexes. -/
+example : True ⊑ wp⟦add (add (lit 1) (lit 2)) (add (lit 3) (lit 4))⟧ (fun v => v = Val.lit (.int 10)) := by
+  simp only [add, lit]
+  vcgen
+  simp [BinOp.eval]
+  vcgen
+  simp
+
+/-! ### Computed conditions -/
+
+/-- The guard is a comparison, not a literal: `if 1 < 2 then 1 else 2 = 1`. -/
+example : True ⊑ wp⟦Exp.if (.binop .lt (lit 1) (lit 2)) (lit 1) (lit 2)⟧ (fun v => v = Val.lit (.int 1)) := by
+  unfold lit
+  vcgen
+  simp [BinOp.eval]
+  vcgen
+
+/-! ### Binders (β-reduction)
+
+The workflow: `vcgen until Exp.subst _ _ _` symbolically executes up to the
+substitution redex, `simp [Exp.subst, Exp.substStr]` computes it, then `vcgen`
+resumes on the concrete substituted program. -/
+
+/-- Identity applied to a literal: `(λx. x) 0`. -/
+example : True ⊑ wp⟦Exp.app (lam "x" (.var "x")) (lit 0)⟧ (fun _v => True) := by
+  simp only [lam, lit]
+  vcgen until Exp.subst _ _ _
+  refine ⟨_, _, _, rfl, ?_⟩
+  simp [Exp.subst, Exp.substStr]
+  vcgen
+
+/-- The bound variable is used in an arithmetic context: `(λx. x + 1) 5 = 6`. -/
+example : True ⊑ wp⟦Exp.app (lam "x" (add (.var "x") (lit 1))) (lit 5)⟧ (fun v => v = Val.lit (.int 6)) := by
+  unfold lam add lit
+  vcgen until Exp.subst _ _ _
+  refine ⟨_, _, _, rfl, ?_⟩
+  simp [Exp.subst, Exp.substStr]
+  vcgen <;> (try simp [BinOp.eval]) <;> (try vcgen) <;> (try simp [BinOp.eval])
+
+/-! ### Products and sums -/
+
+/-- `fst (1 + 2, 3 + 4) = 3`. -/
+example : True ⊑ wp⟦Exp.fst (Exp.pair (add (lit 1) (lit 2)) (add (lit 3) (lit 4)))⟧ (fun v => v = Val.lit (.int 3)) := by
+  unfold add lit
+  vcgen <;> (try simp [BinOp.eval]) <;> (try vcgen) <;> (try simp [BinOp.eval])
+
+end demos
+end Iris.HeapLang.Ax
diff --git a/IrisDoNightly/IrisDoNightly/HeapAxioms.lean b/IrisDoNightly/IrisDoNightly/HeapAxioms.lean
new file mode 100644
index 000000000..3a47edd62
--- /dev/null
+++ b/IrisDoNightly/IrisDoNightly/HeapAxioms.lean
@@ -0,0 +1,159 @@
+module
+
+public import IrisDoNightly.SepLogic
+public import Std.Internal
+public import Std.Tactic.Do
+
+set_option mvcgen.warning false
+
+open Lean.Order
+open Iris.HeapLang
+
+@[expose] public section
+
+namespace Iris.HeapLang.SL
+
+def hpure (φ : Prop) : HProp := fun _ => φ
+def hand (P Q : HProp) : HProp := fun σ => P σ ∧ Q σ
+def hexists {α : Sort _} (P : α → HProp) : HProp := fun σ => ∃ a, P a σ
+def hor (P Q : HProp) : HProp := fun σ => P σ ∨ Q σ
+
+/-! ## The axiomatic interface -/
+
+/-- A predicate `wp` imbues a fragment of HeapLang with the correct separation-logic axiomatic
+semantics. The pure structural fields are `AxSem.HeapLangAxioms` with `→` replaced by `⊑`; the heap
+fields are the small-footprint rules over `↦`. -/
+class HeapLangAxioms (wp : Exp → (Val → HProp) → HProp) where
+  wp_mono : Φ ⊑ Ψ → 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 => hexists fun (f : Binder) => hexists fun (x : Binder) =>
+      hexists fun (body : Exp) => hand (hpure (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 => hexists fun v' => hand (hpure (op.eval v = some v')) (Φ v'))
+      ⊑ wp (Exp.unop op e) Φ
+  wp_binop :
+    wp e₂ (fun v₂ => wp e₁ (fun v₁ => hexists fun v' => hand (hpure (op.eval v₁ v₂ = some v')) (Φ v')))
+      ⊑ wp (Exp.binop op e₁ e₂) Φ
+  wp_cond :
+    wp e₀ (fun vc => hexists fun b => hand (hpure (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 => hexists fun v₁ => hexists fun v₂ => hand (hpure (v = Val.pair v₁ v₂)) (Φ v₁))
+      ⊑ wp (Exp.fst e) Φ
+  wp_snd :
+    wp e (fun v => hexists fun v₁ => hexists fun v₂ => hand (hpure (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 =>
+      hor (hexists fun v => hand (hpure (vc = Val.injL v)) (wp (Exp.app e₁ (Exp.ofVal v)) Φ))
+          (hexists fun v => hand (hpure (vc = Val.injR v)) (wp (Exp.app e₂ (Exp.ofVal v)) Φ)))
+      ⊑ wp (Exp.case e₀ e₁ e₂) Φ
+  wp_load (l : Loc) (w : Val) :
+    pointsTo l w ⊑ wp (Exp.load (Exp.ofVal (Val.lit (.loc l))))
+      (fun v => hand (hpure (v = w)) (pointsTo l w))
+  wp_store (l : Loc) (v w : Val) :
+    pointsTo l v ⊑ wp (Exp.store (Exp.ofVal (Val.lit (.loc l))) (Exp.ofVal w))
+      (fun _ => pointsTo l w)
+  wp_alloc (w : Val) :
+    emp ⊑ wp (Exp.allocN (Exp.ofVal (Val.lit (.int 1))) (Exp.ofVal w))
+      (fun v => hexists fun l => hand (hpure (v = Val.lit (.loc l))) (pointsTo l w))
+  wp_free (l : Loc) (w : Val) :
+    pointsTo l w ⊑ wp (Exp.free (Exp.ofVal (Val.lit (.loc l)))) (fun _ => emp)
+
+open Std.Internal.Do HeapLangAxioms
+
+/-! ## The `Std.Do` `WP` instance -/
+
+set_option synthInstance.checkSynthOrder false in
+instance instWP_SL {wp} [HeapLangAxioms wp] : WP Exp Val HProp EPost.Nil where
+  wpTrans e := ⟨fun Φ _ => wp e Φ⟩
+  wp_trans_monotone _ _ _ _ _ _ hp := wp_mono hp
+
+/-- Local notation for a `Std.Do` weakest precondition. -/
+scoped syntax:max "wp⟦" term:min "⟧" ppSpace term:max : term
+scoped macro_rules
+  | `(wp⟦ $e ⟧ $Φ) => `(Std.Internal.Do.wp $e $Φ Std.Internal.Do.EPost.Nil.mk)
+
+@[grind .] theorem sl_frames {wp} [HeapLangAxioms wp] (e : Exp) (F : HProp) :
+    WP.Frames sepConj e F where
+  conj_wp_le_wp_conj := by sorry
+
+/-! ## The `@[spec]` laws -/
+
+section laws
+variable {wp} [HeapLangAxioms wp]
+
+@[spec] theorem spec_val {v : Val} {Φ : Val → HProp} :
+    Φ v ⊑ wp⟦(Exp.ofVal v : Exp)⟧ Φ := wp_val
+
+@[spec] theorem spec_rec {f x : Binder} {e : Exp} {Φ : Val → HProp} :
+    Φ (.rec_ f x e) ⊑ wp⟦Exp.rec_ f x e⟧ Φ := wp_closure
+
+@[spec] theorem spec_app {e₁ e₂ : Exp} {Φ : Val → HProp} :
+    wp⟦e₂⟧ (fun v₂ => wp⟦e₁⟧ (fun vf => hexists fun (f : Binder) => hexists fun (x : Binder) =>
+        hexists fun (body : Exp) => hand (hpure (vf = Val.rec_ f x body))
+          (wp⟦(body.subst f (.rec_ f x body)).subst x v₂⟧ Φ)))
+      ⊑ wp⟦Exp.app e₁ e₂⟧ Φ := wp_app
+
+@[spec] theorem spec_unop {op : UnOp} {e : Exp} {Φ : Val → HProp} :
+    wp⟦e⟧ (fun v => hexists fun v' => hand (hpure (op.eval v = some v')) (Φ v'))
+      ⊑ wp⟦Exp.unop op e⟧ Φ := wp_unop
+
+@[spec] theorem spec_binop {op : BinOp} {e₁ e₂ : Exp} {Φ : Val → HProp} :
+    wp⟦e₂⟧ (fun v₂ => wp⟦e₁⟧ (fun v₁ => hexists fun v' => hand (hpure (op.eval v₁ v₂ = some v')) (Φ v')))
+      ⊑ wp⟦Exp.binop op e₁ e₂⟧ Φ := wp_binop
+
+@[spec] theorem spec_if {e₀ e₁ e₂ : Exp} {Φ : Val → HProp} :
+    wp⟦e₀⟧ (fun vc => hexists fun b => hand (hpure (vc = Val.lit (.bool b))) (wp⟦if b then e₁ else e₂⟧ Φ))
+      ⊑ wp⟦Exp.if e₀ e₁ e₂⟧ Φ := wp_cond
+
+@[spec] theorem spec_pair {e₁ e₂ : Exp} {Φ : Val → HProp} :
+    wp⟦e₂⟧ (fun v₂ => wp⟦e₁⟧ (fun v₁ => Φ (Val.pair v₁ v₂)))
+      ⊑ wp⟦Exp.pair e₁ e₂⟧ Φ := wp_pair
+
+@[spec] theorem spec_fst {e : Exp} {Φ : Val → HProp} :
+    wp⟦e⟧ (fun v => hexists fun v₁ => hexists fun v₂ => hand (hpure (v = Val.pair v₁ v₂)) (Φ v₁))
+      ⊑ wp⟦Exp.fst e⟧ Φ := wp_fst
+
+@[spec] theorem spec_snd {e : Exp} {Φ : Val → HProp} :
+    wp⟦e⟧ (fun v => hexists fun v₁ => hexists fun v₂ => hand (hpure (v = Val.pair v₁ v₂)) (Φ v₂))
+      ⊑ wp⟦Exp.snd e⟧ Φ := wp_snd
+
+@[spec] theorem spec_injL {e : Exp} {Φ : Val → HProp} :
+    wp⟦e⟧ (fun v => Φ (Val.injL v)) ⊑ wp⟦Exp.injL e⟧ Φ := wp_injL
+
+@[spec] theorem spec_injR {e : Exp} {Φ : Val → HProp} :
+    wp⟦e⟧ (fun v => Φ (Val.injR v)) ⊑ wp⟦Exp.injR e⟧ Φ := wp_injR
+
+@[spec] theorem spec_case {e₀ e₁ e₂ : Exp} {Φ : Val → HProp} :
+    wp⟦e₀⟧ (fun vc =>
+        hor (hexists fun v => hand (hpure (vc = Val.injL v)) (wp⟦Exp.app e₁ (Exp.ofVal v)⟧ Φ))
+            (hexists fun v => hand (hpure (vc = Val.injR v)) (wp⟦Exp.app e₂ (Exp.ofVal v)⟧ Φ)))
+      ⊑ wp⟦Exp.case e₀ e₁ e₂⟧ Φ := wp_case
+
+@[spec] theorem spec_load (l : Loc) (w : Val) :
+    pointsTo l w ⊑ wp⟦Exp.load (Exp.ofVal (Val.lit (.loc l)))⟧
+      (fun v => hand (hpure (v = w)) (pointsTo l w)) := wp_load l w
+
+@[spec] theorem spec_store (l : Loc) (v w : Val) :
+    pointsTo l v ⊑ wp⟦Exp.store (Exp.ofVal (Val.lit (.loc l))) (Exp.ofVal w)⟧
+      (fun _ => pointsTo l w) := wp_store l v w
+
+@[spec] theorem spec_alloc (w : Val) :
+    emp ⊑ wp⟦Exp.allocN (Exp.ofVal (Val.lit (.int 1))) (Exp.ofVal w)⟧
+      (fun v => hexists fun l => hand (hpure (v = Val.lit (.loc l))) (pointsTo l w)) := wp_alloc w
+
+@[spec] theorem spec_free (l : Loc) (w : Val) :
+    pointsTo l w ⊑ wp⟦Exp.free (Exp.ofVal (Val.lit (.loc l)))⟧ (fun _ => emp) := wp_free l w
+
+end laws
+end Iris.HeapLang.SL
diff --git a/IrisDoNightly/IrisDoNightly/Prelude.lean b/IrisDoNightly/IrisDoNightly/Prelude.lean
new file mode 100644
index 000000000..2276dc941
--- /dev/null
+++ b/IrisDoNightly/IrisDoNightly/Prelude.lean
@@ -0,0 +1,169 @@
+module
+
+public import Std.Data.ExtTreeMap
+public import Std.Data.ExtTreeSet
+
+/-!
+# Prelude shims for `IrisDoNightly`
+
+This experimental project ports the HeapLang syntax and operational semantics onto a
+bleeding-edge Lean nightly so that we can play with the `Std.Do` weakest-precondition
+machinery, *without* dragging in the whole Iris algebra/BI stack (which is pinned to an
+older stable toolchain).
+
+Rather than importing `Iris.ProgramLogic.Language`, `Iris.Std.BitOp`,
+`Iris.Std.Infinite`, `Iris.Std.PartialMap`, `Iris.Std.HeapInstances`, … (which transitively
+pull in the entire library), we reproduce here the *small* pieces those files provide that
+the syntax and semantics actually depend on:
+
+* the `Int` bit-wise / shift instances (from `Iris.Std.BitOp`, originally copied from Mathlib);
+* the `InfiniteType` class (from `Iris.Std.Infinite`);
+* the `ToVal` class (from `Iris.ProgramLogic.Language`);
+* a minimal `PartialMap` class together with the `Std.ExtTreeMap` instance
+  (from `Iris.Std.PartialMap` / `Iris.Std.HeapInstances`).
+-/
+
+@[expose] public section
+
+/-! ## Integer bit-wise operations
+
+Copied from `Iris.Std.BitOp` (itself copied from Mathlib). Lean core does not provide
+`AndOp`/`OrOp`/`XorOp`/`ShiftLeft`/`ShiftRight` instances for `Int`, so `BinOp.eval` needs
+them. -/
+
+namespace IrisDoNightly.BitOp
+
+namespace Nat
+
+/-- `ldiff` computes the bitwise "and not" of two natural numbers. -/
+def ldiff : Nat → Nat → Nat :=
+  Nat.bitwise fun a b => a && not b
+
+/-- `bit b` appends the digit `b` to the little end of the binary representation of `n`. -/
+def bit (b : Bool) (n : Nat) : Nat :=
+  cond b (2 * n + 1) (2 * n)
+
+/-- `shiftLeft' b m n` left-shifts `m` `n` times, inserting bit `b` each step. -/
+def shiftLeft' (b : Bool) (m : Nat) : Nat → Nat
+  | 0 => m
+  | n + 1 => bit b (shiftLeft' b m n)
+
+end Nat
+
+namespace Int
+
+open _root_.IrisDoNightly.BitOp.Nat _root_.Int
+
+/-- Bitwise `or` on integers. -/
+def lor : Int → Int → Int
+  | (m : Nat), (n : Nat) => m ||| n
+  | (m : Nat), -[n+1] => -[ldiff n m+1]
+  | -[m+1], (n : Nat) => -[ldiff m n+1]
+  | -[m+1], -[n+1] => -[m &&& n+1]
+
+instance : OrOp Int := ⟨lor⟩
+
+/-- Bitwise `and` on integers. -/
+def land : Int → Int → Int
+  | (m : Nat), (n : Nat) => m &&& n
+  | (m : Nat), -[n+1] => ldiff m n
+  | -[m+1], (n : Nat) => ldiff n m
+  | -[m+1], -[n+1] => -[m ||| n+1]
+
+instance : AndOp Int := ⟨land⟩
+
+/-- Bitwise `xor` on integers. -/
+def xor : Int → Int → Int
+  | (m : Nat), (n : Nat) => (m ^^^ n)
+  | (m : Nat), -[n+1] => -[(m ^^^ n)+1]
+  | -[m+1], (n : Nat) => -[(m ^^^ n)+1]
+  | -[m+1], -[n+1] => (m ^^^ n)
+
+instance : XorOp Int := ⟨xor⟩
+
+/-- Left shift on integers. -/
+instance : ShiftLeft Int where
+  shiftLeft
+  | (m : Nat), (n : Nat) => Nat.shiftLeft' false m n
+  | (m : Nat), -[n+1] => m >>> (Nat.succ n)
+  | -[m+1], (n : Nat) => -[Nat.shiftLeft' true m n+1]
+  | -[m+1], -[n+1] => -[m >>> (Nat.succ n)+1]
+
+/-- Right shift on integers. -/
+instance : ShiftRight Int where
+  shiftRight m n := m <<< (-n)
+
+end Int
+
+end IrisDoNightly.BitOp
+
+-- Bring the `Int` instances into scope everywhere.
+open IrisDoNightly.BitOp.Int
+
+/-! ## Infinite types
+
+Copied from `Iris.Std.Infinite`. -/
+
+/-- A type is *infinite* if there is an injection `Nat → T`. -/
+class InfiniteType (T : Type _) where
+  enum : Nat → T
+  enum_inj : ∀ n m : Nat, enum n = enum m → n = m
+
+instance : InfiniteType Nat where
+  enum := id
+  enum_inj _ _ H := H
+
+/-! ## `ToVal`
+
+Copied from `Iris.ProgramLogic.Language`, minus the `rocq_alias` bookkeeping. -/
+
+namespace Iris.ProgramLogic
+
+class ToVal (Expr : Type _) (Val : outParam (Type _)) where
+  toVal : Expr → Option Val
+  ofVal : Val → Expr
+  /-- If `toVal` is defined for an expression, `ofVal` is its inverse. -/
+  coe_of_toVal_eq_some {e : Expr} {v : Val} : toVal e = some v → ofVal v = e
+  /-- `toVal` is the inverse of `ofVal`. -/
+  toVal_coe (v : Val) : toVal (ofVal v) = some v
+export ToVal (toVal coe_of_toVal_eq_some toVal_coe)
+
+attribute [simp, grind =] ToVal.toVal_coe
+attribute [coe] ToVal.ofVal
+
+namespace ToVal
+
+variable {Expr Val : Type _} [ι : ToVal Expr Val]
+
+instance : Coe Val Expr where coe := ofVal
+
+@[grind! .]
+theorem toVal_eq_iff_coe (e : Expr) (v : Val) : v = e ↔ toVal e = some v :=
+  ⟨(· ▸ toVal_coe v), coe_of_toVal_eq_some⟩
+
+theorem ofVal_inj : ι.ofVal.Injective := by
+  intro x y h
+  simpa [toVal_coe] using congrArg (toVal) h
+
+end ToVal
+end Iris.ProgramLogic
+
+/-! ## Partial maps
+
+A minimal version of `Iris.Std.PartialMap` providing just the `get?`/`insert` operations,
+together with the `Std.ExtTreeMap` instance from `Iris.Std.HeapInstances`, which is all the
+HeapLang semantics needs to model its heap. -/
+
+namespace Iris.Std
+
+class PartialMap (M : Type _ → Type _) (K : outParam (Type _)) where
+  get? : M V → K → Option V
+  insert : M V → K → V → M V
+export PartialMap (get? insert)
+
+instance {K : Type _} [Ord K] [Std.TransOrd K] [Std.LawfulEqOrd K] :
+    PartialMap (Std.ExtTreeMap K · compare) K where
+  get? t k := t[k]?
+  insert t k v := t.alter k (fun _ => some v)
+
+end Iris.Std
diff --git a/IrisDoNightly/IrisDoNightly/SLFrame.lean b/IrisDoNightly/IrisDoNightly/SLFrame.lean
new file mode 100644
index 000000000..eee3cdcdd
--- /dev/null
+++ b/IrisDoNightly/IrisDoNightly/SLFrame.lean
@@ -0,0 +1,110 @@
+module
+
+public import IrisDoNightly.HeapAxioms
+import Lean
+import Std.Internal
+import Std.Tactic.Do
+public meta import Lean.Elab.Tactic.Do.Internal.VCGen.FrameProc
+public meta import Lean.Meta.Sym.Pattern
+
+set_option mvcgen.warning false
+set_option grind.warning false
+
+open Lean Meta Sym Std Std.Internal.Do Lean.Order
+open Iris.HeapLang Iris.HeapLang.SL
+
+@[expose] public section
+
+namespace Iris.HeapLang.SL
+
+/-! ## Separation-logic structural lemmas for the frame split -/
+
+theorem sepConj_mono_r {a b b' : HProp} (h : b ⊑ b') : (sepConj a b) ⊑ (sepConj a b') := by
+  rintro σ ⟨σ₁, σ₂, hd, rfl, ha, hb⟩; exact ⟨σ₁, σ₂, hd, rfl, ha, h _ hb⟩
+
+theorem sepConj_frame_r {pre₀ F R : HProp} (h : pre₀ ⊑ R) : (sepConj pre₀ F) ⊑ (sepConj F R) :=
+  PartialOrder.rel_trans (PartialOrder.rel_of_eq (sepConj_comm pre₀ F)) (sepConj_mono_r h)
+
+@[grind ←] theorem sepConj_comm_le (a b : HProp) : (sepConj a b) ⊑ (sepConj b a) :=
+  PartialOrder.rel_of_eq (sepConj_comm a b)
+
+/-! ## The registered frame procedure for `∗` -/
+
+open Lean.Elab.Tactic.Do.Internal Lean.Elab.Tactic.Do.Internal.VCGen
+
+public meta partial def sepAtoms (e : Expr) : Array Expr :=
+  if e.isAppOf ``sepConj then sepAtoms e.appFn!.appArg! ++ sepAtoms e.appArg!
+  else #[e]
+
+public meta def sepConjFrameProc : FrameInferenceProc := fun _R pre _info specPre => do
+  let mut rest := sepAtoms pre
+  for atom in sepAtoms specPre do
+    let some i ← rest.findIdxM? (isDefEqS atom ·) | return none
+    rest := rest.eraseIdxIfInBounds i
+  if rest.isEmpty then return none
+  return some (rest.pop.foldr (fun a acc => mkApp2 (mkConst ``sepConj) a acc) rest.back!)
+
+@[frameproc] public meta def heapFP : FrameProc where
+  prog := ``Iris.HeapLang.Exp
+  mkOpAppM := fun _ => pure (mkConst ``sepConj)
+  resourceTy := fun _ => pure (mkConst ``HProp)
+  op := { head := ``sepConj, numConst := 0, terminal? := ``sepConj_frame_r }
+  proc := some sepConjFrameProc
+
+theorem le_hexists {α : Sort _} {P : HProp} (Q : α → HProp) (a : α) (h : P ⊑ Q a) :
+    P ⊑ hexists Q := fun σ hσ => ⟨a, h σ hσ⟩
+
+theorem le_hand_pure {P R : HProp} {φ : Prop} (hφ : φ) (h : P ⊑ R) :
+    P ⊑ hand (hpure φ) R := fun σ hσ => ⟨hφ, h σ hσ⟩
+
+section demos
+variable {wp} [HeapLangAxioms wp]
+
+example (l1 l2 : Loc) (a b x : Val) :
+    (l1 ↦ a ∗ l2 ↦ b)
+      ⊑ wp⟦Exp.store (Exp.ofVal (Val.lit (.loc l1))) (Exp.ofVal x)⟧
+        (fun _ => l1 ↦ x ∗ l2 ↦ b) := by
+  vcgen [spec_store] with finish
+
+/-- The same goal with the frame supplied explicitly via the `frames` clause. -/
+example (l1 l2 : Loc) (a b x : Val) :
+    (l1 ↦ a ∗ l2 ↦ b)
+      ⊑ wp⟦Exp.store (Exp.ofVal (Val.lit (.loc l1))) (Exp.ofVal x)⟧
+        (fun _ => l1 ↦ x ∗ l2 ↦ b) := by
+  vcgen [spec_store]
+    frames | Exp.store _ _ => (pointsTo l2 b)
+    with finish
+
+/-- `alloc` yields a fresh cell holding `v`. -/
+example (v : Val) :
+    emp ⊑ wp⟦Exp.allocN (Exp.ofVal (Val.lit (.int 1))) (Exp.ofVal v)⟧
+      (fun r => hexists fun l => hand (hpure (r = Val.lit (.loc l))) (pointsTo l v)) := by
+  vcgen [spec_alloc] with finish
+
+/-- `load` returns the stored value and keeps the cell. -/
+example (l : Loc) (w : Val) :
+    (l ↦ w) ⊑ wp⟦Exp.load (Exp.ofVal (Val.lit (.loc l)))⟧
+      (fun v => hand (hpure (v = w)) (l ↦ w)) := by
+  vcgen [spec_load] with finish
+
+/-- A mixed program that `vcgen` drives end to end: `(λ_. ()) (l := b)` — store `b` into `l`, then
+return unit — carrying the disjoint cell `k ↦ c` untouched across the (framed) store, then a pure
+step. The heap spec is sequenced with a pure value through the application rule; `vcgen` applies the
+frame for the store and reduces the pure tail, leaving only a `∗`-commutativity residual that
+`finish` closes. -/
+example (l k : Loc) (a b c : Val) :
+    ((l ↦ a) ∗ (k ↦ c))
+      ⊑ wp⟦Exp.app (Exp.rec_ .anon .anon (Exp.ofVal (Val.lit .unit)))
+            (Exp.store (Exp.ofVal (Val.lit (.loc l))) (Exp.ofVal b))⟧
+        (fun _ => (l ↦ b) ∗ (k ↦ c)) := by
+  vcgen [spec_store]
+  case vc1 =>
+    refine le_hexists _ .anon (le_hexists _ .anon
+      (le_hexists _ (Exp.ofVal (Val.lit .unit)) (le_hand_pure rfl ?_)))
+    simp only [Exp.subst]
+    vcgen with finish
+  all_goals grind
+
+end demos
+
+end Iris.HeapLang.SL
diff --git a/IrisDoNightly/IrisDoNightly/Semantics.lean b/IrisDoNightly/IrisDoNightly/Semantics.lean
new file mode 100644
index 000000000..dd39d55ad
--- /dev/null
+++ b/IrisDoNightly/IrisDoNightly/Semantics.lean
@@ -0,0 +1,200 @@
+/-
+Copyright (c) 2026 Sergei Stepanenko. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+module
+
+public import IrisDoNightly.Syntax
+public import Std.Data.ExtTreeMap
+public import Std.Data.ExtTreeSet
+
+@[expose] public section
+namespace Iris.HeapLang
+
+open _root_.Std Iris.Std
+
+inductive ECtxItem where
+  | appL (v2 : Val)
+  | appR (e1 : Exp)
+  | unOp (op : UnOp)
+  | binOpL (op : BinOp) (v2 : Val)
+  | binOpR (op : BinOp) (e1 : Exp)
+  | if (e1 e2 : Exp)
+  | pairL (v2 : Val)
+  | pairR (e1 : Exp)
+  | fst
+  | snd
+  | injL
+  | injR
+  | case (e1 e2 : Exp)
+  | allocNL (v2 : Val)
+  | allocNR (e1 : Exp)
+  | free
+  | load
+  | storeL (v2 : Val)
+  | storeR (e1 : Exp)
+  | xchgL (v2 : Val)
+  | xchgR (e1 : Exp)
+  | cmpXchgL (v1 v2 : Val)
+  | cmpXchgM (e0 : Exp) (v2 : Val)
+  | cmpXchgR (e0 e1 : Exp)
+  | faaL (v2 : Val)
+  | faaR (e1 : Exp)
+  | resolveL (ctx : ECtxItem) (v1 v2 : Val)
+  | resolveM (e0 : Exp) (v2 : Val)
+  | resolveR (e0 e1 : Exp)
+  deriving Inhabited, Repr, DecidableEq
+
+def ECtxItem.fill (Ki : ECtxItem) (e : Exp) : Exp :=
+  match Ki with
+  | .appL v2        => .app e (.ofVal v2)
+  | .appR e1        => .app e1 e
+  | .unOp op        => .unop op e
+  | .binOpL op v2   => .binop op e (.ofVal v2)
+  | .binOpR op e1   => .binop op e1 e
+  | .if e1 e2       => .if e e1 e2
+  | .pairL v2       => .pair e (.ofVal v2)
+  | .pairR e1       => .pair e1 e
+  | .fst            => .fst e
+  | .snd            => .snd e
+  | .injL           => .injL e
+  | .injR           => .injR e
+  | .case e1 e2     => .case e e1 e2
+  | .allocNL v2     => .allocN e (.ofVal v2)
+  | .allocNR e1     => .allocN e1 e
+  | .free           => .free e
+  | .load           => .load e
+  | .storeL v2      => .store e (.ofVal v2)
+  | .storeR e1      => .store e1 e
+  | .xchgL v2       => .xchg e (.ofVal v2)
+  | .xchgR e1       => .xchg e1 e
+  | .cmpXchgL v1 v2 => .cmpXchg e (.ofVal v1) (.ofVal v2)
+  | .cmpXchgM e0 v2 => .cmpXchg e0 e (.ofVal v2)
+  | .cmpXchgR e0 e1 => .cmpXchg e0 e1 e
+  | .faaL v2        => .faa e (.ofVal v2)
+  | .faaR e1        => .faa e1 e
+  | .resolveL K v1 v2 => .resolve (K.fill e) (.ofVal v1) (.ofVal v2)
+  | .resolveM e0 v2   => .resolve e0 e (.ofVal v2)
+  | .resolveR e0 e1   => .resolve e0 e1 e
+
+structure State where
+  heap : Std.ExtTreeMap Loc (Option Val)
+  usedProphId : Std.ExtTreeSet ProphId
+
+instance : Inhabited State := ⟨.empty, .empty⟩
+
+abbrev Observation := ProphId × (Val × Val)
+
+def UnOp.eval : UnOp → Val → Option Val
+  | .neg,   .lit (.bool b) => some (.lit (.bool (!b)))
+  | .minus, .lit (.int n)  => some (.lit (.int (-n)))
+  | _,      _              => none
+
+def BinOp.eval : BinOp → Val → Val → Option Val
+  | .plus,   .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1 + n2)))
+  | .minus,  .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1 - n2)))
+  | .mult,   .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1 * n2)))
+  | .tdiv,   .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1.tdiv n2)))
+  | .tmod,   .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1.tmod n2)))
+  | .and,    .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1 &&& n2)))
+  | .or,     .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1 ||| n2)))
+  | .xor,    .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1 ^^^ n2)))
+  | .and,    .lit (.bool b1), .lit (.bool b2) => some (.lit (.bool (b1 && b2)))
+  | .or,     .lit (.bool b1), .lit (.bool b2) => some (.lit (.bool (b1 || b2)))
+  | .xor,    .lit (.bool b1), .lit (.bool b2) => some (.lit (.bool (b1 ^^ b2)))
+  | .shiftl, .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1 <<< n2)))
+  | .shiftr, .lit (.int n1),  .lit (.int n2)  => some (.lit (.int (n1 >>> n2)))
+  | .le,     .lit (.int n1),  .lit (.int n2)  => some (.lit (.bool (n1 ≤ n2)))
+  | .lt,     .lit (.int n1),  .lit (.int n2)  => some (.lit (.bool (n1 < n2)))
+  | .eq,     v1,              v2              =>
+      if v1.compareSafe v2 then some (.lit (.bool (v1 == v2))) else none
+  | .offset, .lit (.loc l),   .lit (.int n)   => some (.lit (.loc (l + n)))
+  | _,       _,               _               => none
+
+abbrev State.initHeap (σ : State) (l : Loc) (n : Int) (v : Option Val) : State :=
+  { σ with heap := (List.range n.toNat).foldl
+            (fun h (i : Nat) => Std.insert
+                (M := fun V => Std.ExtTreeMap Loc V compare)
+                h (l + (i : Int)) v) σ.heap }
+
+abbrev State.get? (σ : State) (l : Loc) : Option (Option Val) :=
+    PartialMap.get? (M := fun V => Std.ExtTreeMap Loc V compare) σ.heap l
+
+inductive BaseStep : Exp → State → List Observation → Exp → State → List Exp → Prop where
+  | recS (f x : Binder) (e : Exp) (σ : State) :
+      BaseStep (.rec_ f x e) σ [] (.ofVal (.rec_ f x e)) σ []
+  | pairS (v1 v2 : Val) (σ : State) :
+      BaseStep (.pair (.ofVal v1) (.ofVal v2)) σ [] (.ofVal (.pair v1 v2)) σ []
+  | injLS (v : Val) (σ : State) :
+      BaseStep (.injL (.ofVal v)) σ [] (.ofVal (.injL v)) σ []
+  | injRS (v : Val) (σ : State) :
+      BaseStep (.injR (.ofVal v)) σ [] (.ofVal (.injR v)) σ []
+  | betaS (f x : Binder) (e1 : Exp) (v2 : Val) (e' : Exp) (σ : State) :
+      e' = (e1.subst f (.rec_ f x e1)).subst x v2 →
+      BaseStep (.app (.ofVal (.rec_ f x e1)) (.ofVal v2)) σ [] e' σ []
+  | unOpS (op : UnOp) (v v' : Val) (σ : State) :
+      op.eval v = some v' →
+      BaseStep (.unop op (.ofVal v)) σ [] (.ofVal v') σ []
+  | binOpS (op : BinOp) (v1 v2 v' : Val) (σ : State) :
+      op.eval v1 v2 = some v' →
+      BaseStep (.binop op (.ofVal v1) (.ofVal v2)) σ [] (.ofVal v') σ []
+  | ifTrueS (e1 e2 : Exp) (σ : State) :
+      BaseStep (.if (.ofVal (.lit (.bool true))) e1 e2) σ [] e1 σ []
+  | ifFalseS (e1 e2 : Exp) (σ : State) :
+      BaseStep (.if (.ofVal (.lit (.bool false))) e1 e2) σ [] e2 σ []
+  | fstS (v1 v2 : Val) (σ : State) :
+      BaseStep (.fst (.ofVal (Val.pair v1 v2))) σ [] (.ofVal v1) σ []
+  | sndS (v1 v2 : Val) (σ : State) :
+      BaseStep (.snd (.ofVal (Val.pair v1 v2))) σ [] (.ofVal v2) σ []
+  | caseLS (v : Val) (e1 e2 : Exp) (σ : State) :
+      BaseStep (.case (.ofVal (.injL v)) e1 e2) σ [] (.app e1 (.ofVal v)) σ []
+  | caseRS (v : Val) (e1 e2 : Exp) (σ : State) :
+      BaseStep (.case (.ofVal (.injR v)) e1 e2) σ [] (.app e2 (.ofVal v)) σ []
+  | allocNS (n : Int) (v : Val) (σ : State) (l : Loc) :
+      0 < n →
+      (∀ i : Int, 0 ≤ i → i < n → σ.get? (l + i) = none) →
+      BaseStep (.allocN (.ofVal (.lit (.int n))) (.ofVal v)) σ
+               [] (.ofVal (.lit (.loc l))) (σ.initHeap l n v) []
+  | freeS (l : Loc) (v : Val) (σ : State) :
+      σ.get? l = some v →
+      BaseStep (.free (.ofVal (.lit (.loc l)))) σ
+               [] (.ofVal (.lit .unit)) (σ.initHeap l 1 none) []
+  | loadS (l : Loc) (v : Val) (σ : State) :
+      σ.get? l = some v →
+      BaseStep (.load (.ofVal (.lit (.loc l)))) σ [] (.ofVal v) σ []
+  | storeS (l : Loc) (v w : Val) (σ : State) :
+      σ.get? l = some v →
+      BaseStep (.store (.ofVal (.lit (.loc l))) (.ofVal w)) σ
+               [] (.ofVal (.lit .unit)) (σ.initHeap l 1 w) []
+  | xchgS (l : Loc) (v1 v2 : Val) (σ : State) :
+      σ.get? l = some v1 →
+      BaseStep (.xchg (.ofVal (.lit (.loc l))) (.ofVal v2)) σ
+               [] (.ofVal v1) (σ.initHeap l 1 v2) []
+  | cmpXchgS (l : Loc) (v1 v2 vl : Val) (σ : State) (b : Bool) :
+      σ.get? l = some vl →
+      vl.compareSafe v1 →
+      decide (vl = v1) = b →
+      BaseStep (.cmpXchg (.ofVal (.lit (.loc l))) (.ofVal v1) (.ofVal v2)) σ
+               []
+               (.ofVal (.pair vl (.lit (.bool b))))
+               (if b then (σ.initHeap l 1 v2) else σ) []
+  | faaS (l : Loc) (i1 i2 : Int) (σ : State) :
+      σ.get? l = some (some (.lit (.int i1))) →
+      BaseStep (.faa (.ofVal (.lit (.loc l))) (.ofVal (.lit (.int i2)))) σ
+               [] (.ofVal (.lit (.int i1)))
+               (σ.initHeap l 1 (some (.lit (.int (i1 + i2))))) []
+  | forkS (e : Exp) (σ : State) :
+      BaseStep (.fork e) σ [] (.ofVal (.lit .unit)) σ [e]
+  | newProphS (σ : State) (p : ProphId) :
+      ¬ σ.usedProphId.contains p →
+      BaseStep .newProph σ
+               [] (.ofVal (.lit (.prophecy p)))
+               { σ with usedProphId := σ.usedProphId.insert p } []
+  | resolveS (p : ProphId) (v : Val) (e : Exp) (σ : State) (w : Val) (σ' : State)
+             (κs : List Observation) (ts : List Exp) :
+      BaseStep e σ κs (.ofVal v) σ' ts →
+      σ.usedProphId.contains p →
+      BaseStep (.resolve e (.ofVal (.lit (.prophecy p))) (.ofVal w)) σ
+               (κs ++ [(p, (v, w))]) (.ofVal v) σ' ts
+
+end Iris.HeapLang
diff --git a/IrisDoNightly/IrisDoNightly/SepAlgebra.lean b/IrisDoNightly/IrisDoNightly/SepAlgebra.lean
new file mode 100644
index 000000000..ed2846020
--- /dev/null
+++ b/IrisDoNightly/IrisDoNightly/SepAlgebra.lean
@@ -0,0 +1,97 @@
+module
+
+public import IrisDoNightly.Semantics
+public import Std.Data.ExtTreeMap
+public import Std.Data.ExtTreeSet
+
+@[expose] public section
+namespace Iris.HeapLang
+
+open _root_.Std Iris.Std
+
+/-! ## The separation algebra operations -/
+
+def State.disjoint (σ₁ σ₂ : State) : Prop :=
+  ∀ l, σ₁.get? l = none ∨ σ₂.get? l = none
+
+def State.union (σ₁ σ₂ : State) : State where
+  heap := σ₁.heap ∪ σ₂.heap
+  usedProphId := σ₁.usedProphId ∪ σ₂.usedProphId
+
+def State.emp : State := ⟨∅, ∅⟩
+
+def State.single (l : Loc) (v : Option Val) : State :=
+  ⟨(∅ : ExtTreeMap Loc (Option Val) compare).insert l v, ∅⟩
+
+scoped infixl:70 " #ₕ " => State.disjoint
+scoped infixl:65 " ⊎ₕ " => State.union
+
+theorem State.ext' {σ₁ σ₂ : State}
+    (hh : σ₁.heap = σ₂.heap) (hu : σ₁.usedProphId = σ₂.usedProphId) : σ₁ = σ₂ := by
+  cases σ₁; cases σ₂; subst hh; subst hu; rfl
+
+theorem State.get?_eq (σ : State) (l : Loc) : σ.get? l = σ.heap[l]? := rfl
+
+@[simp] theorem State.get?_union (σ₁ σ₂ : State) (l : Loc) :
+    (σ₁ ⊎ₕ σ₂).get? l = (σ₂.get? l).or (σ₁.get? l) := by
+  simp only [State.get?_eq, State.union]
+  exact ExtTreeMap.getElem?_union
+
+@[simp] theorem State.get?_emp (l : Loc) : State.emp.get? l = none := by
+  simp only [State.get?_eq, State.emp]
+  exact ExtTreeMap.getElem?_empty
+
+theorem State.get?_single (l l' : Loc) (v : Option Val) :
+    (State.single l v).get? l' = if l' = l then some v else none := by
+  simp only [State.get?_eq, State.single]
+  rw [ExtTreeMap.getElem?_insert, ExtTreeMap.getElem?_empty]
+  by_cases h : l = l'
+  · subst h; simp [compare_self]
+  · rw [if_neg (by simpa [compare_eq_iff_eq] using h), if_neg (fun hc => h hc.symm)]
+
+theorem State.union_none_iff (σ₁ σ₂ : State) (l : Loc) :
+    (σ₁ ⊎ₕ σ₂).get? l = none ↔ σ₁.get? l = none ∧ σ₂.get? l = none := by
+  simp only [State.get?_union, Option.or_eq_none_iff]
+  exact And.comm
+
+theorem State.disjoint_comm {σ₁ σ₂ : State} (h : σ₁ #ₕ σ₂) : σ₂ #ₕ σ₁ :=
+  fun l => (h l).symm
+
+theorem State.union_comm {σ₁ σ₂ : State} (h : σ₁ #ₕ σ₂) : σ₁ ⊎ₕ σ₂ = σ₂ ⊎ₕ σ₁ := by
+  apply State.ext'
+  · ext l
+    simp only [State.union, ExtTreeMap.getElem?_union]
+    rcases h l with hl | hl <;> simp only [State.get?_eq] at hl <;> simp [hl]
+  · show σ₁.usedProphId ∪ σ₂.usedProphId = σ₂.usedProphId ∪ σ₁.usedProphId
+    ext k; simp only [ExtTreeSet.mem_union_iff]; exact Or.comm
+
+theorem State.union_assoc (σ₁ σ₂ σ₃ : State) :
+    (σ₁ ⊎ₕ σ₂) ⊎ₕ σ₃ = σ₁ ⊎ₕ (σ₂ ⊎ₕ σ₃) := by
+  apply State.ext'
+  · ext l; simp only [State.union, ExtTreeMap.getElem?_union, Option.or_assoc]
+  · show (σ₁.usedProphId ∪ σ₂.usedProphId) ∪ σ₃.usedProphId
+        = σ₁.usedProphId ∪ (σ₂.usedProphId ∪ σ₃.usedProphId)
+    ext k; simp only [ExtTreeSet.mem_union_iff]; exact or_assoc
+
+theorem State.disjoint_union_left {σ₁ σ₂ σ₃ : State} :
+    (σ₁ ⊎ₕ σ₂) #ₕ σ₃ ↔ σ₁ #ₕ σ₃ ∧ σ₂ #ₕ σ₃ := by
+  simp only [State.disjoint, State.union_none_iff]
+  grind
+
+theorem State.disjoint_union_right {σ₁ σ₂ σ₃ : State} :
+    σ₁ #ₕ (σ₂ ⊎ₕ σ₃) ↔ σ₁ #ₕ σ₂ ∧ σ₁ #ₕ σ₃ := by
+  simp only [State.disjoint, State.union_none_iff]
+  grind
+
+theorem State.emp_disjoint (σ : State) : State.emp #ₕ σ :=
+  fun l => Or.inl (State.get?_emp l)
+
+theorem State.emp_union (σ : State) : State.emp ⊎ₕ σ = σ := by
+  apply State.ext'
+  · ext l
+    simp only [State.union, State.emp, ExtTreeMap.getElem?_union, ExtTreeMap.getElem?_empty,
+      Option.or_none]
+  · show State.emp.usedProphId ∪ σ.usedProphId = σ.usedProphId
+    ext k; simp only [State.emp, ExtTreeSet.mem_union_iff, ExtTreeSet.not_mem_empty, false_or]
+
+end Iris.HeapLang
diff --git a/IrisDoNightly/IrisDoNightly/SepLogic.lean b/IrisDoNightly/IrisDoNightly/SepLogic.lean
new file mode 100644
index 000000000..c76b0a904
--- /dev/null
+++ b/IrisDoNightly/IrisDoNightly/SepLogic.lean
@@ -0,0 +1,101 @@
+module
+
+public import IrisDoNightly.SepAlgebra
+public import Std.Internal
+public import Std.Tactic.Do
+
+@[expose] public section
+
+open Lean.Order Std Std.Internal.Do Std.Internal.Do.CompleteLattice
+open Iris.HeapLang
+
+namespace Iris.HeapLang
+
+/-! ## Heap assertions -/
+
+def HProp : Type := State → Prop
+
+instance : CompleteLattice HProp := inferInstanceAs (CompleteLattice (State → Prop))
+
+/-! ## The separation-logic connectives -/
+
+def emp : HProp := fun σ => σ = State.emp
+def pointsTo (l : Loc) (w : Val) : HProp := fun σ => σ = State.single l (some w)
+def sepConj (P Q : HProp) : HProp :=
+  fun σ => ∃ σ₁ σ₂, σ₁ #ₕ σ₂ ∧ σ = σ₁ ⊎ₕ σ₂ ∧ P σ₁ ∧ Q σ₂
+def wand (P Q : HProp) : HProp :=
+  fun σ => ∀ σ', σ #ₕ σ' → P σ' → Q (σ ⊎ₕ σ')
+
+scoped notation:70 l:max " ↦ " v:max => pointsTo l v
+scoped infixr:65 " ∗ " => sepConj
+scoped infixr:60 " -∗ " => wand
+
+theorem emp_sepConj (a : HProp) : (sepConj emp a) = a := by
+  funext σ
+  apply propext
+  constructor
+  · rintro ⟨σ₁, σ₂, _, rfl, rfl, ha⟩
+    rwa [State.emp_union]
+  · intro ha
+    exact ⟨State.emp, σ, State.emp_disjoint σ, (State.emp_union σ).symm, rfl, ha⟩
+
+theorem sepConj_assoc (a b c : HProp) :
+    (sepConj (sepConj a b) c) = (sepConj a (sepConj b c)) := by
+  funext σ
+  apply propext
+  constructor
+  · rintro ⟨_, σ₃, hd, rfl, ⟨σ₁, σ₂, hd12, rfl, ha, hb⟩, hc⟩
+    obtain ⟨hd13, hd23⟩ := State.disjoint_union_left.mp hd
+    exact ⟨σ₁, σ₂ ⊎ₕ σ₃, State.disjoint_union_right.mpr ⟨hd12, hd13⟩,
+      State.union_assoc σ₁ σ₂ σ₃, ha, σ₂, σ₃, hd23, rfl, hb, hc⟩
+  · rintro ⟨σ₁, _, hd, rfl, ha, ⟨σ₂, σ₃, hd23, rfl, hb, hc⟩⟩
+    obtain ⟨hd12, hd13⟩ := State.disjoint_union_right.mp hd
+    exact ⟨σ₁ ⊎ₕ σ₂, σ₃, State.disjoint_union_left.mpr ⟨hd13, hd23⟩,
+      (State.union_assoc σ₁ σ₂ σ₃).symm, ⟨σ₁, σ₂, hd12, rfl, ha, hb⟩, hc⟩
+
+theorem sepConj_comm (a b : HProp) : (sepConj a b) = (sepConj b a) := by
+  funext σ; apply propext
+  constructor <;>
+    · rintro ⟨σ₁, σ₂, hd, rfl, hp, hq⟩
+      exact ⟨σ₂, σ₁, State.disjoint_comm hd, State.union_comm hd, hq, hp⟩
+
+/-! ## `∗` preserves sups and its upper adjoint is the wand -/
+
+/-- Pointwise characterization of the sup on `HProp`. -/
+theorem hprop_sup_apply (s : HProp → Prop) (σ : State) :
+    CompleteLattice.sup s σ = ∃ f, s f ∧ f σ := by
+  apply propext
+  constructor
+  · exact fun hh => sup_le s (x := fun σ => ∃ f, s f ∧ f σ)
+      (fun f hf σ' hfσ' => ⟨f, hf, hfσ'⟩) σ hh
+  · rintro ⟨f, hf, hfσ⟩; exact le_sup (c := s) hf σ hfσ
+
+instance (F : HProp) : PreservesSup (sepConj F) where
+  map_sup s := by
+    funext σ
+    apply propext
+    simp only [sepConj, hprop_sup_apply]
+    constructor
+    · rintro ⟨σ₁, σ₂, hd, rfl, hF, x, hx, hxσ₂⟩
+      exact ⟨sepConj F x, ⟨x, hx, rfl⟩, σ₁, σ₂, hd, rfl, hF, hxσ₂⟩
+    · rintro ⟨f, ⟨x, hx, rfl⟩, σ₁, σ₂, hd, rfl, hF, hxσ₂⟩
+      exact ⟨σ₁, σ₂, hd, rfl, hF, x, hx, hxσ₂⟩
+
+/-- The counit of the adjunction `F ∗ · ⊣ F -∗ ·`. -/
+theorem sepConj_wand_le (F b : HProp) : (sepConj F (wand F b)) ⊑ b := by
+  rintro σ ⟨σ₁, σ₂, hd, rfl, hF, hw⟩
+  have := hw σ₁ (State.disjoint_comm hd) hF
+  rwa [State.union_comm (State.disjoint_comm hd)] at this
+
+/-- The upper adjoint of `F ∗ ·` is the magic wand `F -∗ ·`. -/
+theorem sepConj_upperAdjoint (F b : HProp) :
+    PreservesSup.upperAdjoint (sepConj F) b = (wand F b) := by
+  apply PartialOrder.rel_antisymm
+  · unfold PreservesSup.upperAdjoint
+    apply sup_le
+    intro x hx σ hxσ σ' hdisj hF
+    apply hx (σ ⊎ₕ σ')
+    exact ⟨σ', σ, State.disjoint_comm hdisj, State.union_comm hdisj, hF, hxσ⟩
+  · exact PreservesSup.le_upperAdjoint (sepConj F) (sepConj_wand_le F b)
+
+end Iris.HeapLang
diff --git a/IrisDoNightly/IrisDoNightly/Syntax.lean b/IrisDoNightly/IrisDoNightly/Syntax.lean
new file mode 100644
index 000000000..169427fd7
--- /dev/null
+++ b/IrisDoNightly/IrisDoNightly/Syntax.lean
@@ -0,0 +1,247 @@
+/-
+Copyright (c) 2026 Michael Sammler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Sammler
+-/
+module
+
+public import IrisDoNightly.Prelude
+
+@[expose] public section
+namespace Iris.HeapLang
+
+@[ext]
+structure Loc where
+  mk ::
+  n : Int
+deriving Inhabited, Repr, DecidableEq
+
+instance : InfiniteType Loc where
+  enum n := .mk n
+  enum_inj n m := by grind
+
+instance : Ord Loc where
+  compare l₁ l₂ := compare l₁.n l₂.n
+
+instance : Std.TransOrd Loc where
+  eq_swap := by
+    intros l₁ l₂; unfold compare; unfold instOrdLoc; simp;
+    apply Int.instTransOrd.eq_swap
+  isLE_trans := by
+    intros l₁ l₂ l₃; unfold compare; unfold instOrdLoc; simp;
+    apply Int.instTransOrd.isLE_trans
+
+instance : Std.LawfulEqOrd Loc where
+  eq_of_compare := by
+    intros l₁ l₂; unfold compare; unfold instOrdLoc; simp;
+    intros h; ext; assumption
+
+instance : HAdd Loc Int Loc where
+  hAdd l i := ⟨l.n + i⟩
+
+instance : Zero Loc where
+  zero := ⟨0⟩
+
+@[simp]
+theorem loc_add_n (l : Loc) n :
+  (l + n).n = l.n + n := by simp [HAdd.hAdd]
+
+@[ext]
+structure ProphId where
+  mk ::
+  n : Nat
+deriving Inhabited, Repr, DecidableEq
+
+instance : Ord ProphId where
+  compare l₁ l₂ := compare l₁.n l₂.n
+
+instance : Std.TransOrd ProphId where
+  eq_swap := by
+    intros l₁ l₂; unfold compare; unfold instOrdProphId; simp;
+    apply Nat.instTransOrd.eq_swap
+  isLE_trans := by
+    intros l₁ l₂ l₃; unfold compare; unfold instOrdProphId; simp;
+    apply Nat.instTransOrd.isLE_trans
+
+instance : Std.LawfulEqOrd ProphId where
+  eq_of_compare := by
+    intros l₁ l₂; unfold compare; unfold instOrdProphId; simp;
+    intros h; ext; assumption
+
+instance : InfiniteType ProphId where
+  enum n := .mk n
+  enum_inj n m := by grind
+
+inductive Binder where
+  | anon
+  | named (name : String)
+deriving Inhabited, Repr, DecidableEq
+
+inductive BaseLit where
+  | int (n : Int)
+  | bool (b : Bool)
+  | unit
+  | poison
+  | loc (l : Loc)
+  | prophecy (p : ProphId)
+deriving Inhabited, Repr, DecidableEq
+
+inductive UnOp where
+  | neg
+  | minus
+deriving Inhabited, Repr, DecidableEq
+
+inductive BinOp where
+  /- We use "tdiv" and "tmod" instead of "div" and "mod" to
+      better match the behavior of 'real' languages:
+      e.g., in Rust, -30 / -4 == 7. ("div" would return 8.) -/
+  | plus | minus | mult | tdiv | tmod /- arithmetic -/
+  | and | or | xor /- bitwise -/
+  | shiftl | shiftr /- shifts -/
+  | le | lt | eq /- relations -/
+  | offset /- pointer offset -/
+deriving Inhabited, Repr, DecidableEq
+
+mutual
+  inductive Exp : Type where
+    /- values -/
+    -- This constructor should not be used directly. Use Exp.ofVal instead.
+    | val (v : Val)
+    /- Base lambda calculus -/
+    | var (x : String)
+    | rec_ (f x : Binder) (e : Exp)
+    | app (e₁ e₂ : Exp)
+    /- Base types and their operations -/
+    | unop (op : UnOp) (e : Exp)
+    | binop (op : BinOp) (e₁ e₂ : Exp)
+    | if (e₀ e₁ e₂ : Exp)
+    /- Products -/
+    | pair (e₁ e₂ : Exp)
+    | fst (e : Exp)
+    | snd (e : Exp)
+    /- Sums -/
+    | injL (e : Exp)
+    | injR (e : Exp)
+    | case (e₀ e₁ e₂ : Exp)
+    /- Heap -/
+    | allocN (e₁ e₂ : Exp) /- array length, initial value -/
+    | free (e : Exp)
+    | load (e : Exp)
+    | store (e₁ e₂ : Exp)
+    | cmpXchg (e₀ e₁ e₂ : Exp) /- compare exchange -/
+    | xchg (e₁ e₂ : Exp) /- exchange -/
+    | faa (e₁ e₂ : Exp) /- fetch and add -/
+    /- Concurrency -/
+    | fork (e : Exp)
+    /- Prophecy -/
+    | newProph
+    | resolve (e₀ e₁ e₂ : Exp)
+  deriving Inhabited, Repr, DecidableEq
+  inductive Val : Type where
+    | lit (l : BaseLit)
+    | rec_ (f x : Binder) (e : Exp)
+    | pair (v₁ v₂ : Val)
+    | injL (v : Val)
+    | injR (v : Val)
+  deriving Inhabited, Repr, DecidableEq
+end
+
+def Exp.isVal : Exp → Bool
+  | .val _ => true
+  | _ => false
+
+instance instToVal : ProgramLogic.ToVal Exp Val where
+  toVal
+  | .val v => some v
+  | _ => none
+  ofVal := .val
+  coe_of_toVal_eq_some {e v} h := by
+    cases e <;> simp_all
+  toVal_coe _ := rfl
+
+namespace Exp
+export ProgramLogic.ToVal (ofVal)
+end Exp
+
+@[simp]
+theorem val_to_ofVal : Exp.val = Exp.ofVal := rfl
+
+instance : Coe Nat BaseLit where
+  coe n := .int n
+
+instance : Coe Int BaseLit where
+  coe n := .int n
+
+instance : Coe Bool BaseLit where
+  coe b := .bool b
+
+instance : Coe Loc BaseLit where
+  coe l := .loc l
+
+instance : Coe ProphId BaseLit where
+  coe p := .prophecy p
+
+instance : Coe Unit BaseLit where
+  coe _ := .unit
+
+attribute [coe] BaseLit.int BaseLit.bool BaseLit.loc BaseLit.prophecy
+
+def Exp.substStr (x : String) (v : Val) (e : Exp) : Exp :=
+  match e with
+  | .val _ => e
+  | .var x' => if x == x' then .val v else e
+  | .rec_ f x' e => .rec_ f x' $ if .named x != f && .named x != x' then e.substStr x v else e
+  | .app e₁ e₂ => .app (e₁.substStr x v) (e₂.substStr x v)
+  | .unop op e' => .unop op (e'.substStr x v)
+  | .binop op e₁ e₂ => .binop op (e₁.substStr x v) (e₂.substStr x v)
+  | .if e₀ e₁ e₂ => .if (e₀.substStr x v) (e₁.substStr x v) (e₂.substStr x v)
+  | .pair e₁ e₂ => .pair (e₁.substStr x v) (e₂.substStr x v)
+  | .fst e' => .fst (e'.substStr x v)
+  | .snd e' => .snd (e'.substStr x v)
+  | .injL e' => .injL (e'.substStr x v)
+  | .injR e' => .injR (e'.substStr x v)
+  | .case e₀ e₁ e₂ => .case (e₀.substStr x v) (e₁.substStr x v) (e₂.substStr x v)
+  | .allocN e₁ e₂ => .allocN (e₁.substStr x v) (e₂.substStr x v)
+  | .free e' => .free (e'.substStr x v)
+  | .load e' => .load (e'.substStr x v)
+  | .store e₁ e₂ => .store (e₁.substStr x v) (e₂.substStr x v)
+  | .cmpXchg e₀ e₁ e₂ => .cmpXchg (e₀.substStr x v) (e₁.substStr x v) (e₂.substStr x v)
+  | .xchg e₁ e₂ => .xchg (e₁.substStr x v) (e₂.substStr x v)
+  | .faa e₁ e₂ => .faa (e₁.substStr x v) (e₂.substStr x v)
+  | .fork e' => .fork (e'.substStr x v)
+  | .newProph => .newProph
+  | .resolve e₀ e₁ e₂ => .resolve (e₀.substStr x v) (e₁.substStr x v) (e₂.substStr x v)
+
+def Exp.subst (x : Binder) (v : Val) (e : Exp) : Exp :=
+  if let .named x := x then Exp.substStr x v e else e
+
+def BaseLit.isUnboxed : BaseLit → Bool
+  | .prophecy _ | .poison => false
+  | _ => true
+
+def Val.isUnboxed : Val → Bool
+  | .lit l => l.isUnboxed
+  | .injL (.lit l) => l.isUnboxed
+  | .injR (.lit l) => l.isUnboxed
+  | _ => false
+
+def Val.compareSafe (v1 v2 : Val) : Bool :=
+  v1.isUnboxed || v2.isUnboxed
+
+section Derived
+def Exp.stuck : Exp := Exp.app (.ofVal $ .lit $ .int 0) (.ofVal $ .lit $ .int 0)
+
+@[simp]
+theorem Exp.stuck_subst {x v} : Exp.substStr x v Exp.stuck = Exp.stuck := by
+  simp [Exp.stuck, Exp.substStr]
+  simp only [substStr, ofVal]
+
+def Exp.assert (e : Exp) := Exp.if e (.ofVal $ .lit .unit) Exp.stuck
+
+@[simp]
+theorem Exp.assert_subst {x v} e :
+    Exp.substStr x v (Exp.assert e) = Exp.assert (Exp.substStr x v e) := by
+  simp [Exp.assert, Exp.substStr]
+  simp only [substStr, ofVal]
+
+end Derived
diff --git a/IrisDoNightly/README.md b/IrisDoNightly/README.md
new file mode 100644
index 000000000..8027cc63d
--- /dev/null
+++ b/IrisDoNightly/README.md
@@ -0,0 +1 @@
+# IrisDoNightly
\ No newline at end of file
diff --git a/IrisDoNightly/lake-manifest.json b/IrisDoNightly/lake-manifest.json
new file mode 100644
index 000000000..7b20bee1c
--- /dev/null
+++ b/IrisDoNightly/lake-manifest.json
@@ -0,0 +1,6 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "IrisDoNightly",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/IrisDoNightly/lakefile.toml b/IrisDoNightly/lakefile.toml
new file mode 100644
index 000000000..ad6096e75
--- /dev/null
+++ b/IrisDoNightly/lakefile.toml
@@ -0,0 +1,6 @@
+name = "IrisDoNightly"
+version = "0.1.0"
+defaultTargets = ["IrisDoNightly"]
+
+[[lean_lib]]
+name = "IrisDoNightly"
diff --git a/IrisDoNightly/lean-toolchain b/IrisDoNightly/lean-toolchain
new file mode 100644
index 000000000..592d7440f
--- /dev/null
+++ b/IrisDoNightly/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2026-07-24