feat: add an assert do element for intrinsic verification

[sgraf812]

This PR adds an assert element to do notation for intrinsic verification. assert P states that P holds at that point in the program; assert s => P s binds the arguments of the assertion itself, such as the state of a state monad, using the same binders fun accepts. vcgen reads the assertion from the program and proves it as a verification condition; at runtime the element does nothing.

The parser is Lean.Parser.Term.doAssertion, distinct from the existing doAssert of assert!. It leads with nonReservedSymbol "assert" (includeIdent := true) at priority default+10, so a bare assert in statement position wins the equal-length tie against doExpr; assert! is the longer token, so the tokenizer never offers assert there. The clause body follows requiresClause: atomic Term.basicFun <|> (ppSpace >> termParser).

The element elaborates to Std.Internal.Do.assertGadget, and reports a missing-import error when Std.Internal.Do is absent. assertGadget loses its unused name parameter, and its specification Spec.assertGadget is now tagged @[spec] so vcgen finds it.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-07-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 12:12:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2d0879c245c9804aafe2b9b52dde1eca0712f889 --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 13:21:22)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c7673e73d368472501289ee81acc8b68d3000621 --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 14:47:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0a67f6b94669aa99183f0c7d5e15fc5c7f308a9f --onto 0bfc3acaef4ed0576307a77fbaa0c6e1a5dca402. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-30 16:08:14)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-30 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-07-30 12:12:40)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2d0879c245c9804aafe2b9b52dde1eca0712f889 --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-30 13:21:24)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c7673e73d368472501289ee81acc8b68d3000621 --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-30 14:47:41)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0a67f6b94669aa99183f0c7d5e15fc5c7f308a9f --onto a39eab69e1eee9ad38f4efe507907b1026a77808. You can force reference manual CI using the force-manual-ci label. (2026-07-30 16:08:15)

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for e7a008a against 0a67f6b are in. There are significant results. @sgraf812

• 🟥 build//instructions: +8.3G (+0.07%)

New metrics (9✅, 9🟥)

• 🟥 compiled/http_server//chunked_echo: +64ms (+1.23%)
• 🟥 compiled/http_server//cycles: +6.8G (+4.55%)
• 🟥 compiled/http_server//get_keepalive: +479ms (+18.01%)
• 🟥 compiled/http_server//instructions: +652.0M (+0.38%)
• ✅ compiled/http_server//many_headers: -75ms (-2.60%)
• 🟥 compiled/http_server//maxrss: +2MiB (+2.82%)
• 🟥 compiled/http_server//post_echo: +257ms (+7.24%)
• 🟥 compiled/http_server//task-clock: +1s (+3.32%)
• 🟥 compiled/http_server//wall-clock: +723ms (+5.05%)
• ✅ compiled/http_server_tcp//chunked_echo: -174ms (-3.63%)
• ✅ compiled/http_server_tcp//cycles: -4.3G (-3.02%)
• 🟥 compiled/http_server_tcp//get_keepalive: +16ms (+0.81%)
• ✅ compiled/http_server_tcp//instructions: -907.9M (-0.64%)
• ✅ compiled/http_server_tcp//many_headers: -41ms (-1.94%)
• ✅ compiled/http_server_tcp//maxrss: -5MiB (-3.91%)
• ✅ compiled/http_server_tcp//post_echo: -121ms (-3.82%)
• ✅ compiled/http_server_tcp//task-clock: -834ms (-2.45%)
• ✅ compiled/http_server_tcp//wall-clock: -319ms (-2.64%)

Medium changes (1✅)

• ✅ elab/bv_decide_inequality//instructions: -350.5M (-0.31%)

Small changes (30🟥)

• 🟥 build/module/Lake.DSL.DeclUtil//instructions: +146.7M (+4.68%)
• 🟥 build/module/Lean.Elab.AssertExists//instructions: +144.4M (+5.63%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.AuxDef//instructions: +96.0M (+6.28%)
• 🟥 build/module/Lean.Elab.CheckTactic//instructions: +151.1M (+6.61%)
• 🟥 build/module/Lean.Elab.Command.WithWeakNamespace//instructions: +130.8M (+12.05%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.GenInjective//instructions: +145.9M (+15.18%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.InfoTrees//instructions: +150.0M (+11.84%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Print//instructions: +155.6M (+2.57%)
• 🟥 build/module/Lean.Elab.RecommendedSpelling//instructions: +219.5M (+13.54%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.CbvSimproc//instructions: +133.0M (+8.02%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.DiscrTreeKey//instructions: +129.5M (+7.27%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Elab.Tactic.Doc//instructions: +150.5M (+3.78%)
• 🟥 build/module/Lean.Elab.Tactic.Grind.Annotated//instructions: +83.6M (+6.87%)
• 🟥 build/module/Lean.Elab.Tactic.Simproc//instructions: +112.0M (+6.63%)
• 🟥 build/module/Lean.Elab.Time//instructions: +148.0M (+13.70%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Linter.Basic//instructions: +141.0M (+10.34%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Linter.Builtin//instructions: +98.3M (+4.88%)
• 🟥 build/module/Lean.Linter.Coe//instructions: +169.1M (+10.11%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Linter.ConstructorAsVariable//instructions: +128.0M (+5.72%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lean.Linter.DocsOnAlt//instructions: +116.6M (+7.25%) (reduced significance based on absolute threshold)
• and 10 more