diff --git a/Manual.lean b/Manual.lean index 37e699a31..3513c85e9 100644 --- a/Manual.lean +++ b/Manual.lean @@ -31,6 +31,7 @@ import Manual.Namespaces import Manual.Runtime import Manual.SupportedPlatforms import Manual.VCGen +import Manual.MVCGen open Verso.Genre Manual open Verso.Genre.Manual.InlineLean @@ -100,6 +101,8 @@ Thus, this reference manual does not draw a barrier between the two aspects, but {include 0 Manual.VCGen} +{include 0 Manual.MVCGen} + {include 0 Manual.Monads} {include 0 Manual.BasicProps} diff --git a/Manual/BuildTools/Lake.lean b/Manual/BuildTools/Lake.lean index 5b23844cd..7fe5ca6d3 100644 --- a/Manual/BuildTools/Lake.lean +++ b/Manual/BuildTools/Lake.lean @@ -763,6 +763,7 @@ root = "Tests" libPrefixOnWindows := false, allowImportAll := false, builtinLint? := none, + checks := #[], fixedToolchain := false}, configFile := FilePath.mk "lakefile", relConfigFile := FilePath.mk "lakefile", @@ -927,6 +928,7 @@ lean_exe «my-package-tests» where libPrefixOnWindows := false, allowImportAll := false, builtinLint? := none, + checks := #[], fixedToolchain := false}, configFile := FilePath.mk "lakefile.lean", relConfigFile := FilePath.mk "lakefile.lean", @@ -1131,6 +1133,7 @@ root = "Lint" libPrefixOnWindows := false, allowImportAll := false, builtinLint? := none, + checks := #[], fixedToolchain := false}, configFile := FilePath.mk "lakefile", relConfigFile := FilePath.mk "lakefile", @@ -1296,6 +1299,7 @@ lean_exe «my-package-lint» where libPrefixOnWindows := false, allowImportAll := false, builtinLint? := none, + checks := #[], fixedToolchain := false}, configFile := FilePath.mk "lakefile.lean", relConfigFile := FilePath.mk "lakefile.lean", diff --git a/Manual/BuildTools/Lake/CLI.lean b/Manual/BuildTools/Lake/CLI.lean index 3b3ae32b1..582b6d98f 100644 --- a/Manual/BuildTools/Lake/CLI.lean +++ b/Manual/BuildTools/Lake/CLI.lean @@ -895,6 +895,9 @@ OPTIONS: --code-quality records each linter warning as a code quality check result and runs the registered code quality checks. Setting this flag will skip lint driver. + --checks comma-separated list of workspace modules providing + package code quality checks; they are imported + alongside each linted module (implies --code-quality) A lint driver can be configured by either setting the `lintDriver` package configuration option or by tagging a script or executable `@[lint_driver]`. diff --git a/Manual/BuildTools/Lake/Config.lean b/Manual/BuildTools/Lake/Config.lean index c1b4805a9..57d434dfa 100644 --- a/Manual/BuildTools/Lake/Config.lean +++ b/Manual/BuildTools/Lake/Config.lean @@ -193,6 +193,7 @@ name = "example-package" libPrefixOnWindows := false, allowImportAll := false, builtinLint? := none, + checks := #[], fixedToolchain := false}, configFile := FilePath.mk "lakefile", relConfigFile := FilePath.mk "lakefile", @@ -284,6 +285,7 @@ name = "Sorting" libPrefixOnWindows := false, allowImportAll := false, builtinLint? := none, + checks := #[], fixedToolchain := false}, configFile := FilePath.mk "lakefile", relConfigFile := FilePath.mk "lakefile", diff --git a/Manual/MVCGen.lean b/Manual/MVCGen.lean new file mode 100644 index 000000000..d671d0edd --- /dev/null +++ b/Manual/MVCGen.lean @@ -0,0 +1,934 @@ +/- +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 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 + +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) + +open Std.Do + +#doc (Manual) "The `mvcgen` tactic" => +%%% +tag := "mvcgen-tactic" +%%% + +:::tutorials + * {ref "mvcgen-tactic-tutorial" (remote := "tutorials")}[Verifying Imperative Programs Using `mvcgen`] +::: + +The {tactic}`mvcgen` tactic implements a _monadic verification condition generator_: +It breaks down a goal involving a program written using Lean's imperative {keywordOf Lean.Parser.Term.do}`do` notation into a number of smaller {tech (key := "mvcgen verification conditions")}_verification conditions_ ({deftech (key := "mvcgen VCs")}[VCs]) that are sufficient to prove the goal. +In addition to a reference that describes the use of {tactic}`mvcgen`, this chapter includes a {ref "mvcgen-tactic-tutorial" (remote := "tutorials")}[tutorial] that can be read independently of the reference. + +In order to use the {tactic}`mvcgen` tactic, {module}`Std.Tactic.Do` must be imported and the namespace {namespace}`Std.Do` must be opened. + + +# Overview + + + +The workflow of {tactic}`mvcgen` consists of the following: + +1. Monadic programs are re-interpreted according to a {tech (key := "mvcgen predicate transformer semantics")}[predicate transformer semantics]. + An instance of {name}`WP` determines the monad's interpretation. + Each program is interpreted as a mapping from arbitrary {tech (key := "mvcgen postconditions")}[postconditions] to the {tech (key := "mvcgen weakest precondition")}[weakest precondition] that would ensure the postcondition. + This step is invisible to most users, but library authors who want to enable their monads to work with {tactic}`mvcgen` need to understand it. +2. Programs are composed from smaller programs. + Each statement in a {keywordOf Lean.Parser.Term.do}`do`-block is associated with a predicate transformer, and there are general-purpose rules for combining these statements with sequencing and control-flow operators. + A statement with its pre- and postconditions is called a {tech (key := "mvcgen Hoare triple")}_Hoare triple_. + In a program, the postcondition of each statement should suffice to prove the precondition of the next one, and loops require a specified {deftech (key := "mvcgen loop invariant")}_loop invariant_, which is a statement that must be true at the beginning of the loop and at the end of each iteration. + Designated {tech (key := "mvcgen specification lemmas")}_specification lemmas_ associate functions with Hoare triples that specify them. +3. Applying the weakest-precondition semantics of a monadic program to a desired proof goal results in the precondition that must hold in order to prove the goal. + Any missing steps such as loop invariants or proofs that a statement's precondition implies its postcondition become new subgoals. + These missing steps are called the {deftech (key := "mvcgen verification conditions")}_verification conditions_. + The {tactic}`mvcgen` tactic performs this transformation, replacing the goal with its verification conditions. + During this transformation, {tactic}`mvcgen` uses specification lemmas to discharge proofs about individual statements. +4. After supplying loop invariants, many verification conditions can in practice be discharged automatically. + Those that cannot can be proven using either a {ref "tactic-ref-spred"}[special proof mode] or ordinary Lean tactics, depending on whether they are expressed in the logic of program assertions or as ordinary propositions. + + +# Predicate Transformers + +A {deftech (key := "mvcgen predicate transformer semantics")}_predicate transformer semantics_ is an interpretation of programs as functions from predicates to predicates, rather than values to values. +A {deftech (key := "mvcgen postcondition")}_postcondition_ is an assertion that holds after running a program, while a {deftech (key := "mvcgen precondition")}_precondition_ is an assertion that must hold prior to running the program in order for the postcondition to be guaranteed to hold. + +The predicate transformer semantics used by {tactic}`mvcgen` transforms postconditions into the {deftech (key := "mvcgen weakest preconditions")}_weakest preconditions_ under which the program will ensure the postcondition. +An assertion $`P` is weaker than $`P'` if, in all states, $`P'` suffices to prove $`P`, but $`P` does not suffice to prove $`P'`. +Logically equivalent assertions are considered to be equal. + +The predicates in question are stateful: they can mention the program's current state. +Furthermore, postconditions can relate the return value and any exceptions thrown by the program to the final state. +{name}`SPred` is a type of predicates that is parameterized over a monadic state, expressed as a list of the types of the fields that make up the state. +The usual logical connectives and quantifiers are defined for {name}`SPred`. +Each monad that can be used with {tactic}`mvcgen` is assigned a state type by an instance of {name}`WP`, and {name}`Assertion` is the corresponding type of assertions for that monad, which is used for preconditions. +{name}`Assertion` is a wrapper around {name}`SPred`: while {name}`SPred` is parameterized by a list of states types, {name}`Assertion` is parameterized by a more informative type that it translates to a list of state types for {name}`SPred`. +A {name}`PostCond` pairs an {name}`Assertion` about a return value with assertions about potential exceptions; the available exceptions are also specified by the monad's {name}`WP` instance. + + +## Stateful Predicates + +The predicate transformer semantics of monadic programs is based on a logic in which propositions may mention the program's state. +Here, “state” refers not only to mutable state, but also to read-only values such as those that are provided via {name}`ReaderT`. +Different monads have different state types available, but each individual state always has a type. +Given a list of state types, {name}`SPred` is a type of predicates over these states. + +{name}`SPred` is not inherently tied to the monadic verification framework. +The related {name}`Assertion` computes a suitable {name}`SPred` for a monad's state as expressed via its {name}`WP` instance's {name}`PostShape` output parameter. + +{docstring Std.Do.SPred} + +::::leanSection +```lean -show +variable {P : Prop} {σ : List (Type u)} +``` +Ordinary propositions that do not mention the state can be used as stateful predicates by adding a trivial universal quantification. +This is written with the syntax {lean (type := "SPred σ")}`⌜P⌝`, which is syntactic sugar for {name}`SPred.pure`. +:::syntax term (title := "Notation for `SPred`") (namespace := Std.Do) +```grammar +⌜$_:term⌝ +``` +{includeDocstring Std.Do.«term⌜_⌝»} +::: +:::: + +{docstring SPred.pure} + +:::example "Stateful Predicates" +```imports -show +import Std.Do +import Std.Tactic.Do +``` +```lean -show +open Std.Do + +set_option mvcgen.warning false + +``` +The predicate {name}`ItIsSecret` expresses that a state of type {name}`String` is {lean}`"secret"`: +```lean +def ItIsSecret : SPred [String] := fun s => ⌜s = "secret"⌝ +``` +::: + +### Entailment + +Stateful predicates are related by _entailment_. +Entailment of stateful predicates is defined as universally-quantified implication: if $`P` and $`Q` are predicates over a state $`\sigma`, then $`P` entails $`Q` (written $`P \vdash_s Q`) when $`∀ s : \sigma, P(s) → Q(s)`. + +{docstring Std.Do.SPred.entails} + +{docstring Std.Do.SPred.bientails} + +:::syntax term (title := "Notation for `SPred`") (namespace := Std.Do) +```grammar +$_:term ⊢ₛ $_:term +``` +{includeDocstring Std.Do.«term_⊢ₛ_»} + +```grammar +⊢ₛ $_:term +``` +{includeDocstring Std.Do.«term⊢ₛ_»} + +```grammar +$_:term ⊣⊢ₛ $_:term +``` + +{includeDocstring Std.Do.«term_⊣⊢ₛ_»} +::: + +:::leanSection +```lean -show +variable {σ : List (Type u)} {P Q : SPred σ} +``` +The logic of stateful predicates includes an implication connective. +The difference between entailment and implication is that entailment is a statement in Lean's logic, while implication is internal to the stateful logic. +Given stateful predicates {lean}`P` and {lean}`Q` for state {lean}`σ`, {lean (type := "Prop")}`P ⊢ₛ Q` is a {lean}`Prop` while {lean (type := "SPred σ")}`spred(P → Q)` is an {lean}`SPred σ`. +::: + +### Notation + +The syntax of stateful predicates overlaps with that of ordinary Lean terms. +In particular, stateful predicates use the usual syntax for logical connectives and quantifiers. +The syntax associated with stateful predicates is automatically enabled in contexts such as pre- and postconditions where they are clearly intended; other contexts must explicitly opt in to the syntax using {keywordOf Std.Do.«termSpred(_)»}`spred`. +The usual meanings of these operators can be recovered by using the {keywordOf Std.Do.«termTerm(_)»}`term` operator. + +:::syntax term (title := "Predicate Terms") (namespace := Std.Do) +{keywordOf Std.Do.«termSpred(_)»}`spred` indicates that logical connectives and quantifiers should be understood as those pertaining to stateful predicates, while {keywordOf Std.Do.«termTerm(_)»}`term` indicates that they should have the usual meaning. +```grammar +spred($t) +``` +```grammar +term($t) +``` +::: + +### Connectives and Quantifiers + +:::syntax term (title := "Predicate Connectives") (namespace := Std.Do) +```grammar +spred($_ ∧ $_) +``` +Syntactic sugar for {name}`SPred.and`. + +```grammar +spred($_ ∨ $_) +``` +Syntactic sugar for {name}`SPred.or`. + +```grammar +spred(¬ $_) +``` +Syntactic sugar for {name}`SPred.not`. + +```grammar +spred($_ → $_) +``` +Syntactic sugar for {name}`SPred.imp`. + +```grammar +spred($_ ↔ $_) +``` +Syntactic sugar for {name}`SPred.iff`. +::: + + +{docstring SPred.and} + +{docstring SPred.conjunction} + +{docstring SPred.or} + +{docstring SPred.not} + +{docstring SPred.imp} + +{docstring SPred.iff} + +:::syntax term (title := "Predicate Quantifiers") (namespace := Std.Do) +```grammar +spred(∀ $x:ident, $_) +``` +```grammar +spred(∀ $x:ident : $ty, $_) +``` +```grammar +spred(∀ ($x:ident $_* : $ty), $_) +``` +```grammar +spred(∀ _, $_) +``` +```grammar +spred(∀ _ : $ty, $_) +``` +```grammar +spred(∀ (_ $_* : $ty), $_) +``` +Each form of universal quantification is syntactic sugar for an invocation of {name}`SPred.forall` on a function that takes the quantified variable as a parameter. + +```grammar +spred(∃ $x:ident, $_) +``` +```grammar +spred(∃ $x:ident : $ty, $_) +``` +```grammar +spred(∃ ($x:ident $_* : $ty), $_) +``` +```grammar +spred(∃ _, $_) +``` +```grammar +spred(∃ _ : $ty, $_) +``` +```grammar +spred(∃ (_ $_* : $ty), $_) +``` +Each form of existential quantification is syntactic sugar for an invocation of {name}`SPred.exists` on a function that takes the quantified variable as a parameter. +::: + +{docstring SPred.forall} + +{docstring SPred.exists} + +### Stateful Values + +Just as {name}`SPred` represents predicate over states, {name}`SVal` represents a value that is derived from a state. + +{docstring SVal} + +{docstring SVal.getThe} + +{docstring SVal.StateTuple} + +{docstring SVal.curry} + +{docstring SVal.uncurry} + + +## Assertions + +The language of assertions about monadic programs is parameterized by a {deftech (key := "mvcgen postcondition shape")}_postcondition shape_, which describes the inputs to and outputs from a computation in a given monad. +Preconditions may mention the initial values of the monad's state, while postconditions may mention the returned value, the final values of the monad's state, and must furthermore account for any exceptions that could have been thrown. +The postcondition shape of a given monad determines the states and exceptions in the monad. +{name}`PostShape.pure` describes a monad in which assertions may not mention any states, {name}`PostShape.arg` describes a state value, and {name}`PostShape.except` describes a possible exception. +Because these constructors can be continually added, the postcondition shape of a monad transformer can be defined in terms of the postcondition shape of the underlying transformed monad. +Behind the scenes, an {name}`Assertion` is translated into an appropriate {name}`SPred` by translating the postcondition shape into a list of state types, discarding exceptions. + +{docstring PostShape} + +{docstring PostShape.args} + +{docstring Assertion} + +{docstring PostCond} + +:::syntax term (title := "Postconditions") +```grammar +⇓ $_* => $_ +``` +Syntactic sugar for a nested sequence of product constructors, terminating in {lean}`()`, in which the first element is an assertion about non-exceptional return values and the remaining elements are assertions about the exceptional cases for a postcondition. +::: + + +{docstring ExceptConds} + +:::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} +``` +Postconditions for programs that might throw exceptions come in two varieties. The {deftech (key := "mvcgen total correctness interpretation")}_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. The {deftech (key := "mvcgen partial correctness interpretation")}_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. +::: + + +:::syntax term (title := "Exception-Free Postconditions") +```grammar +⇓ $_* => $_ +``` +{includeDocstring PostCond.noThrow} +::: + +{docstring PostCond.noThrow} + +:::syntax term (title := "Partial Postconditions") +```grammar +⇓? $_* => $_ +``` +{includeDocstring PostCond.mayThrow} +::: + +{docstring PostCond.mayThrow} + +:::syntax term (title := "Postcondition Entailment") +```grammar +$_ ⊢ₚ $_ +``` +Syntactic sugar for {name}`PostCond.entails` +::: + +{docstring PostCond.entails} + + +:::syntax term (title := "Postcondition Conjunction") +```grammar +$_ ∧ₚ $_ +``` +Syntactic sugar for {name}`PostCond.and` +::: + +{docstring PostCond.and} + +:::syntax term (title := "Postcondition Implication") +```grammar +$_ →ₚ $_ +``` +Syntactic sugar for {name}`PostCond.imp` +::: + +{docstring PostCond.imp} + + +## Predicate Transformers + +A predicate transformer is a function from postconditions for some postcondition state into assertions for that state. +The function must be {deftech (key := "mvcgen conjunctive")}_conjunctive_, which means it must distribute over {name}`PostCond.and`. + +{docstring PredTrans} + +{docstring PredTrans.Conjunctive} + +{docstring PredTrans.Monotonic} + +:::leanSection +```lean -show +variable {σ : List (Type u)} {ps : PostShape} {x y : PredTrans ps α} {Q : Assertion ps} +``` +The {inst}`LE PredTrans` instance is defined in terms of their logical strength; one transformer is stronger than another if the result of applying it always entails the result of applying the other. +In other words, {lean}`∀ Q, y Q ⊢ₛ x Q`, then {lean}`x ≤ y`. +This means that stronger predicate transformers are considered greater than weaker ones. +::: + +Predicate transformers form a monad. +The {name}`pure` operator is the identity transformer; it simply instantiates the postcondition with the its argument. +The {name}`bind` operator composes predicate transformers. + +{docstring PredTrans.pure} + +{docstring PredTrans.bind} + +The helper operators {name}`PredTrans.pushArg`, {name}`PredTrans.pushExcept`, and {name}`PredTrans.pushOption` modify a predicate transformer by adding a standard side effect. +They are used to implement the {name}`WP` instances for transformers such as {name}`StateT`, {name}`ExceptT`, and {name}`OptionT`; they can also be used to implement monads that can be thought of in terms of one of these. +For example, {name}`PredTrans.pushArg` is typically used for state monads, but can also be used to implement a reader monad's instance, treating the reader's value as read-only state. + +{docstring PredTrans.pushArg} + +{docstring PredTrans.pushExcept} + +{docstring PredTrans.pushOption} + +### Weakest Preconditions + +The {tech (key := "mvcgen weakest precondition")}[weakest precondition] semantics of a monad are provided by the {name}`WP` type class. +Instances of {name}`WP` determine the monad's postcondition shape and provide the logical rules for interpreting the monad's operations as a predicate transformer in its postcondition shape. + +{docstring WP} + +:::syntax term (title := "Weakest Preconditions") +```grammar +wp⟦$_ $[: $_]?⟧ +``` +{includeDocstring Std.Do.«termWp⟦_:_⟧»} +::: + +### Weakest Precondition Monad Morphisms + +Most of the built-in specification lemmas for {tactic}`mvcgen` relies on the presence of a {name}`WPMonad` instance, in addition to the {name}`WP` instance. +In addition to being lawful, weakest preconditions of the monad's implementations of {name}`pure` and {name}`bind` should correspond to the {name}`pure` and {name}`bind` operators for the predicate transformer monad. +Without a {name}`WPMonad` instance, {tactic}`mvcgen` typically returns the original proof goal unchanged. + +{docstring WPMonad} + +:::example "Missing `WPMonad` Instance" +```imports -show +import Std.Do +import Std.Tactic.Do +``` +```lean -show +open Std.Do + +set_option mvcgen.warning false + +``` + +The single-field structure {name}`Identity` acts like the identity monad {name}`Id`. It has a {name}`WP` instance, but no {name}`WPMonad` instance: +```lean +structure Identity (α : Type u) where + run : α + +variable {α : Type u} + +instance : Monad Identity where + pure x := ⟨x⟩ + bind x f := f x.run + +instance : WP Identity .pure where + wp x := PredTrans.pure x.run + +theorem Identity.of_wp_run_eq {x : α} {prog : Identity α} + (h : Identity.run prog = x) (P : α → Prop) : + (⊢ₛ wp⟦prog⟧ (⇓ a => ⟨P a⟩)) → P x := by + simp_all [WP.wp, ← h] +``` + +```lean -show +instance : LawfulMonad Identity := + LawfulMonad.mk' Identity + (id_map := fun _ => rfl) + (pure_bind := fun _ _ => rfl) + (bind_assoc := fun _ _ _ => rfl) +``` + +The missing instance prevents {tactic}`mvcgen` from using its specifications for {name}`pure` and {name}`bind`. +This tends to show up as a verification condition that's equal to the original goal. +This function that reverses a list: +```lean +def rev (xs : List α) : Identity (List α) := do + let mut out := [] + for x in xs do + out := x :: out + return out +``` +It is correct if it is equal to {name}`List.reverse`. +However, {tactic}`mvcgen` does not make the goal easier to prove: +```lean +error -keep (name := noInst) +theorem rev_correct : + (rev xs).run = xs.reverse := by + generalize h : (rev xs).run = x + apply Identity.of_wp_run_eq h + mvcgen [rev] +``` +```leanOutput noInst +unsolved goals +case vc1 +α✝ : Type u_1 +xs x : List α✝ +h : (rev xs).run = x +out✝ : List α✝ := [] +⊢ (wp⟦do + let __s ← forIn xs out✝ fun x __s => pure (ForInStep.yield (x :: __s)) + pure __s⟧ + (PostCond.noThrow fun a => { down := a = xs.reverse })).down +``` +When the verification condition is just the original problem, without even any simplification of {name}`bind`, the problem is usually a missing {name}`WPMonad` instance. +The issue can be resolved by adding a suitable instance: +```lean +instance : WPMonad Identity .pure where + wp_pure _ := rfl + wp_bind _ _ := rfl +``` +With this instance, and a suitable invariant, {tactic}`mvcgen` and {tactic}`grind` can prove the theorem. +```lean +theorem rev_correct : + (rev xs).run = xs.reverse := by + generalize h : (rev xs).run = x + apply Identity.of_wp_run_eq h + simp only [rev] + mvcgen invariants + · ⇓⟨xs, out⟩ => + ⌜out = xs.prefix.reverse⌝ + with grind +``` +::: + +### Adequacy Lemmas +%%% +tag := "mvcgen-adequacy" +%%% + +Monads that can be invoked from pure code typically provide a invocation operator that takes any required input state as a parameter and returns either a value paired with an output state or some kind of exceptional value. +Examples include {name}`StateT.run`, {name}`ExceptT.run`, and {name}`Id.run`. +{deftech (key := "mvcgen Adequacy lemmas")}_Adequacy lemmas_ provide a bridge between statements about invocations of monadic programs and those programs' {tech (key := "mvcgen weakest precondition")}[weakest precondition] semantics as given by their {name}`WP` instances. +They show that a property about the invocation is true if its weakest precondition is true. + +{docstring Id.of_wp_run_eq} + +{docstring StateM.of_wp_run_eq} + +{docstring StateM.of_wp_run'_eq} + +{docstring ReaderM.of_wp_run_eq} + +{docstring Except.of_wp_eq} + +{docstring EStateM.of_wp_run_eq} + +## Hoare Triples + +A {deftech (key := "mvcgen Hoare triple")}_Hoare triple_{citep hoare69}[] consists of a precondition, a program, and a postcondition. +Running the program in a state for which the precondition is true results in a state where the postcondition is true. + +{docstring Triple} + +::::syntax term (title := "Hoare Triples") +```grammar +⦃ $_ ⦄ $_ ⦃ $_ ⦄ +``` +:::leanSection +```lean -show +variable [WP m ps] {x : m α} {P : Assertion ps} {Q : PostCond α ps} +``` +{lean}`⦃P⦄ x ⦃Q⦄` is syntactic sugar for {lean}`Triple x P Q`. +::: +:::: + +{docstring Triple.and} + +{docstring Triple.mp} + +## Specification Lemmas + +{deftech (key := "mvcgen Specification lemmas")}_Specification lemmas_ are designated theorems that associate Hoare triples with functions. +When {tactic}`mvcgen` encounters a function, it checks whether there are any registered specification lemmas and attempts to use them to discharge intermediate {tech (key := "mvcgen verification conditions")}[verification conditions]. +If there is no applicable specification lemma, then the connection between the statement's pre- and postconditions will become a verification condition. +Specification lemmas allow compositional reasoning about libraries of monadic code. + +When applied to a theorem whose statement is a Hoare triple, the {attr}`spec` attribute registers the theorem as a specification lemma. +These lemmas are used in order of priority. + +The {attr}`spec` attribute may also be applied to definitions. +On definitions, it indicates that the definition should be unfolded during verification condition generation. + +:::syntax attr (title := "Specification Lemmas") +```grammar +spec $[$_:prio]? +``` +{includeDocstring Lean.Parser.Attr.spec} +::: + +Universally-quantified variables in specification lemmas can be used to relate input states to output states and return values. +These variables are referred to as {deftech (key := "mvcgen schematic variables")}_schematic variables_. + +:::example "Schematic Variables" +```imports -show +import Std.Do +import Std.Tactic.Do +``` +```lean -show +open Std.Do + +set_option mvcgen.warning false + +``` + +The function {name}`double` doubles the value of a {name}`Nat` state: +```lean +def double : StateM Nat Unit := do + modify (2 * ·) +``` +Its specification should _relate_ the initial and final states, but it cannot know their precise values. +The specification uses a schematic variable to stand for the initial state: +```lean +theorem double_spec : + ⦃ fun s => ⌜s = n⌝ ⦄ double ⦃ ⇓ () s => ⌜s = 2 * n⌝ ⦄ := by + simp [double] + mvcgen with grind +``` + +The assertion in the precondition is a function because the {name}`PostShape` of {lean}`StateM Nat` is {lean (type := "PostShape.{0}")}`.arg Nat .pure`, and {lean}`Assertion (.arg Nat .pure)` is {lean}`SPred [Nat]`. + +::: +```lean -show -keep +-- Test preceding examples' claims +#synth WP (StateM Nat) (.arg Nat .pure : PostShape.{0}) +example : Assertion (.arg Nat .pure) = SPred [Nat] := rfl +``` + +## Invariant Specifications + +These types are used in invariants. +The {tech (key := "mvcgen specification lemmas")}[specification lemmas] for {name}`ForIn.forIn` and {name}`ForIn'.forIn'` take parameters of type {name}`Invariant`, and {tactic}`mvcgen` ensures that invariants are not accidentally generated by other automation. + +{docstring Invariant} + +{docstring Invariant.withEarlyReturn} + +Invariants use lists to model the sequence of values in a {keywordOf Lean.Parser.Term.doFor}`for` loop. +The current position in the loop is tracked with a {name}`List.Cursor` that represents a position in a list as a combination of the elements to the left of the position and the elements to the right. +This type is not a traditional zipper, in which the prefix is reversed for efficient movement: it is intended for use in specifications and proofs, not in run-time code, so the prefix is in the original order. + +{docstring List.Cursor} + +{docstring List.Cursor.at} + +{docstring List.Cursor.pos} + +{docstring List.Cursor.current} + +{docstring List.Cursor.tail} + +{docstring List.Cursor.begin} + +{docstring List.Cursor.end} + + +# Verification Conditions + +The {tactic}`mvcgen` tactic converts a goal that's expressed in terms of {name}`SPred` and weakest preconditions to a set of invariants and verification conditions that, together, suffice to prove the original goal. +In particular, {tech (key := "mvcgen Hoare triples")}[Hoare triples] are defined in terms of weakest preconditions, so {tactic}`mvcgen` can be used to prove them. + +:::leanSection +```lean -show +variable [Monad m] [WPMonad m ps] {e : m α} {P : Assertion ps} {Q : PostCond α ps} +``` +The verification conditions for a goal are generated as follows: +1. A number of simplifications and rewrites are applied. +2. The goal should now be of the form {lean}`P ⊢ₛ wp⟦e⟧ Q` (that is, an entailment from some set of stateful assumptions to the weakest precondition that implies a desired postcondition). +3. {tech}[Reducible] constants and definitions marked {attrs}`@[spec]` in the expression {lean}`e` are unfolded. +4. If the expression is an application of an {tech}[auxiliary matching function] or a conditional ({name}`ite` or {name}`dite`), then it is first simplified. + The {tech (key := "match discriminant")}[discriminant] of each matcher is simplified, and the entire term is reduced in an attempt to eliminate the matcher or conditional. + If this fails, then a new goal is generated for each branch. +5. If the expression is an application of a constant, then the applicable lemmas marked {attrs}`@[spec]` are attempted in priority order. + Lean includes specification lemmas for constants such as {name Bind.bind}`bind`, {name Pure.pure}`pure`, and {name}`ForIn.forIn` that result from desugaring {keywordOf Lean.Parser.Term.do}`do`-notation. + Instantiating the lemma will sometimes discharge its premises, in particular schematic variables due to definitional equalities with the goal. + Assumptions of type {name}`Invariant` are never instantiated this way, however. + If the spec lemma's precondition or postcondition do not exactly match those of the goal, then new metavariables are created that prove the necessary entailments. + If these cannot be immediately discharged using simple automation that attempts to use local assumptions and decomposes conjunctions in postconditions, then they remain as verification conditions. +6. Each remaining goal created by this process is recursively processed for verification conditions if it has the form {lean}`P ⊢ₛ wp⟦e⟧ Q`. If not, it is added to the set of invariants or verification conditions. +7. The resulting subgoals for invariants and verification conditions are assigned suitable names in the proof state. +8. Depending on the tactic's configuration parameters, {tactic}`mvcgen_trivial` and {tactic}`mleave` are attempted in each verification condition. +::: + +Verification condition generation can be improved by defining appropriate {tech (key := "mvcgen specification lemmas")}[specification lemmas] for a library. +The presence of good specification lemmas results in fewer generated verification conditions. +Additionally, ensuring that the {tech}[simp normal form] of terms is suitable for pattern matching, and that there are sufficient lemmas in the default simp set to reduce every possible term to that normal form, can lead to more conditionals and pattern matches being eliminated. + +# Enabling `mvcgen` For Monads + +If a monad is implemented in terms of {tech}[monad transformers] that are provided by the Lean standard library, such as {name}`ExceptT` and {name}`StateT`, then it should not require additional instances. +Other monads will require instances of {name}`WP`, {name}`LawfulMonad`, and {name}`WPMonad`. +The tactic has been designed to support monads that model single-threaded control with state that might be interrupted; in other words, the effects that are present in ordinary imperative programming. +More exotic effects have not yet been investigated. + +Once the basic instances are provided, the next step is to prove an {ref "mvcgen-adequacy"}[adequacy lemma]. +This lemma should show that the weakest precondition for running the monadic computation and asserting a desired predicate is in fact sufficient to prove the predicate. + +In addition to the definition of the monad, typical libraries provide a set of primitive operators. +Each of these should be provided with a {tech (key := "mvcgen specification lemma")}[specification lemma]. +It may additionally be useful to make the internals of the state private, and export a carefully-designed set of assertion operators. + +The specification lemmas for the library's primitive operators should ideally be precise specifications of the operators as predicate transformers. +While it's often easier to think in terms of how the operator transforms an input state into an output state, {tech (key := "mvcgen verification condition")}[verification condition] generation will work more reliably when postconditions are completely free. +This allows automation to instantiate the postcondition with the exact precondition of the next statement, rather than needing to show an entailment. +In other words, specifications that specify the precondition as a function of the postcondition work better in practice than specifications that merely relate the pre- and postconditions. + +:::example "Schematic Postconditions" +```imports -show +import Std.Do +import Std.Tactic.Do +``` +```lean -show +open Std.Do + +set_option mvcgen.warning false + +``` + +The function {name}`double` doubles a natural number state: +```lean +def double : StateM Nat Unit := do + modify (2 * ·) +``` +Thinking chronologically, a reasonable specification is that value of the output state is twice that of the input state. +This is expressed using a schematic variable that stands for the initial state: +```lean -keep +theorem double_spec : + ⦃ fun s => ⌜s = n⌝ ⦄ double ⦃ ⇓ () s => ⌜s = 2 * n⌝ ⦄ := by + simp [double] + mvcgen with grind +``` +However, an equivalent specification that treats the postcondition schematically will lead to smaller verification conditions when {name}`double` is used in other functions: +```lean +@[spec] +theorem better_double_spec {Q : PostCond Unit (.arg Nat .pure)} : + ⦃ fun s => Q.1 () (2 * s) ⦄ double ⦃ Q ⦄ := by + simp [double] + mvcgen with grind +``` +The first projection of the postcondition is its stateful assertion. +Now, the precondition merely states that the postcondition should hold for double the initial state. +::: + +:::example "A Logging Monad" +```imports -show +import Std.Do +import Std.Tactic.Do +``` +```lean -show +open Std.Do + +set_option mvcgen.warning false + +``` + +The monad {name}`LogM` maintains an append-only log during a computation: +```lean +structure LogM (β : Type u) (α : Type v) : Type (max u v) where + log : Array β + value : α + +instance : Monad (LogM β) where + pure x := ⟨#[], x⟩ + bind x f := + let { log, value } := f x.value + { log := x.log ++ log, value } +``` +It has a {name}`LawfulMonad` instance as well. +```lean -show +instance : LawfulMonad (LogM β) where + map_const := rfl + id_map x := rfl + seqLeft_eq x y := rfl + seqRight_eq x y := rfl + pure_seq g x := by + simp [pure, Seq.seq, Functor.map] + bind_pure_comp f x := by + simp [pure, bind, Functor.map] + bind_map f x := by + simp [bind, Seq.seq, Functor.map] + pure_bind x f := by + simp [pure, bind] + bind_assoc x f g := by + simp [bind] +``` + +The log can be written to using {name}`log`, and a value and the associated log can be computed using {name}`LogM.run`. +```lean +def log (v : β) : LogM β Unit := { log := #[v], value := () } + +def LogM.run (x : LogM β α) : α × Array β := (x.value, x.log) +``` + +Rather than writing it from scratch, the {name}`WP` instance uses {name}`PredTrans.pushArg`. +This operator was designed to model state monads, but {name}`LogM` can be seen as a state monad that can only append to the state. +This appending is visible in the body of the instance, where the initial state and the log that resulted from the action are appended: +```lean +instance : WP (LogM β) (.arg (Array β) .pure) where + wp + | { log, value } => + PredTrans.pushArg (fun s => PredTrans.pure (value, s ++ log)) +``` + +The {name}`WPMonad` instance also benefits from the conceptual model as a state monad and admits very short proofs: +```lean +instance : WPMonad (LogM β) (.arg (Array β) .pure) where + wp_pure x := by + ext + simp [wp, pure] + + wp_bind _ _ := by + ext + simp [wp, bind] +``` + +The adequacy lemma has one important detail: the result of the weakest precondition transformation is applied to the empty array. +This is necessary because the logging computation has been modeled as an append-only state, so there must be some initial state. +Semantically, the empty array is the correct choice so as to not place items in a log that don't come from the program; technically, it must also be a value that commutes with the append operator on arrays. +```lean +theorem LogM.of_wp_run_eq {x : α × Array β} {prog : LogM β α} + (h : LogM.run prog = x) (P : α × Array β → Prop) : + (⊢ₛ wp⟦prog⟧ (⇓ v l => ⌜P (v, l)⌝) #[]) → P x := by + rw [← h] + intro h' + simp [wp] at h' + exact h' +``` + +Next, each operator in the library should be provided with a specification lemma. +There is only one: {name}`log`. +For new monads, these proofs must often break the abstraction boundaries of {tech (key := "mvcgen Hoare triples")}[Hoare triples] and weakest preconditions; the specifications that they provide can then be used abstractly by clients of the library. +```lean +theorem log_spec {x : β} : + ⦃ fun s => ⌜s = s'⌝ ⦄ log x ⦃ ⇓ () s => ⌜s = s'.push x⌝ ⦄ := by + simp [log, Triple, wp] +``` + +A better specification for {name}`log` uses a schematic postcondition: +```lean +variable {Q : PostCond Unit (.arg (Array β) .pure)} + +@[spec] +theorem log_spec_better {x : β} : + ⦃ fun s => Q.1 () (s.push x) ⦄ log x ⦃ Q ⦄ := by + simp [log, Triple, wp] +``` + +A function {name}`logUntil` that logs all the natural numbers up to some bound will always result in a log whose length is equal to its argument: +```lean +def logUntil (n : Nat) : LogM Nat Unit := do + for i in 0...n do + log i + +theorem logUntil_length : (logUntil n).run.2.size = n := by + generalize h : (logUntil n).run = x + unfold logUntil at h + apply LogM.of_wp_run_eq h + mvcgen invariants + · ⇓⟨xs, _⟩ s => ⌜xs.pos = s.size⌝ + with + simp_all [List.Cursor.pos] <;> + grind [Std.PRange.Nat.size_rco, Std.Rco.length_toList] +``` +::: + +# Proof Mode +%%% +tag := "mvcgen-proof-mode" +%%% + +Stateful goals can be proven using a special _proof mode_ in which goals are rendered with two contexts of hypotheses: the ordinary Lean context, which contains Lean variables, and a special stateful context, which contains assumptions about the monadic state. +In the proof mode, the goal is an {name}`SPred`, rather than a {lean}`Prop`, and the entire goal is equivalent to an entailment relation ({name}`SPred.entails`) from the conjunction of the hypotheses to the conclusion. + +:::syntax Std.Tactic.Do.mgoalStx (title := "Proof Mode Goals") +Proof mode goals are rendered as a series of named hypotheses, one per line, followed by {keywordOf Std.Tactic.Do.mgoalStx}`⊢ₛ` and a goal. +```grammar +$[$_:ident : $t:term]* +⊢ₛ $_:term +``` +::: + +In the proof mode, special tactics manipulate the stateful context. +These tactics are described in {ref "tactic-ref-spred"}[their own section in the tactic reference]. + +When working with concrete monads, {tactic}`mvcgen` typically does not result in stateful proof goals—they are simplified away. +However, monad-polymorphic theorems can lead to stateful goals remaining. + +:::example "Stateful Proofs" +```imports -show +import Std.Do +import Std.Tactic.Do +``` +```lean -show +open Std.Do + +set_option mvcgen.warning false + +``` +The function {name}`bump` increments its state by the indicated amount and returns the resulting value. +```lean +variable [Monad m] [WPMonad m ps] +def bump (n : Nat) : StateT Nat m Nat := do + modifyThe Nat (· + n) + getThe Nat +``` + +This specification lemma for {name}`bump` is proved in an intentionally low-level manner to demonstrate the intermediate proof states: +```lean +theorem bump_correct : + ⦃ fun n => ⌜n = k⌝ ⦄ + bump (m := m) i + ⦃ ⇓ r n => ⌜r = n ∧ n = k + i⌝ ⦄ := by + mintro n_eq_k + unfold bump + unfold modifyThe + mspec + mspec + mpure_intro + constructor + . trivial + . simp_all +``` + +The lemma can also be proved using only the simplifier: +```lean +theorem bump_correct' : + ⦃ fun n => ⌜n = k⌝ ⦄ + bump (m := m) i + ⦃ ⇓ r n => ⌜r = n ∧ n = k + i⌝ ⦄ := by + mintro _ + simp_all [bump] +``` +::: diff --git a/Manual/Tactics/Reference.lean b/Manual/Tactics/Reference.lean index 21d17109d..5b5839271 100644 --- a/Manual/Tactics/Reference.lean +++ b/Manual/Tactics/Reference.lean @@ -1193,6 +1193,9 @@ tag := "tactic-ref-mvcgen" :::tactic "mvcgen" ::: +:::tactic "vcgen" +::: + ## Tactics for Stateful Goals in `Std.Do.SPred` %%% tag := "tactic-ref-spred" diff --git a/Manual/VCGen.lean b/Manual/VCGen.lean index edf8bf7da..18acb68f0 100644 --- a/Manual/VCGen.lean +++ b/Manual/VCGen.lean @@ -9,6 +9,7 @@ import VersoManual import Manual.Meta import Manual.Papers +import Std.WP import Std.Tactic.Do open Verso.Genre Manual @@ -28,34 +29,35 @@ set_option mvcgen.warning false open Manual (comment) -open Std.Do +open Std.WP Lean.Order -#doc (Manual) "The `mvcgen` tactic" => +#doc (Manual) "The `vcgen` tactic" => %%% -tag := "mvcgen-tactic" +tag := "vcgen-tactic" %%% :::tutorials - * {ref "mvcgen-tactic-tutorial" (remote := "tutorials")}[Verifying Imperative Programs Using `mvcgen`] + * {ref "vcgen-tactic-tutorial" (remote := "tutorials")}[Verifying Imperative Programs Using `vcgen`] ::: -The {tactic}`mvcgen` tactic implements a _monadic verification condition generator_: -It breaks down a goal involving a program written using Lean's imperative {keywordOf Lean.Parser.Term.do}`do` notation into a number of smaller {tech}_verification conditions_ ({deftech}[VCs]) that are sufficient to prove the goal. -In addition to a reference that describes the use of {tactic}`mvcgen`, this chapter includes a {ref "mvcgen-tactic-tutorial" (remote := "tutorials")}[tutorial] that can be read independently of the reference. +The {tactic}`vcgen` tactic implements a _verification condition generator_: +It breaks down a goal involving a program, for example one written using Lean's imperative {keywordOf Lean.Parser.Term.do}`do` notation, into a number of smaller {tech}_verification conditions_ ({deftech}[VCs]) that are sufficient to prove the goal. +In addition to a reference that describes the use of {tactic}`vcgen`, this chapter includes a {ref "vcgen-tactic-tutorial" (remote := "tutorials")}[tutorial] that can be read independently of the reference. -In order to use the {tactic}`mvcgen` tactic, {module}`Std.Tactic.Do` must be imported and the namespace {namespace}`Std.Do` must be opened. +In order to use the {tactic}`vcgen` tactic, {module}`Std.WP` and {module}`Std.Tactic.Do` must be imported and the namespaces {namespace}`Std.WP` and {namespace}`Lean.Order` must be opened. +The dependency on {namespace}`Lean.Order` is a temporary measure: this namespace holds the {ref "partial-fixpoint-theory"}[order theory behind `partial_fixpoint`], which is yet to be upstreamed into `Std`. # Overview -The workflow of {tactic}`mvcgen` consists of the following: +The workflow of {tactic}`vcgen` consists of the following: 1. Monadic programs are re-interpreted according to a {tech}[predicate transformer semantics]. An instance of {name}`WP` determines the monad's interpretation. Each program is interpreted as a mapping from arbitrary {tech}[postconditions] to the {tech}[weakest precondition] that would ensure the postcondition. - This step is invisible to most users, but library authors who want to enable their monads to work with {tactic}`mvcgen` need to understand it. + This step is invisible to most users, but library authors who want to enable their monads to work with {tactic}`vcgen` need to understand it. 2. Programs are composed from smaller programs. Each statement in a {keywordOf Lean.Parser.Term.do}`do`-block is associated with a predicate transformer, and there are general-purpose rules for combining these statements with sequencing and control-flow operators. A statement with its pre- and postconditions is called a {tech}_Hoare triple_. @@ -64,10 +66,10 @@ The workflow of {tactic}`mvcgen` consists of the following: 3. Applying the weakest-precondition semantics of a monadic program to a desired proof goal results in the precondition that must hold in order to prove the goal. Any missing steps such as loop invariants or proofs that a statement's precondition implies its postcondition become new subgoals. These missing steps are called the {deftech}_verification conditions_. - The {tactic}`mvcgen` tactic performs this transformation, replacing the goal with its verification conditions. - During this transformation, {tactic}`mvcgen` uses specification lemmas to discharge proofs about individual statements. + The {tactic}`vcgen` tactic performs this transformation, replacing the goal with its verification conditions. + During this transformation, {tactic}`vcgen` uses specification lemmas to discharge proofs about individual statements. 4. After supplying loop invariants, many verification conditions can in practice be discharged automatically. - Those that cannot can be proven using either a {ref "tactic-ref-spred"}[special proof mode] or ordinary Lean tactics, depending on whether they are expressed in the logic of program assertions or as ordinary propositions. + Those that cannot are ordinary Lean goals, provable with ordinary Lean tactics or with the `grind`-mode step of the `with` clause. # Predicate Transformers @@ -75,376 +77,195 @@ The workflow of {tactic}`mvcgen` consists of the following: A {deftech}_predicate transformer semantics_ is an interpretation of programs as functions from predicates to predicates, rather than values to values. A {deftech}_postcondition_ is an assertion that holds after running a program, while a {deftech}_precondition_ is an assertion that must hold prior to running the program in order for the postcondition to be guaranteed to hold. -The predicate transformer semantics used by {tactic}`mvcgen` transforms postconditions into the {deftech}_weakest preconditions_ under which the program will ensure the postcondition. +The predicate transformer semantics used by {tactic}`vcgen` transforms postconditions into the {deftech}_weakest preconditions_ under which the program will ensure the postcondition. An assertion $`P` is weaker than $`P'` if, in all states, $`P'` suffices to prove $`P`, but $`P` does not suffice to prove $`P'`. Logically equivalent assertions are considered to be equal. -The predicates in question are stateful: they can mention the program's current state. +The predicates in question can be stateful: they can mention the program's current state. Furthermore, postconditions can relate the return value and any exceptions thrown by the program to the final state. -{name}`SPred` is a type of predicates that is parameterized over a monadic state, expressed as a list of the types of the fields that make up the state. -The usual logical connectives and quantifiers are defined for {name}`SPred`. -Each monad that can be used with {tactic}`mvcgen` is assigned a state type by an instance of {name}`WP`, and {name}`Assertion` is the corresponding type of assertions for that monad, which is used for preconditions. -{name}`Assertion` is a wrapper around {name}`SPred`: while {name}`SPred` is parameterized by a list of states types, {name}`Assertion` is parameterized by a more informative type that it translates to a list of state types for {name}`SPred`. -A {name}`PostCond` pairs an {name}`Assertion` about a return value with assertions about potential exceptions; the available exceptions are also specified by the monad's {name}`WP` instance. +Each monad that can be used with {tactic}`vcgen` is assigned an assertion type and an exception assertion type by an instance of {name}`WP`. +For a state monad such as {lean}`StateM Nat`, an assertion is a predicate on the state, of type {lean}`Nat → Prop`. +A postcondition additionally takes the return value as its first argument, and the exception postcondition covers each exception that the monad can throw. -## Stateful Predicates +## Assertion Lattices The predicate transformer semantics of monadic programs is based on a logic in which propositions may mention the program's state. Here, “state” refers not only to mutable state, but also to read-only values such as those that are provided via {name}`ReaderT`. -Different monads have different state types available, but each individual state always has a type. -Given a list of state types, {name}`SPred` is a type of predicates over these states. +Different monads have different assertion types, which can be any complete lattice. +More specifically, assertion types instantiate {name}`Assertion`, which is a `class abbrev` over {name}`CompleteLattice` that is recognized by `vcgen`. -{name}`SPred` is not inherently tied to the monadic verification framework. -The related {name}`Assertion` computes a suitable {name}`SPred` for a monad's state as expressed via its {name}`WP` instance's {name}`PostShape` output parameter. +{docstring Assertion} + +The lattice structure provides the logical vocabulary of assertions: + +* The order relation {name Lean.Order.PartialOrder.rel}`⊑` is entailment. +* The meet {name Lean.Order.meet}`⊓` is conjunction and the join {name Lean.Order.join}`⊔` is disjunction. +* The top element {name Lean.Order.top}`⊤` is the trivial assertion and the bottom element {name Lean.Order.bot}`⊥` is the absurd assertion. +* The indexed supremum {name Lean.Order.iSup}`⨆` is existential quantification and the indexed infimum {name Lean.Order.iInf}`⨅` is universal quantification. +* The Heyting implication {name Lean.Order.himp}`⇨` is implication internal to the assertion language. -{docstring Std.Do.SPred} +The difference between entailment and implication is that entailment is a statement in Lean's logic, while implication is internal to the assertion language: for assertions `P` and `Q`, `P ⊑ Q` is a {lean}`Prop` while `P ⇨ Q` is again an assertion. + +{module}`Std.WP` comes with {name}`Assertion` instances for {lean}`Prop`, function types and pairs. +The lattice operations on {lean}`Prop` coincide with the ordinary logical connectives, with entailment being implication. +The lattice operations on a function type such as {lean}`Nat → Prop` operate pointwise, so entailment of state predicates is universally-quantified implication. +The lattice operations on a pair such as {lean}`(Nat → Prop) × (Bool → Prop)` operate componentwise, so entailment of pair predicates is the pair of entailments on the component predicates. ::::leanSection ```lean -show -variable {P : Prop} {σ : List (Type u)} +universe u +variable {P : Prop} {Pred : Type u} [Assertion Pred] ``` -Ordinary propositions that do not mention the state can be used as stateful predicates by adding a trivial universal quantification. -This is written with the syntax {lean (type := "SPred σ")}`⌜P⌝`, which is syntactic sugar for {name}`SPred.pure`. -:::syntax term (title := "Notation for `SPred`") (namespace := Std.Do) +Ordinary propositions that do not mention the state can be embedded into any assertion lattice with corner brackets. +This is written with the syntax {lean (type := "Pred")}`⌜P⌝`, which is notation for {name}`Lean.Order.CompleteLattice.ofProp`. +The popular Iris proof mode uses the same syntax and meaning. +:::syntax term (title := "Embedding Propositions") (namespace := Lean.Order) ```grammar ⌜$_:term⌝ ``` -{includeDocstring Std.Do.«term⌜_⌝»} +{includeDocstring Lean.Order.CompleteLattice.ofProp} ::: :::: -{docstring SPred.pure} +{docstring Lean.Order.CompleteLattice.ofProp} -:::example "Stateful Predicates" +:::example "Assertions for State Monads" ```imports -show -import Std.Do +import Std.WP import Std.Tactic.Do ``` ```lean -show -open Std.Do +open Std.WP Lean.Order set_option mvcgen.warning false ``` The predicate {name}`ItIsSecret` expresses that a state of type {name}`String` is {lean}`"secret"`: ```lean -def ItIsSecret : SPred [String] := fun s => ⌜s = "secret"⌝ -``` -::: - -### Entailment - -Stateful predicates are related by _entailment_. -Entailment of stateful predicates is defined as universally-quantified implication: if $`P` and $`Q` are predicates over a state $`\sigma`, then $`P` entails $`Q` (written $`P \vdash_s Q`) when $`∀ s : \sigma, P(s) → Q(s)`. - -{docstring Std.Do.SPred.entails} - -{docstring Std.Do.SPred.bientails} - -:::syntax term (title := "Notation for `SPred`") (namespace := Std.Do) -```grammar -$_:term ⊢ₛ $_:term -``` -{includeDocstring Std.Do.«term_⊢ₛ_»} - -```grammar -⊢ₛ $_:term -``` -{includeDocstring Std.Do.«term⊢ₛ_»} - -```grammar -$_:term ⊣⊢ₛ $_:term -``` - -{includeDocstring Std.Do.«term_⊣⊢ₛ_»} -::: - -:::leanSection -```lean -show -variable {σ : List (Type u)} {P Q : SPred σ} -``` -The logic of stateful predicates includes an implication connective. -The difference between entailment and implication is that entailment is a statement in Lean's logic, while implication is internal to the stateful logic. -Given stateful predicates {lean}`P` and {lean}`Q` for state {lean}`σ`, {lean (type := "Prop")}`P ⊢ₛ Q` is a {lean}`Prop` while {lean (type := "SPred σ")}`spred(P → Q)` is an {lean}`SPred σ`. -::: - -### Notation - -The syntax of stateful predicates overlaps with that of ordinary Lean terms. -In particular, stateful predicates use the usual syntax for logical connectives and quantifiers. -The syntax associated with stateful predicates is automatically enabled in contexts such as pre- and postconditions where they are clearly intended; other contexts must explicitly opt in to the syntax using {keywordOf Std.Do.«termSpred(_)»}`spred`. -The usual meanings of these operators can be recovered by using the {keywordOf Std.Do.«termTerm(_)»}`term` operator. - -:::syntax term (title := "Predicate Terms") (namespace := Std.Do) -{keywordOf Std.Do.«termSpred(_)»}`spred` indicates that logical connectives and quantifiers should be understood as those pertaining to stateful predicates, while {keywordOf Std.Do.«termTerm(_)»}`term` indicates that they should have the usual meaning. -```grammar -spred($t) -``` -```grammar -term($t) -``` -::: - -### Connectives and Quantifiers - -:::syntax term (title := "Predicate Connectives") (namespace := Std.Do) -```grammar -spred($_ ∧ $_) -``` -Syntactic sugar for {name}`SPred.and`. - -```grammar -spred($_ ∨ $_) -``` -Syntactic sugar for {name}`SPred.or`. - -```grammar -spred(¬ $_) -``` -Syntactic sugar for {name}`SPred.not`. - -```grammar -spred($_ → $_) +def ItIsSecret : String → Prop := fun s => s = "secret" ``` -Syntactic sugar for {name}`SPred.imp`. - -```grammar -spred($_ ↔ $_) +Entailment between such assertions is pointwise implication: +```lean +example : ItIsSecret ⊑ (⌜True⌝ : String → Prop) := by + simp [ItIsSecret, PartialOrder.rel] ``` -Syntactic sugar for {name}`SPred.iff`. ::: +## Exception Postconditions -{docstring SPred.and} - -{docstring SPred.conjunction} - -{docstring SPred.or} +A postcondition for successful termination is a function from the return value to an assertion. +Programs that can throw exceptions additionally require an {deftech}_exception postcondition_, asserting what holds when the program throws an exception. +The exception postcondition type of a given monad is determined by its {name}`WP` instance. -{docstring SPred.not} +For example, the {name}`WP` instance for {lean}`EStateM String Nat Bool` determines {lean}`Nat → Prop` as the assertion type, hence {lean}`Bool → Nat → Prop` as the postcondition type, and {lean}`String → Nat → Prop` as the exception postcondition type. +A monad without exceptions uses {name}`Unit`, and each exception layer of e.g., {name}`ExceptT` contributes an additional exception postcondition as `(ε → Pred) × EPred`, where `Pred` is the assertion type and `EPred` the exception assertion type of the wrapped base monad. +Since unit and pair types come with {name}`Assertion` instances, such exception postcondition stacks are automatically assertions as well. -{docstring SPred.imp} +The {name}`WP` translation turns monad transformer stacks turn into exception postcondition stacks. +The notation `EStack⟨e₁, e₂, ...⟩` abbreviates the type of exception postcondition stack `e₁ × (e₂ × (... × Unit))`, and the notation `estack⟨v₁, v₂, ...⟩` builds a value `(v₁, v₂, ..., ())` of such a stack. -{docstring SPred.iff} - -:::syntax term (title := "Predicate Quantifiers") (namespace := Std.Do) -```grammar -spred(∀ $x:ident, $_) -``` +:::syntax term (title := "Exception Postcondition Stacks") (namespace := Std.WP) ```grammar -spred(∀ $x:ident : $ty, $_) +EStack⟨$_,*⟩ ``` ```grammar -spred(∀ ($x:ident $_* : $ty), $_) +estack⟨$_,*⟩ ``` -```grammar -spred(∀ _, $_) -``` -```grammar -spred(∀ _ : $ty, $_) -``` -```grammar -spred(∀ (_ $_* : $ty), $_) -``` -Each form of universal quantification is syntactic sugar for an invocation of {name}`SPred.forall` on a function that takes the quantified variable as a parameter. - -```grammar -spred(∃ $x:ident, $_) -``` -```grammar -spred(∃ $x:ident : $ty, $_) -``` -```grammar -spred(∃ ($x:ident $_* : $ty), $_) -``` -```grammar -spred(∃ _, $_) -``` -```grammar -spred(∃ _ : $ty, $_) -``` -```grammar -spred(∃ (_ $_* : $ty), $_) -``` -Each form of existential quantification is syntactic sugar for an invocation of {name}`SPred.exists` on a function that takes the quantified variable as a parameter. ::: -{docstring SPred.forall} - -{docstring SPred.exists} - -### Stateful Values - -Just as {name}`SPred` represents predicate over states, {name}`SVal` represents a value that is derived from a state. - -{docstring SVal} - -{docstring SVal.getThe} - -{docstring SVal.StateTuple} - -{docstring SVal.curry} - -{docstring SVal.uncurry} - - -## Assertions - -The language of assertions about monadic programs is parameterized by a {deftech}_postcondition shape_, which describes the inputs to and outputs from a computation in a given monad. -Preconditions may mention the initial values of the monad's state, while postconditions may mention the returned value, the final values of the monad's state, and must furthermore account for any exceptions that could have been thrown. -The postcondition shape of a given monad determines the states and exceptions in the monad. -{name}`PostShape.pure` describes a monad in which assertions may not mention any states, {name}`PostShape.arg` describes a state value, and {name}`PostShape.except` describes a possible exception. -Because these constructors can be continually added, the postcondition shape of a monad transformer can be defined in terms of the postcondition shape of the underlying transformed monad. -Behind the scenes, an {name}`Assertion` is translated into an appropriate {name}`SPred` by translating the postcondition shape into a list of state types, discarding exceptions. - -{docstring PostShape} - -{docstring PostShape.args} - -{docstring Assertion} - -{docstring PostCond} - -:::syntax term (title := "Postconditions") -```grammar -⇓ $_* => $_ -``` -Syntactic sugar for a nested sequence of product constructors, terminating in {lean}`()`, in which the first element is an assertion about non-exceptional return values and the remaining elements are assertions about the exceptional cases for a postcondition. -::: - - -{docstring ExceptConds} +{TODO}[I think the partial vs. total correctness discussion should maybe happen after we have actually introduced Triple? It discusses its syntax.] :::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} -``` -Postconditions for programs that might throw exceptions come in two varieties. The {deftech}_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. The {deftech}_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. -::: - - -:::syntax term (title := "Exception-Free Postconditions") -```grammar -⇓ $_* => $_ +variable {m : Type u → Type v} [Monad m] {Pred EPred : Type u} [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {P : Pred} {α : Type u} {prog : m α} {Q' : α → Pred} ``` -{includeDocstring PostCond.noThrow} +Specifications for programs that might throw exceptions come in two varieties. The {deftech}_total correctness interpretation_ {lean}`⦃P⦄ prog ⦃Q'⦄` asserts that, given {lean}`P` holds, then {lean}`prog` terminates normally _and_ {lean}`Q'` holds for the result. The {deftech}_partial correctness interpretation_ {lean}`⦃P⦄ prog ⦃Q'; ⊤⦄` asserts that, given {lean}`P` holds, and _if_ {lean}`prog` terminates normally _then_ {lean}`Q'` holds for the result. +A triple without an explicit exception postcondition carries the bottom assertion {lean}`(⊥ : EPred)` and thus has the total interpretation; between `⊥` and `⊤`, the exception postcondition expresses a spectrum of correctness properties. ::: -{docstring PostCond.noThrow} - -:::syntax term (title := "Partial Postconditions") -```grammar -⇓? $_* => $_ -``` -{includeDocstring PostCond.mayThrow} -::: - -{docstring PostCond.mayThrow} - -:::syntax term (title := "Postcondition Entailment") -```grammar -$_ ⊢ₚ $_ -``` -Syntactic sugar for {name}`PostCond.entails` -::: - -{docstring PostCond.entails} - - -:::syntax term (title := "Postcondition Conjunction") -```grammar -$_ ∧ₚ $_ -``` -Syntactic sugar for {name}`PostCond.and` -::: - -{docstring PostCond.and} - -:::syntax term (title := "Postcondition Implication") -```grammar -$_ →ₚ $_ -``` -Syntactic sugar for {name}`PostCond.imp` -::: - -{docstring PostCond.imp} - - ## Predicate Transformers -A predicate transformer is a function from postconditions for some postcondition state into assertions for that state. -The function must be {deftech}_conjunctive_, which means it must distribute over {name}`PostCond.and`. +```lean -show +universe u v w +variable {Pred : Type u} {EPred : Type v} {α : Type w} [Assertion Pred] [Assertion EPred] +``` -{docstring PredTrans} +A predicate transformer is a function from postconditions into assertions that describe preconditions. -{docstring PredTrans.Conjunctive} +{docstring Lean.Order.PredTrans} -{docstring PredTrans.Monotonic} +{docstring Lean.Order.PredTrans.apply} :::leanSection ```lean -show -variable {σ : List (Type u)} {ps : PostShape} {x y : PredTrans ps α} {Q : Assertion ps} +variable {x y : PredTrans Pred EPred α} {post : α → Pred} {epost : EPred} ``` -The {inst}`LE PredTrans` instance is defined in terms of their logical strength; one transformer is stronger than another if the result of applying it always entails the result of applying the other. -In other words, {lean}`∀ Q, y Q ⊢ₛ x Q`, then {lean}`x ≤ y`. -This means that stronger predicate transformers are considered greater than weaker ones. +The partial order on predicate transformers is inherited pointwise from the assertion lattice: {lean}`x ⊑ y` when {lean}`x.apply post epost ⊑ y.apply post epost` for all {lean}`post` and {lean}`epost`. +A predicate transformer is often {deftech}_monotone_, which means it must preserve entailment: the stronger the postcondition, the stronger the resulting precondition. + +{docstring Lean.Order.PredTrans.monotone} ::: Predicate transformers form a monad. -The {name}`pure` operator is the identity transformer; it simply instantiates the postcondition with the its argument. +The {name}`pure` operator is the identity transformer; it simply instantiates the postcondition with its argument. The {name}`bind` operator composes predicate transformers. -{docstring PredTrans.pure} - -{docstring PredTrans.bind} +{docstring Lean.Order.instMonadPredTrans} -The helper operators {name}`PredTrans.pushArg`, {name}`PredTrans.pushExcept`, and {name}`PredTrans.pushOption` modify a predicate transformer by adding a standard side effect. +The helper operators {name}`Lean.Order.pushArg`, {name}`PredTrans.pushExceptT`, and {name}`PredTrans.pushOptionT` modify a predicate transformer by adding a standard side effect. They are used to implement the {name}`WP` instances for transformers such as {name}`StateT`, {name}`ExceptT`, and {name}`OptionT`; they can also be used to implement monads that can be thought of in terms of one of these. -For example, {name}`PredTrans.pushArg` is typically used for state monads, but can also be used to implement a reader monad's instance, treating the reader's value as read-only state. +For example, {name}`Lean.Order.pushArg` is typically used for state monads, but can also be used to implement a reader monad's instance, treating the reader's value as read-only state. -{docstring PredTrans.pushArg} +{docstring Lean.Order.pushArg} -{docstring PredTrans.pushExcept} +{docstring PredTrans.pushExceptT} -{docstring PredTrans.pushOption} +{docstring PredTrans.pushOptionT} ### Weakest Preconditions -The {tech}[weakest precondition] semantics of a monad are provided by the {name}`WP` type class. -Instances of {name}`WP` determine the monad's postcondition shape and provide the logical rules for interpreting the monad's operations as a predicate transformer in its postcondition shape. +```lean -show +variable {Prog : Type u} {Value : Type v} [WP Prog Value Pred EPred] {x : Prog} {post : Value → Pred} {epost : EPred} +``` + +The {tech}[weakest precondition] semantics of a program type are provided by the {name}`WP` type class. +An instance {lean}`WP Prog Value Pred EPred` interprets programs of type {lean}`Prog` with results of type {lean}`Value` as monotone predicate transformers over the assertion type {lean}`Pred` and the exception postcondition type {lean}`EPred`. +The type {lean}`Prog` determines {lean}`Value`, {lean}`Pred` and {lean}`EPred` as {name}`outParam`s. +The function {name}`wp` applies the interpretation: {lean}`wp x post epost` is the weakest precondition under which the program {lean}`x` establishes the postcondition {lean}`post` and the exception postcondition {lean}`epost`. {docstring WP} -:::syntax term (title := "Weakest Preconditions") -```grammar -wp⟦$_ $[: $_]?⟧ -``` -{includeDocstring Std.Do.«termWp⟦_:_⟧»} -::: +{docstring WP.wp} + +A program `x` that is {deftech}_conjunctive_ distributes a weakest precondition of a meet of two postconditions into a meet of the weakest preconditions of the postconditions. +The type class {name}`WPConjunctive` captures this property, which allows for combining two specifications for `x` into a single strongest one, for example ({name}`Triple.and`). + +{docstring WPConjunctive} -### Weakest Precondition Monad Morphisms +### Monads preserving weakest preconditions -Most of the built-in specification lemmas for {tactic}`mvcgen` relies on the presence of a {name}`WPMonad` instance, in addition to the {name}`WP` instance. -In addition to being lawful, weakest preconditions of the monad's implementations of {name}`pure` and {name}`bind` should correspond to the {name}`pure` and {name}`bind` operators for the predicate transformer monad. -Without a {name}`WPMonad` instance, {tactic}`mvcgen` typically returns the original proof goal unchanged. +Most of the built-in specification lemmas for {tactic}`vcgen` rely on the presence of a {name}`WPMonad` instance. +A {name}`WPMonad` instance carries the {name}`WP` interpretation for every result type and asserts that this interpretation is sound for the monad's implementations of {name Pure.pure}`pure` and {name Bind.bind}`bind`. +This means that to prove something about a do block, it suffices to prove it about the chain of elements of the do block. +This unlocks compositional reasoning about do blocks. {docstring WPMonad} :::example "Missing `WPMonad` Instance" ```imports -show -import Std.Do +import Std.WP import Std.Tactic.Do ``` ```lean -show -open Std.Do +open Std.WP Lean.Order set_option mvcgen.warning false ``` -The single-field structure {name}`Identity` acts like the identity monad {name}`Id`. It has a {name}`WP` instance, but no {name}`WPMonad` instance: +The single-field structure {name}`Identity` acts like the identity monad {name}`Id`: ```lean structure Identity (α : Type u) where run : α @@ -455,14 +276,13 @@ instance : Monad Identity where pure x := ⟨x⟩ bind x f := f x.run -instance : WP Identity .pure where - wp x := PredTrans.pure x.run - -theorem Identity.of_wp_run_eq {x : α} {prog : Identity α} - (h : Identity.run prog = x) (P : α → Prop) : - (⊢ₛ wp⟦prog⟧ (⇓ a => ⟨P a⟩)) → P x := by - simp_all [WP.wp, ← h] +def rev (xs : List α) : Identity (List α) := do + let mut out := [] + for x in xs do + out := x :: out + return out ``` +{name}`rev` is correct if it is equal to {name}`List.reverse`. ```lean -show instance : LawfulMonad Identity := @@ -472,61 +292,67 @@ instance : LawfulMonad Identity := (bind_assoc := fun _ _ _ => rfl) ``` -The missing instance prevents {tactic}`mvcgen` from using its specifications for {name}`pure` and {name}`bind`. -This tends to show up as a verification condition that's equal to the original goal. -This function that reverses a list: +The {name}`WP` interpretation of {name}`Identity` is a plain definition marked {attr}`instance_reducible`, following the pattern of the interpretations in {module}`Std.WP`: +{TODO}[It is a wart of `vcgen` that we cannot declare the WP instance below. I'll think about fixing it by canonicalizing `WPMonad.toWP` to the `WP` instance, but not in time for 4.35. Let's maybe leave an "under construction" sign for the reader.] ```lean -def rev (xs : List α) : Identity (List α) := do - let mut out := [] - for x in xs do - out := x :: out - return out +@[instance_reducible] def Identity.wpInst : + WP (Identity α) α Prop EStack⟨⟩ where + wpTrans x := ⟨fun post _ => post x.run⟩ + wp_trans_monotone x := fun _ _ _ _ _ hpost => hpost x.run + +section OnlyWP + +attribute [local instance] Identity.wpInst -- working around the wart ``` -It is correct if it is equal to {name}`List.reverse`. -However, {tactic}`mvcgen` does not make the goal easier to prove: -```lean +error -keep (name := noInst) -theorem rev_correct : +This interpretation alone suffices to state weakest preconditions and to prove an adequacy lemma, but not to run {tactic}`vcgen`: +```lean +error (name := noInst) +theorem Identity.of_run_eq_wp' {x : α} {prog : Identity α} + (h : Identity.run prog = x) (P : α → Prop) + (hwp : wp prog P ()) : P x := by + simp_all [wp, WP.wpTrans, ← h] + +theorem rev_correct_bad {xs : List α} : (rev xs).run = xs.reverse := by generalize h : (rev xs).run = x - apply Identity.of_wp_run_eq h - mvcgen [rev] + apply Identity.of_run_eq_wp' h + vcgen [rev] + +end OnlyWP ``` +The specifications for {name}`pure` and {name}`bind` require a {name}`WPMonad` instance for {name}`Identity`, so {tactic}`vcgen` reports that it cannot take the program apart: ```leanOutput noInst -unsolved goals -case vc1 -α✝ : Type u_1 -xs x : List α✝ -h : (rev xs).run = x -out✝ : List α✝ := [] -⊢ (wp⟦do - let __s ← forIn xs out✝ fun x __s => pure (ForInStep.yield (x :: __s)) - pure __s⟧ - (PostCond.noThrow fun a => { down := a = xs.reverse })).down -``` -When the verification condition is just the original problem, without even any simplification of {name}`bind`, the problem is usually a missing {name}`WPMonad` instance. -The issue can be resolved by adding a suitable instance: +No spec applicable to program (forIn xs [] fun x __s => pure (ForInStep.yield (x :: __s))) >>= + pure in monad Identity. Candidates were [SpecProof.global Std.WP.Spec.bind]. +``` +The issue can be resolved by defining a {name}`WPMonad` instance whose {name}`WPMonad.toWP` field carries the interpretation: ```lean -instance : WPMonad Identity .pure where - wp_pure _ := rfl - wp_bind _ _ := rfl +instance : WPMonad Identity Prop EStack⟨⟩ where + toWP _ := Identity.wpInst + pure_le_wp_pure x post epost := PartialOrder.rel_refl + bind_le_wp_bind x f post epost := PartialOrder.rel_refl ``` -With this instance, and a suitable invariant, {tactic}`mvcgen` and {tactic}`grind` can prove the theorem. +With this instance, and a suitable invariant, {tactic}`vcgen` and the {tactic}`grind`-mode tactic `finish` can prove the theorem. ```lean -theorem rev_correct : +theorem Identity.of_run_eq_wp {x : α} {prog : Identity α} + (h : Identity.run prog = x) (P : α → Prop) + (hwp : wp prog P ()) : P x := by + simp_all [wp, WP.wpTrans, ← h] + +theorem rev_correct {xs : List α} : (rev xs).run = xs.reverse := by generalize h : (rev xs).run = x - apply Identity.of_wp_run_eq h + apply Identity.of_run_eq_wp h simp only [rev] - mvcgen invariants - · ⇓⟨xs, out⟩ => - ⌜out = xs.prefix.reverse⌝ - with grind + set_option trace.Elab.Tactic.Do.vcgen true in + vcgen invariants + · fun pref suff out => out = pref.reverse + with finish ``` ::: ### Adequacy Lemmas %%% -tag := "mvcgen-adequacy" +tag := "vcgen-adequacy" %%% Monads that can be invoked from pure code typically provide a invocation operator that takes any required input state as a parameter and returns either a value paired with an output state or some kind of exceptional value. @@ -534,17 +360,19 @@ Examples include {name}`StateT.run`, {name}`ExceptT.run`, and {name}`Id.run`. {deftech}_Adequacy lemmas_ provide a bridge between statements about invocations of monadic programs and those programs' {tech}[weakest precondition] semantics as given by their {name}`WP` instances. They show that a property about the invocation is true if its weakest precondition is true. -{docstring Id.of_wp_run_eq} +{docstring Id.of_run_eq_wp} -{docstring StateM.of_wp_run_eq} +{docstring StateM.of_run_eq_wp} -{docstring StateM.of_wp_run'_eq} +{docstring StateM.of_run'_eq_wp} -{docstring ReaderM.of_wp_run_eq} +{docstring ReaderM.of_run_eq_wp} -{docstring Except.of_wp_eq} +{docstring Except.of_eq_wp} -{docstring EStateM.of_wp_run_eq} +{docstring Option.of_eq_wp} + +{docstring EStateM.of_run_eq_wp} ## Hoare Triples @@ -557,11 +385,16 @@ Running the program in a state for which the precondition is true results in a s ```grammar ⦃ $_ ⦄ $_ ⦃ $_ ⦄ ``` +```grammar +⦃ $_ ⦄ $_ ⦃ $_; $_ ⦄ +``` :::leanSection ```lean -show -variable [WP m ps] {x : m α} {P : Assertion ps} {Q : PostCond α ps} +universe z +variable {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x : Prog} {P : Pred} {Q : Value → Pred} {E : EPred} ``` -{lean}`⦃P⦄ x ⦃Q⦄` is syntactic sugar for {lean}`Triple x P Q`. +{lean}`⦃ P ⦄ x ⦃ Q; E ⦄` is syntactic sugar for {lean}`Triple x P Q E`. +When the exception postcondition is omitted, as in {lean}`⦃ P ⦄ x ⦃ Q ⦄`, it defaults to the bottom assertion `⊥`, asserting that the program throws no exception. ::: :::: @@ -572,7 +405,7 @@ variable [WP m ps] {x : m α} {P : Assertion ps} {Q : PostCond α ps} ## Specification Lemmas {deftech}_Specification lemmas_ are designated theorems that associate Hoare triples with functions. -When {tactic}`mvcgen` encounters a function, it checks whether there are any registered specification lemmas and attempts to use them to discharge intermediate {tech}[verification conditions]. +When {tactic}`vcgen` encounters a function, it checks whether there are any registered specification lemmas and attempts to use them to discharge intermediate {tech}[verification conditions]. If there is no applicable specification lemma, then the connection between the statement's pre- and postconditions will become a verification condition. Specification lemmas allow compositional reasoning about libraries of monadic code. @@ -594,11 +427,11 @@ These variables are referred to as {deftech}_schematic variables_. :::example "Schematic Variables" ```imports -show -import Std.Do +import Std.WP import Std.Tactic.Do ``` ```lean -show -open Std.Do +open Std.WP Lean.Order set_option mvcgen.warning false @@ -612,88 +445,72 @@ def double : StateM Nat Unit := do Its specification should _relate_ the initial and final states, but it cannot know their precise values. The specification uses a schematic variable to stand for the initial state: ```lean -theorem double_spec : - ⦃ fun s => ⌜s = n⌝ ⦄ double ⦃ ⇓ () s => ⌜s = 2 * n⌝ ⦄ := by +theorem double_spec {n : Nat} : + ⦃ fun s => s = n ⦄ double ⦃ fun _ s => s = 2 * n ⦄ := by simp [double] - mvcgen with grind + vcgen with finish ``` -The assertion in the precondition is a function because the {name}`PostShape` of {lean}`StateM Nat` is {lean (type := "PostShape.{0}")}`.arg Nat .pure`, and {lean}`Assertion (.arg Nat .pure)` is {lean}`SPred [Nat]`. +The assertion in the precondition is a function because the assertion type of {lean}`StateM Nat` is {lean}`Nat → Prop`. ::: ```lean -show -keep -- Test preceding examples' claims -#synth WP (StateM Nat) (.arg Nat .pure : PostShape.{0}) -example : Assertion (.arg Nat .pure) = SPred [Nat] := rfl +#synth WP (StateM Nat Unit) Unit (Nat → Prop) EStack⟨⟩ ``` ## Invariant Specifications These types are used in invariants. -The {tech}[specification lemmas] for {name}`ForIn.forIn` and {name}`ForIn'.forIn'` take parameters of type {name}`Invariant`, and {tactic}`mvcgen` ensures that invariants are not accidentally generated by other automation. +The {tech}[specification lemmas] for {name}`ForIn.forIn` and {name}`ForIn'.forIn'` take parameters of type {name}`Invariant`, and {tactic}`vcgen` ensures that invariants are not accidentally generated by other automation. {docstring Invariant} -{docstring Invariant.withEarlyReturn} - Invariants use lists to model the sequence of values in a {keywordOf Lean.Parser.Term.doFor}`for` loop. -The current position in the loop is tracked with a {name}`List.Cursor` that represents a position in a list as a combination of the elements to the left of the position and the elements to the right. -This type is not a traditional zipper, in which the prefix is reversed for efficient movement: it is intended for use in specifications and proofs, not in run-time code, so the prefix is in the original order. - -{docstring List.Cursor} - -{docstring List.Cursor.at} - -{docstring List.Cursor.pos} - -{docstring List.Cursor.current} - -{docstring List.Cursor.tail} - -{docstring List.Cursor.begin} - -{docstring List.Cursor.end} +An invariant is a function of the prefix of elements that the loop has already consumed, the suffix of elements that remain, the current accumulator state, and any further state arguments of the monad's assertion language. +{docstring Invariant.withEarlyReturnNewDo} # Verification Conditions -The {tactic}`mvcgen` tactic converts a goal that's expressed in terms of {name}`SPred` and weakest preconditions to a set of invariants and verification conditions that, together, suffice to prove the original goal. -In particular, {tech}[Hoare triples] are defined in terms of weakest preconditions, so {tactic}`mvcgen` can be used to prove them. +The {tactic}`vcgen` tactic converts a goal that's expressed in terms of weakest preconditions to a set of invariants and verification conditions that, together, suffice to prove the original goal. +In particular, {tech}[Hoare triples] are defined in terms of weakest preconditions, so {tactic}`vcgen` can be used to prove them. :::leanSection ```lean -show -variable [Monad m] [WPMonad m ps] {e : m α} {P : Assertion ps} {Q : PostCond α ps} +variable {m : Type u → Type v} [Monad m] {Pred EPred : Type u} [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {e : m α} {P : Pred} {Q : α → Pred} {E : EPred} ``` +{TODO}[This is not completely faithful to the current implementation and does not talk about advanced topics like frameprocs. But it is a good model to keep for now, I think] The verification conditions for a goal are generated as follows: -1. A number of simplifications and rewrites are applied. -2. The goal should now be of the form {lean}`P ⊢ₛ wp⟦e⟧ Q` (that is, an entailment from some set of stateful assumptions to the weakest precondition that implies a desired postcondition). -3. {tech}[Reducible] constants and definitions marked {attrs}`@[spec]` in the expression {lean}`e` are unfolded. -4. If the expression is an application of an {tech}[auxiliary matching function] or a conditional ({name}`ite` or {name}`dite`), then it is first simplified. +1. A number of simplifications and rewrites are applied, and the goal context is internalized into `grind`'s E-graph. +2. The goal should now be of the form {lean}`P ⊑ wp e Q E` (that is, an entailment from some assertion to the weakest precondition that implies a desired postcondition). +3. If the expression is an application of an {tech}[auxiliary matching function] or a conditional ({name}`ite` or {name}`dite`), then it is first simplified. The {tech (key := "match discriminant")}[discriminant] of each matcher is simplified, and the entire term is reduced in an attempt to eliminate the matcher or conditional. If this fails, then a new goal is generated for each branch. -5. If the expression is an application of a constant, then the applicable lemmas marked {attrs}`@[spec]` are attempted in priority order. +4. If the expression is an application of a constant, then the applicable lemmas marked {attrs}`@[spec]` are attempted in priority order. Lean includes specification lemmas for constants such as {name Bind.bind}`bind`, {name Pure.pure}`pure`, and {name}`ForIn.forIn` that result from desugaring {keywordOf Lean.Parser.Term.do}`do`-notation. Instantiating the lemma will sometimes discharge its premises, in particular schematic variables due to definitional equalities with the goal. - Assumptions of type {name}`Invariant` are never instantiated this way, however. + Assumptions of a type registered with {attr}`spec_invariant_type` are never instantiated this way, however. If the spec lemma's precondition or postcondition do not exactly match those of the goal, then new metavariables are created that prove the necessary entailments. If these cannot be immediately discharged using simple automation that attempts to use local assumptions and decomposes conjunctions in postconditions, then they remain as verification conditions. -6. Each remaining goal created by this process is recursively processed for verification conditions if it has the form {lean}`P ⊢ₛ wp⟦e⟧ Q`. If not, it is added to the set of invariants or verification conditions. -7. The resulting subgoals for invariants and verification conditions are assigned suitable names in the proof state. -8. Depending on the tactic's configuration parameters, {tactic}`mvcgen_trivial` and {tactic}`mleave` are attempted in each verification condition. +5. Each remaining goal created by this process is recursively processed for verification conditions if it has the form {lean}`P ⊑ wp e Q E`. If not, it is added to the set of invariants or verification conditions. +6. The resulting subgoals for invariants and verification conditions are assigned suitable names in the proof state. +7. An `until` clause stops VC generation at the first program that matches the given pattern. + A `with` clause runs the given `grind`-mode step on every remaining verification condition inside the internalized context. ::: Verification condition generation can be improved by defining appropriate {tech}[specification lemmas] for a library. The presence of good specification lemmas results in fewer generated verification conditions. Additionally, ensuring that the {tech}[simp normal form] of terms is suitable for pattern matching, and that there are sufficient lemmas in the default simp set to reduce every possible term to that normal form, can lead to more conditionals and pattern matches being eliminated. -# Enabling `mvcgen` For Monads +# Enabling `vcgen` For Monads If a monad is implemented in terms of {tech}[monad transformers] that are provided by the Lean standard library, such as {name}`ExceptT` and {name}`StateT`, then it should not require additional instances. Other monads will require instances of {name}`WP`, {name}`LawfulMonad`, and {name}`WPMonad`. The tactic has been designed to support monads that model single-threaded control with state that might be interrupted; in other words, the effects that are present in ordinary imperative programming. More exotic effects have not yet been investigated. -Once the basic instances are provided, the next step is to prove an {ref "mvcgen-adequacy"}[adequacy lemma]. +Once the basic instances are provided, the next step is to prove an {ref "vcgen-adequacy"}[adequacy lemma]. This lemma should show that the weakest precondition for running the monadic computation and asserting a desired predicate is in fact sufficient to prove the predicate. In addition to the definition of the monad, typical libraries provide a set of primitive operators. @@ -707,11 +524,11 @@ In other words, specifications that specify the precondition as a function of th :::example "Schematic Postconditions" ```imports -show -import Std.Do +import Std.WP import Std.Tactic.Do ``` ```lean -show -open Std.Do +open Std.WP Lean.Order set_option mvcgen.warning false @@ -725,30 +542,29 @@ def double : StateM Nat Unit := do Thinking chronologically, a reasonable specification is that value of the output state is twice that of the input state. This is expressed using a schematic variable that stands for the initial state: ```lean -keep -theorem double_spec : - ⦃ fun s => ⌜s = n⌝ ⦄ double ⦃ ⇓ () s => ⌜s = 2 * n⌝ ⦄ := by +theorem double_spec {n : Nat} : + ⦃ fun s => s = n ⦄ double ⦃ fun _ s => s = 2 * n ⦄ := by simp [double] - mvcgen with grind + vcgen with finish ``` However, an equivalent specification that treats the postcondition schematically will lead to smaller verification conditions when {name}`double` is used in other functions: ```lean @[spec] -theorem better_double_spec {Q : PostCond Unit (.arg Nat .pure)} : - ⦃ fun s => Q.1 () (2 * s) ⦄ double ⦃ Q ⦄ := by +theorem better_double_spec {Q : Unit → Nat → Prop} : + ⦃ fun s => Q () (2 * s) ⦄ double ⦃ Q ⦄ := by simp [double] - mvcgen with grind + vcgen with finish ``` -The first projection of the postcondition is its stateful assertion. Now, the precondition merely states that the postcondition should hold for double the initial state. ::: :::example "A Logging Monad" ```imports -show -import Std.Do +import Std.WP import Std.Tactic.Do ``` ```lean -show -open Std.Do +open Std.WP Lean.Order set_option mvcgen.warning false @@ -792,58 +608,52 @@ def log (v : β) : LogM β Unit := { log := #[v], value := () } def LogM.run (x : LogM β α) : α × Array β := (x.value, x.log) ``` -Rather than writing it from scratch, the {name}`WP` instance uses {name}`PredTrans.pushArg`. +Rather than writing it from scratch, the {name}`WP` interpretation inside the {name}`WPMonad` instance uses {name}`Lean.Order.pushArg`. This operator was designed to model state monads, but {name}`LogM` can be seen as a state monad that can only append to the state. This appending is visible in the body of the instance, where the initial state and the log that resulted from the action are appended: ```lean -instance : WP (LogM β) (.arg (Array β) .pure) where - wp - | { log, value } => - PredTrans.pushArg (fun s => PredTrans.pure (value, s ++ log)) -``` - -The {name}`WPMonad` instance also benefits from the conceptual model as a state monad and admits very short proofs: -```lean -instance : WPMonad (LogM β) (.arg (Array β) .pure) where - wp_pure x := by - ext - simp [wp, pure] +@[instance_reducible] +def LogM.instWP : WP (LogM β α) α (Array β → Prop) EStack⟨⟩ where + wpTrans | { log, value } => pushArg (fun s => pure (value, s ++ log)) + wp_trans_monotone x := fun _ _ _ _ _ hpost s => + hpost x.value (s ++ x.log) - wp_bind _ _ := by - ext - simp [wp, bind] +instance : WPMonad (LogM β) (Array β → Prop) EStack⟨⟩ where + toWP _ := LogM.instWP + pure_le_wp_pure x post epost := by simp [wp, WP.wpTrans, pure] + bind_le_wp_bind x f post epost := by simp [wp, WP.wpTrans, bind] ``` -The adequacy lemma has one important detail: the result of the weakest precondition transformation is applied to the empty array. +The adequacy lemma has one important detail: the weakest precondition is applied to the empty array. This is necessary because the logging computation has been modeled as an append-only state, so there must be some initial state. Semantically, the empty array is the correct choice so as to not place items in a log that don't come from the program; technically, it must also be a value that commutes with the append operator on arrays. ```lean -theorem LogM.of_wp_run_eq {x : α × Array β} {prog : LogM β α} - (h : LogM.run prog = x) (P : α × Array β → Prop) : - (⊢ₛ wp⟦prog⟧ (⇓ v l => ⌜P (v, l)⌝) #[]) → P x := by +theorem LogM.of_run_eq_wp {α : Type u} {β : Type v} + {x : α × Array β} {prog : LogM β α} + (h : LogM.run prog = x) (P : α × Array β → Prop) + (hwp : wp prog (fun v l => P (v, l)) () #[]) : P x := by rw [← h] - intro h' - simp [wp] at h' - exact h' + simp [wp, WP.wpTrans] at hwp + exact hwp ``` Next, each operator in the library should be provided with a specification lemma. There is only one: {name}`log`. For new monads, these proofs must often break the abstraction boundaries of {tech}[Hoare triples] and weakest preconditions; the specifications that they provide can then be used abstractly by clients of the library. ```lean -theorem log_spec {x : β} : - ⦃ fun s => ⌜s = s'⌝ ⦄ log x ⦃ ⇓ () s => ⌜s = s'.push x⌝ ⦄ := by - simp [log, Triple, wp] +theorem log_spec {x : β} {s' : Array β} : + ⦃ fun s => s = s' ⦄ log x ⦃ fun _ s => s = s'.push x ⦄ := by + constructor + simp [log, wp, WP.wpTrans] ``` A better specification for {name}`log` uses a schematic postcondition: ```lean -variable {Q : PostCond Unit (.arg (Array β) .pure)} - @[spec] -theorem log_spec_better {x : β} : - ⦃ fun s => Q.1 () (s.push x) ⦄ log x ⦃ Q ⦄ := by - simp [log, Triple, wp] +theorem log_spec_better {x : β} {Q : Unit → Array β → Prop} : + ⦃ fun s => Q () (s.push x) ⦄ log x ⦃ Q ⦄ := by + constructor + simp [log, wp, WP.wpTrans] ``` A function {name}`logUntil` that logs all the natural numbers up to some bound will always result in a log whose length is equal to its argument: @@ -852,83 +662,59 @@ def logUntil (n : Nat) : LogM Nat Unit := do for i in 0...n do log i -theorem logUntil_length : (logUntil n).run.2.size = n := by +theorem logUntil_length {n : Nat} : (logUntil n).run.2.size = n := by generalize h : (logUntil n).run = x unfold logUntil at h - apply LogM.of_wp_run_eq h - mvcgen invariants - · ⇓⟨xs, _⟩ s => ⌜xs.pos = s.size⌝ - with - simp_all [List.Cursor.pos] <;> - grind [Std.PRange.Nat.size_rco, Std.Rco.length_toList] + apply LogM.of_run_eq_wp h + vcgen invariants + · fun pref suff _ s => pref.length = s.size + all_goals simp_all [Std.Internal.ForIn.toList_rco] ``` ::: -# Proof Mode +# Discharging Verification Conditions %%% -tag := "mvcgen-proof-mode" +tag := "vcgen-proof-mode" %%% -Stateful goals can be proven using a special _proof mode_ in which goals are rendered with two contexts of hypotheses: the ordinary Lean context, which contains Lean variables, and a special stateful context, which contains assumptions about the monadic state. -In the proof mode, the goal is an {name}`SPred`, rather than a {lean}`Prop`, and the entire goal is equivalent to an entailment relation ({name}`SPred.entails`) from the conjunction of the hypotheses to the conclusion. - -:::syntax Std.Tactic.Do.mgoalStx (title := "Proof Mode Goals") -Proof mode goals are rendered as a series of named hypotheses, one per line, followed by {keywordOf Std.Tactic.Do.mgoalStx}`⊢ₛ` and a goal. -```grammar -$[$_:ident : $t:term]* -⊢ₛ $_:term -``` -::: - -In the proof mode, special tactics manipulate the stateful context. -These tactics are described in {ref "tactic-ref-spred"}[their own section in the tactic reference]. +The verification conditions that {tactic}`vcgen` produces are ordinary Lean goals, so any tactic can discharge them. +The `with` clause runs a single `grind`-mode step, typically `finish`, on every remaining verification condition. +The step runs inside the goal context that {tactic}`vcgen` internalized into `grind`'s E-graph during generation, so the context is not re-internalized for every verification condition. -When working with concrete monads, {tactic}`mvcgen` typically does not result in stateful proof goals—they are simplified away. -However, monad-polymorphic theorems can lead to stateful goals remaining. +When working with concrete monads, the verification conditions speak directly about result values and states. +Monad-polymorphic theorems instead lead to goals over an abstract assertion lattice; `grind`'s lattice reasoning discharges these as well. -:::example "Stateful Proofs" +:::example "Monad-Polymorphic Proofs" ```imports -show -import Std.Do +import Std.WP import Std.Tactic.Do ``` ```lean -show -open Std.Do +open Std.WP Lean.Order set_option mvcgen.warning false ``` The function {name}`bump` increments its state by the indicated amount and returns the resulting value. +The underlying monad {lean}`m` and its assertion types stay abstract. ```lean -variable [Monad m] [WPMonad m ps] +variable {m : Type → Type v} [Monad m] +variable {Pred EPred : Type} +variable [Assertion Pred] [Assertion EPred] +variable [WPMonad m Pred EPred] + def bump (n : Nat) : StateT Nat m Nat := do modifyThe Nat (· + n) getThe Nat ``` -This specification lemma for {name}`bump` is proved in an intentionally low-level manner to demonstrate the intermediate proof states: +The specification lemma for {name}`bump` quantifies over the abstract assertion lattice, and its verification conditions are entailments in that lattice. +The `finish` step discharges them: ```lean theorem bump_correct : - ⦃ fun n => ⌜n = k⌝ ⦄ - bump (m := m) i - ⦃ ⇓ r n => ⌜r = n ∧ n = k + i⌝ ⦄ := by - mintro n_eq_k - unfold bump - unfold modifyThe - mspec - mspec - mpure_intro - constructor - . trivial - . simp_all -``` - -The lemma can also be proved using only the simplifier: -```lean -theorem bump_correct' : ⦃ fun n => ⌜n = k⌝ ⦄ bump (m := m) i - ⦃ ⇓ r n => ⌜r = n ∧ n = k + i⌝ ⦄ := by - mintro _ - simp_all [bump] + ⦃ fun r n => ⌜r = n ∧ n = k + i⌝ ⦄ := by + vcgen [bump] with finish ``` ::: diff --git a/Tutorial.lean b/Tutorial.lean index 6f892783b..b76958b26 100644 --- a/Tutorial.lean +++ b/Tutorial.lean @@ -4,4 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ import Tutorial.VCGen +import Tutorial.MVCGen import Tutorial.Grind.IndexMap diff --git a/Tutorial/MVCGen.lean b/Tutorial/MVCGen.lean new file mode 100644 index 000000000..a8c88ff75 --- /dev/null +++ b/Tutorial/MVCGen.lean @@ -0,0 +1,1032 @@ +/- +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 VersoTutorial + +import Manual.Meta +import Manual.Papers + +import Std.Tactic.Do + +open Verso.Genre Manual +open Verso.Genre.Manual.InlineLean +open Verso.Code.External (lit) +open Verso.Genre.Tutorial + +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 + +#doc (Tutorial) "Verifying Imperative Programs Using `mvcgen`" => +%%% +tag := "mvcgen-tactic-tutorial" +slug := "mvcgen" +summary := inlines!"A demonstration of how to use Lean's verification condition generator to conveniently and compositionally prove properties of monadic programs." +exampleStyle := .inlineLean `MVCGenTutorial +%%% + +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: + +:::codeOnly +```imports +import Std.Data.HashMap +import Std.Data.HashSet +``` +::: +```imports +import Std.Tactic.Do +``` +:::codeOnly +```lean +set_option mvcgen.warning false +``` +::: +```lean +open Std.Do +``` + +# Preconditions and Postconditions + +One style in which program specifications can be written is to provide a {tech (key := "mvcgen precondition") (remote := "reference")}_precondition_ $`P`, which the caller of a program $`\mathit{prog}` is expected to ensure, and a {tech (key := "mvcgen postcondition") (remote := "reference")}_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_1` with $`P_1 \wedge P_2`. +The {tech (key := "mvcgen weakest precondition") (remote := "reference")}_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. + + +# 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" (remote := "reference")}[local mutable state] and a {keywordOf Lean.Parser.Term.doFor}`for` 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 (`Id` computations never throw exceptions) can be proved by showing that the {tech (key := "mvcgen weakest precondition") (remote := "reference")}[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 (key := "mvcgen verification conditions") (remote := "reference")}[verification conditions]. + +While {tactic}`mvcgen` is mostly automatic, it does require an invariant for the loop. +A {tech (key := "mvcgen loop invariant") (remote := "reference")}_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 + 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 +``` + +:::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 hint to the user of where that particular {tech (key := "mvcgen VC") (remote := "reference")}[VC] came from. +For example: + +* `vc1.step` conveys that this {tech (key := "mvcgen VC") (remote := "reference")}[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.success` is meant to prove that the postcondition of a specification (of {name}`forIn`) implies the desired property. +::: + +:::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 + apply Id.of_wp_run_eq h + mvcgen + case inv1 => exact ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝ + all_goals mleave; grind +``` +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 + apply Id.of_wp_run_eq h + mvcgen + invariants + · ⇓⟨xs, out⟩ => ⌜xs.prefix.sum = out⌝ + with grind +``` +The {multiCode}[{keyword}`mvcgen invariants `{lit}`...`{keyword}` with `{lit}`...`] is an abbreviation for the +tactic sequence {multiCode}[{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 +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 +``` +::: + +:::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 {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: + +* {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 + +:::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 +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 +``` +::: + +::::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 + mvcgen + invariants + · Invariant.withEarlyReturnNewDo + (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝) + (onContinue := fun xs seen => + ⌜(∀ x, x ∈ seen ↔ x ∈ xs.prefix) ∧ xs.prefix.Nodup⌝) + with grind +``` +:::: + + +:::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 (key := "mvcgen loop invariant") (remote := "reference")}[loop invariant]. +Since our loop has an {ref "early-return" (remote := "reference")}[early return], we construct the invariant using the helper function {lean}`Invariant.withEarlyReturnNewDo`, which supports the {ref "do-elab" (remote := "reference")}[extensible `do`-notation elaborator]. +This function allows us to specify the invariant in three parts: + +* {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. +* {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 +``` +::: + +:::paragraph +Note that the form `mvcgen invariants?` will suggest an initial invariant, so there is no need to memorize the exact syntax for specifying invariants: +```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.withEarlyReturnNewDo (onReturn := fun r letMuts => ⌜(r = true ↔ l.Nodup) ∧ l.Nodup⌝) (onContinue := + fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝) +``` +::: + +:::paragraph +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] +``` +::: + +:::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 {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 {tech (key := "E-matching") (remote := "reference")}[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 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 + +:::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 {multiCode}[{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. +::: + +:::leanFirst +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 +``` +::: + +::::leanFirst +:::leanSection +```lean -show +variable (n : Nat) +``` + +{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`: 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 + -- 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 +``` +:::: + +## Hoare Triples + +::::::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 {tech (key := "mvcgen Hoare triple") (remote := "reference")}_Hoare triple_ 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 {stmt1 stmt2 : m PUnit} {ps : PostShape.{0}} {P : Assertion ps} {Q : PostCond Unit ps} {P' : Assertion ps} {Q' : PostCond Unit ps} +``` + +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. +::: + +:::::paragraph +One suitable specification for {name}`mkFresh` as a Hoare triple is this translation of {name}`mkFreshN_correct`: +::::displayOnly +:::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. +::::: + +:::::paragraph +A specification for the single-step {name}`mkFresh` describes its effects on the monad's state: +::::displayOnly +:::leanSection +```lean -show +variable {n : Nat} +``` +```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 to 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. +::: +:::: +::::: + + +:::paragraph +Hoare triples are defined in terms of a logic of stateful predicates plus a {tech (key := "mvcgen weakest precondition") (remote := "reference")}[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 {tech (key := "mvcgen predicate transformer semantics") (remote := "reference")}_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, {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 {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⌝` +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.) + +:::::: + +## Composing Specifications + +Nested unfolding of definitions as in {multiCode}[{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 {tech (key := "mvcgen specification lemmas") (remote := "reference")}_specification lemmas_ for each monadic function. +A specification lemma is a Hoare triple that is automatically used during {tech (key := "mvcgen verification condition") (remote := "reference")}[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. + +::::leanSection + +:::codeOnly +```lean +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 +``` +```lean -show +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`)? + +:::displayOnly +```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⌝⦄ := … +``` +::: + +:::: + +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 {deftech (key := "mvcgen framing")}_framing_ hypotheses (cf. the {tactic}`mpure` and {tactic}`mframe` tactics). +Hypotheses in the Lean context are part of the immutable {deftech (key := "mvcgen frame")}_frame_ of the stateful logic, because in contrast to stateful hypotheses they survive the rule of consequence. + +# Monad Transformers and Lifting + +Real-world programs often use monads that are built from multiple {tech (remote := "reference")}[monad transformers], with operations being frequently {ref "lifting-monads" (remote := "reference")}[lifted] from one monad to another. +Verification of these programs requires taking this into account. +We can tweak the previous example to demonstrate this. + +:::codeOnly +```lean +namespace Transformers +``` +```lean -show +variable {m : Type → Type} {α : Type} {ps : PostShape.{0}} +attribute [-instance] Lake.instMonadLiftTOfMonadLift_lake +``` +::: + +::::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 : CounterM Nat := do + let n ← (·.counter) <$> get + modify fun s => { s with counter := s.counter + 1 } + pure n +``` + +{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 ← mkFresh + acc := acc.push n + return acc.toList +``` +::: +:::: + +::::paragraph +Then the {tactic}`mvcgen`-based proof goes through unchanged: +```lean +@[spec] +theorem mkFresh_spec (c : Nat) : + ⦃fun state => ⌜state.counter = c⌝⦄ + mkFresh + ⦃⇓ 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] + 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 {name}`MonadLift` instances. + +::: + +:::codeOnly +```lean +end Transformers +``` +::: + +# 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} +``` + +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. +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: + +: The {tech (key := "mvcgen total correctness interpretation") (remote := "reference")}_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. + +: The {tech (key := "mvcgen partial correctness interpretation") (remote := "reference")}_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, while {lean}`⇓? r => Q' r` has the partial interpretation. + +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. + +:::: + +:::codeOnly +```lean +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 + 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 grind } + pure n +``` + +The following correctness property expresses this: +```lean +@[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 +``` + +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⌝⦄ + 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 +``` +::: + +:::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 + | .error _ s' => s'.counter = s'.limit := by + generalize h : (mkFreshN n).run s = x + apply EStateM.of_wp_run_eq h + mvcgen +``` +::: + +:::codeOnly +```lean +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. +Hence the {name}`WP` instance for {lean}`EStateM ε σ` maps to the {name}`PostShape` {lean}`PostShape.except ε (.arg σ .pure)`, just +as for {lean}`ExceptT ε (StateM σ)`. +::: + + +# Extending `mvcgen` With Support for Custom Monads + +The {tactic}`mvcgen` framework is designed to be extensible. +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 (key := "mvcgen verification conditions") (remote := "reference")}[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. +::: + +:::::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: + +```lean +inductive Error where + | integerOverflow: Error + -- ... more error kinds ... + +inductive Result (α : Type u) where + | ok (v: α): Result α + | fail (e: Error): Result α + | div +``` +:::codeOnly +```lean +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 + apply LawfulMonad.mk' _ + all_goals (dsimp [Functor.map, bind, pure]; grind) +``` +::: +:::: +::::: + +:::paragraph +There are both {inst}`Monad Result` and {inst}`LawfulMonad Result` instances. +Supporting this monad in {tactic}`mvcgen` is a matter of: + +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. +::: + +:::::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` is similar to that of {lean}`Except Error`. +Each case of {name}`Result` is implemented by an existing predicate transformer: +* {name}`PredTrans.pure` for {lean}`Result.ok` +* {name}`PredTrans.throw` for {lean}`Result.fail` +* {lean}`PredTrans.const ⌜False⌝` for {lean}`Result.div`, meaning that all specifications assert that the program never diverges. +:::: +```lean +instance : WP Result (.except Error .pure) where + wp + | .ok v => PredTrans.pure v + | .fail e => PredTrans.throw e + | .div => PredTrans.const ⌜False⌝ +``` +::::: + +:::paragraph +The implementation of {name}`WP.wp` should distribute over the basic monad operators. +We prove this as separate theorems for {name}`pure` and {name}`bind`. +For {name}`bind`, both the definition of {name}`wp` and the definition of {name}`bind` need to be +unfolded to expose the nested {keyword}`match` structure that {tactic}`grind` makes short process of. +The {tactic}`simp` and {tactic}`grind` theory for predicate transformers triggers whenever a predicate transformer +is applied to a postcondition. +To bring the goals of {name}`WPMonad.wp_pure` and {name}`WPMonad.wp_bind` into this form, we use {tactic}`ext`. +```lean +theorem Result.apply_wp_pure {α} {a : α} {Q} : + wp⟦pure (f := Result) a⟧ Q = Q.1 a := by rfl + +theorem Result.apply_wp_bind {α β} {x} {f : α → Result β} {Q} : + wp⟦do let a ← x; f a⟧ Q = wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2) := by + simp only [wp, bind] + grind + +instance Result.instWPMonad : WPMonad Result (.except Error .pure) where + wp_pure _ := by ext Q : 1; apply Result.apply_wp_pure + wp_bind x f := by ext Q : 1; apply Result.apply_wp_bind +``` +::: + +::: paragraph +Finally, we also prove an adequacy lemma similar to {name}`Except.of_wp_eq` for {lean}`Result`. +```lean +theorem Result.of_wp_eq {α} {x prog : Result α} + (h : prog = x) (P : Result α → Prop) + (hspec : ⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, + fun e => ⌜P (.fail e)⌝⟩) : + P x := by + subst h + match prog with + | .ok a => simpa [wp] using hspec + | .fail e => simpa [wp] using hspec + | .div => simp [wp] at hspec +``` +::: + +:::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_eq`. +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 +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) +``` +::: + +:::paragraph +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) +``` +::: + +:::paragraph +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 {tech (key := "mvcgen verification conditions") (remote := "reference")}[verification conditions] that are straightforward to understand. +For example, when the monad is monomorphic and all loop invariants have been instantiated, an invocation of {multiCode}[{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 {multiCode}[{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 {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: + +```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) +``` + + +:::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 {ref "tactic-ref-spred" (remote := "reference")}[tactic reference] contains a list of all proof mode tactics. + +::: diff --git a/Tutorial/VCGen.lean b/Tutorial/VCGen.lean index 59cb0e399..97ddbd7ad 100644 --- a/Tutorial/VCGen.lean +++ b/Tutorial/VCGen.lean @@ -10,6 +10,7 @@ import VersoTutorial import Manual.Meta import Manual.Papers +import Std.WP import Std.Tactic.Do open Verso.Genre Manual @@ -28,16 +29,16 @@ set_option linter.typography.dashes true set_option mvcgen.warning false -#doc (Tutorial) "Verifying Imperative Programs Using `mvcgen`" => +#doc (Tutorial) "Verifying Imperative Programs Using `vcgen`" => %%% -tag := "mvcgen-tactic-tutorial" -slug := "mvcgen" +tag := "vcgen-tactic-tutorial" +slug := "vcgen" summary := inlines!"A demonstration of how to use Lean's verification condition generator to conveniently and compositionally prove properties of monadic programs." -exampleStyle := .inlineLean `MVCGenTutorial +exampleStyle := .inlineLean `VCGenTutorial %%% -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: +This section is a tutorial that introduces the most important concepts of {tactic}`vcgen` top-down. +Recall that you need to import {module}`Std.WP` and {module}`Std.Tactic.Do` and open the namespaces {namespace}`Std.WP` and {namespace}`Lean.Order` to run these examples: :::codeOnly ```imports @@ -46,15 +47,22 @@ import Std.Data.HashSet ``` ::: ```imports +import Std.WP import Std.Tactic.Do ``` :::codeOnly ```lean set_option mvcgen.warning false ``` +```lean +namespace VCGenTutorial +``` +```lean +section +``` ::: ```lean -open Std.Do +open Std.WP Lean.Order ``` # Preconditions and Postconditions @@ -73,7 +81,7 @@ 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" (remote := "reference")}[local mutable state] and a {keywordOf Lean.Parser.Term.doFor}`for` loop: +As a first example of {tactic}`vcgen`, the function {name}`mySum` computes the sum of an array using {ref "let-mut" (remote := "reference")}[local mutable state] and a {keywordOf Lean.Parser.Term.doFor}`for` loop: ```lean def mySum (l : Array Nat) : Nat := Id.run do @@ -86,80 +94,68 @@ 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`. +Thus, the proof first manipulates the goal into a form that is amenable to the use of {tactic}`vcgen`, using the lemma {name}`Id.of_run_eq_wp`. 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 (remote := "reference")}[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 (remote := "reference")}[verification conditions]. +Next, the proof uses {tactic}`vcgen` to replace the formulation in terms of weakest preconditions with a set of {tech (remote := "reference")}[verification conditions]. -While {tactic}`mvcgen` is mostly automatic, it does require an invariant for the loop. +While {tactic}`vcgen` is mostly automatic, it does require an invariant for the loop. A {tech (remote := "reference")}_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 - apply Id.of_wp_run_eq h + apply Id.of_run_eq_wp 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. + vcgen + -- Specify the invariant which should hold throughout the loop. + -- It is a function of three arguments: + -- * `pref` is the list of elements that the loop has already visited + -- * `suff` is the list of elements that the loop has yet to visit + -- * `out` is the current value of the `let mut` variable -- 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 + case inv1 => exact fun pref suff out => pref.sum = out -- Prove that the invariant is true at the start - case vc2 => + case vc1 => grind -- Prove that the invariant at the end of the loop implies the -- property we wanted - case vc3 h => + case vc2 => + grind + -- Prove that our invariant is preserved at each step of the loop + case vc3 => 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 hint to the user of where that particular {tech (remote := "reference")}[VC] came from. -For example: +The case labels `vc1`, `vc2`, … number the {tech (remote := "reference")}[VCs] in the order in which they arise during generation. +In this proof: -* `vc1.step` conveys that this {tech (remote := "reference")}[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.success` is meant to prove that the postcondition of a specification (of {name}`forIn`) implies the desired property. +* `vc1` proves that the invariant holds when the loop starts. +* `vc2` proves that the invariant after the final iteration implies the desired property. +* `vc3` proves that each iteration of the loop body preserves the invariant. ::: :::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). +After specifying the loop invariant, the proof can be shortened to just {keyword}`all_goals grind`. ```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 + apply Id.of_run_eq_wp h + vcgen + case inv1 => exact fun pref suff out => pref.sum = out + all_goals grind ``` -This pattern is so common that {tactic}`mvcgen` comes with special syntax for it: +This pattern is so common that {tactic}`vcgen` 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 {multiCode}[{keyword}`mvcgen invariants `{lit}`...`{keyword}` with `{lit}`...`] is an abbreviation for the -tactic sequence {multiCode}[{keyword}`mvcgen; case`{lit}` inv1 => ...`{keyword}`; all_goals mleave; grind`] -above. It is the form that we will be using from now on. + apply Id.of_run_eq_wp h + vcgen invariants + · fun pref suff out => pref.sum = out + with finish +``` +The {multiCode}[{keyword}`vcgen invariants `{lit}`...`{keyword}` with `{lit}`...`] form supplies the invariants and then runs the given `grind` step on every remaining VC; the `finish` step closes each VC with `grind`'s full automation. It is the form that we will be using from now on. ::: :::paragraph @@ -179,7 +175,7 @@ theorem mySum_correct_vanilla (l : Array Nat) : mySum l = l.sum := by ::: :::paragraph -This proof is similarly succinct as the proof in {name}`mySum_correct_shorter` that uses {tactic}`mvcgen`. +This proof is similarly succinct as the proof in {name}`mySum_correct_shorter` that uses {tactic}`vcgen`. However, the traditional approach relies on important properties of the program: * 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`. @@ -188,13 +184,13 @@ However, the traditional approach relies on important properties of the program: 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. +In the following sections, we will go through several examples to learn about {tactic}`vcgen` and its support library, and also see where traditional proofs become difficult. This is usually caused by: * {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. +{tactic}`vcgen` scales to these challenges with reasonable effort. ::: @@ -220,18 +216,18 @@ def nodup (l : List Int) : Bool := Id.run do 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`: +Thus, the proof begins by using {name}`Id.of_run_eq_wp` to make the proof state amenable to {tactic}`vcgen`: ```lean 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 + apply Id.of_run_eq_wp h + vcgen invariants · Invariant.withEarlyReturnNewDo - (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝) - (onContinue := fun xs seen => - ⌜(∀ x, x ∈ seen ↔ x ∈ xs.prefix) ∧ xs.prefix.Nodup⌝) - with grind + (onReturn := fun ret seen => ret = false ∧ ¬l.Nodup) + (onContinue := fun pref suff seen => + (∀ x, x ∈ seen ↔ x ∈ pref) ∧ pref.Nodup) + all_goals simp_all + all_goals grind ``` :::: @@ -239,50 +235,27 @@ theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by :::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 +variable {l : List Int} {ret : Bool} {seen : Std.HashSet Int} {pref suff : List Int} +axiom onReturn : Bool → Std.HashSet Int → Prop +axiom onContinue : List Int → List Int → Std.HashSet Int → Prop ``` -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`. +The proof again offloads all verification conditions to {tactic}`grind` and its existing automation around {name}`List.Nodup`; the additional {tactic}`simp_all` step first unfolds the applied invariant combinator in each VC. Therefore, the only difference is in the {tech (remote := "reference")}[loop invariant]. Since our loop has an {ref "early-return" (remote := "reference")}[early return], we construct the invariant using the helper function {lean}`Invariant.withEarlyReturnNewDo`, which supports the {ref "do-elab" (remote := "reference")}[extensible `do`-notation elaborator]. -This function allows us to specify the invariant in three parts: +This function allows us to specify the invariant in two parts: * {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. -* {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`. +* {lean}`onContinue pref suff seen` is the regular induction step that proves the invariant is preserved each loop iteration. + As in {name}`mySum`, the list {lean}`pref` holds the elements that the loop has already visited and {lean}`suff` holds the elements that the loop has yet to visit. 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 ``` ::: :::paragraph -Note that the form `mvcgen invariants?` will suggest an initial invariant, so there is no need to memorize the exact syntax for specifying invariants: -```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.withEarlyReturnNewDo (onReturn := fun r letMuts => ⌜(r = true ↔ l.Nodup) ∧ l.Nodup⌝) (onContinue := - fun xs letMuts => ⌜xs.prefix = [] ∧ letMuts = ∅ ∨ xs.suffix = [] ∧ l.Nodup⌝) -``` -::: - -:::paragraph -Now consider the following direct (and excessively golfed) proof without {tactic}`mvcgen`: +Now consider the following direct (and excessively golfed) proof without {tactic}`vcgen`: ```lean theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by @@ -298,7 +271,7 @@ theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by :::paragraph Some observations: -* The proof is even shorter than the one with {tactic}`mvcgen`. +* The proof is even shorter than the one with {tactic}`vcgen`. * 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 {tech (key := "E-matching") (remote := "reference")}[E-matchable]. @@ -307,9 +280,9 @@ Some observations: 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. +The {tactic}`vcgen` 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. +Furthermore, a {tactic}`vcgen`-powered proof will never need to copy any part of the original program. # Compositional Reasoning About Effectful Programs Using Hoare Triples @@ -354,27 +327,26 @@ variable (n : Nat) {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`: 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. +In this proof, {name}`StateM.of_run'_eq_wp` serves the same role that {name}`Id.of_run_eq_wp` did in the preceding examples. ::: ```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 + apply StateM.of_run'_eq_wp 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 + -- The `mkFreshN` and `mkFresh` arguments to `vcgen` add to an + -- internal `simp` set and makes `vcgen` unfold these definitions. + vcgen [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 + · fun pref suff acc state => + (∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup + with finish ``` :::: @@ -383,16 +355,16 @@ theorem mkFreshN_correct (n : Nat) : ((mkFreshN n).run' s).Nodup := by ::::::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} +variable {m : Type u → Type v} [Monad m] {α σ ε : Type u} {Pred : Type u} {EPred : Type u} [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {P : Pred} {Q : α → Pred} {epost : EPred} {prog : m α} {c : Nat} ``` A {tech (remote := "reference")}_Hoare triple_ 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.] +{lean}`P` and {lean}`Q` are written in an assertion language that is determined by the specific monad {lean}`m`.{margin}[In particular, the 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 {stmt1 stmt2 : m PUnit} {ps : PostShape.{0}} {P : Assertion ps} {Q : PostCond Unit ps} {P' : Assertion ps} {Q' : PostCond Unit ps} +variable {stmt1 stmt2 : m PUnit} {P : Pred} {Q : PUnit → Pred} {P' : Pred} {Q' : PUnit → Pred} ``` Specifications as Hoare triples are compositional because they allow statements to be sequenced. @@ -401,23 +373,20 @@ Just as proofs about ordinary functions can rely on lemmas about the functions t ::: :::::paragraph -One suitable specification for {name}`mkFresh` as a Hoare triple is this translation of {name}`mkFreshN_correct`: +One suitable specification for {name}`mkFreshN` as a Hoare triple is this translation of {name}`mkFreshN_correct`: ::::displayOnly :::leanSection ```lean -show variable {n : Nat} ``` ```leanTerm -⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ +⦃fun _ => True⦄ mkFreshN n ⦃fun 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. +For {name}`StateM` programs, an assertion is a predicate on the state, and a postcondition additionally takes the result value as its first argument. +The precondition {lean}`fun (_ : Supply) => True` imposes no requirements on the state in which the program is called. +The postcondition states that the result value is a list with no duplicate elements, regardless of the final state. ::::: :::::paragraph @@ -429,9 +398,9 @@ variable {n : Nat} ``` ```leanTerm ∀ (c : Nat), -⦃fun state => ⌜state.counter = c⌝⦄ +⦃fun state => state.counter = c⦄ mkFresh -⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ +⦃fun 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 to the initial state. @@ -448,15 +417,23 @@ This is good, because specifications may _abstract over_ uninteresting implement :::paragraph -Hoare triples are defined in terms of a logic of stateful predicates plus a {tech (remote := "reference")}[weakest precondition] semantics {lean}`wp⟦prog⟧` that translates monadic programs into this logic. +Hoare triples are defined in terms of a {tech (remote := "reference")}[weakest precondition] semantics {lean}`wp prog Q epost` that translates monadic programs into assertions. 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 {tech (key := "predicate transformer semantics") (remote := "reference")}_predicate transformers_. -The Hoare triple syntax is notation for {name}`Std.Do.Triple`: +The Hoare triple syntax is notation for {name}`Std.WP.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 +section +variable {Prog : Type u} {Value : Type v} {Pred : Type} {EPred : Type} [Assertion Pred] [Assertion EPred] +``` +```lean +-- This is the definition of Std.WP.Triple: +structure Triple (x : Prog) [WP Prog Value Pred EPred] + (pre : Pred) (post : Value → Pred) (epost : EPred) : Prop where + intro :: + le_wp : pre ⊑ wp x post epost +``` +```lean -show +end ``` ::: @@ -464,81 +441,73 @@ def Triple [WP m ps] {α : Type u} (prog : m α) 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, {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`: +The {name}`WP` type class interprets a program type `Prog` with result values of type `Value` as a predicate transformer over an assertion type `Pred` and an exception assertion type `EPred`. +Many of the standard monads and monad transformers such as {name}`StateT`, {name}`ReaderT` and {name}`ExceptT` come with a canonical {name}`WP` instance. +For example, {lean}`StateT σ` comes with a {name}`WP` instance that adds a {lean}`σ` argument to every assertion. +The entailment `⊑` in the definition is the order of the assertion lattice; for {name}`StateM` it is pointwise implication. +For {name}`StateM` programs, the following type is equivalent to {name}`Std.WP.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 +def StateMTriple {α σ : Type} (prog : StateM σ α) + (P : σ → Prop) (Q : α → σ → Prop) : Prop := + ∀ s, P s → (fun (a, s') => Q a s') (prog.run s) ``` ```lean -show -example : @StateMTriple α σ = Std.Do.Triple (m := StateM σ) := rfl +example {α σ : Type} (prog : StateM σ α) (P : σ → Prop) (Q : α → σ → Prop) : + Std.WP.Triple prog P Q ⊥ ↔ StateMTriple prog P Q := + ⟨fun h => h.le_wp, fun h => ⟨h⟩⟩ ``` ::: - -```lean -show -variable {p : Prop} -``` - -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 binder notation `⦃ P ⦄ prog ⦃ r, Q ⦄` is available for postconditions; it binds the result value `r` in `Q`. +An explicit exception postcondition can be supplied after a semicolon, as in `⦃ P ⦄ prog ⦃ Q; E ⦄`. +When the exception postcondition is omitted, it defaults to the bottom assertion `⊥`, which asserts that the program throws no exception. 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.) :::::: ## Composing Specifications -Nested unfolding of definitions as in {multiCode}[{tactic}`mvcgen`{lit}` [`{name}`mkFreshN`{lit}`, `{name}`mkFresh`{lit}`]`] is quite blunt but effective for small programs. +Nested unfolding of definitions as in {multiCode}[{tactic}`vcgen`{lit}` [`{name}`mkFreshN`{lit}`, `{name}`mkFresh`{lit}`]`] is quite blunt but effective for small programs. A more compositional way is to develop individual {tech (remote := "reference")}_specification lemmas_ for each monadic function. A specification lemma is a Hoare triple that is automatically used during {tech (remote := "reference")}[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: +Specification lemmas can either be passed as arguments to {tactic}`vcgen` 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⌝⦄ + ⦃fun state => state.counter = c⦄ mkFresh - ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by + ⦃fun r state => r = c ∧ c < state.counter⦄ := by -- Unfold `mkFresh` and blast away: - mvcgen [mkFresh] with grind + vcgen [mkFresh] with finish @[spec] theorem mkFreshN_spec (n : Nat) : - ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by - -- `mvcgen [mkFreshN, mkFresh_spec]` if `mkFresh_spec` were not + ⦃fun _ => True⦄ mkFreshN n ⦃fun r _ => r.Nodup⦄ := by + -- `vcgen [mkFreshN, mkFresh_spec]` if `mkFresh_spec` were not -- registered with `@[spec]` - mvcgen [mkFreshN] - invariants + vcgen [mkFreshN] invariants -- As before: - · ⇓⟨xs, acc⟩ state => - ⌜(∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup⌝ - with grind + · fun pref suff acc state => + (∀ x ∈ acc, x < state.counter) ∧ acc.toList.Nodup + with finish ``` ::: :::paragraph -The original correctness theorem can now be proved using {tactic}`mvcgen` alone: +The original correctness theorem can now be proved using {tactic}`vcgen` 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 + apply StateM.of_run'_eq_wp h + vcgen ``` -The specification lemma {name}`mkFreshN_spec` is automatically used by {tactic}`mvcgen`. +The specification lemma {name}`mkFreshN_spec` is automatically used by {tactic}`vcgen`. ::: @@ -551,7 +520,9 @@ This subsection is a bit of a digression and can be skipped on first reading. :::codeOnly ```lean axiom M : Type → Type -variable {x y : UInt8} [Monad M] [WP M .pure] +variable {x y : UInt8} {Pred EPred : Type} +variable [Assertion Pred] [Assertion EPred] +variable [Monad M] [WPMonad M Pred EPred] def addQ (x y : UInt8) : M UInt8 := pure (x + y) local infix:1023 " +? " => addQ ``` @@ -563,18 +534,19 @@ 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`. +The corner brackets `⌜p⌝` embed a proposition `p` into the assertion language as a _pure_ assertion, an assertion that holds independently of the monadic state. 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`)? :::displayOnly ```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⌝⦄ := … + ⦃⌜True⌝⦄ x +? y ⦃fun 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⌝⦄ := … + ⦃fun r => ⌜r.toNat = x.toNat + y.toNat⌝⦄ := … ``` ::: @@ -582,7 +554,7 @@ theorem add_spec_pre (x y : UInt8) : 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 {deftech}_framing_ hypotheses (cf. the {tactic}`mpure` and {tactic}`mframe` tactics). +This is referred to as {deftech}_framing_ hypotheses. 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 Transformers and Lifting @@ -596,7 +568,7 @@ We can tweak the previous example to demonstrate this. namespace Transformers ``` ```lean -show -variable {m : Type → Type} {α : Type} {ps : PostShape.{0}} +variable {m : Type → Type} {α : Type} attribute [-instance] Lake.instMonadLiftTOfMonadLift_lake ``` ::: @@ -632,33 +604,32 @@ def mkFreshN (n : Nat) : AppM (List Nat) := do :::: ::::paragraph -Then the {tactic}`mvcgen`-based proof goes through unchanged: +Then the {tactic}`vcgen`-based proof goes through unchanged: ```lean @[spec] theorem mkFresh_spec (c : Nat) : ⦃fun state => ⌜state.counter = c⌝⦄ mkFresh - ⦃⇓ r state => ⌜r = c ∧ c < state.counter⌝⦄ := by - mvcgen [mkFresh] with grind + ⦃fun r state => ⌜r = c ∧ c < state.counter⌝⦄ := by + vcgen [mkFresh] with finish @[spec] theorem mkFreshN_spec (n : Nat) : - ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by - -- `liftCounterM` here ensures unfolding - mvcgen [mkFreshN] - invariants - · ⇓⟨xs, acc⟩ _ state => + ⦃⌜True⌝⦄ mkFreshN n ⦃fun r => ⌜r.Nodup⌝⦄ := by + vcgen [mkFreshN] invariants + · fun pref suff acc _ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝ - with grind + with finish ``` +The corner brackets absorb the assertion arguments that a specification does not mention: the precondition of {name}`mkFresh_spec` names the {name}`Supply` state, and `⌜state.counter = c⌝` covers the reader environment beneath it. :::: :::leanSection ```lean -show universe u v -variable {m : Type u → Type v} {ps : PostShape.{u}} [WP m ps] {α : Type u} {prog : m α} +variable {m : Type u → Type v} [Monad m] {Pred EPred : Type u} [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {prog : m α} ``` -The {name}`WPMonad` type class asserts that {lean}`wp⟦prog⟧` distributes over the {name}`Monad` operations (“monad morphism”). +The {name}`WPMonad` type class asserts that {name}`wp` 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 {name}`MonadLift` instances. @@ -675,33 +646,32 @@ end Transformers ::::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} +variable {m : Type u → Type v} [Monad m] {Pred EPred : Type u} [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {P : Pred} {α : Type u} {prog : m α} {Q' : α → Pred} ``` 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`. +We have seen how {tactic}`vcgen` 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'`! +Exceptions are the reason why a triple carries an exception postcondition next to the success postcondition. +To see why, suppose there were only the success postcondition, and suppose that program {lean}`prog` throws an exception in a prestate satisfying {lean}`P`. +Should we be able to prove {lean}`⦃P⦄ prog ⦃Q'⦄`? +There is no result value, 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: : The {tech (remote := "reference")}_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. + {lean}`⦃P⦄ prog ⦃Q'⦄` asserts that, given {lean}`P` holds, then {lean}`prog` terminates normally _and_ {lean}`Q'` holds for the result. : The {tech (remote := "reference")}_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. + {lean}`⦃P⦄ prog ⦃Q'; ⊤⦄` asserts that, given {lean}`P` holds, and _if_ {lean}`prog` terminates normally _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. +A triple without an explicit exception postcondition carries the bottom assertion {lean}`(⊥ : EPred)` and thus has the total interpretation: an exception would have to establish `⊥`, so no exception can be thrown. +The top assertion {lean}`(⊤ : EPred)` permits every exception and yields the partial interpretation. -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. +In the running example, {lean}`⦃P⦄ prog ⦃Q'⦄` is unprovable, but {lean}`⦃P⦄ prog ⦃Q'; ⊤⦄` is trivially provable. +Between {lean}`(⊥ : EPred)` and {lean}`(⊤ : EPred)`, the exception postcondition expresses a _spectrum_ of correctness properties. :::: @@ -735,15 +705,15 @@ The following correctness property expresses this: ```lean @[spec] theorem mkFresh_spec (c : Nat) : - ⦃fun state => ⌜state.counter = c⌝⦄ + ⦃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 + ⦃fun r state => r = c ∧ c < state.counter; + fun _ state => c = state.counter ∧ c = state.limit⦄ := by + vcgen [mkFresh] with finish ``` -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. +In this property, the triple has two postconditions, separated by a semicolon: the first covers successful termination, and the second applies when an exception is thrown. +The monad's {name}`WP` instance determines the types of both postconditions: the exception postcondition takes the thrown exception in place of the result value, and each state gives an extra parameter. :::leanFirst In this new monad, {name}`mkFreshN`'s implementation is unchanged, except for the type signature: @@ -757,33 +727,31 @@ def mkFreshN (n : Nat) : EStateM String Supply (List Nat) := do ::: :::paragraph -However, the specification lemma must account for both successful termination and exceptions being thrown, in both the postcondition and the loop invariant: +However, the specification lemma must account for both successful termination and exceptions being thrown; the loop invariant itself stays as before: ```lean @[spec] theorem mkFreshN_spec (n : Nat) : - ⦃⌜True⌝⦄ + ⦃fun _ => 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 + ⦃fun r _ => r.Nodup; + fun _msg state => state.counter = state.limit⦄ := by + vcgen [mkFreshN] invariants + · fun pref suff acc state => + (∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup + with finish ``` ::: :::paragraph -The final proof uses the specification lemmas and {tactic}`mvcgen`, just as before: +The final proof uses the specification lemmas and {tactic}`vcgen`, just as before: ```lean 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 + apply EStateM.of_run_eq_wp h + vcgen with finish ``` ::: @@ -796,37 +764,34 @@ 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} +variable {m : Type u → Type v} [Monad m] {Pred EPred : Type} [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type} {σ ε : Type} ``` -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. -Hence the {name}`WP` instance for {lean}`EStateM ε σ` maps to the {name}`PostShape` {lean}`PostShape.except ε (.arg σ .pure)`, just -as for {lean}`ExceptT ε (StateM σ)`. +A {lean}`StateT σ` layer turns the assertion type `Pred` into `σ → Pred` and leaves the exception postcondition type unchanged. +An {lean}`ExceptT ε` layer leaves the assertion type unchanged and turns the exception postcondition type `EPred` into {lean}`(ε → Pred) × EPred`, adding one exception branch of type `ε → Pred`. +The {name}`WP` instance for {lean}`EStateM ε σ` uses assertions of type `σ → Prop` and exception postconditions of type `ε → σ → Prop`, mirroring the single exception branch of the equivalent transformer stack {lean}`ExceptT ε (StateM σ)`. ::: -# Extending `mvcgen` With Support for Custom Monads +# Extending `vcgen` With Support for Custom Monads -The {tactic}`mvcgen` framework is designed to be extensible. -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 (remote := "reference")}[verification conditions]. +The {tactic}`vcgen` framework is designed to be extensible. +None of the monads presented so far have in any way been hard-coded into {tactic}`vcgen`. +Rather, {tactic}`vcgen` relies on instances of the {name}`WP` and {name}`WPMonad` type class and user-provided specifications to generate {tech (remote := "reference")}[verification conditions]. :::leanSection ```lean -show -variable {m : Type u → Type v} [Monad m] {ps : PostShape.{u}} +universe u v +variable {m : Type u → Type v} [Monad m] {Pred EPred : Type} [Assertion Pred] [Assertion EPred] {α : Type u} ``` -The {name}`WP` instance defines the weakest precondition interpretation of a monad {lean}`m` into a predicate transformer {lean}`PredTrans ps`, +The {name}`WP` instance defines the weakest precondition interpretation of a monad {lean}`m` into predicate transformers {lean}`PredTrans Pred EPred α`, and the matching {name}`WPMonad` instance asserts that this translation distributes over the {name}`Monad` operations. ::: :::::paragraph ::::leanFirst -Suppose one wants to use `mvcgen` to generate verification conditions for programs generated by [`Aeneas`](https://github.com/AeneasVerif/aeneas). +Suppose one wants to use `vcgen` 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 @@ -858,9 +823,9 @@ instance Result.instLawfulMonad : LawfulMonad Result := by :::paragraph There are both {inst}`Monad Result` and {inst}`LawfulMonad Result` instances. -Supporting this monad in {tactic}`mvcgen` is a matter of: +Supporting this monad in {tactic}`vcgen` is a matter of: -1. Adding {name}`WP` and {name}`WPMonad` instances for {name}`Result` +1. Adding a {name}`WPMonad` instance for {name}`Result` 2. Registering specification lemmas for the translation of basic Rust primitives such as addition etc. ::: @@ -869,74 +834,56 @@ Supporting this monad in {tactic}`mvcgen` is a matter of: ```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` is similar to that of {lean}`Except Error`. -Each case of {name}`Result` is implemented by an existing predicate transformer: -* {name}`PredTrans.pure` for {lean}`Result.ok` -* {name}`PredTrans.throw` for {lean}`Result.fail` -* {lean}`PredTrans.const ⌜False⌝` for {lean}`Result.div`, meaning that all specifications assert that the program never diverges. +variable {α : Type u} {v : α} {e : Error} +``` +The {name}`WPMonad` instance for {name}`Result` picks the assertion type {lean}`Prop` because there are no state-like effects, and the exception postcondition type {lean}`Error → Prop` because there is a single exception of type {lean}`Error`. +Its {name}`WP` interpretation translates a program in {lean}`Result α` to a predicate transformer in {lean}`PredTrans Prop (Error → Prop) α`. +That is, a function mapping a postcondition and an exception postcondition to the weakest precondition. +Each case of {name}`Result` determines the precondition directly: +* {lean}`Result.ok v` yields the success postcondition at {lean}`v`. +* {lean}`Result.fail e` yields the exception postcondition at {lean}`e`. +* {name}`Result.div` yields {lean}`False`, meaning that all specifications assert that the program never diverges. + +The remaining fields prove that the interpretation is monotone and that it distributes over {name}`pure` and {name}`bind`. +The law {name}`WPMonad.pure_le_wp_pure` holds by reflexivity, because the interpretation of {lean}`Result.ok v` is exactly the success postcondition at {lean}`v`. +For {name}`WPMonad.bind_le_wp_bind`, a case split on the program exposes the {keyword}`match` structure in the definition of {name}`bind`, and {tactic}`simp` closes each case. :::: ```lean -instance : WP Result (.except Error .pure) where - wp - | .ok v => PredTrans.pure v - | .fail e => PredTrans.throw e - | .div => PredTrans.const ⌜False⌝ +instance Result.instWPMonad : + WPMonad Result Prop (Error → Prop) where + toWP α := { + wpTrans x := ⟨fun post epost => + match x with + | .ok v => post v + | .fail e => epost e + | .div => False⟩ + wp_trans_monotone x := by + intro post post' epost epost' hepost hpost + cases x <;> simp_all [PartialOrder.rel] + } + pure_le_wp_pure x post epost := PartialOrder.rel_refl + bind_le_wp_bind x f post epost := by + cases x <;> simp [wp, WP.wpTrans, bind, PartialOrder.rel] ``` ::::: -:::paragraph -The implementation of {name}`WP.wp` should distribute over the basic monad operators. -We prove this as separate theorems for {name}`pure` and {name}`bind`. -For {name}`bind`, both the definition of {name}`wp` and the definition of {name}`bind` need to be -unfolded to expose the nested {keyword}`match` structure that {tactic}`grind` makes short process of. -The {tactic}`simp` and {tactic}`grind` theory for predicate transformers triggers whenever a predicate transformer -is applied to a postcondition. -To bring the goals of {name}`WPMonad.wp_pure` and {name}`WPMonad.wp_bind` into this form, we use {tactic}`ext`. -```lean -theorem Result.apply_wp_pure {α} {a : α} {Q} : - wp⟦pure (f := Result) a⟧ Q = Q.1 a := by rfl - -theorem Result.apply_wp_bind {α β} {x} {f : α → Result β} {Q} : - wp⟦do let a ← x; f a⟧ Q = wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2) := by - simp only [wp, bind] - grind - -instance Result.instWPMonad : WPMonad Result (.except Error .pure) where - wp_pure _ := by ext Q : 1; apply Result.apply_wp_pure - wp_bind x f := by ext Q : 1; apply Result.apply_wp_bind -``` -::: - ::: paragraph -Finally, we also prove an adequacy lemma similar to {name}`Except.of_wp_eq` for {lean}`Result`. +Finally, we also prove an adequacy lemma similar to {name}`Except.of_eq_wp` for {lean}`Result`. ```lean -theorem Result.of_wp_eq {α} {x prog : Result α} +theorem Result.of_eq_wp {α} {x prog : Result α} (h : prog = x) (P : Result α → Prop) - (hspec : ⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, - fun e => ⌜P (.fail e)⌝⟩) : + (hwp : wp prog (fun a => P (.ok a)) (fun e => P (.fail e))) : P x := by subst h match prog with - | .ok a => simpa [wp] using hspec - | .fail e => simpa [wp] using hspec - | .div => simp [wp] at hspec + | .ok a => simpa [wp, WP.wpTrans] using hwp + | .fail e => simpa [wp, WP.wpTrans] using hwp + | .div => simp [wp, WP.wpTrans] at hwp ``` ::: -:::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_eq`. +The definition of the {name}`WP` interpretation determines what properties can be derived from proved specifications via {name}`Result.of_eq_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: @@ -962,15 +909,18 @@ 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 +theorem Result.throw_spec {α} {post : α → Prop} + {epost : Error → Prop} (e : Error) : + ⦃epost e⦄ throw (m := Result) (α := α) e ⦃post; epost⦄ := + ⟨PartialOrder.rel_refl⟩ @[spec] theorem addOp_ok_spec {x y} (h : x.toNat + y.toNat < UInt32.size) : - ⦃⌜True⌝⦄ + ⦃True⦄ addOp x y - ⦃⇓ r => ⌜r = x + y ∧ (x + y).toNat = x.toNat + y.toNat⌝⦄ := by - mvcgen [addOp] with (simp_all; try grind) + ⦃fun r => r = x + y ∧ (x + y).toNat = x.toNat + y.toNat⦄ := by + vcgen [addOp] + all_goals simp_all; try grind ``` ::: @@ -979,54 +929,35 @@ This is already enough to prove the following example: ```lean example : - ⦃⌜True⌝⦄ - do let mut x ← addOp 1 3 - for _ in [:4] do + ⦃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) + return x : Result UInt32) + ⦃fun r => r.toNat = 24⦄ := by + vcgen invariants + · fun pref suff x => x.toNat = 4 + 5 * pref.length + all_goals simp_all + all_goals grind ``` ::: -# Proof Mode for Stateful Goals +# Discharging Verification Conditions -```lean -show -variable {σs : List (Type u)} {H T : SPred σs} -``` - -It is a priority of {tactic}`mvcgen` to break down monadic programs into {tech (remote := "reference")}[verification conditions] that are straightforward to understand. -For example, when the monad is monomorphic and all loop invariants have been instantiated, an invocation of {multiCode}[{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 {multiCode}[{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 {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: +It is a priority of {tactic}`vcgen` to break down monadic programs into {tech (remote := "reference")}[verification conditions] that are straightforward to understand. +The VCs are ordinary Lean goals, so any tactic can discharge them. +When the assertion language is concrete, as for {name}`Id` or {name}`StateM` programs, the goals speak directly about result values and states, and {tactic}`grind` applies. +When an applied invariant combinator such as {name}`Invariant.withEarlyReturnNewDo` reaches a VC, {tactic}`simp_all` unfolds it into its per-case propositions first. -```lean -keep -abbrev PostShape.args : PostShape.{u} → List (Type u) - | .pure => [] - | .arg σ s => σ :: PostShape.args s - | .except _ s => PostShape.args s +During VC generation, {tactic}`vcgen` internalizes the goal context into `grind`'s E-graph. +The `with` clause runs a single `grind`-mode step on every remaining VC inside that shared context, which avoids re-internalizing the context for every VC. +The step `finish` closes a VC with `grind`'s full automation. -abbrev Assertion (ps : PostShape.{u}) : Type u := - SPred (PostShape.args ps) +:::codeOnly +```lean +end ``` - - -:::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} +```lean +end VCGenTutorial ``` - -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 {ref "tactic-ref-spred" (remote := "reference")}[tactic reference] contains a list of all proof mode tactics. - ::: diff --git a/TutorialMain.lean b/TutorialMain.lean index 9a5984ab8..0f98cec83 100644 --- a/TutorialMain.lean +++ b/TutorialMain.lean @@ -45,7 +45,7 @@ def tutorials : Tutorials where { title := #[inlines!"Tactics"], titleString := "Tactics" description := #[blocks!"These tutorials demonstrate Lean's advanced proof automation."] - tutorials := #[%doc Tutorial.VCGen, %doc Tutorial.Grind.IndexMap] + tutorials := #[%doc Tutorial.VCGen, %doc Tutorial.MVCGen, %doc Tutorial.Grind.IndexMap] } ] diff --git a/lean-toolchain b/lean-toolchain index 7cd7ead2e..77781bc2a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-08-19 +leanprover/lean4:nightly-2026-08-21