feat: erased declarations in do notation - #15090
Merged
Merged
Conversation
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
sgraf812
added
changelog-library
sgraf812
marked this pull request as ready for review
September 10, 2026 12:24
sgraf812
requested review from
hargoniX,
kim-em and
leodemoura
as code owners
September 10, 2026 12:24
sgraf812
force-pushed
the
sg/ghost-do
branch
from
September 10, 2026 12:41
305ff25 to
c30eb5d
Compare
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
sgraf812
force-pushed
the
sg/ghost-do
branch
from
September 10, 2026 14:33
1e7ed59 to
0d7390f
Compare
sgraf812
changed the title
ghost declarations in do notationerased declarations in do notation
sgraf812
force-pushed
the
sg/ghost-do
branch
2 times, most recently
from
September 10, 2026 17:35
d97bb75 to
61a42c0
Compare
|
The adaptation PR for this PR is leanprover/downstream-lean4#64. |
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.
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.
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.
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.
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.
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.
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.
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.
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.
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`.
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.
`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.
`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`.
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`.
It had one caller left.
`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.
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.
`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.
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.
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.
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`.
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.
Name the evidence, `Erased.out`, state the inference and the rule declaratively, and keep the sibling message's cadence.
The term elaborator substitutes the `.out` projection let away itself, replacing the post-elaboration expression pass.
Both producers of a ghost declaration already guarantee the binder-free ident shape that `wrapGhostDecl` destructures.
The doElem keyword, the parser nodes, the elaborators, and the `MutVar` flag all carry the `erased` name, matching the `Erased` type that implements them.
sgraf812
force-pushed
the
sg/ghost-do
branch
from
September 11, 2026 15:49
61a42c0 to
6c23c72
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds erased state to
donotation:erased x := e,erased mut x := e, anderased x ← actdeclare verification-only variables that loopinvariantclauses and assertions can read while compiled code carries only a dummy in their place.An erased variable is backed by the new type
ErasedinInit.Data.Erased, upstreamed from Mathlib.erasedis a doElem of its own besideletandhave. Only the single variable form as the left-hand side pattern is supported.