doc: port mvcgen documentation to vcgen and Std.WP - #927
Draft
sgraf812 wants to merge 17 commits into
Draft
Conversation
Manual/VCGen.lean and Tutorial/VCGen.lean move to MVCGen.lean. Identical copies stay at the VCGen.lean paths for the vcgen port. Both variants are registered in the manual and tutorial include lists. The build stays red until the next commit renames the duplicated tags.
The copies keep verbatim mvcgen content. These changes make both sites build next to the originals: * Verso tags get a vcgen- prefix: vcgen-tactic, vcgen-tactic-tutorial, vcgen-adequacy, vcgen-proof-mode. * The chapter title becomes "The `vcgen` tactic" and the tutorial title becomes "Verifying Imperative Programs Using `vcgen`". Identical titles produced colliding auto-generated section tags. * The tutorial slug becomes "vcgen". * Hidden code blocks wrap the tutorial code in namespace VCGenTutorial. Both tutorials define the same top-level names otherwise. * Every deftech key gets a "vcgen " prefix, so tech references resolve to the single mvcgen definition. Verified with ./generate-html.sh.
The header imports Std.WP next to Std.Tactic.Do and opens Std.WP. A hidden section scopes the open to the ported region. A hidden end restores open Std.Do before the Control Flow section, so the later sections keep elaborating against mvcgen unchanged. The mySum proofs use vcgen. The invariant becomes a plain function of the visited prefix, the pending suffix, and the mutable state. The entry lemma is Id.of_run_eq_wp. The case labels are inv1 and vc1 (entry), vc2 (exit implies goal), vc3 (inductive step). The short form is vcgen invariants ... with finish. The proof-mode step mleave disappears from this region. The example project module becomes VCGenTutorial. Verified with ./generate-html.sh on nightly-2026-08-19.
The nodup proof supplies the early-return invariant through Invariant.withEarlyReturnNewDo. Its onContinue part takes the visited prefix and the pending suffix directly, and there is no onExcept part. The proof reduces the applied invariant combinator with simp_all and then discharges every VC with grind. The scoped open moves forward so the section elaborates under Std.WP. The invariants? paragraph is gone. On this toolchain the suggestion engine answers "There were no suggestions for missing invariants" for this example. Verified with ./generate-html.sh on nightly-2026-08-19.
The mkFreshN proofs use vcgen with a plain-function invariant over prefix, suffix, accumulator, and state. The entry lemma is StateM.of_run'_eq_wp. The compositional proof closes with bare vcgen. The Hoare triple subsection presents Std.WP.Triple: a triple relates a program of any type with a WP instance to a precondition, a postcondition on the result value, and an exception postcondition. The StateM example shows the unfolding to pointwise implication, and a hidden example verifies the equivalence against Std.WP.Triple. The postcondition binder notation and the exception postcondition after a semicolon replace the PostCond and continuation notation. The frame note states the specs with corner brackets over an abstract assertion lattice and introduces the brackets there. Verified with ./generate-html.sh on nightly-2026-08-19.
The CounterM and AppM specs keep their shape. The corner brackets absorb the assertion arguments beneath the named state, so the precondition of mkFresh_spec still reads state.counter = c while the reader environment stays implicit. The loop invariant takes prefix, suffix, accumulator, the Bool state, and the Supply state, and covers the reader environment with corner brackets. The WPMonad paragraph speaks about wp distributing over the Monad operations. Verified with ./generate-html.sh on nightly-2026-08-19.
A triple carries the exception postcondition after a semicolon. The bottom assertion gives the total correctness interpretation, the top assertion the partial one, and values between them span the spectrum that PostCond used to express. The EStateM specs state both postconditions as plain functions, and the loop invariant carries no exception branch. The entry lemma is EStateM.of_run_eq_wp, and the final proof discharges its VCs with finish. The closing paragraph states the transformer action on the assertion types: StateT prepends a state argument to Pred, ExceptT adds an exception branch to EPred, and EStateM mirrors ExceptT over StateM. Verified with ./generate-html.sh on nightly-2026-08-19.
The Result monad gets one WPMonad instance. Its toWP field maps each constructor to a precondition: ok v to the success postcondition at v, fail e to the exception postcondition at e, and div to False. The remaining fields prove monotonicity and the pure and bind laws, which are inequalities in Std.WP. The separate WP instance, the apply lemmas, and the equational laws of the mvcgen version disappear. The adequacy lemma becomes Result.of_eq_wp, mirroring Except.of_eq_wp. The throw spec constrains the head of a schematic exception postcondition. The addOp spec and the closing loop example discharge their VCs with simp_all and grind. Verified with ./generate-html.sh on nightly-2026-08-19.
The SPred proof mode has no counterpart in Std.WP, so the closing section becomes "Discharging Verification Conditions". It states that VCs are ordinary Lean goals, that simp_all unfolds applied invariant combinators, and that the with clause runs one grind-mode step per VC inside the E-graph context that vcgen internalized during generation. The tutorial now targets vcgen and Std.WP in every section, and the scoped opens collapse into one region for the whole file. Verified with ./generate-html.sh on nightly-2026-08-19.
The chapter now documents the Std.WP framework end to end. * The Stateful Predicates section becomes Assertion Lattices: the Assertion class, the lattice vocabulary, the corner-bracket embedding, and NondetFun for reading state values. * The Assertions section becomes Exception Postconditions: EPost.Nil, EPost.Cons, the EPost type and value notations, and the total and partial correctness interpretations via bot and top. * The Predicate Transformers section documents Lean.Order.PredTrans, its monad, the push helpers, WP, wp, WPConjunctive, and WPMonad. The Identity example defines the interpretation inside WPMonad.toWP. A section-local WP-only instance demonstrates the "No spec applicable" error that a missing WPMonad instance causes. * The adequacy list names the of_run_eq_wp and of_eq_wp lemmas. * The Hoare triple section documents Std.WP.Triple with the semicolon and binder notations. The spec lemma and invariant sections use plain-function assertions and the Std.WP Invariant combinators. * The VC generation steps mention E-graph internalization and the until and with clauses. The LogM example builds its interpretation with pushArg inside WPMonad.toWP. * The Proof Mode section becomes Discharging Verification Conditions, with a monad-polymorphic proof over an abstract assertion lattice closed by vcgen with finish. Verified with ./generate-html.sh on nightly-2026-08-19.
The Verification Condition Generation section lists vcgen next to mvcgen. Verified with ./generate-html.sh on nightly-2026-08-19.
The example follows the pattern of the interpretations in Std.WP: an instance_reducible definition Identity.wpInst carries the WP interpretation, the WP-only section installs it as a local instance, and the WPMonad instance passes it as its toWP field. Verified with ./generate-html.sh on nightly-2026-08-19.
The vcgen chapter intro drops "monadic" from the tactic description and links the Lean.Order note to the partial_fixpoint theory section. Verified with ./generate-html.sh on nightly-2026-08-19.
The vcgen chapter and tutorial define and reference their technical terms under the plain keys. The mvcgen chapter and tutorial carry an "mvcgen " prefix on their deftech keys, and their tech references name those keys explicitly, so each document pair links within itself. Verified with ./generate-html.sh on nightly-2026-08-19.
The recorded Lake transcripts gain the new lint option --checks and the package configuration field checks, which this nightly adds. The commit becomes redundant once nightly-testing bumps to this nightly.
The tuple refactor (leanprover/lean4#14836) replaces the bespoke exception postcondition types. EPost.Nil becomes EStack⟨⟩, EPost.Nil.mk becomes (), and the Result monad carries a bare Error → Prop exception postcondition, so epost e replaces epost.head e and the head-projection step leaves the monotonicity proof. The push helpers for transformers are PredTrans.pushExceptT and PredTrans.pushOptionT. The EStack⟨…⟩ and estack⟨…⟩ notations get a syntax block in the exception postcondition section. Verified with ./generate-html.sh on nightly-2026-08-21.
sgraf812
force-pushed
the
vcgen-docs-nightly
branch
from
August 21, 2026 14:43
1fe451a to
1f725b7
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR ports the mvcgen documentation (reference manual chapter and tutorial) to
vcgenand theStd.WPframework. The mvcgen documents stay in place asMVCGen.leantwins, so both doc sets build side by side.The initial port was done by Claude. So far, I have completely reviewed
Manual/VCGen.leanand left a few TODOs.Here's how the port started:
git mvthe mvcgen files toMVCGen.lean, restore byte-identical copies at theVCGen.leanpaths, register both.deftechkey prefixes. Content stays verbatim mvcgen.I took over after in 9c41e3e. Since then, I have worked exclusively on
Manual/VCGen.lean. I think it is in good shape. I haven't looked atTutorial/VCGen.lean.I have not touched the MVCGen.lean files after the AI did steps 1+2 and then subsequently switched around the convention for deftech abbreviations in dacfec5. I'm fairly confident that the AI did the right thing in those steps. What remains is a deprecation notice at the top of those files, pointing to the VCGen content.
I advanced the toolchain to 2026-08-21 from 19 which includes a workaround for a breakage introduced by lake, so that I anticipate most of the changes that landed since then (quite a few). Still, some PRs are still about to land that didn't make it into that nightly. No PR after and including lean4#14870 made it into that nightly. This list might might help with bisecting: https://github.com/leanprover/lean4/pulls?q=is%3Apr+is%3Amerged+author%3Asgraf812