Backward application for VCSpec entries

Shared native application helpers for @[vcspec] entries.

structure OracleComp.ProgramLogic.VCSpecBackwardRule : Type

Cached VCVio wrapper around Lean's symbolic backward rule. The source entry is kept for diagnostics and replay text.

• source : VCSpecEntry
• rawGoal : Bool
• proof : Lean.Meta.AbstractMVarsResult
• declName : Lean.Name
• rule : Lean.Meta.Sym.BackwardRule

opaque OracleComp.ProgramLogic.vcSpecBackwardRuleCache : IO.Ref (Std.HashMap OracleComp.ProgramLogic.VCSpecBackwardRuleCacheKey✝ VCSpecBackwardRule)

def OracleComp.ProgramLogic.VCSpecEntry.hasProofPremise (entry : VCSpecEntry) : Lean.MetaM Bool

Whether applying this registered theorem is expected to leave an ordinary proof obligation, such as an auxiliary premise. Instance arguments and data arguments are ignored.

def OracleComp.ProgramLogic.VCSpecEntry.tryApplyRawUnaryConsequence (entry : VCSpecEntry) (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

Apply a raw unary @[vcspec] theorem under consequence, constructing the proof directly against the current target. This is the unary analogue of the direct raw relational path and covers raw Std.Do'.wp goals with epost⟨⟩ without going through theorem-syntax replay.

def OracleComp.ProgramLogic.runVCSpecEntryRawUnaryConsequence (entry : VCSpecEntry) : Lean.Elab.Tactic.TacticM Bool

Apply a raw unary consequence proof for a @[vcspec] entry to the current main goal, preserving tail goals.

def OracleComp.ProgramLogic.VCSpecEntry.tryApplyRawRelConsequence (entry : VCSpecEntry) (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

Apply a raw relational @[vcspec] theorem under consequence, constructing the consequence proof against the current target directly. This avoids asking elaboration to infer the target rwp shape from an underscore-heavy refine term, which is expensive for premised raw relational rules.

def OracleComp.ProgramLogic.runVCSpecEntryRawRelConsequence (entry : VCSpecEntry) : Lean.Elab.Tactic.TacticM Bool

Apply a raw relational consequence proof for a @[vcspec] entry to the current main goal, preserving tail goals.

def OracleComp.ProgramLogic.VCSpecEntry.tryApplyCachedBackward (entry : VCSpecEntry) (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

Try to apply a cached symbolic backward rule for a registered @[vcspec] entry. Unary and relational rules are normalized through raw wp / rwp sources when their theorem statements expose those forms definitionally.

def OracleComp.ProgramLogic.VCSpecEntry.tryApplyBackward (entry : VCSpecEntry) (mvarId : Lean.MVarId) : Lean.MetaM (Option (List Lean.MVarId))

Try to apply a registered @[vcspec] entry directly to a goal metavariable.

This instantiates the stored SpecProof, bridges Triple proofs when the goal is already in raw weakest-precondition form, applies with fresh metavariables, and returns the generated subgoals. Goal-specific close passes remain in the unary and relational planners because they know which leaf rules are cheap and valid for their logic.

def OracleComp.ProgramLogic.runVCSpecEntryBackward (entry : VCSpecEntry) : Lean.Elab.Tactic.TacticM Bool

Apply a @[vcspec] entry to the current main goal, preserving the tail goals.

This helper performs only the theorem application. Callers should run their existing cheap close pass afterwards.

def OracleComp.ProgramLogic.runVCSpecEntryCachedBackward (entry : VCSpecEntry) : Lean.Elab.Tactic.TacticM Bool

Apply a cached symbolic backward rule for a @[vcspec] entry to the current main goal, preserving the tail goals.

VCSpec simp dispatch

def OracleComp.ProgramLogic.runVCSpecSimp : Lean.Elab.Tactic.TacticM Unit

Run the cached vcspec_simp simp set on the main goal target, swallowing errors and unchanged-goal failures.

This is the single replacement for the previous open-coded simp only [...] blocks that peeled transformer wp layers (apply_wp, *.run, lifts, Std.Do'.EPost.cons.push*, MAlgOrdered.wp_*, the Loom.wp_eq_mAlgOrdered_wp bridges, and the assorted monad/algebra rewrites). Tag a new normalization lemma with @[vcspec_simp] (or rely on the @[vcspec] fallback) instead of appending it to a tactic-local simp list.