17.1. Overview🔗

The workflow of vcgen consists of the following:

Programs are re-interpreted according to a predicate transformer semantics. An instance of WP for the program type determines the interpretation. The program type can be a monadic computation, such as a Lean.Parser.Term.do : termdo-block in StateM Nat. Non-monadic types, such as the syntax trees of a small imperative langauge, are also supported. Each program is interpreted as a mapping from arbitrary postconditions to the weakest precondition that would ensure the postcondition. This step is invisible to most users, but library authors who want to enable their program types to work with vcgen need to understand it.
Programs are composed from smaller programs. Each part of a program, such as a statement in a Lean.Parser.Term.do : termdo-block, is associated with a predicate transformer, and there are general-purpose rules for combining these parts with sequencing and control-flow operators. A statement with its pre- and postconditions is called a Hoare triple. In a program, the postcondition of each statement should suffice to prove the precondition of the next one, and loops require a specified loop invariant, which is a statement that must be true at the beginning of the loop and at the end of each iteration. Designated specification lemmas associate functions with Hoare triples that specify them.
Applying the weakest-precondition semantics of a program to a desired proof goal results in the precondition that must hold in order to prove the goal. The remaining entailments between assertions, such as a proof that the postcondition of one statement implies the precondition of the next, contain no weakest preconditions and become new subgoals. These subgoals are called the verification conditions. Loop invariants that the user supplies become separate subgoals. The vcgen tactic performs this transformation, replacing the goal with its verification conditions. During this transformation, vcgen uses specification lemmas to discharge proofs about individual statements.
After supplying loop invariants, many verification conditions can in practice be discharged automatically. Those that cannot are ordinary Lean goals, provable with ordinary Lean tactics or with the grind-mode step of the Lean.Parser.Tactic.vcgen : tactic`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`.with clause.