The VCGenM monad: its read-only Context (a fixed bundle of pre-built BackwardRules + user-customisable simp methods) and its mutable State (rule caches, accumulated invariants/VCs, simp cache).

inductive Lean.Elab.Tactic.Do.Internal.UntilPatternThunk : Type

A lazily elaborated until pattern, stored behind an IO.Ref so the first force caches its result. The pattern is elaborated against the monad of the first program encountered in solve (supplied as the expected type).

• deferred (elabFn : Expr → MetaM Meta.Sym.Pattern) : UntilPatternThunk

  Not yet elaborated; elabFn m elaborates the pattern against the program monad m.

• elaborated (pat : Meta.Sym.Pattern) : UntilPatternThunk

  Already elaborated and cached.

def Lean.Elab.Tactic.Do.Internal.UntilPatternThunk.force (ref : IO.Ref UntilPatternThunk) (m : Expr) : MetaM Meta.Sym.Pattern

Force the thunk in ref against the program monad m, elaborating, tracing, and caching the pattern on first use; later calls return the cached pattern.

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.Tactic.Do.Internal.VCGen.Context : Type

• entailsConsIntroRule : Meta.Sym.BackwardRule

  The backward rule for SPred.entails_cons_intro.

• entailsNilPureIntroRule : Meta.Sym.BackwardRule

  The backward rule for SPred.entails_nil_pure_intro. Preferred over entails_nil_intro when the LHS is ⌜φ⌝, as it unwraps .down on the pure assertion.

• entailsNilIntroRule : Meta.Sym.BackwardRule

  The backward rule for SPred.entails_nil_intro. Fallback when LHS is not ⌜φ⌝.

• applyPureConsEntailsLRule : Meta.Sym.BackwardRule

  The backward rule for SPred.apply_pure_cons_entails_l. Peels a state arg from SPred.pure (σ::σs) φ s on the LHS of an entailment.

• applyPureConsEntailsRRule : Meta.Sym.BackwardRule

  The backward rule for SPred.apply_pure_cons_entails_r. Peels a state arg from SPred.pure (σ::σs) φ s on the RHS of an entailment.

• downPureIntroRule : Meta.Sym.BackwardRule

  The backward rule for SPred.down_pure_intro. Reduces a target of the form (SPred.pure [] φ).down to φ.

• pureElimRule : Meta.Sym.BackwardRule

  The backward rule for SPred.pure_elim'.

• pureIntroRule : Meta.Sym.BackwardRule

  The backward rule for SPred.pure_intro.

• postCondEntailsRflRule : Meta.Sym.BackwardRule

  The backward rule for PostCond.entails.rfl. Tried first to close by reflexivity.

• postCondEntailsMkRule : Meta.Sym.BackwardRule

  The backward rule for PostCond.entails.mk.

• exceptCondsEntailsRflRule : Meta.Sym.BackwardRule

  The backward rule for ExceptConds.entails.rfl.

• exceptCondsEntailsPureRule : Meta.Sym.BackwardRule

  The backward rule for ExceptConds.entails.pure. Closes the exception side for pure PostShapes, where ExceptConds.entails reduces to True.

• exceptCondsEntailsFalseRule : Meta.Sym.BackwardRule

  The backward rule for ExceptConds.entails_false.

• exceptCondsEntailsTrueRule : Meta.Sym.BackwardRule

  The backward rule for ExceptConds.entails_true.

• tripleOfEntailsWPRule : Meta.Sym.BackwardRule

  The backward rule for Triple.of_entails_wp.

• andIntroRule : Meta.Sym.BackwardRule

  The backward rule for And.intro.

• hypSimpMethods : Option Meta.Sym.Simp.Methods

  User-customizable simp methods used to pre-simplify hypotheses.

• trivial : Bool

  The trivial config option: when true (default), Driver.emitVC runs repeatAndRfl to collapse trivial And.intro chains; when false, the goal is emitted as-is.

• useJP : Bool

  The jp config option: when true, tryLetIntro recognises __do_jp lets whose body is a splitter and sets up shared-continuation handling instead of zeta-unfolding. When false (default, matching original mvcgen), every call site of the JP zeta-unfolds, leading to exponential blow-up on nested splits.

• errorOnMissingSpec : Bool

  The errorOnMissingSpec config option: when true (default), Driver.work raises a hard error when solve returns .noSpecFoundForProgram. When false, the goal is emitted as an unsolved VC for the user to discharge — useful with mvcgen' [-some_spec] patterns where the user knows the spec is intentionally removed and wants to handle the residual goal by hand.

• debug : Bool

  The debug config option: when true, tryApplyRule retries failed BackwardRule.apply calls after unfoldReducible and reports an error when the retry succeeds, pinpointing missing normalization steps in mvcgen'.

• internalize : Bool

  The internalize config option: when true (default), emitVC and the multi-subgoal fork in Driver.work call Grind.processHypotheses. The tactic-mode entry point disables this when there is no with clause.

• invariantAlts : Std.HashMap Nat Syntax

  Pre-parsed invariants/invariants? alternatives, indexed by 1-based invariant number. Bullet form maps positions to entries (bullet n+1 → alt); labelled form maps the parsed inv<n> numbers (out-of-order labels are supported). Empty when no invariants clause is provided or in invariants? (suggest) mode (handled separately).

• untilPat? : Option (IO.Ref UntilPatternThunk)

  The until pattern: when some ref, VC generation stops and emits the current goal as a VC once the program in wp⟦e⟧ matches the (lazily elaborated) pattern, before applying a spec.

structure Lean.Elab.Tactic.Do.Internal.VCGen.Scope : Type

• specs : SpecAttr.SpecTheoremsNew

  Spec database in scope: globals plus locals from in-scope hypotheses.

• jps : FVarIdMap JumpSiteInfo

  __do_jp fvars currently in scope.

• nextDeclIdx : Nat

  Index of the next local declaration to consider for local specs.

@[implicit_reducible]

instance Lean.Elab.Tactic.Do.Internal.VCGen.instInhabitedScope : Inhabited Scope

Equations

• Lean.Elab.Tactic.Do.Internal.VCGen.instInhabitedScope = { default := Lean.Elab.Tactic.Do.Internal.VCGen.instInhabitedScope.default }

structure Lean.Elab.Tactic.Do.Internal.VCGen.State : Type

• specBackwardRuleCache : Std.HashMap (Name × Expr × Nat) Meta.Sym.BackwardRule

  A cache mapping registered SpecThms to their backward rule to apply. The particular rule depends on the theorem name, the monad and the number of excess state arguments that the weakest precondition target is applied to.

• splitBackwardRuleCache : Std.HashMap (Name × Expr × Nat) Meta.Sym.BackwardRule

  A cache mapping matchers to their splitting backward rule to apply. The particular rule depends on the matcher name, the monad and the number of excess state arguments that the weakest precondition target is applied to.

• invariants : Array MVarId

  Holes of type Invariant that have been generated so far.

• vcs : Array Meta.Grind.Goal

  The verification conditions that have been generated so far. Each entry shares the parent Grind.Goal's state.

• simpState : Meta.Sym.Simp.State

  Persistent cache for the Sym.Simp simplifier used to pre-simplify hypotheses before grind internalization. Threading this cache across VCGen iterations avoids re-simplifying shared subexpressions (e.g., s + 1 + 1 + ... chains).

• fuel : Fuel

  Remaining VC-generation steps. Initialized from Context.config.stepLimit (or .unlimited when no limit is set). Decremented at each successful program-shape step (tryLetHoist, trySplit, tryFvarZeta, applySpec). When exhausted, solve short-circuits and emits the current goal as a VC.

• inlineHandledInvariants : Std.HashSet Nat

  Set of invariant numbers that have been inline-elaborated by Driver.emitVC via tryInlineInvariant. The post-hoc invariant elaboration in Frontend consults this to know which user-provided alts have already been consumed (so it doesn't warn about them).

@[reducible, inline]

abbrev Lean.Elab.Tactic.Do.Internal.VCGenM (α : Type) : Type

Equations

• Lean.Elab.Tactic.Do.Internal.VCGenM = ReaderT Lean.Elab.Tactic.Do.Internal.VCGen.Context (StateRefT' IO.RealWorld Lean.Elab.Tactic.Do.Internal.VCGen.State Lean.Meta.Grind.GrindM)

def Lean.Elab.Tactic.Do.Internal.VCGen.Scope.registerJP (s : Scope) (fv : FVarId) (info : JumpSiteInfo) : Scope

Equations

• s.registerJP fv info = { specs := s.specs, jps := s.jps.insert fv info, nextDeclIdx := s.nextDeclIdx }

def Lean.Elab.Tactic.Do.Internal.VCGen.Scope.knownJP? (s : Scope) (fv : FVarId) : Option JumpSiteInfo

Equations

• s.knownJP? fv = Std.TreeMap.get? s.jps fv

def Lean.Elab.Tactic.Do.Internal.VCGen.Scope.insertSpec (s : Scope) (thm : SpecAttr.SpecTheoremNew) : Scope

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.Scope.collectLocalSpecs (scope : Scope) (goal : MVarId) : VCGenM Scope

Walk goal's local context from scope.nextDeclIdx onward, registering any spec-shaped hypotheses as local specs. Advances nextDeclIdx to the current context size so siblings share work.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.Internal.VCGen.outOfFuel : VCGenM Bool

True iff fuel has been exhausted (Fuel.limited 0).

Equations

• Lean.Elab.Tactic.Do.Internal.VCGen.outOfFuel = do let __do_lift ← get pure (match __do_lift.fuel with | Lean.Elab.Tactic.Do.Fuel.limited 0 => true | x => false)

def Lean.Elab.Tactic.Do.Internal.VCGen.burnOne : VCGenM Unit

Decrement remaining fuel by one. No-op when fuel is .unlimited or already at zero.

Equations

• One or more equations did not get rendered due to their size.