Skip to content

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

Open
sgraf812 wants to merge 5 commits into
masterfrom
sg/mvcgen-new-meta-theory
Open

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

Conversation

@sgraf812

@sgraf812 sgraf812 commented Jun 11, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR ports the experimental mvcgen' tactic to the new Std.Internal.Do meta theory. VC generation now works on lattice entailments pre ⊑ wp x post epost instead of the legacy Std.Do SPred triples. The spec lemmas in Std.Internal.Do.Triple.SpecLemmas are registered with @[spec] and populate the new spec database. The spec library 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 main pieces:

  • Spec database: consumes the pattern-keyed SpecTheorems that @[spec] stores at annotation time, plus the equational lemmas from mvcgen_simp. Instantiation normalises Triple and ⊑ wp conclusions with tripleToWpProof?.
  • Rule construction: generalises a spec's concrete pre, post and epost into rule parameters. Each generalisation emits a pointwise VC, via wp_consequence_le, wp_econs_le and the componentwise EPost.Cons decomposition.
  • Lattice goals: ⊓, ⇨, ⌜·⌝ and ⊤ on the RHS decompose through cached logic rules built from their _apply lemmas.

The solver diverges from the legacy algorithm in three points:

  • Reflexivity runs on every entailment, before the pure-precondition lifts. Most attempts fail, and fail fast thanks to maximal sharing. The point is the leaf VCs where a spec's precondition meets an identical goal precondition: Q x ⊑ wp (pure x) Q E ends in Q x ⊑ Q x. Closing these by rfl removes the need for an assumption search. The rfl step also instantiates spec parameters that occur only in rule premises.
  • Reflexivity no longer assigns synthetic opaque metavariables. Invariant holes are function-typed, and the unifier would otherwise solve ⊤ ⊑ ?inv args by assigning ?inv, silently dropping the invariant goal.
  • Pure preconditions are lifted into the local context as soon as they arise, replacing the legacy framing of postcondition VCs. The lifted hypothesis is cached in Scope.lastLiftedPre?, and a targeted assumption step closes the handoff VCs of subsequent spec applications against it: one defeq check against one hypothesis, not an assumption search. Loop invariants need not restate pure facts, and spec chains close under plain mvcgen' at their previous cost.

Invariant suggestion (invariants?) yields no suggestions on the new surface; porting the suggestion analysis is deferred until mvcgen' replaces the legacy mvcgen.

@sgraf812 sgraf812 requested a review from TwoFX as a code owner June 11, 2026 16:11
@github-actions 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
@mathlib-lean-pr-testing

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

Copy link
Copy Markdown

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

leanprover-bot commented Jun 11, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

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 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 sgraf812 added the changelog-tactics User facing tactics label Jun 12, 2026
@sgraf812

sgraf812 commented Jun 12, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Jun 12, 2026 •
edited
Loading

Copy link
Copy Markdown

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

sgraf812 commented Jun 12, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Jun 12, 2026 •
edited
Loading

Copy link
Copy Markdown

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.

@sgraf812 @volodeyka
chore: mvcgen' port onto the new Std.Internal.Do meta theory
a0ed08f 
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>
@sgraf812 sgraf812 force-pushed the sg/mvcgen-new-meta-theory branch from e3eb965 to a0ed08f Compare June 15, 2026 13:33
sgraf812 and others added 4 commits June 15, 2026 15:04
@sgraf812 @volodeyka
refactor: simplify mvcgen' lattice decomposition and precondition han…
8cf5f30 
…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>
@sgraf812 @volodeyka
refactor: dispatch lattice splits through a table and drop the `preIs…
b20a2a5 
…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>
@sgraf812 @volodeyka
fix: skip no-op simp specs in mvcgen'
aab0220 
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>
@sgraf812 @volodeyka
refactor: run BackwardRule construction in MetaM
0668ee9 
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

Assignees

No one assigned

Labels

changelog-tactics User facing tactics toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@sgraf812 @leanprover-bot @leanprover-radar