Can you be faster than `vcgen`?

TL;DR. Feel free to skip ahead to Evaluation: the technique presented here does beat vcgen on some cases from Lean's own vcgen performance benchmark suite. If that catches your interest, come back to the beginning for the idea behind it.

Background

In Lean, vcgen is a tactic for program verification. It rests on a classic foundation, the weakest precondition (WP) calculus.¹ A WP semantics maps a program x and a postcondition Q to a precondition wp x Q: the weakest condition on the initial state under which running x establishes Q (Dijkstra, 1975). In Lean, a Hoare triple ⦃P⦄ x ⦃Q⦄ is defined in terms of wp, as P ⊑ wp x Q.

Given such a goal, vcgen follows the program's structure, repeatedly applying specification lemmas, Hoare triples registered with @[spec]. The remaining entailments are the verification conditions (VCs), which grind can prove.

We can also prove ⦃P⦄ x ⦃Q⦄ in two stages. First expand wp x Q into a plain formula with no wp left, then prove that P entails that formula. One direct way to do this is rewriting. For a program f x, a rule such as wp (f x) = f_wp (wp x) expands the outer wp. We then continue recursively with x.

How this rewriting is done depends on the program. If the program is a deeply embedded syntax tree and wp is defined by recursion on it, the WP computes by definitional reduction. If the program is shallowly embedded, like ordinary Lean code, some metaprogramming is needed: find the terms that match a rule, say through a discrimination tree, and replace them.

The latter kind of rewriting has problems. For example:

• Rewriting with = can only replace a wp by an equivalent one, never by a suitably weaker one. For instance, it cannot use a spec you have already proved.²

• Rewriting builds a proof term as it goes. Lean's simp does, and so do Rocq's rewrite and generalized rewriting. This takes time, which can dominate when the WP is large.

  Can the proofs be skipped? Perhaps, but recovering a proof afterwards takes extra work, such as rewriting again with proofs. Making built-in machinery skip them is not easy either: as of Lean 4.35, simp has no option for it, and dsimp, which produces no proofs, can only use definitional (rfl) lemmas.

The rest of the post presents a rewriting-style approach that

• yields the simplified WP term itself;
• allows weakening along the way, with no special rewriting mechanism, only definitional reduction;
• yields a proof term guaranteeing that the WP is sound.

The idea

The approach rests on two observations, the second building on the first.

First, a compositional WP semantics interprets the program's constructs as predicate transformers. The literature on Dijkstra monads makes this precise: such a WP is a monad morphism from a computational monad into a specification monad, called an effect observation.

Second, if a program p is written against abstract constructs, then running p and computing its WP are two instantiations of the same term. Instantiated at a computational monad, p is the program, denoted as p_prog. Instantiated at the specification monad, p is its WP, denoted as p_wp. The soundness proof connecting the two is an instance of the program’s parametricity theorem. This proof stands apart from both instantiations, so we can work on p_wp directly, with or without it.

The recipe then almost writes itself:

• write the program in tagless final form;
• instantiate its parameters with predicate-transformer types;
• reduce;
• (optional) derive a soundness theorem by parametricity.

Here is an example that uses only the primitives of MonadStateOf:

def step {m : Type → Type} [Monad m] [MonadStateOf Nat m] (v : Nat) : m Unit := do
  let s ← get
  set (s + v)
  let s ← get
  set (s - v)

The specification monad Spec interprets a computation as a predicate transformer. It maps a postcondition on the result and the final state to a precondition on the initial state. We specify the state primitives with a MonadStateOf σ (Spec σ) instance:

abbrev Spec (σ α : Type) := (α → σ → Prop) → σ → Prop

instance : Monad (Spec σ) where
  pure a := fun post s => post a s
  bind w g := fun post s => w (fun a s' => g a post s') s

instance : MonadStateOf σ (Spec σ) where
  get := fun post s => post s s
  set t := fun post _ => post () t
  modifyGet f := fun post s => post (f s).1 (f s).2

At Spec, the program is its WP, and reduction alone exposes it:

example (v : Nat) (post : Unit → Nat → Prop) (s : Nat) :
    step (m := Spec Nat) v post s = post () (s + v - v) := rfl

To connect this WP to execution in StateM Nat, we use Tapas, introduced in the earlier post. We first define Sound x w: whenever w post s holds, running x from s establishes post. The relation is defined for every return type α.

def Sound : ⦃α : Type⦄ → StateM σ α → Spec σ α → Prop :=
  fun {_} x w => ∀ post s, w post s → post (x.run s).1 (x.run s).2

We then prove Monad.Rel Sound and MonadStateOf.Rel Sound. Both type classes appeared in the earlier post, so we give two examples of their meaning here:

• Monad.Rel Sound includes preservation by bind: sound Spec interpretations of x and f compose, through the bind of Spec, into a sound Spec interpretation of x >>= f.
• MonadStateOf.Rel Sound requires the state operations to preserve soundness. For set, this means ∀ t, Sound (set (m := StateM σ) t) (set (m := Spec σ) t).

We name these proofs Sound.monad and Sound.state. Passing them to step.parametric gives soundness of the whole program:

derive_parametric step    -- deriving parametricity with Tapas

theorem step_sound (v : Nat) : Sound (step (m := StateM Nat) v) (step (m := Spec Nat) v) :=
  step.parametric Sound Sound.monad Sound.state v

Reusing specs

The program so far used only primitives. To keep this method working when programs are composed, a caller must use not the callee itself but a stand-in for it.

Why? Suppose a caller calls a procedure directly. The procedure is a constant, and a constant unfolds to the same body under every instantiation, so the caller's WP contains the procedure's exact WP. Reduction re-derives it at every call site, and there is no room for a spec instead, such as one weaker than what the procedure does, or a contract with a precondition, proved once. Here is a procedure and such a spec:

def double {m : Type → Type} [Monad m] [MonadStateOf Nat m] (k : Nat) : m Nat := do
  let n ← get
  set (n + k)
  pure (2 * k)

/-- Weaker than what `double` does: the result is only known to be at least `k`. -/
def doubleSpec (k : Nat) : Spec Nat Nat := fun post s => ∀ r, k ≤ r → post r (s + k)

The stand-in is a type class with the procedure as its operation. It has two instances: the computational one runs the body, and the specification one is the spec.

class Double (m : Type → Type) where
  double : Nat → m Nat

instance : Double (StateM Nat) := ⟨fun k => double k⟩
instance : Double (Spec Nat) := ⟨doubleSpec⟩

Reducing a caller at Spec that goes through the class therefore yields the spec:

def caller {m : Type → Type} [Monad m] [MonadStateOf Nat m] [Double m] : m Nat := do
  let r ← Double.double 3    -- going through the stand-in type class
  let s ← get
  pure (s + r)

example (post : Nat → Nat → Prop) (s : Nat) :
    caller (m := Spec Nat) post s = ∀ r, 3 ≤ r → post (s + 3 + r) (s + 3) := rfl

The weakening happened by reduction, with no monotonicity reasoning at the call site. The price is one obligation, proved once per procedure: the spec must be sound for the body. Parametricity and reduction turn this obligation into a logical entailment. The caller's soundness then follows like step's, with Sound.double for the stand-in:

derive_effect_rel Double  -- defines `Double.Rel`: when two instances are related
derive_parametric double
derive_parametric caller

theorem Sound.double : Double.Rel (Sound (σ := Nat)) where
  double k post s h := double.parametric Sound Sound.monad Sound.state /- ... -/

theorem caller_sound : Sound (caller (m := StateM Nat)) (caller (m := Spec Nat)) :=
  caller.parametric Sound Sound.monad Sound.state Sound.double

Reducing WPs

Above, rfl did the reduction. But to hand a WP to a solver like grind, we need to normalize it. That is, we need to turn it into an explicit formula by unfolding the specification interpretations of the program's operations and subprocedures, using only definitional reduction.

The obvious candidate is dsimp. However, its general-purpose machinery can make it slower than we would like on some examples (see the evaluation results). We therefore developed a small, specialized normalizer. It works like a narrowly focused dsimp: it performs head reduction before descending into subterms and unfolds only definitions relevant to the specification interpretation. Symbolic if and match expressions are left unsplit, so that tools such as grind can handle the branching.

Evaluation

I compared the parametricity + normalizer approach introduced above against vcgen on eight selected cases from Lean's own vcgen benchmark suite. The full results are available on the results page. See PROTOCOL.md for the methods compared, their configurations, and the measurement setup. A playground lets you watch five of these cases both ways in your editor.

The main observations are:

• Generating VCs is cheap. In the three generation-only cases, normalization spends less time in Generate than vcgen at the same tier. Its larger gains in Total also reflect lower proof-sharing and kernel-checking costs.
• Normalization is less sensitive to operation specialization. In cases with hand-written operation specs, replacing them with library specs increases Generate time much more for vcgen than for normalization using PredTrans. The impact on Total is smaller when grind dominates.
• Solving the VC can dominate normalization. In PurePrecond, vcgen discharges each pure precondition as it goes, while normalization collects them into one large conjunction, which grind proves slowly. In GetThrowSet and DiteSplit, the VC nests an if at every step. At the larger tested sizes, vcgen … with finish is faster than normalization: it shares one E-graph across the branches and prunes the unreachable throws.
• Equation-based rewriting can be costly. On AddSubCancel at n = 2200, simp and Sym.simp take about 10 and 16 times the Total time of normalization in the hand-written-specs tier. Most of simp's time is spent rewriting, while Sym.simp is dominated by kernel checking.

Discussion

Of course, more than how it does on toy benchmarks like these, I care whether this technique scales. At that standard, no blog post (let alone a hastily written one) can settle the question, so I will only list a few aspects:

1. How can the stand-in type classes be generated automatically?

   A dedicated frontend for writing programs, as in Veil, should make it feasible.

2. Can this technique handle loops or recursion of various forms? Can this technique discharge VCs while generating them, as vcgen does?

   AI tells me they are possible, but I do not know.

3. Everything above is about monads. Can this technique handle programs that are not monadic?

   There is a preliminary experiment. It covers a small deeply embedded command language whose interpreter is written against an algebra of its constructors rather than a monad. Interpreted in a predicate-transformer algebra, a command computes its WP, and parametricity proves that WP exact.

4. Does this normalizer scale?

   I genuinely don't know.