17.3. Verification Conditions🔗

The vcgen tactic converts a goal that's expressed in terms of weakest preconditions to a set of invariants and verification conditions that, together, suffice to prove the original goal. In particular, Hoare triples are defined in terms of weakest preconditions, so vcgen can be used to prove them.

The verification conditions for a goal are generated using the same machinery as grind. Generation proceeds as follows:

The goal is brought into the form of an entailment P ⊑ R between assertions. Binders are introduced, Hoare triples are unfolded to P ⊑ wp e Q E, and goals of the form wp e Q E become ⊤ ⊑ wp e Q E.
The precondition P is moved into the local context: a pure assertion ⌜φ⌝ becomes a hypothesis φ, an existential ⨆ becomes a variable, and the arguments of a state predicate become variables.
The assertion R is recursively decomposed into goals based on its connectives: meets ⊓ are split into one goal per conjunct, the antecedents of ⇨ are mvoed into the precondition, pure assertions ⌜φ⌝ are transformed into the proposition φ, and ⊤ goals are closed immediately.
If R is wp e Q E, then the program e is decomposed:
1. A Lean.Parser.Term.let : term`let` is used to declare a local definition. Example: ``` let x := 1 let y := x + 1 x + y ``` Since functions are first class citizens in Lean, you can use `let` to declare local functions too. ``` let double := fun x => 2*x double (double 3) ``` For recursive definitions, you should use `let rec`. You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write ``` let (x, y) := p x + y ``` The *anaphoric let* `let := v` defines a variable called `this`.let-binding is introduced, becoming a hypothesis.
2. An application of an auxiliary matching function whose discriminant is a constructor application is reduced; any other conditional or match is split into one goal per branch.
3. An application of a function is handled by the first applicable specification lemma in priority order. Hypotheses that are Hoare triples also count as specification lemmas. Lean includes specification lemmas for bind, pure, ForIn.forIn and the other functions that result from desugaring Lean.Parser.Term.do : termdo-notation. If no specification lemma applies, then vcgen reports an error.
  
  A specification lemma P' ⊑ wp e' Q' E' is applied by transitivity of ⊑: the goal P ⊑ wp e Q E follows from P ⊑ P' and wp e' Q' E' ⊑ wp e Q E. The second entailment holds when e' unifies with e, Q' ⊑ Q and E' ⊑ E. In effect, vcgen replaces the weakest precondition in the goal by the precondition of the lemma, which gives the new goal P ⊑ P'.
4. The variables in the lemma that occur in the program are instantiated using unification. The universally quantified postcondition of an auto-framing specification becomes Q, so Q' ⊑ Q holds by reflexivity and no goal for the postcondition remains. Otherwise, the entailments Q' ⊑ Q and E' ⊑ E become new goals. Assumptions of a type registered with spec_invariant_type become invariant goals. The logical variables of the lemma appear as metavariables in all of these new goals.
Each new goal is processed again from step 1. For example, the specification lemma Spec.bind is auto-framing and has the precondition wp x (fun a => wp (f a) Q E) E. For a goal P ⊑ wp (x >>= f) Q E, the new goal is P ⊑ wp x (fun a => wp (f a) Q E) E. When a specification lemma for x applies to this goal, the entailment between the postconditions has wp (f a) Q E on the right, so the rest of the program is decomposed in the same way. Before a new goal is processed, its hypotheses are internalized into grind's “whiteboard”, and a goal whose hypotheses are contradictory is dropped.
The verification conditions are the remaining goals that cannot be further decomposed by these steps. Before each verification condition is emitted, vcgen solves its conjuncts that are either True or an equality e₁ = e₂ where e₁ and e₂ can be made definitionally equal by unification.. Solving an equality can assign a metavariable, so some logical variables become assigned: a conjunct s = ?n assigns ?n := s. The unsolved conjuncts remain as the verification condition.
The resulting subgoals receive the names inv1, inv2, … for invariants and vc1, vc2, … for verification conditions, in the order of generation.

VC generation stops early after stepLimit program steps. An 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`.until clause stops VC generation at the first program that matches the given pattern. A 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 runs the given grind-mode step on every remaining verification condition. A clause 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`.simplifying_assumptions [h₁, h₂] rewrites the hypotheses that binders and branches introduce, and the state arguments of each weakest precondition, with h₁ and h₂ as additional rewrite rules. This keeps the intermediate goals in a normal form that the user chooses: for example, a sequence of state updates can fold into one constructor application, so that the goals do not grow with the number of updates. Simplified hypotheses also help grind to detect contradictory goals.