The metadata a frame inference procedure operates on: the wp application metadata WPApp and the FrameProc bundling an inference procedure with its frame operator. @[frameproc] registration lives in FrameProcAttr.

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

How the goal precondition frames through the frame operator: vcgen applies the frame rule with the frame, discharging the split VC pre ⊑ (op frame residualPre) s⃗ with proof and leaving proof's subgoals. residualPre is the solver-owned metavariable for the residual precondition, which the solver fills after the frame rule applies.

Build a FrameSplit with FrameSplit.withDischargedSplitVC (proof supplied) or FrameSplit.withDeferredSplitVC (split VC left as one subgoal).

• frame : Expr

  The framed resource.

• residualPre : MVarId

  The residual precondition the program runs against once frame is framed off: in the split VC pre ⊑ op frame residualPre, the complement of frame in pre. Allocated by mkResidualPre, left unassigned by the procedure; applyFrameRule fills it once the frame rule fixes it.

• splitVCProof : Expr

  A proof of the split VC pre ⊑ (op frame residualPre) s⃗.

• subgoals : List MVarId

  The unassigned subgoals of splitVCProof.

def Lean.Elab.Tactic.Do.Internal.VCGen.FrameSplit.instantiateMVarsS (split : FrameSplit) : Meta.Sym.SymM FrameSplit

Instantiate a FrameSplit's data against the current metavariable context (and reshare).

Equations

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

structure Lean.Elab.Tactic.Do.Internal.VCGen.FrameInferenceInfoextends Lean.Elab.Tactic.Do.Internal.VCGen.WPApp : Type

The inputs to a FrameInferenceProc: the goal, how the frame was requested, and the spec being applied. Extends the program's wp metadata (WPApp), so Pred, excessArgs, etc. are available directly.

• head : Expr
• args : Array Expr
• excessArgs : Array Expr
• goal : MVarId

  The entailment goal pre ⊑ wp … the frame rule or spec applies to.

• providedFrame? : Option Expr

  The frame pinned by a matching frames clause, or none to infer the frame, e.g. from the precondition or from specPre?.

• spec? : Option Name

  Declaration name of the @[spec] theorem being applied, none for a local or syntactic spec. A procedure can key a footprint off it, e.g. through an attribute keyed by spec name.

• specRule : Meta.Sym.BackwardRule

  The backward rule of the @[spec] theorem being applied.

• mkOpApp : Meta.Sym.SymM Expr

  Builds the frame operator op : R → Pred → Pred, hash-consed; the selected procedure's FrameProc.mkOpAppM.

def Lean.Elab.Tactic.Do.Internal.VCGen.FrameInferenceInfo.le (i : FrameInferenceInfo) : Meta.Sym.SymM Expr

The goal's entailment relation PartialOrder.rel α inst (carrier and order instance applied); apply it to two operands to build an entailment in the goal's order.

Equations

• i.le = do let __do_lift ← liftM i.goal.getType pure (__do_lift.stripArgsN 2)

def Lean.Elab.Tactic.Do.Internal.VCGen.FrameInferenceInfo.pre (i : FrameInferenceInfo) : Meta.Sym.SymM Expr

What holds going in: the left-hand side of the goal entailment pre ⊑ wp ….

Equations

• i.pre = do let __do_lift ← liftM i.goal.getType pure __do_lift.appFn!.appArg!

def Lean.Elab.Tactic.Do.Internal.VCGen.FrameInferenceInfo.mkResidualPre (i : FrameInferenceInfo) : Meta.Sym.SymM MVarId

A fresh residual-precondition metavariable for a FrameSplit: synthetic-opaque; the procedure builds the split VC against it and leaves it unassigned.

Equations

• i.mkResidualPre = do let __do_lift ← liftM (Lean.Meta.mkFreshExprSyntheticOpaqueMVar i.Pred) pure __do_lift.mvarId!

def Lean.Elab.Tactic.Do.Internal.VCGen.FrameInferenceInfo.specPre? (i : FrameInferenceInfo) : Meta.Sym.SymM (Option Expr)

The spec precondition instantiated at the call site, read off a speculative application of specRule to goal that is rolled back: the precondition VC's metavariables are frozen into a telescope and reopened fresh in the restored context, so they outlive the rollback. none when the rule does not apply or leaves no precondition VC.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.FrameInferenceInfo.mkSplitVCS (i : FrameInferenceInfo) (frame footprint : Expr) : Meta.Sym.SymM Expr

The split VC proposition pre ⊑ (op frame footprint) s⃗: the frame operator applied to frame and footprint, then to the excess state arguments, entailed by pre in the goal's order. frame and footprint must be hash-consed (shareCommon); the result is.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.FrameSplit.withDeferredSplitVC (i : FrameInferenceInfo) (frame : Expr) : Meta.Sym.SymM FrameSplit

A FrameSplit framing frame whose split VC pre ⊑ (op frame residualPre) s⃗ is deferred as a fresh subgoal for the built-in lattice (meet) decomposition to split.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.FrameSplit.withDischargedSplitVC (frame : Expr) (residualPre : MVarId) (splitVCProof : Expr) (subgoals : List MVarId := []) : FrameSplit

A FrameSplit framing frame, discharging the split VC pre ⊑ (op frame residualPre) s⃗ with splitVCProof and leaving its subgoals.

Equations

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

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

A frame backward rule together with the positions of its assignable subgoals in the applied rule's goal list: the schematic frame and the split VC pre ⊑ (op frame W) s⃗, where W is the weakest footprint baked into the rule. The positions are fixed at rule construction, so applying a FrameSplit assigns by index.

• rule : Meta.Sym.BackwardRule

  The backward rule concluding pre ⊑ wp x Q E s⃗.

• splitVCIdx : Nat

  Position of the split VC pre ⊑ (op frame W) s⃗.

• frameIdx : Nat

  Position of the schematic frame (of type R).

@[reducible, inline]

abbrev Lean.Elab.Tactic.Do.Internal.VCGen.FrameInferenceProc : Type

A frame inference procedure: from a FrameInferenceInfo (whose providedFrame? carries the frame of a matching frames clause, if any), optionally produce a FrameSplit; none leaves the spec to apply directly.

The procedure produces the frame and a proof of the split VC pre ⊑ (op frame residualPre) s⃗; it must not assign residualPre, which the solver fills with the weakest footprint after the frame rule applies. Build the result with FrameSplit.withDischargedSplitVC (proof supplied) or FrameSplit.withDeferredSplitVC (split VC left as a subgoal).

Equations

• Lean.Elab.Tactic.Do.Internal.VCGen.FrameInferenceProc = (Lean.Elab.Tactic.Do.Internal.VCGen.FrameInferenceInfo → Lean.Meta.Sym.SymM (Option Lean.Elab.Tactic.Do.Internal.VCGen.FrameSplit))

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

How to decompose a lattice operator head … s⃗ on the RHS of an entailment: the distribution and unfolding rewrites that saturate it, and the terminal ⊑-introduction terminals that close the reduced form. head keys the split in the latticeOps table.

• head : Name

  Head constant of the operator this split decomposes. Keys the latticeOps table.

• numConst : Nat

  The number of leading arguments held constant during rule construction: the operator's carrier type and its typeclass instances. The operands and excess state arguments after them become the rule's schematic parameters. 2 for a connective over a CompleteLattice carrier; 0 for a monomorphic operator.

• rewrites : Array Name

  Distribution and unfolding equalities that saturate the operator applied to state arguments.

• terminal? : Option Name

  The operator's terminal ⊑-introduction rule, or none when it saturates to another operator's terminal.

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

A frame inference procedure registered with @[frameproc], together with its frame operator. The vcgen frontend selects the one whose prog matches the goal program's monad.

• prog : Name

  Head constant of the program type (the monad) whose wp this procedure frames. Keys the procedure in the byProg index; vcgen consults it for a program with that head.

• opHead : Name

  Head constant of the frame operator, locating the split VC in the frame rule.

• mkOpAppM : WPApp → MetaM Expr

  Builds the frame operator (head constant opHead) applied to the goal's assertion type.

• mkResourceTy : WPApp → MetaM Expr

  The resource type R of the operator op : R → Pred → Pred, i.e. the domain of mkOpAppM's result. Provided directly so vcgen reads it without building the operator, which it does only when a frame actually applies.

• proc : FrameInferenceProc

  The frame inference metaprogram.

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

The registered frame inference procedures, indexed by the program monad's head constant (selected per node in solve).

• byProg : Std.HashMap Name FrameProc

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.instInhabitedFrameProcs : Inhabited VCGen.FrameProcs

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.FrameProcs.insert (s : FrameProcs) (fp : FrameProc) : FrameProcs

Equations

• s.insert fp = { byProg := s.byProg.insert fp.prog fp }

def Lean.Elab.Tactic.Do.Internal.VCGen.defaultFrameInferenceProc : FrameInferenceProc

Default frame inference procedure, agnostic of the frame operator: frame the resource pinned by a frames clause, with the weakest footprint.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.meetFrameProc : FrameProc

The default frame operator: lattice meet pre ⊓ frame, the Hoare frame every complete lattice carries. Framed only through an explicit frames clause; used for a monad with no registered @[frameproc].

Equations

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