Unary VCGen Internals

Implementation details for the unary VCGen planner and close passes.

def OracleComp.ProgramLogic.TacticInternals.Unary.throwWpStepError : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.TacticInternals.Unary.runHoareStepRuleUsing (cut : Lean.TSyntax `term) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.tryCloseSpecGoalImmediate : Lean.Elab.Tactic.TacticM Bool

Try to close the current goal using only immediate local information. This is intentionally cheap: it is used while speculating on triple_bind, so it must not launch expensive proof search on goals with unresolved cut metavariables.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryCloseSpecGoalSearch : Lean.Elab.Tactic.TacticM Bool

Try bounded local proof search on a closed goal. We only invoke solve_by_elim once the target has no unresolved expression metavariables; this avoids pathological search on speculative intermediate cuts introduced by triple_bind.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenStepWithTheorem (thm : Lean.TSyntax `term) (requireClosed : Bool := false) : Lean.Elab.Tactic.TacticM Bool

Apply an explicit unary theorem/assumption step and try to close any easy side goals. When requireClosed is true, the step only succeeds if no goals remain afterwards.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryCloseSpecGoal : Lean.Elab.Tactic.TacticM Bool

Try to close the current goal (typically a Triple subgoal) using direct hypotheses, canonical leaf rules, or bounded local consequence search.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryCloseSpecGoalFinal : Lean.Elab.Tactic.TacticM Bool

Finish-only closure step: includes the support-sensitive leaf rules that are too expensive for the default vcstep hot path.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenClosePass : Lean.Elab.Tactic.TacticM Bool

Run one bounded finish/closure pass across all current goals.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryMatchDecomp (comp : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Try to decompose a match expression in the computation by case-splitting on its discriminant(s). Only fires when the computation is a compiled matcher (detected via matchMatcherApp?). Delegates to split which handles the actual case analysis.

def OracleComp.ProgramLogic.TacticInternals.Unary.isConstantLambda (e : Lean.Expr) : Bool

Check if an expression is a lambda whose body does not use the bound variable (i.e. a constant function fun _ => c).

def OracleComp.ProgramLogic.TacticInternals.Unary.tryBindImmediate (comp : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Try the strongest automatic bind step: triple_bind plus immediate closure of the spec side-goal.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryLoopInvariantRuleAuto (comp : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Try only the automatic loop-invariant rules, without the structural fallback rules.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryLoopFallback (comp : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Try only the structural loop fallback rules (succ / cons) after invariant search.

def OracleComp.ProgramLogic.TacticInternals.Unary.runLoopInvExplicit (inv : Lean.TSyntax `term) : Lean.Elab.Tactic.TacticM Bool

Apply a loop invariant rule with an explicitly provided invariant.

def OracleComp.ProgramLogic.TacticInternals.Unary.findHoareCutHintCandidates : Lean.Elab.Tactic.TacticM (Array Lean.Name)

Find the local hypotheses that work as explicit bind cuts.

def OracleComp.ProgramLogic.TacticInternals.Unary.findUniqueHoareCutHint? : Lean.Elab.Tactic.TacticM (Option Lean.Name)

Find the unique local hypothesis that works as an explicit bind cut. Returns none if there are 0 or ≥ 2 viable candidates.

def OracleComp.ProgramLogic.TacticInternals.Unary.findLoopInvHintCandidates : Lean.Elab.Tactic.TacticM (Array Lean.Name)

Find the local hypotheses that work as explicit loop invariants.

def OracleComp.ProgramLogic.TacticInternals.Unary.findUniqueLoopInvHint? : Lean.Elab.Tactic.TacticM (Option Lean.Name)

Find the unique local hypothesis that works as an explicit loop invariant. Returns none if there are 0 or ≥ 2 viable candidates.

def OracleComp.ProgramLogic.TacticInternals.Unary.findRegisteredVCGenRuleCandidates : Lean.Elab.Tactic.TacticM (Array CompiledUnaryVCSpecRule)

Find the registered compiled rules whose bounded application makes progress.

def OracleComp.ProgramLogic.TacticInternals.Unary.findRegisteredVCGenRule? : Lean.Elab.Tactic.TacticM (Option CompiledUnaryVCSpecRule)

Find the first registered compiled rule whose bounded application makes progress.

def OracleComp.ProgramLogic.TacticInternals.Unary.throwVCGenStepError : Lean.Elab.Tactic.TacticM Unit

inductive OracleComp.ProgramLogic.TacticInternals.Unary.ProbEqAction : Type

Try to close or rewrite a Pr[ ...] = Pr[ ...] goal by swapping adjacent independent binds. Handles 0–2 layers of tsum peeling.

• swap : ProbEqAction
• congr : ProbEqAction
• congrNoSupport : ProbEqAction
• rewrite : ProbEqAction
• rewriteUnder (depth : ℕ) : ProbEqAction

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqSwap : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqCongrNoSupportWithNames (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqCongrNoSupport : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqCongrWithNames (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM Bool

Try to decompose a Pr[ ... | mx >>= f₁] = Pr[ ... | mx >>= f₂] goal by congruence, then auto-intro the bound variable and support hypothesis.

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqCongr : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqCongrChainWithNames (supportSensitive : Bool) (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM Bool

partial def OracleComp.ProgramLogic.TacticInternals.Unary.mkProbSwapUnderProof (depth : ℕ) : Lean.Elab.Tactic.TacticM (Lean.TSyntax `term)

Build a theorem that swaps adjacent binds under depth shared prefixes.

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqRewrite : Lean.Elab.Tactic.TacticM Bool

Try to rewrite one top-level bind-swap without closing the goal.

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqRewriteUnder (depth : ℕ) : Lean.Elab.Tactic.TacticM Bool

Try to rewrite one bind-swap under depth shared prefixes on either side.

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqAction : ProbEqAction → Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.tryProbEqActions (steps : List ProbEqAction) : Lean.Elab.Tactic.TacticM Bool

Try a small backtracking-free sequence of probability-equality steps.

def OracleComp.ProgramLogic.TacticInternals.Unary.probEqActionPlans : List (List ProbEqAction)

def OracleComp.ProgramLogic.TacticInternals.Unary.tryProbEqPlans (plans : List (List ProbEqAction)) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbOutputEqRelBridge : Lean.Elab.Tactic.TacticM Bool

Try to handle a Pr[ ...] = Pr[ ...] equality goal by swap, congr, or swap+congr. Also tries a fallback bridge from exact probOutput equalities into relational VCGen.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryProbEqGoal : Lean.Elab.Tactic.TacticM Bool

Try to handle a Pr[ ...] = Pr[ ...] equality goal by swap, congr, or swap+congr.

def OracleComp.ProgramLogic.TacticInternals.Unary.throwVCGenStepRwError (depth : ℕ) : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.TacticInternals.Unary.throwVCGenStepRwCongrError (supportSensitive : Bool) : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.TacticInternals.Unary.tryLowerProbGoal : Lean.Elab.Tactic.TacticM Bool

Try to lower a probability goal into a Triple, wp, or probability-equality goal.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryRawWpStructuralStep : Lean.Elab.Tactic.TacticM Bool

Continue structural stepping on a raw wp goal after probability lowering or explicit wp-level work. This stays deliberately smaller than the Triple path.

def OracleComp.ProgramLogic.TacticInternals.Unary.trySupportCutBind (comp : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Try to synthesize a support-based intermediate postcondition for a bind step. When the computation is oa >>= f and no explicit spec is available, tries applying triple_bind with an inferred cut and closing the spec subgoal via triple_support, which unifies the cut to fun x => ⌜x ∈ support oa⌝.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenStructuralCore : Lean.Elab.Tactic.TacticM Bool

Structural/default unary VCGen step, excluding explicit cut/invariant/theorem-driven fallbacks and the final close/search phase.

def OracleComp.ProgramLogic.TacticInternals.Unary.planVCGenStep? : Lean.Elab.Tactic.TacticM (Option PlannedStep)

Choose one unary VCGen step and remember how to replay it explicitly.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenPlannedStep? : Lean.Elab.Tactic.TacticM (Option PlannedStep)

Execute one planned unary VCGen step, returning the chosen step for replay/trace.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenStep : Lean.Elab.Tactic.TacticM Bool

One step of VCGen on a Triple goal. Returns true if any progress was made.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenPassPlanned : Lean.Elab.Tactic.TacticM (Array PlannedStep)

Run one VCGen pass across all current goals and record the chosen steps.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenPass : Lean.Elab.Tactic.TacticM Bool

Run one VCGen pass across all current goals.