feat: footprint-based frame inference for vcgen via @[frameproc] - #14529
Merged
Conversation
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
sgraf812
force-pushed
the
sg/vcgen-seplogic-listrev
branch
26 times, most recently
from
July 30, 2026 09:54
3218f69 to
4f1875f
Compare
This PR generalizes `vcgen` frame inference beyond the lattice meet: a `@[frameproc]` returns a `FrameSplit` naming the framed resource and a proof of the split VC, so separation-logic `∗` framing works with `vcgen … with finish`. The sep-logic test gains an in-place reverse of a doubly-linked list that frames an unrelated cell across the whole program. `vcgen` applies a single frame rule, `WP.Frames.op_wp_upperAdjoint_le_wp`, with the framed resource `F` schematic and the weakest footprint `W = wp x (fun a => upperAdjoint (op F) (Q a)) E` baked in, so its premises are just the frame condition `WP.Frames op x F` and the split VC `pre ⊑ (op F W) s⃗`. A `@[frameproc]` takes a `FrameInferenceInfo` (the `wp` metadata plus the frame operator, the goal entailment, and the pre/spec/residual preconditions) and returns a `FrameSplit`, building its proof against a solver-owned placeholder for `W` that the solver fills by reading `W` off the applied rule. The meet default and the `DyLean` demo defer the split VC to the built-in meet decomposition; the separation-logic procedure proves it by AC-rearrangement of `∗`; the cost demo emits the `costConj`-reduced meet form. All frameproc term-building goes through the `SymM` builders. `solve` gains an `instantiateGoal?` step that canonicalizes the entailment's carrier and sides after rule application, and precondition normalization gains steps that lift a `⌜φ⌝ ⊓ P` guard (via `ofProp_meet_le`) and eliminate an `iSup` precondition (via `iSup_le`).
sgraf812
force-pushed
the
sg/vcgen-seplogic-listrev
branch
from
July 30, 2026 10:53
4f1875f to
ced713a
Compare
sgraf812
marked this pull request as ready for review
July 30, 2026 11:17
sgraf812
added a commit
that referenced
this pull request
Jul 30, 2026
This PR restores `vcgen` spec application performance regressed by #14529, up to +39% wall-clock on the `vcgen` benchmark suite. Frame inference inputs are computed only when a frame inference procedure consumes them, so applying a spec with no frame to infer costs what it did before frame inference. The spec precondition now comes from `FrameInferenceInfo.specPre?`, a speculative, rolled-back application of the spec's cached backward rule that runs only when a procedure calls it; the solver previously ran the speculation for every spec application with a non-conjunctive precondition and then applied the spec a second time. The frame operator is likewise built only when a procedure constructs a split: `mkSplitVC` and `FrameSplit.withDeferredSplitVC` take it as an argument, and `defaultFrameInferenceProc` (renamed from `meetFrameInferenceProc`; it is agnostic of the operator) takes an operator builder invoked only for a pinned `frames` clause. `FrameInferenceInfo` drops `op`, `le` and `pre` (the latter two become accessors of the new `goal` field), gains the spec's backward rule `specRule`, and replaces `FrameInferenceHint` with `providedFrame? : Option Expr`; `FrameProc.resourceTy` is renamed to `mkResourceTy`. On `PurePrecond(2400)` instruction counts return from 12.1G to 11.2G against a pre-#14529 baseline of 11.05G.
yermakoffivan
pushed a commit
to yermakoffivan/lean4
that referenced
this pull request
Jul 30, 2026
This PR restores `vcgen` spec application performance regressed by leanprover#14529. Frame inference inputs are computed only when a frame inference procedure consumes them, so applying a spec with no frame to infer costs what it did before frame inference.
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
2 participants
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 reworks how a
@[frameproc]procedure discharges its split verification condition so that frame inference scales to operators whose residual the built-in lattice split cannot decompose. A procedure for separating conjunction∗used to leave behind a∗that no split rule could discharge, haltingvcgen; a procedure may now discharge its split VC however it wants, so separation-logic framing closes withvcgen … with finish.A procedure builds its split VC
pre ⊑ (op frame residualPre) s⃗against a solver-owned metavariableresidualPrethat the solver fills with the weakest footprint once the frame rule applies, and returns aFrameSplitthat either carries its own proof of that VC or defers it as a subgoal for the built-in lattice decomposition.