From aa5644be1209d554a7464dd93c586cbfd044d32e Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 22 Sep 2025 09:03:32 +0200 Subject: [PATCH 1/4] feat: add tutorial chapter for `mvcgen` --- .vale/styles/config/ignore/names.txt | 7 + .vale/styles/config/ignore/terms.txt | 9 + Manual.lean | 3 + Manual/VCGen.lean | 806 +++++++++++++++++++++++++++ 4 files changed, 825 insertions(+) create mode 100644 Manual/VCGen.lean diff --git a/.vale/styles/config/ignore/names.txt b/.vale/styles/config/ignore/names.txt index f6f56e5fa..d7dcb0f8c 100644 --- a/.vale/styles/config/ignore/names.txt +++ b/.vale/styles/config/ignore/names.txt @@ -1,13 +1,19 @@ +Bhavik Blott Bruijn Carneiro Collatz +Himmel's +Hoare Lua Madelaine +Markus Mathlib +Mehta Merkin Moura Peano +Rish Selsam Simons Streicher @@ -20,3 +26,4 @@ Nawrocki's Rustan Leino Leino's +Vaishnav's diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt index f3173888e..6b09e7c48 100644 --- a/.vale/styles/config/ignore/terms.txt +++ b/.vale/styles/config/ignore/terms.txt @@ -98,8 +98,10 @@ letterlike linearization linearize linearizing +logics lookup lookups +lossy macro_rules matcher matchers @@ -121,6 +123,7 @@ multipattern multipatterns multiset multisets +mvcgen namespace namespace's namespaces @@ -139,12 +142,16 @@ polymorphic polymorphically ponens popcount +postcondition +postconditions postfix +poststate predicative predicativity prepending preprocesses propositionally +prestate quasiquotation quasiquotations quasiquote @@ -207,5 +214,7 @@ uninstantiated unparenthesized uploader upvote +VC +VCs walkthrough zulip diff --git a/Manual.lean b/Manual.lean index 3b8ae5422..cf226264e 100644 --- a/Manual.lean +++ b/Manual.lean @@ -18,6 +18,7 @@ import Manual.ErrorExplanations import Manual.Tactics import Manual.Simp import Manual.Grind +import Manual.VCGen import Manual.BasicTypes import Manual.BasicProps import Manual.NotationsMacros @@ -98,6 +99,8 @@ Thus, this reference manual does not draw a barrier between the two aspects, but {include 0 Manual.Grind} +{include 0 Manual.VCGen} + {include 0 Manual.BasicProps} {include 0 Manual.BasicTypes} diff --git a/Manual/VCGen.lean b/Manual/VCGen.lean new file mode 100644 index 000000000..e884a1bfd --- /dev/null +++ b/Manual/VCGen.lean @@ -0,0 +1,806 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Sebastian Graf +-/ + +import VersoManual + +import Manual.Meta + +import Std.Tactic.Do + +open Verso.Genre Manual +open Verso.Genre.Manual.InlineLean + +set_option pp.rawOnError true + +set_option verso.docstring.allowMissing true + +set_option linter.unusedVariables false + +set_option linter.typography.quotes true +set_option linter.typography.dashes true + +set_option mvcgen.warning false + +open Manual (comment) + +#doc (Manual) "The `mvcgen` tactic" => +%%% +tag := "mvcgen-tactic" +%%% + +The {tactic}`mvcgen` tactic implements a _monadic verification condition generator_: +It breaks down a goal involving a program written using Lean's imperative `do` notation into a number of pure _verification conditions_ (VCs) that discharge said goal. +A verification condition is a sub-goal that does not mention the monad underlying the `do` block. + +In order to use the {tactic}`mvcgen` tactic, `Std.Tactic.Do` must be imported and the namespace `Std.Do` must be opened. + +``` +import Std.Tactic.Do +open Std.Do +``` + +# Verifying imperative programs using `mvcgen` + +This section is a tutorial introducing the most important concepts of {tactic}`mvcgen` top-down. +Recall that you need to import `Std.Tactic.Do` and open `Std.Do` to run these examples. + +```lean -show +open Std.Do +``` + +:::example "Array Sum" (open := true) (keep := true) +As a “hello world” to {tactic}`mvcgen`, the following example {name}`mySum` computes the sum of an array using local mutability and a `for` loop. +Then it proves {name}`mySum` correct relative to {name}`Array.sum`, requiring us to specify an invariant for the loop: +```lean +def mySum (l : Array Nat) : Nat := Id.run do + let mut out := 0 + for i in l do + out := out + i + return out + +theorem mySum_correct (l : Array Nat) : mySum l = l.sum := by + -- Focus on the part of the program with the `do` block (`Id.run ...`) + generalize h : mySum l = x + apply Id.of_wp_run_eq h + -- Break down into verification conditions + mvcgen + -- Specify the invariant which should hold throughout the loop + -- * `out` refers to the current value of the `let mut` variable + -- * `xs` is a `List.Cursor`, which is a data structure representing + -- a list that is split into `xs.prefix` and `xs.suffix`. + -- It tracks how far into the loop we have gotten. + -- Our invariant is that `out` holds the sum of the prefix. + -- The notation ⌜p⌝ embeds a `p : Prop` into the assertion language. + case inv1 => exact ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝ + -- After specifying the invariant, we can further simplify our goals + -- by "leaving the proof mode". `mleave` is just + -- `simp only [...] at *` with a stable simp subset. + all_goals mleave + -- Prove that our invariant is preserved at each step of the loop + case vc1 ih => + -- The goal here mentions `pref`, which binds the `prefix` field of + -- the cursor passed to the invariant. Unpacking the + -- (dependently-typed) cursor makes it easier for `grind`. + grind + -- Prove that the invariant is true at the start + case vc2 => + grind + -- Prove that the invariant at the end of the loop implies the + -- property we wanted + case vc3 h => + grind +``` +Note that the case labels are actually unique prefixes of the full case labels. +Whenever referring to cases, only this prefix should be used; the suffix is merely a poor man's hint to the user where that particular VC came from. +For example, + +* `vc1.step` conveys that this VC proves the inductive step for the loop +* `vc2.a.pre` is meant to prove that the hypotheses of a goal implies the precondition of a specification (of {name}`forIn`). +* `vc3.a.post` is meant to prove that the postcondition of a specification (of {name}`forIn`) implies the target of the goal. + +After specifying the loop invariant, the proof can be shortened to just `all_goals mleave; grind` (cf. {tactic}`mleave`). +```lean +theorem mySum_correct_short (l : Array Nat) : mySum l = l.sum := by + generalize h : mySum l = x + apply Id.of_wp_run_eq h + mvcgen + case inv1 => exact ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝ + all_goals mleave; grind +``` +This pattern is in fact so popular that `mvcgen` comes with special syntax for it: +```lean +theorem mySum_correct_shorter (l : Array Nat) : mySum l = l.sum := by + generalize h : mySum l = x + apply Id.of_wp_run_eq h + mvcgen + invariants + · ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝ + with grind +``` +The `mvcgen invariants ... with ...` expands to the same syntax as the +tactic sequence `mvcgen; case inv1 => ...; all_goals mleave; grind` +above. It is the form that we will be using from now on. +::: + +It is helpful to compare the proof of {name}`mySum_correct_shorter` to a traditional correctness proof: + +```lean +theorem mySum_correct_vanilla (l : Array Nat) : mySum l = l.sum := by + -- Turn the array into a list + cases l with | mk l => + -- Unfold `mySum` and rewrite `forIn` to `foldl` + simp [mySum] + -- Generalize the inductive hypothesis + suffices h : ∀ out, List.foldl (· + ·) out l = out + l.sum by simp [h] + -- Grind away + induction l with grind +``` + +This proof is similarly succinct as the proof in {name}`mySum_correct_shorter` using {tactic}`mvcgen`. +However, the traditional approach relies on important properties of the program: + +* The `for` loop does not `break` or `return` early. Otherwise, the `forIn` could not be rewritten to a `foldl`. +* The loop body `(· + ·)` is small enough to be repeated in the proof. +* The loop body is `pure`, that is, does not perform any effects. + (Indeed, all computations in the base monad `Id` factor through `pure`.) + While `forIn` could still be rewritten to a `foldlM`, reasoning about the monadic loop body can be tough for `grind`. + +In the following sections, we will go through several examples to learn about {tactic}`mvcgen` and its support library, and also see where traditional proofs become difficult. +This is usually caused by + +* `do` blocks using control flow constructs such as `for` loops, `break`s and early `return`. +* Effectful computations in non-`Id` monads. + Such computations affect the implicit monadic context (state, exceptions) in ways that need to be reflected in loop invariants. + +{tactic}`mvcgen` scales to these challenges with reasonable effort. + +## Control flow + +Let us consider another example that combines `for` loops with an early return. + +:::example "Detecting Duplicates in a List" (open := true) (keep := true) +Recall that {name}`List.Nodup` is a predicate that asserts that a given list does not contain any duplicates. +The function {name}`nodup` below decides this predicate: + +```lean +def nodup (l : List Int) : Bool := Id.run do + let mut seen : Std.HashSet Int := ∅ + for x in l do + if x ∈ seen then + return false + seen := seen.insert x + return true + +theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by + generalize h : nodup l = r + apply Id.of_wp_run_eq h + mvcgen + invariants + · Invariant.withEarlyReturn + (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝) + (onContinue := fun xs seen => + ⌜(∀ x, x ∈ seen ↔ x ∈ xs.prefix) ∧ xs.prefix.Nodup⌝) + with grind +``` +::: + +The proof has the same succinct structure as for the initial {name}`mySum` example, because we again offload all proofs to {tactic}`grind` and its existing framework around {name}`List.Nodup`. +Therefore, the only difference is in the invariant. +Since our loop has an early return, we construct the invariant using the helper function {lean}`Invariant.withEarlyReturn`. +This function allows us to specify the invariant in three parts: + +* `onReturn ret seen` holds after the loop was left through an early return with value `ret`. + In case of {name}`nodup`, the only value that is ever returned is {name}`false`, in which case {name}`nodup` has decided there _is_ a duplicate in the list. +* `onContinue xs seen` is the regular induction step that proves the invariant is preserved each loop iteration. + The iteration state is captured by the cursor `xs`. + The given example asserts that the set `seen` contains all the elements of previous loop iterations and asserts that there were no duplicates so far. +* `onExcept` must hold when the loop throws an exception. + There are no exceptions in `Id`, so we leave it unspecified to use the default. + (Exceptions will be discussed at a later point.) + +:::TODO +Note that the form `mvcgen invariants?` would hint that {name}`Invariant.withEarlyReturn` is a useful way to construct the invariant: +``` +example (l : List Int) : nodup l ↔ l.Nodup := by + generalize h : nodup l = r + apply Id.of_wp_run_eq h + mvcgen invariants? +``` +::: + +Now consider the following direct (and excessively golfed) proof without {tactic}`mvcgen`: + +```lean +theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by + rw [nodup] + generalize hseen : (∅ : Std.HashSet Int) = seen + change ?lhs ↔ l.Nodup + suffices h : ?lhs ↔ l.Nodup ∧ ∀ x ∈ l, x ∉ seen by grind + clear hseen + induction l generalizing seen with grind [Id.run_pure, Id.run_bind] +``` + +Some observations: + +* The proof is even shorter than the one with {tactic}`mvcgen`. +* The use of {tactic}`generalize` to generalize the accumulator relies on there being exactly one occurrence of `∅` to generalize. If that were not the case, we would have to copy parts of the program into the proof. This is a no go for larger functions. +* {tactic}`grind` splits along the control flow of the function and reasons about {name}`Id`, given the right lemmas. + While this works for {name}`Id.run_pure` and {name}`Id.run_bind`, it would not work for {name}`Id.run_seq`, for example, because that lemma is not E-matchable. If {tactic}`grind` would fail, we would be forced to do all the control flow splitting and monadic reasoning by hand until {tactic}`grind` can pick up again. + +The usual way to avoid replicating the control flow of a definition under proof is to use the {tactic}`fun_cases` or {tactic}`fun_induction` tactics. +Unfortunately, {tactic}`fun_cases` does not help with control flow inside a {name}`forIn` application, for example. +This is in contrast to {tactic}`mvcgen`, which ships with support for many {name}`forIn` implementations and is easily extended with `@[spec]` annotations for custom {name}`forIn` implementations. +Furthermore, a {tactic}`mvcgen`-powered proof will never need to copy any part of the original program. + +## Compositional reasoning about effectful programs using Hoare triples + +The previous examples reasoned about functions defined using `Id.run do ` to make use of local mutability and early return in ``. +However, real-world programs often use `do` notation and monads `M` to hide away state and failure conditions as implicit “effects”. +In this use case, functions usually omit the `M.run`. +Instead they have monadic return type `M α` and compose well with other functions of that return type. + +:::example "Generating Fresh Numbers" (open := true) (keep := true) +Here is an example involving a stateful function {name}`mkFresh` that returns auto-incremented counter values: + +```lean +structure Supply where + counter : Nat + +def mkFresh : StateM Supply Nat := do + let n ← (·.counter) <$> get + modify (fun s => {s with counter := s.counter + 1}) + pure n + +def mkFreshN (n : Nat) : StateM Supply (List Nat) := do + let mut acc := #[] + for _ in [:n] do + acc := acc.push (← mkFresh) + pure acc.toList +``` + +`mkFreshN n` returns `n` “fresh” numbers, modifying the internal {name}`Supply` state through {name}`mkFresh`. +Here, “fresh” refers to all previously generated numbers being distinct from the next generated number. +We can formulate and prove a correctness property {name}`mkFreshN_correct` in terms of {name}`List.Nodup`: + +```lean +theorem mkFreshN_correct (n : Nat) : ((mkFreshN n).run' s).Nodup := by + -- Focus on `(mkFreshN n).run' s`. + generalize h : (mkFreshN n).run' s = x + apply StateM.of_wp_run'_eq h + -- Show something about monadic program `mkFresh n`. + -- The `mkFreshN` and `mkFresh` arguments to `mvcgen` add to an + -- internal `simp` set and makes `mvcgen` unfold these definitions. + mvcgen [mkFreshN, mkFresh] + invariants + -- Invariant: The counter is larger than any accumulated number, + -- and all accumulated numbers are distinct. + -- Note that the invariant may refer to the state through function + -- argument `state : Supply`. Since the next number to accumulate is + -- the counter, it is distinct to all accumulated numbers. + · ⇓⟨xs, acc⟩ state => + ⌜(∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup⌝ + with grind +``` +::: + +## Composing specifications + +Nested unfolding of definitions as in `mvcgen [mkFreshN, mkFresh]` is quite blunt but effective for small programs. +A more compositional way is to develop individual _specification lemmas_ for each monadic function. +These can either be passed as arguments to {tactic}`mvcgen` or registered in a global (or `scoped`, or `local`) database of specifications using the `@[spec]` attribute: + +:::example "Decomposing a Proof into Specifications" (open := true) (keep := true) +```lean +@[spec] +theorem mkFresh_spec (c : Nat) : + ⦃fun state => ⌜state.counter = c⌝⦄ + mkFresh + ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by + -- Unfold `mkFresh` and blast away: + mvcgen [mkFresh] with grind + +@[spec] +theorem mkFreshN_spec (n : Nat) : + ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by + -- `mvcgen [mkFreshN, mkFresh_spec]` if `mkFresh_spec` were not + -- registered with `@[spec]` + mvcgen [mkFreshN] + invariants + -- As before: + · ⇓⟨xs, acc⟩ state => + ⌜(∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup⌝ + with grind + +theorem mkFreshN_correct_compositional (n : Nat) : + ((mkFreshN n).run' s).Nodup := + -- The type `⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄` of `mkFreshN` is + -- definitionally equal to + -- `∀ (n : Nat) (s : Supply), True → ((mkFreshN n).run' s).Nodup` + mkFreshN_spec n s True.intro +``` + +```lean -show +variable {c : Nat} +``` +Here, the notation {lean}`⦃fun state => ⌜state.counter = c⌝⦄ mkFresh ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄` denotes a _Hoare triple_ (cf. {name}`Std.Do.Triple`). +Specifications for monadic functions always have such a Hoare triple result type. +::: + +## Hoare triples + +{docstring Std.Do.Triple} + +:::syntax term (title := "Hoare triple") (namespace := Std.Do) +```grammar +⦃ term ⦄ term ⦃ term ⦄ +``` +::: + +{docstring Std.Do.Triple.and} + +{docstring Std.Do.Triple.mp} + +```lean -show +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} [WP m ps] {α σ ε : Type u} {P : Assertion ps} {Q : PostCond α ps} {prog : m α} +``` +Given the meaning of Hoare triples above, the specification theorem for {name}`mkFresh` says: + +> If {lean}`c` refers to the {name}`Supply.counter` field of the {name}`Supply` prestate, then running {name}`mkFresh` returns {lean}`c` and modifies the {name}`Supply.counter` of the poststate to be larger than {lean}`c`. + +Note that this specification is lossy: {name}`mkFresh` could increment its state by an arbitrary non-negative amount and still satisfy the specification. +This is good, because specifications may _abstract over_ uninteresting implementation details, ensuring resilient and small proofs. + +Hoare triples are defined in terms of a logic of stateful predicates plus a weakest precondition semantics {lean}`wp⟦prog⟧` that translates monadic programs into this logic: + +```lean +-- This is the definition of Std.Do.Triple: +def Triple [WP m ps] {α : Type u} (prog : m α) + (P : Assertion ps) (Q : PostCond α ps) : Prop := + P ⊢ₛ wp⟦prog⟧ Q +``` + +The {name}`WP` type class maps a monad {lean}`m` to its {name}`PostShape` {lean}`ps`, and this {name}`PostShape` governs the exact shape of the {name}`Std.Do.Triple`. +Many of the standard monad transformers such as {name}`StateT`, {name}`ReaderT` and {name}`ExceptT` come with a canonical {name}`WP` instance. +For example, `StateT σ` comes with a {name}`WP` instance that adds a `σ` argument to every {name}`Assertion`. +Stateful entailment `⊢ₛ` eta-expands through these additional `σ` arguments. +For {name}`StateM` programs, the following type is definitionally equivalent to {name}`Std.Do.Triple`: + +```lean +def StateMTriple {α σ : Type u} (prog : StateM σ α) + (P : σ → ULift Prop) (Q : (α → σ → ULift Prop) × PUnit) : Prop := + ∀ s, (P s).down → let (a, s') := prog.run s; (Q.1 a s').down + +example : @StateMTriple α σ = Std.Do.Triple (m := StateM σ) := rfl +``` + +```lean -show +variable {p : Prop} +``` + +The common postcondition notation `⇓ r => ...` injects an assertion of type `α → Assertion ps` into +`PostCond ps` (the `⇓` is meant to be parsed like `fun`); in case of {name}`StateM` by adjoining it with an empty tuple {name}`PUnit.unit`. +The shape of postconditions becomes more interesting once exceptions enter the picture. +The notation {lean}`⌜p⌝` embeds a pure hypotheses {lean}`p` into a stateful assertion. +Vice versa, any stateful hypothesis {lean}`P` is called _pure_ if it is equivalent to {lean}`⌜p⌝` +for some {lean}`p`. +Pure, stateful hypotheses may be freely moved into the regular Lean context and back. +(This can be done manually with the {tactic}`mpure` tactic.) + +### An advanced note about pure preconditions and a notion of frame rule + +This subsection is a bit of a digression and can be skipped on first reading. + +Say the specification for some [`Aeneas`](https://github.com/AeneasVerif/aeneas)-inspired monadic addition function `x +? y : M UInt8` has the +requirement that the addition won't overflow, that is, `h : x.toNat + y.toNat ≤ UInt8.size`. +Should this requirement be encoded as a regular Lean hypothesis of the specification (`add_spec_hyp`) or should this requirement be encoded as a pure precondition of the Hoare triple, using `⌜·⌝` notation (`add_spec_pre`)? + +``` +theorem add_spec_hyp (x y : UInt8) (h : x.toNat + y.toNat ≤ UInt8.size) : + ⦃⌜True⌝⦄ x +? y ⦃⇓ r => ⌜r.toNat = x.toNat + y.toNat⌝⦄ := ... + +theorem add_spec_pre (x y : UInt8) : + ⦃⌜x.toNat + y.toNat ≤ UInt8.size⌝⦄ + x +? y + ⦃⇓ r => ⌜r.toNat = x.toNat + y.toNat⌝⦄ := ... +``` + +The first approach is advisable, although it should not make a difference in practice. +The VC generator will move pure hypotheses from the stateful context into the regular Lean context, so the second form turns effectively into the first form. +This is referred to as _framing_ hypotheses (cf. the {tactic}`mpure` and {tactic}`mframe` tactics). +Hypotheses in the Lean context are part of the immutable _frame_ of the stateful logic, because in contrast to stateful hypotheses they survive the rule of consequence. + +## Monad transformer stacks + +Real-world programs often orchestrate the interaction of independent subsystems through a stack of monad transformers. +We can tweak the previous example to demonstrate this. + +```lean -show +namespace Stack +variable {m : Type → Type} {α : Type} {ps : PostShape.{0}} +attribute [-instance] Lake.instMonadLiftTOfMonadLift_lake +``` + +:::example "Transformer Stacks" (open := true) (keep := true) +Suppose that {name}`mkFresh` is generalized to work in any base monad {lean}`m` under {lean}`StateT Supply`. +Furthermore, {name}`mkFreshN` is defined in terms of a concrete monad transformer stack {name}`AppM` and lifts {name}`mkFresh` into {name}`AppM`. +Then the {tactic}`mvcgen`-based proof goes through unchanged: + +```lean +def mkFresh [Monad m] : StateT Supply m Nat := do + let n ← (·.counter) <$> get + modify (fun s => {s with counter := s.counter + 1}) + pure n + +abbrev AppM := StateT Bool (StateT Supply (ReaderM String)) +abbrev liftCounterM : StateT Supply (ReaderM String) α → AppM α := liftM + +def mkFreshN (n : Nat) : AppM (List Nat) := do + let mut acc := #[] + for _ in [:n] do + let n ← liftCounterM mkFresh + acc := acc.push n + return acc.toList + +@[spec] +theorem mkFresh_spec [Monad m] [WPMonad m ps] (c : Nat) : + ⦃fun state => ⌜state.counter = c⌝⦄ + mkFresh (m := m) + ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by + mvcgen [mkFresh] with grind + +@[spec] +theorem mkFreshN_spec (n : Nat) : + ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by + -- `liftCounterM` here ensures unfolding + mvcgen [mkFreshN, liftCounterM] + invariants + · ⇓⟨xs, acc⟩ _ state => + ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝ + with grind +``` + +The {name}`WPMonad` type class asserts that {lean}`wp⟦prog⟧` distributes over the {name}`Monad` operations (“monad morphism”). +This proof might not look much more exciting than when only a single monad was involved. +However, under the radar of the user the proof builds on a cascade of specifications for `MonadLift` instances. +::: + +```lean -show +end Stack +``` + +## Exceptions + +```lean -show +variable {Q' : α → Assertion ps} +``` + +If `let mut` is the first-order pendant to {name}`StateT`, then early `return` is the first-order pendant to {name}`ExceptT`. +We have seen how the {tactic}`mvcgen` copes with {name}`StateT`; here we will look at the program logic's support for {name}`ExceptT`. + +Exceptions are the reason why the type of postconditions {lean}`PostCond α ps` is not simply a single condition of type {lean}`α → Assertion ps` for the success case. +To see why, suppose the latter was the case, and suppose that program {lean}`prog` throws an exception in a prestate satisfying {lean}`P`. +Should we be able to prove {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄`? +(Recall that `⇓` is grammatically similar to `fun`.) +There is no result `r`, so it is unclear what this proof means for {lean}`Q'`! + +So there are two reasonable options, inspired by non-termination in traditional program logics: + +1. _Total_ correctness interpretation: {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄` asserts that, given {lean}`P` holds, then {lean}`prog` terminates _and_ {lean}`Q'` holds for the result. +2. _Partial_ correctness interpretation: {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄` asserts that, given {lean}`P` holds, and _if_ {lean}`prog` terminates _then_ {lean}`Q'` holds for the result. + +The notation {lean}`⇓ r => Q' r` has the total interpretation (cf. {name}`PostCond.noThrow`), while {lean}`⇓? r => Q' r` has the partial interpretation (cf. {name}`PostCond.mayThrow`). + +{docstring Std.Do.PostCond} + +{docstring Std.Do.PostCond.noThrow} + +{docstring Std.Do.PostCond.mayThrow} + +:::syntax term (title := "Postconditions") (namespace := Std.Do) +```grammar +⇓ $_:term* => $_:term +``` + +```grammar +⇓? $_:term* => $_:term +``` +::: + +So in the running example, {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄` is unprovable, but {lean}`⦃P⦄ prog ⦃⇓? r => Q' r⦄` is trivially provable. +However, the binary choice suggests that there is actually a _spectrum_ of correctness properties to express. +The notion of postconditions {name}`PostCond` in `Std.Do` supports this spectrum. + +For example, suppose that our {name}`Supply` of fresh numbers is bounded and we want to throw an exception if the supply is exhausted. +Then {name}`mkFreshN` should throw an exception _only if_ the supply is indeed exhausted. +The following correctness property expresses this: + +```lean -show +namespace Exceptions +``` + +```lean +structure Supply where + counter : Nat + limit : Nat + property : counter ≤ limit + +def mkFresh : EStateM String Supply Nat := do + let supply ← get + if h : supply.counter = supply.limit then + throw s!"Supply exhausted: {supply.counter} = {supply.limit}" + else + let n := supply.counter + have := supply.property + set {supply with counter := n + 1, property := by omega} + pure n + +def mkFreshN (n : Nat) : EStateM String Supply (List Nat) := do + let mut acc := #[] + for _ in [:n] do + acc := acc.push (← mkFresh) + pure acc.toList + +@[spec] +theorem mkFresh_spec (c : Nat) : + ⦃fun state => ⌜state.counter = c⌝⦄ + mkFresh + ⦃post⟨fun r state => ⌜r = c ∧ c < state.counter⌝, + fun _ state => ⌜c = state.counter ∧ c = state.limit⌝⟩⦄ := by + mvcgen [mkFresh] with grind + +@[spec] +theorem mkFreshN_spec (n : Nat) : + ⦃⌜True⌝⦄ + mkFreshN n + ⦃post⟨fun r => ⌜r.Nodup⌝, + fun _msg state => ⌜state.counter = state.limit⌝⟩⦄ := by + mvcgen [mkFreshN] + invariants + · post⟨fun ⟨xs, acc⟩ state => + ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝, + fun _msg state => ⌜state.counter = state.limit⌝⟩ + with grind + +theorem mkFreshN_correct (n : Nat) : + match (mkFreshN n).run s with + | .ok l _ => l.Nodup + | .error _ s' => s'.counter = s'.limit := by + generalize h : (mkFreshN n).run s = x + apply EStateM.of_wp_run_eq h + mvcgen +``` + +Just as any {lean}`StateT σ`-like layer in the monad stack gives rise to a {lean}`PostShape.arg σ` layer in the {lean}`ps` +that {name}`WP` maps into, any {lean}`ExceptT ε`-like layer gives rise to a {lean}`PostShape.except ε` layer. + +Every {lean}`PostShape.arg σ` adds another `σ → ...` layer to the language of {lean}`Assertion`s. +Every {lean}`PostShape.except ε` leaves the {lean}`Assertion` language unchanged, but adds another exception +condition to the postcondition. + +{docstring Std.Do.Assertion} + +Hence the {name}`WP` instance for {lean}`EStateM ε σ` maps to the {name}`PostShape` {lean}`PostShape.except ε (.arg σ .pure)`, just +as for {lean}`ExceptT ε (StateM σ)`. + +```lean -show +end Exceptions +``` + +## Extending `mvcgen` with support for custom monads + +The {tactic}`mvcgen` framework is designed to be extensible. +None of the monads so far have in any way been hard-coded into {tactic}`mvcgen`. +Rather, {tactic}`mvcgen` relies on instances of the {name}`WP` and {name}`WPMonad` type class and user-provided specifications to generate verification conditions. + +The {name}`WP` instance defines the weakest precondition interpretation of a monad {lean}`m` into a predicate transformer {lean}`PredTrans ps`, +and the matching {name}`WPMonad` instance asserts that this translation distributes over the {name}`Monad` operations. + +{docstring Std.Do.PredTrans} + +{docstring Std.Do.WP} + +:::syntax term (title := "Weakest preconditions") (namespace := Std.Do) +```grammar +wp⟦ $_:term ⟧ +``` +::: + +{docstring Std.Do.WPMonad} + +:::example "Adding `mvcgen` support for Aeneas" (open := true) +Suppose one wants to use `mvcgen` to generate verification conditions for programs generated by [`Aeneas`](https://github.com/AeneasVerif/aeneas). +`Aeneas` translates Rust programs into Lean programs in the following {name}`Result` monad: + +```lean +inductive Error where + | integerOverflow: Error + -- ... more error kinds ... + +inductive Result (α : Type u) where + | ok (v: α): Result α + | fail (e: Error): Result α + | div + +instance Result.instMonad : Monad Result where + pure x := .ok x + bind x f := match x with + | .ok v => f v + | .fail e => .fail e + | .div => .div + +instance Result.instLawfulMonad : LawfulMonad Result := by + -- TODO: Replace sorry with grind when it no longer introduces section + -- variables + apply LawfulMonad.mk' <;> (simp only [Result.instMonad]; sorry) +``` + +Support for this monad is a matter of + +1. Adding a {name}`WP` and {name}`WPMonad` instance for {name}`Result` +2. Registering specification lemmas for the translation of basic Rust primitives such as addition etc. + +The first part is straightforward: + +```lean +instance Result.instWP : WP Result (.except Error .pure) where + wp x := match x with + | .ok v => wp (pure v : Except Error _) + | .fail e => wp (throw e : Except Error _) + | .div => PredTrans.const ⌜False⌝ + +-- set_option trace.Meta.synthInstance true in +instance Result.instWPMonad : WPMonad Result (.except Error .pure) where + wp_pure := by + intros + ext Q + simp [wp, PredTrans.pure, pure, Except.pure, Id.run] + wp_bind x f := by + simp only [instWP, bind] + ext Q + cases x <;> simp [PredTrans.bind, PredTrans.const] + +theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) : + (⊢ₛ wp⟦x⟧ post⟨fun a => ⌜P (.ok a)⌝, + fun e => ⌜P (.fail e)⌝⟩) → P x := by + intro hspec + simp only [instWP] at hspec + split at hspec <;> simp_all +``` + +The {name}`WP` instance above translates programs in {lean}`Result α` to predicate transformers in {lean}`PredTrans ps α`. +That is, a function in {lean}`PostCond α ps → Assertion ps`, mapping a postcondition to its weakest precondition. +Note that this definition of the {name}`WP` instance determines what properties can be derived from proved specifications via {lean}`Result.of_wp`. +This lemma defines what “weakest precondition” means. + +To exemplify the second part, here is an example definition of {name}`UInt32` addition in {name}`Result` that models integer overflow: + +```lean +instance : MonadExcept Error Result where + throw e := .fail e + tryCatch x h := match x with + | .ok v => pure v + | .fail e => h e + | .div => .div + +def addOp (x y : UInt32) : Result UInt32 := + if x.toNat + y.toNat ≥ UInt32.size then + throw .integerOverflow + else + pure (x + y) +``` + +There are two relevant specification lemmas to register: + +```lean +@[spec] +theorem Result.throw_spec {α Q} (e : Error) : + ⦃Q.2.1 e⦄ throw (m := Result) (α := α) e ⦃Q⦄ := id + +@[spec] +theorem addOp_ok_spec {x y} (h : x.toNat + y.toNat < UInt32.size) : + ⦃⌜True⌝⦄ + addOp x y + ⦃⇓ r => ⌜r = x + y ∧ (x + y).toNat = x.toNat + y.toNat⌝⦄ := by + mvcgen [addOp] with (simp_all; try grind) +``` + +This is already enough to prove the following example: + +```lean +example : + ⦃⌜True⌝⦄ + do let mut x ← addOp 1 3 + for _ in [:4] do + x ← addOp x 5 + return x + ⦃⇓ r => ⌜r.toNat = 24⌝⦄ := by + mvcgen + invariants + · ⇓⟨xs, x⟩ => ⌜x.toNat = 4 + 5 * xs.prefix.length⌝ + with (simp_all [UInt32.size]; try grind) +``` +::: + +## Proof mode for stateful goals + +```lean -show +variable {σs : List (Type u)} {H T : SPred σs} +``` + +It is a priority of {tactic}`mvcgen` to break down monadic programs into VCs that are straightforward to understand. +For example, when the monad stack is monomorphic and all loop invariants have been instantiated, an invocation of `all_goals mleave` should simplify away any `Std.Do.SPred` specific constructs and leave behind a goal that is easily understood by humans and `grind`. +This `all_goals mleave` step is carried out automatically by {tactic}`mvcgen` after loop invariants have been instantiated. + +However, there are times when `mleave` will be unable to remove all {name}`Std.Do.SPred` constructs. +In this case, verification conditions of the form {lean}`H ⊢ₛ T` will be left behind. +The assertion language {name}`Assertion` translates into an {name}`Std.Do.SPred` as follows: + +```lean -keep +abbrev PostShape.args : PostShape.{u} → List (Type u) + | .pure => [] + | .arg σ s => σ :: PostShape.args s + | .except _ s => PostShape.args s + +abbrev Assertion (ps : PostShape.{u}) : Type u := + SPred (PostShape.args ps) +``` + +{docstring Std.Do.SPred} + +{docstring Std.Do.SPred.entails} + +:::syntax term (title := "Notation for `SPred`") (namespace := Std.Do) +```grammar +⌜$_:term⌝ +``` + +```grammar +$_:term ⊢ₛ $_:term +``` + +```grammar +$_:term ⊣⊢ₛ $_:term +``` + +```grammar +spred($_:term ∧ $_:term) +``` + +```grammar +spred($_:term ∨ $_:term) +``` + +```grammar +spred($_:term → $_:term) +``` + +```grammar +spred(¬$_:term) +``` + +```grammar +spred(∀ $_:ident, $_:term) +``` + +```grammar +spred(∃ $_:ident, $_:term) +``` +::: + +A common case for when a VC of the form {lean}`H ⊢ₛ T` is left behind is when the base monad {lean}`m` is polymorphic. +In this case, the proof will depend on a {lean}`WP m ps` instance which governs the translation into the {name}`Assertion` language, but the exact correspondence to `σs : List (Type u)` is yet unknown. +To successfully discharge such a VC, `mvcgen` comes with an entire proof mode that is inspired by that of the Iris concurrent separation logic. +(In fact, the proof mode was adapted in large part from its Lean clone, [`iris-lean`](https://github.com/leanprover-community/iris-lean).) +The Lean 4 test file [`tests/lean/run/spredProofMode.lean`](https://github.com/leanprover/lean4/blob/76971a88fff3b3df75dceb588b5bd98b1552bafc/tests/lean/run/spredProofMode.lean) contains many examples of that proof mode to learn from, and {ref "tactic-ref-spred"}[the reference manual] contains a list of all proof mode tactics. + +## Further reading + +More examples can be found in Lean's test suite. +* [`tests/lean/run/doLogicTests.lean`](https://github.com/leanprover/lean4/blob/76971a88fff3b3df75dceb588b5bd98b1552bafc/tests/lean/run/doLogicTests.lean) is a kitchen sink test file with many examples. +* [`tests/lean/run/bhaviksSampler.lean`](https://github.com/leanprover/lean4/blob/76971a88fff3b3df75dceb588b5bd98b1552bafc/tests/lean/run/bhaviksSampler.lean) is a stubbed out example from a larger development due to Bhavik Mehta. +* [Markus Himmel's `human-eval-lean` project](https://github.com/TwoFX/human-eval-lean/) has a limited number of `mvcgen`-based proofs for imperative algorithm implementations. Contributions welcome! +* [Rish Vaishnav's ongoing `qsort` formalization](https://github.com/rish987/qsort/) is the largest example of `mvcgen` to date. From e382bacedd25b5c52a22e609695fd8f5783973fe Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 15 Oct 2025 22:47:29 +0200 Subject: [PATCH 2/4] Review and updates of mvcgen tutorial --- Manual/Meta.lean | 2 + Manual/Meta/Imports.lean | 26 ++ Manual/Meta/Namespace.lean | 31 ++ Manual/Monads/Syntax.lean | 6 + Manual/Papers.lean | 10 + Manual/VCGen.lean | 666 ++++++++++++++++++++++++------------- 6 files changed, 516 insertions(+), 225 deletions(-) create mode 100644 Manual/Meta/Imports.lean create mode 100644 Manual/Meta/Namespace.lean diff --git a/Manual/Meta.lean b/Manual/Meta.lean index b9d17aa13..ec3b04891 100644 --- a/Manual/Meta.lean +++ b/Manual/Meta.lean @@ -33,6 +33,8 @@ import Manual.Meta.Syntax import Manual.Meta.Tactics import Manual.Meta.SpliceContents import Manual.Meta.Markdown +import Manual.Meta.Imports +import Manual.Meta.Namespace open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets diff --git a/Manual/Meta/Imports.lean b/Manual/Meta/Imports.lean new file mode 100644 index 000000000..2f61cf632 --- /dev/null +++ b/Manual/Meta/Imports.lean @@ -0,0 +1,26 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + +import VersoManual +import Lean.Elab.InfoTree.Types +import SubVerso.Highlighting.Code + +open scoped Lean.Doc.Syntax + +open Verso Doc Elab +open Lean Elab +open Verso.Genre.Manual InlineLean Scopes +open Verso.SyntaxUtils +open SubVerso.Highlighting + +@[code_block] +def imports : CodeBlockExpanderOf Unit + | (), str => do + let altStr ← parserInputString str + let p := Parser.whitespace >> Parser.Module.header.fn + let headerStx ← p.parseString altStr + let hl ← highlight headerStx #[] {} + ``(Block.other (Block.lean $(quote hl) {}) #[Block.code $(quote str.getString)]) diff --git a/Manual/Meta/Namespace.lean b/Manual/Meta/Namespace.lean new file mode 100644 index 000000000..b32f2c63e --- /dev/null +++ b/Manual/Meta/Namespace.lean @@ -0,0 +1,31 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + +import VersoManual +import Lean.Elab.InfoTree.Types +import SubVerso.Highlighting.Code + +open scoped Lean.Doc.Syntax + +open Verso Doc Elab +open Lean Elab +open Verso.Genre.Manual InlineLean Scopes +open Verso.SyntaxUtils +open SubVerso.Highlighting + +@[role] +def «namespace» : RoleExpanderOf Unit + | (), #[arg] => do + let `(inline|code($s)) := arg + | throwErrorAt arg "Expected code" + -- TODO validate that namespace exists? Or is that too strict? + -- TODO namespace domain for documentation + ``(Inline.code $(quote s.getString)) + | _, more => + if h : more.size > 0 then + throwErrorAt more[0] "Expected code literal with the namespace" + else + throwError "Expected code literal with the namespace" diff --git a/Manual/Monads/Syntax.lean b/Manual/Monads/Syntax.lean index aa521b000..490c4635a 100644 --- a/Manual/Monads/Syntax.lean +++ b/Manual/Monads/Syntax.lean @@ -428,6 +428,9 @@ In addition to convenient support for sequential computations with data dependen These effects are implemented via transformations of the entire {keywordOf Lean.Parser.Term.do}`do` block in a manner akin to {tech}[monad transformers], rather than via a local desugaring. ## Early Return +%%% +tag := "early-return" +%%% Early return terminates a computation immediately with a given value. The value is returned from the closest containing {keywordOf Lean.Parser.Term.do}`do` block; however, this may not be the closest `do` keyword. @@ -452,6 +455,9 @@ Internally, the {keywordOf Lean.Parser.Term.do}`do` elaborator performs a transl On its own, {keywordOf Lean.Parser.Term.doReturn}`return` is short for {keywordOf Lean.Parser.Term.doReturn}`return`​` `​{lean}`()`. ## Local Mutable State +%%% +tag := "let-mut" +%%% Local mutable state is mutable state that cannot escape the {keywordOf Lean.Parser.Term.do}`do` block in which it is defined. The {keywordOf Lean.Parser.Term.doLet}`let mut` binder introduces a locally-mutable binding. diff --git a/Manual/Papers.lean b/Manual/Papers.lean index 670e5a413..c8c004590 100644 --- a/Manual/Papers.lean +++ b/Manual/Papers.lean @@ -60,6 +60,16 @@ def countingBeans : InProceedings where year := 2019 booktitle := inlines!"Proceedings of the 31st Symposium on Implementation and Application of Functional Languages (IFL 2019)" +def hoare69 : Article where + title := inlines!"An Axiomatic Basis for Computer Programming" + authors := #[inlines!"C. A. R. Hoare"] + journal := inlines!"Communications of the ACM" + year := 1969 + volume := inlines!"12" + number := inlines!"10" + month := none + pages := some (576, 583) + def pratt73 : InProceedings where title := inlines!"Top down operator precedence" authors := #[inlines!"Vaughan Pratt"] diff --git a/Manual/VCGen.lean b/Manual/VCGen.lean index e884a1bfd..9d3b62fb2 100644 --- a/Manual/VCGen.lean +++ b/Manual/VCGen.lean @@ -7,11 +7,13 @@ Author: Sebastian Graf import VersoManual import Manual.Meta +import Manual.Papers import Std.Tactic.Do open Verso.Genre Manual open Verso.Genre.Manual.InlineLean +open Verso.Code.External (lit) set_option pp.rawOnError true @@ -29,38 +31,65 @@ open Manual (comment) #doc (Manual) "The `mvcgen` tactic" => %%% tag := "mvcgen-tactic" +htmlSplit := .never %%% The {tactic}`mvcgen` tactic implements a _monadic verification condition generator_: -It breaks down a goal involving a program written using Lean's imperative `do` notation into a number of pure _verification conditions_ (VCs) that discharge said goal. +It breaks down a goal involving a program written using Lean's imperative {keywordOf Lean.Parser.Term.do}`do` notation into a number of pure {deftech}_verification conditions_ ({deftech}[VCs]) that discharge said goal. A verification condition is a sub-goal that does not mention the monad underlying the `do` block. -In order to use the {tactic}`mvcgen` tactic, `Std.Tactic.Do` must be imported and the namespace `Std.Do` must be opened. +In order to use the {tactic}`mvcgen` tactic, {module}`Std.Tactic.Do` must be imported and the namespace {namespace}`Std.Do` must be opened. -``` + +# Verifying Imperative Programs Using `mvcgen` + +This section is a tutorial that introduces the most important concepts of {tactic}`mvcgen` top-down. +Recall that you need to import {module}`Std.Tactic.Do` and open {namespace}`Std.Do` to run these examples: + +```imports import Std.Tactic.Do +``` +```lean open Std.Do ``` -# Verifying imperative programs using `mvcgen` +## Preconditions and Postconditions -This section is a tutorial introducing the most important concepts of {tactic}`mvcgen` top-down. -Recall that you need to import `Std.Tactic.Do` and open `Std.Do` to run these examples. +One style in which program specifications can be written is to provide a {deftech}_precondition_, which the program's caller is expected to ensure, and a {deftech}_postcondition_, which the program itself is expected to ensure. +The program is correct if running it when the precondition holds always results in the postcondition holding. -```lean -show -open Std.Do -``` +In general, many different preconditions might suffice for a program to ensure the postcondition. +After all, new preconditions can be generated by replacing a precondition $`P` with $`P \wedge Q`. +The {deftech}_weakest precondition_ is a precondition that is implied by all other preconditions. + +One way to prove something about the result of a program is to find the weakest precondition that guarantees the desired result, and then to show that this weakest precondition is simply true. +This means that the postcondition holds no matter what. + + +## Loops and Invariants + +:::leanFirst +As a first example of {tactic}`mvcgen`, the function {name}`mySum` computes the sum of an array using {ref "let-mut"}[local mutable state] and a {keywordOf Lean.Parser.Term.doFor}`for` loop: -:::example "Array Sum" (open := true) (keep := true) -As a “hello world” to {tactic}`mvcgen`, the following example {name}`mySum` computes the sum of an array using local mutability and a `for` loop. -Then it proves {name}`mySum` correct relative to {name}`Array.sum`, requiring us to specify an invariant for the loop: ```lean def mySum (l : Array Nat) : Nat := Id.run do let mut out := 0 for i in l do out := out + i return out +``` +::: + +If {name}`mySum` is correct, then it is equal to {name}`Array.sum`. +In {name}`mySum`, the use of {keywordOf Lean.Parser.Term.do}`do` is an internal implementation detail—the function's signature makes no mention of any monad. +Thus, the proof first manipulates the goal into a form that is amenable to the use of {tactic}`mvcgen`, using the lemma {name}`Id.of_wp_run_eq`. +This lemma states that facts about the result of running a computation in the {name}`Id` monad that terminates normally (that is, does not use {ref "early-return"}[early return]) can be proved by showing that the {tech}[weakest precondition] that ensures the desired result is true. +Next, the proof uses {tactic}`mvcgen` to replace the formulation in terms of weakest preconditions with a set of {tech}[verification conditions]. +While {tactic}`mvcgen` is mostly automatic, it does require an invariant for the loop. +A {deftech}_loop invariant_ is a statement that is both assumed and guaranteed by the body of the loop; if it is true when the loop begins, then it will be true when the loop terminates. + +```lean theorem mySum_correct (l : Array Nat) : mySum l = l.sum := by -- Focus on the part of the program with the `do` block (`Id.run ...`) generalize h : mySum l = x @@ -93,15 +122,19 @@ theorem mySum_correct (l : Array Nat) : mySum l = l.sum := by case vc3 h => grind ``` + +:::paragraph Note that the case labels are actually unique prefixes of the full case labels. -Whenever referring to cases, only this prefix should be used; the suffix is merely a poor man's hint to the user where that particular VC came from. -For example, +Whenever referring to cases, only this prefix should be used; the suffix is merely a hint to the user of where that particular {tech}[VC] came from. +For example: -* `vc1.step` conveys that this VC proves the inductive step for the loop -* `vc2.a.pre` is meant to prove that the hypotheses of a goal implies the precondition of a specification (of {name}`forIn`). -* `vc3.a.post` is meant to prove that the postcondition of a specification (of {name}`forIn`) implies the target of the goal. +* `vc1.step` conveys that this {tech}[VC] proves the inductive step for the loop +* `vc2.a.pre` is meant to prove that the hypotheses of a goal imply the precondition of a specification (of {name}`forIn`). +* `vc3.a.post` is meant to prove that the postcondition of a specification (of {name}`forIn`) implies the desired property. +::: -After specifying the loop invariant, the proof can be shortened to just `all_goals mleave; grind` (cf. {tactic}`mleave`). +:::paragraph +After specifying the loop invariant, the proof can be shortened to just {keyword}`all_goals mleave; grind` (where {tactic}`mleave` leaves the stateful proof mode, cleaning up the proof state). ```lean theorem mySum_correct_short (l : Array Nat) : mySum l = l.sum := by generalize h : mySum l = x @@ -110,7 +143,7 @@ theorem mySum_correct_short (l : Array Nat) : mySum l = l.sum := by case inv1 => exact ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝ all_goals mleave; grind ``` -This pattern is in fact so popular that `mvcgen` comes with special syntax for it: +This pattern is so common that {tactic}`mvcgen` comes with special syntax for it: ```lean theorem mySum_correct_shorter (l : Array Nat) : mySum l = l.sum := by generalize h : mySum l = x @@ -120,11 +153,12 @@ theorem mySum_correct_shorter (l : Array Nat) : mySum l = l.sum := by · ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝ with grind ``` -The `mvcgen invariants ... with ...` expands to the same syntax as the -tactic sequence `mvcgen; case inv1 => ...; all_goals mleave; grind` +The {keyword}`mvcgen invariants `{lit}`...`{keyword}` with `{lit}`...` is an abbreviation for the +tactic sequence {keyword}`mvcgen; case`{lit}` inv1 => ...`{keyword}`; all_goals mleave; grind` above. It is the form that we will be using from now on. ::: +:::paragraph It is helpful to compare the proof of {name}`mySum_correct_shorter` to a traditional correctness proof: ```lean @@ -138,31 +172,33 @@ theorem mySum_correct_vanilla (l : Array Nat) : mySum l = l.sum := by -- Grind away induction l with grind ``` +::: -This proof is similarly succinct as the proof in {name}`mySum_correct_shorter` using {tactic}`mvcgen`. +:::paragraph +This proof is similarly succinct as the proof in {name}`mySum_correct_shorter` that uses {tactic}`mvcgen`. However, the traditional approach relies on important properties of the program: -* The `for` loop does not `break` or `return` early. Otherwise, the `forIn` could not be rewritten to a `foldl`. -* The loop body `(· + ·)` is small enough to be repeated in the proof. -* The loop body is `pure`, that is, does not perform any effects. - (Indeed, all computations in the base monad `Id` factor through `pure`.) - While `forIn` could still be rewritten to a `foldlM`, reasoning about the monadic loop body can be tough for `grind`. +* The {keywordOf Lean.Parser.Term.doFor}`for` loop does not {keywordOf Lean.Parser.Term.doBreak}`break` or {keywordOf Lean.Parser.Term.doReturn}`return` early. Otherwise, the {name}`forIn` could not be rewritten to a {name Array.foldl}`foldl`. +* The loop body {lean (type := "Nat → Nat → Nat")}`(· + ·)` is small enough to be repeated in the proof. +* The loop body does not carry out any effects in the underlying monad (that is, the only effects are those introduced by {keywordOf Lean.Parser.Term.do}`do`-notation). + The {name}`Id` monad has no effects, so all of its comptutations are pure. + While {name}`forIn` could still be rewritten to a {name Array.foldlM}`foldlM`, reasoning about the monadic loop body can be tough for {tactic}`grind`. In the following sections, we will go through several examples to learn about {tactic}`mvcgen` and its support library, and also see where traditional proofs become difficult. -This is usually caused by +This is usually caused by: -* `do` blocks using control flow constructs such as `for` loops, `break`s and early `return`. -* Effectful computations in non-`Id` monads. - Such computations affect the implicit monadic context (state, exceptions) in ways that need to be reflected in loop invariants. +* {keywordOf Lean.Parser.Term.do}`do` blocks using control flow constructs such as {keywordOf Lean.Parser.Term.doFor}`for` loops, {keywordOf Lean.Parser.Term.doBreak}`break`s and early {keywordOf Lean.Parser.Term.doReturn}`return`. +* The use of effects in non-{name}`Id` monads, which affects the implicit monadic context (state, exceptions) in ways that need to be reflected in loop invariants. {tactic}`mvcgen` scales to these challenges with reasonable effort. -## Control flow +::: -Let us consider another example that combines `for` loops with an early return. +## Control Flow -:::example "Detecting Duplicates in a List" (open := true) (keep := true) -Recall that {name}`List.Nodup` is a predicate that asserts that a given list does not contain any duplicates. +:::leanFirst +Let us consider another example that combines {keywordOf Lean.Parser.Term.doFor}`for` loops with an early return. +{name}`List.Nodup` is a predicate that asserts that a given list does not contain any duplicates. The function {name}`nodup` below decides this predicate: ```lean @@ -173,7 +209,14 @@ def nodup (l : List Int) : Bool := Id.run do return false seen := seen.insert x return true +``` +::: +:::paragraph +This function is correct if it returns {name}`true` for every list that satisfies {name}`List.Nodup` and {name}`false` for every list that does not. +Just as it was in {name}`mySum`, the use of {keywordOf Lean.Parser.Term.do}`do`-notation and the {name}`Id` monad is an internal implementation detail of {name}`nodup`. +Thus, the proof begins by using {name}`Id.of_wp_run_eq` to make the proof state amenable to {tactic}`mvcgen`: +```lean theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by generalize h : nodup l = r apply Id.of_wp_run_eq h @@ -187,19 +230,32 @@ theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by ``` ::: -The proof has the same succinct structure as for the initial {name}`mySum` example, because we again offload all proofs to {tactic}`grind` and its existing framework around {name}`List.Nodup`. -Therefore, the only difference is in the invariant. -Since our loop has an early return, we construct the invariant using the helper function {lean}`Invariant.withEarlyReturn`. + +:::paragraph +```lean -show +section +variable {l : List Int} {ret : Bool} {seen : Std.HashSet Int} {xs : l.Cursor} +axiom onReturn : Bool → Std.HashSet Int → SPred PostShape.pure.args +axiom onContinue : l.Cursor → Std.HashSet Int → SPred PostShape.pure.args +axiom onExcept : ExceptConds PostShape.pure +``` +The proof has the same succinct structure as for the initial {name}`mySum` example, because we again offload all proofs to {tactic}`grind` and its existing automation around {name}`List.Nodup`. +Therefore, the only difference is in the {tech}[loop invariant]. +Since our loop has an {ref "early-return"}[early return], we construct the invariant using the helper function {lean}`Invariant.withEarlyReturn`. This function allows us to specify the invariant in three parts: -* `onReturn ret seen` holds after the loop was left through an early return with value `ret`. +* {lean}`onReturn ret seen` holds after the loop was left through an early return with value {lean}`ret`. In case of {name}`nodup`, the only value that is ever returned is {name}`false`, in which case {name}`nodup` has decided there _is_ a duplicate in the list. -* `onContinue xs seen` is the regular induction step that proves the invariant is preserved each loop iteration. - The iteration state is captured by the cursor `xs`. - The given example asserts that the set `seen` contains all the elements of previous loop iterations and asserts that there were no duplicates so far. -* `onExcept` must hold when the loop throws an exception. - There are no exceptions in `Id`, so we leave it unspecified to use the default. +* {lean}`onContinue xs seen` is the regular induction step that proves the invariant is preserved each loop iteration. + The iteration state is captured by the cursor {lean}`xs`. + The given example asserts that the set {lean}`seen` contains all the elements of previous loop iterations and asserts that there were no duplicates so far. +* {lean}`onExcept` must hold when the loop throws an exception. + There are no exceptions in {lean}`Id`, so we leave it unspecified to use the default. (Exceptions will be discussed at a later point.) +```lean -show +end +``` +::: :::TODO Note that the form `mvcgen invariants?` would hint that {name}`Invariant.withEarlyReturn` is a useful way to construct the invariant: @@ -211,6 +267,7 @@ example (l : List Int) : nodup l ↔ l.Nodup := by ``` ::: +:::paragraph Now consider the following direct (and excessively golfed) proof without {tactic}`mvcgen`: ```lean @@ -222,27 +279,39 @@ theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by clear hseen induction l generalizing seen with grind [Id.run_pure, Id.run_bind] ``` +::: +:::paragraph Some observations: * The proof is even shorter than the one with {tactic}`mvcgen`. -* The use of {tactic}`generalize` to generalize the accumulator relies on there being exactly one occurrence of `∅` to generalize. If that were not the case, we would have to copy parts of the program into the proof. This is a no go for larger functions. +* The use of {tactic}`generalize` to generalize the accumulator relies on there being exactly one occurrence of {lean (type := "Std.HashSet Int")}`∅` to generalize. If that were not the case, we would have to copy parts of the program into the proof. This is a no-go for larger functions. * {tactic}`grind` splits along the control flow of the function and reasons about {name}`Id`, given the right lemmas. - While this works for {name}`Id.run_pure` and {name}`Id.run_bind`, it would not work for {name}`Id.run_seq`, for example, because that lemma is not E-matchable. If {tactic}`grind` would fail, we would be forced to do all the control flow splitting and monadic reasoning by hand until {tactic}`grind` can pick up again. + While this works for {name}`Id.run_pure` and {name}`Id.run_bind`, it would not work for {name}`Id.run_seq`, for example, because that lemma is not {tech (key := "E-matching")}[E-matchable]. + If {tactic}`grind` would fail, we would be forced to do all the control flow splitting and monadic reasoning by hand until {tactic}`grind` could pick up again. +::: -The usual way to avoid replicating the control flow of a definition under proof is to use the {tactic}`fun_cases` or {tactic}`fun_induction` tactics. -Unfortunately, {tactic}`fun_cases` does not help with control flow inside a {name}`forIn` application, for example. -This is in contrast to {tactic}`mvcgen`, which ships with support for many {name}`forIn` implementations and is easily extended with `@[spec]` annotations for custom {name}`forIn` implementations. -Furthermore, a {tactic}`mvcgen`-powered proof will never need to copy any part of the original program. +The usual way to avoid replicating the control flow of a definition in a proof is to use the {tactic}`fun_cases` or {tactic}`fun_induction` tactics. +Unfortunately, {tactic}`fun_cases` does not help with control flow inside a {name}`forIn` application. +The {tactic}`mvcgen` tactic, on the other hand, ships with support for many {name}`forIn` implementations. +It can easily be extended (with {attrs}`@[spec]` annotations) to support custom {name}`forIn` implementations. +Furthermore, an {tactic}`mvcgen`-powered proof will never need to copy any part of the original program. -## Compositional reasoning about effectful programs using Hoare triples +## Compositional Reasoning About Effectful Programs Using Hoare Triples -The previous examples reasoned about functions defined using `Id.run do ` to make use of local mutability and early return in ``. -However, real-world programs often use `do` notation and monads `M` to hide away state and failure conditions as implicit “effects”. -In this use case, functions usually omit the `M.run`. -Instead they have monadic return type `M α` and compose well with other functions of that return type. +:::leanSection +```lean -show +variable (M : Type u → Type v) [Monad M] (α : Type u) +axiom M.run : M α → β → α +``` +The previous examples reasoned about functions defined using {lean}`Id.run`{lit}` `{keywordOf Lean.Parser.Term.do}`do`{lit}` ` to make use of local mutability and early return in {lit}``. +However, real-world programs often use {keywordOf Lean.Parser.Term.do}`do` notation and monads {lean}`M` to hide away state and failure conditions as implicit “effects”. +In this use case, functions usually omit the {name}`M.run`. +Instead they have a monadic return type {lean}`M α` and compose well with other functions of that return type. +In other words, the monad is part of the function's _interface_, not merely its implementation. +::: -:::example "Generating Fresh Numbers" (open := true) (keep := true) +:::leanFirst Here is an example involving a stateful function {name}`mkFresh` that returns auto-incremented counter values: ```lean @@ -251,7 +320,7 @@ structure Supply where def mkFresh : StateM Supply Nat := do let n ← (·.counter) <$> get - modify (fun s => {s with counter := s.counter + 1}) + modify fun s => { s with counter := s.counter + 1 } pure n def mkFreshN (n : Nat) : StateM Supply (List Nat) := do @@ -260,10 +329,19 @@ def mkFreshN (n : Nat) : StateM Supply (List Nat) := do acc := acc.push (← mkFresh) pure acc.toList ``` +::: + +::::leanFirst +:::leanSection +```lean -show +variable (n : Nat) +``` -`mkFreshN n` returns `n` “fresh” numbers, modifying the internal {name}`Supply` state through {name}`mkFresh`. +{lean}`mkFreshN n` returns {lean}`n` “fresh” numbers, modifying the internal {name}`Supply` state through {name}`mkFresh`. Here, “fresh” refers to all previously generated numbers being distinct from the next generated number. -We can formulate and prove a correctness property {name}`mkFreshN_correct` in terms of {name}`List.Nodup`: +We can formulate and prove a correctness property {name}`mkFreshN_correct` in terms of {name}`List.Nodup`: the returned list of numbers should contain no duplicates. +In this proof, {name}`StateM.of_wp_run'_eq` serves the same role that {name}`Id.of_wp_run_eq` did in the preceding examples. +::: ```lean theorem mkFreshN_correct (n : Nat) : ((mkFreshN n).run' s).Nodup := by @@ -284,105 +362,113 @@ theorem mkFreshN_correct (n : Nat) : ((mkFreshN n).run' s).Nodup := by ⌜(∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup⌝ with grind ``` -::: - -## Composing specifications +:::: -Nested unfolding of definitions as in `mvcgen [mkFreshN, mkFresh]` is quite blunt but effective for small programs. -A more compositional way is to develop individual _specification lemmas_ for each monadic function. -These can either be passed as arguments to {tactic}`mvcgen` or registered in a global (or `scoped`, or `local`) database of specifications using the `@[spec]` attribute: - -:::example "Decomposing a Proof into Specifications" (open := true) (keep := true) -```lean -@[spec] -theorem mkFresh_spec (c : Nat) : - ⦃fun state => ⌜state.counter = c⌝⦄ - mkFresh - ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by - -- Unfold `mkFresh` and blast away: - mvcgen [mkFresh] with grind - -@[spec] -theorem mkFreshN_spec (n : Nat) : - ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by - -- `mvcgen [mkFreshN, mkFresh_spec]` if `mkFresh_spec` were not - -- registered with `@[spec]` - mvcgen [mkFreshN] - invariants - -- As before: - · ⇓⟨xs, acc⟩ state => - ⌜(∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup⌝ - with grind +### Hoare Triples -theorem mkFreshN_correct_compositional (n : Nat) : - ((mkFreshN n).run' s).Nodup := - -- The type `⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄` of `mkFreshN` is - -- definitionally equal to - -- `∀ (n : Nat) (s : Supply), True → ((mkFreshN n).run' s).Nodup` - mkFreshN_spec n s True.intro +:::::leanSection +```lean -show +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} [Monad m] [WP m ps] {α σ ε : Type u} {P : Assertion ps} {Q : PostCond α ps} {prog : m α} {c : Nat} ``` +A {deftech}_Hoare triple_{citep hoare69}[] consists of a precondition, a statement, and a postcondition; it asserts that if the precondition holds, then the postcondition holds after running the statement. +In Lean syntax, this is written {lean}`⦃ P ⦄ prog ⦃ Q ⦄`, where {lean}`P` is the precondition, {typed}`prog : m α` is the statement, and {lean}`Q` is the postcondition. +{lean}`P` and {lean}`Q` are written in an assertion language that is determined by the specific monad {lean}`m`.{margin}[In particular, monad's instance of the type class {name}`WP` specifies the ways in which assertions may refer to the monad's state or the exceptions it may throw.] + +:::leanSection ```lean -show -variable {c : Nat} +variable {stmt1 stmt2 : m PUnit} {ps : PostShape.{0}} {P : Assertion ps} {Q : PostCond Unit ps} {P' : Assertion ps} {Q' : PostCond Unit ps} ``` -Here, the notation {lean}`⦃fun state => ⌜state.counter = c⌝⦄ mkFresh ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄` denotes a _Hoare triple_ (cf. {name}`Std.Do.Triple`). -Specifications for monadic functions always have such a Hoare triple result type. -::: - -## Hoare triples -{docstring Std.Do.Triple} +Specifications as Hoare triples are compositional because they allow statements to be sequenced. +Given {lean}`⦃P⦄ stmt1 ⦃Q⦄` and {lean}`⦃P'⦄ stmt2 ⦃Q'⦄`, if {lean}`Q` implies {lean}`P'` then {lean}`⦃P⦄ (do stmt1; stmt2) ⦃Q'⦄`. +Just as proofs about ordinary functions can rely on lemmas about the functions that they call, proofs about monadic programs can use lemmas that are specified in terms of Hoare triples. +::: -:::syntax term (title := "Hoare triple") (namespace := Std.Do) -```grammar -⦃ term ⦄ term ⦃ term ⦄ +::::paragraph +One suitable specification for {name}`mkFresh` as a Hoare triple is this translation of {name}`mkFreshN_correct`: +:::leanSection +```lean -show +variable {n : Nat} +``` +```leanTerm +⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ ``` ::: +```lean -show +variable {p : Prop} +``` +Corner brackets embed propositions into the monadic assertion language, so {lean}`⌜p⌝` is the assertion of the proposition {lean}`p`. +The precondition {lean}`⌜True⌝` asserts that {lean}`True` is true; this trivial precondition is used to state that the specification imposes no requirements on the state in which it is called. +The postcondition states that the result value is a list with no duplicate elements. +:::: -{docstring Std.Do.Triple.and} - -{docstring Std.Do.Triple.mp} - +::::paragraph +A specification for the single-step {name}`mkFresh` describes its effects on the monad's state: +:::leanSection ```lean -show -universe u v -variable {m : Type u → Type v} {ps : PostShape.{u}} [WP m ps] {α σ ε : Type u} {P : Assertion ps} {Q : PostCond α ps} {prog : m α} +variable {n : Nat} ``` -Given the meaning of Hoare triples above, the specification theorem for {name}`mkFresh` says: +```leanTerm +∀ (c : Nat), +⦃fun state => ⌜state.counter = c⌝⦄ +mkFresh +⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ +``` +When working in a state monad, preconditions may be parameterized over the value of the state prior to running the code. +Here, the universally quantified {name}`Nat` is used to _relate_ the initial state to the final state; the precondition is used to connect it the initial state. +Similarly, the postcondition may also accept the final state as a parameter. +This Hoare triple states: > If {lean}`c` refers to the {name}`Supply.counter` field of the {name}`Supply` prestate, then running {name}`mkFresh` returns {lean}`c` and modifies the {name}`Supply.counter` of the poststate to be larger than {lean}`c`. Note that this specification is lossy: {name}`mkFresh` could increment its state by an arbitrary non-negative amount and still satisfy the specification. This is good, because specifications may _abstract over_ uninteresting implementation details, ensuring resilient and small proofs. +::: +:::: -Hoare triples are defined in terms of a logic of stateful predicates plus a weakest precondition semantics {lean}`wp⟦prog⟧` that translates monadic programs into this logic: -```lean +:::paragraph +Hoare triples are defined in terms of a logic of stateful predicates plus a {tech}[weakest precondition] semantics {lean}`wp⟦prog⟧` that translates monadic programs into this logic. +A weakest precondition semantics is an interpretation of programs as mappings from postconditions to the weakest precondition that the program would require to ensure the postcondition; in this interpretation, programs are understood as _predicate transformers_. +The Hoare triple syntax is notation for {name}`Std.Do.Triple`: + +```lean -keep -- This is the definition of Std.Do.Triple: def Triple [WP m ps] {α : Type u} (prog : m α) (P : Assertion ps) (Q : PostCond α ps) : Prop := P ⊢ₛ wp⟦prog⟧ Q ``` +::: +```lean -show +variable {σ : Type u} +``` +:::paragraph The {name}`WP` type class maps a monad {lean}`m` to its {name}`PostShape` {lean}`ps`, and this {name}`PostShape` governs the exact shape of the {name}`Std.Do.Triple`. Many of the standard monad transformers such as {name}`StateT`, {name}`ReaderT` and {name}`ExceptT` come with a canonical {name}`WP` instance. -For example, `StateT σ` comes with a {name}`WP` instance that adds a `σ` argument to every {name}`Assertion`. -Stateful entailment `⊢ₛ` eta-expands through these additional `σ` arguments. +For example, {lean}`StateT σ` comes with a {name}`WP` instance that adds a {lean}`σ` argument to every {name}`Assertion`. +Stateful entailment `⊢ₛ` eta-expands through these additional {lean}`σ` arguments. For {name}`StateM` programs, the following type is definitionally equivalent to {name}`Std.Do.Triple`: ```lean def StateMTriple {α σ : Type u} (prog : StateM σ α) (P : σ → ULift Prop) (Q : (α → σ → ULift Prop) × PUnit) : Prop := ∀ s, (P s).down → let (a, s') := prog.run s; (Q.1 a s').down - +``` +```lean -show example : @StateMTriple α σ = Std.Do.Triple (m := StateM σ) := rfl ``` +::: + ```lean -show variable {p : Prop} ``` -The common postcondition notation `⇓ r => ...` injects an assertion of type `α → Assertion ps` into -`PostCond ps` (the `⇓` is meant to be parsed like `fun`); in case of {name}`StateM` by adjoining it with an empty tuple {name}`PUnit.unit`. +The common postcondition notation `⇓ r => ...` injects an assertion of type {lean}`α → Assertion ps` into +{lean}`PostCond α ps` (the `⇓` is meant to be parsed like `fun`); in case of {name}`StateM` by adjoining it with an empty tuple {name}`PUnit.unit`. The shape of postconditions becomes more interesting once exceptions enter the picture. The notation {lean}`⌜p⌝` embeds a pure hypotheses {lean}`p` into a stateful assertion. Vice versa, any stateful hypothesis {lean}`P` is called _pure_ if it is equivalent to {lean}`⌜p⌝` @@ -390,95 +476,178 @@ for some {lean}`p`. Pure, stateful hypotheses may be freely moved into the regular Lean context and back. (This can be done manually with the {tactic}`mpure` tactic.) -### An advanced note about pure preconditions and a notion of frame rule +::::: + +### Composing Specifications + +Nested unfolding of definitions as in {tactic}`mvcgen`{lit}` [`{name}`mkFreshN`{lit}`, `{name}`mkFresh`{lit}`]` is quite blunt but effective for small programs. +A more compositional way is to develop individual {deftech}_specification lemmas_ for each monadic function. +A specification lemma is a Hoare triple that is automatically used during {tech}[verification condition] generation to obtain the pre- and postconditions of each statement in a {keywordOf Lean.Parser.Term.do}`do`-block. +When the system cannot automatically prove that the postcondition of one statement implies the precondition of the next, then this missing reasoning step becomes a verification condition. + +:::paragraph +Specification lemmas can either be passed as arguments to {tactic}`mvcgen` or registered in a global (or {keyword}`scoped`, or {keyword}`local`) database of specifications using the {attrs}`@[spec]` attribute: + +```lean +@[spec] +theorem mkFresh_spec (c : Nat) : + ⦃fun state => ⌜state.counter = c⌝⦄ + mkFresh + ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by + -- Unfold `mkFresh` and blast away: + mvcgen [mkFresh] with grind + +@[spec] +theorem mkFreshN_spec (n : Nat) : + ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by + -- `mvcgen [mkFreshN, mkFresh_spec]` if `mkFresh_spec` were not + -- registered with `@[spec]` + mvcgen [mkFreshN] + invariants + -- As before: + · ⇓⟨xs, acc⟩ state => + ⌜(∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup⌝ + with grind +``` +::: + +:::paragraph +The original correctness theorem can now be proved using {tactic}`mvcgen` alone: +```lean +theorem mkFreshN_correct_compositional (n : Nat) : + ((mkFreshN n).run' s).Nodup := by + generalize h : (mkFreshN n).run' s = x + apply StateM.of_wp_run'_eq h + mvcgen +``` +The specification lemma {name}`mkFreshN_spec` is automatically used by {tactic}`mvcgen`. +::: + + +### An Advanced Note About Pure Preconditions and a Notion of Frame Rule This subsection is a bit of a digression and can be skipped on first reading. -Say the specification for some [`Aeneas`](https://github.com/AeneasVerif/aeneas)-inspired monadic addition function `x +? y : M UInt8` has the +:::leanSection +```lean -show +axiom M : Type → Type +variable {x y : UInt8} [Monad M] [WP M .pure] +def addQ (x y : UInt8) : M UInt8 := pure (x + y) +local infix:1023 " +? " => addQ +axiom dots {α} : α +local notation "…" => dots +``` +Say the specification for some [`Aeneas`](https://github.com/AeneasVerif/aeneas)-inspired monadic addition function {typed}`x +? y : M UInt8` has the requirement that the addition won't overflow, that is, `h : x.toNat + y.toNat ≤ UInt8.size`. Should this requirement be encoded as a regular Lean hypothesis of the specification (`add_spec_hyp`) or should this requirement be encoded as a pure precondition of the Hoare triple, using `⌜·⌝` notation (`add_spec_pre`)? -``` -theorem add_spec_hyp (x y : UInt8) (h : x.toNat + y.toNat ≤ UInt8.size) : - ⦃⌜True⌝⦄ x +? y ⦃⇓ r => ⌜r.toNat = x.toNat + y.toNat⌝⦄ := ... +```lean +theorem add_spec_hyp (x y : UInt8) + (h : x.toNat + y.toNat ≤ UInt8.size) : + ⦃⌜True⌝⦄ x +? y ⦃⇓ r => ⌜r.toNat = x.toNat + y.toNat⌝⦄ := … theorem add_spec_pre (x y : UInt8) : ⦃⌜x.toNat + y.toNat ≤ UInt8.size⌝⦄ x +? y - ⦃⇓ r => ⌜r.toNat = x.toNat + y.toNat⌝⦄ := ... + ⦃⇓ r => ⌜r.toNat = x.toNat + y.toNat⌝⦄ := … ``` +::: + The first approach is advisable, although it should not make a difference in practice. The VC generator will move pure hypotheses from the stateful context into the regular Lean context, so the second form turns effectively into the first form. -This is referred to as _framing_ hypotheses (cf. the {tactic}`mpure` and {tactic}`mframe` tactics). -Hypotheses in the Lean context are part of the immutable _frame_ of the stateful logic, because in contrast to stateful hypotheses they survive the rule of consequence. +This is referred to as {deftech}_framing_ hypotheses (cf. the {tactic}`mpure` and {tactic}`mframe` tactics). +Hypotheses in the Lean context are part of the immutable {deftech}_frame_ of the stateful logic, because in contrast to stateful hypotheses they survive the rule of consequence. -## Monad transformer stacks +## Monad Transformers and Lifting -Real-world programs often orchestrate the interaction of independent subsystems through a stack of monad transformers. +Real-world programs often use monads that are built from multiple {tech}[monad transformers], with operations being frequently {ref "lifting-monads"}[lifted] from one monad to another. +Verification of these programs requires taking this into account. We can tweak the previous example to demonstrate this. ```lean -show -namespace Stack +namespace Transformers variable {m : Type → Type} {α : Type} {ps : PostShape.{0}} attribute [-instance] Lake.instMonadLiftTOfMonadLift_lake ``` -:::example "Transformer Stacks" (open := true) (keep := true) -Suppose that {name}`mkFresh` is generalized to work in any base monad {lean}`m` under {lean}`StateT Supply`. -Furthermore, {name}`mkFreshN` is defined in terms of a concrete monad transformer stack {name}`AppM` and lifts {name}`mkFresh` into {name}`AppM`. -Then the {tactic}`mvcgen`-based proof goes through unchanged: +::::paragraph +:::leanFirst +Now, there is an application with two separate monads, both built using transformers: +```lean +abbrev CounterM := StateT Supply (ReaderM String) + +abbrev AppM := StateT Bool CounterM +``` +Instead of using {lean}`StateM Supply`, {name}`mkFresh` uses {lean}`CounterM`: ```lean -def mkFresh [Monad m] : StateT Supply m Nat := do +def mkFresh : CounterM Nat := do let n ← (·.counter) <$> get - modify (fun s => {s with counter := s.counter + 1}) + modify fun s => { s with counter := s.counter + 1 } pure n +``` -abbrev AppM := StateT Bool (StateT Supply (ReaderM String)) -abbrev liftCounterM : StateT Supply (ReaderM String) α → AppM α := liftM - +{name}`mkFreshN` is defined in terms of {name}`AppM`, which includes multiple states and a reader effect. +The definition of {name}`mkFreshN` lifts {name}`mkFresh` into {name}`AppM`: +```lean def mkFreshN (n : Nat) : AppM (List Nat) := do let mut acc := #[] for _ in [:n] do - let n ← liftCounterM mkFresh + let n ← mkFresh acc := acc.push n return acc.toList +``` +::: +:::: +::::paragraph +Then the {tactic}`mvcgen`-based proof goes through unchanged: +```lean @[spec] -theorem mkFresh_spec [Monad m] [WPMonad m ps] (c : Nat) : +theorem mkFresh_spec (c : Nat) : ⦃fun state => ⌜state.counter = c⌝⦄ - mkFresh (m := m) + mkFresh ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by - mvcgen [mkFresh] with grind + --TODO: mvcgen [mkFresh] with grind + sorry @[spec] theorem mkFreshN_spec (n : Nat) : ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by -- `liftCounterM` here ensures unfolding - mvcgen [mkFreshN, liftCounterM] + mvcgen [mkFreshN] invariants · ⇓⟨xs, acc⟩ _ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝ with grind ``` +:::: +:::leanSection +```lean -show +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} [WP m ps] {α : Type u} {prog : m α} +``` The {name}`WPMonad` type class asserts that {lean}`wp⟦prog⟧` distributes over the {name}`Monad` operations (“monad morphism”). This proof might not look much more exciting than when only a single monad was involved. -However, under the radar of the user the proof builds on a cascade of specifications for `MonadLift` instances. +However, under the radar of the user the proof builds on a cascade of specifications for {name}`MonadLift` instances. + ::: ```lean -show -end Stack +end Transformers ``` ## Exceptions +::::leanSection ```lean -show -variable {Q' : α → Assertion ps} +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} [WP m ps] {P : Assertion ps} {α : Type u} {prog : m α} {Q' : α → Assertion ps} ``` -If `let mut` is the first-order pendant to {name}`StateT`, then early `return` is the first-order pendant to {name}`ExceptT`. +If {keyword}`let mut` is the {keywordOf Lean.Parser.Term.do}`do`-equivalent of {name}`StateT`, then early {keywordOf Lean.Parser.Term.doReturn}`return` is the equivalent of {name}`ExceptT`. We have seen how the {tactic}`mvcgen` copes with {name}`StateT`; here we will look at the program logic's support for {name}`ExceptT`. Exceptions are the reason why the type of postconditions {lean}`PostCond α ps` is not simply a single condition of type {lean}`α → Assertion ps` for the success case. @@ -489,39 +658,44 @@ There is no result `r`, so it is unclear what this proof means for {lean}`Q'`! So there are two reasonable options, inspired by non-termination in traditional program logics: -1. _Total_ correctness interpretation: {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄` asserts that, given {lean}`P` holds, then {lean}`prog` terminates _and_ {lean}`Q'` holds for the result. -2. _Partial_ correctness interpretation: {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄` asserts that, given {lean}`P` holds, and _if_ {lean}`prog` terminates _then_ {lean}`Q'` holds for the result. +: The {deftech}_total correctness interpretation_ -The notation {lean}`⇓ r => Q' r` has the total interpretation (cf. {name}`PostCond.noThrow`), while {lean}`⇓? r => Q' r` has the partial interpretation (cf. {name}`PostCond.mayThrow`). + {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄` asserts that, given {lean}`P` holds, then {lean}`prog` terminates _and_ {lean}`Q'` holds for the result. -{docstring Std.Do.PostCond} +: The {deftech}_partial correctness interpretation_ -{docstring Std.Do.PostCond.noThrow} + {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄` asserts that, given {lean}`P` holds, and _if_ {lean}`prog` terminates _then_ {lean}`Q'` holds for the result. + +The notation {lean}`⇓ r => Q' r` has the total interpretation, while {lean}`⇓? r => Q' r` has the partial interpretation. -{docstring Std.Do.PostCond.mayThrow} :::syntax term (title := "Postconditions") (namespace := Std.Do) ```grammar ⇓ $_:term* => $_:term ``` +{includeDocstring Std.Do.PostCond.noThrow} + ```grammar ⇓? $_:term* => $_:term ``` + +{includeDocstring Std.Do.PostCond.mayThrow} ::: So in the running example, {lean}`⦃P⦄ prog ⦃⇓ r => Q' r⦄` is unprovable, but {lean}`⦃P⦄ prog ⦃⇓? r => Q' r⦄` is trivially provable. However, the binary choice suggests that there is actually a _spectrum_ of correctness properties to express. The notion of postconditions {name}`PostCond` in `Std.Do` supports this spectrum. -For example, suppose that our {name}`Supply` of fresh numbers is bounded and we want to throw an exception if the supply is exhausted. -Then {name}`mkFreshN` should throw an exception _only if_ the supply is indeed exhausted. -The following correctness property expresses this: +:::: ```lean -show namespace Exceptions ``` + +For example, suppose that our {name}`Supply` of fresh numbers is bounded and we want to throw an exception if the supply is exhausted. +Then {name}`mkFreshN` should throw an exception _only if_ the supply is indeed exhausted, as in this implementation: ```lean structure Supply where counter : Nat @@ -535,15 +709,12 @@ def mkFresh : EStateM String Supply Nat := do else let n := supply.counter have := supply.property - set {supply with counter := n + 1, property := by omega} + set { supply with counter := n + 1, property := by grind } pure n +``` -def mkFreshN (n : Nat) : EStateM String Supply (List Nat) := do - let mut acc := #[] - for _ in [:n] do - acc := acc.push (← mkFresh) - pure acc.toList - +The following correctness property expresses this: +```lean @[spec] theorem mkFresh_spec (c : Nat) : ⦃fun state => ⌜state.counter = c⌝⦄ @@ -551,7 +722,25 @@ theorem mkFresh_spec (c : Nat) : ⦃post⟨fun r state => ⌜r = c ∧ c < state.counter⌝, fun _ state => ⌜c = state.counter ∧ c = state.limit⌝⟩⦄ := by mvcgen [mkFresh] with grind +``` +In this property, the postcondition has two branches: the first covers successful termination, and the second applies when an exception is thrown. +The monad's {name}`WP` instance determines both how many branches the postcondition may have and the number of parameters in each branch: each exception that might be triggered gives rise to an extra branch, and each state gives an extra parameter. + +:::leanFirst +In this new monad, {name}`mkFreshN`'s implementation is unchanged, except for the type signature: +```lean +def mkFreshN (n : Nat) : EStateM String Supply (List Nat) := do + let mut acc := #[] + for _ in [:n] do + acc := acc.push (← mkFresh) + pure acc.toList +``` +::: + +:::paragraph +However, the specification lemma must account for both successful termination and exceptions being thrown, in both the postcondition and the loop invariant: +```lean @[spec] theorem mkFreshN_spec (n : Nat) : ⦃⌜True⌝⦄ @@ -564,7 +753,12 @@ theorem mkFreshN_spec (n : Nat) : ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝, fun _msg state => ⌜state.counter = state.limit⌝⟩ with grind +``` +::: +:::paragraph +The final proof uses the specification lemmas and {tactic}`mvcgen`, just as before: +```lean theorem mkFreshN_correct (n : Nat) : match (mkFreshN n).run s with | .ok l _ => l.Nodup @@ -573,37 +767,48 @@ theorem mkFreshN_correct (n : Nat) : apply EStateM.of_wp_run_eq h mvcgen ``` +::: -Just as any {lean}`StateT σ`-like layer in the monad stack gives rise to a {lean}`PostShape.arg σ` layer in the {lean}`ps` -that {name}`WP` maps into, any {lean}`ExceptT ε`-like layer gives rise to a {lean}`PostShape.except ε` layer. +```lean -show +end Exceptions +``` + +:::leanSection +```lean -show +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} [WP m ps] {P : Assertion ps} {α σ ε : Type u} {prog : m α} {Q' : α → Assertion ps} +``` + +Just as any {lean}`StateT σ`-like monad transformer gives rise to a {lean}`PostShape.arg σ` layer in the {lean}`ps` that {name}`WP` maps into, any {lean}`ExceptT ε`-like layer gives rise to a {lean}`PostShape.except ε` layer. Every {lean}`PostShape.arg σ` adds another `σ → ...` layer to the language of {lean}`Assertion`s. Every {lean}`PostShape.except ε` leaves the {lean}`Assertion` language unchanged, but adds another exception condition to the postcondition. - -{docstring Std.Do.Assertion} - Hence the {name}`WP` instance for {lean}`EStateM ε σ` maps to the {name}`PostShape` {lean}`PostShape.except ε (.arg σ .pure)`, just as for {lean}`ExceptT ε (StateM σ)`. +::: -```lean -show -end Exceptions -``` -## Extending `mvcgen` with support for custom monads +## Extending `mvcgen` With Support for Custom Monads The {tactic}`mvcgen` framework is designed to be extensible. -None of the monads so far have in any way been hard-coded into {tactic}`mvcgen`. -Rather, {tactic}`mvcgen` relies on instances of the {name}`WP` and {name}`WPMonad` type class and user-provided specifications to generate verification conditions. +None of the monads presented so far have in any way been hard-coded into {tactic}`mvcgen`. +Rather, {tactic}`mvcgen` relies on instances of the {name}`WP` and {name}`WPMonad` type class and user-provided specifications to generate {tech}[verification conditions]. + +:::leanSection +```lean -show +variable {m : Type u → Type v} [Monad m] {ps : PostShape.{u}} +``` The {name}`WP` instance defines the weakest precondition interpretation of a monad {lean}`m` into a predicate transformer {lean}`PredTrans ps`, and the matching {name}`WPMonad` instance asserts that this translation distributes over the {name}`Monad` operations. +::: {docstring Std.Do.PredTrans} {docstring Std.Do.WP} -:::syntax term (title := "Weakest preconditions") (namespace := Std.Do) +:::syntax term (title := "Weakest Preconditions") (namespace := Std.Do) ```grammar wp⟦ $_:term ⟧ ``` @@ -611,7 +816,8 @@ wp⟦ $_:term ⟧ {docstring Std.Do.WPMonad} -:::example "Adding `mvcgen` support for Aeneas" (open := true) +::::paragraph +:::leanFirst Suppose one wants to use `mvcgen` to generate verification conditions for programs generated by [`Aeneas`](https://github.com/AeneasVerif/aeneas). `Aeneas` translates Rust programs into Lean programs in the following {name}`Result` monad: @@ -624,7 +830,8 @@ inductive Result (α : Type u) where | ok (v: α): Result α | fail (e: Error): Result α | div - +``` +```lean -show instance Result.instMonad : Monad Result where pure x := .ok x bind x f := match x with @@ -637,32 +844,54 @@ instance Result.instLawfulMonad : LawfulMonad Result := by -- variables apply LawfulMonad.mk' <;> (simp only [Result.instMonad]; sorry) ``` +::: +:::: -Support for this monad is a matter of +:::paragraph +There are both {inst}`Monad Result` and {inst}`LawfulMonad Result` instances. +Supporting this monad in {tactic}`mvcgen` is a matter of: -1. Adding a {name}`WP` and {name}`WPMonad` instance for {name}`Result` +1. Adding {name}`WP` and {name}`WPMonad` instances for {name}`Result` 2. Registering specification lemmas for the translation of basic Rust primitives such as addition etc. +::: -The first part is straightforward: - +::::paragraph +:::leanSection +```lean -show +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} [WP m ps] {P : Assertion ps} {α σ ε : Type u} {prog : m α} {Q' : α → Assertion ps} +``` +The {name}`WP` instance for {name}`Result` specifies a postcondition shape {lean (type := "PostShape.{0}")}`.except Error .pure` because there are no state-like effects, but there is a single exception of type {lean}`Error`. +The {name}`WP` instance translates programs in {lean}`Result α` to predicate transformers in {lean}`PredTrans ps α`. +That is, a function in {lean}`PostCond α ps → Assertion ps`, mapping a postcondition to its weakest precondition. +The implementation of {name}`WP.wp` reuses the implementation for {lean}`Except Error` for two of its cases, and maps diverging programs to {lean}`False`. +The instance is named so that it can be more easily unfolded in proofs about it. +::: ```lean instance Result.instWP : WP Result (.except Error .pure) where - wp x := match x with - | .ok v => wp (pure v : Except Error _) - | .fail e => wp (throw e : Except Error _) - | .div => PredTrans.const ⌜False⌝ + wp + | .ok v => wp (pure v : Except Error _) + | .fail e => wp (throw e : Except Error _) + | .div => PredTrans.const ⌜False⌝ +``` +:::: --- set_option trace.Meta.synthInstance true in -instance Result.instWPMonad : WPMonad Result (.except Error .pure) where +:::paragraph +The implementation of {name}`WP.wp` should distribute over the basic monad operators: +```lean +instance : WPMonad Result (.except Error .pure) where wp_pure := by intros ext Q simp [wp, PredTrans.pure, pure, Except.pure, Id.run] wp_bind x f := by - simp only [instWP, bind] + simp only [Result.instWP, bind] ext Q cases x <;> simp [PredTrans.bind, PredTrans.const] +``` +::: +```lean theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) : (⊢ₛ wp⟦x⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.fail e)⌝⟩) → P x := by @@ -671,11 +900,17 @@ theorem Result.of_wp {α} {x : Result α} (P : Result α → Prop) : split at hspec <;> simp_all ``` -The {name}`WP` instance above translates programs in {lean}`Result α` to predicate transformers in {lean}`PredTrans ps α`. -That is, a function in {lean}`PostCond α ps → Assertion ps`, mapping a postcondition to its weakest precondition. -Note that this definition of the {name}`WP` instance determines what properties can be derived from proved specifications via {lean}`Result.of_wp`. +:::leanSection +```lean -show +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} [WP m ps] {P : Assertion ps} {α σ ε : Type u} {prog : m α} {Q' : α → Assertion ps} +``` + +The definition of the {name}`WP` instance determines what properties can be derived from proved specifications via {lean}`Result.of_wp`. This lemma defines what “weakest precondition” means. +::: +:::paragraph To exemplify the second part, here is an example definition of {name}`UInt32` addition in {name}`Result` that models integer overflow: ```lean @@ -692,7 +927,9 @@ def addOp (x y : UInt32) : Result UInt32 := else pure (x + y) ``` +::: +:::paragraph There are two relevant specification lemmas to register: ```lean @@ -707,7 +944,9 @@ theorem addOp_ok_spec {x y} (h : x.toNat + y.toNat < UInt32.size) : ⦃⇓ r => ⌜r = x + y ∧ (x + y).toNat = x.toNat + y.toNat⌝⦄ := by mvcgen [addOp] with (simp_all; try grind) ``` +::: +:::paragraph This is already enough to prove the following example: ```lean @@ -725,17 +964,17 @@ example : ``` ::: -## Proof mode for stateful goals +## Proof Mode for Stateful Goals ```lean -show variable {σs : List (Type u)} {H T : SPred σs} ``` -It is a priority of {tactic}`mvcgen` to break down monadic programs into VCs that are straightforward to understand. -For example, when the monad stack is monomorphic and all loop invariants have been instantiated, an invocation of `all_goals mleave` should simplify away any `Std.Do.SPred` specific constructs and leave behind a goal that is easily understood by humans and `grind`. -This `all_goals mleave` step is carried out automatically by {tactic}`mvcgen` after loop invariants have been instantiated. +It is a priority of {tactic}`mvcgen` to break down monadic programs into {tech}[verification conditions] that are straightforward to understand. +For example, when the monad is monomorphic and all loop invariants have been instantiated, an invocation of {tactic}`all_goals`{lit}` `{tactic}`mleave` should simplify away any {name}`Std.Do.SPred`-specific constructs and leave behind a goal that is easily understood by humans and {tactic}`grind`. +This {tactic}`all_goals`{lit}` `{tactic}`mleave` step is carried out automatically by {tactic}`mvcgen` after loop invariants have been instantiated. -However, there are times when `mleave` will be unable to remove all {name}`Std.Do.SPred` constructs. +However, there are times when {tactic}`mleave` will be unable to remove all {name}`Std.Do.SPred` constructs. In this case, verification conditions of the form {lean}`H ⊢ₛ T` will be left behind. The assertion language {name}`Assertion` translates into an {name}`Std.Do.SPred` as follows: @@ -766,41 +1005,18 @@ $_:term ⊢ₛ $_:term $_:term ⊣⊢ₛ $_:term ``` -```grammar -spred($_:term ∧ $_:term) -``` - -```grammar -spred($_:term ∨ $_:term) -``` - -```grammar -spred($_:term → $_:term) -``` - -```grammar -spred(¬$_:term) -``` - -```grammar -spred(∀ $_:ident, $_:term) -``` +::: -```grammar -spred(∃ $_:ident, $_:term) +:::leanSection +```lean -show +universe u v +variable {m : Type u → Type v} {ps : PostShape.{u}} [WP m ps] {P : Assertion ps} {α σ ε : Type u} {prog : m α} {Q' : α → Assertion ps} ``` -::: A common case for when a VC of the form {lean}`H ⊢ₛ T` is left behind is when the base monad {lean}`m` is polymorphic. In this case, the proof will depend on a {lean}`WP m ps` instance which governs the translation into the {name}`Assertion` language, but the exact correspondence to `σs : List (Type u)` is yet unknown. To successfully discharge such a VC, `mvcgen` comes with an entire proof mode that is inspired by that of the Iris concurrent separation logic. (In fact, the proof mode was adapted in large part from its Lean clone, [`iris-lean`](https://github.com/leanprover-community/iris-lean).) -The Lean 4 test file [`tests/lean/run/spredProofMode.lean`](https://github.com/leanprover/lean4/blob/76971a88fff3b3df75dceb588b5bd98b1552bafc/tests/lean/run/spredProofMode.lean) contains many examples of that proof mode to learn from, and {ref "tactic-ref-spred"}[the reference manual] contains a list of all proof mode tactics. - -## Further reading +The {ref "tactic-ref-spred"}[tactic reference] contains a list of all proof mode tactics. -More examples can be found in Lean's test suite. -* [`tests/lean/run/doLogicTests.lean`](https://github.com/leanprover/lean4/blob/76971a88fff3b3df75dceb588b5bd98b1552bafc/tests/lean/run/doLogicTests.lean) is a kitchen sink test file with many examples. -* [`tests/lean/run/bhaviksSampler.lean`](https://github.com/leanprover/lean4/blob/76971a88fff3b3df75dceb588b5bd98b1552bafc/tests/lean/run/bhaviksSampler.lean) is a stubbed out example from a larger development due to Bhavik Mehta. -* [Markus Himmel's `human-eval-lean` project](https://github.com/TwoFX/human-eval-lean/) has a limited number of `mvcgen`-based proofs for imperative algorithm implementations. Contributions welcome! -* [Rish Vaishnav's ongoing `qsort` formalization](https://github.com/rish987/qsort/) is the largest example of `mvcgen` to date. +::: From 3f985f84494eefe086a81f13371af274829d9ffc Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 24 Oct 2025 10:03:32 +0200 Subject: [PATCH 3/4] Small touchups --- .vale/styles/config/ignore/terms.txt | 1 + Manual/VCGen.lean | 30 ++++++++++++++++++---------- 2 files changed, 20 insertions(+), 11 deletions(-) diff --git a/.vale/styles/config/ignore/terms.txt b/.vale/styles/config/ignore/terms.txt index ad13a1dba..eb5529b39 100644 --- a/.vale/styles/config/ignore/terms.txt +++ b/.vale/styles/config/ignore/terms.txt @@ -119,6 +119,7 @@ monad's monoid monomorphic monomorphism +morphism multipattern multipatterns multiset diff --git a/Manual/VCGen.lean b/Manual/VCGen.lean index 9d3b62fb2..6ee08492b 100644 --- a/Manual/VCGen.lean +++ b/Manual/VCGen.lean @@ -55,12 +55,12 @@ open Std.Do ## Preconditions and Postconditions -One style in which program specifications can be written is to provide a {deftech}_precondition_, which the program's caller is expected to ensure, and a {deftech}_postcondition_, which the program itself is expected to ensure. -The program is correct if running it when the precondition holds always results in the postcondition holding. +One style in which program specifications can be written is to provide a {deftech}_precondition_ $`P`, which the caller of a program `prog` is expected to ensure, and a {deftech}_postcondition_ $`Q`, which the `prog` is expected to ensure. +The program `prog` satisfies the specification if running it when the precondition $`P` holds always results in the postcondition $`Q` holding. In general, many different preconditions might suffice for a program to ensure the postcondition. -After all, new preconditions can be generated by replacing a precondition $`P` with $`P \wedge Q`. -The {deftech}_weakest precondition_ is a precondition that is implied by all other preconditions. +After all, new preconditions can be generated by replacing a precondition $`P₁` with $`P₁ \wedge P₂`. +The {deftech}_weakest precondition_ $`\textbf{wp}⟦\texttt{prog}⟧(Q)` of a program `prog` and postcondition $`Q` is a precondition for which `prog` ensures the postcondition `Q` and is implied by all other such preconditions. One way to prove something about the result of a program is to find the weakest precondition that guarantees the desired result, and then to show that this weakest precondition is simply true. This means that the postcondition holds no matter what. @@ -83,7 +83,7 @@ def mySum (l : Array Nat) : Nat := Id.run do If {name}`mySum` is correct, then it is equal to {name}`Array.sum`. In {name}`mySum`, the use of {keywordOf Lean.Parser.Term.do}`do` is an internal implementation detail—the function's signature makes no mention of any monad. Thus, the proof first manipulates the goal into a form that is amenable to the use of {tactic}`mvcgen`, using the lemma {name}`Id.of_wp_run_eq`. -This lemma states that facts about the result of running a computation in the {name}`Id` monad that terminates normally (that is, does not use {ref "early-return"}[early return]) can be proved by showing that the {tech}[weakest precondition] that ensures the desired result is true. +This lemma states that facts about the result of running a computation in the {name}`Id` monad that terminates normally (`Id` computations never throw exceptions) can be proved by showing that the {tech}[weakest precondition] that ensures the desired result is true. Next, the proof uses {tactic}`mvcgen` to replace the formulation in terms of weakest preconditions with a set of {tech}[verification conditions]. While {tactic}`mvcgen` is mostly automatic, it does require an invariant for the loop. @@ -130,7 +130,7 @@ For example: * `vc1.step` conveys that this {tech}[VC] proves the inductive step for the loop * `vc2.a.pre` is meant to prove that the hypotheses of a goal imply the precondition of a specification (of {name}`forIn`). -* `vc3.a.post` is meant to prove that the postcondition of a specification (of {name}`forIn`) implies the desired property. +* `vc3.a.post.success` is meant to prove that the postcondition of a specification (of {name}`forIn`) implies the desired property. ::: :::paragraph @@ -257,13 +257,21 @@ end ``` ::: -:::TODO -Note that the form `mvcgen invariants?` would hint that {name}`Invariant.withEarlyReturn` is a useful way to construct the invariant: -``` +:::paragraph +Note that the form `mvcgen invariants?` will suggest an initial invariant using {name}`Invariant.withEarlyReturn`, so there is no need to memorize the exact syntax for specifying invariants: +```lean +/-- +info: Try this: + [apply] invariants + · + Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝) (onContinue := + fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝) +-/ +#guard_msgs (info) in example (l : List Int) : nodup l ↔ l.Nodup := by generalize h : nodup l = r apply Id.of_wp_run_eq h - mvcgen invariants? + mvcgen invariants? <;> sorry ``` ::: @@ -417,7 +425,7 @@ mkFresh ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ ``` When working in a state monad, preconditions may be parameterized over the value of the state prior to running the code. -Here, the universally quantified {name}`Nat` is used to _relate_ the initial state to the final state; the precondition is used to connect it the initial state. +Here, the universally quantified {name}`Nat` is used to _relate_ the initial state to the final state; the precondition is used to connect it to the initial state. Similarly, the postcondition may also accept the final state as a parameter. This Hoare triple states: From b6b23131e0c0da0378bda33564ef72e776c01059 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 24 Oct 2025 10:55:34 +0200 Subject: [PATCH 4/4] Minor markup updates --- Manual/VCGen.lean | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/Manual/VCGen.lean b/Manual/VCGen.lean index 6ee08492b..fe7788140 100644 --- a/Manual/VCGen.lean +++ b/Manual/VCGen.lean @@ -55,12 +55,12 @@ open Std.Do ## Preconditions and Postconditions -One style in which program specifications can be written is to provide a {deftech}_precondition_ $`P`, which the caller of a program `prog` is expected to ensure, and a {deftech}_postcondition_ $`Q`, which the `prog` is expected to ensure. -The program `prog` satisfies the specification if running it when the precondition $`P` holds always results in the postcondition $`Q` holding. +One style in which program specifications can be written is to provide a {deftech}_precondition_ $`P`, which the caller of a program $`\mathit{prog}` is expected to ensure, and a {deftech}_postcondition_ $`Q`, which the $`\mathit{prog}` is expected to ensure. +The program $`\mathit{prog}` satisfies the specification if running it when the precondition $`P` holds always results in the postcondition $`Q` holding. In general, many different preconditions might suffice for a program to ensure the postcondition. -After all, new preconditions can be generated by replacing a precondition $`P₁` with $`P₁ \wedge P₂`. -The {deftech}_weakest precondition_ $`\textbf{wp}⟦\texttt{prog}⟧(Q)` of a program `prog` and postcondition $`Q` is a precondition for which `prog` ensures the postcondition `Q` and is implied by all other such preconditions. +After all, new preconditions can be generated by replacing a precondition $`P_1` with $`P_1 \wedge P_2`. +The {deftech}_weakest precondition_ $`\textbf{wp}⟦\mathit{prog}⟧(Q)` of a program $`\mathit{prog}` and postcondition $`Q` is a precondition for which $`\mathit{prog}` ensures the postcondition $`Q` and is implied by all other such preconditions. One way to prove something about the result of a program is to find the weakest precondition that guarantees the desired result, and then to show that this weakest precondition is simply true. This means that the postcondition holds no matter what. @@ -259,20 +259,21 @@ end :::paragraph Note that the form `mvcgen invariants?` will suggest an initial invariant using {name}`Invariant.withEarlyReturn`, so there is no need to memorize the exact syntax for specifying invariants: -```lean -/-- -info: Try this: - [apply] invariants - · - Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝) (onContinue := - fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝) --/ -#guard_msgs (info) in +```lean (name := invariants?) example (l : List Int) : nodup l ↔ l.Nodup := by generalize h : nodup l = r apply Id.of_wp_run_eq h mvcgen invariants? <;> sorry ``` +The tactic suggests a starting invariant. +This starting point will not allow the proof to succeed—after all, if the invariant can be inferred by the system, then there's no need to make the user specify it—but it does provide a reminder of the correct syntax to use for assertions in the current monad: +```leanOutput invariants? +Try this: + [apply] invariants + · + Invariant.withEarlyReturn (onReturn := fun r letMuts => ⌜l.Nodup ∧ (r = true ↔ l.Nodup)⌝) (onContinue := + fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝) +``` ::: :::paragraph