From c8717b0b4aebfca620c1b099dee15ea6c23369d4 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 9 Sep 2026 09:16:16 +0000
Subject: [PATCH 01/28] feat: `ghost` declarations in `do` notation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds ghost state to `do` notation: `ghost x := e`, `ghost mut x := e`, `ghost x ← act`, and ghost patterns declare verification-only variables that loop `invariant` clauses and assertions can read while compiled code carries only a dummy in their place.

A ghost variable holds a value of the new type `Erased` in `Init.Data.Erased`, a copy of Mathlib's type. Reads are written `x.out`, reassignments wrap the value in `Erased.mk`, and `@[macro_inline]` on `Erased.mk` moves the argument into erased constructor fields before the noncomputability check, so ghost updates compile while any use of a ghost value in a relevant position is rejected through the noncomputability of `Erased.out`. The `grind` lemmas `Erased.out_mk` and `Erased.mk_out` discharge the verification conditions ghost variables produce.

`ghost` is a doElem of its own beside `let` and `have`, and both forms elaborate nondependently. The parsers `doGhost` and `doGhostArrow` use `nonReservedSymbol "ghost " (includeIdent := true)`, so `ghost` stays a legal identifier, and a doElem head spelled `ghost … := …` or `ghost … ← …` always parses as a ghost declaration. A ghost pattern binds its variables plainly and shadows each with its ghost redeclaration; `ghost x ← act` runs the action and erases its result. Refutable ghost patterns and `|` alternatives are rejected, since erased data cannot decide control flow. Quotations naming the new parsers inside `Lean.Elab` use `internal.parseQuotWithCurrentStage` until stage0 includes them.
---
 src/Init/Data.lean                      |  1 +
 src/Init/Data/Erased.lean               | 43 ++++++++++++
 src/Lean/Elab/BuiltinDo/Let.lean        | 92 ++++++++++++++++++++++---
 src/Lean/Elab/Do/Basic.lean             | 18 ++---
 src/Lean/Elab/Do/InferControlInfo.lean  |  8 +++
 src/Lean/Parser/Do.lean                 | 10 ++-
 tests/elab/erased.lean                  | 14 ++--
 tests/elab/formatTerm.lean              |  5 ++
 tests/elab/formatTerm.lean.out.expected |  8 +++
 tests/elab/intrinsicVerification.lean   | 85 +++++++++++++++++++++++
 tests/elab/usesOfNoncomputable.lean     | 12 +---
 11 files changed, 258 insertions(+), 38 deletions(-)
 create mode 100644 src/Init/Data/Erased.lean

diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index 9f9f8037a7fb..ac4b205d730a 100644
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@@ -38,6 +38,7 @@ public import Init.Data.Queue
 public import Init.Data.Sum
 public import Init.Data.BEq
 public import Init.Data.Subtype
+public import Init.Data.Erased
 public import Init.Data.ULift
 public import Init.Data.PLift
 public import Init.Data.Zero
diff --git a/src/Init/Data/Erased.lean b/src/Init/Data/Erased.lean
new file mode 100644
index 000000000000..337f40475d72
--- /dev/null
+++ b/src/Init/Data/Erased.lean
@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Sebastian Graf
+-/
+module
+
+prelude
+public import Init.Classical
+public import Init.Ext
+import Init.Grind.Attr
+
+public section
+
+/-- A value hidden from compiled code. `Erased.mk 42` erases to a dummy at runtime, and
+proofs recover the `42` as `(Erased.mk 42).out`. -/
+@[expose] def Erased (α : Sort u) : Sort (max 1 u) :=
+  { s : α → Prop // ∃ a, (a = ·) = s }
+
+namespace Erased
+
+/-- Hides `a` in an `Erased α`. Compiled code drops the argument. -/
+@[expose, macro_inline] def mk {α : Sort u} (a : α) : Erased α :=
+  ⟨fun b => a = b, a, rfl⟩
+
+/-- The value hidden in `e`, available to proofs only. -/
+noncomputable def out {α : Sort u} (e : Erased α) : α :=
+  Classical.choose e.property
+
+@[simp, grind =] theorem out_mk {α : Sort u} (a : α) : (mk a).out = a :=
+  cast (congrFun (Classical.choose_spec (mk a).property) a).symm rfl
+
+@[simp, grind =] theorem mk_out {α : Sort u} (e : Erased α) : mk e.out = e := by
+  cases e with
+  | mk s h => exact Subtype.ext (Classical.choose_spec h)
+
+@[ext] theorem out_inj {α : Sort u} {a b : Erased α} (h : a.out = b.out) : a = b := by
+  rw [← mk_out a, ← mk_out b, h]
+
+@[simp, grind] theorem mk_inj {α : Sort u} {a b : α} : mk a = mk b ↔ a = b :=
+  ⟨fun h => by have := congrArg out h; rwa [out_mk, out_mk] at this, fun h => h ▸ rfl⟩
+
+end Erased
diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index 25c53116c1ba..0c578ddc26f8 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -6,6 +6,7 @@ Authors: Sebastian Graf
 module
 
 prelude
+import Init.Data.Erased  -- referenced by the `ghost` quotations
 public import Lean.Elab.Do.Basic
 meta import Lean.Parser.Do
 import Lean.Elab.BuiltinDo.Basic
@@ -13,20 +14,29 @@ import Lean.Elab.Do.PatternVar
 
 public section
 
+-- The `ghost` doElem quotations below need the current stage's parser until stage0 catches up.
+set_option internal.parseQuotWithCurrentStage true
+
 namespace Lean.Elab.Do
 
 open Lean.Parser.Term
 open Lean.Meta
 
 inductive LetOrReassign
-  | let (mutTk? : Option Syntax)
+  | let (mutTk? ghostTk? : Option Syntax)
   | have
   | reassign
 
 def LetOrReassign.getLetMutTk? (letOrReassign : LetOrReassign) : Option Syntax :=
   match letOrReassign with
-  | .let mutTk? => mutTk?
-  | _           => none
+  | .let mutTk? _ => mutTk?
+  | _             => none
+
+/-- Whether the declaration carries the token of a `ghost` declaration. -/
+def LetOrReassign.isGhost (letOrReassign : LetOrReassign) : Bool :=
+  match letOrReassign with
+  | .let _ ghostTk? => ghostTk?.isSome
+  | _               => false
 
 def LetOrReassign.checkMutVars (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit :=
   match letOrReassign with
@@ -43,13 +53,13 @@ def elabDoLetOrReassignWith (hint : MessageData) (letOrReassign : LetOrReassign)
     (k : DoElabM Expr) (elabBody : (body : Term) → TermElabM Expr) : DoElabM Expr := do
   -- letOrReassign.checkMutVars vars -- Should be done by the caller!
   let elabCont : DoElabM Expr := do
-    declareMutVars? letOrReassign.getLetMutTk? vars do
+    declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isGhost do
       letOrReassign.registerReassignAliasInfo vars
       k
   doElabToSyntax hint elabCont fun body => elabBody body
 
 def elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) : DoElabM Expr := do
-  declareMutVars? letOrReassign.getLetMutTk? vars do
+  declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isGhost do
     letOrReassign.registerReassignAliasInfo vars
     k
 
@@ -164,6 +174,11 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
   | `(doIdDecl| $x:ident $[: $xType?]? ← $rhs) =>
     letOrReassign.checkMutVars #[x]
     let dec ← dec.ensureUnitAt tk
+    if letOrReassign matches .reassign then
+      if ((← findMutVar? x.getId).map (·.ghost)).getD false then
+        let y := mkIdentFrom x (← mkFreshUserName `__y)
+        return ← elabDoIdDecl y xType? rhs
+          (elabDoElem (← `(doElem| $x:ident := $y)) dec) (kind := dec.kind)
     -- For plain variable reassignment, we know the expected type of the reassigned variable and
     -- propagate it eagerly via type ascription if the user hasn't provided one themselves:
     let xType? ← match letOrReassign, xType? with
@@ -171,7 +186,7 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
         let decl ← getLocalDeclFromUserName x.getId
         some <$> Term.exprToSyntax decl.type
       | _, _ => pure xType?
-    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x <| dec.continueWithUnit)
+    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.isGhost <| dec.continueWithUnit)
       (kind := dec.kind)
   | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
@@ -182,9 +197,9 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
     elabDoIdDecl x patType? rhs do
       match letOrReassign, otherwise? with
-      | .let mutTk?, some otherwise =>
+      | .let mutTk? _, some otherwise =>
         elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x | $otherwise $(rest?)?)) dec
-      | .let mutTk?, _ =>
+      | .let mutTk? _, _ =>
         elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x)) dec
       | .have, some _otherwise =>
         throwUnsupportedSyntax
@@ -206,7 +221,50 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
 @[builtin_doElem_elab Lean.Parser.Term.doLet] def elabDoLet : DoElab := fun stx dec => do
   let `(doLet| let%$tk $[mut%$mutTk?]? $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
   let config ← getLetConfigAndCheckMut config mutTk?
-  elabDoLetOrReassign config (.let mutTk?) decl tk dec
+  elabDoLetOrReassign config (.let mutTk? none) decl tk dec
+
+/-- Elaborate `ghost $[mut]? $decl`. A single variable binds nondependently at the wrapped type:
+`ghost x : t := e` becomes `have x : Erased t := Erased.mk e`. A pattern binds its variables
+plainly and then shadows each one with its ghost redeclaration. -/
+@[builtin_doElem_elab Lean.Parser.Term.doGhost] def elabDoGhost : DoElab := fun stx dec => do
+  match stx with
+  | `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? := $e) =>
+    let declNew ← match t? with
+      | some t => `(letDecl| $x:ident : Erased $t := Erased.mk $e)
+      | none   => `(letDecl| $x:ident := Erased.mk $e)
+    elabDoLetOrReassign { nondep := true } (.let mutTk? (some tk)) declNew tk dec
+  | `(doGhost| ghost%$tk $[mut%$mutTk?]? $decl:letPatDecl) =>
+    let declNew : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
+    let vars ← getLetDeclVars declNew
+    let redecls ← vars.mapM fun v =>
+      return ⟨(← `(doGhost| ghost%$tk $[mut%$mutTk?]? $v:ident := $v:ident)).raw⟩
+    let dec ← dec.ensureUnitAt tk
+    let dec ← if redecls.isEmpty then pure dec else
+      pure <| DoElemCont.mk (← mkFreshUserName `__r) (← mkPUnit) (elabDoElems1 redecls dec) dec.kind
+    elabDoLetOrReassign {} (.let none none) declNew tk dec
+  | _ => throwUnsupportedSyntax
+
+/-- Elaborate `ghost $[mut]? x ← act`: bind the action's result plainly to a fresh variable and
+funnel it through `ghost x := y`, which wraps. At runtime the result is unused, so the element
+behaves like `_ ← act`. -/
+@[builtin_doElem_elab Lean.Parser.Term.doGhostArrow] def elabDoGhostArrow : DoElab := fun stx dec => do
+  match stx with
+  | `(doGhostArrow| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? ← $rhs) =>
+    checkMutVarsForShadowing #[x]
+    let dec ← dec.ensureUnitAt tk
+    let y := mkIdentFrom x (← mkFreshUserName `__y)
+    elabDoIdDecl y t? rhs
+      (elabDoElem ⟨(← `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident := $y)).raw⟩ dec)
+      (kind := dec.kind)
+  | `(doGhostArrow| ghost%$tk $[mut%$mutTk?]? $pat:term $[: $t?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
+    if otherwise?.isSome then
+      throwErrorAt tk "`ghost` takes no `|` alternative"
+    let dec ← dec.ensureUnitAt tk
+    let y := mkIdentFrom pat (← mkFreshUserName `__y)
+    elabDoIdDecl y t? rhs
+      (elabDoElem ⟨(← `(doGhost| ghost%$tk $[mut%$mutTk?]? $pat:term := $y)).raw⟩ dec)
+      (kind := dec.kind)
+  | _ => throwUnsupportedSyntax
 
 @[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do
   let `(doHave| have%$tk $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
@@ -228,11 +286,23 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   -- def doReassign := letIdDeclNoBinders <|> letPatDecl
   match stx with
   | `(doReassign| $x:ident $[: $xType?]? :=%$tk $rhs) =>
+    -- A ghost variable's reassignment wraps the value, so `x := e` stores `Erased.mk e` and an
+    -- ascription moves inside: `x : t := e` stores `Erased.mk (e : t)`.
+    let isGhostVar := ((← findMutVar? x.getId).map (·.ghost)).getD false
+    let (xType?, rhs) ← if isGhostVar then
+      match xType? with
+      | some t => pure (none, ← `(Erased.mk ($rhs : $t)))
+      | none   => pure (none, ← `(Erased.mk $rhs))
+    else
+      pure (xType?, rhs)
     let decl : TSyntax ``letIdDecl ← `(letIdDecl| $x:ident $[: $xType?]? := $rhs)
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
     elabDoLetOrReassign {} .reassign decl tk dec
   | `(doReassign| $decl:letPatDecl) =>
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
+    for var in (← getLetDeclVars decl) do
+      if ((← findMutVar? var.getId).map (·.ghost)).getD false then
+        throwErrorAt var "a ghost variable takes a plain reassignment, as in `{var.getId} := e`"
     elabDoLetOrReassign {} .reassign decl decl dec
   | _ => throwUnsupportedSyntax
 
@@ -241,7 +311,7 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
     | throwUnsupportedSyntax
   let config ← getLetConfigAndCheckMut cfg mutTk?
   checkLetConfigInDo config
-  let letOrReassign := LetOrReassign.let mutTk?
+  let letOrReassign := LetOrReassign.let mutTk? none
   let vars ← getPatternVarsEx pattern
   letOrReassign.checkMutVars vars
   let mut body ← body?.getDM `(doSeqIndent|pure PUnit.unit)
@@ -260,7 +330,7 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   checkLetConfigInDo config
   if config.nondep || config.usedOnly || config.zeta || config.eq?.isSome then
     throwErrorAt cfg "configuration options are not supported with `←`"
-  elabDoArrow (.let mutTk?) decl tk dec
+  elabDoArrow (.let mutTk? none) decl tk dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do
   match stx with
diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index c09624fdcb4d..35cbe6088336 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -103,6 +103,8 @@ structure MutVar where
   ident : Ident
   /-- The `FVarId` of the initial binding produced by `let mut`. -/
   baseId : FVarId
+  /-- Whether the variable comes from `let ghost mut`, so reassignments wrap in `Erased.mk`. -/
+  ghost : Bool := false
   deriving Inhabited
 
 /-- The raw `Name` of a `mut` variable, as found in the local context. -/
@@ -336,30 +338,30 @@ def DoOps.default : DoOps where
     return mkApp (← read).monadInfo.m α
 
 /-- Register the given name as that of a `mut` variable. -/
-def declareMutVar (x : Ident) (k : DoElabM α) : DoElabM α := do
+def declareMutVar (x : Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α := do
   let fvar ← getFVarFromUserName x.getId
-  let mutVar : MutVar := { ident := x, baseId := fvar.fvarId! }
+  let mutVar : MutVar := { ident := x, baseId := fvar.fvarId!, ghost }
   withReader (fun ctx => { ctx with
     mutVars := ctx.mutVars.push mutVar,
     mutVarDefs := ctx.mutVarDefs.insert x.getId mutVar,
   }) k
 
 /-- Register the given names as that of `mut` variables. -/
-def declareMutVars (xs : Array Ident) (k : DoElabM α) : DoElabM α := do
+def declareMutVars (xs : Array Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α := do
   let fvars ← xs.mapM (getFVarFromUserName ·.getId)
-  let newMutVars : Array MutVar := xs.zipWith (fun x fvar => { ident := x, baseId := fvar.fvarId! }) fvars
+  let newMutVars : Array MutVar := xs.zipWith (fun x fvar => { ident := x, baseId := fvar.fvarId!, ghost }) fvars
   withReader (fun ctx => { ctx with
     mutVars := ctx.mutVars ++ newMutVars,
     mutVarDefs := ctx.mutVarDefs.insertMany (newMutVars.map fun mutVar => (mutVar.getId, mutVar)),
   }) k
 
 /-- Register the given name as that of a `mut` variable if the syntax token `mut` is present. -/
-def declareMutVar? (mutTk? : Option Syntax) (x : Ident) (k : DoElabM α) : DoElabM α :=
-  if mutTk?.isSome then declareMutVar x k else k
+def declareMutVar? (mutTk? : Option Syntax) (x : Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α :=
+  if mutTk?.isSome then declareMutVar x ghost k else k
 
 /-- Register the given names as that of `mut` variables if the syntax token `mut` is present. -/
-def declareMutVars? (mutTk? : Option Syntax) (xs : Array Ident) (k : DoElabM α) : DoElabM α :=
-  if mutTk?.isSome then declareMutVars xs k else k
+def declareMutVars? (mutTk? : Option Syntax) (xs : Array Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α :=
+  if mutTk?.isSome then declareMutVars xs ghost k else k
 
 /-- Look up a declared `mut` variable by its raw `Name`. -/
 def findMutVar? (n : Name) : DoElabM (Option MutVar) := do
diff --git a/src/Lean/Elab/Do/InferControlInfo.lean b/src/Lean/Elab/Do/InferControlInfo.lean
index f7669e6274e3..e0948ceb477f 100644
--- a/src/Lean/Elab/Do/InferControlInfo.lean
+++ b/src/Lean/Elab/Do/InferControlInfo.lean
@@ -13,6 +13,9 @@ import Lean.Elab.Do.PatternVar
 
 public section
 
+-- The `ghost` doElem quotations below need the current stage's parser until stage0 catches up.
+set_option internal.parseQuotWithCurrentStage true
+
 namespace Lean.Elab.Do
 
 open Lean Meta Parser.Term
@@ -157,6 +160,11 @@ partial def ofElem (stx : DoElem) : TermElabM ControlInfo := do
     ofLetOrReassign #[] none otherwise body?
   | `(doElem| let $[mut]? $_:letConfig $decl) =>
     ofLetOrReassignArrow false decl
+  | `(doGhostArrow| ghost $[mut]? $decl:doIdDecl) =>
+    ofLetOrReassignArrow false decl
+  | `(doGhostArrow| ghost $[mut]? $decl:doPatDecl) =>
+    ofLetOrReassignArrow false decl
+  | `(doGhost| ghost $[mut]? $_) => return .pure
   | `(doElem| $decl:letIdDeclNoBinders) =>
     ofLetOrReassign (← getLetIdDeclVars ⟨decl⟩) none none none
   | `(doElem| $decl:letPatDecl) =>
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 4de4f788ff9f..cdd09478cf07 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -63,7 +63,8 @@ def notFollowedByRedefinedTermToken :=
   -- an "open" command follows the `do`-block.
   -- If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
   notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "match_expr" <|> "let" <|> "let_expr" <|> "have" <|>
-      "do" <|> "dbg_trace" <|> "idbg" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
+      "do" <|> "dbg_trace" <|> "idbg" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try" <|>
+      nonReservedSymbol "ghost ")
     "token at 'do' element"
 
 namespace InternalSyntax
@@ -109,6 +110,13 @@ Motivations:
 def letIdDeclNoBinders := leading_parser
   atomic (node ``letId ident >> pushNone >> optType >> " := ") >> termParser
 
+/-- `ghost x := e` declares a verification-only variable; `mut` allows reassignment. -/
+@[builtin_doElem_parser] def doGhost := leading_parser
+  nonReservedSymbol "ghost " (includeIdent := true) >> optional "mut " >> (letIdDeclNoBinders <|> letPatDecl)
+/-- `ghost x ← act` runs `act` and hides its result in a verification-only variable. -/
+@[builtin_doElem_parser] def doGhostArrow := leading_parser
+  nonReservedSymbol "ghost " (includeIdent := true) >> optional "mut " >> (doIdDecl <|> doPatDecl)
+
 @[builtin_doElem_parser] def doReassign      := leading_parser
   notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
 
diff --git a/tests/elab/erased.lean b/tests/elab/erased.lean
index 5f05656e5837..fe85abd14ce5 100644
--- a/tests/elab/erased.lean
+++ b/tests/elab/erased.lean
@@ -4,14 +4,14 @@ import Lean
   of `erased α` are erased in the VM in the same way as types
   and proofs. This can be used to track data without storing it
   literally. -/
-def Erased (α : Sort u) : Sort max 1 u :=
+def ErasedS (α : Sort u) : Sort max 1 u :=
   Σ's : α → Prop, ∃ a, (fun b => a = b) = s
 
-namespace Erased
+namespace ErasedS
 
 /-- Erase a value. -/
 @[inline]
-def mk {α} (a : α) : Erased α :=
+def mk {α} (a : α) : ErasedS α :=
   ⟨fun b => a = b, a, rfl⟩
 
 open Lean.Compiler
@@ -21,11 +21,11 @@ set_option pp.letVarTypes true
 set_option trace.Compiler.saveMono true
 /--
 trace: [Compiler.saveMono] size: 1
-    def Erased.mk._redArg (_dummy : lcVoid) : PSigma lcErased lcAny :=
+    def ErasedS.mk._redArg (_dummy : lcVoid) : PSigma lcErased lcAny :=
       let _x.1 : PSigma lcErased lcAny := PSigma.mk ◾ ◾ ◾ ◾;
       return _x.1
 [Compiler.saveMono] size: 1
-    def Erased.mk (α : lcErased) (a : lcAny) : PSigma lcErased lcAny :=
+    def ErasedS.mk (α : lcErased) (a : lcAny) : PSigma lcErased lcAny :=
       let _x.1 : PSigma lcErased lcAny := PSigma.mk ◾ ◾ ◾ ◾;
       return _x.1
 ---
@@ -43,7 +43,7 @@ trace: [Compiler.saveMono] size: 5
 [Compiler.saveMono] size: 9
     def _private.elab.erased.0._eval (a : @&Lean.Elab.Command.Context) (a : @&lcAny) (a.1 : lcVoid) : EST.Out
       Lean.Exception lcAny PUnit :=
-      let _x.2 : String := "Erased";
+      let _x.2 : String := "ErasedS";
       let _x.3 : String := "mk";
       let _x.4 : Lean.Name := Lean.Name.mkStr2 _x.2 _x.3;
       let _x.5 : Nat := 1;
@@ -58,4 +58,4 @@ trace: [Compiler.saveMono] size: 5
       return _x.10
 -/
 #guard_msgs in
-run_meta Lean.Compiler.compile #[``Erased.mk]
+run_meta Lean.Compiler.compile #[``ErasedS.mk]
diff --git a/tests/elab/formatTerm.lean b/tests/elab/formatTerm.lean
index db1d2e4c5299..7483cfbe0dd1 100644
--- a/tests/elab/formatTerm.lean
+++ b/tests/elab/formatTerm.lean
@@ -85,3 +85,8 @@ def foo : a b c d e f g a b c d e f g h where
   1 = 1 := rfl)
 
 #eval fmt `(by rw [] at h)
+
+-- `ghost` is its own declaration form beside `let` and `have`
+#eval fmt `(do ghost trace := 0; pure ())
+#eval fmt `(do ghost mut trace : List Nat := []; trace := x :: trace.out)
+#eval fmt `(do ghost mut n ← counter)
diff --git a/tests/elab/formatTerm.lean.out.expected b/tests/elab/formatTerm.lean.out.expected
index f03c982e5fdd..68e8b68202eb 100644
--- a/tests/elab/formatTerm.lean.out.expected
+++ b/tests/elab/formatTerm.lean.out.expected
@@ -142,3 +142,11 @@ calc
   1 = 1 := rfl✝
   1 = 1 := rfl✝
 by rw [] at h✝
+do
+  ghost trace✝ := 0;
+  pure✝ ()
+do
+  ghost mut trace✝ : List✝ Nat✝ := [];
+  trace✝ := x✝ :: trace.out✝
+do
+  ghost mut n✝ ← counter✝
diff --git a/tests/elab/intrinsicVerification.lean b/tests/elab/intrinsicVerification.lean
index 5ad1bd98405a..b3fb5fb9a128 100644
--- a/tests/elab/intrinsicVerification.lean
+++ b/tests/elab/intrinsicVerification.lean
@@ -889,3 +889,88 @@ def onOneLine (k : Nat) : Id Nat given (n : Nat) requires k = n ensures r => r =
 /-- info: onOneLine.spec : ∀ (k n : Nat), ⦃ k = n ⦄ onOneLine k ⦃ fun r => r = n ⦄ -/
 #guard_msgs in
 #check @onOneLine.spec
+
+/-! ## Ghost state
+
+`ghost` declares verification-only state. The variable holds an `Erased` value, an
+`invariant` clause reads it with `.out`, and its slot in compiled code holds a dummy. -/
+
+def ghostSumEvens (xs : List Nat) : Id Nat
+    ensures r => r % 2 = 0 := do
+  let mut acc := 0
+  ghost mut seen : List Nat := []
+  for x in xs invariant _pre _suff => acc = 2 * seen.out.length do
+    acc := acc + 2
+    seen := x :: seen.out
+  return acc
+
+/-- info: 6 -/
+#guard_msgs in
+#eval ghostSumEvens [1, 2, 3]
+
+/-! An existential `ensures` takes its witness from a ghost variable: the invariant carries the
+witness, and the exit condition instantiates the existential from it. -/
+
+def ghostDoubleSum (xs : List Nat) : Id Nat
+    ensures r => ∃ n, r = 2 * n := do
+  let mut acc := 0
+  ghost mut half : Nat := 0
+  for x in xs invariant _pre _suff => acc = 2 * half.out do
+    acc := acc + x + x
+    half := half.out + x
+  return acc
+
+/-- info: 12 -/
+#guard_msgs in
+#eval ghostDoubleSum [1, 2, 3]
+
+/-! The declaration forms: `ghost` with and without `mut`, reassignment with an ascription,
+monadic binds (the action runs, its result erases), and patterns. -/
+
+def ghostForms : Id Nat := do
+  ghost y := 5
+  ghost mut x := 1
+  x := x.out + y.out
+  x : Nat := 2
+  ghost z ← pure 3
+  ghost mut m ← pure 4
+  m := m.out + z.out
+  ghost (a, b) := (1, 2)
+  ghost mut (c, d) ← pure (3, 4)
+  c := a.out + b.out + d.out
+  pure 0
+
+/-- info: 0 -/
+#guard_msgs in
+#eval ghostForms
+
+/-! A ghost value reaching compiled code is rejected through the noncomputability of
+`Erased.out`. -/
+
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Erased.out', which is 'noncomputable'
+-/
+#guard_msgs in
+def ghostLeak (xs : List Nat) : Id Nat := do
+  ghost mut seen : List Nat := []
+  for x in xs do
+    seen := x :: seen.out
+  return seen.out.length
+
+/-! Erased data cannot decide control flow, so `ghost` takes no `|` alternative. -/
+
+/-- error: `ghost` takes no `|` alternative -/
+#guard_msgs in
+def ghostArrowElse (o : Option Nat) : Id Nat := do
+  ghost some x ← pure o | return 1
+  return 2
+
+/-! A ghost variable stays out of pattern reassignments. -/
+
+/-- error: a ghost variable takes a plain reassignment, as in `g := e` -/
+#guard_msgs in
+def ghostPatReassign : Id Nat := do
+  let mut a := 1
+  ghost mut g := 2
+  (a, g) := (3, Erased.mk 4)
+  pure a
diff --git a/tests/elab/usesOfNoncomputable.lean b/tests/elab/usesOfNoncomputable.lean
index 97d46d39b91d..5e58989e3fb6 100644
--- a/tests/elab/usesOfNoncomputable.lean
+++ b/tests/elab/usesOfNoncomputable.lean
@@ -41,17 +41,7 @@ error: failed to compile definition, consider marking it as 'noncomputable' beca
 #guard_msgs in
 def test9 (a : Nat) : V := ⟨a, badFun a⟩
 
-universe u
-
-def Erased (α : Sort u) : Sort max 1 u :=
-  { s : α → Prop // ∃ a, (a = ·) = s }
-
-@[macro_inline] def Erased.mk {α} (a : α) : Erased α :=
-  ⟨fun b => a = b, a, rfl⟩
-
-noncomputable def Erased.out {α} : Erased α → α
-  | ⟨_, h⟩ => Classical.choose h
-
+-- `Erased.mk` is `macro_inline`, so its argument erases and `.out` inside it compiles.
 structure Foo where
   spec : Erased Nat
   data : Nat

From 04404426eefb8752ad460ef8735b9c886e388233 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 9 Sep 2026 09:48:45 +0000
Subject: [PATCH 02/28] feat: ghost variables read at their underlying type

A ghost variable now appears at its underlying type everywhere the source names it: the local context, reassignment right-hand sides, `invariant` and `decreasing` clauses, and `assert`. The carried `Erased` binding takes an inaccessible name, and the source name binds a `.out` shadow that is zeta-substituted away at scope close, so it reaches proofs and never compiled code. Loop state tuples, join points, and nested-do tunneling carry the `Erased` binding; the shadow is re-introduced at every rebinding point.
---
 src/Lean/Elab/BuiltinDo/For.lean      | 25 ++++++--
 src/Lean/Elab/BuiltinDo/Let.lean      | 52 +++++++++--------
 src/Lean/Elab/Do/Basic.lean           | 83 +++++++++++++++++++--------
 src/Lean/Elab/Do/Control.lean         |  4 +-
 tests/elab/intrinsicVerification.lean | 41 +++++++++----
 5 files changed, 137 insertions(+), 68 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/For.lean b/src/Lean/Elab/BuiltinDo/For.lean
index 7c628bdad90e..92213b70e2d9 100644
--- a/src/Lean/Elab/BuiltinDo/For.lean
+++ b/src/Lean/Elab/BuiltinDo/For.lean
@@ -6,6 +6,7 @@ Authors: Sebastian Graf
 module
 
 prelude
+import Init.Data.Erased  -- referenced by the ghost shadow quotations
 public import Lean.Elab.BuiltinDo.Basic
 meta import Lean.Parser.Do
 meta import Std.WP.Gadget.ForIn
@@ -169,10 +170,21 @@ structure ForInApp where
   σ : Expr
   /-- The pattern naming the loop's mutable variables in the state tuple. -/
   statePat : Term
+  /-- The ghost variables among the loop's mutable variables; annotations bind their `.out`
+  shadows over the state tuple. -/
+  ghostMutVars : Array MutVar := #[]
+
+/-- Bind the `.out` shadow of each ghost variable over `e`, so that an annotation names ghost
+variables at their underlying type. The bindings sit in erased positions, so they compile. -/
+private def ForInApp.wrapGhostShadows (g : ForInApp) (e : Term) : DoElabM Term := do
+  let mut e := e
+  for mv in g.ghostMutVars do
+    e ← `(let $(mv.userIdent):ident := Erased.out $(⟨mv.ident.raw⟩); $e)
+  return e
 
 /-- Abstract `e` over the loop's state tuple, so that `e` may name the loop's mutable variables. -/
-private def ForInApp.mkStateFun (g : ForInApp) (e : Term) : DoElabM Term :=
-  `(fun $(g.statePat) => $e)
+private def ForInApp.mkStateFun (g : ForInApp) (e : Term) : DoElabM Term := do
+  `(fun $(g.statePat) => $(← g.wrapGhostShadows e))
 
 /-- Elaborate the gadget application that replaces the loop. The gadgets live downstream of this
 module, so `gadget` is an unresolved name that resolves in the user's context. -/
@@ -242,7 +254,7 @@ private def mkForInLoopGadget (g : ForInApp)
     -- unfolded type, and a specification's instance arguments are synthesized before the check that
     -- would unfold it.
     return ((invClause : Syntax), ← `($(mkIdent ``Std.WP.WhileInvariant.mk)
-      fun $exitVar:ident $(g.statePat) => $invBody))
+      fun $exitVar:ident $(g.statePat) => $(← g.wrapGhostShadows invBody)))
   let varArg? ← dec?.mapM fun decClause => do
     let (binders, body) ← match decClause with
       | `(doLoopDecreasing| decreasing $binders* => $body) => pure (binders, body)
@@ -279,7 +291,7 @@ private def mkForInLoopGadget (g : ForInApp)
   let info ← inferControlInfoSeq body
   let oldReturnCont ← getReturnCont
   let returnVarName ← mkFreshUserName `__r
-  let loopMutVars := mutVars.filter fun x => info.reassigns.contains x.getId
+  let loopMutVars := mutVars.filter fun x => info.reassigns.contains x.userName
   let loopMutVarNames :=
     if info.returnsEarly then
       returnVarName :: (loopMutVars.map (·.getId)).toList
@@ -297,7 +309,7 @@ private def mkForInLoopGadget (g : ForInApp)
       defs := defs.push returnVar
     for x in loopMutVars do
       let defn ← getLocalDeclFromUserName x.getId
-      Term.addTermInfo' x.ident defn.toExpr
+      Term.addTermInfo' x.userIdent defn.toExpr
       -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type.
       -- If we don't do this, then we are stuck on solving constraints such as
       --   `max ?u.46 ?u.47 =?= max (max ?u.22 ?u.46) ?u.47`
@@ -367,7 +379,8 @@ private def mkForInLoopGadget (g : ForInApp)
   let mut forIn := mkApp app body
   unless inv?.isNone && dec?.isNone do
     let g : ForInApp :=
-      { xs, init := preS, body, σ, statePat := ← mkStatePat loopMutVars info.returnsEarly }
+      { xs, init := preS, body, σ, statePat := ← mkStatePat loopMutVars info.returnsEarly,
+        ghostMutVars := loopMutVars.filter (·.ghost) }
     if (← instantiateMVars ρ).isConstOf ``Lean.Loop then
       if let some e ← mkForInLoopGadget g inv? dec? then forIn := e
     else if let some decClause := dec? then
diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index 0c578ddc26f8..5cc2615b831f 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -23,7 +23,7 @@ open Lean.Parser.Term
 open Lean.Meta
 
 inductive LetOrReassign
-  | let (mutTk? ghostTk? : Option Syntax)
+  | let (mutTk? : Option Syntax) (ghostUser? : Option Ident)
   | have
   | reassign
 
@@ -32,11 +32,11 @@ def LetOrReassign.getLetMutTk? (letOrReassign : LetOrReassign) : Option Syntax :
   | .let mutTk? _ => mutTk?
   | _             => none
 
-/-- Whether the declaration carries the token of a `ghost` declaration. -/
-def LetOrReassign.isGhost (letOrReassign : LetOrReassign) : Bool :=
+/-- The source identifier of a `ghost` declaration. -/
+def LetOrReassign.ghostUserIdent? (letOrReassign : LetOrReassign) : Option Ident :=
   match letOrReassign with
-  | .let _ ghostTk? => ghostTk?.isSome
-  | _               => false
+  | .let _ ghostUser? => ghostUser?
+  | _                 => none
 
 def LetOrReassign.checkMutVars (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit :=
   match letOrReassign with
@@ -53,13 +53,13 @@ def elabDoLetOrReassignWith (hint : MessageData) (letOrReassign : LetOrReassign)
     (k : DoElabM Expr) (elabBody : (body : Term) → TermElabM Expr) : DoElabM Expr := do
   -- letOrReassign.checkMutVars vars -- Should be done by the caller!
   let elabCont : DoElabM Expr := do
-    declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isGhost do
+    declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.ghostUserIdent? do
       letOrReassign.registerReassignAliasInfo vars
       k
   doElabToSyntax hint elabCont fun body => elabBody body
 
 def elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) : DoElabM Expr := do
-  declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isGhost do
+  declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.ghostUserIdent? do
     letOrReassign.registerReassignAliasInfo vars
     k
 
@@ -186,7 +186,7 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
         let decl ← getLocalDeclFromUserName x.getId
         some <$> Term.exprToSyntax decl.type
       | _, _ => pure xType?
-    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.isGhost <| dec.continueWithUnit)
+    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.ghostUserIdent? <| dec.continueWithUnit)
       (kind := dec.kind)
   | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
@@ -223,16 +223,19 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   let config ← getLetConfigAndCheckMut config mutTk?
   elabDoLetOrReassign config (.let mutTk? none) decl tk dec
 
-/-- Elaborate `ghost $[mut]? $decl`. A single variable binds nondependently at the wrapped type:
-`ghost x : t := e` becomes `have x : Erased t := Erased.mk e`. A pattern binds its variables
-plainly and then shadows each one with its ghost redeclaration. -/
+/-- Elaborate `ghost $[mut]? $decl`. A single variable `x : t := e` binds a carried
+`Erased t := Erased.mk e` under an inaccessible name, and the source name binds the `.out`
+shadow that proofs read. A pattern binds its variables plainly and then shadows each one with
+its ghost redeclaration. -/
 @[builtin_doElem_elab Lean.Parser.Term.doGhost] def elabDoGhost : DoElab := fun stx dec => do
   match stx with
   | `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? := $e) =>
+    let xc := mkIdentFrom x (← mkFreshUserName x.getId) (canonical := true)
     let declNew ← match t? with
-      | some t => `(letDecl| $x:ident : Erased $t := Erased.mk $e)
-      | none   => `(letDecl| $x:ident := Erased.mk $e)
-    elabDoLetOrReassign { nondep := true } (.let mutTk? (some tk)) declNew tk dec
+      | some t => `(letDecl| $xc:ident : Erased $t := Erased.mk $e)
+      | none   => `(letDecl| $xc:ident := Erased.mk $e)
+    let dec := { dec with k := withGhostShadow x xc.getId dec.k }
+    elabDoLetOrReassign { nondep := true } (.let mutTk? (some x)) declNew tk dec
   | `(doGhost| ghost%$tk $[mut%$mutTk?]? $decl:letPatDecl) =>
     let declNew : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
     let vars ← getLetDeclVars declNew
@@ -286,15 +289,18 @@ behaves like `_ ← act`. -/
   -- def doReassign := letIdDeclNoBinders <|> letPatDecl
   match stx with
   | `(doReassign| $x:ident $[: $xType?]? :=%$tk $rhs) =>
-    -- A ghost variable's reassignment wraps the value, so `x := e` stores `Erased.mk e` and an
-    -- ascription moves inside: `x : t := e` stores `Erased.mk (e : t)`.
-    let isGhostVar := ((← findMutVar? x.getId).map (·.ghost)).getD false
-    let (xType?, rhs) ← if isGhostVar then
-      match xType? with
-      | some t => pure (none, ← `(Erased.mk ($rhs : $t)))
-      | none   => pure (none, ← `(Erased.mk $rhs))
-    else
-      pure (xType?, rhs)
+    -- A ghost variable's reassignment rebinds the carried variable with the wrapped value, so
+    -- `x := e` stores `Erased.mk e` and an ascription moves inside: `x : t := e` stores
+    -- `Erased.mk (e : t)`. The source name then rebinds the fresh `.out` shadow.
+    if let some mv := (← findMutVar? x.getId).filter (·.ghost) then
+      let xc := mkIdentFrom x mv.getId
+      let rhs ← match xType? with
+        | some t => `(Erased.mk ($rhs : $t))
+        | none   => `(Erased.mk $rhs)
+      let decl : TSyntax ``letIdDecl ← `(letIdDecl| $xc:ident := $rhs)
+      let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
+      let dec := { dec with k := withGhostShadow mv.userIdent mv.getId dec.k }
+      return ← elabDoLetOrReassign {} .reassign decl tk dec
     let decl : TSyntax ``letIdDecl ← `(letIdDecl| $x:ident $[: $xType?]? := $rhs)
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
     elabDoLetOrReassign {} .reassign decl tk dec
diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index 35cbe6088336..b1cfdc0456a0 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -6,6 +6,7 @@ Authors: Sebastian Graf
 module
 
 prelude
+import Init.Data.Erased
 public import Lean.Elab.Do.InferControlInfo
 public import Lean.Elab.Binders
 import Lean.Meta.ProdN
@@ -99,23 +100,29 @@ def CodeLiveness.lub (a b : CodeLiveness) : CodeLiveness :=
 
 /-- A mutable variable declared by `let mut` in a `do` block. -/
 structure MutVar where
-  /-- The identifier of the `let mut` declaration. -/
+  /-- The binder identifier of the carried binding. For a ghost variable this is an inaccessible
+  name; the source name binds the `.out` shadow instead. -/
   ident : Ident
-  /-- The `FVarId` of the initial binding produced by `let mut`. -/
+  /-- The source identifier of the variable. Equals `ident` except for ghost variables. -/
+  userIdent : Ident
+  /-- The `FVarId` of the initial binding produced by the declaration. -/
   baseId : FVarId
-  /-- Whether the variable comes from `let ghost mut`, so reassignments wrap in `Erased.mk`. -/
+  /-- Whether the variable comes from `ghost mut`, so reassignments wrap in `Erased.mk`. -/
   ghost : Bool := false
   deriving Inhabited
 
-/-- The raw `Name` of a `mut` variable, as found in the local context. -/
+/-- The raw `Name` of a `mut` variable's carried binding, as found in the local context. -/
 def MutVar.getId (mutVar : MutVar) : Name := mutVar.ident.getId
 
+/-- The source name of a `mut` variable. -/
+def MutVar.userName (mutVar : MutVar) : Name := mutVar.userIdent.getId
+
 /--
 Build an `FVarAliasInfo` recording that the reassignment binding `id` aliases the original
 `let mut` binding represented by `mutVar`.
 -/
 def MutVar.mkAliasInfo (mutVar : MutVar) (id : FVarId) : FVarAliasInfo :=
-  { userName := mutVar.getId, id, baseId := mutVar.baseId }
+  { userName := mutVar.userName, id, baseId := mutVar.baseId }
 
 instance : ToMessageData MutVar where
   toMessageData mutVar :=
@@ -337,31 +344,35 @@ def DoOps.default : DoOps where
   mkMonadApp α := do
     return mkApp (← read).monadInfo.m α
 
-/-- Register the given name as that of a `mut` variable. -/
-def declareMutVar (x : Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α := do
+/-- Register the given name as that of a `mut` variable. A ghost variable passes its source
+identifier as `ghostUser?`, while `x` names the carried binding. -/
+def declareMutVar (x : Ident) (ghostUser? : Option Ident) (k : DoElabM α) : DoElabM α := do
   let fvar ← getFVarFromUserName x.getId
-  let mutVar : MutVar := { ident := x, baseId := fvar.fvarId!, ghost }
+  let mutVar : MutVar :=
+    { ident := x, userIdent := ghostUser?.getD x, baseId := fvar.fvarId!, ghost := ghostUser?.isSome }
   withReader (fun ctx => { ctx with
     mutVars := ctx.mutVars.push mutVar,
-    mutVarDefs := ctx.mutVarDefs.insert x.getId mutVar,
+    mutVarDefs := ctx.mutVarDefs.insert x.getId mutVar |>.insert mutVar.userName mutVar,
   }) k
 
 /-- Register the given names as that of `mut` variables. -/
-def declareMutVars (xs : Array Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α := do
+def declareMutVars (xs : Array Ident) (ghostUser? : Option Ident) (k : DoElabM α) : DoElabM α := do
   let fvars ← xs.mapM (getFVarFromUserName ·.getId)
-  let newMutVars : Array MutVar := xs.zipWith (fun x fvar => { ident := x, baseId := fvar.fvarId!, ghost }) fvars
+  let newMutVars : Array MutVar := xs.zipWith (fun x fvar =>
+    { ident := x, userIdent := ghostUser?.getD x, baseId := fvar.fvarId!, ghost := ghostUser?.isSome }) fvars
   withReader (fun ctx => { ctx with
     mutVars := ctx.mutVars ++ newMutVars,
-    mutVarDefs := ctx.mutVarDefs.insertMany (newMutVars.map fun mutVar => (mutVar.getId, mutVar)),
+    mutVarDefs := newMutVars.foldl (init := ctx.mutVarDefs) fun defs mutVar =>
+      defs.insert mutVar.getId mutVar |>.insert mutVar.userName mutVar,
   }) k
 
 /-- Register the given name as that of a `mut` variable if the syntax token `mut` is present. -/
-def declareMutVar? (mutTk? : Option Syntax) (x : Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α :=
-  if mutTk?.isSome then declareMutVar x ghost k else k
+def declareMutVar? (mutTk? : Option Syntax) (x : Ident) (ghostUser? : Option Ident) (k : DoElabM α) : DoElabM α :=
+  if mutTk?.isSome then declareMutVar x ghostUser? k else k
 
 /-- Register the given names as that of `mut` variables if the syntax token `mut` is present. -/
-def declareMutVars? (mutTk? : Option Syntax) (xs : Array Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α :=
-  if mutTk?.isSome then declareMutVars xs ghost k else k
+def declareMutVars? (mutTk? : Option Syntax) (xs : Array Ident) (ghostUser? : Option Ident) (k : DoElabM α) : DoElabM α :=
+  if mutTk?.isSome then declareMutVars xs ghostUser? k else k
 
 /-- Look up a declared `mut` variable by its raw `Name`. -/
 def findMutVar? (n : Name) : DoElabM (Option MutVar) := do
@@ -473,7 +484,10 @@ mut var definition of `y`.
 def withLCtxKeepingMutVarDefs (oldLCtx : LocalContext) (oldCtx : Context) (resultName : Name) (k : DoElabM α) : DoElabM α := do
   let oldMutVars := oldCtx.mutVars
   let oldMutVarDefs := oldCtx.mutVarDefs
-  let tunneledDefs := oldMutVarDefs.insert resultName default  -- tunneledDefs is used as a set, so the value doesn't matter
+  -- tunneledDefs is used as a set, so the value doesn't matter. Only carried bindings tunnel;
+  -- ghost `.out` shadows are zeta-substituted at their own scope.
+  let tunneledDefs := oldMutVars.foldl (init := ({} : Std.HashMap Name MutVar))
+    (fun defs mv => defs.insert mv.getId mv) |>.insert resultName default
   let newCtx ← addReachingDefsAsNonDep oldLCtx (← getLCtx) tunneledDefs
   withLCtx' newCtx <| withReader (fun ctx => { ctx with
     mutVars := oldMutVars,
@@ -604,14 +618,33 @@ def registerMutVarAlias (x : Name) : DoElabM Unit := do
     if id != baseMutVar.baseId then
       pushInfoLeaf <| .ofFVarAliasInfo (baseMutVar.mkAliasInfo id)
 
+/-- Bind `userIdent` to `carried.out` at the underlying type while `k` runs, and zeta-substitute
+the binding away, so the source name reaches proofs and never compiled code. -/
+def withGhostShadow (userIdent : Ident) (carriedName : Name) (k : DoElabM Expr) : DoElabM Expr := do
+  let carried ← getLocalDeclFromUserName carriedName
+  let ty ← instantiateMVars carried.type
+  let .app (.const ``Erased [u]) t := ty
+    | throwError "the carried binding of ghost variable `{userIdent.getId}` has type{indentExpr ty}\ninstead of an `Erased` type"
+  let outVal := mkApp2 (mkConst ``Erased.out [u]) t carried.toExpr
+  withLetDecl userIdent.getId t outVal (nondep := true) fun xv => do
+    Term.addLocalVarInfo userIdent xv
+    let body ← k
+    return (← body.abstractM #[xv]).instantiate1 outVal
+
+/-- Bind the `.out` shadow of each ghost variable among `mutVars` around `k`. -/
+def withGhostShadows (mutVars : Array MutVar) (k : DoElabM Expr) : DoElabM Expr :=
+  (mutVars.filter (·.ghost)).foldr (init := k) fun mv k => withGhostShadow mv.userIdent mv.getId k
+
 /--
 Given a list of mut vars `vars` and an FVar `tupleVar` binding a tuple, bind the mut vars to the
 fields of the tuple and call `k` in the resulting local context.
 -/
-def bindMutVarsFromTuple (vars : List Name) (tupleVar : FVarId) (k : DoElabM Expr) : DoElabM Expr :=
-  do go vars tupleVar (← tupleVar.getType) #[]
+def bindMutVarsFromTuple (vars : List Name) (tupleVar : FVarId) (k : DoElabM Expr) : DoElabM Expr := do
+  let ghosts := (← read).mutVars.filter fun mv => mv.ghost && vars.contains mv.getId
+  let k := withGhostShadows ghosts k
+  go vars tupleVar (← tupleVar.getType) #[] k
 where
-  go vars tupleVar tupleTy letFVars := do
+  go vars tupleVar tupleTy letFVars k := do
     let tuple := mkFVar tupleVar
     match vars with
     | []  => mkLetFVars letFVars (← k)
@@ -631,7 +664,7 @@ where
       withLetDecl x fstTy fst fun xf => do
         registerMutVarAlias x
         withLetDecl (← tupleVar.getUserName) sndTy snd fun r => do
-          go xs r.fvarId! sndTy (letFVars |>.push xf |>.push r)
+          go xs r.fvarId! sndTy (letFVars |>.push xf |>.push r) k
 
 /--
   Backtrackable state for the `TermElabM` monad.
@@ -684,7 +717,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     return ← caller nondupDec
   let γ := (← read).doBlockResultType
   let mγ ← mkMonadApp γ
-  let mutVars := (← read).mutVars |>.filter (callerInfo.reassigns.contains ·.getId)
+  let mutVars := (← read).mutVars |>.filter (callerInfo.reassigns.contains ·.userName)
   let mutVarNames := mutVars.map (·.getId)
   let joinName ← mkFreshUserName `__do_jp
   -- σ is the tuple type of the mut vars, or mγ if jumpCount = 0. Hence it is either level mi.u or mi.v.
@@ -700,7 +733,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     let mut e := mkApp jp' result
     for x in mutVars do
       let newX ← getFVarFromUserName x.getId
-      Term.addTermInfo' x.ident newX
+      Term.addTermInfo' x.userIdent newX
       e := mkApp e (← getFVarFromUserName x.getId)
     return e
 
@@ -713,8 +746,8 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
   let joinRhs ← joinRhsMVar.mvarId!.withContext do
     withLocalDeclD nondupDec.resultName nondupDec.resultType fun r => do
     withLocalDeclsDND (mutDecls.map fun (d : LocalDecl) => (d.userName, d.type)) fun muts => do
-    for (x, newX) in mutVars.zip muts do Term.addTermInfo' x.ident newX
-    let e ← (nondupDec.withDeadCodeFromInfo callerInfo).k
+    for (x, newX) in mutVars.zip muts do Term.addTermInfo' x.userIdent newX
+    let e ← withGhostShadows mutVars (nondupDec.withDeadCodeFromInfo callerInfo).k
     mkLambdaFVars (#[r] ++ muts) e
   unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do
     joinRhsMVar.mvarId!.withContext do
diff --git a/src/Lean/Elab/Do/Control.lean b/src/Lean/Elab/Do/Control.lean
index afef07b33d86..1a5fda615fa1 100644
--- a/src/Lean/Elab/Do/Control.lean
+++ b/src/Lean/Elab/Do/Control.lean
@@ -46,7 +46,7 @@ def ControlStack.stateT (baseMonadInfo : MonadInfo) (muts : Array MutVar) (σ :
     -- See also `StateT.monadControl.liftWith`.
     let mutExprs ← muts.mapM fun x => do
       let defn ← getLocalDeclFromUserName x.getId
-      Term.addTermInfo' x.ident defn.toExpr
+      Term.addTermInfo' x.userIdent defn.toExpr
       pure defn.toExpr
     let (tuple, tupleTy) ← mkProdMkN mutExprs baseMonadInfo.u
     unless ← isDefEq tupleTy σ do -- just for sanity; maybe delete in the future
@@ -208,7 +208,7 @@ structure EffectForwarder where
 /-- Build the lifter plan for a body whose effects are summarised by `info`. -/
 def EffectForwarder.ofCont (info : ControlInfo) (dec : DoElemCont) : DoElabM EffectForwarder := do
   let mi := (← read).monadInfo
-  let reassignedMutVars := (← read).mutVars |>.filter (info.reassigns.contains ·.getId)
+  let reassignedMutVars := (← read).mutVars |>.filter (info.reassigns.contains ·.userName)
   let reassignedMutVarNames := reassignedMutVars.map (·.getId)
   let ρ := (← getReturnCont).resultType
   let σ ← mkProdN (← reassignedMutVarNames.mapM (LocalDecl.type <$> getLocalDeclFromUserName ·)) mi.u
diff --git a/tests/elab/intrinsicVerification.lean b/tests/elab/intrinsicVerification.lean
index b3fb5fb9a128..7fbd85aa0cfb 100644
--- a/tests/elab/intrinsicVerification.lean
+++ b/tests/elab/intrinsicVerification.lean
@@ -892,16 +892,17 @@ def onOneLine (k : Nat) : Id Nat given (n : Nat) requires k = n ensures r => r =
 
 /-! ## Ghost state
 
-`ghost` declares verification-only state. The variable holds an `Erased` value, an
-`invariant` clause reads it with `.out`, and its slot in compiled code holds a dummy. -/
+`ghost` declares verification-only state. The variable reads at its underlying type everywhere,
+its carried `Erased` binding erases in compiled code, and its slot in a loop's state tuple holds
+a dummy. -/
 
 def ghostSumEvens (xs : List Nat) : Id Nat
     ensures r => r % 2 = 0 := do
   let mut acc := 0
   ghost mut seen : List Nat := []
-  for x in xs invariant _pre _suff => acc = 2 * seen.out.length do
+  for x in xs invariant _pre _suff => acc = 2 * seen.length do
     acc := acc + 2
-    seen := x :: seen.out
+    seen := x :: seen
   return acc
 
 /-- info: 6 -/
@@ -915,9 +916,9 @@ def ghostDoubleSum (xs : List Nat) : Id Nat
     ensures r => ∃ n, r = 2 * n := do
   let mut acc := 0
   ghost mut half : Nat := 0
-  for x in xs invariant _pre _suff => acc = 2 * half.out do
+  for x in xs invariant _pre _suff => acc = 2 * half do
     acc := acc + x + x
-    half := half.out + x
+    half := half + x
   return acc
 
 /-- info: 12 -/
@@ -930,20 +931,36 @@ monadic binds (the action runs, its result erases), and patterns. -/
 def ghostForms : Id Nat := do
   ghost y := 5
   ghost mut x := 1
-  x := x.out + y.out
+  x := x + y
   x : Nat := 2
   ghost z ← pure 3
   ghost mut m ← pure 4
-  m := m.out + z.out
+  m := m + z
   ghost (a, b) := (1, 2)
   ghost mut (c, d) ← pure (3, 4)
-  c := a.out + b.out + d.out
+  c := a + b + d
   pure 0
 
 /-- info: 0 -/
 #guard_msgs in
 #eval ghostForms
 
+/-! A ghost variable reassigned in a branch flows through the join point. -/
+
+def ghostBranch (b : Bool) : Id Nat
+    ensures r => r = 0 := do
+  ghost mut n : Nat := 0
+  if b then
+    n := n + 1
+  else
+    n := n + 2
+  assert n > 0
+  return 0
+
+/-- info: 0 -/
+#guard_msgs in
+#eval ghostBranch true
+
 /-! A ghost value reaching compiled code is rejected through the noncomputability of
 `Erased.out`. -/
 
@@ -954,8 +971,8 @@ error: failed to compile definition, consider marking it as 'noncomputable' beca
 def ghostLeak (xs : List Nat) : Id Nat := do
   ghost mut seen : List Nat := []
   for x in xs do
-    seen := x :: seen.out
-  return seen.out.length
+    seen := x :: seen
+  return seen.length
 
 /-! Erased data cannot decide control flow, so `ghost` takes no `|` alternative. -/
 
@@ -972,5 +989,5 @@ def ghostArrowElse (o : Option Nat) : Id Nat := do
 def ghostPatReassign : Id Nat := do
   let mut a := 1
   ghost mut g := 2
-  (a, g) := (3, Erased.mk 4)
+  (a, g) := (3, 4)
   pure a

From 4e15ccfd1fb12b5354c95d8c124ee5e8dd94b5b1 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 9 Sep 2026 11:48:59 +0000
Subject: [PATCH 03/28] refactor: one name per ghost variable

A ghost variable's carried `Erased` binding and its `.out` shadow now share the source name, alternating by shadowing exactly as reassignments of `mut` variables do. `MutVar` returns to its original shape plus a `ghost` flag, the discipline `LetOrReassign` carries the ghost information as a `Bool` on `let` and `reassign`, and both ghost effects, registration and shadow binding, live in `elabWithReassignments`. Sites that pack variables into runtime state (loop state tuples, join points, effect forwarders) wrap ghost values in `Erased.mk` and their slot types in `Erased`. The shadow closes before the carried binder does, so zeta substitution never re-introduces a bound variable.
---
 src/Lean/Elab/BuiltinDo/For.lean |  12 ++--
 src/Lean/Elab/BuiltinDo/Let.lean | 103 +++++++++++++++----------------
 src/Lean/Elab/Do/Basic.lean      |  87 +++++++++++++-------------
 src/Lean/Elab/Do/Control.lean    |  17 +++--
 4 files changed, 112 insertions(+), 107 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/For.lean b/src/Lean/Elab/BuiltinDo/For.lean
index 92213b70e2d9..427918b9a807 100644
--- a/src/Lean/Elab/BuiltinDo/For.lean
+++ b/src/Lean/Elab/BuiltinDo/For.lean
@@ -179,7 +179,7 @@ variables at their underlying type. The bindings sit in erased positions, so the
 private def ForInApp.wrapGhostShadows (g : ForInApp) (e : Term) : DoElabM Term := do
   let mut e := e
   for mv in g.ghostMutVars do
-    e ← `(let $(mv.userIdent):ident := Erased.out $(⟨mv.ident.raw⟩); $e)
+    e ← `(let $(mv.ident):ident := Erased.out $(⟨mv.ident.raw⟩); $e)
   return e
 
 /-- Abstract `e` over the loop's state tuple, so that `e` may name the loop's mutable variables. -/
@@ -291,7 +291,7 @@ private def mkForInLoopGadget (g : ForInApp)
   let info ← inferControlInfoSeq body
   let oldReturnCont ← getReturnCont
   let returnVarName ← mkFreshUserName `__r
-  let loopMutVars := mutVars.filter fun x => info.reassigns.contains x.userName
+  let loopMutVars := mutVars.filter fun x => info.reassigns.contains x.getId
   let loopMutVarNames :=
     if info.returnsEarly then
       returnVarName :: (loopMutVars.map (·.getId)).toList
@@ -309,16 +309,18 @@ private def mkForInLoopGadget (g : ForInApp)
       defs := defs.push returnVar
     for x in loopMutVars do
       let defn ← getLocalDeclFromUserName x.getId
-      Term.addTermInfo' x.userIdent defn.toExpr
+      Term.addTermInfo' x.ident defn.toExpr
+      -- A ghost variable's state slot carries the `Erased` value; the shadow rebinds at unpacking.
+      let v ← if x.ghost then mkErasedMkApp defn.toExpr else pure defn.toExpr
       -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type.
       -- If we don't do this, then we are stuck on solving constraints such as
       --   `max ?u.46 ?u.47 =?= max (max ?u.22 ?u.46) ?u.47`
       -- It's important we do this as a separate isLevelDefEq check on the decremented level because
       -- otherwise (`ensureHasType (mkSort mi.u.succ)`) we are stuck on constraints like
       --   `max (?u+1) (?v+1) =?= ?u+1`
-      let u ← getDecLevel defn.type
+      let u ← getDecLevel (← inferType v)
       discard <| isLevelDefEq u mi.u
-      defs := defs.push defn.toExpr
+      defs := defs.push v
     if info.returnsEarly && loopMutVars.isEmpty then
       defs := defs.push (mkConst ``Unit.unit)
     return defs
diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index 5cc2615b831f..8c730e427e26 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -23,48 +23,48 @@ open Lean.Parser.Term
 open Lean.Meta
 
 inductive LetOrReassign
-  | let (mutTk? : Option Syntax) (ghostUser? : Option Ident)
+  | let (mutTk? : Option Syntax) (ghost : Bool)
   | have
-  | reassign
+  | reassign (ghost : Bool)
 
 def LetOrReassign.getLetMutTk? (letOrReassign : LetOrReassign) : Option Syntax :=
   match letOrReassign with
   | .let mutTk? _ => mutTk?
   | _             => none
 
-/-- The source identifier of a `ghost` declaration. -/
-def LetOrReassign.ghostUserIdent? (letOrReassign : LetOrReassign) : Option Ident :=
+/-- Whether the binding is a `ghost` declaration or the reassignment of a ghost variable. -/
+def LetOrReassign.isGhost (letOrReassign : LetOrReassign) : Bool :=
   match letOrReassign with
-  | .let _ ghostUser? => ghostUser?
-  | _                 => none
+  | .let _ ghost    => ghost
+  | .reassign ghost => ghost
+  | .have           => false
 
 def LetOrReassign.checkMutVars (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit :=
   match letOrReassign with
-  | .reassign => do
+  | .reassign _ => do
     throwUnlessMutVarsDeclared vars
-  | _         => checkMutVarsForShadowing vars
+  | _           => checkMutVarsForShadowing vars
 
 def LetOrReassign.registerReassignAliasInfo (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit := do
-  if letOrReassign matches .reassign then
+  if letOrReassign matches .reassign _ then
     for var in vars do
       registerMutVarAlias var.getId
 
+def elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) : DoElabM Expr := do
+  declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isGhost do
+    letOrReassign.registerReassignAliasInfo vars
+    if letOrReassign.isGhost then
+      vars.foldr (init := k) withGhostShadow
+    else
+      k
+
 def elabDoLetOrReassignWith (hint : MessageData) (letOrReassign : LetOrReassign) (vars : Array Ident)
     (k : DoElabM Expr) (elabBody : (body : Term) → TermElabM Expr) : DoElabM Expr := do
   -- letOrReassign.checkMutVars vars -- Should be done by the caller!
-  let elabCont : DoElabM Expr := do
-    declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.ghostUserIdent? do
-      letOrReassign.registerReassignAliasInfo vars
-      k
-  doElabToSyntax hint elabCont fun body => elabBody body
-
-def elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) : DoElabM Expr := do
-  declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.ghostUserIdent? do
-    letOrReassign.registerReassignAliasInfo vars
-    k
+  doElabToSyntax hint (elabWithReassignments letOrReassign vars k) fun body => elabBody body
 
 private def pushTypeIntoReassignment (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl) : TermElabM (TSyntax ``letDecl) := do
-  if letOrReassign matches .reassign then
+  if letOrReassign matches .reassign false then
     match decl with
     | `(letDecl| $x:ident $[: $xType?]? := $rhs) =>
       -- We use `Term.elabTermEnsuringType` instead of `Term.ensureHasType` to turn type
@@ -147,10 +147,11 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
     trace[Elab.let.decl] "{id.getId} : {type} := {val}"
     withLetDecl id.getId (kind := kind) type val (nondep := nondep) fun x => do
       Term.addLocalVarInfo id x
-      elabWithReassignments letOrReassign vars do
+      -- The ghost `.out` shadow of `elabWithReassignments` must close before `mkLetFVars` binds
+      -- the carried variable, so it wraps only the continuation.
       match config.eq? with
       | none =>
-        let body ← dec.continueWithUnit
+        let body ← elabWithReassignments letOrReassign vars dec.continueWithUnit
         if config.zeta then
           pure <| (← body.abstractM #[x]).instantiate1 val
         else
@@ -159,7 +160,7 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
         let hTy ← mkEq x val
         withLetDecl h.getId hTy (← mkEqRefl x) (nondep := true) fun h' => do
           Term.addLocalVarInfo h h'
-          let body ← dec.continueWithUnit
+          let body ← elabWithReassignments letOrReassign vars dec.continueWithUnit
           if config.zeta then
             pure <| (← body.abstractM #[x, h']).instantiateRev #[val, ← mkEqRefl val]
           else if nondep then
@@ -174,7 +175,7 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
   | `(doIdDecl| $x:ident $[: $xType?]? ← $rhs) =>
     letOrReassign.checkMutVars #[x]
     let dec ← dec.ensureUnitAt tk
-    if letOrReassign matches .reassign then
+    if letOrReassign matches .reassign _ then
       if ((← findMutVar? x.getId).map (·.ghost)).getD false then
         let y := mkIdentFrom x (← mkFreshUserName `__y)
         return ← elabDoIdDecl y xType? rhs
@@ -182,11 +183,11 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
     -- For plain variable reassignment, we know the expected type of the reassigned variable and
     -- propagate it eagerly via type ascription if the user hasn't provided one themselves:
     let xType? ← match letOrReassign, xType? with
-      | .reassign, none =>
+      | .reassign _, none =>
         let decl ← getLocalDeclFromUserName x.getId
         some <$> Term.exprToSyntax decl.type
       | _, _ => pure xType?
-    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.ghostUserIdent? <| dec.continueWithUnit)
+    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.isGhost <| dec.continueWithUnit)
       (kind := dec.kind)
   | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
@@ -205,7 +206,7 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
         throwUnsupportedSyntax
       | .have, _ =>
         elabDoElem (← `(doElem| have $pattern:term := $x)) dec
-      | .reassign, _ =>
+      | .reassign _, _ =>
         -- otherwise? is always `none`, because there is no `doReassignElse`
         unless rest?.isNone do
           throwError "reassignment with `|` (i.e., \"else clause\") is not supported"
@@ -221,21 +222,18 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
 @[builtin_doElem_elab Lean.Parser.Term.doLet] def elabDoLet : DoElab := fun stx dec => do
   let `(doLet| let%$tk $[mut%$mutTk?]? $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
   let config ← getLetConfigAndCheckMut config mutTk?
-  elabDoLetOrReassign config (.let mutTk? none) decl tk dec
+  elabDoLetOrReassign config (.let mutTk? false) decl tk dec
 
-/-- Elaborate `ghost $[mut]? $decl`. A single variable `x : t := e` binds a carried
-`Erased t := Erased.mk e` under an inaccessible name, and the source name binds the `.out`
-shadow that proofs read. A pattern binds its variables plainly and then shadows each one with
-its ghost redeclaration. -/
+/-- Elaborate `ghost $[mut]? $decl`. A single variable `x : t := e` binds the carried
+`x : Erased t := Erased.mk e`, immediately shadowed by the `.out` shadow that the source reads.
+A pattern binds its variables plainly and then shadows each one with its ghost redeclaration. -/
 @[builtin_doElem_elab Lean.Parser.Term.doGhost] def elabDoGhost : DoElab := fun stx dec => do
   match stx with
   | `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? := $e) =>
-    let xc := mkIdentFrom x (← mkFreshUserName x.getId) (canonical := true)
     let declNew ← match t? with
-      | some t => `(letDecl| $xc:ident : Erased $t := Erased.mk $e)
-      | none   => `(letDecl| $xc:ident := Erased.mk $e)
-    let dec := { dec with k := withGhostShadow x xc.getId dec.k }
-    elabDoLetOrReassign { nondep := true } (.let mutTk? (some x)) declNew tk dec
+      | some t => `(letDecl| $x:ident : Erased $t := Erased.mk $e)
+      | none   => `(letDecl| $x:ident := Erased.mk $e)
+    elabDoLetOrReassign {} (.let mutTk? true) declNew tk dec
   | `(doGhost| ghost%$tk $[mut%$mutTk?]? $decl:letPatDecl) =>
     let declNew : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
     let vars ← getLetDeclVars declNew
@@ -244,7 +242,7 @@ its ghost redeclaration. -/
     let dec ← dec.ensureUnitAt tk
     let dec ← if redecls.isEmpty then pure dec else
       pure <| DoElemCont.mk (← mkFreshUserName `__r) (← mkPUnit) (elabDoElems1 redecls dec) dec.kind
-    elabDoLetOrReassign {} (.let none none) declNew tk dec
+    elabDoLetOrReassign {} (.let none false) declNew tk dec
   | _ => throwUnsupportedSyntax
 
 /-- Elaborate `ghost $[mut]? x ← act`: bind the action's result plainly to a fresh variable and
@@ -290,26 +288,25 @@ behaves like `_ ← act`. -/
   match stx with
   | `(doReassign| $x:ident $[: $xType?]? :=%$tk $rhs) =>
     -- A ghost variable's reassignment rebinds the carried variable with the wrapped value, so
-    -- `x := e` stores `Erased.mk e` and an ascription moves inside: `x : t := e` stores
-    -- `Erased.mk (e : t)`. The source name then rebinds the fresh `.out` shadow.
-    if let some mv := (← findMutVar? x.getId).filter (·.ghost) then
-      let xc := mkIdentFrom x mv.getId
+    -- `x := e` stores `Erased.mk e`, at the declared type pinned from the current shadow. The
+    -- source name then rebinds the fresh `.out` shadow.
+    if ((← findMutVar? x.getId).map (·.ghost)).getD false then
+      let t ← Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
       let rhs ← match xType? with
-        | some t => `(Erased.mk ($rhs : $t))
-        | none   => `(Erased.mk $rhs)
-      let decl : TSyntax ``letIdDecl ← `(letIdDecl| $xc:ident := $rhs)
+        | some tAsc => `(Erased.mk ($rhs : $tAsc))
+        | none      => `(Erased.mk ($rhs : $t))
+      let decl : TSyntax ``letIdDecl ← `(letIdDecl| $x:ident : Erased $t := $rhs)
       let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-      let dec := { dec with k := withGhostShadow mv.userIdent mv.getId dec.k }
-      return ← elabDoLetOrReassign {} .reassign decl tk dec
+      return ← elabDoLetOrReassign {} (.reassign true) decl tk dec
     let decl : TSyntax ``letIdDecl ← `(letIdDecl| $x:ident $[: $xType?]? := $rhs)
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    elabDoLetOrReassign {} .reassign decl tk dec
+    elabDoLetOrReassign {} (.reassign false) decl tk dec
   | `(doReassign| $decl:letPatDecl) =>
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
     for var in (← getLetDeclVars decl) do
       if ((← findMutVar? var.getId).map (·.ghost)).getD false then
         throwErrorAt var "a ghost variable takes a plain reassignment, as in `{var.getId} := e`"
-    elabDoLetOrReassign {} .reassign decl decl dec
+    elabDoLetOrReassign {} (.reassign false) decl decl dec
   | _ => throwUnsupportedSyntax
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetElse] def elabDoLetElse : DoElab := fun stx dec => do
@@ -317,7 +314,7 @@ behaves like `_ ← act`. -/
     | throwUnsupportedSyntax
   let config ← getLetConfigAndCheckMut cfg mutTk?
   checkLetConfigInDo config
-  let letOrReassign := LetOrReassign.let mutTk? none
+  let letOrReassign := LetOrReassign.let mutTk? false
   let vars ← getPatternVarsEx pattern
   letOrReassign.checkMutVars vars
   let mut body ← body?.getDM `(doSeqIndent|pure PUnit.unit)
@@ -336,12 +333,12 @@ behaves like `_ ← act`. -/
   checkLetConfigInDo config
   if config.nondep || config.usedOnly || config.zeta || config.eq?.isSome then
     throwErrorAt cfg "configuration options are not supported with `←`"
-  elabDoArrow (.let mutTk? none) decl tk dec
+  elabDoArrow (.let mutTk? false) decl tk dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do
   match stx with
   | `(doReassignArrow| $decl:doIdDecl) =>
-    elabDoArrow .reassign decl decl dec
+    elabDoArrow (.reassign false) decl decl dec
   | `(doReassignArrow| $decl:doPatDecl) =>
-    elabDoArrow .reassign decl decl dec
+    elabDoArrow (.reassign false) decl decl dec
   | _ => throwUnsupportedSyntax
diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index b1cfdc0456a0..8571ac927f00 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -100,29 +100,24 @@ def CodeLiveness.lub (a b : CodeLiveness) : CodeLiveness :=
 
 /-- A mutable variable declared by `let mut` in a `do` block. -/
 structure MutVar where
-  /-- The binder identifier of the carried binding. For a ghost variable this is an inaccessible
-  name; the source name binds the `.out` shadow instead. -/
+  /-- The identifier of the `let mut` or `ghost mut` declaration. -/
   ident : Ident
-  /-- The source identifier of the variable. Equals `ident` except for ghost variables. -/
-  userIdent : Ident
   /-- The `FVarId` of the initial binding produced by the declaration. -/
   baseId : FVarId
-  /-- Whether the variable comes from `ghost mut`, so reassignments wrap in `Erased.mk`. -/
+  /-- Whether the variable comes from `ghost mut`. Its bindings alternate under one name: a
+  carried `Erased` binding, shadowed by the `.out` shadow that the source reads. -/
   ghost : Bool := false
   deriving Inhabited
 
-/-- The raw `Name` of a `mut` variable's carried binding, as found in the local context. -/
+/-- The raw `Name` of a `mut` variable, as found in the local context. -/
 def MutVar.getId (mutVar : MutVar) : Name := mutVar.ident.getId
 
-/-- The source name of a `mut` variable. -/
-def MutVar.userName (mutVar : MutVar) : Name := mutVar.userIdent.getId
-
 /--
 Build an `FVarAliasInfo` recording that the reassignment binding `id` aliases the original
 `let mut` binding represented by `mutVar`.
 -/
 def MutVar.mkAliasInfo (mutVar : MutVar) (id : FVarId) : FVarAliasInfo :=
-  { userName := mutVar.userName, id, baseId := mutVar.baseId }
+  { userName := mutVar.getId, id, baseId := mutVar.baseId }
 
 instance : ToMessageData MutVar where
   toMessageData mutVar :=
@@ -344,35 +339,31 @@ def DoOps.default : DoOps where
   mkMonadApp α := do
     return mkApp (← read).monadInfo.m α
 
-/-- Register the given name as that of a `mut` variable. A ghost variable passes its source
-identifier as `ghostUser?`, while `x` names the carried binding. -/
-def declareMutVar (x : Ident) (ghostUser? : Option Ident) (k : DoElabM α) : DoElabM α := do
+/-- Register the given name as that of a `mut` variable. -/
+def declareMutVar (x : Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α := do
   let fvar ← getFVarFromUserName x.getId
-  let mutVar : MutVar :=
-    { ident := x, userIdent := ghostUser?.getD x, baseId := fvar.fvarId!, ghost := ghostUser?.isSome }
+  let mutVar : MutVar := { ident := x, baseId := fvar.fvarId!, ghost }
   withReader (fun ctx => { ctx with
     mutVars := ctx.mutVars.push mutVar,
-    mutVarDefs := ctx.mutVarDefs.insert x.getId mutVar |>.insert mutVar.userName mutVar,
+    mutVarDefs := ctx.mutVarDefs.insert x.getId mutVar,
   }) k
 
 /-- Register the given names as that of `mut` variables. -/
-def declareMutVars (xs : Array Ident) (ghostUser? : Option Ident) (k : DoElabM α) : DoElabM α := do
+def declareMutVars (xs : Array Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α := do
   let fvars ← xs.mapM (getFVarFromUserName ·.getId)
-  let newMutVars : Array MutVar := xs.zipWith (fun x fvar =>
-    { ident := x, userIdent := ghostUser?.getD x, baseId := fvar.fvarId!, ghost := ghostUser?.isSome }) fvars
+  let newMutVars : Array MutVar := xs.zipWith (fun x fvar => { ident := x, baseId := fvar.fvarId!, ghost }) fvars
   withReader (fun ctx => { ctx with
     mutVars := ctx.mutVars ++ newMutVars,
-    mutVarDefs := newMutVars.foldl (init := ctx.mutVarDefs) fun defs mutVar =>
-      defs.insert mutVar.getId mutVar |>.insert mutVar.userName mutVar,
+    mutVarDefs := ctx.mutVarDefs.insertMany (newMutVars.map fun mutVar => (mutVar.getId, mutVar)),
   }) k
 
 /-- Register the given name as that of a `mut` variable if the syntax token `mut` is present. -/
-def declareMutVar? (mutTk? : Option Syntax) (x : Ident) (ghostUser? : Option Ident) (k : DoElabM α) : DoElabM α :=
-  if mutTk?.isSome then declareMutVar x ghostUser? k else k
+def declareMutVar? (mutTk? : Option Syntax) (x : Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α :=
+  if mutTk?.isSome then declareMutVar x ghost k else k
 
 /-- Register the given names as that of `mut` variables if the syntax token `mut` is present. -/
-def declareMutVars? (mutTk? : Option Syntax) (xs : Array Ident) (ghostUser? : Option Ident) (k : DoElabM α) : DoElabM α :=
-  if mutTk?.isSome then declareMutVars xs ghostUser? k else k
+def declareMutVars? (mutTk? : Option Syntax) (xs : Array Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α :=
+  if mutTk?.isSome then declareMutVars xs ghost k else k
 
 /-- Look up a declared `mut` variable by its raw `Name`. -/
 def findMutVar? (n : Name) : DoElabM (Option MutVar) := do
@@ -484,10 +475,7 @@ mut var definition of `y`.
 def withLCtxKeepingMutVarDefs (oldLCtx : LocalContext) (oldCtx : Context) (resultName : Name) (k : DoElabM α) : DoElabM α := do
   let oldMutVars := oldCtx.mutVars
   let oldMutVarDefs := oldCtx.mutVarDefs
-  -- tunneledDefs is used as a set, so the value doesn't matter. Only carried bindings tunnel;
-  -- ghost `.out` shadows are zeta-substituted at their own scope.
-  let tunneledDefs := oldMutVars.foldl (init := ({} : Std.HashMap Name MutVar))
-    (fun defs mv => defs.insert mv.getId mv) |>.insert resultName default
+  let tunneledDefs := oldMutVarDefs.insert resultName default  -- tunneledDefs is used as a set, so the value doesn't matter
   let newCtx ← addReachingDefsAsNonDep oldLCtx (← getLCtx) tunneledDefs
   withLCtx' newCtx <| withReader (fun ctx => { ctx with
     mutVars := oldMutVars,
@@ -618,22 +606,32 @@ def registerMutVarAlias (x : Name) : DoElabM Unit := do
     if id != baseMutVar.baseId then
       pushInfoLeaf <| .ofFVarAliasInfo (baseMutVar.mkAliasInfo id)
 
-/-- Bind `userIdent` to `carried.out` at the underlying type while `k` runs, and zeta-substitute
-the binding away, so the source name reaches proofs and never compiled code. -/
-def withGhostShadow (userIdent : Ident) (carriedName : Name) (k : DoElabM Expr) : DoElabM Expr := do
-  let carried ← getLocalDeclFromUserName carriedName
+/-- Bind `x` to `carried.out` at the underlying type while `k` runs, and zeta-substitute the
+binding away, so the source name reaches proofs and never compiled code. The newest binding of
+`x` must be the carried `Erased` binding. -/
+def withGhostShadow (x : Ident) (k : DoElabM Expr) : DoElabM Expr := do
+  let carried ← getLocalDeclFromUserName x.getId
   let ty ← instantiateMVars carried.type
   let .app (.const ``Erased [u]) t := ty
-    | throwError "the carried binding of ghost variable `{userIdent.getId}` has type{indentExpr ty}\ninstead of an `Erased` type"
+    | throwError "the carried binding of ghost variable `{x.getId}` has type{indentExpr ty}\ninstead of an `Erased` type"
   let outVal := mkApp2 (mkConst ``Erased.out [u]) t carried.toExpr
-  withLetDecl userIdent.getId t outVal (nondep := true) fun xv => do
-    Term.addLocalVarInfo userIdent xv
+  withLetDecl x.getId t outVal (nondep := true) fun xv => do
+    Term.addLocalVarInfo x xv
     let body ← k
     return (← body.abstractM #[xv]).instantiate1 outVal
 
 /-- Bind the `.out` shadow of each ghost variable among `mutVars` around `k`. -/
 def withGhostShadows (mutVars : Array MutVar) (k : DoElabM Expr) : DoElabM Expr :=
-  (mutVars.filter (·.ghost)).foldr (init := k) fun mv k => withGhostShadow mv.userIdent mv.getId k
+  (mutVars.filter (·.ghost)).foldr (init := k) fun mv k => withGhostShadow mv.ident k
+
+/-- `Erased t` for the type `t` of runtime-erased data. -/
+def mkErasedApp (t : Expr) : MetaM Expr :=
+  return mkApp (mkConst ``Erased [← getLevel t]) t
+
+/-- `Erased.mk e`, which erases `e` in compiled code. -/
+def mkErasedMkApp (e : Expr) : MetaM Expr := do
+  let t ← inferType e
+  return mkApp2 (mkConst ``Erased.mk [← getLevel t]) t e
 
 /--
 Given a list of mut vars `vars` and an FVar `tupleVar` binding a tuple, bind the mut vars to the
@@ -717,13 +715,15 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     return ← caller nondupDec
   let γ := (← read).doBlockResultType
   let mγ ← mkMonadApp γ
-  let mutVars := (← read).mutVars |>.filter (callerInfo.reassigns.contains ·.userName)
+  let mutVars := (← read).mutVars |>.filter (callerInfo.reassigns.contains ·.getId)
   let mutVarNames := mutVars.map (·.getId)
   let joinName ← mkFreshUserName `__do_jp
   -- σ is the tuple type of the mut vars, or mγ if jumpCount = 0. Hence it is either level mi.u or mi.v.
   -- let σ ← mkFreshTypeMVar (userName := `σ)
   let mutDecls ← mutVarNames.mapM (getLocalDeclFromUserName ·)
-  let mutTypes := mutDecls.map (·.type)
+  -- A ghost variable's join parameter carries the `Erased` value; the shadow rebinds below.
+  let mutTypes ← (mutVars.zip mutDecls).mapM fun (mv, d) =>
+    if mv.ghost then mkErasedApp d.type else pure d.type
   let joinTy ← mkArrow nondupDec.resultType (← mkArrowN mutTypes mγ)
   let joinRhsMVar ← mkFreshExprSyntheticOpaqueMVar joinTy
   withLetDecl joinName joinTy joinRhsMVar (kind := .implDetail) (nondep := true) fun jp => do
@@ -733,8 +733,9 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     let mut e := mkApp jp' result
     for x in mutVars do
       let newX ← getFVarFromUserName x.getId
-      Term.addTermInfo' x.userIdent newX
-      e := mkApp e (← getFVarFromUserName x.getId)
+      Term.addTermInfo' x.ident newX
+      let arg ← if x.ghost then mkErasedMkApp newX else pure newX
+      e := mkApp e arg
     return e
 
   let elabBody :=
@@ -745,8 +746,8 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
 
   let joinRhs ← joinRhsMVar.mvarId!.withContext do
     withLocalDeclD nondupDec.resultName nondupDec.resultType fun r => do
-    withLocalDeclsDND (mutDecls.map fun (d : LocalDecl) => (d.userName, d.type)) fun muts => do
-    for (x, newX) in mutVars.zip muts do Term.addTermInfo' x.userIdent newX
+    withLocalDeclsDND ((mutDecls.zip mutTypes).map fun (d, t) => (d.userName, t)) fun muts => do
+    for (x, newX) in mutVars.zip muts do Term.addTermInfo' x.ident newX
     let e ← withGhostShadows mutVars (nondupDec.withDeadCodeFromInfo callerInfo).k
     mkLambdaFVars (#[r] ++ muts) e
   unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do
diff --git a/src/Lean/Elab/Do/Control.lean b/src/Lean/Elab/Do/Control.lean
index 1a5fda615fa1..0daff25cc68b 100644
--- a/src/Lean/Elab/Do/Control.lean
+++ b/src/Lean/Elab/Do/Control.lean
@@ -46,8 +46,8 @@ def ControlStack.stateT (baseMonadInfo : MonadInfo) (muts : Array MutVar) (σ :
     -- See also `StateT.monadControl.liftWith`.
     let mutExprs ← muts.mapM fun x => do
       let defn ← getLocalDeclFromUserName x.getId
-      Term.addTermInfo' x.userIdent defn.toExpr
-      pure defn.toExpr
+      Term.addTermInfo' x.ident defn.toExpr
+      if x.ghost then mkErasedMkApp defn.toExpr else pure defn.toExpr
     let (tuple, tupleTy) ← mkProdMkN mutExprs baseMonadInfo.u
     unless ← isDefEq tupleTy σ do -- just for sanity; maybe delete in the future
       throwError "State tuple type mismatch: expected {σ}, got {tupleTy}. This is a bug in the `do` elaborator."
@@ -64,7 +64,11 @@ def ControlStack.stateT (baseMonadInfo : MonadInfo) (muts : Array MutVar) (σ :
     base.restoreCont { resultName, resultType, k }
 where
   mutVarNames := muts.map (·.getId)
-  getσ := do mkProdN (← mutVarNames.mapM (LocalDecl.type <$> getLocalDeclFromUserName ·)) baseMonadInfo.u
+  getσ := do
+    let tys ← muts.mapM fun mv => do
+      let t := (← getLocalDeclFromUserName mv.getId).type
+      if mv.ghost then mkErasedApp t else pure t
+    mkProdN tys baseMonadInfo.u
   stM α := return mkApp2 (mkConst ``Prod [baseMonadInfo.u, baseMonadInfo.u]) α (← getσ) -- NB: muts `σ` might have been refined by dependent pattern matches
 
 def ControlStack.optionT (baseMonadInfo : MonadInfo) (optionTWrapper casesOnWrapper : Name)
@@ -208,10 +212,11 @@ structure EffectForwarder where
 /-- Build the lifter plan for a body whose effects are summarised by `info`. -/
 def EffectForwarder.ofCont (info : ControlInfo) (dec : DoElemCont) : DoElabM EffectForwarder := do
   let mi := (← read).monadInfo
-  let reassignedMutVars := (← read).mutVars |>.filter (info.reassigns.contains ·.userName)
-  let reassignedMutVarNames := reassignedMutVars.map (·.getId)
+  let reassignedMutVars := (← read).mutVars |>.filter (info.reassigns.contains ·.getId)
   let ρ := (← getReturnCont).resultType
-  let σ ← mkProdN (← reassignedMutVarNames.mapM (LocalDecl.type <$> getLocalDeclFromUserName ·)) mi.u
+  let σ ← mkProdN (← reassignedMutVars.mapM fun mv => do
+    let t := (← getLocalDeclFromUserName mv.getId).type
+    if mv.ghost then mkErasedApp t else pure t) mi.u
 
   let needEarlyReturn := if info.returnsEarly then some ρ else none
   let needBreak := info.breaks && (← getBreakCont).isSome

From 918a1ce13e2edfb8c5a18e818b41b42934b71eed Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 9 Sep 2026 12:41:34 +0000
Subject: [PATCH 04/28] refactor: address review comments

Concentrate all ghost handling in `elabDoLetOrReassign`: it upgrades a reassignment to a ghost reassignment by looking up the variable, rewrites ghost declarations and reassignments to bind the wrapped value, and expands ghost patterns; `elabDoGhost` and `elabDoReassign` reduce to funnels. A ghost pattern `ghost (a, b) := e` now never computes `e`: it binds `e` whole as one ghost variable and each pattern variable by matching that variable in erased positions, matching the single-variable form. Rename the shadow helpers to `withErasedProj`/`wrapErasedProjs`, match the carried type with `let_expr`, make the `Erased` imports `meta`, drop the trailing space in the `notFollowedBy` ghost entry, and remove the `ghost` field default.
---
 src/Lean/Elab/BuiltinDo/For.lean | 14 ++---
 src/Lean/Elab/BuiltinDo/Let.lean | 87 +++++++++++++++++++-------------
 src/Lean/Elab/Do/Basic.lean      | 28 +++++-----
 src/Lean/Parser/Do.lean          |  2 +-
 4 files changed, 72 insertions(+), 59 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/For.lean b/src/Lean/Elab/BuiltinDo/For.lean
index 427918b9a807..2174e9531c3a 100644
--- a/src/Lean/Elab/BuiltinDo/For.lean
+++ b/src/Lean/Elab/BuiltinDo/For.lean
@@ -6,7 +6,7 @@ Authors: Sebastian Graf
 module
 
 prelude
-import Init.Data.Erased  -- referenced by the ghost shadow quotations
+meta import Init.Data.Erased
 public import Lean.Elab.BuiltinDo.Basic
 meta import Lean.Parser.Do
 meta import Std.WP.Gadget.ForIn
@@ -171,12 +171,12 @@ structure ForInApp where
   /-- The pattern naming the loop's mutable variables in the state tuple. -/
   statePat : Term
   /-- The ghost variables among the loop's mutable variables; annotations bind their `.out`
-  shadows over the state tuple. -/
+  projections over the state tuple. -/
   ghostMutVars : Array MutVar := #[]
 
-/-- Bind the `.out` shadow of each ghost variable over `e`, so that an annotation names ghost
+/-- Bind the `.out` projection of each ghost variable over `e`, so that an annotation names ghost
 variables at their underlying type. The bindings sit in erased positions, so they compile. -/
-private def ForInApp.wrapGhostShadows (g : ForInApp) (e : Term) : DoElabM Term := do
+private def ForInApp.wrapErasedProjs (g : ForInApp) (e : Term) : DoElabM Term := do
   let mut e := e
   for mv in g.ghostMutVars do
     e ← `(let $(mv.ident):ident := Erased.out $(⟨mv.ident.raw⟩); $e)
@@ -184,7 +184,7 @@ private def ForInApp.wrapGhostShadows (g : ForInApp) (e : Term) : DoElabM Term :
 
 /-- Abstract `e` over the loop's state tuple, so that `e` may name the loop's mutable variables. -/
 private def ForInApp.mkStateFun (g : ForInApp) (e : Term) : DoElabM Term := do
-  `(fun $(g.statePat) => $(← g.wrapGhostShadows e))
+  `(fun $(g.statePat) => $(← g.wrapErasedProjs e))
 
 /-- Elaborate the gadget application that replaces the loop. The gadgets live downstream of this
 module, so `gadget` is an unresolved name that resolves in the user's context. -/
@@ -254,7 +254,7 @@ private def mkForInLoopGadget (g : ForInApp)
     -- unfolded type, and a specification's instance arguments are synthesized before the check that
     -- would unfold it.
     return ((invClause : Syntax), ← `($(mkIdent ``Std.WP.WhileInvariant.mk)
-      fun $exitVar:ident $(g.statePat) => $(← g.wrapGhostShadows invBody)))
+      fun $exitVar:ident $(g.statePat) => $(← g.wrapErasedProjs invBody)))
   let varArg? ← dec?.mapM fun decClause => do
     let (binders, body) ← match decClause with
       | `(doLoopDecreasing| decreasing $binders* => $body) => pure (binders, body)
@@ -310,7 +310,7 @@ private def mkForInLoopGadget (g : ForInApp)
     for x in loopMutVars do
       let defn ← getLocalDeclFromUserName x.getId
       Term.addTermInfo' x.ident defn.toExpr
-      -- A ghost variable's state slot carries the `Erased` value; the shadow rebinds at unpacking.
+      -- A ghost variable's state slot carries the `Erased` value; its projection rebinds at unpacking.
       let v ← if x.ghost then mkErasedMkApp defn.toExpr else pure defn.toExpr
       -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type.
       -- If we don't do this, then we are stuck on solving constraints such as
diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index 8c730e427e26..ac2225b99198 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -6,7 +6,7 @@ Authors: Sebastian Graf
 module
 
 prelude
-import Init.Data.Erased  -- referenced by the `ghost` quotations
+meta import Init.Data.Erased
 public import Lean.Elab.Do.Basic
 meta import Lean.Parser.Do
 import Lean.Elab.BuiltinDo.Basic
@@ -54,7 +54,7 @@ def elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (
   declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isGhost do
     letOrReassign.registerReassignAliasInfo vars
     if letOrReassign.isGhost then
-      vars.foldr (init := k) withGhostShadow
+      vars.foldr (init := k) withErasedProj
     else
       k
 
@@ -93,13 +93,47 @@ private def checkLetConfigInDo (config : Term.LetConfig) : DoElabM Unit := do
   if config.generalize then
     throwError "`+generalize` is not supported in `do` blocks"
 
+/-- Rewrite a ghost variable binding to bind the wrapped value: a declaration `x : t := e`
+becomes `x : Erased t := Erased.mk e`, and a reassignment pins `t` from the current binding of
+`x`, so reassignments cannot change the type. -/
+private def wrapGhostDecl (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl) :
+    DoElabM (TSyntax ``letDecl) := do
+  let `(letDecl| $x:ident $[: $t?]? := $e) := decl
+    | throwErrorAt decl "`ghost` takes a variable or a pattern"
+  match letOrReassign with
+  | .reassign _ =>
+    let t ← Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
+    let e ← match t? with
+      | some tAsc => `(Erased.mk ($e : $tAsc))
+      | none      => `(Erased.mk ($e : $t))
+    `(letDecl| $x:ident : Erased $t := $e)
+  | _ =>
+    match t? with
+    | some t => `(letDecl| $x:ident : Erased $t := Erased.mk $e)
+    | none   => `(letDecl| $x:ident := Erased.mk $e)
+
 partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl)
     (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
   checkLetConfigInDo config
   let vars ← getLetDeclVars decl
   letOrReassign.checkMutVars vars
   let dec ← dec.ensureUnitAt tk
+  -- A reassignment is a ghost reassignment iff its variable is ghost.
+  let letOrReassign ← do
+    if letOrReassign matches .reassign false then
+      match decl with
+      | `(letDecl| $x:ident $[: $_]? := $_) =>
+        pure (LetOrReassign.reassign (((← findMutVar? x.getId).map (·.ghost)).getD false))
+      | _ =>
+        for var in vars do
+          if ((← findMutVar? var.getId).map (·.ghost)).getD false then
+            throwErrorAt var "a ghost variable takes a plain reassignment, as in `{var.getId} := e`"
+        pure letOrReassign
+    else
+      pure letOrReassign
   -- Some decl preprocessing on the patterns and expected types:
+  let decl ← if letOrReassign.isGhost && !(decl.raw[0].isOfKind ``letPatDecl) then
+    wrapGhostDecl letOrReassign decl else pure decl
   let decl ← pushTypeIntoReassignment letOrReassign decl
   let mγ ← mkMonadApp (← read).doBlockResultType
   match decl with
@@ -107,6 +141,17 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
     let declNew ← `(letDecl| $(⟨← liftMacroM <| Term.expandLetEqnsDecl decl⟩):letIdDecl)
     return ← Term.withMacroExpansion decl declNew <| elabDoLetOrReassign config letOrReassign declNew tk dec
   | `(letDecl| $pattern:term $[: $xType?]? := $rhs) =>
+    if letOrReassign.isGhost then
+      -- `ghost (a, b) := e` never computes `e`: it binds `e` whole as one ghost variable, and
+      -- each pattern variable by matching that variable in erased positions.
+      let mutTk? := letOrReassign.getLetMutTk?
+      let tmp := mkIdentFrom pattern (← mkFreshUserName `__tmp)
+      let rhs ← match xType? with | some t => `(($rhs : $t)) | none => pure rhs
+      let mut elems : Array DoElem := #[⟨(← `(doGhost| ghost $tmp:ident := $rhs)).raw⟩]
+      for v in vars do
+        elems := elems.push
+          ⟨(← `(doGhost| ghost $[mut%$mutTk?]? $v:ident := (match $tmp:ident with | $pattern:term => $v))).raw⟩
+      return ← elabDoElems1 elems dec
     let rhs ← match xType? with | some xType => `(($rhs : $xType)) | none => pure rhs
     let contElab : DoElabM Expr := elabWithReassignments letOrReassign vars dec.continueWithUnit
     doElabToSyntax m!"let body of {pattern}" contElab fun body => do
@@ -147,8 +192,8 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
     trace[Elab.let.decl] "{id.getId} : {type} := {val}"
     withLetDecl id.getId (kind := kind) type val (nondep := nondep) fun x => do
       Term.addLocalVarInfo id x
-      -- The ghost `.out` shadow of `elabWithReassignments` must close before `mkLetFVars` binds
-      -- the carried variable, so it wraps only the continuation.
+      -- The ghost `.out` projection of `elabWithReassignments` must close before `mkLetFVars`
+      -- binds the carried variable, so it wraps only the continuation.
       match config.eq? with
       | none =>
         let body ← elabWithReassignments letOrReassign vars dec.continueWithUnit
@@ -224,30 +269,14 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   let config ← getLetConfigAndCheckMut config mutTk?
   elabDoLetOrReassign config (.let mutTk? false) decl tk dec
 
-/-- Elaborate `ghost $[mut]? $decl`. A single variable `x : t := e` binds the carried
-`x : Erased t := Erased.mk e`, immediately shadowed by the `.out` shadow that the source reads.
-A pattern binds its variables plainly and then shadows each one with its ghost redeclaration. -/
 @[builtin_doElem_elab Lean.Parser.Term.doGhost] def elabDoGhost : DoElab := fun stx dec => do
   match stx with
   | `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? := $e) =>
-    let declNew ← match t? with
-      | some t => `(letDecl| $x:ident : Erased $t := Erased.mk $e)
-      | none   => `(letDecl| $x:ident := Erased.mk $e)
-    elabDoLetOrReassign {} (.let mutTk? true) declNew tk dec
+    elabDoLetOrReassign {} (.let mutTk? true) (← `(letDecl| $x:ident $[: $t?]? := $e)) tk dec
   | `(doGhost| ghost%$tk $[mut%$mutTk?]? $decl:letPatDecl) =>
-    let declNew : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    let vars ← getLetDeclVars declNew
-    let redecls ← vars.mapM fun v =>
-      return ⟨(← `(doGhost| ghost%$tk $[mut%$mutTk?]? $v:ident := $v:ident)).raw⟩
-    let dec ← dec.ensureUnitAt tk
-    let dec ← if redecls.isEmpty then pure dec else
-      pure <| DoElemCont.mk (← mkFreshUserName `__r) (← mkPUnit) (elabDoElems1 redecls dec) dec.kind
-    elabDoLetOrReassign {} (.let none false) declNew tk dec
+    elabDoLetOrReassign {} (.let mutTk? true) ⟨mkNode ``letDecl #[decl]⟩ tk dec
   | _ => throwUnsupportedSyntax
 
-/-- Elaborate `ghost $[mut]? x ← act`: bind the action's result plainly to a fresh variable and
-funnel it through `ghost x := y`, which wraps. At runtime the result is unused, so the element
-behaves like `_ ← act`. -/
 @[builtin_doElem_elab Lean.Parser.Term.doGhostArrow] def elabDoGhostArrow : DoElab := fun stx dec => do
   match stx with
   | `(doGhostArrow| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? ← $rhs) =>
@@ -287,25 +316,11 @@ behaves like `_ ← act`. -/
   -- def doReassign := letIdDeclNoBinders <|> letPatDecl
   match stx with
   | `(doReassign| $x:ident $[: $xType?]? :=%$tk $rhs) =>
-    -- A ghost variable's reassignment rebinds the carried variable with the wrapped value, so
-    -- `x := e` stores `Erased.mk e`, at the declared type pinned from the current shadow. The
-    -- source name then rebinds the fresh `.out` shadow.
-    if ((← findMutVar? x.getId).map (·.ghost)).getD false then
-      let t ← Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
-      let rhs ← match xType? with
-        | some tAsc => `(Erased.mk ($rhs : $tAsc))
-        | none      => `(Erased.mk ($rhs : $t))
-      let decl : TSyntax ``letIdDecl ← `(letIdDecl| $x:ident : Erased $t := $rhs)
-      let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-      return ← elabDoLetOrReassign {} (.reassign true) decl tk dec
     let decl : TSyntax ``letIdDecl ← `(letIdDecl| $x:ident $[: $xType?]? := $rhs)
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
     elabDoLetOrReassign {} (.reassign false) decl tk dec
   | `(doReassign| $decl:letPatDecl) =>
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    for var in (← getLetDeclVars decl) do
-      if ((← findMutVar? var.getId).map (·.ghost)).getD false then
-        throwErrorAt var "a ghost variable takes a plain reassignment, as in `{var.getId} := e`"
     elabDoLetOrReassign {} (.reassign false) decl decl dec
   | _ => throwUnsupportedSyntax
 
diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index 8571ac927f00..cde24eb79cde 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -6,7 +6,7 @@ Authors: Sebastian Graf
 module
 
 prelude
-import Init.Data.Erased
+meta import Init.Data.Erased
 public import Lean.Elab.Do.InferControlInfo
 public import Lean.Elab.Binders
 import Lean.Meta.ProdN
@@ -104,9 +104,8 @@ structure MutVar where
   ident : Ident
   /-- The `FVarId` of the initial binding produced by the declaration. -/
   baseId : FVarId
-  /-- Whether the variable comes from `ghost mut`. Its bindings alternate under one name: a
-  carried `Erased` binding, shadowed by the `.out` shadow that the source reads. -/
-  ghost : Bool := false
+  /-- Whether the variable comes from `ghost mut`. -/
+  ghost : Bool
   deriving Inhabited
 
 /-- The raw `Name` of a `mut` variable, as found in the local context. -/
@@ -609,20 +608,19 @@ def registerMutVarAlias (x : Name) : DoElabM Unit := do
 /-- Bind `x` to `carried.out` at the underlying type while `k` runs, and zeta-substitute the
 binding away, so the source name reaches proofs and never compiled code. The newest binding of
 `x` must be the carried `Erased` binding. -/
-def withGhostShadow (x : Ident) (k : DoElabM Expr) : DoElabM Expr := do
+def withErasedProj (x : Ident) (k : DoElabM Expr) : DoElabM Expr := do
   let carried ← getLocalDeclFromUserName x.getId
-  let ty ← instantiateMVars carried.type
-  let .app (.const ``Erased [u]) t := ty
-    | throwError "the carried binding of ghost variable `{x.getId}` has type{indentExpr ty}\ninstead of an `Erased` type"
-  let outVal := mkApp2 (mkConst ``Erased.out [u]) t carried.toExpr
+  let_expr c@Erased t ← carried.type
+    | throwError "the carried binding of ghost variable `{x.getId}` has type{indentExpr carried.type}\ninstead of an `Erased` type"
+  let outVal := mkApp2 (mkConst ``Erased.out c.constLevels!) t carried.toExpr
   withLetDecl x.getId t outVal (nondep := true) fun xv => do
     Term.addLocalVarInfo x xv
     let body ← k
     return (← body.abstractM #[xv]).instantiate1 outVal
 
-/-- Bind the `.out` shadow of each ghost variable among `mutVars` around `k`. -/
-def withGhostShadows (mutVars : Array MutVar) (k : DoElabM Expr) : DoElabM Expr :=
-  (mutVars.filter (·.ghost)).foldr (init := k) fun mv k => withGhostShadow mv.ident k
+/-- Bind the `.out` projection of each ghost variable among `mutVars` around `k`. -/
+def withErasedProjs (mutVars : Array MutVar) (k : DoElabM Expr) : DoElabM Expr :=
+  (mutVars.filter (·.ghost)).foldr (init := k) fun mv k => withErasedProj mv.ident k
 
 /-- `Erased t` for the type `t` of runtime-erased data. -/
 def mkErasedApp (t : Expr) : MetaM Expr :=
@@ -639,7 +637,7 @@ fields of the tuple and call `k` in the resulting local context.
 -/
 def bindMutVarsFromTuple (vars : List Name) (tupleVar : FVarId) (k : DoElabM Expr) : DoElabM Expr := do
   let ghosts := (← read).mutVars.filter fun mv => mv.ghost && vars.contains mv.getId
-  let k := withGhostShadows ghosts k
+  let k := withErasedProjs ghosts k
   go vars tupleVar (← tupleVar.getType) #[] k
 where
   go vars tupleVar tupleTy letFVars k := do
@@ -721,7 +719,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
   -- σ is the tuple type of the mut vars, or mγ if jumpCount = 0. Hence it is either level mi.u or mi.v.
   -- let σ ← mkFreshTypeMVar (userName := `σ)
   let mutDecls ← mutVarNames.mapM (getLocalDeclFromUserName ·)
-  -- A ghost variable's join parameter carries the `Erased` value; the shadow rebinds below.
+  -- A ghost variable's join parameter carries the `Erased` value; its projection rebinds below.
   let mutTypes ← (mutVars.zip mutDecls).mapM fun (mv, d) =>
     if mv.ghost then mkErasedApp d.type else pure d.type
   let joinTy ← mkArrow nondupDec.resultType (← mkArrowN mutTypes mγ)
@@ -748,7 +746,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withLocalDeclD nondupDec.resultName nondupDec.resultType fun r => do
     withLocalDeclsDND ((mutDecls.zip mutTypes).map fun (d, t) => (d.userName, t)) fun muts => do
     for (x, newX) in mutVars.zip muts do Term.addTermInfo' x.ident newX
-    let e ← withGhostShadows mutVars (nondupDec.withDeadCodeFromInfo callerInfo).k
+    let e ← withErasedProjs mutVars (nondupDec.withDeadCodeFromInfo callerInfo).k
     mkLambdaFVars (#[r] ++ muts) e
   unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do
     joinRhsMVar.mvarId!.withContext do
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index cdd09478cf07..feb3ac8a7ed5 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -64,7 +64,7 @@ def notFollowedByRedefinedTermToken :=
   -- If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
   notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "match_expr" <|> "let" <|> "let_expr" <|> "have" <|>
       "do" <|> "dbg_trace" <|> "idbg" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try" <|>
-      nonReservedSymbol "ghost ")
+      nonReservedSymbol "ghost")
     "token at 'do' element"
 
 namespace InternalSyntax

From 9562c6d04fdcaf5600fc3f4ecf3f2a4416cac246 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 9 Sep 2026 13:06:45 +0000
Subject: [PATCH 05/28] refactor: `ghost` takes a single variable

A ghost pattern would bind its variables to `match` projections, which reduce worse in proofs than the tuple the variable holds, so `doGhost` and `doGhostArrow` parse only a single identifier.
---
 src/Lean/Elab/BuiltinDo/Let.lean       | 47 ++++++--------------------
 src/Lean/Elab/Do/InferControlInfo.lean |  2 --
 src/Lean/Parser/Do.lean                |  4 +--
 tests/elab/intrinsicVerification.lean  | 15 ++------
 4 files changed, 15 insertions(+), 53 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index ac2225b99198..f8676b4b76e4 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -132,8 +132,7 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
     else
       pure letOrReassign
   -- Some decl preprocessing on the patterns and expected types:
-  let decl ← if letOrReassign.isGhost && !(decl.raw[0].isOfKind ``letPatDecl) then
-    wrapGhostDecl letOrReassign decl else pure decl
+  let decl ← if letOrReassign.isGhost then wrapGhostDecl letOrReassign decl else pure decl
   let decl ← pushTypeIntoReassignment letOrReassign decl
   let mγ ← mkMonadApp (← read).doBlockResultType
   match decl with
@@ -141,17 +140,6 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
     let declNew ← `(letDecl| $(⟨← liftMacroM <| Term.expandLetEqnsDecl decl⟩):letIdDecl)
     return ← Term.withMacroExpansion decl declNew <| elabDoLetOrReassign config letOrReassign declNew tk dec
   | `(letDecl| $pattern:term $[: $xType?]? := $rhs) =>
-    if letOrReassign.isGhost then
-      -- `ghost (a, b) := e` never computes `e`: it binds `e` whole as one ghost variable, and
-      -- each pattern variable by matching that variable in erased positions.
-      let mutTk? := letOrReassign.getLetMutTk?
-      let tmp := mkIdentFrom pattern (← mkFreshUserName `__tmp)
-      let rhs ← match xType? with | some t => `(($rhs : $t)) | none => pure rhs
-      let mut elems : Array DoElem := #[⟨(← `(doGhost| ghost $tmp:ident := $rhs)).raw⟩]
-      for v in vars do
-        elems := elems.push
-          ⟨(← `(doGhost| ghost $[mut%$mutTk?]? $v:ident := (match $tmp:ident with | $pattern:term => $v))).raw⟩
-      return ← elabDoElems1 elems dec
     let rhs ← match xType? with | some xType => `(($rhs : $xType)) | none => pure rhs
     let contElab : DoElabM Expr := elabWithReassignments letOrReassign vars dec.continueWithUnit
     doElabToSyntax m!"let body of {pattern}" contElab fun body => do
@@ -270,31 +258,18 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   elabDoLetOrReassign config (.let mutTk? false) decl tk dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doGhost] def elabDoGhost : DoElab := fun stx dec => do
-  match stx with
-  | `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? := $e) =>
-    elabDoLetOrReassign {} (.let mutTk? true) (← `(letDecl| $x:ident $[: $t?]? := $e)) tk dec
-  | `(doGhost| ghost%$tk $[mut%$mutTk?]? $decl:letPatDecl) =>
-    elabDoLetOrReassign {} (.let mutTk? true) ⟨mkNode ``letDecl #[decl]⟩ tk dec
-  | _ => throwUnsupportedSyntax
+  let `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? := $e) := stx | throwUnsupportedSyntax
+  elabDoLetOrReassign {} (.let mutTk? true) (← `(letDecl| $x:ident $[: $t?]? := $e)) tk dec
 
 @[builtin_doElem_elab Lean.Parser.Term.doGhostArrow] def elabDoGhostArrow : DoElab := fun stx dec => do
-  match stx with
-  | `(doGhostArrow| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? ← $rhs) =>
-    checkMutVarsForShadowing #[x]
-    let dec ← dec.ensureUnitAt tk
-    let y := mkIdentFrom x (← mkFreshUserName `__y)
-    elabDoIdDecl y t? rhs
-      (elabDoElem ⟨(← `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident := $y)).raw⟩ dec)
-      (kind := dec.kind)
-  | `(doGhostArrow| ghost%$tk $[mut%$mutTk?]? $pat:term $[: $t?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
-    if otherwise?.isSome then
-      throwErrorAt tk "`ghost` takes no `|` alternative"
-    let dec ← dec.ensureUnitAt tk
-    let y := mkIdentFrom pat (← mkFreshUserName `__y)
-    elabDoIdDecl y t? rhs
-      (elabDoElem ⟨(← `(doGhost| ghost%$tk $[mut%$mutTk?]? $pat:term := $y)).raw⟩ dec)
-      (kind := dec.kind)
-  | _ => throwUnsupportedSyntax
+  let `(doGhostArrow| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? ← $rhs) := stx
+    | throwUnsupportedSyntax
+  checkMutVarsForShadowing #[x]
+  let dec ← dec.ensureUnitAt tk
+  let y := mkIdentFrom x (← mkFreshUserName `__y)
+  elabDoIdDecl y t? rhs
+    (elabDoElem ⟨(← `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident := $y)).raw⟩ dec)
+    (kind := dec.kind)
 
 @[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do
   let `(doHave| have%$tk $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
diff --git a/src/Lean/Elab/Do/InferControlInfo.lean b/src/Lean/Elab/Do/InferControlInfo.lean
index e0948ceb477f..088e1d9f63c6 100644
--- a/src/Lean/Elab/Do/InferControlInfo.lean
+++ b/src/Lean/Elab/Do/InferControlInfo.lean
@@ -162,8 +162,6 @@ partial def ofElem (stx : DoElem) : TermElabM ControlInfo := do
     ofLetOrReassignArrow false decl
   | `(doGhostArrow| ghost $[mut]? $decl:doIdDecl) =>
     ofLetOrReassignArrow false decl
-  | `(doGhostArrow| ghost $[mut]? $decl:doPatDecl) =>
-    ofLetOrReassignArrow false decl
   | `(doGhost| ghost $[mut]? $_) => return .pure
   | `(doElem| $decl:letIdDeclNoBinders) =>
     ofLetOrReassign (← getLetIdDeclVars ⟨decl⟩) none none none
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index feb3ac8a7ed5..4ac60180303c 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -112,10 +112,10 @@ def letIdDeclNoBinders := leading_parser
 
 /-- `ghost x := e` declares a verification-only variable; `mut` allows reassignment. -/
 @[builtin_doElem_parser] def doGhost := leading_parser
-  nonReservedSymbol "ghost " (includeIdent := true) >> optional "mut " >> (letIdDeclNoBinders <|> letPatDecl)
+  nonReservedSymbol "ghost " (includeIdent := true) >> optional "mut " >> letIdDeclNoBinders
 /-- `ghost x ← act` runs `act` and hides its result in a verification-only variable. -/
 @[builtin_doElem_parser] def doGhostArrow := leading_parser
-  nonReservedSymbol "ghost " (includeIdent := true) >> optional "mut " >> (doIdDecl <|> doPatDecl)
+  nonReservedSymbol "ghost " (includeIdent := true) >> optional "mut " >> doIdDecl
 
 @[builtin_doElem_parser] def doReassign      := leading_parser
   notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
diff --git a/tests/elab/intrinsicVerification.lean b/tests/elab/intrinsicVerification.lean
index 7fbd85aa0cfb..337acf2321b6 100644
--- a/tests/elab/intrinsicVerification.lean
+++ b/tests/elab/intrinsicVerification.lean
@@ -925,8 +925,8 @@ def ghostDoubleSum (xs : List Nat) : Id Nat
 #guard_msgs in
 #eval ghostDoubleSum [1, 2, 3]
 
-/-! The declaration forms: `ghost` with and without `mut`, reassignment with an ascription,
-monadic binds (the action runs, its result erases), and patterns. -/
+/-! The declaration forms: `ghost` with and without `mut`, reassignment with an ascription, and
+monadic binds (the action runs, its result erases). -/
 
 def ghostForms : Id Nat := do
   ghost y := 5
@@ -936,9 +936,6 @@ def ghostForms : Id Nat := do
   ghost z ← pure 3
   ghost mut m ← pure 4
   m := m + z
-  ghost (a, b) := (1, 2)
-  ghost mut (c, d) ← pure (3, 4)
-  c := a + b + d
   pure 0
 
 /-- info: 0 -/
@@ -974,14 +971,6 @@ def ghostLeak (xs : List Nat) : Id Nat := do
     seen := x :: seen
   return seen.length
 
-/-! Erased data cannot decide control flow, so `ghost` takes no `|` alternative. -/
-
-/-- error: `ghost` takes no `|` alternative -/
-#guard_msgs in
-def ghostArrowElse (o : Option Nat) : Id Nat := do
-  ghost some x ← pure o | return 1
-  return 2
-
 /-! A ghost variable stays out of pattern reassignments. -/
 
 /-- error: a ghost variable takes a plain reassignment, as in `g := e` -/

From 4713e24e37525b988b698db49981d6533fb73446 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 9 Sep 2026 15:45:59 +0000
Subject: [PATCH 06/28] fix: alias ghost projection bindings to the variable's
 base binding

Uses of a ghost variable resolve to its `.out` projection, so find-references and rename need the projection fvars in the alias table alongside the carried rebindings.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 9 +++++----
 src/Lean/Elab/Do/Basic.lean      | 4 ++++
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index f8676b4b76e4..26cbbc6a4822 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -93,13 +93,14 @@ private def checkLetConfigInDo (config : Term.LetConfig) : DoElabM Unit := do
   if config.generalize then
     throwError "`+generalize` is not supported in `do` blocks"
 
-/-- Rewrite a ghost variable binding to bind the wrapped value: a declaration `x : t := e`
-becomes `x : Erased t := Erased.mk e`, and a reassignment pins `t` from the current binding of
-`x`, so reassignments cannot change the type. -/
+/--
+Wrap a ghost decl `ghost x : t := e` as `let x : Erased t := Erased.mk e`, similarly for
+reassigments.
+-/
 private def wrapGhostDecl (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl) :
     DoElabM (TSyntax ``letDecl) := do
   let `(letDecl| $x:ident $[: $t?]? := $e) := decl
-    | throwErrorAt decl "`ghost` takes a variable or a pattern"
+    | throwErrorAt decl "`ghost` takes a variable"
   match letOrReassign with
   | .reassign _ =>
     let t ← Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index cde24eb79cde..068735c462e5 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -615,6 +615,10 @@ def withErasedProj (x : Ident) (k : DoElabM Expr) : DoElabM Expr := do
   let outVal := mkApp2 (mkConst ``Erased.out c.constLevels!) t carried.toExpr
   withLetDecl x.getId t outVal (nondep := true) fun xv => do
     Term.addLocalVarInfo x xv
+    -- Uses of `x` resolve to the projection, so alias it to the variable's base binding for
+    -- find-references and rename.
+    let baseId := ((← findMutVar? x.getId).map (·.baseId)).getD carried.fvarId
+    pushInfoLeaf <| .ofFVarAliasInfo { userName := x.getId, id := xv.fvarId!, baseId }
     let body ← k
     return (← body.abstractM #[xv]).instantiate1 outVal
 

From 8e4903b9f94a789268acf430d488bf320724ae6d Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 9 Sep 2026 15:54:19 +0000
Subject: [PATCH 07/28] refactor: emit ghost projection info like non-ghost
 rebindings

Tuple rebinds contribute only aliases for non-ghost variables, so the projections there do the same; reassignment-site projections already anchor at the site ident via `elabWithReassignments`, and join projections at the declaration ident like the join term infos.
---
 src/Lean/Elab/Do/Basic.lean | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index 068735c462e5..0ad3207b0883 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -608,13 +608,14 @@ def registerMutVarAlias (x : Name) : DoElabM Unit := do
 /-- Bind `x` to `carried.out` at the underlying type while `k` runs, and zeta-substitute the
 binding away, so the source name reaches proofs and never compiled code. The newest binding of
 `x` must be the carried `Erased` binding. -/
-def withErasedProj (x : Ident) (k : DoElabM Expr) : DoElabM Expr := do
+def withErasedProj (x : Ident) (k : DoElabM Expr) (info : Bool := true) : DoElabM Expr := do
   let carried ← getLocalDeclFromUserName x.getId
   let_expr c@Erased t ← carried.type
     | throwError "the carried binding of ghost variable `{x.getId}` has type{indentExpr carried.type}\ninstead of an `Erased` type"
   let outVal := mkApp2 (mkConst ``Erased.out c.constLevels!) t carried.toExpr
   withLetDecl x.getId t outVal (nondep := true) fun xv => do
-    Term.addLocalVarInfo x xv
+    if info then
+      Term.addLocalVarInfo x xv
     -- Uses of `x` resolve to the projection, so alias it to the variable's base binding for
     -- find-references and rename.
     let baseId := ((← findMutVar? x.getId).map (·.baseId)).getD carried.fvarId
@@ -623,8 +624,8 @@ def withErasedProj (x : Ident) (k : DoElabM Expr) : DoElabM Expr := do
     return (← body.abstractM #[xv]).instantiate1 outVal
 
 /-- Bind the `.out` projection of each ghost variable among `mutVars` around `k`. -/
-def withErasedProjs (mutVars : Array MutVar) (k : DoElabM Expr) : DoElabM Expr :=
-  (mutVars.filter (·.ghost)).foldr (init := k) fun mv k => withErasedProj mv.ident k
+def withErasedProjs (mutVars : Array MutVar) (k : DoElabM Expr) (info : Bool := true) : DoElabM Expr :=
+  (mutVars.filter (·.ghost)).foldr (init := k) fun mv k => withErasedProj mv.ident k info
 
 /-- `Erased t` for the type `t` of runtime-erased data. -/
 def mkErasedApp (t : Expr) : MetaM Expr :=
@@ -641,7 +642,8 @@ fields of the tuple and call `k` in the resulting local context.
 -/
 def bindMutVarsFromTuple (vars : List Name) (tupleVar : FVarId) (k : DoElabM Expr) : DoElabM Expr := do
   let ghosts := (← read).mutVars.filter fun mv => mv.ghost && vars.contains mv.getId
-  let k := withErasedProjs ghosts k
+  -- Like the rebindings themselves, the projections contribute only aliases here.
+  let k := withErasedProjs ghosts k (info := false)
   go vars tupleVar (← tupleVar.getType) #[] k
 where
   go vars tupleVar tupleTy letFVars k := do

From 0214e063f222d3db919ebe2d02dab0a5d08bf001 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 9 Sep 2026 15:54:19 +0000
Subject: [PATCH 08/28] refactor: derive a reassignment's ghostness from its
 `MutVar`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The `ghost` bit on `LetOrReassign.reassign` only cached what `findMutVar?` already knows, so it is gone; `.reassign` is nullary again and `elabWithReassignments` looks the variables up. `wrapGhostDecl` overlapped `pushTypeIntoReassignment` inconsistently: it applied the user's ascription inside the wrap where the latter checks the ascription against the declared type and then pins that type. The wrap now runs after `pushTypeIntoReassignment` as the mechanical `t ↦ Erased t`, `e ↦ Erased.mk e`, so ghost reassignments get the same ascription semantics as plain ones.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 74 ++++++++++++++++----------------
 1 file changed, 36 insertions(+), 38 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index 26cbbc6a4822..bf4720a74104 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -25,38 +25,39 @@ open Lean.Meta
 inductive LetOrReassign
   | let (mutTk? : Option Syntax) (ghost : Bool)
   | have
-  | reassign (ghost : Bool)
+  | reassign
 
 def LetOrReassign.getLetMutTk? (letOrReassign : LetOrReassign) : Option Syntax :=
   match letOrReassign with
   | .let mutTk? _ => mutTk?
   | _             => none
 
-/-- Whether the binding is a `ghost` declaration or the reassignment of a ghost variable. -/
-def LetOrReassign.isGhost (letOrReassign : LetOrReassign) : Bool :=
+/-- Whether the binding is a `ghost` declaration. A reassignment's ghostness follows from its
+variable's `MutVar` record instead. -/
+def LetOrReassign.isGhostDecl (letOrReassign : LetOrReassign) : Bool :=
   match letOrReassign with
-  | .let _ ghost    => ghost
-  | .reassign ghost => ghost
-  | .have           => false
+  | .let _ ghost => ghost
+  | _            => false
 
 def LetOrReassign.checkMutVars (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit :=
   match letOrReassign with
-  | .reassign _ => do
+  | .reassign => do
     throwUnlessMutVarsDeclared vars
-  | _           => checkMutVarsForShadowing vars
+  | _         => checkMutVarsForShadowing vars
 
 def LetOrReassign.registerReassignAliasInfo (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit := do
-  if letOrReassign matches .reassign _ then
+  if letOrReassign matches .reassign then
     for var in vars do
       registerMutVarAlias var.getId
 
 def elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) : DoElabM Expr := do
-  declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isGhost do
+  declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isGhostDecl do
     letOrReassign.registerReassignAliasInfo vars
-    if letOrReassign.isGhost then
-      vars.foldr (init := k) withErasedProj
-    else
-      k
+    let ghostVars ← match letOrReassign with
+      | .let _ true => pure vars
+      | .reassign   => vars.filterM fun v => return ((← findMutVar? v.getId).map (·.ghost)).getD false
+      | _           => pure #[]
+    ghostVars.foldr (init := k) withErasedProj
 
 def elabDoLetOrReassignWith (hint : MessageData) (letOrReassign : LetOrReassign) (vars : Array Ident)
     (k : DoElabM Expr) (elabBody : (body : Term) → TermElabM Expr) : DoElabM Expr := do
@@ -64,7 +65,7 @@ def elabDoLetOrReassignWith (hint : MessageData) (letOrReassign : LetOrReassign)
   doElabToSyntax hint (elabWithReassignments letOrReassign vars k) fun body => elabBody body
 
 private def pushTypeIntoReassignment (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl) : TermElabM (TSyntax ``letDecl) := do
-  if letOrReassign matches .reassign false then
+  if letOrReassign matches .reassign then
     match decl with
     | `(letDecl| $x:ident $[: $xType?]? := $rhs) =>
       -- We use `Term.elabTermEnsuringType` instead of `Term.ensureHasType` to turn type
@@ -102,7 +103,7 @@ private def wrapGhostDecl (letOrReassign : LetOrReassign) (decl : TSyntax ``letD
   let `(letDecl| $x:ident $[: $t?]? := $e) := decl
     | throwErrorAt decl "`ghost` takes a variable"
   match letOrReassign with
-  | .reassign _ =>
+  | .reassign =>
     let t ← Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
     let e ← match t? with
       | some tAsc => `(Erased.mk ($e : $tAsc))
@@ -119,22 +120,19 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
   let vars ← getLetDeclVars decl
   letOrReassign.checkMutVars vars
   let dec ← dec.ensureUnitAt tk
-  -- A reassignment is a ghost reassignment iff its variable is ghost.
-  let letOrReassign ← do
-    if letOrReassign matches .reassign false then
-      match decl with
-      | `(letDecl| $x:ident $[: $_]? := $_) =>
-        pure (LetOrReassign.reassign (((← findMutVar? x.getId).map (·.ghost)).getD false))
-      | _ =>
-        for var in vars do
-          if ((← findMutVar? var.getId).map (·.ghost)).getD false then
-            throwErrorAt var "a ghost variable takes a plain reassignment, as in `{var.getId} := e`"
-        pure letOrReassign
+  -- Reassigning a ghost variable wraps its value, which only the single-variable form can do.
+  let isGhost ← do
+    if letOrReassign matches .reassign then
+      let some v ← vars.findM? fun v => return ((← findMutVar? v.getId).map (·.ghost)).getD false
+        | pure false
+      unless decl matches `(letDecl| $_:ident $[: $_]? := $_) do
+        throwErrorAt v "a ghost variable takes a plain reassignment, as in `{v.getId} := e`"
+      pure true
     else
-      pure letOrReassign
+      pure letOrReassign.isGhostDecl
   -- Some decl preprocessing on the patterns and expected types:
-  let decl ← if letOrReassign.isGhost then wrapGhostDecl letOrReassign decl else pure decl
-  let decl ← pushTypeIntoReassignment letOrReassign decl
+  let decl ← if isGhost then wrapGhostDecl letOrReassign decl
+             else pushTypeIntoReassignment letOrReassign decl
   let mγ ← mkMonadApp (← read).doBlockResultType
   match decl with
   | `(letDecl| $decl:letEqnsDecl) =>
@@ -209,7 +207,7 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
   | `(doIdDecl| $x:ident $[: $xType?]? ← $rhs) =>
     letOrReassign.checkMutVars #[x]
     let dec ← dec.ensureUnitAt tk
-    if letOrReassign matches .reassign _ then
+    if letOrReassign matches .reassign then
       if ((← findMutVar? x.getId).map (·.ghost)).getD false then
         let y := mkIdentFrom x (← mkFreshUserName `__y)
         return ← elabDoIdDecl y xType? rhs
@@ -217,11 +215,11 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
     -- For plain variable reassignment, we know the expected type of the reassigned variable and
     -- propagate it eagerly via type ascription if the user hasn't provided one themselves:
     let xType? ← match letOrReassign, xType? with
-      | .reassign _, none =>
+      | .reassign, none =>
         let decl ← getLocalDeclFromUserName x.getId
         some <$> Term.exprToSyntax decl.type
       | _, _ => pure xType?
-    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.isGhost <| dec.continueWithUnit)
+    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.isGhostDecl <| dec.continueWithUnit)
       (kind := dec.kind)
   | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
@@ -240,7 +238,7 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
         throwUnsupportedSyntax
       | .have, _ =>
         elabDoElem (← `(doElem| have $pattern:term := $x)) dec
-      | .reassign _, _ =>
+      | .reassign, _ =>
         -- otherwise? is always `none`, because there is no `doReassignElse`
         unless rest?.isNone do
           throwError "reassignment with `|` (i.e., \"else clause\") is not supported"
@@ -294,10 +292,10 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   | `(doReassign| $x:ident $[: $xType?]? :=%$tk $rhs) =>
     let decl : TSyntax ``letIdDecl ← `(letIdDecl| $x:ident $[: $xType?]? := $rhs)
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    elabDoLetOrReassign {} (.reassign false) decl tk dec
+    elabDoLetOrReassign {} .reassign decl tk dec
   | `(doReassign| $decl:letPatDecl) =>
     let decl : TSyntax ``letDecl := ⟨mkNode ``letDecl #[decl]⟩
-    elabDoLetOrReassign {} (.reassign false) decl decl dec
+    elabDoLetOrReassign {} .reassign decl decl dec
   | _ => throwUnsupportedSyntax
 
 @[builtin_doElem_elab Lean.Parser.Term.doLetElse] def elabDoLetElse : DoElab := fun stx dec => do
@@ -329,7 +327,7 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
 @[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do
   match stx with
   | `(doReassignArrow| $decl:doIdDecl) =>
-    elabDoArrow (.reassign false) decl decl dec
+    elabDoArrow .reassign decl decl dec
   | `(doReassignArrow| $decl:doPatDecl) =>
-    elabDoArrow (.reassign false) decl decl dec
+    elabDoArrow .reassign decl decl dec
   | _ => throwUnsupportedSyntax

From 0cd18c09db903275357a2ce817198076395c1457 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 9 Sep 2026 16:08:31 +0000
Subject: [PATCH 09/28] refactor: one ghostness predicate for bindings

A reassignment either has one variable, whose `MutVar` answers the question, or several, none of which is ghost: `checkMutVars` enforces that a ghost variable takes the single-variable form, `isGhost` reads the first variable, and `elabWithReassignments` binds the projections for all variables or none.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 34 ++++++++++++++++++--------------
 1 file changed, 19 insertions(+), 15 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index bf4720a74104..2c26968f3515 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -39,10 +39,24 @@ def LetOrReassign.isGhostDecl (letOrReassign : LetOrReassign) : Bool :=
   | .let _ ghost => ghost
   | _            => false
 
+def isGhost (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Bool := do
+  match letOrReassign with
+  | .let _ ghost => return ghost
+  | .reassign    =>
+    let some v := vars[0]? | return false
+    let some mv ← findMutVar? v.getId | return false
+    return mv.ghost
+  | _            => return false
+
 def LetOrReassign.checkMutVars (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit :=
   match letOrReassign with
   | .reassign => do
     throwUnlessMutVarsDeclared vars
+    -- Reassigning a ghost variable wraps its value, which only the single-variable form can do.
+    unless vars.size == 1 do
+      for v in vars do
+        if ((← findMutVar? v.getId).map (·.ghost)).getD false then
+          throwErrorAt v "a ghost variable takes a plain reassignment, as in `{v.getId} := e`"
   | _         => checkMutVarsForShadowing vars
 
 def LetOrReassign.registerReassignAliasInfo (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit := do
@@ -53,11 +67,10 @@ def LetOrReassign.registerReassignAliasInfo (letOrReassign : LetOrReassign) (var
 def elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) : DoElabM Expr := do
   declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isGhostDecl do
     letOrReassign.registerReassignAliasInfo vars
-    let ghostVars ← match letOrReassign with
-      | .let _ true => pure vars
-      | .reassign   => vars.filterM fun v => return ((← findMutVar? v.getId).map (·.ghost)).getD false
-      | _           => pure #[]
-    ghostVars.foldr (init := k) withErasedProj
+    if ← isGhost letOrReassign vars then
+      vars.foldr (init := k) withErasedProj
+    else
+      k
 
 def elabDoLetOrReassignWith (hint : MessageData) (letOrReassign : LetOrReassign) (vars : Array Ident)
     (k : DoElabM Expr) (elabBody : (body : Term) → TermElabM Expr) : DoElabM Expr := do
@@ -120,16 +133,7 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
   let vars ← getLetDeclVars decl
   letOrReassign.checkMutVars vars
   let dec ← dec.ensureUnitAt tk
-  -- Reassigning a ghost variable wraps its value, which only the single-variable form can do.
-  let isGhost ← do
-    if letOrReassign matches .reassign then
-      let some v ← vars.findM? fun v => return ((← findMutVar? v.getId).map (·.ghost)).getD false
-        | pure false
-      unless decl matches `(letDecl| $_:ident $[: $_]? := $_) do
-        throwErrorAt v "a ghost variable takes a plain reassignment, as in `{v.getId} := e`"
-      pure true
-    else
-      pure letOrReassign.isGhostDecl
+  let isGhost ← isGhost letOrReassign vars
   -- Some decl preprocessing on the patterns and expected types:
   let decl ← if isGhost then wrapGhostDecl letOrReassign decl
              else pushTypeIntoReassignment letOrReassign decl

From 9febc91b2167880c1e33c29ebb2cbb6f8c802d20 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 07:35:40 +0000
Subject: [PATCH 10/28] refactor: `MutVar.stateType` and `MutVar.stateValue`

Every site that packs a mutable variable into runtime state repeated the lookup plus the ghost `Erased` wrap; the two accessors name it once, and `mkErasedApp` folds into `stateType`.
---
 src/Lean/Elab/BuiltinDo/For.lean |  6 ++----
 src/Lean/Elab/Do/Basic.lean      | 28 +++++++++++++++-------------
 src/Lean/Elab/Do/Control.lean    | 15 ++++-----------
 3 files changed, 21 insertions(+), 28 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/For.lean b/src/Lean/Elab/BuiltinDo/For.lean
index 2174e9531c3a..a10ce2c1bcbd 100644
--- a/src/Lean/Elab/BuiltinDo/For.lean
+++ b/src/Lean/Elab/BuiltinDo/For.lean
@@ -308,10 +308,8 @@ private def mkForInLoopGadget (g : ForInApp)
         | some e => mkSome oldReturnCont.resultType e
       defs := defs.push returnVar
     for x in loopMutVars do
-      let defn ← getLocalDeclFromUserName x.getId
-      Term.addTermInfo' x.ident defn.toExpr
-      -- A ghost variable's state slot carries the `Erased` value; its projection rebinds at unpacking.
-      let v ← if x.ghost then mkErasedMkApp defn.toExpr else pure defn.toExpr
+      Term.addTermInfo' x.ident (← getFVarFromUserName x.getId)
+      let v ← x.stateValue
       -- ForIn forces the mut tuple into the universe mi.u: that of the do block result type.
       -- If we don't do this, then we are stuck on solving constraints such as
       --   `max ?u.46 ?u.47 =?= max (max ?u.22 ?u.46) ?u.47`
diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index 0ad3207b0883..0dbc5fc7820c 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -627,15 +627,22 @@ def withErasedProj (x : Ident) (k : DoElabM Expr) (info : Bool := true) : DoElab
 def withErasedProjs (mutVars : Array MutVar) (k : DoElabM Expr) (info : Bool := true) : DoElabM Expr :=
   (mutVars.filter (·.ghost)).foldr (init := k) fun mv k => withErasedProj mv.ident k info
 
-/-- `Erased t` for the type `t` of runtime-erased data. -/
-def mkErasedApp (t : Expr) : MetaM Expr :=
-  return mkApp (mkConst ``Erased [← getLevel t]) t
-
 /-- `Erased.mk e`, which erases `e` in compiled code. -/
 def mkErasedMkApp (e : Expr) : MetaM Expr := do
   let t ← inferType e
   return mkApp2 (mkConst ``Erased.mk [← getLevel t]) t e
 
+/-- The type of `mv`'s slot in runtime state (tuples, join parameters): a ghost variable's slot
+carries the `Erased` value. -/
+def MutVar.stateType (mv : MutVar) : MetaM Expr := do
+  let t := (← getLocalDeclFromUserName mv.getId).type
+  if mv.ghost then return mkApp (mkConst ``Erased [← getLevel t]) t else return t
+
+/-- The current value of `mv` as packed into runtime state. -/
+def MutVar.stateValue (mv : MutVar) : MetaM Expr := do
+  let v := (← getLocalDeclFromUserName mv.getId).toExpr
+  if mv.ghost then mkErasedMkApp v else return v
+
 /--
 Given a list of mut vars `vars` and an FVar `tupleVar` binding a tuple, bind the mut vars to the
 fields of the tuple and call `k` in the resulting local context.
@@ -720,14 +727,11 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
   let γ := (← read).doBlockResultType
   let mγ ← mkMonadApp γ
   let mutVars := (← read).mutVars |>.filter (callerInfo.reassigns.contains ·.getId)
-  let mutVarNames := mutVars.map (·.getId)
   let joinName ← mkFreshUserName `__do_jp
   -- σ is the tuple type of the mut vars, or mγ if jumpCount = 0. Hence it is either level mi.u or mi.v.
   -- let σ ← mkFreshTypeMVar (userName := `σ)
-  let mutDecls ← mutVarNames.mapM (getLocalDeclFromUserName ·)
   -- A ghost variable's join parameter carries the `Erased` value; its projection rebinds below.
-  let mutTypes ← (mutVars.zip mutDecls).mapM fun (mv, d) =>
-    if mv.ghost then mkErasedApp d.type else pure d.type
+  let mutTypes ← mutVars.mapM (·.stateType)
   let joinTy ← mkArrow nondupDec.resultType (← mkArrowN mutTypes mγ)
   let joinRhsMVar ← mkFreshExprSyntheticOpaqueMVar joinTy
   withLetDecl joinName joinTy joinRhsMVar (kind := .implDetail) (nondep := true) fun jp => do
@@ -736,10 +740,8 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     let result ← getFVarFromUserName nondupDec.resultName
     let mut e := mkApp jp' result
     for x in mutVars do
-      let newX ← getFVarFromUserName x.getId
-      Term.addTermInfo' x.ident newX
-      let arg ← if x.ghost then mkErasedMkApp newX else pure newX
-      e := mkApp e arg
+      Term.addTermInfo' x.ident (← getFVarFromUserName x.getId)
+      e := mkApp e (← x.stateValue)
     return e
 
   let elabBody :=
@@ -750,7 +752,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
 
   let joinRhs ← joinRhsMVar.mvarId!.withContext do
     withLocalDeclD nondupDec.resultName nondupDec.resultType fun r => do
-    withLocalDeclsDND ((mutDecls.zip mutTypes).map fun (d, t) => (d.userName, t)) fun muts => do
+    withLocalDeclsDND ((mutVars.zip mutTypes).map fun (mv, t) => (mv.getId, t)) fun muts => do
     for (x, newX) in mutVars.zip muts do Term.addTermInfo' x.ident newX
     let e ← withErasedProjs mutVars (nondupDec.withDeadCodeFromInfo callerInfo).k
     mkLambdaFVars (#[r] ++ muts) e
diff --git a/src/Lean/Elab/Do/Control.lean b/src/Lean/Elab/Do/Control.lean
index 0daff25cc68b..e93239baf5cf 100644
--- a/src/Lean/Elab/Do/Control.lean
+++ b/src/Lean/Elab/Do/Control.lean
@@ -45,9 +45,8 @@ def ControlStack.stateT (baseMonadInfo : MonadInfo) (muts : Array MutVar) (σ :
     -- `e : StateT σ m α`. Fetch the state tuple `s : σ` and apply it to `e`, `e.run s`.
     -- See also `StateT.monadControl.liftWith`.
     let mutExprs ← muts.mapM fun x => do
-      let defn ← getLocalDeclFromUserName x.getId
-      Term.addTermInfo' x.ident defn.toExpr
-      if x.ghost then mkErasedMkApp defn.toExpr else pure defn.toExpr
+      Term.addTermInfo' x.ident (← getFVarFromUserName x.getId)
+      x.stateValue
     let (tuple, tupleTy) ← mkProdMkN mutExprs baseMonadInfo.u
     unless ← isDefEq tupleTy σ do -- just for sanity; maybe delete in the future
       throwError "State tuple type mismatch: expected {σ}, got {tupleTy}. This is a bug in the `do` elaborator."
@@ -64,11 +63,7 @@ def ControlStack.stateT (baseMonadInfo : MonadInfo) (muts : Array MutVar) (σ :
     base.restoreCont { resultName, resultType, k }
 where
   mutVarNames := muts.map (·.getId)
-  getσ := do
-    let tys ← muts.mapM fun mv => do
-      let t := (← getLocalDeclFromUserName mv.getId).type
-      if mv.ghost then mkErasedApp t else pure t
-    mkProdN tys baseMonadInfo.u
+  getσ := do mkProdN (← muts.mapM (·.stateType)) baseMonadInfo.u
   stM α := return mkApp2 (mkConst ``Prod [baseMonadInfo.u, baseMonadInfo.u]) α (← getσ) -- NB: muts `σ` might have been refined by dependent pattern matches
 
 def ControlStack.optionT (baseMonadInfo : MonadInfo) (optionTWrapper casesOnWrapper : Name)
@@ -214,9 +209,7 @@ def EffectForwarder.ofCont (info : ControlInfo) (dec : DoElemCont) : DoElabM Eff
   let mi := (← read).monadInfo
   let reassignedMutVars := (← read).mutVars |>.filter (info.reassigns.contains ·.getId)
   let ρ := (← getReturnCont).resultType
-  let σ ← mkProdN (← reassignedMutVars.mapM fun mv => do
-    let t := (← getLocalDeclFromUserName mv.getId).type
-    if mv.ghost then mkErasedApp t else pure t) mi.u
+  let σ ← mkProdN (← reassignedMutVars.mapM (·.stateType)) mi.u
 
   let needEarlyReturn := if info.returnsEarly then some ρ else none
   let needBreak := info.breaks && (← getBreakCont).isSome

From a27c0c13340332a5334ccafdc1a5b5cdb9099309 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 07:51:01 +0000
Subject: [PATCH 11/28] =?UTF-8?q?refactor:=20reduce=20every=20reassignment?=
 =?UTF-8?q?=20`x=20=E2=86=90=20act`=20to=20`x=20:=3D=20y`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The bind binder takes the action's result at the variable's declared type under a fresh name, and the reassignment routes through `elabDoLetOrReassign`, the one home of type pinning, ghost wrapping, projection rebinding and alias registration. This also registers the previously missing `FVarAliasInfo` for plain arrow reassignments, which `elabDoIdDecl` never emitted.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 24 +++++++++++-------------
 1 file changed, 11 insertions(+), 13 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index 2c26968f3515..c36367086736 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -212,19 +212,17 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
     letOrReassign.checkMutVars #[x]
     let dec ← dec.ensureUnitAt tk
     if letOrReassign matches .reassign then
-      if ((← findMutVar? x.getId).map (·.ghost)).getD false then
-        let y := mkIdentFrom x (← mkFreshUserName `__y)
-        return ← elabDoIdDecl y xType? rhs
-          (elabDoElem (← `(doElem| $x:ident := $y)) dec) (kind := dec.kind)
-    -- For plain variable reassignment, we know the expected type of the reassigned variable and
-    -- propagate it eagerly via type ascription if the user hasn't provided one themselves:
-    let xType? ← match letOrReassign, xType? with
-      | .reassign, none =>
-        let decl ← getLocalDeclFromUserName x.getId
-        some <$> Term.exprToSyntax decl.type
-      | _, _ => pure xType?
-    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.isGhostDecl <| dec.continueWithUnit)
-      (kind := dec.kind)
+      -- Reduce to a `:=`-reassignment: the bind binder takes the action's result at the
+      -- variable's declared type, and the reassignment of `x`, with its type pinning, ghost
+      -- wrapping and alias registration, has its one home in `elabDoLetOrReassign`.
+      let xType? ← match xType? with
+        | none => some <$> Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
+        | some t => pure (some t)
+      let y := mkIdentFrom x (← mkFreshUserName `__y)
+      elabDoIdDecl y xType? rhs (elabDoElem (← `(doElem| $x:ident := $y)) dec) (kind := dec.kind)
+    else
+      elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.isGhostDecl <| dec.continueWithUnit)
+        (kind := dec.kind)
   | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
     let dec ← dec.ensureUnitAt tk

From 9cb8d84e2fc14f03a4abd53c058cb14a467ed258 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 09:07:48 +0000
Subject: [PATCH 12/28] =?UTF-8?q?refactor:=20expand=20`x=20=E2=86=90=20act?=
 =?UTF-8?q?`=20reassignments=20as=20a=20builtin=20macro?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`doReassignArrow` expands to `do let __x ← act; x := __x` for identifiers, patterns and holes alike, so `elabDoReassignArrow` is gone and `elabDoArrow` rejects `.reassign` as an elaborator bug. The `:=`-reassignment owns type pinning, ghost wrapping, projection rebinding and alias registration, and `InferControlInfo` sees the expansion, so no arrow-specific reassignment logic remains anywhere.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 41 +++++++++++++-------------------
 1 file changed, 16 insertions(+), 25 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index c36367086736..0a9e4d1b2214 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -32,8 +32,6 @@ def LetOrReassign.getLetMutTk? (letOrReassign : LetOrReassign) : Option Syntax :
   | .let mutTk? _ => mutTk?
   | _             => none
 
-/-- Whether the binding is a `ghost` declaration. A reassignment's ghostness follows from its
-variable's `MutVar` record instead. -/
 def LetOrReassign.isGhostDecl (letOrReassign : LetOrReassign) : Bool :=
   match letOrReassign with
   | .let _ ghost => ghost
@@ -207,22 +205,14 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
   | _ => throwUnsupportedSyntax
 
 def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``doPatDecl]) (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
+  if letOrReassign matches .reassign then
+    throwError "Reassigning `←` expands to `:=` before elaboration. This is an elaborator bug."
   match stx with
   | `(doIdDecl| $x:ident $[: $xType?]? ← $rhs) =>
     letOrReassign.checkMutVars #[x]
     let dec ← dec.ensureUnitAt tk
-    if letOrReassign matches .reassign then
-      -- Reduce to a `:=`-reassignment: the bind binder takes the action's result at the
-      -- variable's declared type, and the reassignment of `x`, with its type pinning, ghost
-      -- wrapping and alias registration, has its one home in `elabDoLetOrReassign`.
-      let xType? ← match xType? with
-        | none => some <$> Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
-        | some t => pure (some t)
-      let y := mkIdentFrom x (← mkFreshUserName `__y)
-      elabDoIdDecl y xType? rhs (elabDoElem (← `(doElem| $x:ident := $y)) dec) (kind := dec.kind)
-    else
-      elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.isGhostDecl <| dec.continueWithUnit)
-        (kind := dec.kind)
+    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.isGhostDecl <| dec.continueWithUnit)
+      (kind := dec.kind)
   | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
     let dec ← dec.ensureUnitAt tk
@@ -240,11 +230,7 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
         throwUnsupportedSyntax
       | .have, _ =>
         elabDoElem (← `(doElem| have $pattern:term := $x)) dec
-      | .reassign, _ =>
-        -- otherwise? is always `none`, because there is no `doReassignElse`
-        unless rest?.isNone do
-          throwError "reassignment with `|` (i.e., \"else clause\") is not supported"
-        elabDoElem (← `(doElem| $pattern:term := $x)) dec
+      | .reassign, _ => unreachable!
   | _ => throwUnsupportedSyntax
 
 private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letConfig)
@@ -326,10 +312,15 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
     throwErrorAt cfg "configuration options are not supported with `←`"
   elabDoArrow (.let mutTk? false) decl tk dec
 
-@[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do
+@[builtin_macro Lean.Parser.Term.doReassignArrow] def expandDoReassignArrow : Macro := fun stx => do
   match stx with
-  | `(doReassignArrow| $decl:doIdDecl) =>
-    elabDoArrow .reassign decl decl dec
-  | `(doReassignArrow| $decl:doPatDecl) =>
-    elabDoArrow .reassign decl decl dec
-  | _ => throwUnsupportedSyntax
+  | `(doReassignArrow| $x:ident $[: $t?]? ← $rhs) =>
+    let y := mkIdentFrom x (← MonadQuotation.addMacroScope `__x)
+    `(doElem| do let $y:ident $[: $t?]? ← $rhs; $x:ident := $y)
+  | `(doReassignArrow| $pat:term $[: $t?]? ← $rhs $[| $otherwise? $(_rest?)?]?) =>
+    if otherwise?.isSome then
+      Macro.throwErrorAt stx "reassignment with `|` (i.e., \"else clause\") is not supported"
+    else
+      let y := mkIdentFrom pat (← MonadQuotation.addMacroScope `__x)
+      `(doElem| do let $y:ident $[: $t?]? ← $rhs; $pat:term := $y)
+  | _ => Macro.throwUnsupported

From 4a131be170f5829bcf1c1d9abb8f9e6e48fa05bb Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 09:23:39 +0000
Subject: [PATCH 13/28] =?UTF-8?q?refactor:=20expand=20`ghost=20x=20?=
 =?UTF-8?q?=E2=86=90=20act`=20as=20a=20builtin=20macro?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`doGhostArrow` expands to `do let __x ← act; ghost x := __x`, so its elaborator is gone and `InferControlInfo` reads the expansion. The ghost element is built with a named quotation and spliced, since the category grammar of the compiling stage predates `doGhost`.
---
 src/Lean/Elab/BuiltinDo/Let.lean       | 19 ++++++++-----------
 src/Lean/Elab/Do/Basic.lean            |  2 +-
 src/Lean/Elab/Do/InferControlInfo.lean |  2 --
 3 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index 0a9e4d1b2214..e34ffbbea7e5 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -181,8 +181,6 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
     trace[Elab.let.decl] "{id.getId} : {type} := {val}"
     withLetDecl id.getId (kind := kind) type val (nondep := nondep) fun x => do
       Term.addLocalVarInfo id x
-      -- The ghost `.out` projection of `elabWithReassignments` must close before `mkLetFVars`
-      -- binds the carried variable, so it wraps only the continuation.
       match config.eq? with
       | none =>
         let body ← elabWithReassignments letOrReassign vars dec.continueWithUnit
@@ -248,15 +246,14 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   let `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? := $e) := stx | throwUnsupportedSyntax
   elabDoLetOrReassign {} (.let mutTk? true) (← `(letDecl| $x:ident $[: $t?]? := $e)) tk dec
 
-@[builtin_doElem_elab Lean.Parser.Term.doGhostArrow] def elabDoGhostArrow : DoElab := fun stx dec => do
-  let `(doGhostArrow| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? ← $rhs) := stx
-    | throwUnsupportedSyntax
-  checkMutVarsForShadowing #[x]
-  let dec ← dec.ensureUnitAt tk
-  let y := mkIdentFrom x (← mkFreshUserName `__y)
-  elabDoIdDecl y t? rhs
-    (elabDoElem ⟨(← `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident := $y)).raw⟩ dec)
-    (kind := dec.kind)
+@[builtin_macro Lean.Parser.Term.doGhostArrow] def expandDoGhostArrow : Macro := fun stx => do
+  match stx with
+  | `(doGhostArrow| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? ← $rhs) =>
+    let y := mkIdentFrom x (← MonadQuotation.addMacroScope `__x)
+    let letElem ← `(doElem| let $y:ident $[: $t?]? ← $rhs)
+    let ghostElem : TSyntax `doElem := ⟨(← `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident := $y)).raw⟩
+    `(doElem| do $letElem:doElem; $ghostElem:doElem)
+  | _ => Macro.throwUnsupported
 
 @[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do
   let `(doHave| have%$tk $config:letConfig $decl:letDecl) := stx | throwUnsupportedSyntax
diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index 0dbc5fc7820c..a85805ae5761 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -649,7 +649,7 @@ fields of the tuple and call `k` in the resulting local context.
 -/
 def bindMutVarsFromTuple (vars : List Name) (tupleVar : FVarId) (k : DoElabM Expr) : DoElabM Expr := do
   let ghosts := (← read).mutVars.filter fun mv => mv.ghost && vars.contains mv.getId
-  -- Like the rebindings themselves, the projections contribute only aliases here.
+  -- Like the ghost rebindings themselves, the projections contribute only aliases here.
   let k := withErasedProjs ghosts k (info := false)
   go vars tupleVar (← tupleVar.getType) #[] k
 where
diff --git a/src/Lean/Elab/Do/InferControlInfo.lean b/src/Lean/Elab/Do/InferControlInfo.lean
index 088e1d9f63c6..e9f87e4f6be7 100644
--- a/src/Lean/Elab/Do/InferControlInfo.lean
+++ b/src/Lean/Elab/Do/InferControlInfo.lean
@@ -160,8 +160,6 @@ partial def ofElem (stx : DoElem) : TermElabM ControlInfo := do
     ofLetOrReassign #[] none otherwise body?
   | `(doElem| let $[mut]? $_:letConfig $decl) =>
     ofLetOrReassignArrow false decl
-  | `(doGhostArrow| ghost $[mut]? $decl:doIdDecl) =>
-    ofLetOrReassignArrow false decl
   | `(doGhost| ghost $[mut]? $_) => return .pure
   | `(doElem| $decl:letIdDeclNoBinders) =>
     ofLetOrReassign (← getLetIdDeclVars ⟨decl⟩) none none none

From 9dc21d3402e4275f42d49291f3d0e860b08e994c Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 09:32:37 +0000
Subject: [PATCH 14/28] refactor: `elabDoArrow` takes `mutTk?` and `ghost`

Its one caller is `doLetArrow`: reassignment arrows expand to `:=` before elaboration, and `have` has no arrow form, so the `LetOrReassign` parameter and the dead `.have` and `.reassign` arms go. A pattern arrow re-emits a `let` unconditionally, which for the bind binder is indistinguishable from `have`.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 27 ++++++++-------------------
 1 file changed, 8 insertions(+), 19 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index e34ffbbea7e5..bba75ee72edb 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -70,11 +70,6 @@ def elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (
     else
       k
 
-def elabDoLetOrReassignWith (hint : MessageData) (letOrReassign : LetOrReassign) (vars : Array Ident)
-    (k : DoElabM Expr) (elabBody : (body : Term) → TermElabM Expr) : DoElabM Expr := do
-  -- letOrReassign.checkMutVars vars -- Should be done by the caller!
-  doElabToSyntax hint (elabWithReassignments letOrReassign vars k) fun body => elabBody body
-
 private def pushTypeIntoReassignment (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl) : TermElabM (TSyntax ``letDecl) := do
   if letOrReassign matches .reassign then
     match decl with
@@ -202,14 +197,13 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
             mkLetFVars #[x, h'] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
   | _ => throwUnsupportedSyntax
 
-def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``doPatDecl]) (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
-  if letOrReassign matches .reassign then
-    throwError "Reassigning `←` expands to `:=` before elaboration. This is an elaborator bug."
+def elabDoArrow (mutTk? : Option Syntax) (ghost : Bool) (stx : TSyntax [``doIdDecl, ``doPatDecl])
+    (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
   match stx with
   | `(doIdDecl| $x:ident $[: $xType?]? ← $rhs) =>
-    letOrReassign.checkMutVars #[x]
+    checkMutVarsForShadowing #[x]
     let dec ← dec.ensureUnitAt tk
-    elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x letOrReassign.isGhostDecl <| dec.continueWithUnit)
+    elabDoIdDecl x xType? rhs (declareMutVar? mutTk? x ghost <| dec.continueWithUnit)
       (kind := dec.kind)
   | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
@@ -219,16 +213,11 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
     let rest? := rest?.join
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
     elabDoIdDecl x patType? rhs do
-      match letOrReassign, otherwise? with
-      | .let mutTk? _, some otherwise =>
+      match otherwise? with
+      | some otherwise =>
         elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x | $otherwise $(rest?)?)) dec
-      | .let mutTk? _, _ =>
+      | none =>
         elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x)) dec
-      | .have, some _otherwise =>
-        throwUnsupportedSyntax
-      | .have, _ =>
-        elabDoElem (← `(doElem| have $pattern:term := $x)) dec
-      | .reassign, _ => unreachable!
   | _ => throwUnsupportedSyntax
 
 private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letConfig)
@@ -307,7 +296,7 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   checkLetConfigInDo config
   if config.nondep || config.usedOnly || config.zeta || config.eq?.isSome then
     throwErrorAt cfg "configuration options are not supported with `←`"
-  elabDoArrow (.let mutTk? false) decl tk dec
+  elabDoArrow mutTk? false decl tk dec
 
 @[builtin_macro Lean.Parser.Term.doReassignArrow] def expandDoReassignArrow : Macro := fun stx => do
   match stx with

From c680bd51c57af0e715efd67cfb4b94366a7a5b27 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 09:36:56 +0000
Subject: [PATCH 15/28] refactor: inline `elabDoArrow` into `elabDoLetArrow`

It had one caller left.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 44 +++++++++++++++-----------------
 1 file changed, 20 insertions(+), 24 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index bba75ee72edb..8cbb5431d24c 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -197,29 +197,6 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
             mkLetFVars #[x, h'] body (usedLetOnly := config.usedOnly) (generalizeNondepLet := false)
   | _ => throwUnsupportedSyntax
 
-def elabDoArrow (mutTk? : Option Syntax) (ghost : Bool) (stx : TSyntax [``doIdDecl, ``doPatDecl])
-    (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
-  match stx with
-  | `(doIdDecl| $x:ident $[: $xType?]? ← $rhs) =>
-    checkMutVarsForShadowing #[x]
-    let dec ← dec.ensureUnitAt tk
-    elabDoIdDecl x xType? rhs (declareMutVar? mutTk? x ghost <| dec.continueWithUnit)
-      (kind := dec.kind)
-  | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
-    let x := mkIdentFrom pattern (← mkFreshUserName `__x)
-    let dec ← dec.ensureUnitAt tk
-    elabDoIdDecl x patType? rhs dec.continueWithUnit (kind := dec.kind)
-  | `(doPatDecl| $pattern:term $[: $patType?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
-    let rest? := rest?.join
-    let x := mkIdentFrom pattern (← mkFreshUserName `__x)
-    elabDoIdDecl x patType? rhs do
-      match otherwise? with
-      | some otherwise =>
-        elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x | $otherwise $(rest?)?)) dec
-      | none =>
-        elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x)) dec
-  | _ => throwUnsupportedSyntax
-
 private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letConfig)
     (mutTk? : Option Syntax) (initConfig : Term.LetConfig := {}) : DoElabM Term.LetConfig := do
   if mutTk?.isSome && !letConfigStx.raw[0].getArgs.isEmpty then
@@ -296,7 +273,26 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   checkLetConfigInDo config
   if config.nondep || config.usedOnly || config.zeta || config.eq?.isSome then
     throwErrorAt cfg "configuration options are not supported with `←`"
-  elabDoArrow mutTk? false decl tk dec
+  match decl with
+  | `(doIdDecl| $x:ident $[: $xType?]? ← $rhs) =>
+    checkMutVarsForShadowing #[x]
+    let dec ← dec.ensureUnitAt tk
+    elabDoIdDecl x xType? rhs (declareMutVar? mutTk? x false <| dec.continueWithUnit)
+      (kind := dec.kind)
+  | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
+    let x := mkIdentFrom pattern (← mkFreshUserName `__x)
+    let dec ← dec.ensureUnitAt tk
+    elabDoIdDecl x patType? rhs dec.continueWithUnit (kind := dec.kind)
+  | `(doPatDecl| $pattern:term $[: $patType?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
+    let rest? := rest?.join
+    let x := mkIdentFrom pattern (← mkFreshUserName `__x)
+    elabDoIdDecl x patType? rhs do
+      match otherwise? with
+      | some otherwise =>
+        elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x | $otherwise $(rest?)?)) dec
+      | none =>
+        elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x)) dec
+  | _ => throwUnsupportedSyntax
 
 @[builtin_macro Lean.Parser.Term.doReassignArrow] def expandDoReassignArrow : Macro := fun stx => do
   match stx with

From 91ee8e82a9eb8bdf3c9d51137ed93940204004a5 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 10:22:11 +0000
Subject: [PATCH 16/28] refactor: zeta the `.out` projections of loop
 annotations

`wrapErasedProjs`'s syntax-level lets survive into verification conditions where the join-point path inlines the projection, so the gadget call zeta-substitutes them after elaboration and annotation goals carry ghost projections inline uniformly.
---
 src/Lean/Elab/BuiltinDo/For.lean | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/BuiltinDo/For.lean b/src/Lean/Elab/BuiltinDo/For.lean
index a10ce2c1bcbd..a0a766080252 100644
--- a/src/Lean/Elab/BuiltinDo/For.lean
+++ b/src/Lean/Elab/BuiltinDo/For.lean
@@ -182,6 +182,14 @@ private def ForInApp.wrapErasedProjs (g : ForInApp) (e : Term) : DoElabM Term :=
     e ← `(let $(mv.ident):ident := Erased.out $(⟨mv.ident.raw⟩); $e)
   return e
 
+/-- Zeta-substitute the `.out` projection lets of `wrapErasedProjs`, so annotations carry the
+projection inline like the compiled body does. -/
+private partial def zetaErasedProjs (e : Expr) : Expr :=
+  e.replace fun
+    | .letE _ _ v b _ =>
+      if v.isAppOfArity ``Erased.out 2 then some (zetaErasedProjs (b.instantiate1 v)) else none
+    | _ => none
+
 /-- Abstract `e` over the loop's state tuple, so that `e` may name the loop's mutable variables. -/
 private def ForInApp.mkStateFun (g : ForInApp) (e : Term) : DoElabM Term := do
   `(fun $(g.statePat) => $(← g.wrapErasedProjs e))
@@ -198,7 +206,8 @@ private def ForInApp.mkCall (g : ForInApp) (ref : Syntax) (gadget : Name)
   let call ← `(open scoped Std.WP Lean.Order in
     $(mkIdent gadget) $(← Term.exprToSyntax g.xs) $(← Term.exprToSyntax g.init)
       $(← Term.exprToSyntax g.body) $annotations*)
-  Term.elabTermEnsuringType call (mkApp (← read).monadInfo.m g.σ)
+  let e ← Term.elabTermEnsuringType call (mkApp (← read).monadInfo.m g.σ)
+  return zetaErasedProjs (← instantiateMVars e)
 
 /-- The binders and body of an `invariant` clause. An ascription covering the binder list would
 cover the loop's binders and the assertion's alike, so it is reported here. -/

From 0febbdf580fdd92c115011c3904c89b8a1120a0e Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 10:22:11 +0000
Subject: [PATCH 17/28] doc: why the else arrow form keeps its continuation
 type

The else form swallows the rest of the block into `rest?`, so coercing the element to `Unit` there rejects valid programs; state the fact where the hoist looks tempting.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index 8cbb5431d24c..b0b2c44f016d 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -283,6 +283,8 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
     let dec ← dec.ensureUnitAt tk
     elabDoIdDecl x patType? rhs dec.continueWithUnit (kind := dec.kind)
+  -- No `ensureUnitAt` here: the else form swallows the rest of the block into `rest?`, so the
+  -- element keeps `dec`'s result type.
   | `(doPatDecl| $pattern:term $[: $patType?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
     let rest? := rest?.join
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)

From 6bc0b9471ab11fed48fd4f001b372a062623d2b7 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 10:47:43 +0000
Subject: [PATCH 18/28] fix: keep `ghost`-headed statements of a variable named
 `ghost` parsing

`notFollowedByRedefinedTermToken` also guards `doExpr`, so listing `ghost` there broke every statement headed by an identifier of that name. Follow `assert` instead: the ghost parsers take priority `default+10`, which breaks their equal-length tie with the pattern-reassignment parse of `ghost x := e`, and `doExpr`'s trailing guard already rejects that shape. Applications, reassignments and binds of a variable named `ghost` parse again.
---
 src/Lean/Parser/Do.lean               |  7 +++----
 tests/elab/intrinsicVerification.lean | 13 +++++++++++++
 2 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 4ac60180303c..7424e86da790 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -63,8 +63,7 @@ def notFollowedByRedefinedTermToken :=
   -- an "open" command follows the `do`-block.
   -- If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
   notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "match_expr" <|> "let" <|> "let_expr" <|> "have" <|>
-      "do" <|> "dbg_trace" <|> "idbg" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try" <|>
-      nonReservedSymbol "ghost")
+      "do" <|> "dbg_trace" <|> "idbg" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
     "token at 'do' element"
 
 namespace InternalSyntax
@@ -111,10 +110,10 @@ def letIdDeclNoBinders := leading_parser
   atomic (node ``letId ident >> pushNone >> optType >> " := ") >> termParser
 
 /-- `ghost x := e` declares a verification-only variable; `mut` allows reassignment. -/
-@[builtin_doElem_parser] def doGhost := leading_parser
+@[builtin_doElem_parser default+10] def doGhost := leading_parser
   nonReservedSymbol "ghost " (includeIdent := true) >> optional "mut " >> letIdDeclNoBinders
 /-- `ghost x ← act` runs `act` and hides its result in a verification-only variable. -/
-@[builtin_doElem_parser] def doGhostArrow := leading_parser
+@[builtin_doElem_parser default+10] def doGhostArrow := leading_parser
   nonReservedSymbol "ghost " (includeIdent := true) >> optional "mut " >> doIdDecl
 
 @[builtin_doElem_parser] def doReassign      := leading_parser
diff --git a/tests/elab/intrinsicVerification.lean b/tests/elab/intrinsicVerification.lean
index 337acf2321b6..072ce9e5c38a 100644
--- a/tests/elab/intrinsicVerification.lean
+++ b/tests/elab/intrinsicVerification.lean
@@ -971,6 +971,19 @@ def ghostLeak (xs : List Nat) : Id Nat := do
     seen := x :: seen
   return seen.length
 
+/-! `ghost` stays a regular identifier at a doElem head when no ghost shape parses. -/
+
+def ghostAsIdent (ghost : Nat → Id Unit) : Id Nat := do
+  ghost 5
+  let mut ghost := 1
+  ghost := ghost + 1
+  ghost ← pure 3
+  pure ghost
+
+/-- info: 3 -/
+#guard_msgs in
+#eval ghostAsIdent fun _ => pure ()
+
 /-! A ghost variable stays out of pattern reassignments. -/
 
 /-- error: a ghost variable takes a plain reassignment, as in `g := e` -/

From f87ddffc4195ecda6aa388b7ff7b8590660db162 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 10:57:14 +0000
Subject: [PATCH 19/28] fix: ghost ascription checking and reassignment-arrow
 error blame
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Restore the push-then-wrap order that the ghost-bit removal reverted: `pushTypeIntoReassignment` runs for ghost reassignments too, so a contradicting ascription errors like a plain one, and `wrapGhostDecl` is the mechanical wrap again. The ident form of `x ← act` moves from the expansion macro back to an elaborator that pins the variable's declared type on the bind, so a type error blames the action instead of the hygienic bind variable; patterns and the else rejection stay in the macro.
---
 src/Lean/Elab/BuiltinDo/Let.lean      | 40 ++++++++++++---------------
 tests/elab/intrinsicVerification.lean | 16 +++++++++++
 2 files changed, 34 insertions(+), 22 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index b0b2c44f016d..eb7ccf3a0f1b 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -100,25 +100,14 @@ private def checkLetConfigInDo (config : Term.LetConfig) : DoElabM Unit := do
   if config.generalize then
     throwError "`+generalize` is not supported in `do` blocks"
 
-/--
-Wrap a ghost decl `ghost x : t := e` as `let x : Erased t := Erased.mk e`, similarly for
-reassigments.
--/
-private def wrapGhostDecl (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl) :
-    DoElabM (TSyntax ``letDecl) := do
+/-- Wrap a ghost binding `x : t := e` as `x : Erased t := Erased.mk e`. For a reassignment,
+`pushTypeIntoReassignment` has already checked the ascription and pinned `t`. -/
+private def wrapGhostDecl (decl : TSyntax ``letDecl) : DoElabM (TSyntax ``letDecl) := do
   let `(letDecl| $x:ident $[: $t?]? := $e) := decl
     | throwErrorAt decl "`ghost` takes a variable"
-  match letOrReassign with
-  | .reassign =>
-    let t ← Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
-    let e ← match t? with
-      | some tAsc => `(Erased.mk ($e : $tAsc))
-      | none      => `(Erased.mk ($e : $t))
-    `(letDecl| $x:ident : Erased $t := $e)
-  | _ =>
-    match t? with
-    | some t => `(letDecl| $x:ident : Erased $t := Erased.mk $e)
-    | none   => `(letDecl| $x:ident := Erased.mk $e)
+  match t? with
+  | some t => `(letDecl| $x:ident : Erased $t := Erased.mk $e)
+  | none   => `(letDecl| $x:ident := Erased.mk $e)
 
 partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl)
     (tk : Syntax) (dec : DoElemCont) : DoElabM Expr := do
@@ -128,8 +117,8 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
   let dec ← dec.ensureUnitAt tk
   let isGhost ← isGhost letOrReassign vars
   -- Some decl preprocessing on the patterns and expected types:
-  let decl ← if isGhost then wrapGhostDecl letOrReassign decl
-             else pushTypeIntoReassignment letOrReassign decl
+  let decl ← pushTypeIntoReassignment letOrReassign decl
+  let decl ← if isGhost then wrapGhostDecl decl else pure decl
   let mγ ← mkMonadApp (← read).doBlockResultType
   match decl with
   | `(letDecl| $decl:letEqnsDecl) =>
@@ -298,9 +287,6 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
 
 @[builtin_macro Lean.Parser.Term.doReassignArrow] def expandDoReassignArrow : Macro := fun stx => do
   match stx with
-  | `(doReassignArrow| $x:ident $[: $t?]? ← $rhs) =>
-    let y := mkIdentFrom x (← MonadQuotation.addMacroScope `__x)
-    `(doElem| do let $y:ident $[: $t?]? ← $rhs; $x:ident := $y)
   | `(doReassignArrow| $pat:term $[: $t?]? ← $rhs $[| $otherwise? $(_rest?)?]?) =>
     if otherwise?.isSome then
       Macro.throwErrorAt stx "reassignment with `|` (i.e., \"else clause\") is not supported"
@@ -308,3 +294,13 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
       let y := mkIdentFrom pat (← MonadQuotation.addMacroScope `__x)
       `(doElem| do let $y:ident $[: $t?]? ← $rhs; $pat:term := $y)
   | _ => Macro.throwUnsupported
+
+@[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do
+  let `(doReassignArrow| $x:ident $[: $t?]? ← $rhs) := stx | throwUnsupportedSyntax
+  throwUnlessMutVarDeclared x
+  -- Pin the variable's declared type on the bind, so a type error blames the action.
+  let t ← match t? with
+    | some t => pure t
+    | none   => Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
+  let y := mkIdentFrom x (← mkFreshUserName `__x)
+  elabDoIdDecl y (some t) rhs (elabDoElem (← `(doElem| $x:ident := $y)) dec) (kind := dec.kind)
diff --git a/tests/elab/intrinsicVerification.lean b/tests/elab/intrinsicVerification.lean
index 072ce9e5c38a..f4c54a3ad2a0 100644
--- a/tests/elab/intrinsicVerification.lean
+++ b/tests/elab/intrinsicVerification.lean
@@ -971,6 +971,22 @@ def ghostLeak (xs : List Nat) : Id Nat := do
     seen := x :: seen
   return seen.length
 
+/-! A ghost reassignment checks a contradicting type ascription like a plain one. -/
+
+/--
+error: Type mismatch
+  g
+has type
+  Int
+but is expected to have type
+  Nat
+-/
+#guard_msgs in
+def ghostAscriptionMismatch : Id Nat := do
+  ghost mut g : Int := 0
+  g : Nat := 1
+  pure 0
+
 /-! `ghost` stays a regular identifier at a doElem head when no ghost shape parses. -/
 
 def ghostAsIdent (ghost : Nat → Id Unit) : Id Nat := do

From 0840e3783f9ed32173ab343fa0b273b28951aa5c Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 11:28:37 +0000
Subject: [PATCH 20/28] refactor: one elaborator for `doReassignArrow`

The pin forces an elaborator for the ident form, so the pattern form and the else rejection join it instead of living in a macro half; the legacy elaborator's native path resumes entirely.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 33 +++++++++++++++-----------------
 1 file changed, 15 insertions(+), 18 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index eb7ccf3a0f1b..f06212c4fb32 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -285,22 +285,19 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
         elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x)) dec
   | _ => throwUnsupportedSyntax
 
-@[builtin_macro Lean.Parser.Term.doReassignArrow] def expandDoReassignArrow : Macro := fun stx => do
-  match stx with
-  | `(doReassignArrow| $pat:term $[: $t?]? ← $rhs $[| $otherwise? $(_rest?)?]?) =>
-    if otherwise?.isSome then
-      Macro.throwErrorAt stx "reassignment with `|` (i.e., \"else clause\") is not supported"
-    else
-      let y := mkIdentFrom pat (← MonadQuotation.addMacroScope `__x)
-      `(doElem| do let $y:ident $[: $t?]? ← $rhs; $pat:term := $y)
-  | _ => Macro.throwUnsupported
-
 @[builtin_doElem_elab Lean.Parser.Term.doReassignArrow] def elabDoReassignArrow : DoElab := fun stx dec => do
-  let `(doReassignArrow| $x:ident $[: $t?]? ← $rhs) := stx | throwUnsupportedSyntax
-  throwUnlessMutVarDeclared x
-  -- Pin the variable's declared type on the bind, so a type error blames the action.
-  let t ← match t? with
-    | some t => pure t
-    | none   => Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
-  let y := mkIdentFrom x (← mkFreshUserName `__x)
-  elabDoIdDecl y (some t) rhs (elabDoElem (← `(doElem| $x:ident := $y)) dec) (kind := dec.kind)
+  match stx with
+  | `(doReassignArrow| $x:ident $[: $t?]? ← $rhs) =>
+    throwUnlessMutVarDeclared x
+    -- Pin the variable's declared type on the bind, so a type error blames the action.
+    let t ← match t? with
+      | some t => pure t
+      | none   => Term.exprToSyntax (← getLocalDeclFromUserName x.getId).type
+    let y := mkIdentFrom x (← mkFreshUserName `__x)
+    elabDoIdDecl y (some t) rhs (elabDoElem (← `(doElem| $x:ident := $y)) dec) (kind := dec.kind)
+  | `(doReassignArrow| $pat:term $[: $t?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
+    unless otherwise?.isNone && rest?.join.isNone do
+      throwError "reassignment with `|` (i.e., \"else clause\") is not supported"
+    let y := mkIdentFrom pat (← mkFreshUserName `__x)
+    elabDoIdDecl y t? rhs (elabDoElem (← `(doElem| $pat:term := $y)) dec) (kind := dec.kind)
+  | _ => throwUnsupportedSyntax

From 60bd9dc0660198dd319342cedc42ae2a24dc21c7 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 11:34:07 +0000
Subject: [PATCH 21/28] fix: keep `Erased.mk` out of ghost type-mismatch errors

An ascribed ghost binding wraps its value as `Erased.mk (e : t)`, so a mismatch reports the plain ascription error instead of an application mismatch inside the generated `Erased.mk`.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index f06212c4fb32..64e0745e9db4 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -106,7 +106,7 @@ private def wrapGhostDecl (decl : TSyntax ``letDecl) : DoElabM (TSyntax ``letDec
   let `(letDecl| $x:ident $[: $t?]? := $e) := decl
     | throwErrorAt decl "`ghost` takes a variable"
   match t? with
-  | some t => `(letDecl| $x:ident : Erased $t := Erased.mk $e)
+  | some t => `(letDecl| $x:ident : Erased $t := Erased.mk ($e : $t))
   | none   => `(letDecl| $x:ident := Erased.mk $e)
 
 partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOrReassign) (decl : TSyntax ``letDecl)

From 239a166031cc5d490b421240c9411617ff75e229 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 11:58:22 +0000
Subject: [PATCH 22/28] feat: ghost-specific noncomputability error

A definition that uses a ghost value in compiled code now reports what a ghost variable is and where its value is available, instead of naming `Erased.out` as a noncomputable dependency.
---
 src/Lean/Compiler/LCNF/ToLCNF.lean    | 2 ++
 tests/elab/intrinsicVerification.lean | 2 +-
 tests/elab/usesOfNoncomputable.lean   | 2 +-
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index 3e905cc1a9f2..9e2f7cfd29fd 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -447,6 +447,8 @@ private def checkComputable (ref : Name) : M Unit := do
   -- `noncomputable section`, where the failure to compile the `_unsafe_rec` version is tolerated and
   -- only that auxiliary is marked `noncomputable`, leaving `ref` itself unmarked.
   if isNoncomputable (← getEnv) ref || isNoncomputable (← getEnv) (mkUnsafeRecName ref) then
+    if ref == `Erased.out then
+      throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition: it uses the value of a ghost (`Erased`) variable in compiled code. Ghost values exist for verification only: use them in specifications, `invariant` clauses and `assert`s, or mark the definition 'noncomputable'"
     throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName ref}', which is 'noncomputable'"
   else if getOriginalConstKind? (← getEnv) ref matches some .axiom | some .quot | some .induct | some .thm then
     throwNamedError lean.dependsOnNoncomputable f!"`{ref}` not supported by code generator; consider marking definition as `noncomputable`"
diff --git a/tests/elab/intrinsicVerification.lean b/tests/elab/intrinsicVerification.lean
index f4c54a3ad2a0..28cb69eeb0fa 100644
--- a/tests/elab/intrinsicVerification.lean
+++ b/tests/elab/intrinsicVerification.lean
@@ -962,7 +962,7 @@ def ghostBranch (b : Bool) : Id Nat
 `Erased.out`. -/
 
 /--
-error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Erased.out', which is 'noncomputable'
+error: failed to compile definition: it uses the value of a ghost (`Erased`) variable in compiled code. Ghost values exist for verification only: use them in specifications, `invariant` clauses and `assert`s, or mark the definition 'noncomputable'
 -/
 #guard_msgs in
 def ghostLeak (xs : List Nat) : Id Nat := do
diff --git a/tests/elab/usesOfNoncomputable.lean b/tests/elab/usesOfNoncomputable.lean
index 5e58989e3fb6..3bbe6302d246 100644
--- a/tests/elab/usesOfNoncomputable.lean
+++ b/tests/elab/usesOfNoncomputable.lean
@@ -51,7 +51,7 @@ def test10 : Foo where
   data := 0
 
 /--
-error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Erased.out', which is 'noncomputable'
+error: failed to compile definition: it uses the value of a ghost (`Erased`) variable in compiled code. Ghost values exist for verification only: use them in specifications, `invariant` clauses and `assert`s, or mark the definition 'noncomputable'
 -/
 #guard_msgs in
 def test11 : Foo where

From 5266f61d526ba5832a3f031cc53969c4a24f1f74 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 12:05:14 +0000
Subject: [PATCH 23/28] refactor: reword the ghost noncomputability error

Name the evidence, `Erased.out`, state the inference and the rule declaratively, and keep the sibling message's cadence.
---
 src/Lean/Compiler/LCNF/ToLCNF.lean    | 2 +-
 tests/elab/intrinsicVerification.lean | 2 +-
 tests/elab/usesOfNoncomputable.lean   | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index 9e2f7cfd29fd..f5e20673ec71 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -448,7 +448,7 @@ private def checkComputable (ref : Name) : M Unit := do
   -- only that auxiliary is marked `noncomputable`, leaving `ref` itself unmarked.
   if isNoncomputable (← getEnv) ref || isNoncomputable (← getEnv) (mkUnsafeRecName ref) then
     if ref == `Erased.out then
-      throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition: it uses the value of a ghost (`Erased`) variable in compiled code. Ghost values exist for verification only: use them in specifications, `invariant` clauses and `assert`s, or mark the definition 'noncomputable'"
+      throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition: it depends on 'Erased.out', which recovers the value of a ghost variable. A ghost variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'."
     throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName ref}', which is 'noncomputable'"
   else if getOriginalConstKind? (← getEnv) ref matches some .axiom | some .quot | some .induct | some .thm then
     throwNamedError lean.dependsOnNoncomputable f!"`{ref}` not supported by code generator; consider marking definition as `noncomputable`"
diff --git a/tests/elab/intrinsicVerification.lean b/tests/elab/intrinsicVerification.lean
index 28cb69eeb0fa..51a9ff030247 100644
--- a/tests/elab/intrinsicVerification.lean
+++ b/tests/elab/intrinsicVerification.lean
@@ -962,7 +962,7 @@ def ghostBranch (b : Bool) : Id Nat
 `Erased.out`. -/
 
 /--
-error: failed to compile definition: it uses the value of a ghost (`Erased`) variable in compiled code. Ghost values exist for verification only: use them in specifications, `invariant` clauses and `assert`s, or mark the definition 'noncomputable'
+error: failed to compile definition: it depends on 'Erased.out', which recovers the value of a ghost variable. A ghost variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'.
 -/
 #guard_msgs in
 def ghostLeak (xs : List Nat) : Id Nat := do
diff --git a/tests/elab/usesOfNoncomputable.lean b/tests/elab/usesOfNoncomputable.lean
index 3bbe6302d246..f21fac66e5f8 100644
--- a/tests/elab/usesOfNoncomputable.lean
+++ b/tests/elab/usesOfNoncomputable.lean
@@ -51,7 +51,7 @@ def test10 : Foo where
   data := 0
 
 /--
-error: failed to compile definition: it uses the value of a ghost (`Erased`) variable in compiled code. Ghost values exist for verification only: use them in specifications, `invariant` clauses and `assert`s, or mark the definition 'noncomputable'
+error: failed to compile definition: it depends on 'Erased.out', which recovers the value of a ghost variable. A ghost variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'.
 -/
 #guard_msgs in
 def test11 : Foo where

From 74d334af39387a7e3bb60fda07d2aa6340a6e9b1 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 12:11:43 +0000
Subject: [PATCH 24/28] refactor: `+zeta` for the annotation projection
 bindings

The term elaborator substitutes the `.out` projection let away itself, replacing the post-elaboration expression pass.
---
 src/Lean/Elab/BuiltinDo/For.lean | 16 ++++------------
 1 file changed, 4 insertions(+), 12 deletions(-)

diff --git a/src/Lean/Elab/BuiltinDo/For.lean b/src/Lean/Elab/BuiltinDo/For.lean
index a0a766080252..fc808307c996 100644
--- a/src/Lean/Elab/BuiltinDo/For.lean
+++ b/src/Lean/Elab/BuiltinDo/For.lean
@@ -175,21 +175,14 @@ structure ForInApp where
   ghostMutVars : Array MutVar := #[]
 
 /-- Bind the `.out` projection of each ghost variable over `e`, so that an annotation names ghost
-variables at their underlying type. The bindings sit in erased positions, so they compile. -/
+variables at their underlying type. The `+zeta` substitutes the binding away at elaboration, so
+annotation goals carry the projection inline like the compiled body does. -/
 private def ForInApp.wrapErasedProjs (g : ForInApp) (e : Term) : DoElabM Term := do
   let mut e := e
   for mv in g.ghostMutVars do
-    e ← `(let $(mv.ident):ident := Erased.out $(⟨mv.ident.raw⟩); $e)
+    e ← `(let +zeta $(mv.ident):ident := Erased.out $(⟨mv.ident.raw⟩); $e)
   return e
 
-/-- Zeta-substitute the `.out` projection lets of `wrapErasedProjs`, so annotations carry the
-projection inline like the compiled body does. -/
-private partial def zetaErasedProjs (e : Expr) : Expr :=
-  e.replace fun
-    | .letE _ _ v b _ =>
-      if v.isAppOfArity ``Erased.out 2 then some (zetaErasedProjs (b.instantiate1 v)) else none
-    | _ => none
-
 /-- Abstract `e` over the loop's state tuple, so that `e` may name the loop's mutable variables. -/
 private def ForInApp.mkStateFun (g : ForInApp) (e : Term) : DoElabM Term := do
   `(fun $(g.statePat) => $(← g.wrapErasedProjs e))
@@ -206,8 +199,7 @@ private def ForInApp.mkCall (g : ForInApp) (ref : Syntax) (gadget : Name)
   let call ← `(open scoped Std.WP Lean.Order in
     $(mkIdent gadget) $(← Term.exprToSyntax g.xs) $(← Term.exprToSyntax g.init)
       $(← Term.exprToSyntax g.body) $annotations*)
-  let e ← Term.elabTermEnsuringType call (mkApp (← read).monadInfo.m g.σ)
-  return zetaErasedProjs (← instantiateMVars e)
+  Term.elabTermEnsuringType call (mkApp (← read).monadInfo.m g.σ)
 
 /-- The binders and body of an `invariant` clause. An ascription covering the binder list would
 cover the loop's binders and the assertion's alike, so it is reported here. -/

From 389dc88f76d716ec230cd94be4f9ca6347652e63 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 12:14:52 +0000
Subject: [PATCH 25/28] refactor: replace a dead ghost-shape error with
 throwUnsupportedSyntax

Both producers of a ghost declaration already guarantee the binder-free ident shape that `wrapGhostDecl` destructures.
---
 src/Lean/Elab/BuiltinDo/Let.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index 64e0745e9db4..bbc4294ed175 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -104,7 +104,7 @@ private def checkLetConfigInDo (config : Term.LetConfig) : DoElabM Unit := do
 `pushTypeIntoReassignment` has already checked the ascription and pinned `t`. -/
 private def wrapGhostDecl (decl : TSyntax ``letDecl) : DoElabM (TSyntax ``letDecl) := do
   let `(letDecl| $x:ident $[: $t?]? := $e) := decl
-    | throwErrorAt decl "`ghost` takes a variable"
+    | throwUnsupportedSyntax
   match t? with
   | some t => `(letDecl| $x:ident : Erased $t := Erased.mk ($e : $t))
   | none   => `(letDecl| $x:ident := Erased.mk $e)

From e749d3e665a6480d5f3b3ad8c7585ec3483bbc52 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 12:42:55 +0000
Subject: [PATCH 26/28] refactor: `grind =` for `Erased.mk_inj`

---
 src/Init/Data/Erased.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/Erased.lean b/src/Init/Data/Erased.lean
index 337f40475d72..8c7d3ddf7f68 100644
--- a/src/Init/Data/Erased.lean
+++ b/src/Init/Data/Erased.lean
@@ -37,7 +37,7 @@ noncomputable def out {α : Sort u} (e : Erased α) : α :=
 @[ext] theorem out_inj {α : Sort u} {a b : Erased α} (h : a.out = b.out) : a = b := by
   rw [← mk_out a, ← mk_out b, h]
 
-@[simp, grind] theorem mk_inj {α : Sort u} {a b : α} : mk a = mk b ↔ a = b :=
+@[simp, grind =] theorem mk_inj {α : Sort u} {a b : α} : mk a = mk b ↔ a = b :=
   ⟨fun h => by have := congrArg out h; rwa [out_mk, out_mk] at this, fun h => h ▸ rfl⟩
 
 end Erased

From d81f1d5a9df8914979cb615fa969925d74423cfd Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 16:45:21 +0000
Subject: [PATCH 27/28] refactor: rename `ghost` declarations to `erased`

The doElem keyword, the parser nodes, the elaborators, and the `MutVar` flag all carry the `erased` name, matching the `Erased` type that implements them.
---
 src/Lean/Compiler/LCNF/ToLCNF.lean      |  2 +-
 src/Lean/Elab/BuiltinDo/For.lean        | 10 ++--
 src/Lean/Elab/BuiltinDo/Let.lean        | 44 +++++++-------
 src/Lean/Elab/Do/Basic.lean             | 42 ++++++-------
 src/Lean/Elab/Do/InferControlInfo.lean  |  4 +-
 src/Lean/Parser/Do.lean                 | 12 ++--
 tests/elab/formatTerm.lean              |  8 +--
 tests/elab/formatTerm.lean.out.expected |  6 +-
 tests/elab/intrinsicVerification.lean   | 78 ++++++++++++-------------
 tests/elab/usesOfNoncomputable.lean     |  2 +-
 10 files changed, 104 insertions(+), 104 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index f5e20673ec71..1b8ba44b17a2 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -448,7 +448,7 @@ private def checkComputable (ref : Name) : M Unit := do
   -- only that auxiliary is marked `noncomputable`, leaving `ref` itself unmarked.
   if isNoncomputable (← getEnv) ref || isNoncomputable (← getEnv) (mkUnsafeRecName ref) then
     if ref == `Erased.out then
-      throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition: it depends on 'Erased.out', which recovers the value of a ghost variable. A ghost variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'."
+      throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition: it depends on 'Erased.out', which recovers the value of an erased variable. An erased variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'."
     throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName ref}', which is 'noncomputable'"
   else if getOriginalConstKind? (← getEnv) ref matches some .axiom | some .quot | some .induct | some .thm then
     throwNamedError lean.dependsOnNoncomputable f!"`{ref}` not supported by code generator; consider marking definition as `noncomputable`"
diff --git a/src/Lean/Elab/BuiltinDo/For.lean b/src/Lean/Elab/BuiltinDo/For.lean
index fc808307c996..27d6c4e9a678 100644
--- a/src/Lean/Elab/BuiltinDo/For.lean
+++ b/src/Lean/Elab/BuiltinDo/For.lean
@@ -170,16 +170,16 @@ structure ForInApp where
   σ : Expr
   /-- The pattern naming the loop's mutable variables in the state tuple. -/
   statePat : Term
-  /-- The ghost variables among the loop's mutable variables; annotations bind their `.out`
+  /-- The erased variables among the loop's mutable variables; annotations bind their `.out`
   projections over the state tuple. -/
-  ghostMutVars : Array MutVar := #[]
+  erasedMutVars : Array MutVar := #[]
 
-/-- Bind the `.out` projection of each ghost variable over `e`, so that an annotation names ghost
+/-- Bind the `.out` projection of each erased variable over `e`, so that an annotation names erased
 variables at their underlying type. The `+zeta` substitutes the binding away at elaboration, so
 annotation goals carry the projection inline like the compiled body does. -/
 private def ForInApp.wrapErasedProjs (g : ForInApp) (e : Term) : DoElabM Term := do
   let mut e := e
-  for mv in g.ghostMutVars do
+  for mv in g.erasedMutVars do
     e ← `(let +zeta $(mv.ident):ident := Erased.out $(⟨mv.ident.raw⟩); $e)
   return e
 
@@ -381,7 +381,7 @@ private def mkForInLoopGadget (g : ForInApp)
   unless inv?.isNone && dec?.isNone do
     let g : ForInApp :=
       { xs, init := preS, body, σ, statePat := ← mkStatePat loopMutVars info.returnsEarly,
-        ghostMutVars := loopMutVars.filter (·.ghost) }
+        erasedMutVars := loopMutVars.filter (·.erased) }
     if (← instantiateMVars ρ).isConstOf ``Lean.Loop then
       if let some e ← mkForInLoopGadget g inv? dec? then forIn := e
     else if let some decClause := dec? then
diff --git a/src/Lean/Elab/BuiltinDo/Let.lean b/src/Lean/Elab/BuiltinDo/Let.lean
index bbc4294ed175..6d04a6c55d13 100644
--- a/src/Lean/Elab/BuiltinDo/Let.lean
+++ b/src/Lean/Elab/BuiltinDo/Let.lean
@@ -14,7 +14,7 @@ import Lean.Elab.Do.PatternVar
 
 public section
 
--- The `ghost` doElem quotations below need the current stage's parser until stage0 catches up.
+-- The `erased` doElem quotations below need the current stage's parser until stage0 catches up.
 set_option internal.parseQuotWithCurrentStage true
 
 namespace Lean.Elab.Do
@@ -23,7 +23,7 @@ open Lean.Parser.Term
 open Lean.Meta
 
 inductive LetOrReassign
-  | let (mutTk? : Option Syntax) (ghost : Bool)
+  | let (mutTk? : Option Syntax) (erased : Bool)
   | have
   | reassign
 
@@ -32,29 +32,29 @@ def LetOrReassign.getLetMutTk? (letOrReassign : LetOrReassign) : Option Syntax :
   | .let mutTk? _ => mutTk?
   | _             => none
 
-def LetOrReassign.isGhostDecl (letOrReassign : LetOrReassign) : Bool :=
+def LetOrReassign.isErasedDecl (letOrReassign : LetOrReassign) : Bool :=
   match letOrReassign with
-  | .let _ ghost => ghost
+  | .let _ erased => erased
   | _            => false
 
-def isGhost (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Bool := do
+def isErased (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Bool := do
   match letOrReassign with
-  | .let _ ghost => return ghost
+  | .let _ erased => return erased
   | .reassign    =>
     let some v := vars[0]? | return false
     let some mv ← findMutVar? v.getId | return false
-    return mv.ghost
+    return mv.erased
   | _            => return false
 
 def LetOrReassign.checkMutVars (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit :=
   match letOrReassign with
   | .reassign => do
     throwUnlessMutVarsDeclared vars
-    -- Reassigning a ghost variable wraps its value, which only the single-variable form can do.
+    -- Reassigning an erased variable wraps its value, which only the single-variable form can do.
     unless vars.size == 1 do
       for v in vars do
-        if ((← findMutVar? v.getId).map (·.ghost)).getD false then
-          throwErrorAt v "a ghost variable takes a plain reassignment, as in `{v.getId} := e`"
+        if ((← findMutVar? v.getId).map (·.erased)).getD false then
+          throwErrorAt v "an erased variable takes a plain reassignment, as in `{v.getId} := e`"
   | _         => checkMutVarsForShadowing vars
 
 def LetOrReassign.registerReassignAliasInfo (letOrReassign : LetOrReassign) (vars : Array Ident) : DoElabM Unit := do
@@ -63,9 +63,9 @@ def LetOrReassign.registerReassignAliasInfo (letOrReassign : LetOrReassign) (var
       registerMutVarAlias var.getId
 
 def elabWithReassignments (letOrReassign : LetOrReassign) (vars : Array Ident) (k : DoElabM Expr) : DoElabM Expr := do
-  declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isGhostDecl do
+  declareMutVars? letOrReassign.getLetMutTk? vars letOrReassign.isErasedDecl do
     letOrReassign.registerReassignAliasInfo vars
-    if ← isGhost letOrReassign vars then
+    if ← isErased letOrReassign vars then
       vars.foldr (init := k) withErasedProj
     else
       k
@@ -100,9 +100,9 @@ private def checkLetConfigInDo (config : Term.LetConfig) : DoElabM Unit := do
   if config.generalize then
     throwError "`+generalize` is not supported in `do` blocks"
 
-/-- Wrap a ghost binding `x : t := e` as `x : Erased t := Erased.mk e`. For a reassignment,
+/-- Wrap an erased binding `x : t := e` as `x : Erased t := Erased.mk e`. For a reassignment,
 `pushTypeIntoReassignment` has already checked the ascription and pinned `t`. -/
-private def wrapGhostDecl (decl : TSyntax ``letDecl) : DoElabM (TSyntax ``letDecl) := do
+private def wrapErasedDecl (decl : TSyntax ``letDecl) : DoElabM (TSyntax ``letDecl) := do
   let `(letDecl| $x:ident $[: $t?]? := $e) := decl
     | throwUnsupportedSyntax
   match t? with
@@ -115,10 +115,10 @@ partial def elabDoLetOrReassign (config : Term.LetConfig) (letOrReassign : LetOr
   let vars ← getLetDeclVars decl
   letOrReassign.checkMutVars vars
   let dec ← dec.ensureUnitAt tk
-  let isGhost ← isGhost letOrReassign vars
+  let isErased ← isErased letOrReassign vars
   -- Some decl preprocessing on the patterns and expected types:
   let decl ← pushTypeIntoReassignment letOrReassign decl
-  let decl ← if isGhost then wrapGhostDecl decl else pure decl
+  let decl ← if isErased then wrapErasedDecl decl else pure decl
   let mγ ← mkMonadApp (← read).doBlockResultType
   match decl with
   | `(letDecl| $decl:letEqnsDecl) =>
@@ -197,17 +197,17 @@ private def getLetConfigAndCheckMut (letConfigStx : TSyntax ``Parser.Term.letCon
   let config ← getLetConfigAndCheckMut config mutTk?
   elabDoLetOrReassign config (.let mutTk? false) decl tk dec
 
-@[builtin_doElem_elab Lean.Parser.Term.doGhost] def elabDoGhost : DoElab := fun stx dec => do
-  let `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? := $e) := stx | throwUnsupportedSyntax
+@[builtin_doElem_elab Lean.Parser.Term.doErased] def elabDoErased : DoElab := fun stx dec => do
+  let `(doErased| erased%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? := $e) := stx | throwUnsupportedSyntax
   elabDoLetOrReassign {} (.let mutTk? true) (← `(letDecl| $x:ident $[: $t?]? := $e)) tk dec
 
-@[builtin_macro Lean.Parser.Term.doGhostArrow] def expandDoGhostArrow : Macro := fun stx => do
+@[builtin_macro Lean.Parser.Term.doErasedArrow] def expandDoErasedArrow : Macro := fun stx => do
   match stx with
-  | `(doGhostArrow| ghost%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? ← $rhs) =>
+  | `(doErasedArrow| erased%$tk $[mut%$mutTk?]? $x:ident $[: $t?]? ← $rhs) =>
     let y := mkIdentFrom x (← MonadQuotation.addMacroScope `__x)
     let letElem ← `(doElem| let $y:ident $[: $t?]? ← $rhs)
-    let ghostElem : TSyntax `doElem := ⟨(← `(doGhost| ghost%$tk $[mut%$mutTk?]? $x:ident := $y)).raw⟩
-    `(doElem| do $letElem:doElem; $ghostElem:doElem)
+    let erasedElem : TSyntax `doElem := ⟨(← `(doErased| erased%$tk $[mut%$mutTk?]? $x:ident := $y)).raw⟩
+    `(doElem| do $letElem:doElem; $erasedElem:doElem)
   | _ => Macro.throwUnsupported
 
 @[builtin_doElem_elab Lean.Parser.Term.doHave] def elabDoHave : DoElab := fun stx dec => do
diff --git a/src/Lean/Elab/Do/Basic.lean b/src/Lean/Elab/Do/Basic.lean
index a85805ae5761..29330123cc41 100644
--- a/src/Lean/Elab/Do/Basic.lean
+++ b/src/Lean/Elab/Do/Basic.lean
@@ -100,12 +100,12 @@ def CodeLiveness.lub (a b : CodeLiveness) : CodeLiveness :=
 
 /-- A mutable variable declared by `let mut` in a `do` block. -/
 structure MutVar where
-  /-- The identifier of the `let mut` or `ghost mut` declaration. -/
+  /-- The identifier of the `let mut` or `erased mut` declaration. -/
   ident : Ident
   /-- The `FVarId` of the initial binding produced by the declaration. -/
   baseId : FVarId
-  /-- Whether the variable comes from `ghost mut`. -/
-  ghost : Bool
+  /-- Whether the variable comes from `erased mut`. -/
+  erased : Bool
   deriving Inhabited
 
 /-- The raw `Name` of a `mut` variable, as found in the local context. -/
@@ -339,30 +339,30 @@ def DoOps.default : DoOps where
     return mkApp (← read).monadInfo.m α
 
 /-- Register the given name as that of a `mut` variable. -/
-def declareMutVar (x : Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α := do
+def declareMutVar (x : Ident) (erased : Bool) (k : DoElabM α) : DoElabM α := do
   let fvar ← getFVarFromUserName x.getId
-  let mutVar : MutVar := { ident := x, baseId := fvar.fvarId!, ghost }
+  let mutVar : MutVar := { ident := x, baseId := fvar.fvarId!, erased }
   withReader (fun ctx => { ctx with
     mutVars := ctx.mutVars.push mutVar,
     mutVarDefs := ctx.mutVarDefs.insert x.getId mutVar,
   }) k
 
 /-- Register the given names as that of `mut` variables. -/
-def declareMutVars (xs : Array Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α := do
+def declareMutVars (xs : Array Ident) (erased : Bool) (k : DoElabM α) : DoElabM α := do
   let fvars ← xs.mapM (getFVarFromUserName ·.getId)
-  let newMutVars : Array MutVar := xs.zipWith (fun x fvar => { ident := x, baseId := fvar.fvarId!, ghost }) fvars
+  let newMutVars : Array MutVar := xs.zipWith (fun x fvar => { ident := x, baseId := fvar.fvarId!, erased }) fvars
   withReader (fun ctx => { ctx with
     mutVars := ctx.mutVars ++ newMutVars,
     mutVarDefs := ctx.mutVarDefs.insertMany (newMutVars.map fun mutVar => (mutVar.getId, mutVar)),
   }) k
 
 /-- Register the given name as that of a `mut` variable if the syntax token `mut` is present. -/
-def declareMutVar? (mutTk? : Option Syntax) (x : Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α :=
-  if mutTk?.isSome then declareMutVar x ghost k else k
+def declareMutVar? (mutTk? : Option Syntax) (x : Ident) (erased : Bool) (k : DoElabM α) : DoElabM α :=
+  if mutTk?.isSome then declareMutVar x erased k else k
 
 /-- Register the given names as that of `mut` variables if the syntax token `mut` is present. -/
-def declareMutVars? (mutTk? : Option Syntax) (xs : Array Ident) (ghost : Bool) (k : DoElabM α) : DoElabM α :=
-  if mutTk?.isSome then declareMutVars xs ghost k else k
+def declareMutVars? (mutTk? : Option Syntax) (xs : Array Ident) (erased : Bool) (k : DoElabM α) : DoElabM α :=
+  if mutTk?.isSome then declareMutVars xs erased k else k
 
 /-- Look up a declared `mut` variable by its raw `Name`. -/
 def findMutVar? (n : Name) : DoElabM (Option MutVar) := do
@@ -611,7 +611,7 @@ binding away, so the source name reaches proofs and never compiled code. The new
 def withErasedProj (x : Ident) (k : DoElabM Expr) (info : Bool := true) : DoElabM Expr := do
   let carried ← getLocalDeclFromUserName x.getId
   let_expr c@Erased t ← carried.type
-    | throwError "the carried binding of ghost variable `{x.getId}` has type{indentExpr carried.type}\ninstead of an `Erased` type"
+    | throwError "the carried binding of erased variable `{x.getId}` has type{indentExpr carried.type}\ninstead of an `Erased` type"
   let outVal := mkApp2 (mkConst ``Erased.out c.constLevels!) t carried.toExpr
   withLetDecl x.getId t outVal (nondep := true) fun xv => do
     if info then
@@ -623,34 +623,34 @@ def withErasedProj (x : Ident) (k : DoElabM Expr) (info : Bool := true) : DoElab
     let body ← k
     return (← body.abstractM #[xv]).instantiate1 outVal
 
-/-- Bind the `.out` projection of each ghost variable among `mutVars` around `k`. -/
+/-- Bind the `.out` projection of each erased variable among `mutVars` around `k`. -/
 def withErasedProjs (mutVars : Array MutVar) (k : DoElabM Expr) (info : Bool := true) : DoElabM Expr :=
-  (mutVars.filter (·.ghost)).foldr (init := k) fun mv k => withErasedProj mv.ident k info
+  (mutVars.filter (·.erased)).foldr (init := k) fun mv k => withErasedProj mv.ident k info
 
 /-- `Erased.mk e`, which erases `e` in compiled code. -/
 def mkErasedMkApp (e : Expr) : MetaM Expr := do
   let t ← inferType e
   return mkApp2 (mkConst ``Erased.mk [← getLevel t]) t e
 
-/-- The type of `mv`'s slot in runtime state (tuples, join parameters): a ghost variable's slot
+/-- The type of `mv`'s slot in runtime state (tuples, join parameters): an erased variable's slot
 carries the `Erased` value. -/
 def MutVar.stateType (mv : MutVar) : MetaM Expr := do
   let t := (← getLocalDeclFromUserName mv.getId).type
-  if mv.ghost then return mkApp (mkConst ``Erased [← getLevel t]) t else return t
+  if mv.erased then return mkApp (mkConst ``Erased [← getLevel t]) t else return t
 
 /-- The current value of `mv` as packed into runtime state. -/
 def MutVar.stateValue (mv : MutVar) : MetaM Expr := do
   let v := (← getLocalDeclFromUserName mv.getId).toExpr
-  if mv.ghost then mkErasedMkApp v else return v
+  if mv.erased then mkErasedMkApp v else return v
 
 /--
 Given a list of mut vars `vars` and an FVar `tupleVar` binding a tuple, bind the mut vars to the
 fields of the tuple and call `k` in the resulting local context.
 -/
 def bindMutVarsFromTuple (vars : List Name) (tupleVar : FVarId) (k : DoElabM Expr) : DoElabM Expr := do
-  let ghosts := (← read).mutVars.filter fun mv => mv.ghost && vars.contains mv.getId
-  -- Like the ghost rebindings themselves, the projections contribute only aliases here.
-  let k := withErasedProjs ghosts k (info := false)
+  let erasedVars := (← read).mutVars.filter fun mv => mv.erased && vars.contains mv.getId
+  -- Like the erased rebindings themselves, the projections contribute only aliases here.
+  let k := withErasedProjs erasedVars k (info := false)
   go vars tupleVar (← tupleVar.getType) #[] k
 where
   go vars tupleVar tupleTy letFVars k := do
@@ -730,7 +730,7 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
   let joinName ← mkFreshUserName `__do_jp
   -- σ is the tuple type of the mut vars, or mγ if jumpCount = 0. Hence it is either level mi.u or mi.v.
   -- let σ ← mkFreshTypeMVar (userName := `σ)
-  -- A ghost variable's join parameter carries the `Erased` value; its projection rebinds below.
+  -- An erased variable's join parameter carries the `Erased` value; its projection rebinds below.
   let mutTypes ← mutVars.mapM (·.stateType)
   let joinTy ← mkArrow nondupDec.resultType (← mkArrowN mutTypes mγ)
   let joinRhsMVar ← mkFreshExprSyntheticOpaqueMVar joinTy
diff --git a/src/Lean/Elab/Do/InferControlInfo.lean b/src/Lean/Elab/Do/InferControlInfo.lean
index e9f87e4f6be7..c46ca91996ec 100644
--- a/src/Lean/Elab/Do/InferControlInfo.lean
+++ b/src/Lean/Elab/Do/InferControlInfo.lean
@@ -13,7 +13,7 @@ import Lean.Elab.Do.PatternVar
 
 public section
 
--- The `ghost` doElem quotations below need the current stage's parser until stage0 catches up.
+-- The `erased` doElem quotations below need the current stage's parser until stage0 catches up.
 set_option internal.parseQuotWithCurrentStage true
 
 namespace Lean.Elab.Do
@@ -160,7 +160,7 @@ partial def ofElem (stx : DoElem) : TermElabM ControlInfo := do
     ofLetOrReassign #[] none otherwise body?
   | `(doElem| let $[mut]? $_:letConfig $decl) =>
     ofLetOrReassignArrow false decl
-  | `(doGhost| ghost $[mut]? $_) => return .pure
+  | `(doErased| erased $[mut]? $_) => return .pure
   | `(doElem| $decl:letIdDeclNoBinders) =>
     ofLetOrReassign (← getLetIdDeclVars ⟨decl⟩) none none none
   | `(doElem| $decl:letPatDecl) =>
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 7424e86da790..92fc8a4455d1 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -109,12 +109,12 @@ Motivations:
 def letIdDeclNoBinders := leading_parser
   atomic (node ``letId ident >> pushNone >> optType >> " := ") >> termParser
 
-/-- `ghost x := e` declares a verification-only variable; `mut` allows reassignment. -/
-@[builtin_doElem_parser default+10] def doGhost := leading_parser
-  nonReservedSymbol "ghost " (includeIdent := true) >> optional "mut " >> letIdDeclNoBinders
-/-- `ghost x ← act` runs `act` and hides its result in a verification-only variable. -/
-@[builtin_doElem_parser default+10] def doGhostArrow := leading_parser
-  nonReservedSymbol "ghost " (includeIdent := true) >> optional "mut " >> doIdDecl
+/-- `erased x := e` declares a verification-only variable; `mut` allows reassignment. -/
+@[builtin_doElem_parser default+10] def doErased := leading_parser
+  nonReservedSymbol "erased " (includeIdent := true) >> optional "mut " >> letIdDeclNoBinders
+/-- `erased x ← act` runs `act` and hides its result in a verification-only variable. -/
+@[builtin_doElem_parser default+10] def doErasedArrow := leading_parser
+  nonReservedSymbol "erased " (includeIdent := true) >> optional "mut " >> doIdDecl
 
 @[builtin_doElem_parser] def doReassign      := leading_parser
   notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
diff --git a/tests/elab/formatTerm.lean b/tests/elab/formatTerm.lean
index 7483cfbe0dd1..730394759573 100644
--- a/tests/elab/formatTerm.lean
+++ b/tests/elab/formatTerm.lean
@@ -86,7 +86,7 @@ def foo : a b c d e f g a b c d e f g h where
 
 #eval fmt `(by rw [] at h)
 
--- `ghost` is its own declaration form beside `let` and `have`
-#eval fmt `(do ghost trace := 0; pure ())
-#eval fmt `(do ghost mut trace : List Nat := []; trace := x :: trace.out)
-#eval fmt `(do ghost mut n ← counter)
+-- `erased` is its own declaration form beside `let` and `have`
+#eval fmt `(do erased trace := 0; pure ())
+#eval fmt `(do erased mut trace : List Nat := []; trace := x :: trace.out)
+#eval fmt `(do erased mut n ← counter)
diff --git a/tests/elab/formatTerm.lean.out.expected b/tests/elab/formatTerm.lean.out.expected
index 68e8b68202eb..10104d663186 100644
--- a/tests/elab/formatTerm.lean.out.expected
+++ b/tests/elab/formatTerm.lean.out.expected
@@ -143,10 +143,10 @@ calc
   1 = 1 := rfl✝
 by rw [] at h✝
 do
-  ghost trace✝ := 0;
+  erased trace✝ := 0;
   pure✝ ()
 do
-  ghost mut trace✝ : List✝ Nat✝ := [];
+  erased mut trace✝ : List✝ Nat✝ := [];
   trace✝ := x✝ :: trace.out✝
 do
-  ghost mut n✝ ← counter✝
+  erased mut n✝ ← counter✝
diff --git a/tests/elab/intrinsicVerification.lean b/tests/elab/intrinsicVerification.lean
index 51a9ff030247..1f8a23410804 100644
--- a/tests/elab/intrinsicVerification.lean
+++ b/tests/elab/intrinsicVerification.lean
@@ -890,16 +890,16 @@ def onOneLine (k : Nat) : Id Nat given (n : Nat) requires k = n ensures r => r =
 #guard_msgs in
 #check @onOneLine.spec
 
-/-! ## Ghost state
+/-! ## Erased state
 
-`ghost` declares verification-only state. The variable reads at its underlying type everywhere,
+`erased` declares verification-only state. The variable reads at its underlying type everywhere,
 its carried `Erased` binding erases in compiled code, and its slot in a loop's state tuple holds
 a dummy. -/
 
-def ghostSumEvens (xs : List Nat) : Id Nat
+def erasedSumEvens (xs : List Nat) : Id Nat
     ensures r => r % 2 = 0 := do
   let mut acc := 0
-  ghost mut seen : List Nat := []
+  erased mut seen : List Nat := []
   for x in xs invariant _pre _suff => acc = 2 * seen.length do
     acc := acc + 2
     seen := x :: seen
@@ -907,15 +907,15 @@ def ghostSumEvens (xs : List Nat) : Id Nat
 
 /-- info: 6 -/
 #guard_msgs in
-#eval ghostSumEvens [1, 2, 3]
+#eval erasedSumEvens [1, 2, 3]
 
-/-! An existential `ensures` takes its witness from a ghost variable: the invariant carries the
+/-! An existential `ensures` takes its witness from an erased variable: the invariant carries the
 witness, and the exit condition instantiates the existential from it. -/
 
-def ghostDoubleSum (xs : List Nat) : Id Nat
+def erasedDoubleSum (xs : List Nat) : Id Nat
     ensures r => ∃ n, r = 2 * n := do
   let mut acc := 0
-  ghost mut half : Nat := 0
+  erased mut half : Nat := 0
   for x in xs invariant _pre _suff => acc = 2 * half do
     acc := acc + x + x
     half := half + x
@@ -923,30 +923,30 @@ def ghostDoubleSum (xs : List Nat) : Id Nat
 
 /-- info: 12 -/
 #guard_msgs in
-#eval ghostDoubleSum [1, 2, 3]
+#eval erasedDoubleSum [1, 2, 3]
 
-/-! The declaration forms: `ghost` with and without `mut`, reassignment with an ascription, and
+/-! The declaration forms: `erased` with and without `mut`, reassignment with an ascription, and
 monadic binds (the action runs, its result erases). -/
 
-def ghostForms : Id Nat := do
-  ghost y := 5
-  ghost mut x := 1
+def erasedForms : Id Nat := do
+  erased y := 5
+  erased mut x := 1
   x := x + y
   x : Nat := 2
-  ghost z ← pure 3
-  ghost mut m ← pure 4
+  erased z ← pure 3
+  erased mut m ← pure 4
   m := m + z
   pure 0
 
 /-- info: 0 -/
 #guard_msgs in
-#eval ghostForms
+#eval erasedForms
 
-/-! A ghost variable reassigned in a branch flows through the join point. -/
+/-! An erased variable reassigned in a branch flows through the join point. -/
 
-def ghostBranch (b : Bool) : Id Nat
+def erasedBranch (b : Bool) : Id Nat
     ensures r => r = 0 := do
-  ghost mut n : Nat := 0
+  erased mut n : Nat := 0
   if b then
     n := n + 1
   else
@@ -956,22 +956,22 @@ def ghostBranch (b : Bool) : Id Nat
 
 /-- info: 0 -/
 #guard_msgs in
-#eval ghostBranch true
+#eval erasedBranch true
 
-/-! A ghost value reaching compiled code is rejected through the noncomputability of
+/-! An erased value reaching compiled code is rejected through the noncomputability of
 `Erased.out`. -/
 
 /--
-error: failed to compile definition: it depends on 'Erased.out', which recovers the value of a ghost variable. A ghost variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'.
+error: failed to compile definition: it depends on 'Erased.out', which recovers the value of an erased variable. An erased variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'.
 -/
 #guard_msgs in
-def ghostLeak (xs : List Nat) : Id Nat := do
-  ghost mut seen : List Nat := []
+def erasedLeak (xs : List Nat) : Id Nat := do
+  erased mut seen : List Nat := []
   for x in xs do
     seen := x :: seen
   return seen.length
 
-/-! A ghost reassignment checks a contradicting type ascription like a plain one. -/
+/-! An erased reassignment checks a contradicting type ascription like a plain one. -/
 
 /--
 error: Type mismatch
@@ -982,30 +982,30 @@ but is expected to have type
   Nat
 -/
 #guard_msgs in
-def ghostAscriptionMismatch : Id Nat := do
-  ghost mut g : Int := 0
+def erasedAscriptionMismatch : Id Nat := do
+  erased mut g : Int := 0
   g : Nat := 1
   pure 0
 
-/-! `ghost` stays a regular identifier at a doElem head when no ghost shape parses. -/
+/-! `erased` stays a regular identifier at a doElem head when no erased shape parses. -/
 
-def ghostAsIdent (ghost : Nat → Id Unit) : Id Nat := do
-  ghost 5
-  let mut ghost := 1
-  ghost := ghost + 1
-  ghost ← pure 3
-  pure ghost
+def erasedAsIdent (erased : Nat → Id Unit) : Id Nat := do
+  erased 5
+  let mut erased := 1
+  erased := erased + 1
+  erased ← pure 3
+  pure erased
 
 /-- info: 3 -/
 #guard_msgs in
-#eval ghostAsIdent fun _ => pure ()
+#eval erasedAsIdent fun _ => pure ()
 
-/-! A ghost variable stays out of pattern reassignments. -/
+/-! An erased variable stays out of pattern reassignments. -/
 
-/-- error: a ghost variable takes a plain reassignment, as in `g := e` -/
+/-- error: an erased variable takes a plain reassignment, as in `g := e` -/
 #guard_msgs in
-def ghostPatReassign : Id Nat := do
+def erasedPatReassign : Id Nat := do
   let mut a := 1
-  ghost mut g := 2
+  erased mut g := 2
   (a, g) := (3, 4)
   pure a
diff --git a/tests/elab/usesOfNoncomputable.lean b/tests/elab/usesOfNoncomputable.lean
index f21fac66e5f8..edbd0cc1004e 100644
--- a/tests/elab/usesOfNoncomputable.lean
+++ b/tests/elab/usesOfNoncomputable.lean
@@ -51,7 +51,7 @@ def test10 : Foo where
   data := 0
 
 /--
-error: failed to compile definition: it depends on 'Erased.out', which recovers the value of a ghost variable. A ghost variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'.
+error: failed to compile definition: it depends on 'Erased.out', which recovers the value of an erased variable. An erased variable's value is available in specifications such as `invariant` clauses and `assert`s, but not in compiled code. Consider marking the definition as 'noncomputable'.
 -/
 #guard_msgs in
 def test11 : Foo where

From 6c23c72425af657f71dfeac54706078eee37f562 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Thu, 10 Sep 2026 16:45:21 +0000
Subject: [PATCH 28/28] chore: check stage0 box

---
 stage0/src/stdlib_flags.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 3baec9ac0fdd..d96a46b866db 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,6 +1,6 @@
 #include "util/options.h"
 
-// [ ] Check box to force CI to test stage 2 and run update-stage0 on PR merge
+// [x] Check box to force CI to test stage 2 and run update-stage0 on PR merge
 // (any other change to this file will do the same; ALL changes should be made to the stage0/ copy)
 
 namespace lean {