test: add vcgen benchmark over the verina corpus#14340
Merged
Merged
Conversation
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
sgraf812
force-pushed
the
sg/vcgen-verina-bench
branch
from
45d8d92 to
0ac6bfa
Compare
sgraf812
changed the title
sgraf812
force-pushed
the
sg/vcgen-verina-bench
branch
from
0ac6bfa to
8954878
Compare
Contributor
Author
|
!bench |
|
Benchmark results for 8954878 against 8554442 are in. No significant results found. @sgraf812
Small changes (2✅)
|
sgraf812
force-pushed
the
sg/vcgen-verina-bench
branch
from
8954878 to
6cdb932
Compare
Contributor
Author
|
!bench |
|
Benchmark results for 6cdb932 against 8554442 are in. No significant results found. @sgraf812
Small changes (1✅)
|
Add `tests/elab_bench/verina.lean`: the Verina verification corpus (27 programs plus two intrinsic re-proofs), each discharged with `vcgen … with finish` in the `Std.Internal.Do` Hoare logic, every fixture in its own namespace with `@[local grind]` lemmas. Everything `vcgen` cannot discharge on its own, the supporting lemmas and a few manual verification-condition steps, is `sorry`'d following the `dag_hassorry_issue.lean` precedent, so the measured elaboration cost is the `vcgen` decomposition and `grind` search itself. The empty `.out.ignored` skips output checking, since the `grind` hints are irrelevant to the measurement. Verified compiling on nightly-2026-07-07; not yet re-verified against current master, as `vcgen`/`finish` still changes frequently and the proofs may need minor re-tuning.
sgraf812
force-pushed
the
sg/vcgen-verina-bench
branch
from
6cdb932 to
da85feb
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
3 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 adds a benchmark exercising
vcgen/grindon the Verina verification corpus, AI-ported from Velvet proofs.Each of the 27 programs' proofs are discharged with
vcgen … with finish; the supporting lemmas and the few manual VC steps aresorry'd, so the elaboration cost measured here is thevcgendecomposition andgrindsearch itself. Each fixture lives in its own namespace with@[local grind]lemmas so nothing leaks between them.