feat: intrinsic verification syntax for do-notation loops and def contracts by sgraf812 · Pull Request #14389 · leanprover/lean4

sgraf812 · 2026-07-14T16:31:50Z

This PR adds intrinsic verification syntax for Std.Internal.Do do-notation: loop invariants and function contracts that vcgen discharges automatically.

A for x in xs invariant cur => I do … loop annotates its invariant onto the loop combinator, elaborated in the loop body's scope so mutable variables and outer-loop variables resolve by name; nested loops are supported. A def may carry require P and ensures b => Q clauses on its signature, expanding to the plain definition plus an @[spec]-tagged specification theorem f.spec : ⦃P⦄ f args ⦃fun b => Q⦄ proved by vcgen [f] with finish. The test example findSmallest is then fully automatic with zero manual proof.

invariant, require, and ensures remain usable as ordinary identifiers; a bare occurrence only ends the preceding term in the position where the clause is expected. The contract expander is a builtin macro, so contracts work when only Std.Tactic.Do is imported. Scope is the MVP: for loops over List and Std.Legacy.Range; while, signals, and residual-VC discharge are not included.

Performance

The contract clauses are parsed as an alternative tried only after the ordinary def value parser fails, so a contract-free def parses exactly the previous grammar and its syntax tree is unchanged; metaprograms matching def syntax compile the same matchers as before. The remaining instruction regressions are small and intrinsic to adding syntax to the compiler: extending the built-in def and do grammar enlarges the parser tables that every Lean process initializes at startup, a fixed cost of a few million instructions per invocation that recurs across all module builds and surfaces as a larger percentage only on the smallest modules, and the type in a def signature is parsed with require/ensures excluded as identifiers, which reduces parser cache sharing for signatures by about +0.4% on the dedicated parser benchmark.

mathlib-lean-pr-testing · 2026-07-14T17:27:26Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3c080a47dbbe4b32ab01fd7ae332ad6bd30b4054 --onto 12c859a4d735fbcdb3ebbddb42dcc8619bcc7a7d. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-14 17:27:25)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3c080a47dbbe4b32ab01fd7ae332ad6bd30b4054 --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-15 12:12:43)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase aacd6121be3b52724ac1cd63ea5eca9f4b1c3c09 --onto 323137b022369d56a044ae5af01d1efd55872361. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-21 10:29:44)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase aacd6121be3b52724ac1cd63ea5eca9f4b1c3c09 --onto 3259610687883ec1ea48c481aba2469f2f83facf. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-21 16:29:18)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 749f580c3b7aec0908a057a51a89b304ecbd8151 --onto 3259610687883ec1ea48c481aba2469f2f83facf. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-23 15:56:14)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7fc3135964788ce99a700906daf7e538e34cd63d --onto 3259610687883ec1ea48c481aba2469f2f83facf. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-24 15:34:37)

leanprover-bot · 2026-07-14T17:27:28Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3c080a47dbbe4b32ab01fd7ae332ad6bd30b4054 --onto 7847ce51363794755252279e6732240bd4f27ca8. You can force reference manual CI using the force-manual-ci label. (2026-07-14 17:27:27)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3c080a47dbbe4b32ab01fd7ae332ad6bd30b4054 --onto a4b639c5a1e545677b36b09a4770b7b559df805b. You can force reference manual CI using the force-manual-ci label. (2026-07-15 12:12:45)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase aacd6121be3b52724ac1cd63ea5eca9f4b1c3c09 --onto 49ff95727f98d43984726b26742d17a1ceea9dd5. You can force reference manual CI using the force-manual-ci label. (2026-07-21 10:29:46)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 749f580c3b7aec0908a057a51a89b304ecbd8151 --onto 49ff95727f98d43984726b26742d17a1ceea9dd5. You can force reference manual CI using the force-manual-ci label. (2026-07-23 15:56:16)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 7fc3135964788ce99a700906daf7e538e34cd63d --onto 49ff95727f98d43984726b26742d17a1ceea9dd5. You can force reference manual CI using the force-manual-ci label. (2026-07-24 15:34:39)

Seasawher · 2026-07-23T09:19:13Z

This is a fantastic feature. I’m looking forward to its release.

sgraf812 · 2026-07-23T15:40:52Z

!bench

leanprover-radar · 2026-07-23T16:02:49Z

Benchmark results for 99e8d1c against 749f580 are in. There are significant results. @sgraf812

🟥 build exited with code 1
🟥 other exited with code 1

No significant changes detected.

sgraf812 · 2026-07-24T07:41:11Z

!bench

leanprover-radar · 2026-07-24T07:41:17Z

Benchmark results for a3f9058 against 749f580 are in. There are significant results. @sgraf812

🟥 build//instructions: +19.2G (+0.16%)

Large changes (1🟥)

🟥 compiled/parser//instructions: +457.0M (+1.33%)

Small changes (2✅, 18🟥)

🟥 build/module/Init.Data.Array//instructions: +3.9M (+0.70%)
🟥 build/module/Init.Data.ByteArray//instructions: +4.2M (+0.82%)
🟥 build/module/Init.Data.FloatArray//instructions: +4.2M (+0.77%)
🟥 build/module/Init.Data.Nat.Internal//instructions: +3.8M (+0.90%)
🟥 build/module/Init.Data.Queue//instructions: +4.2M (+0.60%)
🟥 build/module/Init.Data.UInt.Log2//instructions: +3.7M (+0.83%)
🟥 build/module/Init.Grind.Homo//instructions: +3.7M (+0.65%)
🟥 build/module/Lean.Elab.BuiltinDo.For//instructions: +3.3G (+39.70%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Do.InferControlInfo//instructions: +380.7M (+3.33%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Linter.Builtin//instructions: +59.0M (+2.94%)
🟥 build/module/Lean.Parser.Basic//instructions: +56.5M (+0.73%)
🟥 build/module/Lean.Parser.Command//instructions: +211.4M (+1.92%) (reduced significance based on *//lines)
🟥 build/module/Lean.Parser.Do//instructions: +104.6M (+1.77%)
✅ compiled/deriv//maxrss: -359kiB (-0.07%)
🟥 compiled/liasolver//instructions: +4.0M (+0.12%)
🟥 compiled/phashmap//instructions: +4.2M (+0.05%)
🟥 compiled/rbmap_library//instructions: +4.6M (+0.05%)
🟥 compiled/workspaceSymbolsNewRanges//instructions: +3.7M (+0.56%)
🟥 lake/inundation/startup//instructions: +4.0M (+2.12%)
✅ misc/leanchecker --fresh Init//maxrss: -7MiB (-1.38%)

sgraf812 · 2026-07-24T08:22:47Z

!bench

leanprover-radar · 2026-07-24T08:22:55Z

Benchmark results for 243b273 against 749f580 are in. There are significant results. @sgraf812

🟥 build//instructions: +19.0G (+0.16%)

Large changes (1🟥)

🟥 compiled/parser//instructions: +434.1M (+1.26%)

Small changes (21🟥)

🟥 build/module/Init.Data.Array//instructions: +3.8M (+0.70%)
🟥 build/module/Init.Data.ByteArray//instructions: +3.9M (+0.76%)
🟥 build/module/Init.Data.Iterators.Combinators//instructions: +4.0M (+0.81%)
🟥 build/module/Init.Data.Iterators.Lemmas.Consumers.Access//instructions: +4.1M (+0.59%)
🟥 build/module/Init.Data.Nat.Internal//instructions: +3.8M (+0.91%)
🟥 build/module/Init.Data.UInt.Log2//instructions: +3.7M (+0.83%)
🟥 build/module/Init.Grind.Homo//instructions: +3.9M (+0.68%)
🟥 build/module/Init.Syntax//instructions: +3.9M (+1.12%)
🟥 build/module/Lake.DSL.Targets//instructions: +50.3M (+0.51%)
🟥 build/module/Lean.Elab.BuiltinDo.For//instructions: +3.3G (+39.66%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Do.InferControlInfo//instructions: +387.0M (+3.39%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Tactic.Do//instructions: +15.2M (+1.45%)
🟥 build/module/Lean.Linter.Builtin//instructions: +56.6M (+2.82%)
🟥 build/module/Lean.Parser.Basic//instructions: +91.0M (+1.18%)
🟥 build/module/Lean.Parser.Command//instructions: +315.9M (+2.86%) (reduced significance based on *//lines)
🟥 build/module/Lean.Parser.Do//instructions: +162.3M (+2.75%) (reduced significance based on *//lines)
🟥 compiled/liasolver//instructions: +3.9M (+0.12%)
🟥 compiled/phashmap//instructions: +4.0M (+0.05%)
🟥 compiled/server_startup//instructions: +8.9M (+2.47%)
🟥 compiled/workspaceSymbolsNewRanges//instructions: +4.2M (+0.63%)
and 1 more

sgraf812 · 2026-07-24T14:08:08Z

!bench

leanprover-radar · 2026-07-24T14:08:22Z

Benchmark results for 8b30968 against 749f580 are in. There are significant results. @sgraf812

🟥 build//instructions: +32.3G (+0.28%)

Medium changes (1🟥)

🟥 compiled/parser//instructions: +126.8M (+0.37%)

Small changes (151🟥)

🟥 build/module/Init.CbvSimproc//instructions: +18.5M (+0.88%)
🟥 build/module/Init.Data.Float.Model.Unpacked.Operations.Compare//instructions: +56.3M (+7.90%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Float.Model.Unpacked.Operations.Sign//instructions: +60.7M (+10.66%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Float.Model.Unpacked.Operations.Status//instructions: +55.3M (+9.84%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Float.Model.Unpacked.Round//instructions: +68.1M (+7.92%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Format.Instances//instructions: +240.9M (+28.71%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Format.Syntax//instructions: +19.9M (+2.31%)
🟥 build/module/Init.Data.Format//instructions: +61.6M (+13.75%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Int.ToString//instructions: +54.0M (+9.20%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Iterators.Lemmas.Combinators//instructions: +44.5M (+8.38%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.Rat.Basic//instructions: +41.7M (+1.64%)
🟥 build/module/Init.Data.Slice.Array.Iterator//instructions: +29.8M (+2.14%)
🟥 build/module/Init.Data.Slice.List.Iterator//instructions: +63.9M (+7.08%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Extra//instructions: +266.6M (+8.71%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Iter.Intercalate//instructions: +89.0M (+12.81%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Iter//instructions: +16.3M (+3.11%)
🟥 build/module/Init.Data.String.Lemmas.Hashable//instructions: +127.7M (+22.21%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Lemmas.Intercalate//instructions: +424.7M (+33.97%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Lemmas.Iter//instructions: +109.9M (+12.29%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Lemmas.Length//instructions: +141.8M (+24.01%) (reduced significance based on absolute threshold)
and 130 more
and 1 hidden

…tracts This PR adds intrinsic verification syntax for `Std.Internal.Do` do-notation: loop invariants and function contracts that `vcgen` discharges automatically. A `for x in xs invariant cur => I do …` loop annotates its invariant onto the loop combinator, elaborated in the loop body's scope so mutable variables and outer-loop variables resolve by name; nested loops are supported. A `def` may carry `require P` and `ensures b => Q` clauses on its signature, expanding to the plain definition plus an `@[spec]`-tagged specification theorem `f.spec : ⦃P⦄ f args ⦃fun b => Q⦄` proved by `vcgen [f] with finish`.

sgraf812 · 2026-07-24T15:24:49Z

!bench

leanprover-radar · 2026-07-24T15:25:12Z

Benchmarking f51437b against 7fc3135 (preliminary results).

_{React with 👀 to be notified when the results are in. The command author is always notified.}

leanprover-radar · 2026-07-24T16:05:35Z

Benchmark results for f51437b against 7fc3135 are in. There are significant results. @sgraf812

🟥 build//instructions: +20.5G (+0.18%)

New metrics (3✅, 2🟥)

✅ elab/delayed_lift//cycles: -21.4M (-0.67%)
🟥 elab/delayed_lift//instructions: +13.8M (+0.24%)
🟥 elab/delayed_lift//maxrss: +2MiB (+0.10%)
✅ elab/delayed_lift//task-clock: -3ms (-0.57%)
✅ elab/delayed_lift//wall-clock: -4ms (-0.67%)

Medium changes (1🟥)

🟥 compiled/parser//instructions: +129.8M (+0.38%)

Small changes (65🟥)

🟥 build/module/Init.Data.Format.Instances//instructions: +82.6M (+9.84%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Extra//instructions: +163.2M (+5.33%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Lemmas.Pattern.Find.Basic//instructions: +73.9M (+3.23%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Lemmas.Pattern.Pred//instructions: +178.9M (+3.08%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Lemmas.Pattern.Split.Basic//instructions: +165.8M (+5.30%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Lemmas.Pattern.String.ForwardSearcher//instructions: +109.0M (+0.56%)
🟥 build/module/Init.Data.String.Lemmas.Pattern.TakeDrop.Basic//instructions: +185.2M (+2.84%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Lemmas.Search//instructions: +84.9M (+10.65%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.Lemmas.TakeDrop//instructions: +147.0M (+19.63%) (reduced significance based on absolute threshold)
🟥 build/module/Init.Data.String.TakeDrop//instructions: +20.2M (+0.73%)
🟥 build/module/Init.Data.ToString.Name//instructions: +101.1M (+8.93%) (reduced significance based on absolute threshold)
🟥 build/module/Init.System.FilePath//instructions: +122.2M (+6.52%) (reduced significance based on absolute threshold)
🟥 build/module/Init.System.Uri//instructions: +20.3M (+1.28%)
🟥 build/module/Lake.Config.Defaults//instructions: +34.8M (+6.73%) (reduced significance based on absolute threshold)
🟥 build/module/Lake.DSL.DeclUtil//instructions: +167.2M (+5.35%) (reduced significance based on absolute threshold)
🟥 build/module/Lake.Util.Casing//instructions: +60.9M (+7.76%) (reduced significance based on absolute threshold)
🟥 build/module/Lake.Util.Cli//instructions: +135.8M (+7.04%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Compiler.FFI//instructions: +50.3M (+5.06%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Data.Json.Basic//instructions: +32.5M (+1.15%)
🟥 build/module/Lean.Data.Json.Parser//instructions: +268.3M (+9.20%) (reduced significance based on absolute threshold)
and 45 more

sgraf812 added the changelog-language Language features and metaprograms label Jul 14, 2026

sgraf812 force-pushed the sg/kr1-intrinsic-do branch from ae7fb19 to 2adc4e1 Compare July 14, 2026 16:50

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

sgraf812 force-pushed the sg/kr1-intrinsic-do branch 3 times, most recently from fa3413e to 2e74ff6 Compare July 21, 2026 10:05

sgraf812 force-pushed the sg/kr1-intrinsic-do branch from 261936f to 8249948 Compare July 23, 2026 06:06

sgraf812 force-pushed the sg/kr1-intrinsic-do branch from aeff689 to 52530f0 Compare July 23, 2026 14:28

sgraf812 marked this pull request as ready for review July 23, 2026 15:40

sgraf812 requested review from TwoFX and kim-em as code owners July 23, 2026 15:40

sgraf812 force-pushed the sg/kr1-intrinsic-do branch 2 times, most recently from f8e503e to a3f9058 Compare July 24, 2026 06:44

sgraf812 requested a review from kmill as a code owner July 24, 2026 08:21

sgraf812 force-pushed the sg/kr1-intrinsic-do branch from 8b30968 to f51437b Compare July 24, 2026 15:05

Uh oh!

Conversation

sgraf812 commented Jul 14, 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 Jul 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

Seasawher commented Jul 23, 2026

Uh oh!

sgraf812 commented Jul 23, 2026

Uh oh!

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

Uh oh!

Uh oh!

sgraf812 commented Jul 24, 2026

Uh oh!

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

Uh oh!

Uh oh!

sgraf812 commented Jul 24, 2026

Uh oh!

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

Uh oh!

Uh oh!

sgraf812 commented Jul 24, 2026

Uh oh!

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

Uh oh!

Uh oh!

sgraf812 commented Jul 24, 2026

Uh oh!

leanprover-radar commented Jul 24, 2026

Uh oh!

leanprover-radar commented Jul 24, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

sgraf812 commented Jul 14, 2026 •

edited

Loading

mathlib-lean-pr-testing Bot commented Jul 14, 2026 •

edited

Loading

leanprover-bot commented Jul 14, 2026 •

edited

Loading

leanprover-radar commented Jul 23, 2026 •

edited

Loading

leanprover-radar commented Jul 24, 2026 •

edited

Loading

leanprover-radar commented Jul 24, 2026 •

edited

Loading

leanprover-radar commented Jul 24, 2026 •

edited

Loading