feat: intrinsic verification syntax for do-notation loops and def contracts

src/Init/Control/Id.lean

@@ -82,9 +82,9 @@ instance : LawfulMonadAttach Id where
 end Id
 
 /-- Turn a collection with a pure `ForIn` instance into an array. -/
-def ForIn.toArray {α : Type u} [inst : ForIn Id ρ α] (xs : ρ) : Array α :=
+@[expose] def ForIn.toArray {α : Type u} [inst : ForIn Id ρ α] (xs : ρ) : Array α :=
   ForIn.forIn xs Array.empty (fun a acc => pure (.yield (acc.push a))) |> Id.run
 
 /-- Turn a collection with a pure `ForIn` instance into a list. -/
-def ForIn.toList {α : Type u} [ForIn Id ρ α] (xs : ρ) : List α :=
+@[expose] def ForIn.toList {α : Type u} [ForIn Id ρ α] (xs : ρ) : List α :=
   ForIn.toArray xs |>.toList

src/Lean/Elab/BuiltinDo/For.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Elab.BuiltinDo.Basic
 meta import Lean.Parser.Do
 import Init.Control.Do
+import Init.While
 import Lean.Meta.ProdN
 
 public section
@@ -20,10 +21,13 @@ open Lean.Meta
 
 @[builtin_macro Lean.Parser.Term.doFor] def expandDoFor : Macro := fun stx => do
   match stx with
-  | `(doFor| for $[$_ : ]? $_:ident in $_ do $_) =>
+  | `(doFor| for $[$_ : ]? $_:ident in $_ $[$_inv:doForInvariant]? do $_) =>
     -- This is the target form of the expander, handled by `elabDoFor` below.
     Macro.throwUnsupported
-  | `(doFor| for%$tk $decls:doForDecl,* do $body) =>
+  | `(doFor| for%$tk $decls:doForDecl,* $[$inv:doForInvariant]? do $body) =>
+    if let some inv := inv then
+      Macro.throwErrorAt inv "The `invariant` clause is only supported on `for x in xs do …` \
+        with a single identifier binder."
     let decls := decls.getElems
     let `(doForDecl| $[$h? : ]? $pattern in $xs) := decls[0]! | Macro.throwUnsupported
     let mut doElems := #[]
@@ -78,8 +82,40 @@ open Lean.Meta
     `(doElem| do $doElems*)
   | _ => Macro.throwUnsupported
 
+/-- Rebuild the already-elaborated loop as a `forInWithInvariant` call carrying the `invariant`
+clause: `ForIn.forInWithInvariant`, or `ForIn'.forInWithInvariant'` for a membership-proof binder
+(`for h : x in xs`). The state tuple's layout is `[return?, mutVars…, unit?]`, so the invariant can
+name the loop's mutable variables directly; the early-return slot becomes a wildcard. -/
+private def mkForInWithInvariant (invClause : Syntax) (h? : Option Syntax)
+    (xs preS body σ : Expr) (loopMutVars : Array MutVar) (returnsEarly : Bool)
+    (mi : MonadInfo) : DoElabM Expr := do
+  let `(doForInvariant| invariant $cursorBinders* => $invBody) := invClause | throwUnsupportedSyntax
+  let hole ← `(_)
+  let mut binders : Array Term := #[]
+  if returnsEarly then binders := binders.push hole
+  for mv in loopMutVars do binders := binders.push ⟨mv.ident.raw⟩
+  if returnsEarly && loopMutVars.isEmpty then binders := binders.push hole
+  let statePat : Term ← match binders with
+    | #[]  => `(_)
+    | #[b] => pure b
+    | _    => `(⟨$binders,*⟩)
+  let stateId := mkIdentFrom invClause (← mkFreshUserName `__s)
+  let invLam ← `(fun $cursorBinders* $stateId:ident =>
+    match $stateId:ident with | $statePat => $invBody)
+  -- The `forInWithInvariant` gadgets live downstream of this module, so they are referenced by an
+  -- unresolved name that resolves in the user's context (which imports the metatheory).
+  let gadget := if h?.isSome then `Std.Internal.Do.ForIn'.forInWithInvariant'
+    else `Std.Internal.Do.ForIn.forInWithInvariant
+  unless (← getEnv).contains gadget do
+    throwErrorAt invClause
+      "the `invariant` clause elaborates to a `vcgen` gadget; add `import Std.Internal.Do` to use it."
+  let call ← `($(mkIdent gadget)
+    $(← Term.exprToSyntax xs) $(← Term.exprToSyntax preS) $(← Term.exprToSyntax body) $invLam)
+  Term.elabTermEnsuringType call (mkApp mi.m σ)
+
 @[builtin_doElem_elab Lean.Parser.Term.doFor] def elabDoFor : DoElab := fun stx dec => do
-  let `(doFor| for%$tk $[$h? : ]? $x:ident in $xs do $body) := stx | throwUnsupportedSyntax
+  let `(doFor| for%$tk $[$h? : ]? $x:ident in $xs $[$inv?:doForInvariant]? do $body) := stx
+    | throwUnsupportedSyntax
   let dec ← dec.ensureUnitAt tk
   checkMutVarsForShadowing #[x]
   let uα ← mkFreshLevelMVar
@@ -176,7 +212,9 @@ open Lean.Meta
     -- Elaborate the loop body, which must have result type `PUnit`, just like the whole `for` loop.
     elabDoSeq body { dec with k := continueCont, kind := .duplicable }
 
-  let forIn := mkApp app body
+  let forIn ← match inv? with
+    | none => pure (mkApp app body)
+    | some invClause => mkForInWithInvariant invClause h? xs preS body σ loopMutVars info.returnsEarly mi
 
   let γ := (← read).doBlockResultType
   let rest ←

src/Lean/Elab/Do/InferControlInfo.lean

@@ -185,7 +185,7 @@ partial def ofElem (stx : DoElem) : TermElabM ControlInfo := do
   | `(doElem| unless $_ do $elseSeq) =>
     ControlInfo.alternative {} <$> ofSeq elseSeq
   -- For/Repeat
-  | `(doElem| for $[$[$_ :]? $_ in $_],* do $bodySeq) =>
+  | `(doElem| for $[$[$_ :]? $_ in $_],* $[$_:doForInvariant]? do $bodySeq) =>
     let info ← ofSeq bodySeq
     return { info with  -- keep only reassigns and returnsEarly
       numRegularExits := 1,

src/Lean/Elab/Do/Legacy.lean

@@ -1563,7 +1563,7 @@ mutual
      `doFor` is of the form
      ```
      def doForDecl := leading_parser termParser >> " in " >> withForbidden "do" termParser
-     def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
+     def doFor := leading_parser "for " >> sepBy1 doForDecl ", " >> optional doForInvariant >> " do " >> doSeq
      ```
   -/
   partial def doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do
@@ -1593,7 +1593,7 @@ mutual
       let y  := doForDecl[1]
       let ys := doForDecl[3]
       let doForDecls := doForDecls.eraseIdx 1
-      let body := doFor[3]
+      let body := doFor[4]
       withFreshMacroScope do
         /- Recall that `@` (explicit) disables `coeAtOutParam`.
            We used `@` at `Stream` functions to make sure `resultIsOutParamSupport` is not used. -/
@@ -1612,7 +1612,7 @@ mutual
       let x         := doForDecls[0]![1]
       withRef x <| checkNotShadowingMutable (← getPatternVarsEx x)
       let xs        := doForDecls[0]![3]
-      let forElems  := getDoSeqElems doFor[3]
+      let forElems  := getDoSeqElems doFor[4]
       let forInBodyCodeBlock ← withFor (doSeqToCode forElems)
       let ⟨uvars, forInBody⟩ ← mkForInBody x forInBodyCodeBlock
       let ctx ← read

src/Lean/Elab/Tactic/Do.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Elab.Tactic.Do.ProofMode
 public import Lean.Elab.Tactic.Do.Syntax
 public import Lean.Elab.Tactic.Do.Attr
+public import Lean.Elab.Tactic.Do.Contract
 public import Lean.Elab.Tactic.Do.LetElim
 public import Lean.Elab.Tactic.Do.Spec
 public import Lean.Elab.Tactic.Do.VCGen

src/Lean/Elab/Tactic/Do/Contract.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Std.Tactic.Do.Syntax
+public import Std.Internal.Do
+public import Lean.Elab.Util
+import Lean.DocString.Extension
+meta import Lean.Parser.Command
+meta import Lean.Parser.Term
+import Init.Syntax
+import Init.Grind.Interactive
+
+/-!
+# `require`/`ensures` contracts on `def`
+
+A definition carrying `require P` / `ensures b => Q` clauses expands to the plain definition plus a
+`vcgen`-proven, `@[spec]`-tagged specification theorem `f.spec`.
+-/
+
+public section
+
+open Lean Lean.Parser.Command Std.Internal.Do Lean.Order
+
+namespace Lean.Elab.Tactic.Do
+
+/-- The identifiers bound by an explicit `(…)` binder, used to apply the definition in its spec. -/
+def contractBinderIdents (binder : Syntax) : Array Ident :=
+  match binder with
+  | `(Lean.Parser.Term.bracketedBinderF| ($ids* $[: $_]? $(_annot?)?)) =>
+      ids.filterMap fun b => if b.raw.isIdent then some ⟨b.raw⟩ else none
+  | _ =>
+      if binder.isIdent then #[⟨binder⟩] else #[]
+
+/-- Expand a `def` carrying `require`/`ensures` clauses into the plain `def` plus a spec theorem
+`@[spec] theorem f.spec : ⦃P⦄ f args ⦃fun b => Q⦄ := by vcgen [f] with finish`. -/
+@[builtin_macro Lean.Parser.Command.declaration]
+def expandDefContract : Macro := fun stx => do
+  let decl := stx[1]
+  unless decl.isOfKind ``Lean.Parser.Command.definition do Macro.throwUnsupported
+  -- `definition = "def "(0) >> declId(1) >> optDeclSig(2) >> (declVal <|> contractDeclVal)(3) >> …`
+  -- `contractDeclVal = optional requireClause(0) >> optional ensuresClause(1) >> declVal(2)`
+  let val := decl[3]
+  unless val.isOfKind ``Lean.Parser.Command.contractDeclVal do Macro.throwUnsupported
+  let requireStx := val[0]
+  let ensuresStx := val[1]
+  -- Replace the contract-carrying value with its inner `declVal` so the `def` elaborates normally.
+  let cleanDeclaration := stx.setArg 1 (decl.setArg 3 val[2])
+  if requireStx.isNone && ensuresStx.isNone then
+    return cleanDeclaration
+  unless (← Macro.hasDecl ``Std.Internal.Do.Triple) do
+    Macro.throwErrorAt (if requireStx.isNone then ensuresStx else requireStx)
+      "`require`/`ensures` contracts elaborate to a `vcgen`-proved specification theorem; \
+add `import Std.Internal.Do` and `import Std.Tactic.Do` to use them."
+  let sig := decl[2]
+  let fId : Ident := ⟨decl[1][0]⟩
+  let specId := mkIdentFrom fId (fId.getId ++ `spec)
+  let sigBinders := sig[0].getArgs
+  let binders : TSyntaxArray [`ident, ``Lean.Parser.Term.hole, ``Lean.Parser.Term.bracketedBinder] :=
+    sigBinders.map (⟨·⟩)
+  let args := sigBinders.flatMap contractBinderIdents
+  let pre : Term ← if requireStx.isNone then `(⊤) else
+    match requireStx[0] with
+    | `(requireClause| require $p) => pure p
+    | _ => Macro.throwUnsupported
+  let post : Term ← if ensuresStx.isNone then `(fun _ => ⊤) else
+    match ensuresStx[0] with
+    | `(ensuresClause| ensures $bs* => $q) => `(fun $bs* => $q)
+    | _ => Macro.throwUnsupported
+  let thm ← `(command|
+    @[spec] theorem $specId $binders* : ⦃ $pre ⦄ $fId $args* ⦃ $post ⦄ := by
+      vcgen [$fId:ident] with finish)
+  return mkNullNode #[cleanDeclaration, thm]
+
+end Lean.Elab.Tactic.Do

src/Lean/Parser/Basic.lean

@@ -1595,6 +1595,30 @@ This parser has the same arity as `p` - it just forwards the results of `p`. -/
     (fun c => if c.forbiddenTks.contains tk then c
               else { c with forbiddenTks := c.forbiddenTks.push tk }) p
 
+/-- Appends the tokens from `tks` missing from `init`; the tokens in `tks` must be distinct. -/
+private def mergeForbiddenTks (init tks : Array Token) : Array Token := Id.run do
+  -- Membership is tested on the prefix seeded from `init`, so the loop does not hold a second
+  -- reference to the original array while pushing.
+  let size := init.size
+  let mut ts := init
+  for tk in tks do
+    unless ts.any (· == tk) (stop := size) do
+      ts := ts.push tk
+  return ts
+
+/-- `withForbiddens(tks, p)` runs `p` with every token in `tks` treated as forbidden, i.e. the
+combined effect of nesting `withForbidden` for each token (see `withForbidden`). The tokens in
+`tks` must be distinct.
+
+This parser has the same arity as `p` - it just forwards the results of `p`. -/
+@[builtin_doc] def withForbiddens (tks : Array Token) (p : Parser)
+    (_h : tks.toList.Nodup := by decide) : Parser :=
+  adaptCacheableContext (fun c =>
+    if c.forbiddenTks.isEmpty then
+      { c with forbiddenTks := tks }
+    else
+      { c with forbiddenTks := mergeForbiddenTks c.forbiddenTks tks }) p
+
 /-- `withoutForbidden(p)` runs `p` disabling the "forbidden token" (see `withForbidden`), if any.
 This is usually used by bracketing constructs like `(...)` because there is no parsing ambiguity
 inside these nested constructs.

src/Lean/Parser/Command.lean

@@ -129,10 +129,20 @@ def declId := leading_parser
 -- @[builtin_doc] -- FIXME: suppress the hover
 def declSig := leading_parser
   many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.typeSpec
+/-- The `require P` precondition clause of a `def` contract. -/
+def requireClause := leading_parser
+  ppIndent (ppSpace >> nonReservedSymbol "require" >> ppSpace >> withForbidden "ensures" termParser)
+/-- The `ensures b => Q` postcondition clause of a `def` contract, binding the result `b`. -/
+def ensuresClause := leading_parser
+  ppIndent (ppSpace >> nonReservedSymbol "ensures" >> Term.basicFun)
+/-- The `: type` of a `def`. It may carry contract clauses, so we forbid `require`/`ensures` in the type. -/
+def defTypeSpec := withForbiddens #["require", "ensures"] Term.typeSpec
 /-- `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` -/
 -- @[builtin_doc] -- FIXME: suppress the hover
 def optDeclSig := leading_parser
-  many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.optType
+  withForbiddens #["require", "ensures"]
+    (many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder))) >>
+  optional defTypeSpec
 /-- Right-hand side of a `:=` in a declaration, a term. -/
 def declBody : Parser :=
   /-
@@ -184,6 +194,12 @@ def whereStructInst  := leading_parser
   -- Issue #753 shows an example that fails to be parsed when we used `Term.whereDecls`.
   withAntiquot (mkAntiquot "declVal" decl_name% (isPseudoKind := true)) <|
     declValSimple <|> declValEqns <|> whereStructInst
+/-- `require P`/`ensures b => Q` contract clauses followed by the value of a `def`. Tried only
+after `declVal` fails, so contract-free definitions parse without probing for the clauses.
+`withoutInfo` avoids collecting `declVal`'s tokens and kinds a second time at startup; they are
+already registered through the `declVal` alternative of `definition`. -/
+def contractDeclVal := leading_parser
+  optional requireClause >> optional ensuresClause >> withoutInfo declVal
 def «abbrev»         := leading_parser
   "abbrev " >> declId >> ppIndent optDeclSig >> declVal
 def derivingClass    := leading_parser
@@ -192,7 +208,8 @@ def derivingClasses  := sepBy1 derivingClass ", "
 def optDefDeriving   :=
   optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance" >> notSymbol "noncomputable") >> derivingClasses)
 def definition     := leading_parser
-  "def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> declVal >> optDefDeriving
+  "def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >>
+  (declVal <|> contractDeclVal) >> optDefDeriving
 def «theorem»        := leading_parser
   "theorem " >> recover declId skipUntilWsOrDelim >> ppIndent declSig >> declVal
 def «opaque»         := leading_parser

src/Lean/Parser/Do.lean

@@ -175,7 +175,15 @@ def doIfCond    :=
 @[builtin_doElem_parser] def doUnless := leading_parser
   "unless " >> withForbidden "do" termParser >> " do " >> doSeq
 def doForDecl := leading_parser
-  optional (atomic (ident >> " : ")) >> termParser >> " in " >> withForbidden "do" termParser
+  optional (atomic (ident >> " : ")) >> termParser >> " in " >>
+    withForbiddens #["do", "invariant"] termParser
+/--
+The optional `invariant cur => e` clause of a `for` loop. The invariant annotates the loop so
+`vcgen` reads it from the program, with `cur` bound to the iteration cursor and mutable variables
+referenced by name.
+-/
+def doForInvariant := leading_parser
+  ppSpace >> nonReservedSymbol "invariant" >> withForbidden "do" basicFun
 /--
 `for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
 `break` and `continue` are supported inside `for` loops.
@@ -184,7 +192,7 @@ until at least one of them is exhausted.
 The types of `e2` etc. must implement the `Std.ToStream` typeclass.
 -/
 @[builtin_doElem_parser] def doFor    := leading_parser
-  "for " >> sepBy1 doForDecl ", " >> " do " >> doSeq
+  "for " >> sepBy1 doForDecl ", " >> optional doForInvariant >> " do " >> doSeq
 
 def dependentParam := leading_parser
   atomic ("(" >> nonReservedSymbol "dependent") >> " := " >>
@@ -334,7 +342,7 @@ They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ...
 @[builtin_term_parser] def termUnless := leading_parser
   "unless " >> withForbidden "do" termParser >> " do " >> doSeq
 @[builtin_term_parser] def termFor := leading_parser
-  "for " >> sepBy1 doForDecl ", " >> " do " >> doSeq
+  "for " >> sepBy1 doForDecl ", " >> optional doForInvariant >> " do " >> doSeq
 @[builtin_term_parser] def termTry    := leading_parser
   "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
 /--

src/Lean/PrettyPrinter/Formatter.lean

@@ -346,6 +346,10 @@ def node.formatter (k : SyntaxNodeKind) (p : Formatter) : Formatter := do
 @[combinator_formatter withFn, expose]
 def withFn.formatter (_ : ParserFn → ParserFn) (p : Formatter) : Formatter := p
 
+@[combinator_formatter withForbiddens, expose]
+def withForbiddens.formatter (tks : Array Token) (p : Formatter) (_h : tks.toList.Nodup) :
+    Formatter := p
+
 @[combinator_formatter trailingNode, expose]
 def trailingNode.formatter (k : SyntaxNodeKind) (_ _ : Nat) (p : Formatter) : Formatter := do
   checkKind k

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -451,6 +451,10 @@ def checkPrec.parenthesizer (prec : Nat) : Parenthesizer :=
 @[combinator_parenthesizer withFn, expose]
 def withFn.parenthesizer (_ : ParserFn → ParserFn) (p : Parenthesizer) : Parenthesizer := p
 
+@[combinator_parenthesizer withForbiddens, expose]
+def withForbiddens.parenthesizer (tks : Array Token) (p : Parenthesizer)
+    (_h : tks.toList.Nodup) : Parenthesizer := p
+
 @[combinator_parenthesizer leadingNode, expose]
 def leadingNode.parenthesizer (k : SyntaxNodeKind) (prec : Nat) (p : Parenthesizer) : Parenthesizer := do
   node.parenthesizer k p

src/Std/Do/Triple/SpecLemmas.lean

@@ -75,6 +75,10 @@ structure Cursor {α : Type u} (l : List α) : Type u where
   /-- Appending the prefix to the suffix yields the original list. -/
   property : «prefix» ++ suffix = l
 
+/-- Transports a cursor along an equality of the list it ranges over. -/
+@[inline] def Cursor.cast {α} {l l' : List α} (c : Cursor l) (h : l = l') : Cursor l' :=
+  ⟨c.prefix, c.suffix, h ▸ c.property⟩
+
 /--
 Creates a cursor at position `n` in the list `l`.
 The prefix contains the first `n` elements, and the suffix contains the remaining elements.

src/Std/Internal/Do.lean

@@ -8,3 +8,4 @@ module
 prelude
 public import Std.Internal.Do.WP
 public import Std.Internal.Do.Triple
+public import Std.Internal.Do.Gadget.ForIn