Syntax of the vcgen tactic for the Std.WP program logic. The builtin elaborator lives in Lean.Elab.Tactic.VCGen.

def Lean.Parser.Attr.spec : ParserDescr

Marks a specification for the vcgen tactic.

• On a theorem foo_spec : ⦃P⦄ foo a b c ⦃Q⦄, vcgen uses foo_spec for calls to foo.
• On a definition foo or an equation that @[simp] accepts, vcgen rewrites calls with its equations.

Equations

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

def Lean.Parser.Tactic.invariantDotAlt : ParserDescr

An invariant alternative of the form · term, one per invariant goal.

Equations

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

def Lean.Parser.Tactic.invariantCaseAlt : ParserDescr

An invariant alternative of the form | inv<n> a b c => term, one per invariant goal.

Equations

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

def Lean.Parser.Tactic.invariantsKW : ParserDescr

Either the contextual keyword invariants or its tracing form invariants? which suggests skeletons for missing invariants as a hint.

Equations

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

def Lean.Parser.Tactic.invariantAlts : ParserDescr

After mvcgen [...], there can be an optional invariants followed by either

• a bulleted list of invariants · term; · term.
• a labelled list of invariants | inv1 => term; inv2 a b c => term, which is useful for naming inaccessibles. The tracing variant invariants? will suggest a skeleton for missing invariants; see the docstring for mvcgen.

Equations

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

def Lean.Parser.Tactic.frameAlt : ParserDescr

A single frames alternative | f a _ c => frame: a program pattern (a head identifier applied to binder or _ arguments, matched like the until pattern) and the frame assertion to apply when the spec for that program is used during VC generation. The named binders (e.g. a, c) are in scope in frame, bound to the matched arguments.

Equations

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

def Lean.Parser.Category.vcgenDischarge : Category

The discharging step in vcgen … with. It is a single grind-mode tactic (e.g. finish, intro) so it can share vcgen's internalised E-graph. The tactic alternative is a lower-priority catch-all so that a non-grind step (e.g. with grind, with simp) still parses and the elaborator can report a helpful error instead of a raw expected grind parser error.

Equations

• Lean.Parser.Category.vcgenDischarge = { }

def Lean.Parser.Tactic.vcgenDischarge.quot : ParserDescr

Equations

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

def Lean.Parser.Tactic.vcgenDischargeGrind : ParserDescr

Equations

• Lean.Parser.Tactic.vcgenDischargeGrind = Lean.ParserDescr.node `Lean.Parser.Tactic.vcgenDischargeGrind 1022 (Lean.ParserDescr.cat `grind 0)

def Lean.Parser.Tactic.vcgenDischargeTactic : ParserDescr

Equations

• Lean.Parser.Tactic.vcgenDischargeTactic = Lean.ParserDescr.node `Lean.Parser.Tactic.vcgenDischargeTactic 1022 (Lean.ParserDescr.cat `tactic 0)

def Lean.Parser.Tactic.vcgen : ParserDescr

vcgen will break down a Hoare triple proof goal like ⦃P⦄ prog ⦃Q⦄ into verification conditions, provided that all functions used in prog have specifications registered with @[spec].

vcgen is experimental and subject to change. set_option experimental.vcgen true acknowledges its experimental status and silences the warning that each call reports.

Program types

vcgen works on any program type Prog that carries a Std.WP.WP interpretation. A monad is one such program type. An inductive type of commands is another, once its weakest precondition is defined in terms of an operational semantics.

Verification conditions and specifications

A verification condition is an entailment pre ⊑ post in the assertion lattice of the goal. The original program prog no longer occurs in it. The assertion lattice is any CompleteLattice, and the entailment is its order, so a verification condition is an ordinary Lean goal that grind can attack.

A @[spec] theorem declares a specification in one of two forms. A Hoare triple foo_spec : ⦃P⦄ foo a b c ⦃Q⦄ states it directly. An equation baz_eq : baz a b c = ... states it by rewriting.

Features

When used like vcgen [foo_spec, bar_def, baz_eq], vcgen will additionally

• add a Hoare triple specification foo_spec : ⦃P⦄ foo ... ⦃Q⦄ to the spec set for a function foo occurring in prog,
• unfold a definition def bar_def ... := ... in prog,
• rewrite with an equational specification baz_eq : baz ... = ... in prog.

Config options

See Lean.Elab.Tactic.Do.VCGen.Config for the options. Of particular note are stepLimit = some 42, which is useful for bisecting bugs and tracing execution, and errorOnMissingSpec := false, which leaves a goal whose head has no matching spec as a verification condition for you to discharge.

Extended syntax

Often, vcgen will be used like this:

vcgen [...] invariants
· I1
· I2
with try finish

The with clause takes one step of grind mode, such as finish. That step shares the E-graph that vcgen builds, so it sees the hypotheses of every verification condition. A sequence of steps needs explicit grouping, as in with (s₁; s₂).

Invariants also take a labelled form, which is useful for naming inaccessibles:

vcgen [...] invariants
| inv1 _ acc _ => I1 acc
| _ => I2

vcgen has two further clauses.

vcgen until f a _ c

stops VC generation at the first program that matches the pattern, and leaves that program in the goal. Holes are written _, as in conv in.

vcgen frames
| f a _ c => F

supplies a frame for a call. Take mkFreshNat : StateM (Nat × Nat) Nat, which returns s.1 and increments it. Its specification mentions s.1 alone:

@[spec] theorem mkFreshNat_spec :
    ⦃fun s => ⌜s.1 = n⌝⦄ mkFreshNat ⦃fun r s => ⌜r = n ∧ s.1 = n + 1⌝⦄

A caller that knows s.2 = 7 loses that fact at the call, because the postcondition says nothing about s.2. Writing

vcgen frames
| mkFreshNat => fun s => ⌜s.2 = 7⌝

carries s.2 = 7 past the call, and vcgen proves that mkFreshNat preserves it. The named binders are in scope in the frame, bound to the matched arguments.

Invariant suggestions

vcgen [...] invariants? warns that invariant suggestions are not available in vcgen and that the keyword is slated for removal. Alternatives after invariants? elaborate like invariants.

Equations

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

def Lean.Parser.Tactic.Grind.vcgen : ParserDescr

vcgen step for sym => … blocks. No with clause: compose with subsequent grind steps using <;> instead.

Equations

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