feat: port the mvcgen' tactic to the new Std.Internal.Do meta theory by sgraf812 · Pull Request #14015 · leanprover/lean4

sgraf812 · 2026-06-11T16:11:35Z

This PR ports the experimental mvcgen' tactic to the new Std.Internal.Do meta theory, where verification-condition generation works on lattice entailments pre ⊑ wp x post epost. Two changes are visible at the proof surface: mvcgen' now eagerly introduces all state components as local hypotheses, so more facts reach grind; and loop invariants no longer have to restate the exceptional postcondition.

Previously the invariant for a loop that can throw had to repeat the exception condition alongside the actual invariant:

theorem throwing_loop_spec :
    ⦃fun s => ⌜s = 4⌝⦄
    throwing_loop
    ⦃post⟨fun _ _ => ⌜False⌝,
          fun e s => ⌜e = 42 ∧ s = 4⌝⟩⦄ := by
  mvcgen' [throwing_loop]
  case inv1 => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝,
                         fun e s => ⌜e = 42 ∧ s = 4⌝⟩

Now the exceptional postcondition is taken from the surrounding Triple, so the invariant case carries only the invariant:

theorem throwing_loop_spec :
    ⦃fun s => s = 4⦄
    throwing_loop
    ⦃fun _ _ => False;
     fun e s => e = 42 ∧ s = 4⦄ := by
  mvcgen' [throwing_loop]
  case inv1 => exact ⟨fun (xs, r) s => r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⟩

The spec lemmas in Std.Internal.Do.Triple.SpecLemmas are registered with @[spec] and populate the new spec database, which also gains the whileM/Lean.Loop specifications, Invariant.withEarlyReturnNewDo, and pointwise entailment lemmas for state introduction.

The port replays Vladimir Gladshtein's #13978 onto master's file structure.

The solver diverges from the legacy algorithm in three points. Reflexivity runs on every entailment before the pure-precondition lifts, closing the leaf VCs where a spec precondition meets an identical goal precondition (Q x ⊑ wp (pure x) Q E ends in Q x ⊑ Q x) and instantiating spec parameters that occur only in rule premises. Reflexivity no longer assigns synthetic opaque metavariables, so function-typed invariant holes are not silently solved away. Pure preconditions are lifted into the local context as soon as they arise; the lifted hypothesis is cached in Scope.lastLiftedPre?, and a targeted assumption step closes the handoff VCs of subsequent spec applications against it.

This is the second of two steps that land vova/new-mvcgen onto master. The first step (#13954) updated the @[spec] builtin attribute and regenerated stage0, so this PR reuses master's stage0 and contains no generated C changes. Invariant suggestion (invariants?) yields no suggestions on the new surface; porting the suggestion analysis is deferred until mvcgen' replaces the legacy mvcgen.

mathlib-lean-pr-testing · 2026-06-11T16:47:58Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2686a6cc077b5b3c46180d84bb106d4d835b7aa0 --onto d2f48db30713019241520218d0965227bbb64eed. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-11 16:47:58)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6271d8f21262dee2f13e23853bf76893295d2b36 --onto 659e8bb858995b0a1ada239c5b3819c8f8f2772f. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-12 16:05:05)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 659e8bb858995b0a1ada239c5b3819c8f8f2772f. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-15 14:07:56)

leanprover-bot · 2026-06-11T16:48:00Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2686a6cc077b5b3c46180d84bb106d4d835b7aa0 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-11 16:47:59)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6271d8f21262dee2f13e23853bf76893295d2b36 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-12 16:05:06)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ab122a187d64224faf53004c9631f664b852bb96 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-15 14:07:58)

sgraf812 · 2026-06-12T17:49:20Z

!bench

leanprover-radar · 2026-06-12T17:49:26Z

Benchmark results for 79370a9 against 6271d8f are in. There are significant results. @sgraf812

🟥 build//instructions: +5.0G (+0.04%)

Large changes (35✅, 3🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (8✅)

✅ mvcgen/sym/AddSubCancelDeep/400/vcgen//wall-clock: -38ms (-13.57%)
✅ mvcgen/sym/AddSubCancelSimp/100/kernel//wall-clock: -7ms (-31.82%)
✅ mvcgen/sym/AddSubCancelSimp/250/kernel//wall-clock: -16ms (-32.00%)
✅ mvcgen/sym/GetThrowSet/100/kernel//wall-clock: -9ms (-29.03%)
✅ mvcgen/sym/GetThrowSetGrind/100/kernel//wall-clock: -25ms (-18.12%)
✅ mvcgen/sym/GetThrowSetGrind/150/kernel//wall-clock: -33ms (-11.26%)
✅ mvcgen/sym/GetThrowSetGrind/50/kernel//wall-clock: -9ms (-17.31%)
✅ mvcgen/sym/MatchIota/50/kernel//wall-clock: -6ms (-37.50%)

Small changes (4✅, 14🟥)

✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Context//instructions: -93.8M (-3.59%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Driver//instructions: +580.4M (+11.38%) (reduced significance based on *//lines)
✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Entails//instructions: -5.2G (-64.88%) (reduced significance based on *//lines)
✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Frontend//instructions: -52.0M (-0.55%)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache//instructions: +669.7M (+42.50%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.RuleConstruction//instructions: +5.8G (+71.86%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Solve//instructions: +319.3M (+1.59%)
✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB//instructions: -1.1G (-27.44%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Util//instructions: +174.4M (+3.74%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen//instructions: +38.1M (+5.47%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal//instructions: +36.8M (+5.29%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Tactic.Do.VCGen//instructions: +187.9M (+0.71%)
🟥 build/module/Lean.Elab.Tactic.Do//instructions: +36.7M (+5.24%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Tactic//instructions: +9.2M (+1.00%)
🟥 build/module/Lean.Elab//instructions: +7.6M (+0.79%)
🟥 build/module/Std.Internal.Do.Order.Basic//instructions: +48.6M (+2.15%) (reduced significance based on *//lines)
🟥 build/module/Std.Internal.Do.Triple.SpecLemmas//instructions: +1.4G (+8.18%) (reduced significance based on *//lines)
🟥 elab/charactersIn//instructions: +67.7M (+0.19%)

sgraf812 · 2026-06-12T18:59:07Z

!bench

leanprover-radar · 2026-06-12T18:59:21Z

Benchmark results for e3eb965 against 6271d8f are in. There are significant results. @sgraf812

🟥 build//instructions: +4.9G (+0.04%)

Large changes (35✅, 3🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (7✅)

✅ mvcgen/sym/AddSubCancelSimp/100/kernel//wall-clock: -7ms (-31.82%)
✅ mvcgen/sym/AddSubCancelSimp/250/kernel//wall-clock: -16ms (-32.00%)
✅ mvcgen/sym/GetThrowSet/100/kernel//wall-clock: -9ms (-29.03%)
✅ mvcgen/sym/GetThrowSetGrind/100/kernel//wall-clock: -26ms (-18.84%)
✅ mvcgen/sym/GetThrowSetGrind/150/kernel//wall-clock: -36ms (-12.29%)
✅ mvcgen/sym/GetThrowSetGrind/50/kernel//wall-clock: -9ms (-17.31%)
✅ mvcgen/sym/MatchIota/50/kernel//wall-clock: -6ms (-37.50%)

Small changes (5✅, 16🟥)

Too many entries to display here. View the full report on radar instead.

Accumulates the mvcgen' tactic port and its test suite. The Std.Internal.Do specification cleanup it builds on has landed upstream (#14051), so after rebasing this carries only the tactic and test changes. Co-authored-by: volodeyka <vovaglad00@gmail.com>

…dling Replace the `LogicOp` classify-then-dispatch enum with a `LatticeSplit` record bundling each connective's rebuild function, distribution lemma, and split lemma, so the `match_expr` arm produces the rule data directly instead of re-dispatching across four tables. Drop the `preIsTop` rule specialization. Rather than baking `⊤` into a connective rule and selecting a `⊤`-specialized split lemma, `himp` always splits via `himp_complete`, and the residual `P ⊓ ⊤` precondition is cancelled by a new `meet_top_le_of_le` normalization step in `normalizePre?`. This removes `himp_complete_top` and shrinks the lattice-rule cache key. Also remove the dead `topStateArgIntro` rule and apply a `?`-suffix naming sweep to the `solve` strategies. Add a `⇨` regression test exercising the split and the `⊓ ⊤` cancellation. Co-authored-by: volodeyka <vovaglad00@gmail.com>

…Top` flag Replace the `match_expr` head dispatch in `splitLatticeOp?` (formerly `solveLatticeConnective?`) with a `latticeSplits : HashMap Name LatticeSplit` lookup keyed on the RHS head constant, so adding a connective is one map entry plus a `LatticeSplit` value. The per-connective argument slicing folds into a `numOperands` field, and the carrier-type argument is chosen from the existing `needApplyArgs` flag. Drop the `preIsTop` soundness check on `⌜p⌝`. The `ofProp` split now uses `top_le_ofProp` (LHS fixed to `⊤`), so its rule only unifies against a `⊤` precondition and falls through otherwise, making the gate a property of the lemma rather than an external probe. Credit Vladimir Gladshtein on the remaining ported tactic files (`Context`, `Frontend`, `RuleCache`). Co-authored-by: volodeyka <vovaglad00@gmail.com>

mvcgen' looped on programs containing a raw `monadLift`/`liftM`: `liftM.eq_1 : @liftM = @monadLift` registered as a productive simp spec and rewrote `monadLift …` to itself forever, since `liftM` is a reducible `abbrev` for `monadLift`. The no-op guard in `mkSpecTheoremFromSimpDecl?` only fired for value-level equations (`etaArgs == 0`) and compared the eta-expanded key against the un-expanded RHS, missing this function-level case. Compare the pre-eta key (`pattern.pattern`, already reducibly preprocessed) structurally against the RHS, dropping the `etaArgs` gate. A structural `==` skips only syntactic no-ops, so productive unfolds whose RHS is merely definitionally equal (`monadLift_trans`, ordinary `foo.eq_1`) stay registered. Add a `RawMonadLiftRegression` test pinning that a raw lift now terminates. Co-authored-by: volodeyka <vovaglad00@gmail.com>

The rule-construction functions in `RuleConstruction.lean` carried no `VCGenM` state and only needed plain metaprogramming, so move them from `SymM` to `MetaM`. The matcher re-shares subgoal types, so the `Sym.inferType` hash-consing was redundant; replace it with `Meta.inferType` and drop the `shareCommon` calls and the `Sym` infrastructure imports. Co-authored-by: volodeyka <vovaglad00@gmail.com>

Replace the local `predLevel` helper with `decLevel` when building the `bot_apply` rewrite in exception-postcondition reduction, and clarify the lifted-hypothesis discharge docstring. Co-authored-by: volodeyka <vovaglad00@gmail.com>

The function does one job: it adds the simp-side `@[spec]` equational lemmas to the triple spec database. The old name was a fossil from when the database was live-converted from a legacy representation. Co-authored-by: volodeyka <vovaglad00@gmail.com>

Collapse the separate `noEntailment`, `noProgramOrLatticeFoundInTarget`, and `noStrategyForProgram` constructors into a single `stop` carrying a `StopReason`, since every one of them is handled identically by emitting the current goal as a VC. The genuinely unreachable program case now throws. Co-authored-by: volodeyka <vovaglad00@gmail.com>

sgraf812 · 2026-06-16T08:32:38Z

!bench

leanprover-radar · 2026-06-16T08:32:44Z

Benchmark results for af52cf1 against ab122a1 are in. There are significant results. @sgraf812

🟥 build//instructions: +172.0M (+0.00%)

Large changes (36✅, 3🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (5✅)

✅ mvcgen/sym/AddSubCancelSimp/250/kernel//wall-clock: -17ms (-33.33%)
✅ mvcgen/sym/GetThrowSet/100/kernel//wall-clock: -9ms (-29.03%)
✅ mvcgen/sym/GetThrowSetGrind/100/kernel//wall-clock: -27ms (-19.42%)
✅ mvcgen/sym/GetThrowSetGrind/150/kernel//wall-clock: -36ms (-12.16%)
✅ mvcgen/sym/MatchIota/50/kernel//wall-clock: -6ms (-37.50%)

Small changes (7✅, 13🟥)

✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Context//instructions: -99.3M (-3.80%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Driver//instructions: -359.8M (-7.06%) (reduced significance based on absolute threshold)
✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Entails//instructions: -5.2G (-65.06%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.RuleCache//instructions: +633.4M (+40.22%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.RuleConstruction//instructions: +772.9M (+9.57%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Solve//instructions: +2.3G (+11.65%) (reduced significance based on *//lines)
✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB//instructions: -1.2G (-27.77%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Util//instructions: +226.7M (+4.86%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen//instructions: +37.0M (+5.30%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Do.Internal//instructions: +38.0M (+5.47%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Tactic.Do.VCGen//instructions: +175.6M (+0.67%)
🟥 build/module/Lean.Elab.Tactic.Do//instructions: +36.1M (+5.15%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Tactic//instructions: +9.2M (+1.00%)
🟥 build/module/Lean.Elab//instructions: +8.9M (+0.92%)
✅ build/module/Std.Internal.Do.Order.Frame//instructions: -14.3M (-1.54%)
🟥 compiled/incr_header_save//maxrss: +3MiB (+0.14%)
🟥 elab/charactersIn//instructions: +74.2M (+0.20%)
✅ mvcgen/sym/AddSubCancelDeep/400/vcgen//wall-clock: -29ms (-10.36%)
🟥 mvcgen/sym/AddSubCancelDeep/700/vcgen//wall-clock: +41ms (+9.86%)
✅ mvcgen/sym/AddSubCancelSimp/100/kernel//wall-clock: -6ms (-30.00%)

sgraf812 requested a review from TwoFX as a code owner June 11, 2026 16:11

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 11, 2026

sgraf812 force-pushed the sg/mvcgen-new-meta-theory branch 3 times, most recently from a63dc24 to 850515c Compare June 12, 2026 16:06

sgraf812 added the changelog-tactics User facing tactics label Jun 12, 2026

sgraf812 force-pushed the sg/mvcgen-new-meta-theory branch from e3eb965 to a0ed08f Compare June 15, 2026 13:33

sgraf812 and others added 7 commits June 15, 2026 15:04

sgraf812 enabled auto-merge June 16, 2026 08:55

sgraf812 added this pull request to the merge queue Jun 16, 2026

Merged via the queue into master with commit 99683cc Jun 16, 2026
23 checks passed

sgraf812 deleted the sg/mvcgen-new-meta-theory branch June 16, 2026 09:34

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat: port the mvcgen' tactic to the new Std.Internal.Do meta theory#14015

feat: port the mvcgen' tactic to the new Std.Internal.Do meta theory#14015
sgraf812 merged 8 commits into
masterfrom
sg/mvcgen-new-meta-theory

sgraf812 commented Jun 11, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing Bot commented Jun 11, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Jun 11, 2026 •

edited

Loading

Uh oh!

sgraf812 commented Jun 12, 2026

Uh oh!

leanprover-radar commented Jun 12, 2026 •

edited

Loading

Uh oh!

sgraf812 commented Jun 12, 2026

Uh oh!

leanprover-radar commented Jun 12, 2026 •

edited

Loading

Uh oh!

sgraf812 commented Jun 16, 2026

Uh oh!

leanprover-radar commented Jun 16, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

sgraf812 commented Jun 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing Bot commented Jun 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Jun 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgraf812 commented Jun 12, 2026

Uh oh!

leanprover-radar commented Jun 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgraf812 commented Jun 12, 2026

Uh oh!

leanprover-radar commented Jun 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sgraf812 commented Jun 16, 2026

Uh oh!

leanprover-radar commented Jun 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

sgraf812 commented Jun 11, 2026 •

edited

Loading

mathlib-lean-pr-testing Bot commented Jun 11, 2026 •

edited

Loading

leanprover-bot commented Jun 11, 2026 •

edited

Loading

leanprover-radar commented Jun 12, 2026 •

edited

Loading

leanprover-radar commented Jun 12, 2026 •

edited

Loading

leanprover-radar commented Jun 16, 2026 •

edited

Loading