Obs.lean

-- LEGACY: statement target of pre-rebuild theorems; compiles, refuses what
-- it does not implement, gains no consumers; deleted when re-founded.
import LeanModels.Core.Order
import LeanModels.Python.Logic

/-!
# Fuel monotonicity and cross-fuel determinism (`LeanModels.Python`)

The enabling theorems for the `Obs` spine (docs/spec-surface.md §10): adding
fuel never changes a decided (non-`timeout`) interpreter result. This is what
makes the fuel parameter a pure implementation detail — any two runs that
decide, at any two fuels, decide identically, so `CallsTo` is functional and
the strengthened partial judgment `~~>` becomes stateable.

Since the H1 core re-shape the mutual block is `Run`-typed (state is data:
the decided outcome CONTAINS the final `FrameState`/`World`, and
monotonicity is in fuel only — a decided state survives fuel increase
exactly like a decided value), and the public `callFunction` is a
non-recursive wrapper. Structure:

* `Res.le` (`x ⊑ y`) — the flat approximation order on public results, and
  `Run.le` (`x ⊑ʳ y`) — the same order on `Run`-typed outcomes. Fuel-indexed
  runs form a chain in them.
* `fuelMono` — THE theorem: one conjunction over all nine functions of the
  interpreter's mutual block (`evalExpr`, `evalExprs`, `evalBoolChain`,
  `evalCompareChain`, `execStmt`, `execStmts`, `execWhile`, `callIn`,
  `execFor`), proved by a single induction on fuel. Each case is symbolic
  execution of one interpreter step, glued by the congruence lemmas
  `Run.le_bind` / `Run.le_ite` / `Run.le_withLocals` / `Run.le_toWorld`
  (every fuel-free helper is `⊑ʳ`-reflexive, every recursive call is the
  induction hypothesis at the decremented fuel).
* `evalExpr_mono` … `callIn_mono`, `execFor_mono` — the per-function
  corollaries in implication form, and `callFunction_mono` — the public
  monotonicity, derived through the wrapper decomposition (thaw and freeze
  are fuel-free; the only fuel inside the wrapper is `callIn`'s).
* `callFunction_det` — cross-fuel determinism; `CallsTo.functional` /
  `CallsTo.not_raises` — the spec-level consequences.
* `PyOut` / `Obs` — the observation spine itself (docs/spec-surface.md §10):
  the four-way outcome partition of a call, with fuel confined inside the
  judgment; `Obs.det` (at most one outcome, stuck *messages included*) and
  `Obs.total` (at least one, classically), hence `Obs.existsUnique` — the
  outcome is a well-defined denotation of the call.
-/

namespace LeanModels.Python

/-! ## The approximation order on results -/

/-- Flat approximation order on public interpreter results: `x ⊑ y` iff `x`
is `timeout` (the run gave up) or `x = y` (the run decided, and `y` agrees). -/
protected def Res.le {α : Type} (x y : Res α) : Prop :=
  x = .timeout ∨ x = y

@[inherit_doc] scoped infix:50 " ⊑ " => Res.le

theorem Res.le_iff {α : Type} {x y : Res α} :
    x ⊑ y ↔ (x = .timeout ∨ x = y) := Iff.rfl

theorem Res.le_refl {α : Type} (x : Res α) : x ⊑ x := Or.inr rfl

theorem Res.timeout_le {α : Type} (y : Res α) : (.timeout : Res α) ⊑ y :=
  Or.inl rfl

/-- A decided (non-`timeout`) lower bound is already the value: `⊑` collapses
to equality. This is the extraction step of every `_mono` corollary. -/
theorem Res.le_eq {α : Type} {x y : Res α} (h : x ⊑ y) (hx : x ≠ .timeout) :
    x = y := (Res.le_iff.mp h).resolve_left hx

/-- **`Res.le` IS Core's flat order** (`LeanModels/Core/Order.lean`), and this
`Iff.rfl` is the whole bridge. Stated as an iff rather than as a redefinition on
purpose: `Res.le`'s spelling, its `⊑` notation and its consumers all stay put,
and the tree gains the shared name additively. The congruences below stay
tier-local — `Sv.Res` and `Python.Res` are different types, so `le_bind` and
`le_ite` are each tier's own. -/
theorem Res.le_iff_flatLe {α : Type} {x y : Res α} :
    x ⊑ y ↔ FlatLe .timeout x y := Iff.rfl

/-- Congruence of `⊑` under `bind`: run the prefix (IH), then the
continuation pointwise (IH again, or reflexivity for fuel-free tails). -/
theorem Res.le_bind {α β : Type} {x x' : Res α} {f f' : α → Res β}
    (hx : x ⊑ x') (hf : ∀ a, f a ⊑ f' a) : (x >>= f) ⊑ (x' >>= f') := by
  rcases hx with h | h
  · subst h; exact Or.inl rfl
  · subst h
    cases x with
    | ok a => exact hf a
    | exn e => exact Or.inr rfl
    | timeout => exact Or.inl rfl
    | unsupported msg => exact Or.inr rfl

/-- Congruence of `⊑` under `if`: same condition on both sides, each branch
by its own proof. -/
theorem Res.le_ite {α : Type} {c : Prop} [Decidable c] {x x' y y' : Res α}
    (hx : x ⊑ x') (hy : y ⊑ y') :
    (if c then x else y) ⊑ (if c then x' else y') := by
  by_cases h : c
  · simpa only [if_pos h] using hx
  · simpa only [if_neg h] using hy

/-! ## The approximation order on `Run`-typed outcomes

State is data: `x ⊑ʳ y` compares whole outcomes — final state, value, error,
message and all. `fuelMono` shows every function of the mutual block is
monotone in fuel wrt `⊑ʳ`: a run that decided keeps its exact outcome
(state included) at any higher fuel. -/

/-- Flat approximation order on `Run`-typed outcomes. -/
protected def Run.le {σ α : Type} (x y : Run σ α) : Prop :=
  x = .timeout ∨ x = y

@[inherit_doc] scoped infix:50 " ⊑ʳ " => Run.le

theorem Run.le_iff {σ α : Type} {x y : Run σ α} :
    x ⊑ʳ y ↔ (x = .timeout ∨ x = y) := Iff.rfl

theorem Run.le_refl {σ α : Type} (x : Run σ α) : x ⊑ʳ x := Or.inr rfl

theorem Run.timeout_le {σ α : Type} (y : Run σ α) :
    (.timeout : Run σ α) ⊑ʳ y := Or.inl rfl

/-- A decided (non-`timeout`) lower bound is already the outcome. -/
theorem Run.le_eq {σ α : Type} {x y : Run σ α} (h : x ⊑ʳ y)
    (hx : x ≠ .timeout) : x = y := (Run.le_iff.mp h).resolve_left hx

/-- The same bridge for the state-carrying order — the fourth instance of the
one shape. -/
theorem Run.le_iff_flatLe {σ α : Type} {x y : Run σ α} :
    x ⊑ʳ y ↔ FlatLe .timeout x y := Iff.rfl

/-- Congruence of `⊑ʳ` under `Run.bind`: run the prefix (IH), then the
continuation pointwise at every intermediate state. -/
theorem Run.le_bind {σ α β : Type} {x x' : Run σ α} {f f' : σ → α → Run σ β}
    (hx : x ⊑ʳ x') (hf : ∀ s a, f s a ⊑ʳ f' s a) : x.bind f ⊑ʳ x'.bind f' := by
  rcases hx with h | h
  · subst h; exact Or.inl rfl
  · subst h
    cases x with
    | ok s a => exact hf s a
    | exn s e => exact Or.inr rfl
    | timeout => exact Or.inl rfl
    | unsupported msg => exact Or.inr rfl

theorem flattenStarRun_mono {r r' : Run FrameState (List RVal)}
    (h : r ⊑ʳ r') : flattenStarRun r ⊑ʳ flattenStarRun r' := by
  exact Run.le_bind h (fun st vs => Run.le_refl _)

/-- Congruence of `⊑ʳ` under `Run.bindE` (the exceptions tier: the
stepper's close-on-exn-through-resume continuation — `fuelMono`'s glue
for the one `bindE` consumer). -/
theorem Run.le_bindE {σ α β : Type} {x x' : Run σ α} {f f' : σ → α → Run σ β}
    {g g' : σ → PyErr → Run σ β} (hx : x ⊑ʳ x')
    (hf : ∀ s a, f s a ⊑ʳ f' s a) (hg : ∀ s e, g s e ⊑ʳ g' s e) :
    x.bindE f g ⊑ʳ x'.bindE f' g' := by
  rcases hx with h | h
  · subst h; exact Or.inl rfl
  · subst h
    cases x with
    | ok s a => exact hf s a
    | exn s e => exact hg s e
    | timeout => exact Or.inl rfl
    | unsupported msg => exact Or.inr rfl

/-- Congruence of `⊑ʳ` under `if`. -/
theorem Run.le_ite {σ α : Type} {c : Prop} [Decidable c] {x x' y y' : Run σ α}
    (hx : x ⊑ʳ x') (hy : y ⊑ʳ y') :
    (if c then x else y) ⊑ʳ (if c then x' else y') := by
  by_cases h : c
  · simpa only [if_pos h] using hx
  · simpa only [if_neg h] using hy

/-- Congruence of `⊑ʳ` under `Run.withLocals` (the nested-call splice). -/
theorem Run.le_withLocals {α : Type} {l : REnv} {x x' : Run World α}
    (h : x ⊑ʳ x') : Run.withLocals l x ⊑ʳ Run.withLocals l x' := by
  rcases h with h | h
  · subst h; exact Or.inl rfl
  · subst h; exact Or.inr rfl

/-- Congruence of `⊑ʳ` under `Run.toWorld` (the call-return projection). -/
theorem Run.le_toWorld {α : Type} {x x' : Run FrameState α}
    (h : x ⊑ʳ x') : Run.toWorld x ⊑ʳ Run.toWorld x' := by
  rcases h with h | h
  · subst h; exact Or.inl rfl
  · subst h; exact Or.inr rfl

/-- Congruence of `⊑`→`⊑ʳ` under `Run.liftRes` (the fueled helper splice:
`evalCompareOpH` is fuel-dependent since H1-proper). -/
theorem Run.le_liftRes {σ α : Type} {s : σ} {x y : Res α} (h : x ⊑ y) :
    Run.liftRes s x ⊑ʳ Run.liftRes s y := by
  rcases h with h | h
  · subst h; exact Or.inl rfl
  · subst h; exact Or.inr rfl

/-! ## Dict-equality fuel monotonicity (the `heapEq` mutual block)

`heapEq` is the only fueled helper outside the interpreter's mutual block
(dict `==` recurses through stored values). Its monotonicity is what lets
`fuelMono`'s compare-chain case splice it. -/

/-- Fuel monotonicity for the `heapEq`/`heapEqList`/`heapEqEntries` block,
one conjunction, by induction on fuel. -/
theorem heapEqMono (fuel : Nat) :
    (∀ (h : Heap) (active : List (Addr × Addr)) (a b : RVal) (fuel' : Nat),
      fuel ≤ fuel' → heapEq h fuel active a b ⊑ heapEq h fuel' active a b) ∧
    (∀ (h : Heap) (active : List (Addr × Addr)) (as bs : List RVal) (fuel' : Nat),
      fuel ≤ fuel' → heapEqList h fuel active as bs ⊑ heapEqList h fuel' active as bs) ∧
    (∀ (h : Heap) (active : List (Addr × Addr)) (left right : List (RVal × RVal))
        (fuel' : Nat), fuel ≤ fuel' →
      heapEqEntries h fuel active left right ⊑ heapEqEntries h fuel' active left right) := by
  induction fuel with
  | zero =>
    refine ⟨?_, ?_, ?_⟩
    · exact fun h active a b fuel' _ => Or.inl (by simp [heapEq])
    · exact fun h active as bs fuel' _ => Or.inl (by simp [heapEqList])
    · exact fun h active l r fuel' _ => Or.inl (by simp [heapEqEntries])
  | succ fuel ih =>
    obtain ⟨ihE, ihL, ihN⟩ := ih
    refine ⟨?_, ?_, ?_⟩
    · intro h active a b fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases a <;> cases b <;> simp only [heapEq] <;>
          try exact Res.le_refl _
        -- remaining: tuple/tuple, listV/listV, the tuple/namedtuple square
        -- (elementwise), ref/ref (dicts)
        case tuple.tuple xs ys => exact ihL h active xs.toList ys.toList k hk
        case listV.listV xs ys => exact ihL h active xs.toList ys.toList k hk
        case ntuple.ntuple tn1 fs1 xs tn2 fs2 ys =>
          exact ihL h active xs.toList ys.toList k hk
        case ntuple.tuple tn1 fs1 xs ys =>
          exact ihL h active xs.toList ys.toList k hk
        case tuple.ntuple xs tn2 fs2 ys =>
          exact ihL h active xs.toList ys.toList k hk
        case ref.ref x y =>
          cases hmx : instanceEqMarkerH h (.ref x) with
          | some bx => exact Res.le_refl _
          | none =>
            cases hmy : instanceEqMarkerH h (.ref y) with
            | some bval => exact Res.le_refl _
            | none =>
              simp only [hmx, hmy]
              refine Res.le_ite (Res.le_refl _) (Res.le_ite (Res.le_refl _) ?_)
              cases hx : Heap.get? h x with
              | none =>
                cases Heap.get? h y <;> exact Res.le_refl _
              | some o1 =>
                cases Heap.get? h y with
                | none => cases o1 <;> simp [heapEq, Res.le_iff]
                | some o2 =>
                  cases o1 with
                  | cell cv => cases o2 <;> exact Res.le_refl _
                  | dict es v1 =>
                    cases o2 with
                    | dict fs v2 =>
                      exact Res.le_ite (ihN h ((x, y) :: active) es.toList fs.toList k hk)
                        (Res.le_refl _)
                    | list ys => exact Res.le_refl _
                    | dictView da kind => exact Res.le_refl _
                    | «instance» ci attrs => exact Res.le_refl _
                    | generator qn lo kk stt => exact Res.le_refl _
                    | cell cv => exact Res.le_refl _
                    | closure nm ps ao lo' hg ig bd cap => exact Res.le_refl _
                    | pyset zs => exact Res.le_refl _
                  | list xs =>
                    cases o2 with
                    | dict fs v2 => exact Res.le_refl _
                    | list ys =>
                      exact Res.le_ite (ihL h ((x, y) :: active) xs.toList ys.toList k hk)
                        (Res.le_refl _)
                    | dictView da kind => exact Res.le_refl _
                    | «instance» ci attrs => exact Res.le_refl _
                    | generator qn lo kk stt => exact Res.le_refl _
                    | cell cv => exact Res.le_refl _
                    | closure nm ps ao lo' hg ig bd cap => exact Res.le_refl _
                    | pyset zs => exact Res.le_refl _
                  | dictView da kind =>
                    cases o2 with
                    | dictView da₂ kind₂ =>
                      cases kind <;> cases kind₂ <;> exact Res.le_refl _
                    | _ => simp [heapEq, Res.le_iff]
                  | «instance» ci attrs => cases o2 <;> exact Res.le_refl _
                  | generator qn lo kk stt => cases o2 <;> exact Res.le_refl _
                  | closure nm ps ao lo' hg ig bd cap =>
                    cases o2 <;> exact Res.le_refl _
                  | pyset zs => cases o2 <;> exact Res.le_refl _
    · intro h active as bs fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases as with
        | nil => cases bs <;> (simp only [heapEqList]; exact Res.le_refl _)
        | cons a as' =>
          cases bs with
          | nil => simp only [heapEqList]; exact Res.le_refl _
          | cons b bs' =>
            simp only [heapEqList]
            exact Res.le_bind (ihE h active a b k hk) fun e =>
              Res.le_ite (ihL h active as' bs' k hk) (Res.le_refl _)
    · intro h active l r fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases l with
        | nil => simp only [heapEqEntries]; exact Res.le_refl _
        | cons kv rest =>
          obtain ⟨kk, vv⟩ := kv
          simp only [heapEqEntries]
          cases dictFind r kk with
          | none => exact Res.le_refl _
          | some w =>
            exact Res.le_bind (ihE h active vv w k hk) fun e =>
              Res.le_ite (ihN h active rest r k hk) (Res.le_refl _)

/-- Fuel monotonicity of the H2 list-membership scan (elementwise
`heapEq` splices). -/
theorem heapContainsScan_mono {h : Heap} {fuel : Nat} {x : RVal}
    {l : List RVal} {fuel' : Nat} (hf : fuel ≤ fuel') :
    heapContainsScan h fuel x l ⊑ heapContainsScan h fuel' x l := by
  induction l with
  | nil => exact Res.le_refl _
  | cons v vs ih =>
    simp only [heapContainsScan]
    exact Res.le_bind ((heapEqMono fuel).1 h [] v x fuel' hf)
      fun e => Res.le_ite (Res.le_refl _) ih

/-- Fuel monotonicity of membership in a live `dict_items` view. -/
theorem dictItemContainsList_mono {h : Heap} {fuel : Nat}
    {es : Array (RVal × RVal)} {probe : List RVal} {fuel' : Nat}
    (hf : fuel ≤ fuel') :
    dictItemContainsList h fuel es probe ⊑ dictItemContainsList h fuel' es probe := by
  cases probe with
  | nil => exact Res.le_refl _
  | cons key rest =>
    cases rest with
    | nil => exact Res.le_refl _
    | cons value tail =>
      cases tail with
      | nil =>
        simp only [dictItemContainsList]
        by_cases hk : hashableKey key
        · cases hd : dictFind es.toList key with
          | none => simp [hk, hd]; exact Res.le_refl _
          | some stored =>
            simp [hk, hd]
            exact (heapEqMono fuel).1 h [] stored value fuel' hf
        · simp [hk]; exact Res.le_refl _
      | cons extra tail' => exact Res.le_refl _

theorem dictItemContains_mono {h : Heap} {fuel : Nat}
    {es : Array (RVal × RVal)} {probe : RVal} {fuel' : Nat}
    (hf : fuel ≤ fuel') :
    dictItemContains h fuel es probe ⊑ dictItemContains h fuel' es probe := by
  cases probe with
  | tuple xs => exact dictItemContainsList_mono (probe := xs.toList) hf
  | ntuple tn fields xs =>
      exact dictItemContainsList_mono (probe := xs.toList) hf
  | none => exact Res.le_refl _
  | ellipsis => exact Res.le_refl _
  | bool b => exact Res.le_refl _
  | int n => exact Res.le_refl _
  | float value => exact Res.le_refl _
  | str s => exact Res.le_refl _
  | bytes xs => exact Res.le_refl _
  | listV xs => exact Res.le_refl _
  | rangeV lo hi step => exact Res.le_refl _
  | ref a => exact Res.le_refl _

/-- Fuel monotonicity for `setDedup` (H7+ set construction): the
element-equality scans thread the fuel; the accumulator generalizes. -/
theorem setDedup_mono {h : Heap} {fuel fuel' : Nat} {xs : List RVal}
    (hf : fuel ≤ fuel') :
    ∀ acc, setDedup h fuel acc xs ⊑ setDedup h fuel' acc xs := by
  induction xs with
  | nil => intro acc; exact Res.le_refl _
  | cons v vs ih =>
    intro acc
    simp only [setDedup]
    refine Res.le_ite ?_ (Res.le_refl _)
    exact Res.le_bind (heapContainsScan_mono hf) fun dup =>
      Res.le_ite (ih _) (ih _)

/-- Fuel monotonicity of heap-container membership. -/
theorem heapContains_mono {h : Heap} {fuel : Nat} {a : Addr} {k : RVal}
    {fuel' : Nat} (hf : fuel ≤ fuel') :
    heapContains h fuel a k ⊑ heapContains h fuel' a k := by
  simp only [heapContains]
  cases Heap.get? h a with
  | none => exact Res.le_refl _
  | some o =>
    cases o with
    | dict es v => exact Res.le_refl _
    | list xs => exact heapContainsScan_mono hf
    | dictView da kind =>
      cases hv : Heap.get? h da with
      | none => simp [dictViewEntries, hv, Res.le_iff]
      | some obj =>
        cases obj with
        | dict es ver =>
          cases kind with
          | keys => simp [dictViewEntries, hv, Res.le_iff]
          | values =>
            simpa [dictViewEntries, hv] using
              (heapContainsScan_mono (h := h) (fuel := fuel) (fuel' := fuel')
                (x := k) (l := (dictViewElems es .values).toList) hf)
          | items =>
            simpa [dictViewEntries, hv] using
              (dictItemContains_mono (h := h) (fuel := fuel) (fuel' := fuel')
                (es := es) (probe := k) hf)
        | _ => simp [dictViewEntries, hv, Res.le_iff]
    | «instance» ci attrs => exact Res.le_refl _
    | generator qn lo kk stt => exact Res.le_refl _
    | cell cv => exact Res.le_refl _
    | closure nm ps ao lo' hg ig bd cap => exact Res.le_refl _
    | pyset zs => exact Res.le_ite (heapContainsScan_mono hf) (Res.le_refl _)

/-- Fuel monotonicity of the heap deep-freeze (`freezeH`/`freezeListH`),
one conjunction by induction on fuel — the freeze leg of the public
wrapper's monotonicity decomposition (docs/memory-model.md v2). -/
theorem freezeHMono (fuel : Nat) :
    (∀ (h : Heap) (path : List Addr) (v : RVal) (fuel' : Nat), fuel ≤ fuel' →
      RVal.freezeH h fuel path v ⊑ RVal.freezeH h fuel' path v) ∧
    (∀ (h : Heap) (path : List Addr) (l : List RVal) (fuel' : Nat), fuel ≤ fuel' →
      RVal.freezeListH h fuel path l ⊑ RVal.freezeListH h fuel' path l) := by
  induction fuel with
  | zero =>
    refine ⟨?_, ?_⟩
    · exact fun h path v fuel' _ => Or.inl (by simp [RVal.freezeH])
    · exact fun h path l fuel' _ => Or.inl (by simp [RVal.freezeListH])
  | succ fuel ih =>
    obtain ⟨ihV, ihL⟩ := ih
    refine ⟨?_, ?_⟩
    · intro h path v fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases v <;> simp only [RVal.freezeH] <;> try exact Res.le_refl _
        case listV xs =>
          exact Res.le_bind (ihL h path xs.toList k hk) fun vs => Res.le_refl _
        case tuple xs =>
          exact Res.le_bind (ihL h path xs.toList k hk) fun vs => Res.le_refl _
        case ref a =>
          refine Res.le_ite (Res.le_refl _) ?_
          cases Heap.get? h a with
          | none => exact Res.le_refl _
          | some o =>
            cases o with
            | dict es v => exact Res.le_refl _
            | dictView da kind => exact Res.le_refl _
            | «instance» ci attrs => exact Res.le_refl _
            | generator qn lo kk stt => exact Res.le_refl _
            | cell cv => exact Res.le_refl _
            | closure nm ps ao lo' hg ig bd cap => exact Res.le_refl _
            | pyset zs => exact Res.le_refl _
            | list xs =>
              exact Res.le_bind (ihL h (a :: path) xs.toList k hk)
                fun vs => Res.le_refl _
    · intro h path l fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases l with
        | nil => simp only [RVal.freezeListH]; exact Res.le_refl _
        | cons v vs =>
          simp only [RVal.freezeListH]
          exact Res.le_bind (ihV h path v k hk) fun v' =>
            Res.le_bind (ihL h path vs k hk) fun vs' => Res.le_refl _

/-- Fuel monotonicity of container membership (H5 iteration): a str
receiver is pure, every element-scanning receiver splices the H2 scan. -/
theorem valContains_mono {h : Heap} {fuel : Nat} {a b : RVal}
    {fuel' : Nat} (hf : fuel ≤ fuel') :
    valContains h fuel a b ⊑ valContains h fuel' a b := by
  cases b <;> simp only [valContains] <;> try exact Res.le_refl _
  case ref d => exact heapContains_mono hf
  case listV xs => exact heapContainsScan_mono hf
  case tuple xs => exact heapContainsScan_mono hf
  case ntuple tn fs xs => exact heapContainsScan_mono hf

/-- Fuel monotonicity of the heap-aware comparison step. -/
theorem evalCompareOpH_mono {h : Heap} {fuel : Nat} {op : CmpOp} {a b : RVal}
    {fuel' : Nat} (hf : fuel ≤ fuel') :
    evalCompareOpH h fuel op a b ⊑ evalCompareOpH h fuel' op a b := by
  cases op <;> simp only [evalCompareOpH] <;> try exact Res.le_refl _
  case eq =>
    exact Res.le_ite (Res.le_refl _) ((heapEqMono fuel).1 h [] a b fuel' hf)
  case notEq =>
    exact Res.le_ite (Res.le_refl _)
      (Res.le_bind ((heapEqMono fuel).1 h [] a b fuel' hf)
        fun e => Res.le_refl _)
  case inOp => exact valContains_mono hf
  case notIn =>
    exact Res.le_bind (valContains_mono hf) fun e => Res.le_refl _

/-! ## Fuel monotonicity — the enabling theorem -/

/-- **Fuel monotonicity**, one conjunction over the whole mutual block, by
induction on fuel: for every interpreter function `F` and `fuel ≤ fuel'`,
`F fuel ⊑ʳ F fuel'` — a run that decided keeps its exact outcome (final
state included) at any higher fuel. Conjunct order: `evalExpr`, `evalExprs`,
`evalBoolChain`, `evalCompareChain`, `execStmt`, `execStmts`, `execWhile`,
`callIn`, `execFor` (the mutual block's order — `callIn` sits where
`callFunction` sat before the H1 re-shape, keeping the projection paths of
the other corollaries stable). Consume it through the per-function `_mono`
corollaries below. -/
theorem fuelMono (fuel : Nat) :
    (∀ (m : Module) (st : FrameState) (e : Expr) (fuel' : Nat), fuel ≤ fuel' →
      evalExpr m fuel st e ⊑ʳ evalExpr m fuel' st e) ∧
    (∀ (m : Module) (st : FrameState) (es : List Expr) (fuel' : Nat), fuel ≤ fuel' →
      evalExprs m fuel st es ⊑ʳ evalExprs m fuel' st es) ∧
    (∀ (m : Module) (st : FrameState) (op : BoolOp) (e : Expr) (rest : List Expr)
        (fuel' : Nat), fuel ≤ fuel' →
      evalBoolChain m fuel st op e rest ⊑ʳ evalBoolChain m fuel' st op e rest) ∧
    (∀ (m : Module) (st : FrameState) (lhs : RVal) (ops : List CmpOp) (cs : List Expr)
        (fuel' : Nat), fuel ≤ fuel' →
      evalCompareChain m fuel st lhs ops cs ⊑ʳ evalCompareChain m fuel' st lhs ops cs) ∧
    (∀ (m : Module) (st : FrameState) (s : Stmt) (fuel' : Nat), fuel ≤ fuel' →
      execStmt m fuel st s ⊑ʳ execStmt m fuel' st s) ∧
    (∀ (m : Module) (st : FrameState) (ss : List Stmt) (fuel' : Nat), fuel ≤ fuel' →
      execStmts m fuel st ss ⊑ʳ execStmts m fuel' st ss) ∧
    (∀ (m : Module) (st : FrameState) (test : Expr) (body orelse : List Stmt)
        (fuel' : Nat), fuel ≤ fuel' →
      execWhile m fuel st test body orelse ⊑ʳ execWhile m fuel' st test body orelse) ∧
    (∀ (m : Module) (w : World) (fname : String) (args : Array RVal)
        (fuel' : Nat), fuel ≤ fuel' →
      callIn m fuel w fname args ⊑ʳ callIn m fuel' w fname args) ∧
    (∀ (m : Module) (st : FrameState) (target : Expr) (xs : List RVal)
        (body : List Stmt) (fuel' : Nat), fuel ≤ fuel' →
      execFor m fuel st target xs body ⊑ʳ execFor m fuel' st target xs body) ∧
    (∀ (m : Module) (st : FrameState) (keys values : List Expr) (fuel' : Nat),
        fuel ≤ fuel' →
      evalDictItems m fuel st keys values ⊑ʳ evalDictItems m fuel' st keys values) ∧
    (∀ (m : Module) (st : FrameState) (target : Expr) (a : Addr) (i : Nat)
        (body : List Stmt) (fuel' : Nat), fuel ≤ fuel' →
      execForList m fuel st target a i body ⊑ʳ execForList m fuel' st target a i body) ∧
    (∀ (m : Module) (st : FrameState) (a : Addr) (attr : String)
        (args : List Expr) (fuel' : Nat), fuel ≤ fuel' →
      execAttrCall m fuel st a attr args ⊑ʳ execAttrCall m fuel' st a attr args) ∧
    -- H4 (appended LAST, the recorded discipline: existing projection
    -- paths stay put): the generator stepper, the continuation walker
    -- and the lazy `for` cursor.
    (∀ (m : Module) (w : World) (a : Addr) (fuel' : Nat), fuel ≤ fuel' →
      stepIter m fuel w a ⊑ʳ stepIter m fuel' w a) ∧
    (∀ (m : Module) (st : FrameState) (k : GenCont) (fuel' : Nat), fuel ≤ fuel' →
      execGen m fuel st k ⊑ʳ execGen m fuel' st k) ∧
    (∀ (m : Module) (st : FrameState) (target : Expr) (a : Addr)
        (body : List Stmt) (fuel' : Nat), fuel ≤ fuel' →
      execForGen m fuel st target a body ⊑ʳ execForGen m fuel' st target a body) ∧
    -- H6 (appended LAST, the recorded discipline): the draining
    -- consumers' full drain and short-circuit drain
    (∀ (m : Module) (w : World) (a : Addr) (fuel' : Nat), fuel ≤ fuel' →
      drainIter m fuel w a ⊑ʳ drainIter m fuel' w a) ∧
    (∀ (m : Module) (w : World) (a : Addr) (isAll : Bool) (fuel' : Nat), fuel ≤ fuel' →
      anyAllIter m fuel w a isAll ⊑ʳ anyAllIter m fuel' w a isAll) ∧
    -- H7 (appended LAST): the closure invocation
    (∀ (m : Module) (w : World) (name : String) (params : Array Param)
        (ao lo ig : Bool) (body : Array Stmt) (cap : REnv) (args : Array RVal)
        (fuel' : Nat), fuel ≤ fuel' →
      callClosure m fuel w name params ao lo ig body cap args ⊑ʳ
        callClosure m fuel' w name params ao lo ig body cap args) := by
  induction fuel with
  | zero =>
    -- Fuel 0 is `.timeout` everywhere, the bottom of `⊑ʳ`.
    refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
    · exact fun m st e fuel' _ => Or.inl (by simp [evalExpr])
    · exact fun m st es fuel' _ => Or.inl (by simp [evalExprs])
    · exact fun m st op e rest fuel' _ => Or.inl (by simp [evalBoolChain])
    · exact fun m st lhs ops cs fuel' _ => Or.inl (by simp [evalCompareChain])
    · exact fun m st s fuel' _ => Or.inl (by simp [execStmt])
    · exact fun m st ss fuel' _ => Or.inl (by simp [execStmts])
    · exact fun m st test body orelse fuel' _ => Or.inl (by simp [execWhile])
    · exact fun m w fname args fuel' _ => Or.inl (by simp [callIn])
    · exact fun m st target xs body fuel' _ => Or.inl (by simp [execFor])
    · exact fun m st keys values fuel' _ => Or.inl (by simp [evalDictItems])
    · exact fun m st target a i body fuel' _ => Or.inl (by simp [execForList])
    · exact fun m st a attr args fuel' _ => Or.inl (by simp [execAttrCall])
    · exact fun m w a fuel' _ => Or.inl (by simp [stepIter])
    · exact fun m st k fuel' _ => Or.inl (by simp [execGen])
    · exact fun m st target a body fuel' _ => Or.inl (by simp [execForGen])
    · exact fun m w a fuel' _ => Or.inl (by simp [drainIter])
    · exact fun m w a isAll fuel' _ => Or.inl (by simp [anyAllIter])
    · exact fun m w name params ao lo ig body cap args fuel' _ =>
        Or.inl (by simp [callClosure])
  | succ fuel ih =>
    obtain ⟨ihE, ihEs, ihB, ihC, ihS, ihSs, ihW, ihCall, ihFor, ihItems, ihForL,
      ihAttrC, ihStep, ihGen, ihForG, ihDrain, ihAnyAll, ihClosure⟩ := ih
    refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
    -- evalExpr
    · intro m st e fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases e with
        | constant c _ => simp only [evalExpr]; exact Run.le_refl _
        | namedExpr id v _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihE m st v k hk) fun st r => Run.le_refl _
        | name id _ => simp only [evalExpr]; exact Run.le_refl _
        | binOp l op r _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihE m st l k hk) fun st a =>
            Run.le_bind (ihE m st r k hk) fun st b => Run.le_refl _
        | unaryOp op operand _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihE m st operand k hk) fun st v => Run.le_refl _
        | formattedValue expression reprConversion _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihE m st expression k hk) fun nextState value => Run.le_refl _
        | formattedValueAscii expression _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihE m st expression k hk) fun nextState value => Run.le_refl _
        | boolOp op values _ =>
          simp only [evalExpr]
          cases values.toList with
          | nil => exact Run.le_refl _
          | cons e0 es => exact ihB m st op e0 es k hk
        | compare l ops comparators _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihE m st l k hk) fun st a =>
            ihC m st a ops.toList comparators.toList k hk
        | call cf cargs ckw cu _ =>
          cases cu with
          | some reason => simp only [evalExpr]; exact Run.le_refl _
          | none =>
            -- H6: unfold once, split on the keyword gate (the `cases`
            -- substitutes the scrutinee in the goal), reduce the ite,
            -- THEN fork on the callee shape
            simp only [evalExpr]
            cases hkw : ckw.isEmpty with
            | false =>
              -- ===== H6 keyword tier: positionals bind, keyword VALUES
              -- bind, the pure merge lifts, the call recurses through
              -- `callIn` (its own conjunct) =====
              simp only [Bool.false_eq_true, if_false]
              cases cf <;> try (dsimp only; exact Run.le_refl _)
              case name fname _ =>
                dsimp only
                cases Env.lookup st.locals fname with
                | some v =>
                  cases v <;>
                    exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st _ =>
                      Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st _ =>
                        Run.le_refl _
                | none =>
                  cases lookupG (moduleGlobals m).1 fname with
                  | some vv =>
                    cases vv with
                    | some v =>
                      cases v <;>
                        exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st _ =>
                          Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st _ =>
                            Run.le_refl _
                    | none => exact Run.le_refl _
                  | none =>
                    cases findFunction m fname with
                    | some fdefn =>
                      try dsimp only
                      refine Run.le_ite (Run.le_refl _) (Run.le_ite (Run.le_refl _) ?_)
                      refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                      refine Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st kvs => ?_
                      refine Run.le_bind (Run.le_refl _) fun st full => ?_
                      exact Run.le_withLocals (ihCall m st.world fname full k hk)
                    | none =>
                      try dsimp only
                      -- 2026-08-13: `dict(k=v, …)` sits before `sorted`
                      -- — a positional-argument refusal, else the kwarg
                      -- values bind and the allocation is fuel-free
                      refine Run.le_ite (Run.le_refl _) (Run.le_ite ?_
                        (Run.le_ite
                          (Run.le_ite (Run.le_refl _)
                            (Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk)
                              fun st _ => Run.le_refl _))
                          (Run.le_ite ?_ (Run.le_ite ?_ (Run.le_ite ?_ (Run.le_ite ?_ (Run.le_ite (Run.le_refl _)
                            (Run.le_ite (Run.le_refl _) (Run.le_refl _)))))))))
                      cases findNamedTuple m fname with
                      | some nt =>
                        exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st _ =>
                          Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st _ =>
                            Run.le_refl _
                      | none => exact Run.le_refl _
                      -- sorted with keywords (H6 draining tier): key= is
                      -- a fuel-free refusal; a stray keyword binds then
                      -- raises; reverse= binds, truthiness, then the
                      -- drain / heap sort
                      refine Run.le_ite (Run.le_refl _) ?_
                      cases ckw.toList.find? (fun kv => kv.1 != "reverse") with
                      | some kv =>
                        exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st _ =>
                          Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st _ =>
                            Run.le_refl _
                      | none =>
                        refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                        refine Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st kvs => ?_
                        cases vs with
                        | nil => exact Run.le_refl _
                        | cons v vtail =>
                          cases vtail with
                          | cons _ _ => exact Run.le_refl _
                          | nil =>
                            cases kvs with
                            | nil => exact Run.le_refl _
                            | cons rv rtail =>
                              cases rtail with
                              | cons _ _ => exact Run.le_refl _
                              | nil =>
                                refine Run.le_bind (Run.le_refl _) fun st desc => ?_
                                cases v <;> try exact Run.le_refl _
                                case ref a =>
                                  dsimp only
                                  cases Heap.get? st.world.heap a with
                                  | none => exact Run.le_refl _
                                  | some obj =>
                                    cases obj <;> try exact Run.le_refl _
                                    case generator q l c stat =>
                                      refine Run.le_bind
                                        (Run.le_withLocals (ihDrain m st.world a k hk))
                                        fun st vals => ?_
                                      exact Run.le_bind (Run.le_refl _) fun st s2 =>
                                        Run.le_refl _
                      -- float, divmod, len, bool, and repr with keywords: both argument lists bind before
                      -- the faithful positional-only TypeError.
                      exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st _ =>
                        Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st _ =>
                          Run.le_refl _
                      exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st _ =>
                        Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st _ =>
                          Run.le_refl _
                      exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st _ =>
                        Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st _ =>
                          Run.le_refl _
              case «attribute» recv attr spa =>
                dsimp only
                refine Run.le_bind (ihE m st recv k hk) fun st r => ?_
                cases r <;> try exact Run.le_refl _
                case ref a =>
                  -- H7+: instance-method keywords — plan fork, then the
                  -- merge and the call through `callIn`'s conjunct
                  dsimp only
                  cases attrCallPlan m st.world.heap a attr <;> try exact Run.le_refl _
                  case instMethod qname =>
                    dsimp only
                    cases findFunction m qname with
                    | some fdefn =>
                      try dsimp only
                      refine Run.le_ite (Run.le_refl _) ?_
                      refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                      refine Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st kvs => ?_
                      refine Run.le_bind (Run.le_refl _) fun st full => ?_
                      exact Run.le_withLocals (ihCall m st.world qname full k hk)
                    | none => exact Run.le_refl _
                case ntuple tn fs xs =>
                  dsimp only
                  cases ntupleCallPlan m tn fs attr <;> try exact Run.le_refl _
                  case instMethod qname =>
                    dsimp only
                    cases findFunction m qname with
                    | some fdefn =>
                      try dsimp only
                      refine Run.le_ite (Run.le_refl _) ?_
                      refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                      refine Run.le_bind (ihEs m st (ckw.toList.map (·.2)) k hk) fun st kvs => ?_
                      refine Run.le_bind (Run.le_refl _) fun st full => ?_
                      exact Run.le_withLocals (ihCall m st.world qname full k hk)
                    | none => exact Run.le_refl _
            | true =>
              simp only [eq_self_iff_true, if_true]
              cases cf <;> try (dsimp only; exact Run.le_refl _)
              case «attribute» recv attr spa =>
                -- receiver-first dispatch (H3): the receiver evaluates, then
                -- `execAttrCall` forks on the pure plan (its own conjunct);
                -- an ntuple VALUE receiver (H5) forks on `ntupleCallPlan` —
                -- only the method arm recurses (args + `callIn`).
                -- Pass 6: the TRACE-CLOCK fork comes first (`isClockCall`
                -- is fuel-free, so both sides split identically; the pop
                -- and its refusals are fuel-free too).
                dsimp only
                split
                · exact Run.le_refl _
                refine Run.le_bind (ihE m st recv k hk) fun st r => ?_
                cases r <;>
                  first
                  | exact Run.le_refl _
                  | exact ihAttrC m st _ attr cargs.toList k hk
                  | skip
                case ntuple tn fs xs =>
                  -- iota-reduce the receiver matcher, then fork on the plan
                  dsimp only
                  cases ntupleCallPlan m tn fs attr <;> try exact Run.le_refl _
                  case instMethod qname =>
                    exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs =>
                      Run.le_withLocals
                        (ihCall m st.world qname ((RVal.ntuple tn fs xs :: vs).toArray) k hk)
                case str sv =>
                  -- str METHOD dispatch (H5 strings): fork on the pure plan;
                  -- every in-tier arm is args + a fuel-independent worker
                  dsimp only
                  cases strCallPlan attr <;>
                    first
                    | exact Run.le_refl _
                    | exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk))
                        fun st vs => Run.le_refl _
                case float fv =>
                  -- `float.is_integer()` is a pure zero-argument query;
                  -- argument evaluation is the only recursive part.
                  dsimp only
                  split
                  · exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk))
                      fun st vs => Run.le_refl _
                  · exact Run.le_refl _
              case name fname _ =>
                dsimp only
                cases hstar : fname == starArgBuiltinName with
                | true =>
                  simp only [if_true]
                  cases cargs.toList with
                  | nil => exact Run.le_refl _
                  | cons arg rest =>
                    cases rest with
                    | nil =>
                      cases ckw.toList with
                      | nil =>
                        exact Run.le_bind (ihE m st arg k hk) fun st v =>
                          Run.le_bind (Run.le_refl _) fun st xs => Run.le_refl _
                      | cons _ _ => exact Run.le_refl _
                    | cons _ _ => exact Run.le_refl _
                | false =>
                  simp only [hstar, Bool.false_eq_true, if_false]
                  cases Env.lookup st.locals fname with
                  | some v =>
                    cases v <;>
                      first
                      | exact Run.le_refl _
                      | exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun _ _ =>
                          Run.le_refl _
                      | skip
                    case ref a =>
                      -- H7: the guarded closure call
                      refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                      refine Run.le_ite (Run.le_refl _) ?_
                      cases Heap.get? st.world.heap a with
                      | none => exact Run.le_refl _
                      | some o =>
                        cases o <;> try exact Run.le_refl _
                        case closure nm ps ao lo hg ig bd cap =>
                          exact Run.le_bind (Run.le_refl _) fun st cap' =>
                            Run.le_withLocals
                              (ihClosure m st.world
                                nm ps ao lo ig bd cap' vs.toArray k hk)
                  | none =>
                    -- module globals (G1) → module function → builtins →
                    -- NameError/unsupported (the globals and the final fork are
                    -- fuel-independent, hence `le_refl`)
                    refine Run.le_ite (Run.le_refl _) ?_
                    cases lookupG (moduleGlobals m).1 fname with
                    | some vv =>
                      cases vv with
                      | some v =>
                        cases v <;>
                          exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun _ _ =>
                            Run.le_refl _
                      | none =>
                        -- pass 3: the poisoned-arm live view — value/exn
                        -- arms bind then decide; a closure ref recurses
                        -- through `callClosure` (its own conjunct)
                        cases Env.lookup st.world.globals fname with
                        | none => exact Run.le_refl _
                        | some v =>
                          cases v with
                          | none => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | ellipsis => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | bool _ => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | int _ => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | float _ => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | str _ => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | bytes _ => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | listV _ => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | tuple _ => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | ntuple _ _ _ => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | rangeV _ _ _ => exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) (fun st _ => Run.le_refl _)
                          | ref a =>
                            refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            refine Run.le_ite (Run.le_refl _) ?_
                            cases Heap.get? st.world.heap a with
                            | none => exact Run.le_refl _
                            | some obj =>
                              cases obj <;> try exact Run.le_refl _
                              case closure nm ps ao lo hg ig bd cap =>
                                exact Run.le_bind (Run.le_refl _) fun st cap' =>
                                  Run.le_withLocals
                                    (ihClosure m st.world
                                      nm ps ao lo ig bd cap' vs.toArray k hk)
                    | none =>
                      -- findFunction (def/class collision → call) → class
                      -- instantiation (guards, args, `__init__` through
                      -- `callIn`) → len → sorted → max → min → abs → int →
                      -- NameError/unsupported (each builtin: bind args, result
                      -- fuel-independent)
                      have hb : ∀ {β : Type} (g : FrameState → List RVal → Run FrameState β),
                          (flattenStarRun (evalExprs m fuel st cargs.toList)).bind g ⊑ʳ
                          (flattenStarRun (evalExprs m k st cargs.toList)).bind g :=
                        fun g => Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk))
                          fun st vs => Run.le_refl _
                      refine Run.le_ite
                        (Run.le_ite (Run.le_refl _)
                          (Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs =>
                            Run.le_withLocals (ihCall m st.world fname vs.toArray k hk)))
                        ?_
                      cases findClass m fname with
                      | some p =>
                        obtain ⟨ci, c⟩ := p
                        -- namedtuple-collision guard, then the exceptions
                        -- tier's isExc guard (both fuel-independent)
                        refine Run.le_ite (Run.le_refl _) (Run.le_ite (Run.le_refl _) ?_)
                        cases c.ntBase with
                        | some nt =>
                          -- value-like subclass construction (H5): guards,
                          -- then args, then a fuel-independent value/arity fork
                          refine Run.le_ite (Run.le_refl _) (Run.le_ite (Run.le_refl _)
                            (Run.le_ite (Run.le_refl _) ?_))
                          exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk))
                            fun st vs => Run.le_refl _
                        | none =>
                          refine Run.le_ite (Run.le_refl _) (Run.le_ite (Run.le_refl _) ?_)
                          refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                          cases classMethodQname m ci "__init__" with
                          | some initName =>
                            refine Run.le_bind (Run.le_withLocals
                              (ihCall m _ initName ((RVal.ref st.world.heap.size :: vs).toArray) k hk))
                              fun st'' r => ?_
                            cases r <;> exact Run.le_refl _
                          | none => exact Run.le_refl _
                      | none =>
                        -- namedtuple construction binds the arguments, then a
                        -- fuel-independent value/arity fork; the builtin chain
                        -- is as before
                        cases findNamedTuple m fname with
                        | some nt => exact hb _
                        | none =>
                          -- len, sorted (drains a generator), max/min (the
                          -- guarded drain), any/all (the short-circuit
                          -- drain), abs, round, int, enumerate, count (both
                          -- ALLOCATE an iterator object), NEXT (binds the
                          -- args, then steps the generator), ord, chr
                          -- len → sorted → max → min → any/all → set → abs →
                          -- int → sum → tuple → list → dict → range →
                          -- enumerate → count → next → ord → chr → hex → format → tail
                          refine Run.le_ite ?_                                  -- literal f-string format
                              (Run.le_ite ?_                                  -- len(sequence * count)
                              (Run.le_ite (hb _)                                  -- len
                              (Run.le_ite ?_                                     -- sorted
                               (Run.le_ite ?_                                    -- max
                                (Run.le_ite ?_                                   -- min
                                 (Run.le_ite ?_                                  -- any/all
                                  (Run.le_ite ?_                                 -- set
                                   (Run.le_ite (hb _)                            -- abs
                                    (Run.le_ite (hb _)                           -- round
                                     (Run.le_ite (hb _)                           -- int
                                     (Run.le_ite (hb _)
                                     (Run.le_ite (hb _)
                                     (Run.le_ite (hb _)
                                     (Run.le_ite ?_                              -- pow
                                     (Run.le_ite ?_                              -- sum
                                      (Run.le_ite ?_                             -- tuple
                                       (Run.le_ite ?_                            -- list
                                        (Run.le_ite ?_                           -- dict
                                         (Run.le_ite (hb _)                      -- range
                                        (Run.le_ite (hb _)                       -- enumerate
                                         (Run.le_ite (hb _)                      -- count
                                          (Run.le_ite ?_                         -- next
                                           (Run.le_ite (hb _)                    -- ord
                                               (Run.le_ite (hb _)                 -- chr
                                               (Run.le_ite (hb _)                 -- hex
                                                (Run.le_ite (hb _)                -- format
                                                ?_))))))))))))))))))))))))))
                          -- Literal f-string format specifications evaluate their
                          -- two structural arguments and then use the pure
                          -- format worker.
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons _ rest =>
                              cases rest with
                              | nil => exact Run.le_refl _
                              | cons _ rest' =>
                                cases rest' with
                                | nil => exact Run.le_refl _
                                | cons _ _ => exact Run.le_refl _
                          -- `<lenmult>` evaluates its operands once and then
                          -- chooses a fuel-independent length/result worker.
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons left rest =>
                              cases rest with
                              | nil => exact Run.le_refl _
                              | cons right rest' =>
                                cases rest' with
                                | nil =>
                                  cases sequenceMultLength left right <;> exact Run.le_refl _
                                | cons _ _ => exact Run.le_refl _
                          -- sorted
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons v vtail =>
                              cases vtail with
                              | cons _ _ => exact Run.le_refl _
                              | nil =>
                                dsimp only
                                cases v <;> try exact Run.le_refl _
                                case ref a =>
                                  dsimp only
                                  cases Heap.get? st.world.heap a with
                                  | none => exact Run.le_refl _
                                  | some obj =>
                                    cases obj <;> try exact Run.le_refl _
                                    case generator q l c stat =>
                                      refine Run.le_bind
                                        (Run.le_withLocals (ihDrain m st.world a k hk))
                                        fun st vals => ?_
                                      exact Run.le_bind (Run.le_refl _) fun st s2 =>
                                        Run.le_refl _
                          -- max
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons v vtail =>
                              cases v <;> try exact Run.le_refl _
                              case ref a =>
                                cases vtail with
                                | cons _ _ => exact Run.le_refl _
                                | nil =>
                                  dsimp only
                                  cases Heap.get? st.world.heap a with
                                  | none => exact Run.le_refl _
                                  | some obj =>
                                    cases obj <;> try exact Run.le_refl _
                                    case generator q l c stat =>
                                      refine Run.le_ite (Run.le_refl _) ?_
                                      refine Run.le_bind
                                        (Run.le_withLocals (ihDrain m st.world a k hk))
                                        fun st vals => ?_
                                      exact Run.le_refl _
                          -- min
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons v vtail =>
                              cases v <;> try exact Run.le_refl _
                              case ref a =>
                                cases vtail with
                                | cons _ _ => exact Run.le_refl _
                                | nil =>
                                  dsimp only
                                  cases Heap.get? st.world.heap a with
                                  | none => exact Run.le_refl _
                                  | some obj =>
                                    cases obj <;> try exact Run.le_refl _
                                    case generator q l c stat =>
                                      refine Run.le_ite (Run.le_refl _) ?_
                                      refine Run.le_bind
                                        (Run.le_withLocals (ihDrain m st.world a k hk))
                                        fun st vals => ?_
                                      exact Run.le_refl _
                          -- any/all
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons v vtail =>
                              cases vtail with
                              | cons _ _ => exact Run.le_refl _
                              | nil =>
                                cases v <;> try exact Run.le_refl _
                                case ref a =>
                                  dsimp only
                                  cases Heap.get? st.world.heap a with
                                  | none => exact Run.le_refl _
                                  | some obj =>
                                    cases obj <;> try exact Run.le_refl _
                                    case generator q l c stat =>
                                      refine Run.le_bind
                                        (Run.le_withLocals
                                          (ihAnyAll m st.world a (fname == "all") k hk))
                                        fun st b => ?_
                                      exact Run.le_refl _
                          -- set (H7+): binds, then per-receiver dedup
                          -- (fuel-threaded scans) or the generator drain
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons v vtail =>
                              cases vtail with
                              | cons _ _ => exact Run.le_refl _
                              | nil =>
                                dsimp only
                                cases v <;>
                                  first
                                  | exact Run.le_refl _
                                  | exact Run.le_bind (Run.le_liftRes (setDedup_mono hk _))
                                      fun st es => Run.le_refl _
                                  | skip
                                case rangeV lo hi step =>
                                  exact Run.le_bind (Run.le_refl _) fun st xs =>
                                    Run.le_bind (Run.le_liftRes (setDedup_mono hk _))
                                      fun st es => Run.le_refl _
                                case ref a =>
                                  dsimp only
                                  cases Heap.get? st.world.heap a with
                                  | none => exact Run.le_refl _
                                  | some obj =>
                                    cases obj <;>
                                      first
                                      | exact Run.le_refl _
                                      | exact Run.le_bind (Run.le_liftRes (setDedup_mono hk _))
                                          fun st es => Run.le_refl _
                                      | skip
                                    case generator q l c stat =>
                                      refine Run.le_bind
                                        (Run.le_withLocals (ihDrain m st.world a k hk))
                                        fun st vals => ?_
                                      exact Run.le_bind (Run.le_liftRes (setDedup_mono hk _))
                                        fun st es => Run.le_refl _
                          -- pow: argument evaluation followed by the pure
                          -- binary operation, or the loud modulus refusal
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons _ rest =>
                              cases rest with
                              | nil => exact Run.le_refl _
                              | cons _ rest =>
                                cases rest with
                                | nil => exact Run.le_refl _
                                | cons _ _ => exact Run.le_refl _
                          -- sum (pass 3): arity fork, the str-start fork,
                          -- then the receiver — every value arm is the pure
                          -- fold; the single-generator arm drains behind the
                          -- `moduleGenFree` guard, like max/min
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases sumArgs vs with
                            | none => exact Run.le_refl _
                            | some pr =>
                              obtain ⟨v, start⟩ := pr
                              dsimp only
                              cases start <;> try exact Run.le_refl _
                              all_goals
                                cases v <;> try exact Run.le_refl _
                              all_goals
                                case ref a =>
                                  dsimp only
                                  cases Heap.get? st.world.heap a with
                                  | none => exact Run.le_refl _
                                  | some obj =>
                                    cases obj <;> try exact Run.le_refl _
                                    case generator q l c stat =>
                                      refine Run.le_ite (Run.le_refl _) ?_
                                      exact Run.le_bind
                                        (Run.le_withLocals (ihDrain m st.world a k hk))
                                        fun st vals => Run.le_refl _
                          -- tuple (pass 3): snapshot constructors are
                          -- fuel-free; the generator arm drains, guarded
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons v vtail =>
                              cases vtail with
                              | cons _ _ => exact Run.le_refl _
                              | nil =>
                                dsimp only
                                cases v <;> try exact Run.le_refl _
                                case ref a =>
                                  dsimp only
                                  cases Heap.get? st.world.heap a with
                                  | none => exact Run.le_refl _
                                  | some obj =>
                                    cases obj <;> try exact Run.le_refl _
                                    case generator q l c stat =>
                                      refine Run.le_ite (Run.le_refl _) ?_
                                      exact Run.le_bind
                                        (Run.le_withLocals (ihDrain m st.world a k hk))
                                        fun st vals => Run.le_refl _
                          -- list (2026-08-13): `tuple`'s inventory with an
                          -- allocation, and the generator arm drains
                          -- UNGUARDED (the call is outside heapFree, so no
                          -- `moduleGenFree` ite to walk)
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons v vtail =>
                              cases vtail with
                              | cons _ _ => exact Run.le_refl _
                              | nil =>
                                dsimp only
                                cases v <;> try exact Run.le_refl _
                                case ref a =>
                                  dsimp only
                                  cases Heap.get? st.world.heap a with
                                  | none => exact Run.le_refl _
                                  | some obj =>
                                    cases obj <;> try exact Run.le_refl _
                                    case generator q l c stat =>
                                      exact Run.le_bind
                                        (Run.le_withLocals (ihDrain m st.world a k hk))
                                        fun st vals => Run.le_refl _
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons value remaining =>
                              cases remaining with
                              | cons _ _ => exact Run.le_refl _
                              | nil =>
                                dsimp only
                                cases value <;> try exact Run.le_refl _
                                case ref address =>
                                  dsimp only
                                  cases Heap.get? st.world.heap address with
                                  | none => exact Run.le_refl _
                                  | some obj =>
                                    cases obj <;> try exact Run.le_refl _
                                    case generator kind locals captured status =>
                                      exact Run.le_bind
                                        (Run.le_withLocals (ihDrain m st.world address k hk))
                                        fun st vals =>
                                          Run.le_bind (Run.le_refl _) fun st items =>
                                            Run.le_bind (Run.le_refl _) fun st entries =>
                                              Run.le_refl _
                          -- next
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                            cases vs with
                            | nil => exact Run.le_refl _
                            | cons v rest =>
                              cases v <;> try exact Run.le_refl _
                              case ref ad =>
                                cases rest with
                                | nil =>
                                  refine Run.le_bind
                                    (Run.le_withLocals (ihStep m st.world ad k hk))
                                    fun st r => ?_
                                  cases r <;> exact Run.le_refl _
                                | cons d rest' =>
                                  cases rest' with
                                  | nil =>
                                    refine Run.le_bind
                                      (Run.le_withLocals (ihStep m st.world ad k hk))
                                      fun st r => ?_
                                    cases r <;> exact Run.le_refl _
                                  | cons _ _ => exact Run.le_refl _
                          -- the tail: str (pass 8 — args bind, pure
                          -- worker) / input / print / module dunder, then
                          -- the pass-3 absent-arm live view — the closure
                          -- dispatch recurses through callClosure
                          · refine Run.le_ite
                              (Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk))
                                fun st _ => Run.le_refl _)
                              (Run.le_ite
                                (Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk))
                                  fun st _ => Run.le_refl _)
                              (Run.le_ite (Run.le_refl _)
                                (Run.le_ite
                                  (Run.le_bind (ihEs m st (complexPrintArgs cargs.toList) k hk)
                                    fun st _ => Run.le_refl _)
                                  (Run.le_ite (Run.le_refl _) ?_))))
                            cases Env.lookup st.world.globals fname with
                            | none => exact Run.le_refl _
                            | some v =>
                              cases v <;>
                                first
                                  | exact Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk))
                                      fun st _ => Run.le_refl _
                                  | skip
                              case ref a =>
                                refine Run.le_bind (flattenStarRun_mono (ihEs m st cargs.toList k hk)) fun st vs => ?_
                                refine Run.le_ite (Run.le_refl _) ?_
                                cases Heap.get? st.world.heap a with
                                | none => exact Run.le_refl _
                                | some obj =>
                                  cases obj <;> try exact Run.le_refl _
                                  case closure nm ps ao lo hg ig bd cap =>
                                    exact Run.le_bind (Run.le_refl _) fun st cap' =>
                                      Run.le_withLocals
                                        (ihClosure m st.world
                                          nm ps ao lo ig bd cap' vs.toArray k hk)
        | genExp elt tgt it ifs wb _ =>
          simp only [evalExpr]; exact Run.le_refl _
        | list elts _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihEs m st elts.toList k hk) fun st vs => Run.le_refl _
        | tuple elts _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihEs m st elts.toList k hk) fun st vs => Run.le_refl _
        | subscript v idx _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihE m st v k hk) fun st c =>
            Run.le_bind (ihE m st idx k hk) fun st i => Run.le_refl _
        | dict keys values _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihItems m st keys.toList values.toList k hk)
            fun st items => Run.le_bind (Run.le_refl _) fun st entries =>
              Run.le_refl _
        | «attribute» recv attr _ =>
          -- attribute READ (H3): receiver, then a fuel-free heap fork
          simp only [evalExpr]
          exact Run.le_bind (ihE m st recv k hk) fun st r => Run.le_refl _
        | ifExp t b o _ =>
          simp only [evalExpr]
          exact Run.le_bind (ihE m st t k hk) fun st tv =>
            Run.le_bind (Run.le_refl _) fun st cond =>
              Run.le_ite (ihE m st b k hk) (ihE m st o k hk)
        | slice v l u stp _ =>
          -- H5 strings: four sequential component binds, then the pure
          -- (fuel-independent) `sliceVal`
          simp only [evalExpr]
          exact Run.le_bind (ihE m st v k hk) fun st cv =>
            Run.le_bind (ihE m st l k hk) fun st lv =>
              Run.le_bind (ihE m st u k hk) fun st uv =>
                Run.le_bind (ihE m st stp k hk) fun st sv => Run.le_refl _
        | unsupported pyKind text _ => simp only [evalExpr]; exact Run.le_refl _
    -- evalExprs
    · intro m st es fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases es with
        | nil => simp only [evalExprs]; exact Run.le_refl _
        | cons e rest =>
          simp only [evalExprs]
          exact Run.le_bind (ihE m st e k hk) fun st v =>
            Run.le_bind (ihEs m st rest k hk) fun st vs => Run.le_refl _
    -- evalBoolChain
    · intro m st op e rest fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        simp only [evalBoolChain]
        refine Run.le_bind (ihE m st e k hk) fun st v => ?_
        cases rest with
        | nil => exact Run.le_refl _
        | cons e' rest' =>
          refine Run.le_bind (Run.le_refl _) fun st b => ?_
          cases op with
          | and => exact Run.le_ite (ihB m st .and e' rest' k hk) (Run.le_refl _)
          | or => exact Run.le_ite (Run.le_refl _) (ihB m st .or e' rest' k hk)
    -- evalCompareChain
    · intro m st lhs ops cs fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases ops with
        | nil =>
          cases cs with
          | nil => simp only [evalCompareChain]; exact Run.le_refl _
          | cons c cs' => simp only [evalCompareChain]; exact Run.le_refl _
        | cons op ops' =>
          cases cs with
          | nil => simp only [evalCompareChain]; exact Run.le_refl _
          | cons e rest =>
            simp only [evalCompareChain]
            exact Run.le_bind (ihE m st e k hk) fun st rhs =>
              Run.le_bind (Run.le_refl _) fun st _ =>
              Run.le_bind (Run.le_liftRes (evalCompareOpH_mono hk)) fun st b =>
                Run.le_ite (ihC m st rhs ops' rest k hk) (Run.le_refl _)
    -- execStmt
    · intro m st s fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases s with
        | defStmt name params ao lo hg ig body caps _ =>
          simp only [execStmt]; exact Run.le_refl _
        | unpackAssign before star after value _ =>
          simp only [execStmt]
          exact Run.le_bind (ihE m st value k hk) (fun st v =>
            Run.le_bind (Run.le_refl _) (fun st parts => Run.le_refl _))
        | yieldFromStmt v _ =>
          -- pass 5: an un-lowered `yield from` refuses, fuel-free
          simp only [execStmt]; exact Run.le_refl _
        | raiseStmt exc cause _ =>
          -- The admitted literal payload form is fuel-free, like the
          -- class-identity raise path.
          simp only [execStmt]
          exact Run.le_refl _
        | delStmt names _ =>
          -- del RECONCILED: fuel-free — a pure fold over the locals
          simp only [execStmt]; exact Run.le_refl _
        | assertStmt test msg _ =>
          -- the tail batch: two evalExpr calls, the message's only on
          -- the FAILING branch — an ordinary bind-shaped arm
          simp only [execStmt]
          refine Run.le_bind (ihE m st test k hk) fun st t => ?_
          refine Run.le_bind (Run.le_refl _) fun st b => ?_
          refine Run.le_ite (Run.le_refl _) ?_
          cases msg with
          | none => exact Run.le_refl _
          | some e =>
            exact Run.le_bind (ihE m st e k hk) fun st v => Run.le_refl _
        | tryStmt body excName handler tu _ =>
          simp only [execStmt]
          cases tu with
          | some reason => exact Run.le_refl _
          | none =>
            -- shadow guard, handler-class resolution, isExc — all
            -- fuel-independent; then the body run (IH), the match on its
            -- retained outcome, and the handler run (IH again)
            by_cases hempty : excName.isEmpty
            · simp [hempty]
              rcases ihSs m st body.toList k hk with h | h
              · rw [h]; exact Or.inl rfl
              · rw [h]
                cases execStmts m k st body.toList with
                | ok st' flow => exact Run.le_refl _
                | exn st' e => exact ihSs m st' handler.toList k hk
                | timeout => exact Run.le_refl _
                | unsupported msg => exact Run.le_refl _
            · by_cases htuple : excHandlerTuple excName
              · simp [hempty, htuple]
                split <;> try exact Run.le_refl _
                split <;> try exact Run.le_refl _
                rcases ihSs m st body.toList k hk with h | h
                · rw [h]; exact Or.inl rfl
                · rw [h]
                  cases execStmts m k st body.toList with
                  | ok st' flow => exact Run.le_refl _
                  | exn st' e =>
                    exact Run.le_ite (ihSs m st' handler.toList k hk)
                      (Run.le_refl _)
                  | timeout => exact Run.le_refl _
                  | unsupported msg => exact Run.le_refl _
              · simp [hempty, htuple]
                refine Run.le_ite (Run.le_refl _) ?_
                cases findClass m excName with
                | none =>
                  refine Run.le_ite ?_ ?_
                  · exact Run.le_bindE (ihSs m st body.toList k hk)
                      (fun _ _ => Run.le_refl _) (fun _ _ => Run.le_refl _)
                  -- Pass 0 (§import forms): the pinned import-error table
                  -- branch — the class branch's body/handler IH shape, with
                  -- no cid ite (every `.importError` matches either name)
                  · refine Run.le_ite ?_ ?_
                    · rcases ihSs m st body.toList k hk with h | h
                      · rw [h]; exact Or.inl rfl
                      · rw [h]
                        cases execStmts m k st body.toList with
                        | ok st' flow => exact Run.le_refl _
                        | exn st' e =>
                          cases e <;> try exact Run.le_refl _
                          case importError mod =>
                            exact ihSs m st' handler.toList k hk
                        | timeout => exact Run.le_refl _
                        | unsupported msg => exact Run.le_refl _
                    · refine Run.le_ite ?_ (Run.le_refl _)
                      rcases ihSs m st body.toList k hk with h | h
                      · rw [h]; exact Or.inl rfl
                      · rw [h]
                        cases execStmts m k st body.toList with
                        | ok st' flow => exact Run.le_refl _
                        | exn st' e =>
                          exact Run.le_ite (ihSs m st' handler.toList k hk)
                            (Run.le_refl _)
                        | timeout => exact Run.le_refl _
                        | unsupported msg => exact Run.le_refl _
                | some p =>
                  obtain ⟨ci, c⟩ := p
                  refine Run.le_ite (Run.le_refl _) ?_
                  rcases ihSs m st body.toList k hk with h | h
                  · rw [h]; exact Or.inl rfl
                  · rw [h]
                    cases execStmts m k st body.toList with
                    | ok st' flow => exact Run.le_refl _
                    | exn st' e =>
                      cases e <;> try exact Run.le_refl _
                      case user cid nm =>
                        exact Run.le_ite (ihSs m st' handler.toList k hk)
                          (Run.le_refl _)
                      case userMessage cid nm msg =>
                        exact Run.le_ite (ihSs m st' handler.toList k hk)
                          (Run.le_refl _)
                    | timeout => exact Run.le_refl _
                    | unsupported msg => exact Run.le_refl _
        | withStmt items body tu _ =>
          simp only [execStmt]
          cases tu with
          | some reason => exact Run.le_refl _
          | none =>
            cases hitems : items.toList with
            | nil => simp [hitems]; exact Run.le_refl _
            | cons item rest =>
              cases hrest : rest with
              | cons item2 rest2 => simp [hitems, hrest]; exact Run.le_refl _
              | nil =>
                cases hctx : item.context with
                | call func args kwargs callUnsupported csp =>
                  cases hfunc : func with
                  | name fname fsp =>
                    cases hkwargs : kwargs.toList with
                    | cons kw kws =>
                      have hkwNonempty : kwargs.isEmpty = false := by
                        apply Bool.eq_false_iff.mpr
                        intro he
                        have hkwEmpty : kwargs = #[] := Array.isEmpty_iff.mp he
                        simp [hkwEmpty] at hkwargs
                      simp [hitems, hrest, hctx, hfunc, hkwNonempty]
                      exact Run.le_refl _
                    | nil =>
                      have hkwEmpty : kwargs = #[] :=
                        Array.toList_inj.mp (by simpa using hkwargs)
                      cases hcall : callUnsupported with
                      | some reason => simp [hitems, hrest, hctx, hfunc, hkwEmpty, hcall]; exact Run.le_refl _
                      | none =>
                        cases hclass : findContextClass m fname with
                        | none => simp [hitems, hrest, hctx, hfunc, hkwEmpty, hcall, hclass]; exact Run.le_refl _
                        | some pr =>
                          obtain ⟨ci, cdef⟩ := pr
                          simp [hitems, hrest, hctx, hfunc, hkwEmpty, hcall, hclass]
                          split
                          · exact Run.le_refl _
                          · refine Run.le_bind (flattenStarRun_mono (ihEs m st args.toList k hk)) fun s2 vs => ?_
                            cases vs with
                            | nil =>
                              let a := s2.world.heap.size
                              let s2' := { s2 with world :=
                                { s2.world with heap := s2.world.heap.push (.instance ci (instanceAttrs m ci)) } }
                              refine Run.le_bind
                                (Run.le_withLocals
                                  (ihCall m s2'.world (fname ++ ".__enter__") #[.ref a] k hk))
                                fun sEnter entered => ?_
                              cases htarget : item.target with
                              | none =>
                                simp only [htarget]
                                refine Run.le_bindE (ihSs m sEnter body.toList k hk)
                                  (fun sAfter flow => ?_)
                                  (fun sBody _ =>
                                    Run.le_bind
                                      (Run.le_withLocals
                                        (ihCall m sBody.world (fname ++ ".__exit__")
                                          (withExitArgs
                                            ((findFunction m (fname ++ ".__exit__")).map
                                              FunctionDefn.withExitExceptionTypeTest == some true) a) k hk))
                                      (fun sExit _ => Run.le_refl _))
                                cases flow with
                                | next | ret _ | brk | cont =>
                                  exact Run.le_bind
                                    (Run.le_withLocals
                                      (ihCall m sAfter.world (fname ++ ".__exit__")
                                        #[.ref a, .none, .none, .none] k hk))
                                    (fun sExit _ => Run.le_refl _)
                              | some target =>
                                simp only [htarget]
                                refine Run.le_bind (Run.le_refl _) fun sBody env' => ?_
                                refine Run.le_bindE (ihSs m { sBody with locals := env' }
                                  body.toList k hk)
                                  (fun sAfter flow => ?_)
                                  (fun sBody _ =>
                                    Run.le_bind
                                      (Run.le_withLocals
                                        (ihCall m sBody.world (fname ++ ".__exit__")
                                          (withExitArgs
                                            ((findFunction m (fname ++ ".__exit__")).map
                                              FunctionDefn.withExitExceptionTypeTest == some true) a) k hk))
                                      (fun sExit _ => Run.le_refl _))
                                cases flow with
                                | next | ret _ | brk | cont =>
                                  exact Run.le_bind
                                    (Run.le_withLocals
                                      (ihCall m sAfter.world (fname ++ ".__exit__")
                                        #[.ref a, .none, .none, .none] k hk))
                                    (fun sExit _ => Run.le_refl _)
                            | cons v rest => exact Run.le_refl _
                  | _ => simp [hitems, hrest, hctx, hfunc]; exact Run.le_refl _
                | _ => simp [hitems, hrest, hctx]; exact Run.le_refl _

        | importFrom mod names star _ =>
          -- Pass 0 (§import forms): fuel-free — the arm raises
          -- immediately, state unchanged (the raiseStmt shape)
          simp only [execStmt]; exact Run.le_refl _
        | ret value _ =>
          cases value with
          | none => simp only [execStmt]; exact Run.le_refl _
          | some e =>
            simp only [execStmt]
            exact Run.le_bind (ihE m st e k hk) fun st v => Run.le_refl _
        | assign targets value _ =>
          simp only [execStmt]
          cases targets.toList with
          | nil => exact Run.le_refl _
          | cons t rest =>
            cases rest with
            | nil =>
              -- subscript targets: value, primary, key, then the
              -- fuel-independent store; every other target: the old shape
              cases t
              case subscript dE kE sp =>
                exact Run.le_bind (ihE m st value k hk) fun st v =>
                  Run.le_bind (ihE m st dE k hk) fun st c =>
                    Run.le_bind (ihE m st kE k hk) fun st kk => Run.le_refl _
              case «attribute» recvE attr sp =>
                exact Run.le_bind (ihE m st value k hk) fun st v =>
                  Run.le_bind (ihE m st recvE k hk) fun st r => Run.le_refl _
              case tuple elts sp =>
                -- pass 4: the all-names/attribute-elements fork — both
                -- branches bind the value, then a fuel-free tail
                exact Run.le_ite
                  (Run.le_bind (ihE m st value k hk) fun st v => Run.le_refl _)
                  (Run.le_bind (ihE m st value k hk) fun st v => Run.le_refl _)
              all_goals
                exact Run.le_bind (ihE m st value k hk) fun st v =>
                  Run.le_bind (Run.le_refl _) fun st env' => Run.le_refl _
            | cons t2 rest2 =>
              -- the compiled matcher still splits on the head constructor
              cases t <;> exact Run.le_refl _
        | augAssign target op value _ =>
          cases target <;> try (simp only [execStmt]; exact Run.le_refl _)
          case name id _ =>
            simp only [execStmt]
            cases Env.lookup st.locals id with
            | none => exact Run.le_refl _
            | some old =>
              cases old <;>
                first
                | exact Run.le_refl _
                | exact Run.le_bind (ihE m st value k hk) fun st v =>
                    Run.le_bind (Run.le_refl _) fun st r => Run.le_refl _
          case «attribute» recvE attr _ =>
            -- pass 4: receiver, the fuel-free attribute load, then (for
            -- immediate old values) the value and the fuel-free store
            simp only [execStmt]
            refine Run.le_bind (ihE m st recvE k hk) fun st r => ?_
            cases r <;> try exact Run.le_refl _
            case ref a =>
              refine Run.le_bind (Run.le_refl _) fun st old => ?_
              cases old <;> try exact Run.le_refl _
              case ref a2 =>
                exact Run.le_bind (ihE m st value k hk) fun st v =>
                  Run.le_bind (Run.le_refl _) fun st h' => Run.le_refl _
              all_goals
                exact Run.le_bind (ihE m st value k hk) fun st v =>
                  Run.le_bind (Run.le_refl _) fun st res =>
                    Run.le_bind (Run.le_refl _) fun st h' => Run.le_refl _
        | whileLoop test body orelse _ =>
          simp only [execStmt]
          exact ihW m st test body.toList orelse.toList k hk
        | forStmt target iter body orelse _ =>
          simp only [execStmt]
          cases horelse : orelse.toList with
          | cons o os => exact Run.le_refl _
          | nil =>
            refine Run.le_bind (ihE m st iter k hk) fun st it => ?_
            cases it <;> try exact Run.le_refl _
            case str s =>
              exact ihFor m st target (strCharVals s) body.toList k hk
            case bytes xs =>
              exact ihFor m st target (bytesIntVals xs) body.toList k hk
            case listV xs => exact ihFor m st target xs.toList body.toList k hk
            case tuple xs => exact ihFor m st target xs.toList body.toList k hk
            case ntuple tn fs xs => exact ihFor m st target xs.toList body.toList k hk
            case rangeV lo hi step =>
              exact Run.le_bind (Run.le_refl _) fun st xs =>
                ihFor m st target xs body.toList k hk
            case ref a => exact ihForL m st target a 0 body.toList k hk
        | ifStmt test body orelse _ =>
          simp only [execStmt]
          exact Run.le_bind (ihE m st test k hk) fun st t =>
            Run.le_bind (Run.le_refl _) fun st b =>
              Run.le_ite (ihSs m st body.toList k hk) (ihSs m st orelse.toList k hk)
        | exprStmt e _ =>
          simp only [execStmt]
          exact Run.le_bind (ihE m st e k hk) fun st v => Run.le_refl _
        | yieldStmt e _ => simp only [execStmt]; exact Run.le_refl _
        | pass _ => simp only [execStmt]; exact Run.le_refl _
        | brk _ => simp only [execStmt]; exact Run.le_refl _
        | cont _ => simp only [execStmt]; exact Run.le_refl _
        | unsupported pyKind text _ =>
          simp [execStmt]
          by_cases h : pyKind == "AnnAssign:no-value"
          · have hstr : pyKind = "AnnAssign:no-value" := by simpa using h
            subst pyKind
            simp [h, annNoValueName]
            exact Run.le_refl _
          · have hn : pyKind ≠ "AnnAssign:no-value" := by simpa using h
            simp [hn]
            exact Run.le_refl _
    -- execStmts
    · intro m st ss fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases ss with
        | nil => simp only [execStmts]; exact Run.le_refl _
        | cons s rest =>
          simp only [execStmts]
          refine Run.le_bind (ihS m st s k hk) fun st flow => ?_
          cases flow with
          | next => exact ihSs m st rest k hk
          | ret v => exact Run.le_refl _
          | brk => exact Run.le_refl _
          | cont => exact Run.le_refl _
    -- execWhile
    · intro m st test body orelse fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        simp only [execWhile]
        refine Run.le_bind (ihE m st test k hk) fun st t => ?_
        refine Run.le_bind (Run.le_refl _) fun st b => ?_
        refine Run.le_ite ?_ (ihSs m st orelse k hk)
        refine Run.le_bind (ihSs m st body k hk) fun st flow => ?_
        cases flow with
        | next => exact ihW m st test body orelse k hk
        | ret v => exact Run.le_refl _
        | brk => exact Run.le_refl _
        | cont => exact ihW m st test body orelse k hk
    -- callIn
    · intro m w fname args fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        simp only [callIn]
        cases findFunction m fname with
        | none => exact Run.le_refl _
        | some f =>
          -- argsOk / localsOk / arity guards, then the H4 generator
          -- branch (allocation only — fuel-independent)
          refine Run.le_ite (Run.le_refl _) (Run.le_ite (Run.le_refl _)
            (Run.le_ite (Run.le_refl _) (Run.le_ite (Run.le_refl _) ?_)))
          refine Run.le_toWorld
            (Run.le_bind
              (ihSs m
                ⟨w, markUnboundLocals f.body.toList (mkCallEnv f.params args)⟩
                f.body.toList k hk)
              fun st flow => ?_)
          cases flow <;> exact Run.le_refl _
    -- execFor
    · intro m st target xs body fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases xs with
        | nil => simp only [execFor]; exact Run.le_refl _
        | cons x rest =>
          simp only [execFor]
          refine Run.le_bind (Run.le_refl _) fun st env₁ => ?_
          refine Run.le_bind (ihSs m { st with locals := env₁ } body k hk)
            fun st flow => ?_
          cases flow with
          | next => exact ihFor m st target rest body k hk
          | cont => exact ihFor m st target rest body k hk
          | brk => exact Run.le_refl _
          | ret v => exact Run.le_refl _
    -- evalDictItems
    · intro m st keys values fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        cases keys with
        | nil => cases values <;> (simp only [evalDictItems]; exact Run.le_refl _)
        | cons kE ks =>
          cases values with
          | nil => simp only [evalDictItems]; exact Run.le_refl _
          | cons vE vs =>
            simp only [evalDictItems]
            exact Run.le_bind (ihE m st kE k hk) fun st kv =>
              Run.le_bind (ihE m st vE k hk) fun st vv =>
                Run.le_bind (ihItems m st ks vs k hk) fun st rest' =>
                  Run.le_refl _
    -- execForList (H2: the live list cursor)
    · intro m st target a i body fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        simp only [execForList]
        cases Heap.get? st.world.heap a with
        | none => exact Run.le_refl _
        | some o =>
          cases o with
          | dict es ver => exact Run.le_refl _
          | dictView da kind => exact Run.le_refl _
          | «instance» ci attrs => exact Run.le_refl _
          | cell cv => exact Run.le_refl _
          | closure nm ps ao lo' hg ig bd cap => exact Run.le_refl _
          | pyset zs => exact Run.le_refl _
          | generator qn lo kk stt =>
            exact Run.le_ite (Run.le_refl _) (ihForG m st target a body k hk)
          | list xs =>
            refine Run.le_ite ?_ (Run.le_refl _)
            refine Run.le_bind (Run.le_refl _) fun st env₁ => ?_
            refine Run.le_bind (ihSs m { st with locals := env₁ } body k hk)
              fun st flow => ?_
            cases flow with
            | next => exact ihForL m st target a (i + 1) body k hk
            | cont => exact ihForL m st target a (i + 1) body k hk
            | brk => exact Run.le_refl _
            | ret v => exact Run.le_refl _
    -- execAttrCall (H3: the attribute-call dispatch)
    · intro m st a attr args fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        simp only [execAttrCall]
        cases attrCallPlan m st.world.heap a attr with
        | instMethod qname =>
          exact Run.le_bind (ihEs m st args k hk) fun st vs =>
            Run.le_withLocals
              (ihCall m st.world qname ((RVal.ref a :: vs).toArray) k hk)
        | instAttrValue => exact Run.le_refl _
        | attrMissing => exact Run.le_refl _
        | dictGet =>
          exact Run.le_bind (ihEs m st args k hk) fun st vs => Run.le_refl _
        | dictView kind => exact Run.le_refl _
        | dictClear =>
          -- pass 5: arg-eval then a fuel-free heap update
          exact Run.le_bind (ihEs m st args k hk) fun st vs => Run.le_refl _
        | listAppend =>
          exact Run.le_bind (ihEs m st args k hk) fun st vs => Run.le_refl _
        | listPop =>
          exact Run.le_bind (ihEs m st args k hk) fun st vs => Run.le_refl _
        | listInsert =>
          -- the §2.5 residue: arg-eval then a fuel-free clamped update
          exact Run.le_bind (ihEs m st args k hk) fun st vs => Run.le_refl _
        | refuse msg => exact Run.le_refl _
        | dangling => exact Run.le_refl _
    -- stepIter (H4: the generator stepper)
    · intro m w a fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        simp only [stepIter]
        cases Heap.get? w.heap a with
        | none => exact Run.le_refl _
        | some o =>
          cases o with
          | dict es ver => exact Run.le_refl _
          | list xs => exact Run.le_refl _
          | dictView da kind => exact Run.le_refl _
          | «instance» ci attrs => exact Run.le_refl _
          | cell cv => exact Run.le_refl _
          | closure nm ps ao lo' hg ig bd cap => exact Run.le_refl _
          | pyset zs => exact Run.le_refl _
          | generator qn lo kk stt =>
            cases stt with
            | closed => exact Run.le_refl _
            | failed error => exact Run.le_refl _
            | running => exact Run.le_refl _
            | created =>
              dsimp only
              cases Heap.update w.heap a (.generator qn lo kk .running) with
              | none => exact Run.le_refl _
              | some h₁ =>
                refine Run.le_toWorld (Run.le_bindE
                  (ihGen m ⟨{ w with heap := h₁ }, lo⟩ kk k hk)
                  (fun st r => ?_)
                  (fun st e => ?_))
                · cases r with
                  | none =>
                    dsimp only
                    cases Heap.update st.world.heap a
                        (.generator qn st.locals [] .closed) <;> exact Run.le_refl _
                  | some p =>
                    obtain ⟨v, cont'⟩ := p
                    dsimp only
                    cases Heap.update st.world.heap a
                        (.generator qn st.locals cont' .suspended) <;> exact Run.le_refl _
                · -- the exceptions tier's close-on-exn arm: fuel-free
                  cases Heap.update st.world.heap a
                      (.generator qn st.locals [] .closed) <;> exact Run.le_refl _
            | suspended =>
              dsimp only
              cases Heap.update w.heap a (.generator qn lo kk .running) with
              | none => exact Run.le_refl _
              | some h₁ =>
                refine Run.le_toWorld (Run.le_bindE
                  (ihGen m ⟨{ w with heap := h₁ }, lo⟩ kk k hk)
                  (fun st r => ?_)
                  (fun st e => ?_))
                · cases r with
                  | none =>
                    dsimp only
                    cases Heap.update st.world.heap a
                        (.generator qn st.locals [] .closed) <;> exact Run.le_refl _
                  | some p =>
                    obtain ⟨v, cont'⟩ := p
                    dsimp only
                    cases Heap.update st.world.heap a
                        (.generator qn st.locals cont' .suspended) <;> exact Run.le_refl _
                · -- the exceptions tier's close-on-exn arm: fuel-free
                  cases Heap.update st.world.heap a
                      (.generator qn st.locals [] .closed) <;> exact Run.le_refl _
    -- execGen (H4: the continuation walker)
    · intro m st k fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ kf =>
        have hk : fuel ≤ kf := Nat.le_of_succ_le_succ hf
        -- `execGen` pattern-matches on the CONTINUATION as well as on
        -- fuel, so its equations only fire once the frame is concrete:
        -- case first, unfold per leaf.
        cases k with
        | nil => simp only [execGen]; exact Run.le_refl _
        | cons fr rest =>
          cases fr with
          | block ss =>
            cases ss with
            | nil => simp only [execGen]; exact ihGen m st rest kf hk
            | cons s ss' =>
              simp only [execGen]
              -- the H3 free-scrutinee discipline: fork on the PURE plan
              cases genPlan s with
              | delegate =>
                refine Run.le_bind (ihS m st s kf hk) fun st flow => ?_
                cases flow with
                | next => exact ihGen m st (.block ss' :: rest) kf hk
                | ret v => cases v <;> exact Run.le_refl _
                | brk =>
                  cases genBreak rest with
                  | none => exact Run.le_refl _
                  | some k'' => exact ihGen m st k'' kf hk
                | cont =>
                  cases genContinue rest with
                  | none => exact Run.le_refl _
                  | some k'' => exact ihGen m st k'' kf hk
              | yieldHere e =>
                exact Run.le_bind (ihE m st e kf hk) fun st v => Run.le_refl _
              | branch test body orelse =>
                refine Run.le_bind (ihE m st test kf hk) fun st t => ?_
                refine Run.le_bind (Run.le_refl _) fun st b => ?_
                exact ihGen m st _ kf hk
              | whileHere test body orelse => exact ihGen m st _ kf hk
              | forHere target iter body =>
                refine Run.le_bind (ihE m st iter kf hk) fun st it => ?_
                cases it with
                | none => exact Run.le_refl _
                | ellipsis => exact Run.le_refl _
                | bool b => exact Run.le_refl _
                | int n => exact Run.le_refl _
                | float value => exact Run.le_refl _
                | str sv => exact ihGen m st _ kf hk
                | bytes xs => exact ihGen m st _ kf hk
                | listV xs => exact ihGen m st _ kf hk
                | tuple xs => exact ihGen m st _ kf hk
                | ntuple tn fs xs => exact ihGen m st _ kf hk
                | rangeV lo hi step =>
                  exact Run.le_bind (Run.le_refl _) fun st xs => ihGen m st _ kf hk
                | ref ad =>
                  dsimp only
                  cases Heap.get? st.world.heap ad with
                  | none => exact Run.le_refl _
                  | some o =>
                    cases o with
                    | dict es ver => exact Run.le_refl _
                    | dictView da kind => exact Run.le_refl _
                    | «instance» ci attrs => exact Run.le_refl _
                    | cell cv => exact Run.le_refl _
                    | closure nm ps ao lo' hg ig bd cap => exact Run.le_refl _
                    | pyset zs => exact Run.le_refl _
                    | list xs => exact ihGen m st _ kf hk
                    | generator qn lo kk stt => exact ihGen m st _ kf hk
              | refuse msg => exact Run.le_refl _
          | forSeq target xs body =>
            cases xs with
            | nil => simp only [execGen]; exact ihGen m st rest kf hk
            | cons x rest' =>
              simp only [execGen]
              refine Run.le_bind (Run.le_refl _) fun st env₁ => ?_
              exact ihGen m { st with locals := env₁ } _ kf hk
          | forList target ad i body =>
            simp only [execGen]
            cases Heap.get? st.world.heap ad with
            | none => exact Run.le_refl _
            | some o =>
              cases o with
              | dict es ver => exact Run.le_refl _
              | dictView da kind => exact Run.le_refl _
              | «instance» ci attrs => exact Run.le_refl _
              | generator qn lo kk stt => exact Run.le_refl _
              | cell cv => exact Run.le_refl _
              | closure nm ps ao lo' hg ig bd cap => exact Run.le_refl _
              | pyset zs => exact Run.le_refl _
              | list xs =>
                refine Run.le_ite ?_ (ihGen m st rest kf hk)
                refine Run.le_bind (Run.le_refl _) fun st env₁ => ?_
                exact ihGen m { st with locals := env₁ } _ kf hk
          | forGen target ad body =>
            simp only [execGen]
            refine Run.le_bind (Run.le_withLocals (ihStep m st.world ad kf hk))
              fun st r => ?_
            cases r with
            | none => exact ihGen m st rest kf hk
            | some v =>
              refine Run.le_bind (Run.le_refl _) fun st env₁ => ?_
              exact ihGen m { st with locals := env₁ } _ kf hk
          | enumSeq i xs =>
            simp only [execGen]
            cases xs <;> first | exact ihGen m st rest kf hk | exact Run.le_refl _
          | enumList i ad cur =>
            simp only [execGen]
            cases Heap.get? st.world.heap ad with
            | none => exact Run.le_refl _
            | some o =>
              cases o with
              | list xs => exact Run.le_ite (Run.le_refl _) (ihGen m st rest kf hk)
              | dict es ver => exact Run.le_refl _
              | dictView da kind => exact Run.le_refl _
              | «instance» ci attrs => exact Run.le_refl _
              | generator qn lo kk stt => exact Run.le_refl _
              | cell cv => exact Run.le_refl _
              | closure nm ps ao lo' hg ig bd cap => exact Run.le_refl _
              | pyset zs => exact Run.le_refl _
          -- §3c-i-c: the trunk refuses to STEP `enumDict`; both fuels agree
          | enumDict i ad cur n sv kind => simp only [execGen]; exact Run.le_refl _
          -- §iter: the trunk's `iterDict` arm refuses; both fuels agree
          | iterDict ad cur n sv => simp only [execGen]; exact Run.le_refl _
          -- §iterList: and its `iterList` arm refuses for the same reason
          | iterList ad cur => simp only [execGen]; exact Run.le_refl _
          | iterBytes xs cur => simp only [execGen]; exact Run.le_refl _
          -- §3a: the trunk's `forDict` arm refuses; both fuels agree
          | forDict tg ad i n sv kd bd => simp only [execGen]; exact Run.le_refl _
          | countFrom cur step => simp only [execGen]; exact Run.le_refl _
          | countFromVal cur step => simp only [execGen]; exact Run.le_refl _
          | whileLoop test body orelse =>
            simp only [execGen]
            refine Run.le_bind (ihE m st test kf hk) fun st t => ?_
            refine Run.le_bind (Run.le_refl _) fun st b => ?_
            exact Run.le_ite (ihGen m st _ kf hk) (ihGen m st _ kf hk)
    -- execForGen (H4: the lazy `for` cursor)
    · intro m st target a body fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        simp only [execForGen]
        refine Run.le_bind (Run.le_withLocals (ihStep m st.world a k hk))
          fun st r => ?_
        cases r with
        | none => exact Run.le_refl _
        | some v =>
          refine Run.le_bind (Run.le_refl _) fun st env₁ => ?_
          refine Run.le_bind (ihSs m { st with locals := env₁ } body k hk)
            fun st flow => ?_
          cases flow with
          | next => exact ihForG m st target a body k hk
          | cont => exact ihForG m st target a body k hk
          | brk => exact Run.le_refl _
          | ret v => exact Run.le_refl _
    -- drainIter (H6: the full drain)
    · intro m w a fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        simp only [drainIter]
        refine Run.le_bind (ihStep m w a k hk) fun w r => ?_
        cases r with
        | none => exact Run.le_refl _
        | some v =>
          exact Run.le_bind (ihDrain m w a k hk) fun w vs => Run.le_refl _
    -- anyAllIter (H6: the short-circuit drain)
    · intro m w a isAll fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        simp only [anyAllIter]
        refine Run.le_bind (ihStep m w a k hk) fun w r => ?_
        cases r with
        | none => exact Run.le_refl _
        | some v =>
          refine Run.le_bind (Run.le_refl _) fun w b => ?_
          split
          · exact Run.le_refl _
          · exact ihAnyAll m w a isAll k hk
    -- callClosure (H7: the closure invocation)
    · intro m w name params ao lo ig body cap args fuel' hf
      cases fuel' with
      | zero => exact absurd hf (Nat.not_succ_le_zero fuel)
      | succ k =>
        have hk : fuel ≤ k := Nat.le_of_succ_le_succ hf
        simp only [callClosure]
        refine Run.le_ite (Run.le_refl _) (Run.le_ite (Run.le_refl _)
          (Run.le_ite (Run.le_refl _) ?_))
        refine Run.le_ite (Run.le_refl _) ?_
        refine Run.le_toWorld ?_
        refine Run.le_bind
          (ihSs m ⟨w, mkCallEnv params args ++ cap⟩ body.toList k hk)
          fun st flow => ?_
        cases flow <;> exact Run.le_refl _

/-! ## Per-function corollaries (the `FuelMono` statement shape) -/

private theorem mono_of_le {α : Type} {x y r : Res α}
    (hle : x ⊑ y) (h : x = r) (hr : r ≠ .timeout) : y = r := by
  subst h; exact (Res.le_eq hle hr).symm

private theorem mono_of_leR {σ α : Type} {x y r : Run σ α}
    (hle : x ⊑ʳ y) (h : x = r) (hr : r ≠ .timeout) : y = r := by
  subst h; exact (Run.le_eq hle hr).symm

/-- Fuel monotonicity for `evalExpr`: a decided outcome (state and value)
survives any fuel increase, exactly. -/
theorem evalExpr_mono {m : Module} {fuel : Nat} {st : FrameState} {e : Expr}
    {r : Run FrameState RVal} (h : evalExpr m fuel st e = r) (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, evalExpr m fuel' st e = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).1 m st e fuel' hf) h hr

/-- Fuel monotonicity for `evalExprs`. -/
theorem evalExprs_mono {m : Module} {fuel : Nat} {st : FrameState} {es : List Expr}
    {r : Run FrameState (List RVal)} (h : evalExprs m fuel st es = r)
    (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, evalExprs m fuel' st es = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).2.1 m st es fuel' hf) h hr

/-- Fuel monotonicity for `evalBoolChain`. -/
theorem evalBoolChain_mono {m : Module} {fuel : Nat} {st : FrameState} {op : BoolOp}
    {e : Expr} {rest : List Expr} {r : Run FrameState RVal}
    (h : evalBoolChain m fuel st op e rest = r) (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, evalBoolChain m fuel' st op e rest = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).2.2.1 m st op e rest fuel' hf) h hr

/-- Fuel monotonicity for `evalCompareChain`. -/
theorem evalCompareChain_mono {m : Module} {fuel : Nat} {st : FrameState} {lhs : RVal}
    {ops : List CmpOp} {cs : List Expr} {r : Run FrameState RVal}
    (h : evalCompareChain m fuel st lhs ops cs = r) (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, evalCompareChain m fuel' st lhs ops cs = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).2.2.2.1 m st lhs ops cs fuel' hf) h hr

/-- Fuel monotonicity for `execStmt`. -/
theorem execStmt_mono {m : Module} {fuel : Nat} {st : FrameState} {s : Stmt}
    {r : Run FrameState RFlow} (h : execStmt m fuel st s = r) (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, execStmt m fuel' st s = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).2.2.2.2.1 m st s fuel' hf) h hr

/-- Fuel monotonicity for `execStmts`. -/
theorem execStmts_mono {m : Module} {fuel : Nat} {st : FrameState} {ss : List Stmt}
    {r : Run FrameState RFlow} (h : execStmts m fuel st ss = r) (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, execStmts m fuel' st ss = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.1 m st ss fuel' hf) h hr

/-- Fuel monotonicity for `execWhile`. -/
theorem execWhile_mono {m : Module} {fuel : Nat} {st : FrameState} {test : Expr}
    {body orelse : List Stmt} {r : Run FrameState RFlow}
    (h : execWhile m fuel st test body orelse = r) (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, execWhile m fuel' st test body orelse = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.1 m st test body orelse fuel' hf) h hr

/-- Fuel monotonicity for `callIn`: a decided nested-call outcome (world
and value) is the same at every larger fuel. -/
theorem callIn_mono {m : Module} {w : World} {fname : String} {args : Array RVal}
    {fuel : Nat} {r : Run World RVal} (h : callIn m fuel w fname args = r)
    (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, callIn m fuel' w fname args = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.1 m w fname args fuel' hf) h hr

/-- Fuel monotonicity for `execFor`. -/
theorem execFor_mono {m : Module} {fuel : Nat} {st : FrameState} {target : Expr}
    {xs : List RVal} {body : List Stmt} {r : Run FrameState RFlow}
    (h : execFor m fuel st target xs body = r) (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, execFor m fuel' st target xs body = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.2.1 m st target xs body fuel' hf) h hr

/-- Fuel monotonicity for `evalDictItems`. -/
theorem evalDictItems_mono {m : Module} {fuel : Nat} {st : FrameState}
    {keys values : List Expr} {r : Run FrameState (List (RVal × RVal))}
    (h : evalDictItems m fuel st keys values = r) (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, evalDictItems m fuel' st keys values = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.2.2.1 m st keys values fuel' hf) h hr

/-- Fuel monotonicity for `execForList` (H2: the live list cursor). -/
theorem execForList_mono {m : Module} {fuel : Nat} {st : FrameState}
    {target : Expr} {a : Addr} {i : Nat} {body : List Stmt}
    {r : Run FrameState RFlow}
    (h : execForList m fuel st target a i body = r) (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, execForList m fuel' st target a i body = r := fun fuel' hf =>
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.2.2.2.1 m st target a i body fuel' hf) h hr

/-- Fuel monotonicity for `execAttrCall` (H3: the attribute-call
dispatch). -/
theorem execAttrCall_mono {m : Module} {fuel : Nat} {st : FrameState}
    {a : Addr} {attr : String} {args : List Expr} {r : Run FrameState RVal}
    (h : execAttrCall m fuel st a attr args = r) (hr : r ≠ .timeout)
    (fuel' : Nat) (hf : fuel ≤ fuel') : execAttrCall m fuel' st a attr args = r :=
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.2.2.2.2.1 m st a attr args fuel' hf) h hr

/-- Fuel monotonicity for `stepIter` (H4: the generator stepper). -/
theorem stepIter_mono {m : Module} {fuel : Nat} {w : World} {a : Addr}
    {r : Run World (Option RVal)} (h : stepIter m fuel w a = r)
    (hr : r ≠ .timeout) (fuel' : Nat) (hf : fuel ≤ fuel') :
    stepIter m fuel' w a = r :=
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.2.2.2.2.2.1 m w a fuel' hf) h hr

/-- Fuel monotonicity for `execGen` (H4: the continuation walker). -/
theorem execGen_mono {m : Module} {fuel : Nat} {st : FrameState} {k : GenCont}
    {r : Run FrameState (Option (RVal × GenCont))} (h : execGen m fuel st k = r)
    (hr : r ≠ .timeout) (fuel' : Nat) (hf : fuel ≤ fuel') :
    execGen m fuel' st k = r :=
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.2.2.2.2.2.2.1 m st k fuel' hf) h hr

/-- Fuel monotonicity for `execForGen` (H4: the lazy `for` cursor). -/
theorem execForGen_mono {m : Module} {fuel : Nat} {st : FrameState}
    {target : Expr} {a : Addr} {body : List Stmt} {r : Run FrameState RFlow}
    (h : execForGen m fuel st target a body = r) (hr : r ≠ .timeout)
    (fuel' : Nat) (hf : fuel ≤ fuel') :
    execForGen m fuel' st target a body = r :=
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.2.2.2.2.2.2.2.1 m st target a body fuel' hf) h hr

/-- Fuel monotonicity for `drainIter` (H6: the full drain). -/
theorem drainIter_mono {m : Module} {fuel : Nat} {w : World} {a : Addr}
    {r : Run World (List RVal)}
    (h : drainIter m fuel w a = r) (hr : r ≠ .timeout)
    (fuel' : Nat) (hf : fuel ≤ fuel') :
    drainIter m fuel' w a = r :=
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.1 m w a fuel' hf) h hr

/-- Fuel monotonicity for `anyAllIter` (H6: the short-circuit drain). -/
theorem anyAllIter_mono {m : Module} {fuel : Nat} {w : World} {a : Addr}
    {isAll : Bool} {r : Run World Bool}
    (h : anyAllIter m fuel w a isAll = r) (hr : r ≠ .timeout)
    (fuel' : Nat) (hf : fuel ≤ fuel') :
    anyAllIter m fuel' w a isAll = r :=
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.1 m w a isAll fuel' hf) h hr

/-- Fuel monotonicity for `callClosure` (H7: the closure invocation). -/
theorem callClosure_mono {m : Module} {fuel : Nat} {w : World} {name : String}
    {params : Array Param} {ao lo ig : Bool} {body : Array Stmt} {cap : REnv}
    {args : Array RVal} {r : Run World RVal}
    (h : callClosure m fuel w name params ao lo ig body cap args = r)
    (hr : r ≠ .timeout) (fuel' : Nat) (hf : fuel ≤ fuel') :
    callClosure m fuel' w name params ao lo ig body cap args = r :=
  mono_of_leR ((fuelMono fuel).2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2.2
    m w name params ao lo ig body cap args fuel' hf) h hr

mutual
  /-- Fuel monotonicity of the boundary freeze: the structural arms are
  fuel-independent; the `.ref` arm is `freezeHMono`. -/
  theorem RVal.freezeB_mono (h : Heap) :
      (v : RVal) → ∀ {fuel fuel' : Nat}, fuel ≤ fuel' →
        RVal.freezeB h fuel v ⊑ RVal.freezeB h fuel' v
    | .none, _, _, _ => Res.le_refl _
    | .ellipsis, _, _, _ => Res.le_refl _
    | .bool b, _, _, _ => Res.le_refl _
    | .int n, _, _, _ => Res.le_refl _
    | .float value, _, _, _ => Res.le_refl _
    | .str s, _, _, _ => Res.le_refl _
    | .bytes xs, _, _, _ => Res.le_refl _
    | .listV xs, _, _, hf => by
        simp only [RVal.freezeB]
        exact Res.le_bind (RVal.freezeListB_mono h xs.toList hf)
          fun vs => Res.le_refl _
    | .tuple xs, _, _, hf => by
        simp only [RVal.freezeB]
        exact Res.le_bind (RVal.freezeListB_mono h xs.toList hf)
          fun vs => Res.le_refl _
    | .ntuple _ _ _, _, _, _ => Res.le_refl _
    | .rangeV .., _, _, _ => Res.le_refl _
    | .ref a, fuel, fuel', hf => (freezeHMono fuel).1 h [] (.ref a) fuel' hf

  /-- Elementwise `freezeB_mono`. -/
  theorem RVal.freezeListB_mono (h : Heap) :
      (l : List RVal) → ∀ {fuel fuel' : Nat}, fuel ≤ fuel' →
        RVal.freezeListB h fuel l ⊑ RVal.freezeListB h fuel' l
    | [], _, _, _ => Res.le_refl _
    | v :: vs, _, _, hf => by
        simp only [RVal.freezeListB]
        exact Res.le_bind (RVal.freezeB_mono h v hf) fun v' =>
          Res.le_bind (RVal.freezeListB_mono h vs hf) fun vs' => Res.le_refl _
end

/-- Fuel monotonicity of the public erasure (H2): `freezeB_mono` at the
`.ok` arm. -/
theorem Run.toPublic_mono {x : Run World RVal} {fuel fuel' : Nat}
    (hf : fuel ≤ fuel') : Run.toPublic fuel x ⊑ Run.toPublic fuel' x := by
  cases x with
  | ok w v =>
    simp only [Run.toPublic_ok]
    exact RVal.freezeB_mono w.heap v hf
  | exn w e => exact Res.le_refl _
  | timeout => exact Res.le_refl _
  | unsupported msg => exact Res.le_refl _

/-- **Public fuel monotonicity**, derived through the wrapper decomposition
(docs/memory-model.md v2): thaw and init are fuel-free, `callIn_mono`
transports the decided run, and `Run.toPublic_mono` carries the freeze
leg (fuel-free on the ref-free fast path; `freezeHMono` on returned heap
lists). -/
theorem callFunction_mono {m : Module} {fname : String} {args : Array Val}
    {fuel : Nat} {r : Res Val} (h : callFunction m fname args fuel = r)
    (hr : r ≠ .timeout) :
    ∀ fuel' ≥ fuel, callFunction m fname args fuel' = r := by
  intro fuel' hf
  unfold callFunction at h ⊢
  rcases (fuelMono fuel).2.2.2.2.2.2.2.1 m (initWorld m) fname
      (RVal.thawArgs args) fuel' hf with hto | heq
  · -- The inner run timed out at `fuel`: then the public result was
    -- `.timeout`, contradicting `hr`.
    rw [hto] at h
    exact absurd h.symm (by simpa using hr)
  · rw [← heq]
    have hle := Run.toPublic_mono
      (x := callIn m fuel (initWorld m) fname (RVal.thawArgs args)) hf
    rw [h] at hle
    exact (Res.le_eq hle hr).symm

/-! ## Conditional world invariance (the heap-free fragment)

Since H1-proper dict literals ALLOCATE and subscript stores MUTATE, so
unconditional world invariance is gone. What survives — and what the
pinned-state proof layer runs on — is invariance over the HEAP-FREE
fragment (`Expr.heapFree`/`Stmt.heapFree`/`Module.heapFree`,
Semantics.lean): a decided `.ok` outcome of heap-free code carries exactly
the input world. The predicates are syntactic and kernel-computable, so
concrete modules discharge the hypotheses by `rfl` — that is the frame
theorem lifting pure `CallsTo` specs into the stateful `CallsIn` world
(`CallsTo.callsIn_frame`, Surface.lean). Heap READS (subscript reads,
membership, `len`, `.get`, `==`, truthiness) are world-preserving and stay
inside the fragment; loud and raising arms are vacuous for
`.ok`-invariance. -/

/-- `Run.OkW p x`: every decided `.ok` outcome of `x` lands in a state
satisfying `p` (nothing is claimed about `.exn`/`.timeout`/`.unsupported`
— the ok-chain is all the world-invariance consumers need). -/
def Run.OkW {σ α : Type} (p : σ → Prop) (x : Run σ α) : Prop :=
  ∀ s a, x = .ok s a → p s

namespace Run.OkW

theorem ok {σ α : Type} {p : σ → Prop} {s : σ} (h : p s) (a : α) :
    Run.OkW p (.ok s a) := fun _ _ he => by cases he; exact h

/-- `ok` with the frame-world predicate pinned in the statement shape —
the leaf the `worldInv` cases use (the generic `ok` at a `rfl` argument
commits the elaborator to a wrong higher-order predicate). -/
theorem okF {α : Type} {w : World} {st : FrameState} (h : st.world = w) (a : α) :
    Run.OkW (fun s : FrameState => s.world = w) (.ok st a) :=
  fun _ _ he => by cases he; exact h

/-- `ok` with the world-equality predicate pinned (the `callIn` leaf). -/
theorem okA {α : Type} {w w' : World} (h : w' = w) (a : α) :
    Run.OkW (fun x : World => x = w) (.ok w' a) :=
  fun _ _ he => by cases he; exact h

theorem exn {σ α : Type} {p : σ → Prop} {s : σ} {e : PyErr} :
    Run.OkW p (.exn s e : Run σ α) := fun _ _ he => by cases he

theorem timeout {σ α : Type} {p : σ → Prop} :
    Run.OkW p (.timeout : Run σ α) := fun _ _ he => by cases he

theorem unsupported {σ α : Type} {p : σ → Prop} {msg : String} :
    Run.OkW p (.unsupported msg : Run σ α) := fun _ _ he => by cases he

theorem mono {σ α : Type} {p q : σ → Prop} {x : Run σ α}
    (hpq : ∀ s, p s → q s) (h : Run.OkW p x) : Run.OkW q x :=
  fun s a he => hpq s (h s a he)

theorem bind {σ α β : Type} {p : σ → Prop} {x : Run σ α}
    {f : σ → α → Run σ β} (hx : Run.OkW p x)
    (hf : ∀ s a, p s → Run.OkW p (f s a)) : Run.OkW p (x.bind f) := by
  intro s' b h
  rw [Run.bind_eq_ok] at h
  obtain ⟨s, a, hx', hf'⟩ := h
  exact hf s a (hx s a hx') s' b hf'

theorem flattenStarRun_okW {σ : Type} {p : σ → Prop}
    {r : Run σ (List RVal)} (h : Run.OkW p r) :
    Run.OkW p (Run.bind r (fun s vs => .ok s (flattenStarCallArgs vs))) := by
  exact bind h (fun s vs hs => ok hs _)

theorem ite {σ α : Type} {p : σ → Prop} {c : Prop} [Decidable c]
    {x y : Run σ α} (hx : Run.OkW p x) (hy : Run.OkW p y) :
    Run.OkW p (if c then x else y) := by
  by_cases h : c
  · simpa only [if_pos h] using hx
  · simpa only [if_neg h] using hy

theorem liftRes {σ α : Type} {p : σ → Prop} {s : σ} (h : p s) (r : Res α) :
    Run.OkW p (Run.liftRes s r) := by
  intro s' a he
  rw [Run.liftRes_eq_ok] at he
  exact he.1 ▸ h

/-- `liftRes` with the frame-world predicate pinned (see `okF`). -/
theorem liftResF {α : Type} {w : World} {st : FrameState} (h : st.world = w)
    (r : Res α) :
    Run.OkW (fun s : FrameState => s.world = w) (Run.liftRes st r) := by
  intro s' a he
  rw [Run.liftRes_eq_ok] at he
  exact he.1 ▸ h

/-- A nested call whose out-world is pinned rides `withLocals` into a
frame whose world is pinned. -/
theorem withLocals {α : Type} {w : World} {l : REnv} {x : Run World α}
    (h : Run.OkW (· = w) x) :
    Run.OkW (fun st : FrameState => st.world = w) (Run.withLocals l x) := by
  intro st a he
  rw [Run.withLocals_eq_ok] at he
  obtain ⟨w', hx', rfl⟩ := he
  exact h w' a hx'

/-- A body run with pinned frame-world projects to a pinned out-world. -/
theorem toWorld {α : Type} {w : World} {x : Run FrameState α}
    (h : Run.OkW (fun st : FrameState => st.world = w) x) :
    Run.OkW (· = w) (Run.toWorld x) := by
  intro w' a he
  rw [Run.toWorld_eq_ok] at he
  obtain ⟨st, hx', rfl⟩ := he
  exact h st a hx'

end Run.OkW

/-- **Conditional world invariance**, one conjunction over the mutual
block (same order as `fuelMono`, minus `evalDictItems` — dict literals are
outside the fragment, so that conjunct would be vacuous): in a heap-free
module, every decided `.ok` outcome of heap-free code carries the input
world unchanged — `callIn`'s conjunct says a nested call returns exactly
the world it was given. See the section comment for scope. -/
theorem worldInv (m : Module) (hm : m.heapFree = true) (fuel : Nat) :
    (∀ (st : FrameState) (e : Expr), e.heapFree = true →
      Run.OkW (·.world = st.world) (evalExpr m fuel st e)) ∧
    (∀ (st : FrameState) (es : List Expr), Expr.heapFreeList es = true →
      Run.OkW (·.world = st.world) (evalExprs m fuel st es)) ∧
    (∀ (st : FrameState) (op : BoolOp) (e : Expr) (rest : List Expr),
        e.heapFree = true → Expr.heapFreeList rest = true →
      Run.OkW (·.world = st.world) (evalBoolChain m fuel st op e rest)) ∧
    (∀ (st : FrameState) (lhs : RVal) (ops : List CmpOp) (cs : List Expr),
        Expr.heapFreeList cs = true →
      Run.OkW (·.world = st.world) (evalCompareChain m fuel st lhs ops cs)) ∧
    (∀ (st : FrameState) (s : Stmt), s.heapFree = true →
      Run.OkW (·.world = st.world) (execStmt m fuel st s)) ∧
    (∀ (st : FrameState) (ss : List Stmt), Stmt.heapFreeList ss = true →
      Run.OkW (·.world = st.world) (execStmts m fuel st ss)) ∧
    (∀ (st : FrameState) (test : Expr) (body orelse : List Stmt),
        test.heapFree = true → Stmt.heapFreeList body = true →
        Stmt.heapFreeList orelse = true →
      Run.OkW (·.world = st.world) (execWhile m fuel st test body orelse)) ∧
    (∀ (w : World) (fname : String) (args : Array RVal),
      Run.OkW (· = w) (callIn m fuel w fname args)) ∧
    (∀ (st : FrameState) (target : Expr) (xs : List RVal) (body : List Stmt),
        Stmt.heapFreeList body = true →
      Run.OkW (·.world = st.world) (execFor m fuel st target xs body)) ∧
    (∀ (st : FrameState) (target : Expr) (a : Addr) (i : Nat) (body : List Stmt),
        Stmt.heapFreeList body = true →
      Run.OkW (·.world = st.world) (execForList m fuel st target a i body)) ∧
    -- generalized 2026-08-15 from `attr = "get"` to the whole
    -- `heapFreeAttr` whitelist (docs/backlog.md)
    (∀ (st : FrameState) (a : Addr) (attr : String) (args : List Expr),
        heapFreeAttr attr = true → Expr.heapFreeList args = true →
      Run.OkW (·.world = st.world) (execAttrCall m fuel st a attr args)) := by
  induction fuel with
  | zero =>
    refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
    · intro st e _ s a h; simp [evalExpr] at h
    · intro st es _ s a h; simp [evalExprs] at h
    · intro st op e rest _ _ s a h; simp [evalBoolChain] at h
    · intro st lhs ops cs _ s a h; simp [evalCompareChain] at h
    · intro st s _ s' a h; simp [execStmt] at h
    · intro st ss _ s a h; simp [execStmts] at h
    · intro st test body orelse _ _ _ s a h; simp [execWhile] at h
    · intro w fname args w' a h; simp [callIn] at h
    · intro st target xs body _ s a h; simp [execFor] at h
    · intro st target a i body _ s' a' h; simp [execForList] at h
    · intro st a attr args _ _ s' a' h; simp [execAttrCall] at h
  | succ fuel ih =>
    obtain ⟨ihE, ihEs, ihB, ihC, ihS, ihSs, ihW, ihCall, ihFor, ihForL, ihAttrC⟩ := ih
    have wtrans : ∀ (st st₁ : FrameState), st₁.world = st.world →
        ∀ s : FrameState, s.world = st₁.world → s.world = st.world :=
      fun _ _ h₁ _ h₂ => h₂.trans h₁
    refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
    -- evalExpr
    · intro st e hfree
      cases e with
      | constant c _ => simp only [evalExpr]; exact .okF rfl _
      | namedExpr id v _ => simp [Expr.heapFree] at hfree
      | name id _ =>
        simp only [evalExpr]
        cases Env.lookup st.locals id with
        | some v => exact .okF rfl _
        | none =>
          cases hu : hasUnboundLocal st.locals id with
          | true =>
            simp only [hu, if_true]
            exact .exn
          | false =>
            simp only [hu, Bool.false_eq_true, if_false]
            cases lookupG (moduleGlobals m).1 id with
            | some vv =>
              cases vv with
              | some v =>
                by_cases hname : id == "__name__"
                · simp [hname]
                  cases Env.lookup st.world.globals (deletedModuleDunderMarker id) with
                  | some dv => exact .okF rfl _
                  | none => exact .okF rfl _
                · simp [hname]
                  exact .okF rfl _
              | none =>
                -- pass 3: the poisoned-arm live view — a hit is a pure
                -- world read, a miss the old refusal
                cases Env.lookup st.world.globals id with
                | some v => exact .okF rfl _
                | none => exact .unsupported
            | none =>
              -- findFunction / findClass / findNamedTuple / isBuiltinName /
              -- isModuleDunder / the pass-3 live view / analysable → NameError
              refine .ite .unsupported (.ite .unsupported (.ite .unsupported
                (.ite .unsupported (.ite .unsupported ?_))))
              cases Env.lookup st.world.globals id with
              | some v => exact .okF rfl _
              -- the unmodelled-CPython-builtin refusal (2026-08-13) sits in
              -- front of the analysable/NameError fork
              | none => exact .ite (.okF rfl _) (.ite .unsupported (.ite .exn .unsupported))
      | binOp l op r _ =>
        cases hop : op == .bitAnd with
        | true =>
          cases op <;> try { change false = true at hop; cases hop }
          simp only [Expr.heapFree, Bool.and_eq_true] at hfree
          have hf := hfree.1.1
          change false = true at hf
          cases hf
        | false =>
          simp only [Expr.heapFree, Bool.and_eq_true] at hfree
          simp only [evalExpr, hop]
          exact .bind (ihE st l hfree.1.2) fun st₁ a h₁ =>
            .bind ((ihE st₁ r hfree.2).mono (wtrans st st₁ h₁)) fun st₂ b h₂ =>
              .liftResF h₂ _
      | unaryOp op operand _ =>
        simp only [Expr.heapFree] at hfree
        simp only [evalExpr]
        exact .bind (ihE st operand hfree) fun st₁ v h₁ => .liftResF h₁ _
      | formattedValue expression reprConversion _ =>
        simp only [Expr.heapFree] at hfree
        simp only [evalExpr]
        exact .bind (ihE st expression hfree) fun nextState value worldEq => .liftResF worldEq _
      | formattedValueAscii expression _ =>
        simp only [Expr.heapFree] at hfree
        simp only [evalExpr]
        exact .bind (ihE st expression hfree) fun nextState value worldEq => .liftResF worldEq _
      | boolOp op values _ =>
        simp only [Expr.heapFree] at hfree
        simp only [evalExpr]
        cases hv : values.toList with
        | nil => exact .unsupported
        | cons e0 es =>
          rw [hv] at hfree
          simp only [Expr.heapFreeList, Bool.and_eq_true] at hfree
          exact ihB st op e0 es hfree.1 hfree.2
      | compare l ops comparators _ =>
        simp only [Expr.heapFree, Bool.and_eq_true] at hfree
        simp only [evalExpr]
        exact .bind (ihE st l hfree.1) fun st₁ a h₁ =>
          (ihC st₁ a ops.toList comparators.toList hfree.2).mono (wtrans st st₁ h₁)
      | call cf cargs ckw cu _ =>
        cases cu with
        | some reason => simp only [evalExpr]; exact .unsupported
        | none =>
          -- H6: every `heapFree` call arm's FIRST conjunct pins
          -- `ckw.isEmpty`, so the keyword gate reduces to the positional
          -- path; in the catch-all arms both branches are loud
          cases cf <;> try (simp only [evalExpr]; exact .ite .unsupported .unsupported)
          case «attribute» recv attr spa =>
            -- the method tier: the FRAGMENT admits the `heapFreeAttr`
            -- whitelist — `.get` (a heap READ) plus the PURE str methods
            -- (2026-08-15, generalized from `.get`-only). `hfree` pins the
            -- attribute to the whitelist, which kills every MUTATING
            -- branch (`.clear`/`.append`/`.pop`/`.insert`); instance
            -- receivers dispatch to classes, and a heap-free module HAS
            -- no classes (hm), so the method branch is vacuous.
            simp only [Expr.heapFree, Bool.and_eq_true] at hfree
            obtain ⟨⟨⟨hkw, hattr⟩, hrecv⟩, hargsF⟩ := hfree
            -- pass 6: the trace-clock fork dies at its FIRST conjunct
            -- (`attr == "time"`, and `time` is deliberately outside the
            -- whitelist — the attr test sits outside the receiver match
            -- precisely so this closes before the receiver is evaluated)
            have hclk : isClockCall m st recv attr = false :=
              isClockCall_of_heapFreeAttr hattr
            simp only [evalExpr, hkw, if_true, hclk,
              Bool.false_eq_true, if_false]
            refine .bind (ihE st recv hrecv) fun st₁ r h₁ => ?_
            cases r <;>
              first
              | exact .exn
              | exact ((ihAttrC st₁ _ attr cargs.toList hattr hargsF).mono
                  (wtrans st st₁ h₁))
              | skip
            case ntuple tn fs xs =>
              -- heap-free: no classes ⇒ the plan never dispatches
              dsimp only
              rcases ntupleCallPlan_heapFree hm tn fs attr with hp | ⟨msg, hp⟩ <;>
                rw [hp]
              · exact .exn
              · exact .unsupported
            case str sv =>
              -- H5 strings (2026-08-15): the PURE str methods are IN the
              -- fragment now. Every in-tier arm is argument evaluation
              -- followed by `Run.liftRes` on a TOTAL PURE worker —
              -- strings are immutable VALUES, so nothing allocates and
              -- nothing mutates — while every arity miss is an `.exn`
              -- and every out-of-tier name a decided refusal.
              -- All five in-tier plans have ONE shape — evaluate the
              -- arguments, then decide purely — so one recipe closes
              -- them: `split` opens the arity matcher (and, for
              -- `.index`, the nested start/end `ite`), and every leaf is
              -- a `liftRes` of a pure worker, the faithful arity `.exn`,
              -- or a decided refusal. `split` rather than `cases` on the
              -- argument list: the recipe must not depend on how the
              -- 4-pattern matcher happened to compile.
              dsimp only
              have hvs := (Run.OkW.flattenStarRun_okW (ihEs st₁ cargs.toList hargsF)).mono
                (wtrans st st₁ h₁)
              cases strCallPlan attr <;>
                first
                | exact .unsupported
                | (refine .bind hvs fun st₂ vs h₂ => ?_
                   split <;> (try split) <;>
                     first
                     | exact .liftResF h₂ _
                     | exact .exn
                     | exact .unsupported)
            case float fv =>
              -- `float.is_integer()` preserves the world after its
              -- arguments have been evaluated, and its arity error is an
              -- exception carrying that same state.
              dsimp only
              split
              · refine .bind ((Run.OkW.flattenStarRun_okW (ihEs st₁ cargs.toList hargsF)).mono
                  (wtrans st st₁ h₁)) fun st₂ vs h₂ => ?_
                cases vs with
                | nil => exact .okF h₂ _
                | cons _ _ => exact .exn
              · exact .exn
          case name fname _ =>
            -- H2: `sorted` ALLOCATES its result, so the fragment excludes
            -- it (hfree carries `fname != "sorted"` — the branch is
            -- rewritten away before the ite walk)
            simp only [Expr.heapFree, Bool.and_eq_true] at hfree
            -- §iter added a TWELFTH exclusion (`iter` ALLOCATES a key cursor);
            -- it is discarded here because this interpreter has no `iter` arm,
            -- so the chain below has no branch for it to rewrite away.
            rcases hfree with ⟨hfree, hflE⟩
            rcases hfree with ⟨hfree, hff⟩
            rcases hfree with ⟨hfree, hlm⟩
            rcases hfree with ⟨hfree, _⟩
            rcases hfree with ⟨hfree, hndct⟩
            rcases hfree with ⟨hfree, hstarArg⟩
            rcases hfree with ⟨hfree, hstar⟩
            rcases hfree with ⟨hfree, hnlst⟩
            rcases hfree with ⟨hfree, hnpr⟩
            rcases hfree with ⟨hfree, hnset⟩
            rcases hfree with ⟨hfree, hnl⟩
            rcases hfree with ⟨hfree, hna⟩
            rcases hfree with ⟨hfree, hnc⟩
            rcases hfree with ⟨hfree, hne⟩
            rcases hfree with ⟨hfree, hnn⟩
            rcases hfree with ⟨hkw, hns⟩
            have hs : (fname == "sorted") = false := by
              cases hbe : fname == "sorted"
              · rfl
              · rw [bne, hbe] at hns; simp at hns
            have hlmx : (fname == lenMultBuiltinName) = false := by
              cases hbe : fname == lenMultBuiltinName
              · rfl
              · rw [bne, hbe] at hlm; simp at hlm
            have hffx : (fname == fstringFormatBuiltinName) = false := by
              cases hbe : fname == fstringFormatBuiltinName
              · rfl
              · rw [bne, hbe] at hff; simp at hff
            -- H4: `next` STEPS a generator and `enumerate`/`count`
            -- ALLOCATE an iterator object; H6 adds `any`/`all` (an
            -- unguarded short-circuit drain) — the fragment excludes all
            -- five, the same syntactic carve-out as `sorted`
            have hnx : (fname == "next") = false := by
              cases hbe : fname == "next"
              · rfl
              · rw [bne, hbe] at hnn; simp at hnn
            have hex : (fname == "enumerate") = false := by
              cases hbe : fname == "enumerate"
              · rfl
              · rw [bne, hbe] at hne; simp at hne
            have hcx : (fname == "count") = false := by
              cases hbe : fname == "count"
              · rfl
              · rw [bne, hbe] at hnc; simp at hnc
            have hay : (fname == "any") = false := by
              cases hbe : fname == "any"
              · rfl
              · rw [bne, hbe] at hna; simp at hna
            have hal : (fname == "all") = false := by
              cases hbe : fname == "all"
              · rfl
              · rw [bne, hbe] at hnl; simp at hnl
            have hsetx : (fname == "set") = false := by
              cases hbe : fname == "set"
              · rfl
              · rw [bne, hbe] at hnset; simp at hnset
            -- 2026-08-13: `print` MUTATES `World.stdout` (the one effect
            -- the interpreter performs), so the fragment excludes it the
            -- same syntactic way, and its branch is rewritten away below
            have hprx : (fname == "print") = false := by
              cases hbe : fname == "print"
              · rfl
              · rw [bne, hbe] at hnpr; simp at hnpr
            -- `list(…)` ALLOCATES a fresh heap object (2026-08-13,
            -- list comprehensions) — the `sorted` carve-out again
            have hlstx : (fname == "list") = false := by
              cases hbe : fname == "list"
              · rfl
              · rw [bne, hbe] at hnlst; simp at hnlst
            have hstarx : (fname == starListBuiltinName) = false := by
              cases hbe : fname == starListBuiltinName
              · rfl
              · rw [bne, hbe] at hstar; simp at hstar
            have hstarArgx : (fname == starArgBuiltinName) = false := by
              cases hbe : fname == starArgBuiltinName
              · rfl
              · rw [bne, hbe] at hstarArg; simp at hstarArg
            -- `dict(…)` ALLOCATES too (2026-08-13)
            have hdctx : (fname == "dict") = false := by
              cases hbe : fname == "dict"
              · rfl
              · rw [bne, hbe] at hndct; simp at hndct
            simp only [evalExpr, hkw, funsHeapFree, Module.heapFree_funs hm,
              eq_self_iff_true, if_true, hstarArgx]
            have hargs0 : Run.OkW (·.world = st.world) (evalExprs m fuel st cargs.toList) :=
              ihEs st cargs.toList hflE
            have hargs : Run.OkW (·.world = st.world)
                (flattenStarRun (evalExprs m fuel st cargs.toList)) := by
              exact Run.OkW.flattenStarRun_okW hargs0
            cases Env.lookup st.locals fname with
            | some v =>
              cases v <;>
                first
                | exact .unsupported
                | exact .bind hargs fun st₁ _ h₁ => .exn
                | skip
              case ref a =>
                -- H7 (+pass 3): hm's function-body walk AND top-level
                -- def-freedom discharge the guard — the closure call is
                -- unreachable in a heap-free module
                refine .bind hargs fun st₁ vs h₁ => ?_
                simp only [Module.heapFree_funs hm, Module.heapFree_topDefFree hm,
                  Bool.and_self, eq_self_iff_true, if_true]
                exact .exn
            | none =>
              cases lookupG (moduleGlobals m).1 fname with
              | some vv =>
                cases vv with
                | some v => cases v <;> exact .bind hargs fun st₁ _ h₁ => .exn
                | none =>
                  -- pass 3: the poisoned-arm live view — the guard kills
                  -- the closure dispatch in a heap-free module
                  cases Env.lookup st.world.globals fname with
                  | none => exact .unsupported
                  | some v =>
                    cases v <;>
                      first
                        | exact .bind hargs fun st₁ _ h₁ => .exn
                        | skip
                    case ref a =>
                      refine .bind hargs fun st₁ vs h₁ => ?_
                      simp only [Module.heapFree_funs hm, Module.heapFree_topDefFree hm,
                        Bool.and_self, eq_self_iff_true, if_true]
                      exact .exn
              | none =>
                -- a heap-free module has no classes: the instantiation
                -- branch reduces away; the def/namedtuple collision guard
                -- stays an undecided (walked) ite, and namedtuple
                -- CONSTRUCTION is a pure value — world-preserving
                simp only [hlmx, hffx, hs, hnx, hex, hcx, hay, hal, hsetx, hprx, hlstx, hstarx,
                  hstarArgx, hdctx,
                  findClass_heapFree hm fname,
                  Option.isSome_none, Bool.false_or, Bool.false_eq_true, if_false]
                refine .ite .exn ?_
                refine .ite (.ite .unsupported (.bind hargs fun st₁ vs h₁ => ?_)) ?_
                · exact ((ihCall st₁.world fname vs.toArray).withLocals
                    (l := st₁.locals)).mono
                      (fun s hs => (show s.world = st₁.world from hs).trans h₁)
                · cases hnt : findNamedTuple m fname with
                  | some nt =>
                    exact .bind hargs fun st₁ vs h₁ => .ite (.okF h₁ _) .exn
                  | none =>
                    refine .ite (.bind hargs fun st₁ vs h₁ => ?_) ?_
                    · cases vs with
                      | nil => exact .exn
                      | cons v rest =>
                        cases rest with
                        | nil => exact .liftResF h₁ _
                        | cons _ _ => exact .exn
                    · -- max/min (H6): the single-generator-argument arm
                      -- drains behind the `moduleGenFree` GUARD, which a
                      -- heap-free module discharges (`heapFree_genFree`)
                      -- — every other shape is the pure fold
                      refine .ite (.bind hargs fun st₁ vs h₁ => ?_) ?_
                      · cases vs with
                        | nil => exact .liftResF h₁ _
                        | cons v vtail =>
                          cases v <;> try exact .liftResF h₁ _
                          case ref a =>
                            cases vtail with
                            | cons _ _ => exact .liftResF h₁ _
                            | nil =>
                              dsimp only
                              cases Heap.get? st₁.world.heap a with
                              | none => exact .liftResF h₁ _
                              | some obj =>
                                cases obj <;> try exact .liftResF h₁ _
                                case generator q l c stat =>
                                  simp only [Module.heapFree_genFree hm,
                                    eq_self_iff_true, if_true]
                                  exact .unsupported
                      refine .ite (.bind hargs fun st₁ vs h₁ => ?_) ?_
                      · cases vs with
                        | nil => exact .liftResF h₁ _
                        | cons v vtail =>
                          cases v <;> try exact .liftResF h₁ _
                          case ref a =>
                            cases vtail with
                            | cons _ _ => exact .liftResF h₁ _
                            | nil =>
                              dsimp only
                              cases Heap.get? st₁.world.heap a with
                              | none => exact .liftResF h₁ _
                              | some obj =>
                                cases obj <;> try exact .liftResF h₁ _
                                case generator q l c stat =>
                                  simp only [Module.heapFree_genFree hm,
                                    eq_self_iff_true, if_true]
                                  exact .unsupported
                      refine .ite (.bind hargs fun st₁ vs h₁ => ?_) ?_
                      · cases vs with
                        | nil => exact .exn
                        | cons v rest =>
                          cases rest with
                          | nil => exact .liftResF h₁ _
                          | cons _ _ => exact .exn
                      · -- `round`, then `int`, then the pass-3 trio
                        -- `sum`/`tuple`/
                        -- `range` (value folds; the generator drains sit
                        -- behind the `moduleGenFree` guard, discharged by
                        -- `heapFree_genFree`), then `next` (rewritten
                        -- away by `hnx` — outside the fragment), the H5
                        -- pair `ord`/`chr`, then print / module dunder /
                        -- NameError / loud
                        refine .ite (.bind hargs fun st₁ vs h₁ => ?_)
                          (.ite (.bind hargs fun st₁ vs h₁ => ?_)
                          (.ite (.bind hargs fun st₁ vs h₁ => .liftResF h₁ _)
                           (.ite (.bind hargs fun st₁ vs h₁ => .liftResF h₁ _)
                           (.ite (.bind hargs fun st₁ vs h₁ => .liftResF h₁ _)
                           (.ite (.bind hargs fun st₁ vs h₁ => ?_)
                           (.ite (.bind hargs fun st₁ vs h₁ => ?_)
                            (.ite (.bind hargs fun st₁ vs h₁ => ?_)
                              (.ite (.bind hargs fun st₁ vs h₁ => .liftResF h₁ _)
                                (.ite (.bind hargs fun st₁ vs h₁ => ?_)
                                  (.ite (.bind hargs fun st₁ vs h₁ => ?_)
                                    (.ite (.bind hargs fun st₁ vs h₁ => ?_)
                                      (.ite (.bind hargs fun st₁ vs h₁ => ?_)
                                        (.ite (.bind hargs fun st₁ vs h₁ => by
                                          cases vs with
                                          | nil => exact .okF h₁ _
                                          | cons v rest =>
                                            cases rest with
                                            | nil => exact .liftResF h₁ _
                                            | cons _ _ => exact .unsupported)
                                        (.ite (.bind hargs fun st₁ vs h₁ => .liftResF h₁ _)
                                        (.ite .unsupported ?_)))))))))))))))
                        · cases vs with
                          | nil => exact .exn
                          | cons v rest =>
                            cases rest with
                            | nil =>
                              cases v <;>
                                first
                                | exact .okF h₁ _
                                | exact .unsupported
                            | cons _ _ => exact .unsupported
                        · exact .liftResF h₁ _
                        · cases vs with
                          | nil => exact .exn
                          | cons _ rest =>
                            cases rest with
                            | nil => exact .exn
                            | cons _ rest =>
                              cases rest with
                              | nil => exact .liftResF h₁ _
                              | cons _ rest =>
                                cases rest with
                                | nil => exact .liftResF h₁ _
                                | cons _ _ => exact .exn
                        · -- sum
                          cases sumArgs vs with
                          | none => exact .exn
                          | some pr =>
                            obtain ⟨v, start⟩ := pr
                            dsimp only
                            cases start <;> try exact .exn
                            all_goals
                              cases v <;> try exact .liftResF h₁ _
                            all_goals try exact .exn
                            all_goals
                              case ref a =>
                                dsimp only
                                cases Heap.get? st₁.world.heap a with
                                | none => exact .unsupported
                                | some obj =>
                                  cases obj <;>
                                    first
                                      | exact .liftResF h₁ _
                                      | exact .unsupported
                                      | exact .exn
                                      | skip
                                  case generator q l c stat =>
                                    simp only [Module.heapFree_genFree hm,
                                      eq_self_iff_true, if_true]
                                    exact .unsupported
                        · -- tuple
                          cases vs with
                          | nil => exact .okF h₁ _
                          | cons v vtail =>
                            cases vtail with
                            | cons _ _ => exact .exn
                            | nil =>
                              dsimp only
                              cases v <;>
                                first
                                  | exact .okF h₁ _
                                  | exact .liftResF h₁ _
                                  | exact .exn
                                  | skip
                              case ref a =>
                                dsimp only
                                cases Heap.get? st₁.world.heap a with
                                | none => exact .unsupported
                                | some obj =>
                                  cases obj <;>
                                    first
                                      | exact .okF h₁ _
                                      | exact .unsupported
                                      | exact .exn
                                      | skip
                                  case generator q l c stat =>
                                    simp only [Module.heapFree_genFree hm,
                                      eq_self_iff_true, if_true]
                                    exact .unsupported
                        · cases vs with
                          | nil => exact .exn
                          | cons v rest =>
                            cases rest with
                            | nil => exact .liftResF h₁ _
                            | cons _ _ => exact .exn
                        · cases vs with
                          | nil => exact .exn
                          | cons v rest =>
                            cases rest with
                            | nil => exact .liftResF h₁ _
                            | cons _ _ => exact .exn
                        · cases vs with
                          | nil => exact .exn
                          | cons v rest =>
                            cases rest with
                            | nil => exact .liftResF h₁ _
                            | cons _ _ => exact .exn
                        · -- format: the empty-spec and value-only forms are
                          -- pure rendering; non-empty specs and bad arities
                          -- are decided without changing the world
                          cases vs with
                          | nil => exact .exn
                          | cons v rest =>
                            cases rest with
                            | nil => exact .liftResF h₁ _
                            | cons spec rest' =>
                              cases rest' with
                              | nil =>
                                cases spec <;> try (simp only; exact .exn)
                                case str spec =>
                                  dsimp only
                                  split
                                  · exact .liftResF h₁ _
                                  · exact .liftResF h₁ _
                              | cons _ _ => simp only; exact .exn
                        · -- the pass-3 absent-arm live view: the guard
                          -- (funs + top-level def-freedom, both from hm)
                          -- kills the closure dispatch
                          cases hdu : isModuleDunder fname
                          · simp only [hdu, Bool.false_eq_true, if_false]
                            cases Env.lookup st.world.globals fname with
                            | none => exact .ite .unsupported (.ite .exn .unsupported)
                            | some v =>
                              cases v <;>
                                first
                                  | exact .bind hargs fun st₁ _ h₁ => .exn
                                  | skip
                              case ref a =>
                                refine .bind hargs fun st₁ vs h₁ => ?_
                                simp only [Module.heapFree_funs hm,
                                  Module.heapFree_topDefFree hm,
                                  Bool.and_self, eq_self_iff_true, if_true]
                                exact .exn
                          · simp only [hdu, if_true]
                            exact .unsupported
      | genExp elt tgt it ifs wb _ =>
        -- H4: a genexp ALLOCATES a generator — outside the fragment
        simp [Expr.heapFree] at hfree
      | list elts _ =>
        -- H2: list displays ALLOCATE — outside the fragment
        simp [Expr.heapFree] at hfree
      | tuple elts _ =>
        simp only [Expr.heapFree] at hfree
        simp only [evalExpr]
        exact .bind (ihEs st elts.toList hfree) fun st₁ vs h₁ => .okF h₁ _
      | subscript v idx _ =>
        simp only [Expr.heapFree, Bool.and_eq_true] at hfree
        simp only [evalExpr]
        exact .bind (ihE st v hfree.1) fun st₁ c h₁ =>
          .bind ((ihE st₁ idx hfree.2).mono (wtrans st st₁ h₁)) fun st₂ i h₂ =>
            .bind (.liftResF h₂ _) fun st₃ _ h₃ => .liftResF h₃ _
      | dict keys values _ =>
        -- outside the fragment: `heapFree = false` refutes the hypothesis
        simp [Expr.heapFree] at hfree
      | ifExp t b o _ =>
        simp only [Expr.heapFree, Bool.and_eq_true] at hfree
        simp only [evalExpr]
        refine .bind (ihE st t hfree.1.1) fun st₁ tv h₁ => ?_
        refine .bind (.liftResF h₁ _) fun st₂ cond h₂ => ?_
        exact .ite ((ihE st₂ b hfree.1.2).mono (wtrans st st₂ h₂))
          ((ihE st₂ o hfree.2).mono (wtrans st st₂ h₂))
      | slice v l u stp _ =>
        simp [Expr.heapFree] at hfree
      | «attribute» recv attr _ =>
        -- attribute READ (H3): a pure heap read — world-preserving; the
        -- bound-method/AttributeError forks are all ok-free or pinned
        simp only [Expr.heapFree] at hfree
        simp only [evalExpr]
        refine .bind (ihE st recv hfree) fun st₁ r h₁ => ?_
        cases r <;>
          first
          | exact .exn
          | exact .liftResF h₁ _
          | exact fun s₂ v₂ he => (attrReadResult_ok he) ▸ h₁
      | unsupported pyKind text _ => simp only [evalExpr]; exact .unsupported
    -- evalExprs
    · intro st es hfree
      cases es with
      | nil => simp only [evalExprs]; exact .okF rfl _
      | cons e rest =>
        simp only [Expr.heapFreeList, Bool.and_eq_true] at hfree
        simp only [evalExprs]
        exact .bind (ihE st e hfree.1) fun st₁ v h₁ =>
          .bind ((ihEs st₁ rest hfree.2).mono (wtrans st st₁ h₁)) fun st₂ vs h₂ =>
            .okF h₂ _
    -- evalBoolChain
    · intro st op e rest hfree hrest
      simp only [evalBoolChain]
      refine .bind (ihE st e hfree) fun st₁ v h₁ => ?_
      cases rest with
      | nil => exact .okF h₁ _
      | cons e' rest' =>
        simp only [Expr.heapFreeList, Bool.and_eq_true] at hrest
        refine .bind (.liftResF h₁ _) fun st₂ b h₂ => ?_
        cases op with
        | and =>
          exact .ite ((ihB st₂ .and e' rest' hrest.1 hrest.2).mono
            (wtrans st st₂ h₂)) (.okF h₂ _)
        | or =>
          exact .ite (.okF h₂ _) ((ihB st₂ .or e' rest' hrest.1 hrest.2).mono
            (wtrans st st₂ h₂))
    -- evalCompareChain
    · intro st lhs ops cs hfree
      cases ops with
      | nil =>
        cases cs with
        | nil => simp only [evalCompareChain]; exact .okF rfl _
        | cons c cs' => simp only [evalCompareChain]; exact .unsupported
      | cons op ops' =>
        cases cs with
        | nil => simp only [evalCompareChain]; exact .unsupported
        | cons e rest =>
          simp only [Expr.heapFreeList, Bool.and_eq_true] at hfree
          simp only [evalCompareChain]
          refine .bind (ihE st e hfree.1) fun st₁ rhs h₁ => ?_
          refine .bind (.liftResF h₁ _) fun stChecked _ hChecked => ?_
          refine .bind (.liftResF hChecked _) fun st₂ b h₂ => ?_
          exact .ite ((ihC st₂ rhs ops' rest hfree.2).mono (wtrans st st₂ h₂))
            (.okF h₂ _)
    -- execStmt
    · intro st s hfree
      cases s with
      | defStmt name params ao lo hg ig body caps _ =>
        simp [Stmt.heapFree] at hfree
      | unpackAssign before star after value _ =>
        simp [Stmt.heapFree] at hfree
      | yieldFromStmt v _ =>
        -- pass 5: OUT of the fragment (docs/memory-model.md §yield from)
        simp [Stmt.heapFree] at hfree
      | tryStmt body excName handler tu _ =>
        -- OUT of the fragment (as-built delta, docs/memory-model.md
        -- §exceptions): the handler resumes from the body's retained
        -- `.exn` state, invisible to the ok-only invariant
        simp [Stmt.heapFree] at hfree
      | withStmt items body tu _ =>
        simp [Stmt.heapFree] at hfree
      | importFrom mod names star _ =>
        -- Pass 0 (§import forms): IN the fragment, vacuously — the arm
        -- never decides `.ok` (it raises, fuel-free); the `raiseStmt`
        -- argument. The future modeled-module BINDING arm must flip
        -- `Stmt.heapFree` to `false` or re-prove this — the recorded
        -- review point.
        simp only [execStmt]
        exact .exn
      | raiseStmt exc cause _ =>
        -- IN the fragment, vacuously: the raise arm never decides `.ok`
        simp only [execStmt]
        cases cause with
        | some c => exact .unsupported
        | none =>
          cases exc with
          | none => exact .unsupported
          | some e =>
            cases e <;> try exact .unsupported
            case name id _ =>
              by_cases hunbound : hasUnboundLocal st.locals id
              · simp [hunbound]
                exact .exn
              · simp [hunbound]
                cases hlocal : Env.lookup st.locals id with
                | none =>
                  simp [hlocal]
                  refine .ite .unsupported ?_
                  cases findClass m id with
                  | none =>
                    refine .ite .exn ?_
                    by_cases hb : id ∈ admittedBuiltinRaise
                    · simp [hb]
                      exact .exn
                    · simp [hb]
                      exact .unsupported
                  | some p =>
                    obtain ⟨ci, c⟩ := p
                    exact .ite .exn .unsupported
                | some v =>
                  cases v <;> try exact .exn
                  case ref a => exact .unsupported
            case call func args kwargs cu _ =>
              cases func with
              | name id _ =>
                cases hkw : kwargs.toList with
                | cons _ _ =>
                  have hkwNonempty : kwargs.isEmpty = false := by
                    apply Bool.eq_false_iff.mpr
                    intro he
                    have hkwEmpty : kwargs = #[] := Array.isEmpty_iff.mp he
                    simp [hkwEmpty] at hkw
                  simp [hkwNonempty]
                  exact .unsupported
                | nil =>
                  have hkwEmpty : kwargs = #[] :=
                    Array.toList_inj.mp (by simpa using hkw)
                  cases hcu : cu with
                  | some reason => simp [hkw, hkwEmpty, hcu]; exact .unsupported
                  | none =>
                    simp [hkw, hkwEmpty, hcu]
                    split
                    · exact .unsupported
                    · cases hfc : findClass m id with
                      | some p =>
                        obtain ⟨ci, c⟩ := p
                        simp [hfc]
                        split
                        · cases args.toList with
                          | nil => exact .unsupported
                          | cons arg rest =>
                            cases rest with
                            | cons _ _ => simp; exact .unsupported
                            | nil =>
                              cases arg with
                              | constant c _ =>
                                cases c with
                                | str msg => simp; exact .exn
                                | _ => exact .unsupported
                              | _ => exact .unsupported
                        · exact .unsupported
                      | none =>
                        cases hnt : findNamedTuple m id with
                        | some nt => simp [hfc, hnt]; exact .unsupported
                        | none =>
                          by_cases hpy : isPyBuiltinName id
                          · simp [hfc, hnt, hpy]
                            cases args.toList with
                            | nil => exact .unsupported
                            | cons arg rest =>
                              cases rest with
                              | cons _ _ => simp; exact .unsupported
                              | nil =>
                                cases arg with
                                | constant c _ =>
                                  cases c with
                                  | str msg =>
                                    cases hbe : builtinExcWithMessage id msg with
                                    | some e => simp [hbe]; exact .exn
                                    | none =>
                                      simp [hbe]
                                      split <;> exact .unsupported
                                  | _ => exact .unsupported
                                | _ => exact .unsupported
                          · simp [hfc, hnt, hpy]
                            exact .exn
              | _ => exact .unsupported
      | assertStmt test msg _ =>
        -- the tail batch: IN the fragment and NOT vacuously — the
        -- passing path decides `.ok` with the input state untouched
        -- (nothing is allocated or mutated), the failing path raises.
        simp only [Stmt.heapFree, Bool.and_eq_true] at hfree
        simp only [execStmt]
        refine .bind (ihE st test hfree.1) fun st₁ t h₁ => ?_
        refine .bind (.liftResF h₁ _) fun st₂ b h₂ => ?_
        refine .ite (.okF h₂ _) ?_
        cases msg with
        | none => exact .exn
        | some e =>
          -- `(Option.map Expr.heapFree (some e)).getD true` reduces
          -- definitionally, so hfree.2 IS `e.heapFree = true`
          refine .bind ((ihE st₂ e hfree.2).mono (wtrans st st₂ h₂))
            fun st₃ v h₃ => ?_
          cases printOne st₃.world.heap v with
          | none => exact .unsupported
          | some r => exact .exn
      | delStmt names _ =>
        -- del RECONCILED: IN the fragment and NOT vacuously — the ok
        -- path rewrites only `st.locals`, which is not a `World` field
        -- (the recorded design's `.okF` pricing); the miss path refuses.
        simp only [execStmt]
        cases delNames st.locals names.toList with
        | mk env miss =>
          cases miss with
          | none => exact .okF rfl _
          | some n => exact .exn
      | yieldStmt e _ => simp only [execStmt]; exact .unsupported
      | ret value _ =>
        cases value with
        | none => simp only [execStmt]; exact .okF rfl _
        | some e =>
          simp only [Stmt.heapFree] at hfree
          simp only [execStmt]
          exact .bind (ihE st e hfree) fun st₁ v h₁ => .okF h₁ _
      | assign targets value _ =>
        simp only [Stmt.heapFree, Bool.and_eq_true] at hfree
        simp only [execStmt]
        cases htl : targets.toList with
        | nil => exact .unsupported
        | cons t rest =>
          rw [htl] at hfree
          cases rest with
          | nil =>
            cases t
            case subscript dE kE sp => exact absurd hfree.1 (by simp)
            case «attribute» recvE attr sp => exact absurd hfree.1 (by simp)
            case tuple elts sp =>
              -- pass 4: the fragment admits only the all-names fork
              -- (`targetNames.isSome` — hfree's first conjunct), which is
              -- the unchanged pure path
              have h1 : (targetNames elts).isSome = true := hfree.1
              dsimp only
              rw [if_pos h1]
              exact .bind (ihE st value hfree.2) fun st₁ v h₁ =>
                .bind (.liftResF h₁ _) fun st₂ env' h₂ =>
                  fun _ _ he => by cases he; exact h₂
            all_goals
              exact .bind (ihE st value hfree.2) fun st₁ v h₁ =>
                .bind (.liftResF h₁ _) fun st₂ env' h₂ =>
                  fun _ _ he => by cases he; exact h₂
          | cons t2 rest2 =>
            cases t <;> exact .unsupported
      | augAssign target op value _ =>
        cases target
        case «attribute» recvE attr _ =>
          -- pass 4: an attribute-target `+=` STORES — out of the fragment
          simp [Stmt.heapFree] at hfree
        case name id _ =>
          simp only [Stmt.heapFree, Bool.and_eq_true] at hfree
          simp only [execStmt]
          cases Env.lookup st.locals id with
          | none => exact .exn
          | some old =>
            cases old <;>
              first
              | exact .unsupported
              | exact .bind (ihE st value hfree.2) fun st₁ v h₁ =>
                  .bind (.liftResF h₁ _) fun st₂ r h₂ =>
                    fun _ _ he => by cases he; exact h₂
        all_goals simp only [execStmt]; exact .unsupported
      | whileLoop test body orelse _ =>
        simp only [Stmt.heapFree, Bool.and_eq_true] at hfree
        simp only [execStmt]
        exact ihW st test body.toList orelse.toList hfree.1.1 hfree.1.2 hfree.2
      | forStmt target iter body orelse _ =>
        simp only [Stmt.heapFree, Bool.and_eq_true] at hfree
        simp only [execStmt]
        cases orelse.toList with
        | cons o os => exact .unsupported
        | nil =>
          refine .bind (ihE st iter hfree.1.1) fun st₁ it h₁ => ?_
          cases it with
          | none => exact .exn
          | ellipsis => exact .exn
          | bool b => exact .exn
          | int n => exact .exn
          | float value => exact .exn
          | bytes xs =>
            exact (ihFor st₁ target _ body.toList hfree.1.2).mono
              (wtrans st st₁ h₁)
          | str s =>
            -- H5 iteration: a str's code points are a pure snapshot —
            -- the loop preserves the world exactly when the body does
            exact (ihFor st₁ target _ body.toList hfree.1.2).mono
              (wtrans st st₁ h₁)
          | listV xs =>
            exact (ihFor st₁ target _ body.toList hfree.1.2).mono
              (wtrans st st₁ h₁)
          | tuple xs =>
            exact (ihFor st₁ target _ body.toList hfree.1.2).mono
              (wtrans st st₁ h₁)
          | ntuple tn fs xs =>
            exact (ihFor st₁ target _ body.toList hfree.1.2).mono
              (wtrans st st₁ h₁)
          | rangeV lo hi step =>
            -- pass 3: materialization is a pure liftRes; the loop is the
            -- ordinary value-sequence `for`
            refine .bind (.liftResF h₁ _) fun st₂ xs h₂ => ?_
            exact (ihFor st₂ target _ body.toList hfree.1.2).mono
              (wtrans st st₂ h₂)
          | ref a =>
            -- H2: the list cursor (referent dispatch inside) preserves
            -- the world when the body does
            exact (ihForL st₁ target a 0 body.toList hfree.1.2).mono
              (wtrans st st₁ h₁)
      | ifStmt test body orelse _ =>
        simp only [Stmt.heapFree, Bool.and_eq_true] at hfree
        simp only [execStmt]
        refine .bind (ihE st test hfree.1.1) fun st₁ t h₁ => ?_
        refine .bind (.liftResF h₁ _) fun st₂ b h₂ => ?_
        exact .ite ((ihSs st₂ body.toList hfree.1.2).mono (wtrans st st₂ h₂))
          ((ihSs st₂ orelse.toList hfree.2).mono (wtrans st st₂ h₂))
      | exprStmt e _ =>
        simp only [Stmt.heapFree] at hfree
        simp only [execStmt]
        exact .bind (ihE st e hfree) fun st₁ v h₁ => .okF h₁ _
      | pass _ => simp only [execStmt]; exact .okF rfl _
      | brk _ => simp only [execStmt]; exact .okF rfl _
      | cont _ => simp only [execStmt]; exact .okF rfl _
      | unsupported pyKind text _ =>
        simp only [execStmt]
        by_cases h : pyKind == "AnnAssign:no-value"
        · have hstr : pyKind = "AnnAssign:no-value" := by simpa using h
          subst pyKind
          cases hn : annNoValueName text with
          | some id => simp [hn]; exact .okF rfl _
          | none => simp [hn]; exact .unsupported
        · have hn : pyKind ≠ "AnnAssign:no-value" := by simpa using h
          simp [hn]
          exact .unsupported
    -- execStmts
    · intro st ss hfree
      cases ss with
      | nil => simp only [execStmts]; exact .okF rfl _
      | cons s rest =>
        simp only [Stmt.heapFreeList, Bool.and_eq_true] at hfree
        simp only [execStmts]
        refine .bind (ihS st s hfree.1) fun st₁ flow h₁ => ?_
        cases flow with
        | next => exact (ihSs st₁ rest hfree.2).mono (wtrans st st₁ h₁)
        | ret v => exact .okF h₁ _
        | brk => exact .okF h₁ _
        | cont => exact .okF h₁ _
    -- execWhile
    · intro st test body orelse htest hbody horelse
      simp only [execWhile]
      refine .bind (ihE st test htest) fun st₁ t h₁ => ?_
      refine .bind (.liftResF h₁ _) fun st₂ b h₂ => ?_
      refine .ite ?_ ((ihSs st₂ orelse horelse).mono (wtrans st st₂ h₂))
      refine .bind ((ihSs st₂ body hbody).mono (wtrans st st₂ h₂))
        fun st₃ flow h₃ => ?_
      cases flow with
      | next =>
        exact (ihW st₃ test body orelse htest hbody horelse).mono
          (wtrans st st₃ h₃)
      | ret v => exact .okF h₃ _
      | brk => exact .okF h₃ _
      | cont =>
        exact (ihW st₃ test body orelse htest hbody horelse).mono
          (wtrans st st₃ h₃)
    -- callIn
    · intro w fname args
      simp only [callIn]
      cases hff : findFunction m fname with
      | none => exact .exn
      | some f =>
        -- H4: `f.isGenerator` is FALSE in a heap-free module (no
        -- generator defs — `Module.heapFree`'s third conjunct), so the
        -- allocating branch is rewritten away before the walk
        simp only [findFunction_notGen hm hff, Bool.false_eq_true, if_false]
        refine .ite .unsupported (.ite .unsupported (.ite .exn ?_))
        refine Run.OkW.toWorld ?_
        refine .bind
          (ihSs
            ⟨w, markUnboundLocals f.body.toList (mkCallEnv f.params args)⟩
            f.body.toList
          (findFunction_heapFree hm hff)) fun st₁ flow h₁ => ?_
        cases flow with
        | ret v => exact .okF h₁ _
        | next => exact .okF h₁ _
        | brk => exact .unsupported
        | cont => exact .unsupported
    -- execFor
    · intro st target xs body hbody
      cases xs with
      | nil => simp only [execFor]; exact .okF rfl _
      | cons x rest =>
        simp only [execFor]
        refine .bind (.liftResF rfl _) fun st₁ env₁ h₁ => ?_
        refine .bind ((ihSs { st₁ with locals := env₁ } body hbody).mono
          (fun s hs => hs.trans h₁)) fun st₂ flow h₂ => ?_
        cases flow with
        | next => exact (ihFor st₂ target rest body hbody).mono (wtrans st st₂ h₂)
        | cont => exact (ihFor st₂ target rest body hbody).mono (wtrans st st₂ h₂)
        | brk => exact .okF h₂ _
        | ret v => exact .okF h₂ _
    -- execForList (H2: the live cursor READS the list; a heap-free body
    -- keeps the world pinned through every step)
    · intro st target a i body hbody
      simp only [execForList]
      cases Heap.get? st.world.heap a with
      | none => exact .unsupported
      | some o =>
        cases o with
        | cell cv => exact .unsupported
        | dict es ver => exact .unsupported
        | dictView da kind => exact .unsupported
        | «instance» ci attrs => exact .exn
        | closure nm ps ao lo' hg ig bd cap => exact .unsupported
        | pyset zs => exact .unsupported
        | generator qn lo kk stt =>
          -- H4: a generator object cannot exist in a generator-free
          -- module, and the guard says so LOUDLY — which is exactly what
          -- keeps this theorem free of a heap-side invariant
          simp only [Module.heapFree_genFree hm, if_true]
          exact .unsupported
        | list xs =>
          refine .ite ?_ (.okF rfl _)
          refine .bind (.liftResF rfl _) fun st₁ env₁ h₁ => ?_
          refine .bind ((ihSs { st₁ with locals := env₁ } body hbody).mono
            (fun s hs => hs.trans h₁)) fun st₂ flow h₂ => ?_
          cases flow with
          | next => exact (ihForL st₂ target a (i + 1) body hbody).mono (wtrans st st₂ h₂)
          | cont => exact (ihForL st₂ target a (i + 1) body hbody).mono (wtrans st st₂ h₂)
          | brk => exact .okF h₂ _
          | ret v => exact .okF h₂ _
    -- execAttrCall (H3): in a heap-free module a WHITELISTED attribute
    -- plan is a heap READ or a decided refusal (`attrCallPlan_heapFree`)
    · intro st a attr args hattr hargs
      simp only [execAttrCall]
      rcases attrCallPlan_heapFree hm st.world.heap a hattr with
        hp | hp | hp | ⟨msg, hp⟩ <;> rw [hp]
      · refine .bind (ihEs st args hargs) fun st₂ vs h₂ => ?_
        cases vs with
        | nil => exact .exn
        | cons k rest =>
          cases rest with
          | nil => exact .liftResF h₂ _
          | cons d rest2 =>
            cases rest2 with
            | nil => exact .liftResF h₂ _
            | cons _ _ => exact .exn
      · exact .unsupported
      · exact .unsupported
      · exact .unsupported

/-- `evalExpr` world invariance, direct form (heap-free module and
expression). -/
theorem evalExpr_world {m : Module} {fuel : Nat} {st st' : FrameState}
    {e : Expr} {v : RVal} (hm : m.heapFree = true) (hfree : e.heapFree = true)
    (h : evalExpr m fuel st e = .ok st' v) :
    st'.world = st.world := (worldInv m hm fuel).1 st e hfree st' v h

/-- `evalExprs` world invariance, direct form. -/
theorem evalExprs_world {m : Module} {fuel : Nat} {st st' : FrameState}
    {es : List Expr} {vs : List RVal} (hm : m.heapFree = true)
    (hfree : Expr.heapFreeList es = true)
    (h : evalExprs m fuel st es = .ok st' vs) :
    st'.world = st.world := (worldInv m hm fuel).2.1 st es hfree st' vs h

/-- `execStmts` world invariance, direct form. -/
theorem execStmts_world {m : Module} {fuel : Nat} {st st' : FrameState}
    {ss : List Stmt} {flow : RFlow} (hm : m.heapFree = true)
    (hfree : Stmt.heapFreeList ss = true)
    (h : execStmts m fuel st ss = .ok st' flow) :
    st'.world = st.world := (worldInv m hm fuel).2.2.2.2.2.1 st ss hfree st' flow h

/-- `callIn` world invariance, direct form: in a heap-free module a nested
call hands back exactly the world it was given — the frame theorem's
engine (`CallsTo.callsIn_frame`, Surface.lean). -/
theorem callIn_world {m : Module} {fuel : Nat} {w w' : World} {fname : String}
    {args : Array RVal} {v : RVal} (hm : m.heapFree = true)
    (h : callIn m fuel w fname args = .ok w' v) :
    w' = w := (worldInv m hm fuel).2.2.2.2.2.2.2.1 w fname args w' v h

/-! ## The boundary-flip rescue lemma (docs/backlog.md, H2 step 3b)

Once `callFunction` thaws `Val.list` ARGUMENTS onto the heap
(`RVal.thawArgsH`), a `for` over a boundary-passed list runs the LIVE
cursor (`execForList`) instead of `execFor` over the transitional value
list — and the frozen-tail `for` induction pattern
(`Examples/python/sf_bound_for/proof.lean`) speaks `execFor`. The rescue:
over a heap-free module and a heap-free body, every iteration's world is
PINNED (`worldInv`), so the cursor's per-step re-read always sees the same
object — the live cursor IS `execFor` over the snapshot. -/

/-- The list element `execForList` reads at cursor `i` is the snapshot's
`i`-th element (bounds given). -/
private theorem getD_toList_getElem (xs : Array RVal) (i : Nat)
    (h : i < xs.size) : xs.getD i .none = xs.toList[i]'(by simpa using h) := by
  simp [Array.getD, h]

/-- **The live cursor is `execFor` on the snapshot** (pinned worlds): in a
heap-free module, iterating a heap list at `a` with a heap-free body from
cursor `i` is exactly `execFor` over the object's element snapshot from
`i` — same fuel, same outcome, states included. By induction on fuel: the
body cannot move the world (`execStmts_world`), so the next re-read sees
`xs` again. The H2 boundary flip's proof-rebase route rewrites
`execForList` to `execFor` through this and reuses the frozen-tail
induction pattern verbatim. -/
theorem execForList_eq_execFor_snapshot {m : Module} (hm : m.heapFree = true) :
    ∀ (fuel : Nat) (st : FrameState) (target : Expr) (a : Addr) (i : Nat)
      (body : List Stmt) (xs : Array RVal),
      Stmt.heapFreeList body = true →
      Heap.get? st.world.heap a = some (.list xs) →
      execForList m fuel st target a i body
        = execFor m fuel st target (xs.toList.drop i) body
  | 0, st, target, a, i, body, xs, _, _ => by
    simp [execForList, execFor]
  | fuel + 1, st, target, a, i, body, xs, hfree, hget => by
    rw [execForList, execFor.eq_def]
    rw [hget]
    dsimp only
    by_cases hi : i < xs.size
    · have hlen : i < xs.toList.length := by simpa using hi
      rw [if_pos hi, List.drop_eq_getElem_cons hlen]
      simp only [← getD_toList_getElem xs i hi]
      -- equal prefixes (the element bind and the body bind); the
      -- continuations agree on every reachable outcome. Case on the PURE
      -- helper results (never on the `Run` terms — `cases` on them
      -- generalizes `st` out of the context).
      cases hA : assignToH st.world.heap st.locals target (xs.getD i .none) with
      | ok env₁ =>
        rw [Run.liftRes_ok, Run.ok_bind, Run.ok_bind]
        cases hB : execStmts m fuel { st with locals := env₁ } body with
        | ok st₂ flow =>
          rw [Run.ok_bind, Run.ok_bind]
          -- `execStmts_world`'s RHS carries the record-literal state; its
          -- `.world` projection is DEFEQ to `st.world` (exact closes it)
          have hw₂ := execStmts_world hm hfree hB
          cases flow with
          | next =>
            have hget₂ : Heap.get? st₂.world.heap a = some (.list xs) := by
              rw [hw₂]; exact hget
            simpa using execForList_eq_execFor_snapshot hm
              fuel st₂ target a (i + 1) body xs hfree hget₂
          | cont =>
            have hget₂ : Heap.get? st₂.world.heap a = some (.list xs) := by
              rw [hw₂]; exact hget
            simpa using execForList_eq_execFor_snapshot hm
              fuel st₂ target a (i + 1) body xs hfree hget₂
          | brk => rfl
          | ret v => rfl
        | exn st₂ e => rw [Run.exn_bind, Run.exn_bind]
        | timeout => rw [Run.timeout_bind, Run.timeout_bind]
        | unsupported msg => rw [Run.unsupported_bind, Run.unsupported_bind]
      | exn e => rw [Run.liftRes_exn, Run.exn_bind, Run.exn_bind]
      | timeout => rw [Run.liftRes_timeout, Run.timeout_bind, Run.timeout_bind]
      | unsupported msg =>
        rw [Run.liftRes_unsupported, Run.unsupported_bind, Run.unsupported_bind]
    · rw [if_neg hi]
      have hdrop : xs.toList.drop i = [] :=
        List.drop_eq_nil_of_le (by simpa using Nat.le_of_not_lt hi)
      rw [hdrop]

/-! ## Cross-fuel determinism -/

/-- **Cross-fuel determinism**: two decided (non-`timeout`) results of the
same call, at *any* two fuels, are equal. Fuel is an implementation detail. -/
theorem callFunction_det {m : Module} {fname : String} {args : Array Val}
    {fuel₁ fuel₂ : Nat} {r₁ r₂ : Res Val}
    (h₁ : callFunction m fname args fuel₁ = r₁)
    (h₂ : callFunction m fname args fuel₂ = r₂)
    (hr₁ : r₁ ≠ .timeout) (hr₂ : r₂ ≠ .timeout) : r₁ = r₂ := by
  rcases Nat.le_total fuel₁ fuel₂ with hle | hle
  · exact (callFunction_mono h₁ hr₁ fuel₂ hle).symm.trans h₂
  · exact h₁.symm.trans (callFunction_mono h₂ hr₂ fuel₁ hle)

/-- `CallsTo` is functional: the returned value is unique across all fuels.
The spec-level payoff of `fuelMono`. -/
theorem CallsTo.functional {m : Module} {f : String} {args : Array Val}
    {v w : Val} (hv : CallsTo m f args v) (hw : CallsTo m f args w) : v = w := by
  obtain ⟨fuel₁, h₁⟩ := hv
  obtain ⟨fuel₂, h₂⟩ := hw
  have hd : (.ok v : Res Val) = .ok w :=
    callFunction_det h₁ h₂ (by simp) (by simp)
  exact Res.ok.inj hd

/-- A call cannot both return a value and raise: `==>` and `==>!` are
mutually exclusive (needed for outcome-uniqueness of the `Obs` spine). -/
theorem CallsTo.not_raises {m : Module} {f : String} {args : Array Val}
    {v : Val} {e : PyErr} (hv : CallsTo m f args v)
    (he : ∃ fuel, callFunction m f args fuel = .exn e) : False := by
  obtain ⟨fuel₁, h₁⟩ := hv
  obtain ⟨fuel₂, h₂⟩ := he
  have hd : (.ok v : Res Val) = .exn e :=
    callFunction_det h₁ h₂ (by simp) (by simp)
  cases hd

/-! ## The observation spine (`PyOut` / `Obs`)

The semantic spine of the spec surface (docs/spec-surface.md §10). Fuel
lives *inside* `Obs` and never above it: the decided outcomes
(`returns`/`raises`/`stuck`) assert that *some* fuel decides that way
(fuel monotonicity then makes every larger fuel agree), while `diverges`
asserts that *every* fuel times out. `stuck` (out of the supported tier,
`Res.unsupported`) is deliberately distinct from `diverges` — that
distinction is what keeps specs falsifiable on unsupported programs.

On message-uniqueness of `stuck` (decision, documented): outcomes are
compared *including* the message, because message-uniqueness holds — the
interpreter is a function of fuel, and `callFunction_det` makes any two
decided results (messages and all) equal across fuels. No "up to message"
quotient is needed. -/

/-- Everything a Python call can be observed to do — the outcome alphabet
of the `Obs` judgment. -/
inductive PyOut where
  /-- Terminates normally, returning `v`. -/
  | returns (v : Val)
  /-- Terminates by raising the Python error `e`. -/
  | raises (e : PyErr)
  /-- Never terminates: every fuel times out. -/
  | diverges
  /-- Leaves the supported semantic tier (`Res.unsupported msg`) — loud,
  and distinct from `diverges`. -/
  | stuck (msg : String)
deriving Repr, Inhabited, BEq

/-- The observation judgment: `Obs m f args o` — calling `f` in module `m`
on `args` is observed to do `o`. This is the fuel boundary: no judgment
built on `Obs` mentions fuel again. -/
def Obs (m : Module) (f : String) (args : Array Val) : PyOut → Prop
  | .returns v => ∃ fuel, callFunction m f args fuel = .ok v
  | .raises e => ∃ fuel, callFunction m f args fuel = .exn e
  | .diverges => ∀ fuel, callFunction m f args fuel = .timeout
  | .stuck msg => ∃ fuel, callFunction m f args fuel = .unsupported msg

/-- `returns` is exactly the spec-layer `CallsTo`. -/
@[simp] theorem Obs.returns_iff {m : Module} {f : String} {args : Array Val}
    {v : Val} : Obs m f args (.returns v) ↔ CallsTo m f args v := Iff.rfl

@[simp] theorem Obs.raises_iff {m : Module} {f : String} {args : Array Val}
    {e : PyErr} :
    Obs m f args (.raises e) ↔ ∃ fuel, callFunction m f args fuel = .exn e :=
  Iff.rfl

@[simp] theorem Obs.diverges_iff {m : Module} {f : String} {args : Array Val} :
    Obs m f args .diverges ↔ ∀ fuel, callFunction m f args fuel = .timeout :=
  Iff.rfl

@[simp] theorem Obs.stuck_iff {m : Module} {f : String} {args : Array Val}
    {msg : String} :
    Obs m f args (.stuck msg) ↔
      ∃ fuel, callFunction m f args fuel = .unsupported msg := Iff.rfl

/-- The decided `Res` value an outcome asserts (`diverges ↦ .timeout` — note
the readings differ: `Obs`'s `diverges` is "timeout at *every* fuel").
Injective, which is what reduces `Obs.det` to `callFunction_det`. -/
def PyOut.asRes : PyOut → Res Val
  | .returns v => .ok v
  | .raises e => .exn e
  | .diverges => .timeout
  | .stuck msg => .unsupported msg

theorem PyOut.asRes_inj {o₁ o₂ : PyOut} (h : o₁.asRes = o₂.asRes) : o₁ = o₂ := by
  cases o₁ <;> cases o₂ <;> simp_all [PyOut.asRes]

theorem PyOut.asRes_ne_timeout {o : PyOut} (h : o ≠ .diverges) :
    o.asRes ≠ .timeout := by
  cases o <;> first | exact absurd rfl h | simp [PyOut.asRes]

/-- A non-`diverges` outcome carries a fuel witness deciding exactly its
`asRes` value. -/
theorem Obs.decided {m : Module} {f : String} {args : Array Val} {o : PyOut}
    (h : Obs m f args o) (hd : o ≠ .diverges) :
    ∃ fuel, callFunction m f args fuel = o.asRes := by
  cases o with
  | returns v => exact h
  | raises e => exact h
  | diverges => exact absurd rfl hd
  | stuck msg => exact h

/-- **Outcome determinism**: a call has at most one observable outcome —
values, errors, and stuck *messages* included. Decided-vs-decided is
`callFunction_det` (FuelMono) through the injection `PyOut.asRes`;
decided-vs-`diverges` is a direct contradiction at the deciding fuel. -/
theorem Obs.det {m : Module} {f : String} {args : Array Val} {o₁ o₂ : PyOut}
    (h₁ : Obs m f args o₁) (h₂ : Obs m f args o₂) : o₁ = o₂ := by
  by_cases d₁ : o₁ = .diverges <;> by_cases d₂ : o₂ = .diverges
  · rw [d₁, d₂]
  · -- o₁ diverges but o₂ decides: contradiction at o₂'s fuel.
    subst d₁
    obtain ⟨fuel, hf⟩ := h₂.decided d₂
    exact absurd (hf.symm.trans (Obs.diverges_iff.mp h₁ fuel))
      (PyOut.asRes_ne_timeout d₂)
  · subst d₂
    obtain ⟨fuel, hf⟩ := h₁.decided d₁
    exact absurd (hf.symm.trans (Obs.diverges_iff.mp h₂ fuel))
      (PyOut.asRes_ne_timeout d₁)
  · obtain ⟨fuel₁, hf₁⟩ := h₁.decided d₁
    obtain ⟨fuel₂, hf₂⟩ := h₂.decided d₂
    exact PyOut.asRes_inj (callFunction_det hf₁ hf₂
      (PyOut.asRes_ne_timeout d₁) (PyOut.asRes_ne_timeout d₂))

/-- **Outcome totality** (classical): every call observes *some* outcome —
the four `PyOut` cases partition behaviours. Either every fuel times out
(`diverges`), or some fuel decides, and the decided constructor names the
outcome. -/
theorem Obs.total (m : Module) (f : String) (args : Array Val) :
    ∃ o, Obs m f args o := by
  by_cases h : ∀ fuel, callFunction m f args fuel = .timeout
  · exact ⟨.diverges, h⟩
  · obtain ⟨fuel, hf⟩ := Classical.not_forall.mp h
    cases hr : callFunction m f args fuel with
    | ok v => exact ⟨.returns v, fuel, hr⟩
    | exn e => exact ⟨.raises e, fuel, hr⟩
    | timeout => exact absurd hr hf
    | unsupported msg => exact ⟨.stuck msg, fuel, hr⟩

/-- The outcome of a call is a well-defined denotation: exactly one `PyOut`
observes (`Obs.total` + `Obs.det`; stated explicitly — no Mathlib `∃!`). -/
theorem Obs.existsUnique (m : Module) (f : String) (args : Array Val) :
    ∃ o, Obs m f args o ∧ ∀ o', Obs m f args o' → o' = o := by
  obtain ⟨o, ho⟩ := Obs.total m f args
  exact ⟨o, ho, fun o' ho' => Obs.det ho' ho⟩

end LeanModels.Python