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

structure Lean.Elab.Tactic.Do.Internal.FrameEntry : Type

A single elaborated frames alternative: its program pattern, the binder name of each pattern variable (none for _, index-aligned with pat.varTypes), the raw frame term (elaborated in the matched goal's context), the source position (a precedence tiebreak among matches, and its index into FrameDB.entries), and whether it has already been applied.

• pat : Meta.Sym.Pattern
• varNames : Array (Option Name)
• frameStx : Syntax
• srcIdx : Nat
• retired : Bool

  Set once this alternative has been applied, so it frames at most one occurrence.

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.instInhabitedFrameEntry : Inhabited FrameEntry

Equations

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

structure Lean.Elab.Tactic.Do.Internal.FrameDB : Type

The frame database: program patterns keyed in a discrimination tree to the srcIdx of the matching alternative, alongside the alternatives themselves in source order. Held in State.frameDB; the discrimination tree is fixed, and only the retired flags of entries change.

• tree : Meta.DiscrTree Nat
• entries : Array FrameEntry

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.instInhabitedFrameDB : Inhabited FrameDB

Equations

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

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

Pre-built backward rules used by solve.

• tripleIntro : Meta.Sym.BackwardRule

  The backward rule for Triple.intro. Unfolds ⦃P⦄ x ⦃Q; E⦄ into P ⊑ wp x Q E.

• stateArgIntro : Meta.Sym.BackwardRule

  The backward rule for Lean.Order.le_of_forall_le. Peels one excess state argument from a function-lattice entailment.

• propPreIntro : Meta.Sym.BackwardRule

  The backward rule for Lean.Order.le_of_imp_top_le. Introduces a bare pure precondition on the Prop lattice.

• ofPropPreIntro : Meta.Sym.BackwardRule

  The backward rule for Lean.Order.ofProp_le. Introduces an embedded pure precondition ⌜p⌝ on any complete lattice.

• truePreIntro : Meta.Sym.BackwardRule

  The backward rule for Lean.Order.true_le_of_top_le. Replaces a True precondition with ⊤ on the Prop lattice.

• elimPre : Meta.Sym.BackwardRule

  The backward rule for Lean.Order.top_le_prop. Strips a (⊤ : Prop) ⊑ · wrapper from a VC before it is emitted.

• andIntro : Meta.Sym.BackwardRule

  The backward rule for And.intro.

• refl : Meta.Sym.BackwardRule

  The backward rule for Lean.Order.PartialOrder.rel_refl. Closes a reflexive entailment pre ⊑ pre.

• meetTop : Meta.Sym.BackwardRule

  The backward rule for meet_top_le_of_le. Cancels a redundant ⊓ ⊤ on the left of an entailment, turning P ⊓ ⊤ ⊑ Q into P ⊑ Q.

def Lean.Elab.Tactic.Do.Internal.VCGen.mkBackwardRules : MetaM BackwardRules

Build the backward rules used by solve from their underlying lemmas.

Equations

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

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

• backwardRules : BackwardRules

  Pre-built backward rules used by solve.

• frameProcs : FrameProcs

  The @[frameproc] registry snapshot taken at frontend init. solve selects a procedure per program node by the node's monad.

• latticeOps : Std.HashMap Name LatticeOp

  Lattice splits keyed by operator head, merging the built-in connectives with the registered frame operators. Built once at frontend init; splitLatticeOp? looks a head up here.

• 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 solveTrivialConjuncts 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), a program with no matching spec raises a hard error. When false, the goal is emitted as an unsolved VC for the user to discharge — useful with vcgen [-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 vcgen.

• 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 Meta.Sym.Pattern

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

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

• specs : SpecAttr.SpecTheorems

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

• jps : FVarIdMap JumpSiteInfo

  __do_jp fvars currently in scope.

• lastLiftedPre? : Option FVarId

  The most recently lifted pure precondition. tryLiftedHyp closes handoff VCs against it without walking the local context.

• nextDeclIdx : Nat

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

@[instance_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 × Meta.Sym.ExprPtr × Nat) Meta.Sym.BackwardRule

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

  The instance is keyed by ExprPtr, so lookups compare it by pointer rather than structurally. This is sound because the instance is a subterm of the hash-consed goal target.

• splitBackwardRuleCache : Std.HashMap (Name × Meta.Sym.ExprPtr × 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.

  The instance is keyed by ExprPtr, so lookups compare it by pointer rather than structurally. This is sound because the instance is a subterm of the hash-consed goal target.

• latticeBackwardRuleCache : Std.HashMap (Meta.Sym.ExprPtr × Nat) Meta.Sym.BackwardRule

  A cache mapping lattice connectives to their backward rule to apply, keyed by the head … cₙ prefix of constant arguments the rule bakes in verbatim and the total argument count that fixes the schematic operand and state count.

  The prefix is keyed by ExprPtr, so lookups compare it by pointer rather than structurally. This is sound because it is a subterm of the hash-consed goal target.

• frameBackwardRuleCache : Std.HashMap (Meta.Sym.ExprPtr × Nat) Meta.Sym.BackwardRule

  Caches the F-abstract upper-adjoint frame rule (op_wp_upperAdjoint_le_wp), keyed by the WPMonad instance and the number of excess state arguments.

• frameDB : FrameDB

  The frame database from the frames clause.

• 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, lastLiftedPre? := s.lastLiftedPre?, 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.SpecTheorem) : Scope

Equations

• s.insertSpec thm = { specs := s.specs.insert thm, jps := s.jps, lastLiftedPre? := s.lastLiftedPre?, nextDeclIdx := s.nextDeclIdx }

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.