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

inductive Lean.Elab.Tactic.Do.Internal.VCGen.PreTac : Type

Pre-tactic to try on each emitted VC before returning it to the user.

• none : PreTac

  No pre-tactic; VCs are returned as-is.

• grind (silent : Bool := false) : PreTac

  Use grind with the given hypothesis simplification methods.

• tactic (tac : Syntax) : PreTac

  Use a user-provided tactic syntax.

def Lean.Elab.Tactic.Do.Internal.VCGen.PreTac.isGrind : PreTac → Bool

Equations

• (Lean.Elab.Tactic.Do.Internal.VCGen.PreTac.grind silent).isGrind = true
• x✝.isGrind = false

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

• specThms : SpecAttr.SpecTheoremsNew
• 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.

• preTac : PreTac

  Pre-tactic to try on each emitted VC.

• 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'.

• 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).

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).

• jps : FVarIdMap JumpSiteInfo

  Map from __do_jp fvar id to its JumpSiteInfo. Populated when tryLetIntro registers a join point (Context.useJP = true); consulted by tryFvarZeta / tryJumpSite to short-circuit zeta-unfolding at call sites.

• 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).

• preTacFailed : Bool

  Set when a pre-tactic failed on some VC; elabMVCGen' throws if true.

@[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.registerJP (fv : FVarId) (info : JumpSiteInfo) : VCGenM Unit

Register a join-point JumpSiteInfo for the given fvar. Called when a let __do_jp := … is detected as a shared continuation.

Equations

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

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

Look up a previously-registered join point by fvar id.

Equations

• Lean.Elab.Tactic.Do.Internal.VCGen.knownJP? fv = do let __do_lift ← get pure (Std.TreeMap.get? __do_lift.jps fv)

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.