18.1. Overview

The workflow of mvcgen consists of the following:

1. Monadic programs are re-interpreted according to a predicate transformer semantics. An instance of WP determines the monad's interpretation. 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 monads to work with mvcgen need to understand it.

2. Programs are composed from smaller programs. Each statement in a Lean.Parser.Term.do : termdo-block is associated with a predicate transformer, and there are general-purpose rules for combining these statements 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.

3. Applying the weakest-precondition semantics of a monadic program to a desired proof goal results in the precondition that must hold in order to prove the goal. Any missing steps such as loop invariants or proofs that a statement's precondition implies its postcondition become new subgoals. These missing steps are called the verification conditions. The mvcgen tactic performs this transformation, replacing the goal with its verification conditions. During this transformation, mvcgen uses specification lemmas to discharge proofs about individual statements.

4. After supplying loop invariants, many verification conditions can in practice be discharged automatically. Those that cannot can be proven using either a special proof mode or ordinary Lean tactics, depending on whether they are expressed in the logic of program assertions or as ordinary propositions.