Skip to content

perf: compute vcgen frame inference inputs on demand - #14605

Merged
sgraf812 merged 12 commits into
masterfrom
sg/vcgen-frameproc-lazy
Jul 30, 2026
Merged

perf: compute vcgen frame inference inputs on demand#14605
sgraf812 merged 12 commits into
masterfrom
sg/vcgen-frameproc-lazy

Conversation

@sgraf812

@sgraf812 sgraf812 commented Jul 30, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR restores vcgen spec application performance regressed by #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.

@sgraf812 sgraf812 added the changelog-no Do not include this PR in the release changelog label Jul 30, 2026
@sgraf812

sgraf812 commented Jul 30, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Jul 30, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for c41f492 against 103ef69 are in. There are significant results. @sgraf812

  • ✅ build//instructions: -2.5G (-0.02%)
  • 🟥 other exited with code -1

Small changes (1✅, 1🟥)

  • 🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.FrameProc//instructions: +447.0M (+34.01%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Solve//instructions: -1.2G (-5.12%) (reduced significance based on *//lines)

@sgraf812
perf: compute vcgen frame inference inputs on demand
7419dd9 
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.
@sgraf812
sgraf812 force-pushed the sg/vcgen-frameproc-lazy branch from c41f492 to 7419dd9 Compare July 30, 2026 13:56
@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 Jul 30, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jul 30, 2026

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 103ef690cc308618eb98476944213297cc5599a7 --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 14:31:36)

@leanprover-bot

leanprover-bot commented Jul 30, 2026

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 103ef690cc308618eb98476944213297cc5599a7 --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-30 14:31:37)

@sgraf812

sgraf812 commented Jul 30, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Jul 30, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 7419dd9 against 103ef69 are in. There are significant results. @sgraf812

  • ✅ build//instructions: -2.1G (-0.02%)

New metrics (12✅, 6🟥)

  • ✅ compiled/http_server//chunked_echo: -82ms (-1.58%)
  • 🟥 compiled/http_server//cycles: +616.4M (+0.42%)
  • 🟥 compiled/http_server//get_keepalive: +52ms (+1.97%)
  • 🟥 compiled/http_server//instructions: +621.0M (+0.36%)
  • 🟥 compiled/http_server//many_headers: +53ms (+1.93%)
  • ✅ compiled/http_server//maxrss: -4MiB (-5.25%)
  • ✅ compiled/http_server//post_echo: -14ms (-0.39%)
  • 🟥 compiled/http_server//task-clock: +177ms (+0.45%)
  • 🟥 compiled/http_server//wall-clock: +12ms (+0.09%)
  • ✅ compiled/http_server_tcp//chunked_echo: -136ms (-2.86%)
  • ✅ compiled/http_server_tcp//cycles: -2.7G (-1.89%)
  • ✅ compiled/http_server_tcp//get_keepalive: -49ms (-2.49%)
  • ✅ compiled/http_server_tcp//instructions: -654.0M (-0.46%)
  • ✅ compiled/http_server_tcp//many_headers: -60ms (-2.81%)
  • ✅ compiled/http_server_tcp//maxrss: -24MiB (-17.37%)
  • ✅ compiled/http_server_tcp//post_echo: -15ms (-0.49%)
  • ✅ compiled/http_server_tcp//task-clock: -541ms (-1.61%)
  • ✅ compiled/http_server_tcp//wall-clock: -263ms (-2.20%)

Large changes (2✅)

  • ✅ vcgen/PurePrecond/2400/vcgen//wall-clock: -62ms (-21.99%)
  • ✅ vcgen/PurePrecond/4400/vcgen//wall-clock: -118ms (-20.52%)

Medium changes (3✅)

  • ✅ elab/bv_decide_inequality//instructions: -353.6M (-0.31%)
  • ✅ vcgen/AddSubCancelSimp/700/vcgen//wall-clock: -161ms (-13.53%)
  • ✅ vcgen/PurePrecond/400/vcgen//wall-clock: -8ms (-18.18%)

Small changes (2✅, 1🟥)

  • 🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.FrameProc//instructions: +455.6M (+34.66%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Solve//instructions: -1.2G (-5.05%) (reduced significance based on *//lines)
  • ✅ vcgen/AddSubCancelSimp/400/vcgen//wall-clock: -59ms (-9.46%)

@sgraf812
sgraf812 marked this pull request as ready for review July 30, 2026 16:03
@sgraf812

sgraf812 commented Jul 30, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Jul 30, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for f6990f7 against 103ef69 are in. There are significant results. @sgraf812

  • ✅ build//instructions: -1.3G (-0.01%)

New metrics (9✅, 9🟥)

  • 🟥 compiled/http_server//chunked_echo: +3s (+71.18%)
  • 🟥 compiled/http_server//cycles: +100.9G (+68.83%)
  • 🟥 compiled/http_server//get_keepalive: +1s (+69.92%)
  • 🟥 compiled/http_server//instructions: +13.6G (+7.90%)
  • 🟥 compiled/http_server//many_headers: +2s (+74.12%)
  • 🟥 compiled/http_server//maxrss: +16MiB (+20.99%)
  • 🟥 compiled/http_server//post_echo: +2s (+73.94%)
  • 🟥 compiled/http_server//task-clock: +20s (+51.92%)
  • 🟥 compiled/http_server//wall-clock: +10s (+72.20%)
  • ✅ compiled/http_server_tcp//chunked_echo: -118ms (-2.48%)
  • ✅ compiled/http_server_tcp//cycles: -2.4G (-1.69%)
  • ✅ compiled/http_server_tcp//get_keepalive: -5ms (-0.25%)
  • ✅ compiled/http_server_tcp//instructions: -645.3M (-0.46%)
  • ✅ compiled/http_server_tcp//many_headers: -39ms (-1.83%)
  • ✅ compiled/http_server_tcp//maxrss: -9MiB (-6.20%)
  • ✅ compiled/http_server_tcp//post_echo: -43ms (-1.41%)
  • ✅ compiled/http_server_tcp//task-clock: -489ms (-1.45%)
  • ✅ compiled/http_server_tcp//wall-clock: -207ms (-1.73%)

Large changes (4✅)

  • ✅ vcgen/AddSubCancelSimp/700/vcgen//wall-clock: -178ms (-14.96%)
  • ✅ vcgen/PurePrecond/2400/vcgen//wall-clock: -70ms (-24.82%)
  • ✅ vcgen/PurePrecond/400/vcgen//wall-clock: -9ms (-20.45%)
  • ✅ vcgen/PurePrecond/4400/vcgen//wall-clock: -135ms (-23.48%)

Medium changes (2✅)

  • ✅ elab/bv_decide_inequality//instructions: -359.8M (-0.32%)
  • ✅ vcgen/AddSubCancelSimp/400/vcgen//wall-clock: -72ms (-11.54%)

Small changes (1✅, 2🟥)

  • 🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.FrameProc//instructions: +610.7M (+46.46%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Elab.Tactic.Do.Internal.VCGen.Solve//instructions: -1.3G (-5.71%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Elab.Tactic.Do.Internal.VCGen.SpecDB//instructions: +72.6M (+2.84%) (reduced significance based on *//lines)

@sgraf812
sgraf812 added this pull request to the merge queue Jul 30, 2026
Merged via the queue into master with commit a97629d Jul 30, 2026
22 checks passed
@sgraf812
sgraf812 deleted the sg/vcgen-frameproc-lazy branch August 6, 2026 07:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

changelog-no Do not include this PR in the release changelog 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-radar @leanprover-bot