Merge branch 'master' into sofia/async-http-headers

.github/workflows/ci.yml

@@ -166,7 +166,7 @@ jobs:
       # 0: PRs without special label
       # 1: PRs with `merge-ci` label, merge queue checks, master commits
       # 2: nightlies
-      # 3: PRs with `release-ci` label, full releases
+      # 3: PRs with `release-ci` or `lake-ci` label, full releases
       - name: Set check level
         id: set-level
         # We do not use github.event.pull_request.labels.*.name here because
@@ -175,6 +175,7 @@ jobs:
         run: |
           check_level=0
           fast=false
+          lake_ci=false
 
           if [[ -n "${{ steps.set-release.outputs.RELEASE_TAG }}" || -n "${{ steps.set-release-custom.outputs.RELEASE_TAG }}" ]]; then
             check_level=3
@@ -189,13 +190,19 @@ jobs:
             elif echo "$labels" | grep -q "merge-ci"; then
               check_level=1
             fi
+            if echo "$labels" | grep -q "lake-ci"; then
+              lake_ci=true
+            fi
             if echo "$labels" | grep -q "fast-ci"; then
               fast=true
             fi
           fi
 
-          echo "check-level=$check_level" >> "$GITHUB_OUTPUT"
-          echo "fast=$fast" >> "$GITHUB_OUTPUT"
+          {
+            echo "check-level=$check_level"
+            echo "fast=$fast"
+            echo "lake-ci=$lake_ci"
+          } >> "$GITHUB_OUTPUT"
         env:
           GH_TOKEN: ${{ github.token }}
 
@@ -206,6 +213,7 @@ jobs:
           script: |
             const level = ${{ steps.set-level.outputs.check-level }};
             const fast = ${{ steps.set-level.outputs.fast }};
+            const lakeCi = "${{ steps.set-level.outputs.lake-ci }}" == "true";
             console.log(`level: ${level}, fast: ${fast}`);
             // use large runners where available (original repo)
             let large = ${{ github.repository == 'leanprover/lean4' }};
@@ -379,6 +387,11 @@ jobs:
                 job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DUSE_LAKE=OFF";
               }
             }
+            if (lakeCi) {
+              for (const job of matrix) {
+                job["CMAKE_OPTIONS"] = (job["CMAKE_OPTIONS"] ? job["CMAKE_OPTIONS"] + " " : "") + "-DLAKE_CI=ON";
+              }
+            }
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`);
             matrix = matrix.filter((job) => job["enabled"]);
             core.setOutput('matrix', matrix.filter((job) => !job["secondary"]));

.github/workflows/labels-from-comments.yml

@@ -1,5 +1,5 @@
 # This workflow allows any user to add one of the `awaiting-review`, `awaiting-author`, `WIP`,
-# `release-ci`, or a `changelog-XXX` label by commenting on the PR or issue.
+# `release-ci`, `lake-ci`, or a `changelog-XXX` label by commenting on the PR or issue.
 # If any labels from the set {`awaiting-review`, `awaiting-author`, `WIP`} are added, other labels
 # from that set are removed automatically at the same time.
 # Similarly, if any `changelog-XXX` label is added, other `changelog-YYY` labels are removed.
@@ -12,7 +12,7 @@ on:
 
 jobs:
   update-label:
-    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'changelog-'))
+    if: github.event.issue.pull_request != null && (contains(github.event.comment.body, 'awaiting-review') || contains(github.event.comment.body, 'awaiting-author') || contains(github.event.comment.body, 'WIP') || contains(github.event.comment.body, 'release-ci') || contains(github.event.comment.body, 'lake-ci') || contains(github.event.comment.body, 'changelog-'))
     runs-on: ubuntu-latest
 
     steps:
@@ -28,6 +28,7 @@ jobs:
           const awaitingAuthor = commentLines.includes('awaiting-author');
           const wip = commentLines.includes('WIP');
           const releaseCI = commentLines.includes('release-ci');
+          const lakeCI = commentLines.includes('lake-ci');
           const changelogMatch = commentLines.find(line => line.startsWith('changelog-'));
 
           if (awaitingReview || awaitingAuthor || wip) {
@@ -49,6 +50,9 @@ jobs:
           if (releaseCI) {
             await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['release-ci'] });
           }
+          if (lakeCI) {
+            await github.rest.issues.addLabels({ owner, repo, issue_number, labels: ['lake-ci'] });
+          }
 
           if (changelogMatch) {
             const changelogLabel = changelogMatch.trim();

.github/workflows/restart-on-label.yml

@@ -7,7 +7,7 @@ on:
 jobs:
   restart-on-label:
     runs-on: ubuntu-latest
-    if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci')
+    if: contains(github.event.label.name, 'merge-ci') || contains(github.event.label.name, 'release-ci') || contains(github.event.label.name, 'lake-ci')
     steps:
     - run: |
         # Finding latest CI workflow run on current pull request

CONTRIBUTING.md

@@ -7,7 +7,7 @@ Helpful links
 -------
 
 * [Development Setup](./doc/dev/index.md)
-* [Testing](./doc/dev/testing.md)
+* [Testing](./tests/README.md)
 * [Commit convention](./doc/dev/commit_convention.md)
 
 Before You Submit a Pull Request (PR):

doc/dev/index.md

@@ -1,7 +1,9 @@
 # Development Workflow
 
 If you want to make changes to Lean itself, start by [building Lean](../make/index.md) from a clean checkout to make sure that everything is set up correctly.
-After that, read on below to find out how to set up your editor for changing the Lean source code, followed by further sections of the development manual where applicable such as on the [test suite](testing.md) and [commit convention](commit_convention.md).
+After that, read on below to find out how to set up your editor for changing the Lean source code,
+followed by further sections of the development manual where applicable
+such as on the [test suite](../../tests/README.md) and [commit convention](commit_convention.md).
 
 If you are planning to make any changes that may affect the compilation of Lean itself, e.g. changes to the parser, elaborator, or compiler, you should first read about the [bootstrapping pipeline](bootstrap.md).
 You should not edit the `stage0` directory except using the commands described in that section when necessary.

doc/dev/testing.md

@@ -1,142 +0,0 @@
-# Test Suite
-
-**Warning:** This document is partially outdated.
-It describes the old test suite, which is currently in the process of being replaced.
-The new test suite's documentation can be found at [`tests/README.md`](../../tests/README.md).
-
-After [building Lean](../make/index.md) you can run all the tests using
-```
-cd build/release
-make test ARGS=-j4
-```
-Change the 4 to the maximum number of parallel tests you want to
-allow. The best choice is the number of CPU cores on your machine as
-the tests are mostly CPU bound.  You can find the number of processors
-on linux using `nproc` and on Windows it is the `NUMBER_OF_PROCESSORS`
-environment variable.
-
-You can run tests after [building a specific stage](bootstrap.md) by
-adding the `-C stageN` argument. The default when run as above is stage 1.  The
-Lean tests will automatically use that stage's corresponding Lean
-executables
-
-Running `make test` will not pick up new test files; run
-```bash
-cmake build/release/stage1
-```
-to update the list of tests.
-
-You can also use `ctest` directly if you are in the right folder.  So
-to run stage1 tests with a 300 second timeout run this:
-
-```bash
-cd build/release/stage1
-ctest -j 4 --output-on-failure --timeout 300
-```
-Useful `ctest` flags are `-R <name of test>` to run a single test, and
-`--rerun-failed` to run all tests that failed during the last run.
-You can also pass `ctest` flags via `make test ARGS="--rerun-failed"`.
-
-To get verbose output from ctest pass the `--verbose` command line
-option. Test output is normally suppressed and only summary
-information is displayed. This option will show all test output.
-
-## Test Suite Organization
-
-All these tests are included by [src/shell/CMakeLists.txt](https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt):
-
-- [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/): contains tests that come equipped with a
-  .lean.expected.out file. The driver script [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/test_single.sh) runs
-  each test and checks the actual output (*.produced.out) with the
-  checked in expected output.
-
-- [`tests/lean/run`](https://github.com/leanprover/lean4/tree/master/tests/lean/run/): contains tests that are run through the lean
-  command line one file at a time. These tests only look for error
-  codes and do not check the expected output even though output is
-  produced, it is ignored.
-
-  **Note:** Tests in this directory run with `-Dlinter.all=false` to reduce noise.
-  If your test needs to verify linter behavior (e.g., deprecation warnings),
-  explicitly enable the relevant linter with `set_option linter.<name> true`.
-
-- [`tests/lean/interactive`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/): are designed to test server requests at a
-  given position in the input file. Each .lean file contains comments
-  that indicate how to simulate a client request at that position.
-  using a `--^` point to the line position. Example:
-    ```lean,ignore
-    open Foo in
-    theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
-    Bla.
-      --^ completion
-    ```
-    In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
-    auto-completion request at `Bla.`. The expected output is stored in
-    a .lean.expected.out in the json format that is part of the
-    [Language Server
-    Protocol](https://microsoft.github.io/language-server-protocol/).
-
-    This can also be used to test the following additional requests:
-    ```
-    --^ textDocument/hover
-    --^ textDocument/typeDefinition
-    --^ textDocument/definition
-    --^ $/lean/plainGoal
-    --^ $/lean/plainTermGoal
-    --^ insert: ...
-    --^ collectDiagnostics
-    ```
-
-- [`tests/lean/server`](https://github.com/leanprover/lean4/tree/master/tests/lean/server/): Tests more of the Lean `--server` protocol.
-  There are just a few of them, and it uses .log files containing
-  JSON.
-
-- [`tests/compiler`](https://github.com/leanprover/lean4/tree/master/tests/compiler/): contains tests that will run the Lean compiler and
-  build an executable that is executed and the output is compared to
-  the .lean.expected.out file. This test also contains a subfolder
-  [`foreign`](https://github.com/leanprover/lean4/tree/master/tests/compiler/foreign/) which shows how to extend Lean using C++.
-
-- [`tests/lean/trust0`](https://github.com/leanprover/lean4/tree/master/tests/lean/trust0): tests that run Lean in a mode that Lean doesn't
-  even trust the .olean files (i.e., trust 0).
-
-- [`tests/bench`](https://github.com/leanprover/lean4/tree/master/tests/bench/): contains performance tests.
-
-- [`tests/plugin`](https://github.com/leanprover/lean4/tree/master/tests/plugin/): tests that compiled Lean code can be loaded into
-  `lean` via the `--plugin` command line option.
-
-## Writing Good Tests
-
-Every test file should contain:
-* an initial `/-! -/` module docstring summarizing the test's purpose
-* a module docstring for each test section that describes what is tested
-  and, if not 100% clear, why that is the desirable behavior
-
-At the time of writing, most tests do not follow these new guidelines yet.
-For an example of a conforming test, see [`tests/lean/1971.lean`](https://github.com/leanprover/lean4/tree/master/tests/lean/1971.lean).
-
-## Fixing Tests
-
-When the Lean source code or the standard library are modified, some of the
-tests break because the produced output is slightly different, and we have
-to reflect the changes in the `.lean.expected.out` files.
-We should not blindly copy the new produced output since we may accidentally
-miss a bug introduced by recent changes.
-The test suite contains commands that allow us to see what changed in a convenient way.
-First, we must install [meld](http://meldmerge.org/). On Ubuntu, we can do it by simply executing
-
-```
-sudo apt-get install meld
-```
-
-Now, suppose `bad_class.lean` test is broken. We can see the problem by going to [`tests/lean`](https://github.com/leanprover/lean4/tree/master/tests/lean) directory and
-executing
-
-```
-./test_single.sh -i bad_class.lean
-```
-
-When the `-i` option is provided, `meld` is automatically invoked
-whenever there is discrepancy between the produced and expected
-outputs. `meld` can also be used to repair the problems.
-
-In Emacs, we can also execute `M-x lean4-diff-test-file` to check/diff the file of the current buffer.
-To mass-copy all `.produced.out` files to the respective `.expected.out` file, use `tests/lean/copy-produced`.

doc/examples/compiler/run_test

@@ -1,11 +1,7 @@
 #!/usr/bin/env bash
 source ../../../tests/env_test.sh
-source "$TEST_DIR/util.sh"
 
 leanmake --always-make bin
 
-exec_capture test.lean \
-  ./build/bin/test hello world
-
-check_exit test.lean
-check_out test.lean
+capture ./build/bin/test hello world
+check_out_contains "[hello, world]"

doc/examples/run_test

@@ -1,9 +1,7 @@
 #!/usr/bin/env bash
 source ../../tests/env_test.sh
-source "$TEST_DIR/util.sh"
 
-exec_capture "$1" \
+capture_only "$1" \
   lean -Dlinter.all=false "$1"
-
-check_exit "$1"
-check_out "$1"
+check_exit_is_success
+check_out_file

src/Init.lean

@@ -30,6 +30,7 @@ public import Init.Hints
 public import Init.Conv
 public import Init.Guard
 public import Init.Simproc
+public import Init.CbvSimproc
 public import Init.SizeOfLemmas
 public import Init.BinderPredicates
 public import Init.Ext

src/Init/CbvSimproc.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public meta import Init.Data.ToString.Name  -- shake: keep (transitive public meta dep, fix)
+public import Init.Tactics
+import Init.Meta.Defs
+
+public section
+
+namespace Lean.Parser
+
+syntax cbvSimprocEval := "cbv_eval"
+
+/--
+A user-defined simplification procedure used by the `cbv` tactic.
+The body must have type `Lean.Meta.Sym.Simp.Simproc` (`Expr → SimpM Result`).
+Procedures are indexed by a discrimination tree pattern and fire at one of three phases:
+`↓` (pre), `cbv_eval` (eval), or `↑` (post, default).
+-/
+syntax (docComment)? attrKind "cbv_simproc " (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? ident " (" term ")" " := " term : command
+
+/--
+A `cbv_simproc` declaration without automatically adding it to the cbv simproc set.
+To activate, use `attribute [cbv_simproc]`.
+-/
+syntax (docComment)? "cbv_simproc_decl " ident " (" term ")" " := " term : command
+
+syntax (docComment)? attrKind "builtin_cbv_simproc " (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? ident " (" term ")" " := " term : command
+
+syntax (docComment)? "builtin_cbv_simproc_decl " ident " (" term ")" " := " term : command
+
+syntax (name := cbvSimprocPattern) "cbv_simproc_pattern% " term " => " ident : command
+
+syntax (name := cbvSimprocPatternBuiltin) "builtin_cbv_simproc_pattern% " term " => " ident : command
+
+namespace Attr
+
+syntax (name := cbvSimprocAttr) "cbv_simproc" (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? : attr
+
+syntax (name := cbvSimprocBuiltinAttr) "builtin_cbv_simproc" (Tactic.simpPre <|> Tactic.simpPost <|> cbvSimprocEval)? : attr
+
+end Attr
+
+macro_rules
+  | `($[$doc?:docComment]? cbv_simproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Sym.Simp.Simproc
+    `($[$doc?:docComment]? meta def $n:ident : $(mkIdent simprocType) := $body
+      cbv_simproc_pattern% $pattern => $n)
+
+macro_rules
+  | `($[$doc?:docComment]? builtin_cbv_simproc_decl $n:ident ($pattern:term) := $body) => do
+    let simprocType := `Lean.Meta.Sym.Simp.Simproc
+    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+      builtin_cbv_simproc_pattern% $pattern => $n)
+
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind cbv_simproc $[$phase?]? $n:ident ($pattern:term) := $body) => do
+    `($[$doc?:docComment]? cbv_simproc_decl $n ($pattern) := $body
+      attribute [$kind cbv_simproc $[$phase?]?] $n)
+
+macro_rules
+  | `($[$doc?:docComment]? $kind:attrKind builtin_cbv_simproc $[$phase?]? $n:ident ($pattern:term) := $body) => do
+    `($[$doc?:docComment]? builtin_cbv_simproc_decl $n ($pattern) := $body
+      attribute [$kind builtin_cbv_simproc $[$phase?]?] $n)
+
+end Lean.Parser

src/Init/Data/Array/Basic.lean

@@ -2151,7 +2151,4 @@ protected def repr {α : Type u} [Repr α] (xs : Array α) : Std.Format :=
 instance {α : Type u} [Repr α] : Repr (Array α) where
   reprPrec xs _ := Array.repr xs
 
-instance [ToString α] : ToString (Array α) where
-  toString xs := String.Internal.append "#" (toString xs.toList)
-
 end Array

src/Init/Data/ByteArray/Basic.lean

@@ -469,5 +469,3 @@ def prevn : Iterator → Nat → Iterator
 
 end Iterator
 end ByteArray
-
-instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩

src/Init/Data/FloatArray/Basic.lean

@@ -9,6 +9,7 @@ prelude
 public import Init.Data.Float
 import Init.Ext
 public import Init.GetElem
+public import Init.Data.ToString.Extra
 
 public section
 universe u

src/Init/Data/Rat/Basic.lean

@@ -11,6 +11,7 @@ public import Init.Data.OfScientific
 public import Init.Data.Int.DivMod.Basic
 public import Init.Data.String.Defs
 public import Init.Data.ToString.Macro
+public import Init.Data.ToString.Extra
 import Init.Data.Hashable
 import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Int.DivMod.Lemmas

src/Init/Data/SInt/Basic.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.UInt.Basic
+public import Init.Data.ToString.Extra
 
 @[expose] public section
 

src/Init/Data/Slice/Array/Iterator.lean

@@ -10,6 +10,7 @@ public import Init.Data.Slice.Operations
 import all Init.Data.Range.Polymorphic.Basic
 import Init.Omega
 public import Init.Data.Array.Subarray
+public import Init.Data.ToString.Extra
 
 public section
 

src/Init/Data/Slice/List/Iterator.lean

@@ -11,6 +11,7 @@ public import Init.Data.Iterators.Producers.List
 public import Init.Data.Iterators.Combinators.Take
 import all Init.Data.Range.Polymorphic.Basic
 public import Init.Data.Slice.Operations
+public import Init.Data.ToString.Extra
 
 public section
 

src/Init/Data/ToString.lean

@@ -9,3 +9,4 @@ prelude
 public import Init.Data.ToString.Basic
 public import Init.Data.ToString.Macro
 public import Init.Data.ToString.Name
+public import Init.Data.ToString.Extra

src/Init/Data/ToString/Basic.lean

@@ -51,29 +51,6 @@ instance {p : Prop} : ToString (Decidable p) := ⟨fun h =>
   | Decidable.isTrue _  => "true"
   | Decidable.isFalse _ => "false"⟩
 
-/--
-Converts a list into a string, using `ToString.toString` to convert its elements.
-
-The resulting string resembles list literal syntax, with the elements separated by `", "` and
-enclosed in square brackets.
-
-The resulting string may not be valid Lean syntax, because there's no such expectation for
-`ToString` instances.
-
-Examples:
-* `[1, 2, 3].toString = "[1, 2, 3]"`
-* `["cat", "dog"].toString = "[cat, dog]"`
-* `["cat", "dog", ""].toString = "[cat, dog, ]"`
--/
-protected def List.toString [ToString α] : List α → String
-  | [] => "[]"
-  | [x] => String.Internal.append (String.Internal.append "[" (toString x)) "]"
-  | x::xs => String.push (xs.foldl (fun l r => String.Internal.append (String.Internal.append l ", ") (toString r))
-      (String.Internal.append "[" (toString x))) ']'
-
-instance {α : Type u} [ToString α] : ToString (List α) :=
-  ⟨List.toString⟩
-
 instance : ToString PUnit.{u+1} :=
   ⟨fun _ => "()"⟩
 
@@ -89,11 +66,6 @@ instance : ToString Nat :=
 instance : ToString String.Pos.Raw :=
   ⟨fun p => Nat.repr p.byteIdx⟩
 
-instance : ToString Int where
-  toString
-    | Int.ofNat m   => toString m
-    | Int.negSucc m => String.Internal.append "-" (toString (succ m))
-
 instance (n : Nat) : ToString (Fin n) :=
   ⟨fun f => toString (Fin.val f)⟩
 

src/Init/Data/ToString/Extra.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+module
+
+prelude
+public import Init.Data.String.Defs
+
+public section
+
+/--
+Converts a list into a string, using `ToString.toString` to convert its elements.
+
+The resulting string resembles list literal syntax, with the elements separated by `", "` and
+enclosed in square brackets.
+
+The resulting string may not be valid Lean syntax, because there's no such expectation for
+`ToString` instances.
+
+Examples:
+* `[1, 2, 3].toString = "[1, 2, 3]"`
+* `["cat", "dog"].toString = "[cat, dog]"`
+* `["cat", "dog", ""].toString = "[cat, dog, ]"`
+-/
+protected def List.toString [ToString α] : List α → String
+  | [] => "[]"
+  | [x] => "[" ++ toString x ++ "]"
+  | x::xs => String.push (xs.foldl (fun l r => l ++ ", " ++ toString r) ("[" ++ (toString x))) ']'
+
+instance {α : Type u} [ToString α] : ToString (List α) :=
+  ⟨List.toString⟩
+
+instance [ToString α] : ToString (Array α) where
+  toString xs := "#" ++ (toString xs.toList)
+
+instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
+
+instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)

src/Init/Grind/Config.lean

@@ -15,6 +15,9 @@ Passed to `grind` using, for example, the `grind (config := { matchEqs := true }
 structure Config where
   /-- If `trace` is `true`, `grind` records used E-matching theorems and case-splits. -/
   trace : Bool := false
+  /-- If `markInstances` is `true`, E-matching proofs are marked with instance IDs
+  for precise tracking of which theorems appear in the final proof. -/
+  markInstances : Bool := false
   /-- If `lax` is `true`, `grind` will silently ignore any parameters referring to non-existent theorems
   or for which no patterns can be generated. -/
   lax : Bool := false

src/Init/Omega/Constraint.lean

@@ -52,6 +52,11 @@ namespace Constraint
 private local instance : Append String where
   append := String.Internal.append
 
+private local instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)
+
 instance : ToString Constraint where
   toString := private fun
   | ⟨none, none⟩ => "(-∞, ∞)"

src/Init/Omega/LinearCombo.lean

@@ -41,6 +41,14 @@ private def join (l : List String) : String :=
 private local instance : Append String where
   append := String.Internal.append
 
+private local instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)
+
+private local instance : Append String where
+  append := String.Internal.append
+
 instance : ToString LinearCombo where
   toString lc := private
     s!"{lc.const}{join <| lc.coeffs.toList.zipIdx.map fun ⟨c, i⟩ => s!" + {c} * x{i+1}"}"

src/Init/Tactics.lean

@@ -2262,6 +2262,42 @@ with grind
 ```
 This is more convenient than the equivalent `· by rename_i _ acc _; exact I1 acc`.
 
+### Witnesses
+
+When a specification has a parameter whose type is tagged with `@[mvcgen_witness_type]`, `mvcgen`
+classifies the corresponding goal as a *witness* rather than a verification condition.
+Witnesses are concrete values that the user must provide (inspired by zero-knowledge proofs),
+as opposed to invariants (predicates maintained across loop iterations) or verification conditions
+(propositions to prove).
+
+Witness goals are labelled `witness1`, `witness2`, etc. and can be provided in a `witnesses` section
+that appears before the `invariants` section:
+```
+mvcgen [...] witnesses
+· W1
+· W2
+invariants
+· I1
+with grind
+```
+Like invariants, witnesses support case label syntax:
+```
+mvcgen [...] witnesses
+| witness1 => W1
+```
+
+See the `@[mvcgen_witness_type]` attribute for how to register custom witness types.
+
+### Invariant and witness type attributes
+
+The `@[mvcgen_invariant_type]` and `@[mvcgen_witness_type]` tag attributes control how `mvcgen`
+classifies subgoals:
+* A goal whose type is an application of a type tagged with `@[mvcgen_invariant_type]` is classified
+  as an invariant (`inv<n>`).
+* A goal whose type is an application of a type tagged with `@[mvcgen_witness_type]` is classified
+  as a witness (`witness<n>`).
+* All other goals are classified as verification conditions (`vc<n>`).
+
 ### Invariant suggestions
 
 `mvcgen` will suggest invariants for you if you use the `invariants?` keyword.

src/Lean/AddDecl.lean

@@ -169,7 +169,7 @@ def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit :=
 where
   doAdd := do
     profileitM Exception "type checking" (← getOptions) do
-      withTraceNode `Kernel (return m!"{exceptEmoji ·} typechecking declarations {decl.getTopLevelNames}") do
+      withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do
         warnIfUsesSorry decl
         try
           let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?

src/Lean/Compiler/IR.lean

@@ -13,7 +13,6 @@ public import Lean.Compiler.IR.CompilerM
 public import Lean.Compiler.IR.NormIds
 public import Lean.Compiler.IR.Checker
 public import Lean.Compiler.IR.UnboxResult
-public import Lean.Compiler.IR.EmitC
 public import Lean.Compiler.IR.Sorry
 public import Lean.Compiler.IR.ToIR
 public import Lean.Compiler.IR.ToIRType
@@ -34,7 +33,6 @@ def compile (decls : Array Decl) : CompilerM (Array Decl) := do
   let mut decls := decls
   decls ← updateSorryDep decls
   logDecls `result decls
-  checkDecls decls
   addDecls decls
   inferMeta decls
   return decls

src/Lean/Compiler/IR/AddExtern.lean

@@ -15,6 +15,7 @@ import Lean.Compiler.LCNF.ExplicitBoxing
 import Lean.Compiler.LCNF.Internalize
 public import Lean.Compiler.ExternAttr
 import Lean.Compiler.LCNF.ExplicitRC
+import Lean.Compiler.Options
 
 public section
 
@@ -32,9 +33,10 @@ where
     let type ← Compiler.LCNF.getOtherDeclMonoType declName
     let mut typeIter := type
     let mut params := #[]
+    let ignoreBorrow := Compiler.compiler.ignoreBorrowAnnotation.get (← getOptions)
     repeat
       let .forallE binderName ty b _ := typeIter | break
-      let borrow := isMarkedBorrowed ty
+      let borrow := !ignoreBorrow && isMarkedBorrowed ty
       params := params.push {
         fvarId := (← mkFreshFVarId)
         type := ty,
@@ -70,6 +72,9 @@ where
       decl.saveImpure
       let decls ← Compiler.LCNF.addBoxedVersions #[decl]
       let decls ← Compiler.LCNF.runExplicitRc decls
+      for decl in decls do
+        decl.saveImpure
+        modifyEnv fun env => Compiler.LCNF.recordFinalImpureDecl env decl.name
       return decls
 
   addIr (decls : Array (Compiler.LCNF.Decl .impure)) : CoreM Unit := do

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -9,7 +9,6 @@ prelude
 public import Lean.Compiler.NameMangling
 public import Lean.Compiler.IR.EmitUtil
 public import Lean.Compiler.IR.NormIds
-public import Lean.Compiler.IR.SimpCase
 public import Lean.Compiler.IR.LLVMBindings
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.ModPkgExt

src/Lean/Compiler/IR/SimpCase.lean

@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-
-prelude
-public import Lean.Compiler.IR.Basic
-
-public section
-
-namespace Lean.IR
-
-def ensureHasDefault (alts : Array Alt) : Array Alt :=
-  if alts.any Alt.isDefault then alts
-  else if alts.size < 2 then alts
-  else
-    let last := alts.back!
-    let alts := alts.pop
-    alts.push (Alt.default last.body)
-
-end Lean.IR

src/Lean/Compiler/LCNF/Basic.lean

@@ -850,9 +850,11 @@ where
     | .jmp .. => inc
     | .return .. | unreach .. => return ()
 
+@[inline]
 partial def Code.forM [Monad m] (c : Code pu) (f : Code pu → m Unit) : m Unit :=
   go c
 where
+  @[specialize]
   go (c : Code pu) : m Unit := do
     f c
     match c with

src/Lean/Compiler/LCNF/EmitUtil.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+module
+
+prelude
+public import Lean.Compiler.LCNF.CompilerM
+import Lean.Compiler.LCNF.PhaseExt
+import Lean.Compiler.InitAttr
+
+namespace Lean.Compiler.LCNF
+
+private structure CollectUsedDeclsState where
+  visited : NameSet := {}
+  localDecls : Array (Decl .impure) := #[]
+  extSigs : Array (Signature .impure) := #[]
+
+/--
+Find all declarations that the declarations in `decls` transitively depend on. They are returned
+partitioned into the declarations from the current module and declarations from other modules.
+-/
+public partial def collectUsedDecls (decls : Array Name) :
+    CoreM (Array (Decl .impure) × Array (Signature .impure)) := do
+  let (_, state) ← go decls |>.run {}
+  return (state.localDecls, state.extSigs)
+where
+  go (names : Array Name) : StateRefT CollectUsedDeclsState CoreM Unit :=
+    names.forM fun name => do
+      if (← get).visited.contains name then return
+      modify fun s => { s with visited := s.visited.insert name }
+      if let some decl ← getLocalImpureDecl? name then
+        modify fun s => { s with localDecls := s.localDecls.push decl }
+        decl.value.forCodeM (·.forM visitCode)
+        let env ← getEnv
+        if let some initializer := getBuiltinInitFnNameFor? env decl.name <|> getInitFnNameFor? env decl.name then
+          go #[initializer]
+      else if let some sig ← getImpureSignature? name then
+        modify fun s => { s with extSigs := s.extSigs.push sig }
+      else
+        panic! s!"collectUsedDecls: could not find declaration or signature for '{name}'"
+
+  visitCode (code : Code .impure) : StateRefT CollectUsedDeclsState CoreM Unit := do
+    match code with
+    | .let decl _ =>
+      match decl.value with
+      | .const declName .. | .fap declName .. | .pap declName .. =>
+        go #[declName]
+      | _ => return ()
+    | _ => return ()
+
+public def usesModuleFrom (env : Environment) (modulePrefix : Name) : Bool :=
+  env.header.modules.any fun mod => mod.irPhases != .comptime && modulePrefix.isPrefixOf mod.module
+
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Internalize.lean

@@ -32,14 +32,10 @@ def InternalizeM.run' (x : InternalizeM pu α) (state : FVarSubst pu) (ctx : Con
 private def refreshBinderName (binderName : Name) : InternalizeM pu Name := do
   match binderName with
   | .num p _ =>
-    let r := .num p (← getThe CompilerM.State).nextIdx
-    modifyThe CompilerM.State fun s => { s with nextIdx := s.nextIdx + 1 }
-    return r
+    return .num p (← modifyGetThe CompilerM.State fun s => (s.nextIdx, { s with nextIdx := s.nextIdx + 1 }))
   | _ =>
     if (← read).uniqueIdents then
-      let r := .num binderName (← getThe CompilerM.State).nextIdx
-      modifyThe CompilerM.State fun s => { s with nextIdx := s.nextIdx + 1 }
-      return r
+      return .num binderName (← modifyGetThe CompilerM.State fun s => (s.nextIdx, { s with nextIdx := s.nextIdx + 1 }))
     else
       return binderName
 
@@ -59,7 +55,10 @@ private def mkNewFVarId (fvarId : FVarId) : InternalizeM pu FVarId := do
   addFVarSubst fvarId fvarId'
   return fvarId'
 
-private partial def internalizeExpr (e : Expr) : InternalizeM pu Expr :=
+private partial def internalizeExpr (e : Expr) : InternalizeM pu Expr := do
+  if pu == .impure then
+    -- impure types don't contain fvars
+    return e
   go e
 where
   goApp (e : Expr) : InternalizeM pu Expr := do

src/Lean/Compiler/LCNF/Passes.lean

@@ -85,7 +85,9 @@ def saveImpure : Pass where
   phaseOut := .impure
   name := `saveImpure
   run decls := decls.mapM fun decl => do
-    (← normalizeFVarIds decl).saveImpure
+    let decl ← normalizeFVarIds decl
+    decl.saveImpure
+    modifyEnv fun env => recordFinalImpureDecl env decl.name
     return decl
   shouldAlwaysRunCheck := true
 
@@ -160,8 +162,8 @@ def builtinPassManager : PassManager := {
     pushProj (occurrence := 1),
     detectSimpleGround,
     inferVisibility (phase := .impure),
-    saveImpure, -- End of impure phase
     toposortPass,
+    saveImpure, -- End of impure phase
   ]
 }
 

src/Lean/Compiler/LCNF/PhaseExt.lean

@@ -23,15 +23,15 @@ namespace Lean.Compiler.LCNF
 /--
 Set of public declarations whose base bodies should be exported to other modules
 -/
-private builtin_initialize baseTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkDeclSetExt
+private builtin_initialize baseTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
 /--
 Set of public declarations whose mono bodies should be exported to other modules
 -/
-private builtin_initialize monoTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkDeclSetExt
+private builtin_initialize monoTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
 /--
 Set of public declarations whose impure bodies should be exported to other modules
 -/
-private builtin_initialize impureTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkDeclSetExt
+private builtin_initialize impureTransparentDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
 
 private def getTransparencyExt : Phase → EnvExtension (List Name × NameSet)
   | .base => baseTransparentDeclsExt
@@ -171,6 +171,9 @@ def getMonoDecl? (declName : Name) : CoreM (Option (Decl .pure)) := do
 def getLocalImpureDecl? (declName : Name) : CoreM (Option (Decl .impure)) := do
   return impureExt.getState (← getEnv) |>.find? declName
 
+def getLocalImpureDecls : CoreM (Array Name) := do
+  return impureExt.getState (← getEnv) |>.toArray |>.map (·.fst)
+
 def getImpureSignature? (declName : Name) : CoreM (Option (Signature .impure)) := do
   return getSigCore? (← getEnv) impureSigExt declName
 
@@ -224,4 +227,23 @@ def getLocalDecl? (declName : Name) : CompilerM (Option ((pu : Purity) × Decl p
   let some decl ← getLocalDeclAt? declName (← getPhase) | return none
   return some ⟨_, decl⟩
 
+builtin_initialize declOrderExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
+
+def recordFinalImpureDecl (env : Environment) (name : Name) : Environment :=
+  declOrderExt.modifyState env fun s =>
+    (name :: s.1, s.2.insert name)
+
+def getImpureDeclIndices (env : Environment) (targets : Array Name) : Std.HashMap Name Nat := Id.run do
+  let (names, set) := declOrderExt.getState env
+  let mut map := Std.HashMap.emptyWithCapacity set.size
+  let targetSet := Std.HashSet.ofArray targets
+  let mut i := set.size
+  for name in names do
+    if targetSet.contains name then
+      map := map.insert name i
+    assert! i != 0
+    i := i - 1
+  assert! map.size == targets.size
+  return map
+
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/PublicDeclsExt.lean

@@ -10,15 +10,18 @@ public import Lean.Environment
 
 namespace Lean.Compiler.LCNF
 
-/-- Creates a replayable local environment extension holding a name set. -/
-public def mkDeclSetExt : IO (EnvExtension (List Name × NameSet)) :=
+/--
+Creates a replayable local environment extension holding a name set and the list of names in the
+order they were added to the set.
+-/
+public def mkOrderedDeclSetExt : IO (EnvExtension (List Name × NameSet)) :=
   registerEnvExtension
     (mkInitial := pure ([], {}))
     (asyncMode := .sync)
     (replay? := some <| fun oldState newState _ s =>
       let newEntries := newState.1.take (newState.1.length - oldState.1.length)
-      newEntries.foldl (init := s) fun s n =>
-        if s.1.contains n then
+      newEntries.reverse.foldl (init := s) fun s n =>
+        if s.2.contains n then
           s
         else
           (n :: s.1, if newState.2.contains n then s.2.insert n else s.2))
@@ -26,7 +29,7 @@ public def mkDeclSetExt : IO (EnvExtension (List Name × NameSet)) :=
 /--
 Set of declarations to be exported to other modules; visibility shared by base/mono/IR phases.
 -/
-private builtin_initialize publicDeclsExt : EnvExtension (List Name × NameSet) ← mkDeclSetExt
+private builtin_initialize publicDeclsExt : EnvExtension (List Name × NameSet) ← mkOrderedDeclSetExt
 
 public def isDeclPublic (env : Environment) (declName : Name) : Bool := Id.run do
   if !env.header.isModule then

src/Lean/Compiler/LCNF/SimpCase.lean

@@ -115,6 +115,16 @@ def Decl.simpCase (decl : Decl .impure) : CompilerM (Decl .impure) := do
   let value ← decl.value.mapCodeM (·.simpCase)
   return { decl with value }
 
+public def ensureHasDefault (alts : Array (Alt .impure)) : Array (Alt .impure) :=
+  if alts.any (· matches .default ..) then
+    alts
+  else if alts.size < 2 then
+    alts
+  else
+    let last := alts.back!
+    let alts := alts.pop
+    alts.push (.default last.getCode)
+
 public def simpCase : Pass :=
   Pass.mkPerDeclaration `simpCase .impure Decl.simpCase 0
 

src/Lean/Compiler/LCNF/ToDecl.lean

@@ -7,10 +7,13 @@ module
 prelude
 public import Lean.Compiler.InitAttr
 public import Lean.Compiler.LCNF.ToLCNF
+import Lean.Compiler.Options
 import Lean.Meta.Transform
 import Lean.Meta.Match.MatcherInfo
 import Init.While
+
 public section
+
 namespace Lean.Compiler.LCNF
 /--
 Inline constants tagged with the `[macro_inline]` attribute occurring in `e`.
@@ -127,10 +130,11 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
   let paramsFromTypeBinders (expr : Expr) : CompilerM (Array (Param .pure)) := do
     let mut params := #[]
     let mut currentExpr := expr
+    let ignoreBorrow := compiler.ignoreBorrowAnnotation.get (← getOptions)
     repeat
       match currentExpr with
       | .forallE binderName type body _ =>
-        let borrow := isMarkedBorrowed type
+        let borrow := !ignoreBorrow && isMarkedBorrowed type
         params := params.push (← mkParam binderName type borrow)
         currentExpr := body
       | _ => break
@@ -156,12 +160,15 @@ def toDecl (declName : Name) : CompilerM (Decl .pure) := do
       let value ← macroInline value
       return (type, value)
     let code ← toLCNF value
-    let decl ← if let .fun decl (.return _) := code then
+    let mut decl ← if let .fun decl (.return _) := code then
       eraseFunDecl decl (recursive := false)
       pure { name := declName, params := decl.params, type, value := .code decl.value, levelParams := info.levelParams, safe, inlineAttr? : Decl .pure }
     else
       pure { name := declName, params := #[], type, value := .code code, levelParams := info.levelParams, safe, inlineAttr? }
     /- `toLCNF` may eta-reduce simple declarations. -/
-    decl.etaExpand
+    decl ← decl.etaExpand
+    if compiler.ignoreBorrowAnnotation.get (← getOptions) then
+      decl := { decl with params := ← decl.params.mapM (·.updateBorrow false) }
+    return decl
 
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Toposort.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Compiler.LCNF.CompilerM
 public import Lean.Compiler.LCNF.PassManager
+import Lean.Compiler.InitAttr
 
 /-!
 This module "topologically sorts" an SCC of decls (an SCC of decls in the pipeline may in fact
@@ -42,8 +43,11 @@ where
     if (← get).seen.contains decl.name then
       return ()
 
+    let env ← getEnv
     modify fun s => { s with seen := s.seen.insert decl.name }
     decl.value.forCodeM (·.forM visitConsts)
+    if let some initializer := getBuiltinInitFnNameFor? env decl.name <|> getInitFnNameFor? env decl.name then
+      visitConst initializer
     modify fun s => { s with order := s.order.push decl }
 
   visitConsts (code : Code pu) : ToposortM pu Unit := do
@@ -51,15 +55,16 @@ where
     | .let decl _ =>
       match decl.value with
       | .const declName .. | .fap declName .. | .pap declName .. =>
-        if let some d := (← read).declsMap[declName]? then
-          process d
+        visitConst declName
       | _ => return ()
     | _ => return ()
 
+  visitConst (declName : Name) : ToposortM pu Unit := do
+    if let some d := (← read).declsMap[declName]? then
+      process d
+
 public def toposortDecls (decls : Array (Decl pu)) : CompilerM (Array (Decl pu)) := do
-  let (externDecls, otherDecls) := decls.partition (fun decl => decl.value matches .extern ..)
-  let otherDecls ← toposort otherDecls
-  return externDecls ++ otherDecls
+  toposort decls
 
 public def toposortPass : Pass where
   phase := .impure

src/Lean/Compiler/Options.lean

@@ -35,4 +35,10 @@ register_builtin_option compiler.relaxedMetaCheck : Bool := {
   descr := "Allow mixed `meta`/non-`meta` references in the same module. References to imports are unaffected."
 }
 
+register_builtin_option compiler.ignoreBorrowAnnotation : Bool := {
+  defValue := false
+  descr := "Ignore user defined borrow inference annotations. This is useful for export/extern \
+    forward declarations"
+}
+
 end Lean.Compiler

src/Lean/CoreM.lean

@@ -431,6 +431,10 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 @[inline] def CoreM.run' (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α :=
   Prod.fst <$> x.run ctx s
 
+/--
+Run a `CoreM` monad in IO.
+Note that the value of `ctx.initHeartbeats` is ignored and replaced with `IO.getNumHeartbeats`.
+-/
 @[inline] def CoreM.toIO (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) := do
   match (← (x.run { ctx with initHeartbeats := (← IO.getNumHeartbeats) } s).toIO') with
   | Except.error (Exception.error _ msg)   => throw <| IO.userError (← msg.toString)
@@ -440,7 +444,7 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 @[inline] def CoreM.toIO' (x : CoreM α) (ctx : Context) (s : State) : IO α :=
   (·.1) <$> x.toIO ctx s
 
--- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
+/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`. -/
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
 

src/Lean/Data.lean

@@ -29,3 +29,4 @@ public import Lean.Data.NameTrie
 public import Lean.Data.RBTree
 public import Lean.Data.RBMap
 public import Lean.Data.RArray
+public import Lean.Data.Iterators

src/Lean/Data/Iterators.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Lean.Data.Iterators.Producers

src/Lean/Data/Iterators/Producers.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Lean.Data.Iterators.Producers.PersistentHashMap

src/Lean/Data/Iterators/Producers/PersistentHashMap.lean

@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Array.Subarray
+public import Init.Data.Array.Subarray.Split
+public import Lean.Data.PersistentHashMap
+import Init.Data.Iterators.Consumers
+import Init.Omega
+import Init.Data.Slice.Array.Lemmas
+import Init.Data.Array.Mem
+import Init.Data.List.TakeDrop
+
+/-!
+# PersistentHashMap iterator
+
+This module provides an iterator for `Lean.PersistentHashMap` that is accessible via
+`Lean.PersistentHashMap.iter`.
+-/
+
+public section
+
+namespace Lean.PersistentHashMap
+
+open Std Std.Iterators
+
+/--
+A zipper for traversing a `PersistentHashMap`. This is an inductive structure
+representing the remaining key-value pairs to yield.
+-/
+inductive Zipper (α : Type u) (β : Type v) where
+  /-- No more elements to yield. -/
+  | done
+  /-- A frame of entries from a trie node. -/
+  | consEntries : Subarray (Entry α β (Node α β)) → Zipper α β → Zipper α β
+  /-- A frame of key-value pairs from a collision node. -/
+  | consCollision : (keys : Subarray α) → (vals : Subarray β) → keys.size = vals.size →
+      Zipper α β → Zipper α β
+
+def Zipper.prependNode (node : Node α β) (z : Zipper α β) : Zipper α β :=
+  match node with
+  | .entries es => .consEntries es.toSubarray z
+  | .collision keys vals hsz => .consCollision keys[*...*] vals[*...*] (by simpa) z
+
+@[inline]
+def Zipper.step (it : IterM (α := Zipper α β) Id (α × β)) : IterStep (IterM (α := Zipper α β) Id (α × β)) (α × β) :=
+  match it.internalState with
+  | .done => .done
+  | .consEntries es z' =>
+    if h : 0 < es.size then
+      let z : Zipper α β := .consEntries (es.drop 1) z'
+      match es[0] with
+      | .null => .skip ⟨z⟩
+      | .entry k v => .yield ⟨z⟩ (k, v)
+      | .ref node => .skip ⟨z.prependNode node⟩
+    else
+      .skip ⟨z'⟩
+  | .consCollision keys vals hsz z' =>
+    if h : 0 < vals.size then
+      .yield ⟨.consCollision (keys.drop 1) (vals.drop 1) (by simp [*]) z'⟩ (keys[0], vals[0])
+    else
+      .skip ⟨z'⟩
+
+instance instIterator : Iterator (Zipper α β) Id (α × β) where
+  IsPlausibleStep it step := step = Zipper.step it
+  step it := return .deflate <| ⟨Zipper.step it, rfl⟩
+
+/-- Counts the total number of entries reachable from a node, including nested children. -/
+def Node.measure (node : Node α β) : Nat :=
+  match node with
+  | .entries es => measureEntries es 0
+  | .collision _ vals _ => vals.size
+termination_by (sizeOf node, 0)
+where
+  /-- Counts the total entries in an entries array starting at index `i`. -/
+  measureEntries (es : Array (Entry α β (Node α β))) (i : Nat) : Nat :=
+    if h : i < es.size then
+      (match h_eq : es[i] with
+       | .null => 1
+       | .entry _ _ => 1
+       | .ref node =>
+         have : sizeOf node < sizeOf es := by
+           have h1 := Array.sizeOf_get es i h
+           rw [h_eq] at h1
+           simp +arith at h1
+           omega
+         2 + Node.measure node) + measureEntries es (i + 1)
+    else 0
+  termination_by (sizeOf es, es.size - i)
+  decreasing_by all_goals simp_wf <;> omega
+
+def Entry.measure (entry : Entry α β (Node α β)) : Nat :=
+  match entry with
+  | .null => 1
+  | .entry _ _ => 1
+  | .ref node => 2 + node.measure
+
+/-- Counts entries remaining in a subarray, including nested children. -/
+def subarrayMeasure (es : Subarray (Entry α β (Node α β))) : Nat :=
+  es.toList.map (·.measure) |>.sum
+
+/-- Counts the total remaining work in a zipper, including entries nested in child nodes. -/
+def Zipper.measure : Zipper α β → Nat
+  | .done => 0
+  | .consEntries es z' => subarrayMeasure es + z'.measure + 1
+  | .consCollision _ vals _ z' => vals.size + z'.measure + 1
+
+private theorem subarrayMeasure_cons (es : Subarray (Entry α β (Node α β)))
+    (h : 0 < es.size) :
+    subarrayMeasure es = es[0].measure + subarrayMeasure (es.drop 1) := by
+  simp only [subarrayMeasure, Subarray.toList_drop]
+  have hlen : 0 < es.toList.length := by simpa [Subarray.length_toList] using h
+  conv => lhs; rw [show es.toList = List.drop 0 es.toList from List.drop_zero.symm]
+  rw [List.drop_eq_getElem_cons (by omega)]
+  simp [List.map_cons, List.sum_cons, Subarray.getElem_eq_getElem_toList]
+
+private theorem measureEntries_eq_list_sum (es : Array (Entry α β (Node α β))) (i : Nat) :
+    Node.measure.measureEntries es i =
+      ((es.toList.drop i).map Entry.measure).sum := by
+  unfold Node.measure.measureEntries
+  split
+  · rename_i h
+    rw [List.drop_eq_getElem_cons (by simpa using h)]
+    simp only [List.map_cons, List.sum_cons]
+    rw [measureEntries_eq_list_sum es (i + 1)]
+    congr 1
+    simp only [Array.getElem_toList]
+    cases es[i] <;> simp [Entry.measure]
+  · rename_i h
+    rw [List.drop_eq_nil_of_le (by simpa using h)]
+    simp
+  termination_by es.size - i
+
+private theorem subarrayMeasure_toSubarray_eq (nes : Array (Entry α β (Node α β))) :
+    subarrayMeasure nes.toSubarray = Node.measure (.entries nes) := by
+  simp only [subarrayMeasure, Node.measure]
+  have h1 : nes.toSubarray.toList = nes.toList := by
+    rw [Subarray.toList_eq_drop_take]
+    simp only [Array.size_eq_length_toList, Array.start_toSubarray, le_refl, Nat.min_eq_left,
+      Nat.zero_le, Array.stop_toSubarray, Array.array_toSubarray, List.take_length, List.drop_zero]
+  have h2 := measureEntries_eq_list_sum nes 0
+  simp only [List.drop_zero] at h2
+  rw [h1]
+  exact h2.symm
+
+private def instFinitenessRelation :
+    FinitenessRelation (Zipper α β) Id where
+  Rel t' t := t'.internalState.measure < t.internalState.measure
+  wf := InvImage.wf _ Nat.lt_wfRel.wf
+  subrelation {it it'} h := by
+    obtain ⟨step, h, h'⟩ := h
+    simp only [IterM.IsPlausibleStep, Iterator.IsPlausibleStep, instIterator] at h'
+    subst h'
+    simp only [Zipper.step] at h
+    split at h
+    · -- .done: no successor
+      simp only [IterStep.successor_done] at h
+      exact nomatch h
+    · -- .consEntries es z'
+      rename_i es z' heq
+      split at h
+      · -- 0 < es.size
+        rename_i hsz
+        have h1 := subarrayMeasure_cons es hsz
+        match heq_es0 : es[0] with
+        | .null =>
+          simp only [heq_es0, IterStep.successor_skip, Option.some.injEq] at h; subst h
+          simp only [heq, Zipper.measure, heq_es0, Entry.measure] at h1 ⊢; omega
+        | .entry k v =>
+          simp only [heq_es0, IterStep.successor_yield, Option.some.injEq] at h; subst h
+          simp only [heq, Zipper.measure, heq_es0, Entry.measure] at h1 ⊢; omega
+        | .ref node =>
+          simp only [heq_es0, IterStep.successor_skip, Option.some.injEq] at h; subst h
+          simp only [heq_es0, Entry.measure] at h1
+          match heq_node : node with
+          | .entries nes =>
+            simp only [Zipper.prependNode, heq, Zipper.measure]
+            have h2 := subarrayMeasure_toSubarray_eq nes
+            omega
+          | .collision ks vs hsz' =>
+            simp only [Zipper.prependNode, heq, Zipper.measure, Array.size_mkSlice_rii]
+            simp only [Node.measure] at h1
+            omega
+      · -- ¬(0 < es.size) → skip to z'
+        simp only [IterStep.successor_skip, Option.some.injEq] at h; subst h
+        simp only [heq, Zipper.measure]; omega
+    · -- .consCollision keys vals hsz z'
+      rename_i keys vals hsz_eq z' heq
+      split at h
+      · -- 0 < vals.size → yield
+        simp only [IterStep.successor_yield, Option.some.injEq] at h; subst h
+        simp only [heq, Zipper.measure, Subarray.size_drop]; omega
+      · -- ¬(0 < vals.size) → skip
+        simp only [IterStep.successor_skip, Option.some.injEq] at h; subst h
+        simp only [heq, Zipper.measure]; omega
+
+instance instFinite : Finite (Zipper α β) Id :=
+  .of_finitenessRelation instFinitenessRelation
+
+@[always_inline, inline]
+instance instIteratorLoop {n : Type _ → Type _} [Monad n] :
+    IteratorLoop (Zipper α β) Id n :=
+  .defaultImplementation
+
+/--
+Returns a finite iterator over the key-value pairs of the given `PersistentHashMap`.
+The iteration order is unspecified.
+
+**Termination properties:**
+
+* `Finite` instance: always
+* `Productive` instance: always
+-/
+@[inline]
+def iter [BEq α] [Hashable α] (map : PersistentHashMap α β) :
+    Iter (α := Zipper α β) (α × β) :=
+  ⟨Zipper.prependNode map.root .done⟩
+
+end Lean.PersistentHashMap

src/Lean/Data/KVMap.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Format.Syntax
 public import Init.Data.ToString.Name
+public import Init.Data.ToString.Extra
 
 public section
 

src/Lean/Data/Name.lean

@@ -205,7 +205,7 @@ def anyS (n : Name) (f : String → Bool) : Bool :=
 /-- Return true if the name is in a namespace associated to metaprogramming. -/
 def isMetaprogramming (n : Name) : Bool :=
   let components := n.components
-  components.head? == some `Lean || (components.any fun n => n == `Tactic || n == `Linter)
+  components.head?.any (· == `Lean) || (components.any (· matches `Tactic | `Linter | `Simproc | `Meta))
 
 end Name
 end Lean

src/Lean/Data/OpenDecl.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.ToString.Name
+public import Init.Data.ToString.Extra
 
 public section
 

src/Lean/Elab/BuiltinDo/Let.lean

@@ -145,13 +145,13 @@ def elabDoArrow (letOrReassign : LetOrReassign) (stx : TSyntax [``doIdDecl, ``do
       | _, _ => pure xType?
     elabDoIdDecl x xType? rhs (declareMutVar? letOrReassign.getLetMutTk? x <| dec.continueWithUnit)
       (kind := dec.kind)
-  | `(doPatDecl| _%$pattern ← $rhs) =>
+  | `(doPatDecl| _%$pattern $[: $patType?]? ← $rhs) =>
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
-    elabDoIdDecl x none rhs dec.continueWithUnit (kind := dec.kind)
-  | `(doPatDecl| $pattern:term ← $rhs $[| $otherwise? $(rest?)?]?) =>
+    elabDoIdDecl x patType? rhs dec.continueWithUnit (kind := dec.kind)
+  | `(doPatDecl| $pattern:term $[: $patType?]? ← $rhs $[| $otherwise? $(rest?)?]?) =>
     let rest? := rest?.join
     let x := mkIdentFrom pattern (← mkFreshUserName `__x)
-    elabDoIdDecl x none rhs do
+    elabDoIdDecl x patType? rhs do
       match letOrReassign, otherwise? with
       | .let mutTk?, some otherwise =>
         elabDoElem (← `(doElem| let $[mut%$mutTk?]? $pattern:term := $x | $otherwise $(rest?)?)) dec

src/Lean/Elab/Do/InferControlInfo.lean

@@ -184,7 +184,7 @@ partial def ofLetOrReassignArrow (reassignment : Bool) (decl : TSyntax [``doIdDe
   | `(doIdDecl| $x:ident $[: $_]? ← $rhs) =>
     let reassigns := if reassignment then #[x] else #[]
     ofLetOrReassign reassigns rhs none none
-  | `(doPatDecl| $pattern ← $rhs $[| $otherwise? $[$body??]?]?) =>
+  | `(doPatDecl| $pattern $[: $_]? ← $rhs $[| $otherwise? $[$body??]?]?) =>
     let reassigns ← if reassignment then getPatternVarsEx pattern else pure #[]
     ofLetOrReassign reassigns rhs otherwise? body??.join
   | _ => throwError "Not a let or reassignment declaration: {toString decl}"

src/Lean/Elab/Do/Legacy.lean

@@ -722,7 +722,7 @@ def getDoLetRecVars (doLetRec : Syntax) : TermElabM (Array Var) := do
 def getDoIdDeclVar (doIdDecl : Syntax) : Var :=
   doIdDecl[0]
 
--- termParser >> leftArrow >> termParser >> optional (" | " >> termParser)
+-- termParser >> optType >> leftArrow >> termParser >> optional (" | " >> termParser)
 def getDoPatDeclVars (doPatDecl : Syntax) : TermElabM (Array Var) := do
   let pattern := doPatDecl[0]
   getPatternVarsEx pattern
@@ -1420,7 +1420,7 @@ mutual
      where
      ```
      def doIdDecl   := leading_parser ident >> optType >> leftArrow >> doElemParser
-     def doPatDecl  := leading_parser termParser >> leftArrow >> doElemParser >> optional ((" | " >> doSeq) >> optional doSeq)
+     def doPatDecl  := leading_parser termParser >> optType >> leftArrow >> doElemParser >> optional ((" | " >> doSeq) >> optional doSeq)
      ```
   -/
   partial def doLetArrowToCode (doLetArrow : Syntax) (doElems : List Syntax) : M CodeBlock := do
@@ -1440,13 +1440,21 @@ mutual
         | kRef::_  => concat c kRef y k
     else if decl.getKind == ``Parser.Term.doPatDecl then
       let pattern := decl[0]
-      let doElem  := decl[2]
-      let optElse := decl[3]
+      let optType := decl[1]
+      let doElem  := decl[3]
+      let optElse := decl[4]
       if optElse.isNone then withFreshMacroScope do
-        let auxDo ← if isMutableLet doLetArrow then
-          `(do let%$doLetArrow __discr ← $doElem; let%$doLetArrow mut $pattern:term := __discr)
+        let auxDo ← if optType.isNone then
+          if isMutableLet doLetArrow then
+            `(do let%$doLetArrow __discr ← $doElem; let%$doLetArrow mut $pattern:term := __discr)
+          else
+            `(do let%$doLetArrow __discr ← $doElem; let%$doLetArrow $pattern:term := __discr)
         else
-          `(do let%$doLetArrow __discr ← $doElem; let%$doLetArrow $pattern:term := __discr)
+          let ty := optType[0][1]
+          if isMutableLet doLetArrow then
+            `(do let%$doLetArrow __discr : $ty ← $doElem; let%$doLetArrow mut $pattern:term := __discr)
+          else
+            `(do let%$doLetArrow __discr : $ty ← $doElem; let%$doLetArrow $pattern:term := __discr)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
       else
         let elseSeq := optElse[1]
@@ -1457,7 +1465,11 @@ mutual
         else
           pure (getDoSeqElems contSeq).toArray
         let contSeq := mkDoSeq contSeq
-        let auxDo ← `(do let%$doLetArrow __discr ← $doElem; match%$doLetArrow __discr with | $pattern:term => $contSeq | _ => $elseSeq)
+        let auxDo ← if optType.isNone then
+          `(do let%$doLetArrow __discr ← $doElem; match%$doLetArrow __discr with | $pattern:term => $contSeq | _ => $elseSeq)
+        else
+          let ty := optType[0][1]
+          `(do let%$doLetArrow __discr : $ty ← $doElem; match%$doLetArrow __discr with | $pattern:term => $contSeq | _ => $elseSeq)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
     else
       throwError "unexpected kind of `do` declaration"
@@ -1492,10 +1504,15 @@ mutual
       doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
     else if decl.getKind == ``Parser.Term.doPatDecl then
       let pattern := decl[0]
-      let doElem  := decl[2]
-      let optElse := decl[3]
+      let optType := decl[1]
+      let doElem  := decl[3]
+      let optElse := decl[4]
       if optElse.isNone then withFreshMacroScope do
-        let auxDo ← `(do let __discr ← $doElem; $pattern:term := __discr)
+        let auxDo ← if optType.isNone then
+          `(do let __discr ← $doElem; $pattern:term := __discr)
+        else
+          let ty := optType[0][1]
+          `(do let __discr : $ty ← $doElem; $pattern:term := __discr)
         doSeqToCode <| getDoSeqElems (getDoSeq auxDo) ++ doElems
       else
         throwError "reassignment with `|` (i.e., \"else clause\") is not currently supported"

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -56,7 +56,7 @@ def unfoldLHS (declName : Name) (mvarId : MVarId) : MetaM MVarId := mvarId.withC
     deltaLHS mvarId
 
 private partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := do
-  withTraceNode `Elab.definition.eqns (return m!"{exceptEmoji ·} proving:{indentExpr type}") do
+  withTraceNode `Elab.definition.eqns (fun _ => return m!"proving:{indentExpr type}") do
   withNewMCtxDepth do
     let main ← mkFreshExprSyntheticOpaqueMVar type
     let (_, mvarId) ← main.mvarId!.intros
@@ -78,7 +78,7 @@ private partial def mkEqnProof (declName : Name) (type : Expr) : MetaM Expr := d
   recursion and structural recursion can and should use this too.
   -/
   go (mvarId : MVarId) : MetaM Unit := do
-    withTraceNode `Elab.definition.eqns (return m!"{exceptEmoji ·} step:\n{MessageData.ofGoal mvarId}") do
+    withTraceNode `Elab.definition.eqns (fun _ => return m!"step:\n{MessageData.ofGoal mvarId}") do
     if (← tryURefl mvarId) then
       return ()
     else if (← tryContradiction mvarId) then

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -118,7 +118,7 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
   The dictionary is built using the `PProd` (`And` for inductive predicates).
   We keep searching it until we find `C recArg`, where `C` is the auxiliary fresh variable created at `withBelowDict`.  -/
 partial def toBelow (below : Expr) (numIndParams : Nat) (positions : Positions) (fnIndex : Nat) (recArg : Expr) : MetaM Expr := do
-  withTraceNode `Elab.definition.structural (return m!"{exceptEmoji ·} searching IH for {recArg} in {←inferType below}") do
+  withTraceNode `Elab.definition.structural (fun _ => return m!"searching IH for {recArg} in {←inferType below}") do
     withBelowDict below numIndParams positions fun Cs belowDict =>
       toBelowAux Cs[fnIndex]! belowDict recArg below
 

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -73,7 +73,7 @@ Creates the proof of the unfolding theorem for `declName` with type `type`. It
    is solved using `rfl` or `contradiction`.
 -/
 partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
-  withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} proving:{indentExpr type}") do
+  withTraceNode `Elab.definition.structural.eqns (fun _ => return m!"proving:{indentExpr type}") do
     prependError m!"failed to generate equational theorem for `{.ofConstName declName}`" do
     withNewMCtxDepth do
       let main ← mkFreshExprSyntheticOpaqueMVar type
@@ -83,7 +83,7 @@ partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
       instantiateMVars main
 where
   goUnfold (mvarId : MVarId) : MetaM Unit := do
-    withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} goUnfold:\n{MessageData.ofGoal mvarId}") do
+    withTraceNode `Elab.definition.structural.eqns (fun _ => return m!"goUnfold:\n{MessageData.ofGoal mvarId}") do
     let mvarId' ← mvarId.withContext do
       -- This should now be headed by `.brecOn`
       let goal ← mvarId.getType
@@ -110,7 +110,7 @@ where
     go mvarId'
 
   go (mvarId : MVarId) : MetaM Unit := do
-    withTraceNode `Elab.definition.structural.eqns (return m!"{exceptEmoji ·} step:\n{MessageData.ofGoal mvarId}") do
+    withTraceNode `Elab.definition.structural.eqns (fun _ => return m!"step:\n{MessageData.ofGoal mvarId}") do
       if (← tryURefl mvarId) then
         trace[Elab.definition.structural.eqns] "tryURefl succeeded"
         return ()

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -53,7 +53,7 @@ So we create a unfold equation generator that aliases an existing private `eq_de
 wherever the current module expects it.
 -/
 def copyPrivateUnfoldTheorem : GetUnfoldEqnFn := fun declName => do
-  withTraceNode `ReservedNameAction (pure m!"{exceptOptionEmoji ·} copyPrivateUnfoldTheorem running for {declName}") do
+  withTraceNode `ReservedNameAction (fun _ => pure m!"copyPrivateUnfoldTheorem running for {declName}") do
   let name := mkEqLikeNameFor (← getEnv) declName unfoldThmSuffix
   if let some mod ← findModuleOf? declName then
     let unfoldName' := mkPrivateNameCore mod (.str (privateToUserName declName) unfoldThmSuffix)

src/Lean/Elab/Tactic.lean

@@ -17,6 +17,7 @@ public import Lean.Elab.Tactic.Location
 public import Lean.Elab.Tactic.SimpTrace
 public import Lean.Elab.Tactic.Simp
 public import Lean.Elab.Tactic.Simproc
+public import Lean.Elab.Tactic.CbvSimproc
 public import Lean.Elab.Tactic.BuiltinTactic
 public import Lean.Elab.Tactic.Split
 public import Lean.Elab.Tactic.Conv

src/Lean/Elab/Tactic/CbvSimproc.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Init.CbvSimproc
+public import Lean.Meta.Tactic.Cbv.CbvSimproc
+public import Lean.Elab.Command
+
+public section
+
+namespace Lean.Elab
+open Lean Meta Sym
+
+-- NB: This duplicates `elabSimprocPattern` from `Lean.Elab.Tactic.Simproc`
+-- to avoid pulling in simp simproc elaboration as a dependency.
+def elabCbvSimprocPattern (stx : Syntax) : MetaM Expr := do
+  let go : TermElabM Expr := do
+    let pattern ← Term.elabTerm stx none
+    Term.synthesizeSyntheticMVars
+    return pattern
+  go.run'
+
+-- **Note**: `abstractMVars` returns a lambda expression, but `mkPatternFromExpr` expects a
+-- proof term (it calls `inferType` to get the forall type used as the pattern). We convert the
+-- lambda telescope into a forall telescope, then create a metavariable of that forall type so
+-- that `mkPatternFromExpr` can recover it via `inferType`. This is a workaround until the
+-- pattern API supports lambda telescopes directly (see `Sym.mkSimprocPatternFromExpr'`).
+public def mkSimprocPatternFromExpr (e : Expr) : MetaM Pattern := do
+  let result ← abstractMVars e
+  let forallExpr ← lambdaTelescope result.expr fun args body => mkForallFVars args body
+  let term ← mkFreshExprMVar forallExpr
+  mkPatternFromExpr term result.paramNames.toList
+
+
+def elabCbvSimprocKeys (stx : Syntax) : MetaM (Array DiscrTree.Key) := do
+  let pattern ← elabCbvSimprocPattern stx
+  let symPattern ← mkSimprocPatternFromExpr pattern
+  return symPattern.mkDiscrTreeKeys
+
+def checkCbvSimprocType (declName : Name) : CoreM Unit := do
+  let decl ← getConstInfo declName
+  match decl.type with
+  | .const ``Sym.Simp.Simproc _ => pure ()
+  | _ => throwError "Unexpected type for cbv simproc pattern: Expected \
+      `{.ofConstName ``Sym.Simp.Simproc}`, but `{declName}` has type{indentExpr decl.type}"
+
+namespace Command
+open Lean.Meta.Tactic.Cbv
+
+@[builtin_command_elab Lean.Parser.cbvSimprocPattern] def elabCbvSimprocPattern : CommandElab := fun stx => do
+  let `(cbv_simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
+  liftTermElabM do
+    let declName ← realizeGlobalConstNoOverload declName
+    checkCbvSimprocType declName
+    let keys ← elabCbvSimprocKeys pattern
+    registerCbvSimproc declName keys
+
+@[builtin_command_elab Lean.Parser.cbvSimprocPatternBuiltin] def elabCbvSimprocPatternBuiltin : CommandElab := fun stx => do
+  let `(builtin_cbv_simproc_pattern% $pattern => $declName) := stx | throwUnsupportedSyntax
+  liftTermElabM do
+    let declName ← realizeGlobalConstNoOverload declName
+    checkCbvSimprocType declName
+    let keys ← elabCbvSimprocKeys pattern
+    let val := mkAppN (mkConst ``registerBuiltinCbvSimproc)
+      #[toExpr declName, toExpr keys, mkConst declName]
+    let initDeclName ← mkFreshUserName (declName ++ `declare)
+    declareBuiltin initDeclName val
+
+end Command
+
+end Lean.Elab

src/Lean/Elab/Tactic/Do/Attr.lean

@@ -250,3 +250,42 @@ def SpecExtension.getTheorems (ext : SpecExtension) : CoreM SpecTheorems :=
 
 def getSpecTheorems : CoreM SpecTheorems :=
   specAttr.getTheorems
+
+/--
+Marks a type as an invariant type for the `mvcgen` tactic.
+Goals whose type is an application of a tagged type will be classified
+as invariants rather than verification conditions.
+-/
+builtin_initialize mvcgenInvariantAttr : TagAttribute ←
+  registerTagAttribute `mvcgen_invariant_type
+    "marks a type as an invariant type for the `mvcgen` tactic"
+
+/--
+Returns `true` if `ty` is an application of a type tagged with `@[mvcgen_invariant_type]`.
+-/
+def isMVCGenInvariantType (env : Environment) (ty : Expr) : Bool :=
+  if let .const name .. := ty.getAppFn then
+    mvcgenInvariantAttr.hasTag env name
+  else
+    false
+
+/--
+Marks a type as a witness type for the `mvcgen` tactic.
+Goals whose type is an application of a tagged type will be classified
+as witnesses rather than verification conditions.
+In the spirit of zero-knowledge proofs, witnesses are concrete values that the user
+must provide, as opposed to invariants (predicates maintained across iterations)
+or verification conditions (propositions to prove).
+-/
+builtin_initialize mvcgenWitnessTypeAttr : TagAttribute ←
+  registerTagAttribute `mvcgen_witness_type
+    "marks a type as a witness type for the `mvcgen` tactic"
+
+/--
+Returns `true` if `ty` is an application of a type tagged with `@[mvcgen_witness_type]`.
+-/
+def isMVCGenWitnessType (env : Environment) (ty : Expr) : Bool :=
+  if let .const name .. := ty.getAppFn then
+    mvcgenWitnessTypeAttr.hasTag env name
+  else
+    false

src/Lean/Elab/Tactic/Do/VCGen.lean

@@ -35,6 +35,7 @@ namespace VCGen
 
 structure Result where
   invariants : Array MVarId
+  witnesses : Array MVarId
   vcs : Array MVarId
 
 partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result := do
@@ -45,10 +46,13 @@ partial def genVCs (goal : MVarId) (ctx : Context) (fuel : Fuel) : MetaM Result
     for h : idx in *...state.invariants.size do
       let mv := state.invariants[idx]
       mv.setTag (Name.mkSimple ("inv" ++ toString (idx + 1)))
+    for h : idx in *...state.witnesses.size do
+      let mv := state.witnesses[idx]
+      mv.setTag (Name.mkSimple ("witness" ++ toString (idx + 1)))
     for h : idx in *...state.vcs.size do
       let mv := state.vcs[idx]
       mv.setTag (Name.mkSimple ("vc" ++ toString (idx + 1)) ++ (← mv.getTag).eraseMacroScopes)
-    return { invariants := state.invariants, vcs := state.vcs }
+    return { invariants := state.invariants, witnesses := state.witnesses, vcs := state.vcs }
 where
   onFail (goal : MGoal) (name : Name) : VCGenM Expr := do
     -- trace[Elab.Tactic.Do.vcgen] "fail {goal.toExpr}"
@@ -351,60 +355,77 @@ where
 
 end VCGen
 
+/-- Shared implementation for elaborating goal sections (invariants, witnesses).
+    `tagPrefix` is `"inv"` or `"witness"`, used to parse labels like `inv1` or `witness2`.
+    `label` is `"invariant"` or `"witness"`, used in error messages.
+    When `requireAll` is true, an error is thrown if fewer alts are provided than goals. -/
+private def elabGoalSection (goals : Array MVarId) (alts : Array Syntax)
+    (tagPrefix : String) (label : String) (requireAll := true) : TacticM Unit := do
+  let goals ← goals.filterM (not <$> ·.isAssigned)
+  let mut dotOrCase := LBool.undef -- .true => dot
+  for h : n in 0...alts.size do
+    let alt := alts[n]
+    match alt with
+    | `(goalDotAlt| · $rhs) =>
+      if dotOrCase matches .false then
+        logErrorAt alt m!"Alternation between labelled and bulleted {label}s is not supported."
+        break
+      dotOrCase := .true
+      let some mv := goals[n]? | do
+        logErrorAt alt m!"More {label}s have been defined ({alts.size}) than there were unassigned {label} goals `{tagPrefix}<n>` ({goals.size})."
+        continue
+      withRef rhs do
+      discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
+    | `(goalCaseAlt| | $tag $args* => $rhs) =>
+      if dotOrCase matches .true then
+        logErrorAt alt m!"Alternation between labelled and bulleted {label}s is not supported."
+        break
+      dotOrCase := .false
+      let n? : Option Nat := do
+          let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal
+          let .str .anonymous s := tag.getId | none
+          s.dropPrefix? tagPrefix >>= String.Slice.toNat?
+      let some mv := do goals[(← n?) - 1]? | do
+        logErrorAt alt m!"No {label} with label {tag} {repr tag}."
+        continue
+      if ← mv.isAssigned then
+        logErrorAt alt m!"{label} {n?.get!} is already assigned."
+        continue
+      withRef rhs do
+      discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv
+    | _ => logErrorAt alt m!"Expected `goalDotAlt`, got {alt}"
+  if requireAll && alts.size < goals.size then
+    let missingTypes ← goals[alts.size:].toArray.mapM (·.getType)
+    throwError "Lacking definitions for the following {label}s.\n{toMessageList missingTypes}"
+
+def elabWitnesses (stx : Syntax) (witnesses : Array MVarId) : TacticM Unit := do
+  let some stx := stx.getOptional? | return ()
+  let stx : TSyntax ``witnessAlts := ⟨stx⟩
+  withRef stx do
+  match stx with
+  | `(witnessAlts| witnesses $alts*) =>
+    elabGoalSection witnesses alts "witness" "witness"
+  | _ => logErrorAt stx m!"Expected witnessAlts, got {stx}"
+
 def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant : MVarId → TacticM Term) : TacticM Unit := do
   let some stx := stx.getOptional? | return ()
   let stx : TSyntax ``invariantAlts := ⟨stx⟩
   withRef stx do
   match stx with
   | `(invariantAlts| $invariantsKW $alts*) =>
-    let invariants ← invariants.filterM (not <$> ·.isAssigned)
-
-    let mut dotOrCase := LBool.undef -- .true => dot
-    for h : n in 0...alts.size do
-      let alt := alts[n]
-      match alt with
-      | `(invariantDotAlt| · $rhs) =>
-        if dotOrCase matches .false then
-          logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported."
-          break
-        dotOrCase := .true
-        let some mv := invariants[n]? | do
-          logErrorAt alt m!"More invariants have been defined ({alts.size}) than there were unassigned invariants goals `inv<n>` ({invariants.size})."
-          continue
-        withRef rhs do
-        discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
-      | `(invariantCaseAlt| | $tag $args* => $rhs) =>
-        if dotOrCase matches .true then
-          logErrorAt alt m!"Alternation between labelled and bulleted invariants is not supported."
-          break
-        dotOrCase := .false
-        let n? : Option Nat := do
-            let `(binderIdent| $tag:ident) := tag | some n -- fall back to ordinal
-            let .str .anonymous s := tag.getId | none
-            s.dropPrefix? "inv" >>= String.Slice.toNat?
-        let some mv := do invariants[(← n?) - 1]? | do
-          logErrorAt alt m!"No invariant with label {tag} {repr tag}."
-          continue
-        if ← mv.isAssigned then
-          logErrorAt alt m!"Invariant {n?.get!} is already assigned."
-          continue
-        withRef rhs do
-        discard <| evalTacticAt (← `(tactic| rename_i $args*; exact $rhs)) mv
-      | _ => logErrorAt alt m!"Expected `invariantDotAlt`, got {alt}"
-
     if let `(invariantsKW| invariants) := invariantsKW then
-      if alts.size < invariants.size then
-        let missingTypes ← invariants[alts.size:].toArray.mapM (·.getType)
-        throwErrorAt stx m!"Lacking definitions for the following invariants.\n{toMessageList missingTypes}"
+      elabGoalSection invariants alts "inv" "invariant"
     else
-      -- Otherwise, we have `invariants?`. Suggest missing invariants.
+      -- We have `invariants?`. First elaborate any user-provided alts, then suggest the rest.
+      elabGoalSection invariants alts "inv" "invariant" (requireAll := false)
+      let invariants ← invariants.filterM (not <$> ·.isAssigned)
       let mut suggestions := #[]
       for i in 0...invariants.size do
         let mv := invariants[i]!
         if ← mv.isAssigned then
           continue
         let invariant ← suggestInvariant mv
-        suggestions := suggestions.push (← `(invariantDotAlt| · $invariant))
+        suggestions := suggestions.push (← `(goalDotAlt| · $invariant))
       let alts' := alts ++ suggestions
       let stx' ← `(invariantAlts|invariants $alts'*)
       if suggestions.size > 0 then
@@ -456,8 +477,8 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
     | none => .unlimited
   let goal ← getMainGoal
   let goal ← if ctx.config.elimLets then elimLets goal else pure goal
-  let { invariants, vcs } ← VCGen.genVCs goal ctx fuel
-  trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  let { invariants, witnesses, vcs } ← VCGen.genVCs goal ctx fuel
+  trace[Elab.Tactic.Do.vcgen] "after genVCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
   let runOnVCs (tac : TSyntax `tactic) (extraMsg : MessageData) (vcs : Array MVarId) : TermElabM (Array MVarId) :=
     vcs.flatMapM fun vc =>
       tryCatchRuntimeEx
@@ -466,10 +487,13 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
         (fun ex => throwError "Error while running {tac} on {vc}Message: {indentD ex.toMessageData}\n{extraMsg}")
   let invariants ←
     if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) "Try again with -leave." invariants else pure invariants
-  trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ vcs).mapM fun m => m.getTag}"
-  elabInvariants stx[3] invariants (suggestInvariant vcs)
+  trace[Elab.Tactic.Do.vcgen] "before elabWitnesses {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
+  elabWitnesses stx[3] witnesses
+  let witnesses ← witnesses.filterM (not <$> ·.isAssigned)
+  trace[Elab.Tactic.Do.vcgen] "before elabInvariants {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
+  elabInvariants stx[4] invariants (suggestInvariant vcs)
   let invariants ← invariants.filterM (not <$> ·.isAssigned)
-  trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
+  trace[Elab.Tactic.Do.vcgen] "before trying trivial VCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
   let vcs ← do
     let vcs ← if ctx.config.trivial then runOnVCs (← `(tactic| try mvcgen_trivial)) "Try again with -trivial." vcs else pure vcs
     let vcs ← if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) "Try again with -leave." vcs else pure vcs
@@ -477,17 +501,17 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
   -- Eliminating lets here causes some metavariables in `mkFreshPair_triple` to become nonassignable
   -- so we don't do it. Presumably some weird delayed assignment thing is going on.
   -- let vcs ← if ctx.config.elimLets then liftMetaM <| vcs.mapM elimLets else pure vcs
-  trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ vcs).mapM fun m => m.getTag}"
-  let vcs ← elabVCs stx[4] vcs
-  trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ vcs).mapM fun m => m.getTag}"
-  replaceMainGoal (invariants ++ vcs).toList
+  trace[Elab.Tactic.Do.vcgen] "before elabVCs {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
+  let vcs ← elabVCs stx[5] vcs
+  trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ witnesses ++ vcs).mapM fun m => m.getTag}"
+  replaceMainGoal (invariants ++ witnesses ++ vcs).toList
   -- trace[Elab.Tactic.Do.vcgen] "replaced main goal, new: {← getGoals}"
 
 @[builtin_tactic Lean.Parser.Tactic.mvcgenHint]
 def elabMVCGenHint : Tactic := fun stx => withMainContext do
   let stx' : TSyntax ``mvcgen := TSyntax.mk <| stx
     |>.setKind ``Lean.Parser.Tactic.mvcgen
-    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
+    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push mkNullNode |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
   -- logInfo m!"{stx}\n{toString stx}\n{repr stx}"
   -- logInfo m!"{stx'}\n{toString stx'}\n{repr stx'}"
   Lean.Meta.Tactic.TryThis.addSuggestion stx stx'

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -73,6 +73,10 @@ structure State where
   -/
   invariants : Array MVarId := #[]
   /--
+  Holes of witness type that have been generated so far.
+  -/
+  witnesses : Array MVarId := #[]
+  /--
   The verification conditions that have been generated so far.
   -/
   vcs : Array MVarId := #[]
@@ -104,8 +108,11 @@ def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
   -- VC to the user as-is, without abstracting any variables in the local context.
   -- This only makes sense for synthetic opaque metavariables.
   goal.setKind .syntheticOpaque
-  if ty.isAppOf ``Std.Do.Invariant then
+  let env ← getEnv
+  if isMVCGenInvariantType env ty then
     modify fun s => { s with invariants := s.invariants.push goal }
+  else if isMVCGenWitnessType env ty then
+    modify fun s => { s with witnesses := s.witnesses.push goal }
   else
     modify fun s => { s with vcs := s.vcs.push goal }
 

src/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.lean

@@ -408,20 +408,20 @@ public def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term :
   --
   -- Finally, build the syntax for the suggestion. It's a giant configuration space mess, because
   -- 1. Generally want to suggest something using `⇓ ⟨xs, letMuts⟩ => ...`, i.e. `PostCond.noThrow`.
-  -- 2. However, on early return we want to suggest something using `Invariant.withEarlyReturn`.
+  -- 2. However, on early return we want to suggest something using `Invariant.withEarlyReturnNewDo`.
   -- 3. When there are non-`False` failure conditions, we cannot suggest `⇓ ⟨xs, letMuts⟩ => ...`.
   --    We might be able to suggest `⇓? ⟨xs, letMuts⟩ => ...` (`True` failure condition),
   --    or `post⟨...⟩` (more than 0 failure handlers, but ending in `PUnit.unit`), and fall back to
   --    `by exact ⟨...⟩` (not ending in `PUnit.unit`).
-  -- 4. Similarly for the `onExcept` argument of `Invariant.withEarlyReturn`.
+  -- 4. Similarly for the `onExcept` argument of `Invariant.withEarlyReturnNewDo`.
   -- Hence the spaghetti code.
   --
   if let some (ρ, σ) ← hasEarlyReturn vcs inv letMutsTy then
     -- logWarning m!"Found early return for {inv}!"
-    -- Suggest an invariant using `Invariant.withEarlyReturn`.
+    -- Suggest an invariant using `Invariant.withEarlyReturnNewDo`.
     if let some (success, onReturn, failureConds) := suggestion? then
       -- First construct `onContinue` and `onReturn` clause and simplify them according to the
-      -- definition of `Invariant.withEarlyReturn`.
+      -- definition of `Invariant.withEarlyReturnNewDo`.
       let (onContinue, onReturn) ← withLocalDeclD `xs (mkApp2 (mkConst ``List.Cursor us) α l) fun xs =>
         withLocalDeclD `r ρ fun r =>
         withLocalDeclD `letMuts σ fun letMuts => do
@@ -439,21 +439,21 @@ public def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term :
       if failureConds.points.isEmpty then
         match failureConds.default with
         | .false | .punit =>
-          `(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue))
+          `(Invariant.withEarlyReturnNewDo (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue))
         -- we handle the following two cases here rather than through
         -- `postCondWithMultipleConditions` below because that would insert a superfluous `by exact _`.
         | .true =>
-          `(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue (onExcept := ExceptConds.true)))
+          `(Invariant.withEarlyReturnNewDo (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue (onExcept := ExceptConds.true)))
         | .other e =>
-          `(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue (onExcept := $(← Lean.PrettyPrinter.delab e))))
+          `(Invariant.withEarlyReturnNewDo (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue (onExcept := $(← Lean.PrettyPrinter.delab e))))
       else -- need the postcondition long form as `onExcept` arg
         let mut terms : Array Term := #[]
         for point in failureConds.points do
           terms := terms.push (← Lean.PrettyPrinter.delab point)
         let onExcept ← postCondWithMultipleConditions terms failureConds.default
-        `(Invariant.withEarlyReturn (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue) (onExcept := $onExcept))
+        `(Invariant.withEarlyReturnNewDo (onReturn := fun r letMuts => $onReturn) (onContinue := fun xs letMuts => $onContinue) (onExcept := $onExcept))
     else -- No suggestion. Just fill in `_`.
-      `(Invariant.withEarlyReturn (onReturn := fun r letMuts => _) (onContinue := fun xs letMuts => _))
+      `(Invariant.withEarlyReturnNewDo (onReturn := fun r letMuts => _) (onContinue := fun xs letMuts => _))
   else if let some (success, _, failureConds) := suggestion? then
     -- No early return, but we do have a suggestion.
     withLocalDeclD `xs (mkApp2 (mkConst ``List.Cursor us) α l) fun xs =>

src/Lean/Elab/Tactic/Grind/Main.lean

@@ -253,6 +253,9 @@ def grind
     return ()
   mvarId.withContext do
     let params ← mkGrindParams config only ps mvarId
+    let params := if Grind.grind.unusedLemmaThreshold.get (← getOptions) > 0 then
+      { params with config.markInstances := true }
+    else params
     Grind.withProtectedMCtx config mvarId fun mvarId' => do
       let finalize (result : Grind.Result) : TacticM Unit := do
         if result.hasFailed then
@@ -263,7 +266,10 @@ def grind
           Grind.evalGrindTactic seq
           -- **Note**: We are returning only the first goal that could not be solved.
           let goal? := if let goal :: _ := (← get).goals then some goal else none
-          Grind.liftGrindM <| Grind.mkResult params goal?
+          let result ← Grind.liftGrindM <| Grind.mkResult params goal?
+          if goal?.isNone then
+            Grind.liftGrindM <| Grind.checkUnusedActivations mvarId' result.counters
+          return result
         finalize result
       else
         let result ← Grind.main mvarId' params

src/Lean/Elab/Tactic/NormCast.lean

@@ -38,7 +38,7 @@ def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) :=
 
 /-- Proves `a = b` by simplifying using move and squash lemmas. -/
 def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
-  withTraceNode `Tactic.norm_cast (return m!"{exceptOptionEmoji ·} proving: {← mkEq a b}") do
+  withTraceNode `Tactic.norm_cast (fun _ => return m!"proving: {← mkEq a b}") do
   proveEqUsing (← normCastExt.down.getTheorems) a b
 
 /-- Constructs the expression `(e : ty)`. -/
@@ -97,9 +97,8 @@ def splittingProcedure (expr : Expr) : MetaM Simp.Result := do
 
   let msg := m!"splitting {expr}"
   let msg
-    | .error _ => return m!"{bombEmoji} {msg}"
-    | .ok r => return if r.expr == expr then m!"{crossEmoji} {msg}" else
-      m!"{checkEmoji} {msg} to {r.expr}"
+    | .error _ => return msg
+    | .ok r => return if r.expr == expr then msg else m!"{msg} to {r.expr}"
   withTraceNode `Tactic.norm_cast msg do
 
   try
@@ -140,7 +139,7 @@ Discharging function used during simplification in the "squash" step.
 -- TODO: normCast takes a list of expressions to use as lemmas for the discharger
 -- TODO: a tactic to print the results the discharger fails to prove
 def prove (e : Expr) : SimpM (Option Expr) := do
-  withTraceNode `Tactic.norm_cast (return m!"{exceptOptionEmoji ·} discharging: {e}") do
+  withTraceNode `Tactic.norm_cast (fun _ => return m!"discharging: {e}") do
   return (← findLocalDeclWithType? e).map mkFVar
 
 /--

src/Lean/Message.lean

@@ -66,9 +66,29 @@ structure NamingContext where
   currNamespace : Name
   openDecls : List OpenDecl
 
+/-- Structured result status of a trace node action, produced by `withTraceNode` and
+`withTraceNodeBefore` and included in the `TraceData` of trace messages. Either
+`.success` (✅️), `.failure` (❌️), or `.error` (💥️).
+
+This is used both to render emojis in trace messages and to allow more
+robust inspection of trace logs via metaprogramming.
+
+See also `Except.toTraceResult` for converting an `Except ε α` to a `TraceResult`. -/
+inductive TraceResult where
+  /-- The traced action succeeded (✅️, `checkEmoji`). -/
+  | success
+  /-- The traced action failed (❌️, `crossEmoji`). -/
+  | failure
+  /-- An exception was thrown during the traced action (💥️, `bombEmoji`). -/
+  | error
+  deriving Inhabited, BEq, Repr
+
 structure TraceData where
   /-- Trace class, e.g. `Elab.step`. -/
   cls       : Name
+  /-- Structured success/failure result set by `withTraceNode`/`withTraceNodeBefore`.
+  `none` for trace nodes not created by these functions (e.g. `addTrace`, diagnostic nodes). -/
+  result?   : Option TraceResult := none
   /-- Start time in seconds; 0 if unknown to avoid `Option` allocation. -/
   startTime : Float := 0
   /-- Stop time in seconds; 0 if unknown to avoid `Option` allocation. -/

src/Lean/Meta/AppBuilder.lean

@@ -341,8 +341,7 @@ private def mkFun (constName : Name) : MetaM (Expr × Expr) := do
 
 private def withAppBuilderTrace [ToMessageData α] [ToMessageData β]
     (f : α) (xs : β) (k : MetaM Expr) : MetaM Expr :=
-  let emoji | .ok .. => checkEmoji | .error .. => crossEmoji
-  withTraceNode `Meta.appBuilder (return m!"{emoji ·} f: {f}, xs: {xs}") do
+  withTraceNode `Meta.appBuilder (fun _ => return m!"f: {f}, xs: {xs}") do
     try
       let res ← k
       trace[Meta.appBuilder.result] res

src/Lean/Meta/Check.lean

@@ -329,8 +329,8 @@ where
 Throw an exception if `e` is not type correct.
 -/
 def check (e : Expr) : MetaM Unit :=
-  withTraceNode `Meta.check (fun res =>
-      return m!"{if res.isOk then checkEmoji else crossEmoji} {e}") do
+  withTraceNode `Meta.check (fun _ =>
+      return m!"{e}") do
     try
       withTransparency TransparencyMode.all $ checkAux e
     catch ex =>

src/Lean/Meta/Eqns.lean

@@ -304,7 +304,7 @@ def getUnfoldEqnFor? (declName : Name) (nonRec := false) : MetaM (Option Name) :
 
 builtin_initialize
   registerReservedNameAction fun name => do
-    withTraceNode `ReservedNameAction (pure m!"{exceptBoolEmoji ·} Lean.Meta.Eqns reserved name action for {name}") do
+    withTraceNode `ReservedNameAction (fun _ => pure m!"Lean.Meta.Eqns reserved name action for {name}") do
       if let some (declName, suffix) := declFromEqLikeName (← getEnv) name then
         if name == mkEqLikeNameFor (← getEnv) declName suffix then
           if isEqnReservedNameSuffix suffix then

src/Lean/Meta/IndPredBelow.lean

@@ -319,7 +319,7 @@ the first `nrealParams` are parameters and the remaining are motives.
 public partial def mkBelowMatcher (matcherApp : MatcherApp) (belowParams : Array Expr) (nrealParams : Nat)
     (ctx : RecursionContext) (transformAlt : RecursionContext → Expr → MetaM Expr) :
     MetaM (Option (Expr × MetaM Unit)) :=
-  withTraceNode `Meta.IndPredBelow.match (return m!"{exceptEmoji ·} {matcherApp.toExpr} and {belowParams}") do
+  withTraceNode `Meta.IndPredBelow.match (fun _ => return m!"{matcherApp.toExpr} and {belowParams}") do
   let mut input ← getMkMatcherInputInContext matcherApp (unfoldNamed := false)
   let mut discrs := matcherApp.discrs
   let mut matchTypeAdd := #[] -- #[(discrIdx, ), ...]
@@ -448,7 +448,7 @@ where
       StateRefT (Array NewDecl) MetaM (Pattern × Pattern) := do
     match originalPattern with
     | .ctor ctorName us params fields =>
-      withTraceNode `Meta.IndPredBelow.match (return m!"{exceptEmoji ·} pattern {← originalPattern.toExpr} to {belowIndName}") do
+      withTraceNode `Meta.IndPredBelow.match (fun _ => return m!"pattern {← originalPattern.toExpr} to {belowIndName}") do
       let ctorInfo ← getConstInfoCtor ctorName
       let shortCtorName := ctorName.replacePrefix ctorInfo.induct .anonymous
       let belowCtor ← getConstInfoCtor (belowIndName ++ shortCtorName)

src/Lean/Meta/Injective.lean

@@ -107,7 +107,7 @@ def mkInjectiveTheoremNameFor (ctorName : Name) : Name :=
 
 private def mkInjectiveTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
   let name := mkInjectiveTheoremNameFor ctorVal.name
-  withTraceNode `Meta.injective (msg := (return m!"{exceptEmoji ·} generating `{name}`")) do
+  withTraceNode `Meta.injective (msg := (fun _ => return m!"generating `{name}`")) do
   let some type ← mkInjectiveTheoremType? ctorVal
     | return ()
   trace[Meta.injective] "type: {type}"
@@ -164,7 +164,7 @@ private def mkInjectiveEqTheoremValue (ctorVal : ConstructorVal) (targetType : E
 
 private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
   let name := mkInjectiveEqTheoremNameFor ctorVal.name
-  withTraceNode `Meta.injective (msg := (return m!"{exceptEmoji ·} generating `{name}`")) do
+  withTraceNode `Meta.injective (msg := (fun _ => return m!"generating `{name}`")) do
   let some type ← mkInjectiveEqTheoremType? ctorVal
     | return ()
   trace[Meta.injective] "type: {type}"
@@ -186,7 +186,7 @@ register_builtin_option genInjectivity : Bool := {
 
 def mkInjectiveTheorems (declName : Name) : MetaM Unit := do
   if (← getEnv).contains ``Eq.propIntro && genInjectivity.get (← getOptions) &&  !(← isInductivePredicate declName) then
-    withTraceNode `Meta.injective (return m!"{exceptEmoji ·} {declName}") do
+    withTraceNode `Meta.injective (fun _ => return m!"{declName}") do
     let info ← getConstInfoInduct declName
     unless info.isUnsafe do
       -- We need to reset the local context here because `solveEqOfCtorEq` uses

src/Lean/Meta/LetToHave.lean

@@ -396,8 +396,8 @@ private partial def visitProj (e : Expr) (structName : Name) (idx : Nat) (struct
     return { expr := e.updateProj! struct, type? := lastFieldTy }
 
 private partial def visit (e : Expr) : M Result := do
-  withTraceNode `Meta.letToHave.debug (fun res =>
-      return m!"{if res.isOk then checkEmoji else crossEmoji} visit (check := {(← read).check}){indentExpr e}") do
+  withTraceNode `Meta.letToHave.debug (fun _ =>
+      return m!"visit (check := {(← read).check}){indentExpr e}") do
     match e with
     | .bvar .. => throwError "unexpected bound variable {e}"
     | .fvar .. => visitFVar e
@@ -415,8 +415,8 @@ end
 
 private def main (e : Expr) : MetaM Expr := do
   Prod.fst <$> withTraceNode `Meta.letToHave (fun
-      | .ok (_, msg) => pure m!"{checkEmoji} {msg}"
-      | .error ex => pure m!"{crossEmoji} {ex.toMessageData}") do
+      | .ok (_, msg) => pure msg
+      | .error ex => pure ex.toMessageData) do
     if hasDepLet e then
       withTrackingZetaDelta <|
       withTransparency TransparencyMode.all <|

src/Lean/Meta/LevelDefEq.lean

@@ -132,7 +132,7 @@ mutual
   partial def isLevelDefEqAuxImpl : Level → Level → MetaM Bool
     | Level.succ lhs, Level.succ rhs => isLevelDefEqAux lhs rhs
     | lhs, rhs =>
-      withTraceNode `Meta.isLevelDefEq (return m!"{exceptBoolEmoji ·} {lhs} =?= {rhs}") do
+      withTraceNode `Meta.isLevelDefEq (fun _ => return m!"{lhs} =?= {rhs}") do
       if lhs.getLevelOffset == rhs.getLevelOffset then
         return lhs.getOffset == rhs.getOffset
       else

src/Lean/Meta/Match/Match.lean

@@ -431,7 +431,7 @@ private def isCtorIdxHasNotBit? (e : Expr) : Option FVarId := do
 
 private partial def contradiction (mvarId : MVarId) : MetaM Bool := do
   mvarId.withContext do
-    withTraceNode `Meta.Match.match (msg := (return m!"{exceptBoolEmoji ·} Match.contradiction")) do
+    withTraceNode `Meta.Match.match (msg := (fun _ => return m!"Match.contradiction")) do
     trace[Meta.Match.match] m!"Match.contradiction:\n{mvarId}"
     if (← mvarId.contradictionCore {}) then
       trace[Meta.Match.match] "Contradiction found!"
@@ -937,7 +937,7 @@ private def processFirstVarDone (p : Problem) : Problem :=
 private def tracedForM (xs : Array α) (process : α → StateRefT State MetaM Unit) : StateRefT State MetaM Unit :=
   if xs.size > 1 then
     for x in xs, i in [:xs.size] do
-      withTraceNode `Meta.Match.match (msg := (return m!"{exceptEmoji ·} subgoal {i+1}/{xs.size}")) do
+      withTraceNode `Meta.Match.match (msg := (fun _ => return m!"subgoal {i+1}/{xs.size}")) do
         process x
   else
     for x in xs do

src/Lean/Meta/Match/Rewrite.lean

@@ -96,7 +96,7 @@ def rwMatcher (altIdx : Nat) (e : Expr) : MetaM Simp.Result := do
       return { expr := e }
     let eqnThm := eqns[altIdx]!
     try
-      withTraceNode `Meta.Match.debug (pure m!"{exceptEmoji ·} rewriting with {.ofConstName eqnThm} in{indentExpr e}") do
+      withTraceNode `Meta.Match.debug (fun _ => pure m!"rewriting with {.ofConstName eqnThm} in{indentExpr e}") do
       let eqProof := mkAppN (mkConst eqnThm e.getAppFn.constLevels!) e.getAppArgs
       let (hyps, _, eqType) ← forallMetaTelescope (← inferType eqProof)
       trace[Meta.Match.debug] "eqProof has type{indentExpr eqType}"

src/Lean/Meta/SplitSparseCasesOn.lean

@@ -28,7 +28,7 @@ public def reduceSparseCasesOn (mvarId : MVarId) : MetaM (Array MVarId) := do
   lhs.withApp fun f xs => do
   let .const matchDeclName _  := f | throwError "Not a const application"
   let some sparseCasesOnInfo ← getSparseCasesOnInfo matchDeclName | throwError "Not a sparse casesOn application"
-  withTraceNode `Meta.Match.matchEqs (msg := (return m!"{exceptEmoji ·} splitSparseCasesOn")) do
+  withTraceNode `Meta.Match.matchEqs (msg := (fun _ => return m!"splitSparseCasesOn")) do
   if xs.size < sparseCasesOnInfo.arity then
     throwError "Not enough arguments for sparse casesOn application"
   let majorIdx := sparseCasesOnInfo.majorPos
@@ -52,7 +52,7 @@ public def splitSparseCasesOn (mvarId : MVarId) : MetaM (Array MVarId) := do
   lhs.withApp fun f xs => do
   let .const matchDeclName _  := f | throwError "Not a const application"
   let some sparseCasesOnInfo ← getSparseCasesOnInfo matchDeclName | throwError "Not a sparse casesOn application"
-  withTraceNode `Meta.Match.matchEqs (msg := (return m!"{exceptEmoji ·} splitSparseCasesOn")) do
+  withTraceNode `Meta.Match.matchEqs (msg := (fun _ => return m!"splitSparseCasesOn")) do
   try
     trace[Meta.Match.matchEqs] "splitSparseCasesOn running on\n{mvarId}"
     if xs.size < sparseCasesOnInfo.arity then

src/Lean/Meta/Sym/Pattern.lean

@@ -17,6 +17,7 @@ import Lean.Meta.Sym.ProofInstInfo
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.Offset
 import Lean.Meta.Sym.Eta
+import Lean.Meta.AbstractMVars
 import Init.Data.List.MapIdx
 import Init.Data.Nat.Linear
 import Std.Do.Triple.Basic
@@ -260,6 +261,45 @@ public def mkEqPatternFromDecl (declName : Name) : MetaM (Pattern × Expr) := do
     let_expr Eq _ lhs rhs := type | throwError "conclusion is not a equality{indentExpr type}"
     return (lhs, rhs)
 
+/--
+Like `mkPatternCore` but takes a lambda expression instead of a forall type.
+Uses `lambdaBoundedTelescope` to open binders and detect instance/proof arguments.
+-/
+def mkPatternCoreFromLambda (lam : Expr) (levelParams : List Name)
+    (varTypes : Array Expr) (pattern : Expr) : MetaM Pattern := do
+  let fnInfos ← mkProofInstInfoMapFor pattern
+  let checkTypeMask := mkCheckTypeMask pattern varTypes.size
+  let checkTypeMask? := if checkTypeMask.all (· == false) then none else some checkTypeMask
+  let varInfos? ← lambdaBoundedTelescope lam varTypes.size fun xs _ =>
+    mkProofInstArgInfo? xs
+  return { levelParams, varTypes, pattern, fnInfos, varInfos?, checkTypeMask? }
+
+def mkPatternFromLambda (levelParams : List Name) (lam : Expr) : MetaM Pattern := do
+  let rec go (pattern : Expr) (varTypes : Array Expr) : MetaM Pattern := do
+    if let .lam _ d b _ := pattern then
+      return (← go b (varTypes.push d))
+    let pattern ← preprocessType pattern
+    mkPatternCoreFromLambda lam levelParams varTypes pattern
+  go lam #[]
+
+/--
+Creates a `Pattern` from an expression containing metavariables.
+
+Metavariables in `e` become pattern variables (wildcards). For example,
+`Nat.succ ?m` produces a pattern matching `Nat.succ _` with discrimination
+tree keys `[Nat.succ, *]`.
+
+This is used for user-registered simproc patterns where the user provides
+an expression with underscores (elaborated as metavariables) to specify
+what the simproc should match.
+-/
+public def mkSimprocPatternFromExpr (e : Expr) : MetaM Pattern := do
+  let result ← abstractMVars e
+  let levelParams := result.paramNames.mapIdx fun i _ => Name.num uvarPrefix i
+  let us := levelParams.toList.map mkLevelParam
+  let expr := result.expr.instantiateLevelParamsArray result.paramNames us.toArray
+  mkPatternFromLambda levelParams.toList expr
+
 structure UnifyM.Context where
   pattern   : Pattern
   unify     : Bool := true

src/Lean/Meta/SynthInstance.lean

@@ -351,8 +351,8 @@ def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext
   let localInsts ← getLocalInstances
   forallTelescopeReducing mvarType fun xs mvarTypeBody => do
     let { subgoals, instVal, instTypeBody } ← getSubgoals lctx localInsts xs inst
-    withTraceNode `Meta.synthInstance.tryResolve (withMCtx (← getMCtx) do
-        return m!"{exceptOptionEmoji ·} {← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
+    withTraceNode `Meta.synthInstance.tryResolve (fun _ => do withMCtx (← getMCtx) do
+        return m!"{← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
     if (← isDefEq mvarTypeBody instTypeBody) then
       /-
       We set `etaReduce := true`.
@@ -425,7 +425,7 @@ def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
     trace[Meta.synthInstance.answer] "{crossEmoji} {← instantiateMVars (← inferType cNode.mvar)}{Format.line}(size: {cNode.size} ≥ {(← read).maxResultSize})"
   else
     withTraceNode `Meta.synthInstance.answer
-      (fun _ => return m!"{checkEmoji} {← instantiateMVars (← inferType cNode.mvar)}") do
+      (fun _ => return m!"{← instantiateMVars (← inferType cNode.mvar)}") do
     let answer ← mkAnswer cNode
     -- Remark: `answer` does not contain assignable or assigned metavariables.
     let key := cNode.key
@@ -574,7 +574,7 @@ def generate : SynthM Unit := do
             return
     discard do withMCtx mctx do
       withTraceNode `Meta.synthInstance.apply
-        (return m!"{exceptOptionEmoji ·} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
+        (fun _ => return m!"apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
       modifyTop fun gNode => { gNode with currInstanceIdx := idx }
       if let some (mctx, subgoals) ← tryResolve mvar inst then
         consume { key, mvar, subgoals, mctx, size := 0 }
@@ -875,7 +875,7 @@ def synthInstanceCore? (type : Expr) (maxResultSize? : Option Nat := none) : Met
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
   withTraceNode `Meta.synthInstance
-    (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
+    (fun _ => return m!"{← instantiateMVars type}") do
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
                                           foApprox := true, ctxApprox := true, constApprox := false, univApprox := false }) do
   withInTypeClassResolution do

src/Lean/Meta/Tactic/Backtrack.lean

@@ -110,25 +110,25 @@ private def run (goals : List MVarId) (n : Nat) (curr acc : List MVarId) : MetaM
     cfg.proc goals curr
   catch e =>
     withTraceNode trace
-      (return m!"{exceptEmoji ·} BacktrackConfig.proc failed: {e.toMessageData}") do
+      (fun _ => return m!"BacktrackConfig.proc failed: {e.toMessageData}") do
     throw e
   match procResult? with
   | some curr' => run goals n curr' acc
   | none =>
   match curr with
   -- If there are no active goals, return the accumulated goals.
-  | [] => withTraceNode trace (return m!"{exceptEmoji ·} success!") do
+  | [] => withTraceNode trace (fun _ => return m!"success!") do
       return acc.reverse
   | g :: gs =>
   -- Discard any goals which have already been assigned.
   if ← g.isAssigned then
-    withTraceNode trace (return m!"{exceptEmoji ·} discarding already assigned goal {g}") do
+    withTraceNode trace (fun _ => return m!"discarding already assigned goal {g}") do
       run goals (n+1) gs acc
   else
   withTraceNode trace
     -- Note: the `addMessageContextFull` ensures we show the goal using the mvar context before
     -- the `do` block below runs, potentially unifying mvars in the goal.
-    (return m!"{exceptEmoji ·} working on: {← addMessageContextFull g}")
+    (fun _ => return m!"working on: {← addMessageContextFull g}")
     do
       -- Check if we should suspend the search here:
       if (← cfg.suspend g) then

src/Lean/Meta/Tactic/Cbv.lean

@@ -16,5 +16,6 @@ namespace Lean
 
 builtin_initialize registerTraceClass `Meta.Tactic.cbv
 builtin_initialize registerTraceClass `Debug.Meta.Tactic.cbv
+builtin_initialize registerTraceClass `Debug.Meta.Tactic.cbv.simprocs (inherited := true)
 
 end Lean

src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/Array.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+import Lean.Meta.Sym.Simp.SimpM
+import Lean.Meta.Sym.LitValues
+import Lean.Meta.Sym.InferType
+import Init.CbvSimproc
+import Lean.Meta.Tactic.Cbv.CbvSimproc
+import Lean.Meta.Tactic.Cbv.Util
+import Init.GetElem
+
+namespace Lean.Meta.Tactic.Cbv
+
+/-- Extract elements from an array literal (`Array.mk` applied to a list literal). -/
+private def getArrayLitElems? (e : Expr) : Option <| Array Expr :=
+  match_expr e with
+  | Array.mk _ as => getListLitElems as
+  | _ => none
+
+/-- Reduce `#[...][n]` for literal arrays and literal `Nat` indices. -/
+builtin_cbv_simproc cbv_eval simpArrayGetElem (@GetElem.getElem (Array _) Nat _ _ _ _ _ _) := fun e => do
+  let_expr GetElem.getElem _ _ _ _ _ xs n _ := e | return .rfl
+  let some elems := getArrayLitElems? xs | return .rfl
+  let some idx := Sym.getNatValue? n | return .rfl
+  if h : idx < elems.size then
+    let result := elems[idx]
+    return .step result (← Sym.mkEqRefl result)
+  else
+    return .rfl
+
+/-- Reduce `#[...][n]?` for literal arrays and literal `Nat` indices. -/
+builtin_cbv_simproc cbv_eval simpArrayGetElem? (@GetElem?.getElem? (Array _) Nat _ _ _ _ _) := fun e => do
+  let_expr GetElem?.getElem? _ _ α _ _ xs n := e | return .rfl
+  let some elems := getArrayLitElems? xs | return .rfl
+  let some idx := Sym.getNatValue? n | return .rfl
+  let sortLevel ← Sym.getLevel α
+  let .succ u := sortLevel | return .rfl
+  let result ←
+    if h : idx < elems.size then
+      Sym.share <| mkApp2 (mkConst ``Option.some [u]) α elems[idx]
+    else
+      Sym.share <| mkApp (mkConst ``Option.none [u]) α
+  return .step result (← Sym.mkEqRefl result)
+
+end Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/Core.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+prelude
+import Lean.Meta.Sym.Simp.SimpM
+import Init.Sym.Lemmas
+import Init.CbvSimproc
+import Lean.Meta.Tactic.Cbv.CbvSimproc
+
+namespace Lean.Meta.Sym.Simp
+
+/-- Short-circuit evaluation of `Or`. Simplifies only the left argument;
+if it reduces to `True`, returns `True` immediately without evaluating the right side. -/
+builtin_cbv_simproc ↓ simpOr (@Or _ _) := fun e => do
+  let_expr Or a b := e | return .rfl
+  match (← simp a) with
+  | .rfl _ =>
+    if (← isTrueExpr a) then
+      return .step (← getTrueExpr) (mkApp (mkConst ``true_or) b) (done := true)
+    else if (← isFalseExpr a) then
+      return .step b (mkApp (mkConst ``false_or) b)
+    else
+      return .rfl
+  | .step a' ha _ =>
+    if (← isTrueExpr a') then
+      return .step (← getTrueExpr) (mkApp (e.replaceFn ``Sym.or_eq_true_left) ha) (done := true)
+    else if (← isFalseExpr a') then
+      return .step b (mkApp (e.replaceFn ``Sym.or_eq_right) ha)
+    else
+      return .rfl
+
+/-- Short-circuit evaluation of `And`. Simplifies only the left argument;
+if it reduces to `False`, returns `False` immediately without evaluating the right side. -/
+builtin_cbv_simproc ↓ simpAnd (@And _ _) := fun e => do
+  let_expr And a b := e | return .rfl
+  match (← simp a) with
+  | .rfl _ =>
+    if (← isFalseExpr a) then
+      return .step (← getFalseExpr) (mkApp (mkConst ``false_and) b) (done := true)
+    else if (← isTrueExpr a) then
+      return .step b (mkApp (mkConst ``true_and) b)
+    else
+      return .rfl
+  | .step a' ha _ =>
+    if (← isFalseExpr a') then
+      return .step (← getFalseExpr) (mkApp (e.replaceFn ``Sym.and_eq_false_left) ha) (done := true)
+    else if (← isTrueExpr a') then
+      return .step b (mkApp (e.replaceFn ``Sym.and_eq_left) ha)
+    else
+      return .rfl
+
+end Lean.Meta.Sym.Simp

src/Lean/Meta/Tactic/Cbv/BuiltinCbvSimprocs/String.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+import Lean.Meta.Sym.Simp.SimpM
+import Lean.Meta.Sym.LitValues
+import Init.CbvSimproc
+import Lean.Meta.Tactic.Cbv.CbvSimproc
+import Lean.Meta.Tactic.Cbv.Util
+
+namespace Lean.Meta.Tactic.Cbv
+
+/-- Reduce `"abc" ++ "def"` to `"abcdef"` for literal strings. -/
+builtin_cbv_simproc cbv_eval simpStringAppend (@HAppend.hAppend String String String _ _ _) := fun e => do
+  let some a := Sym.getStringValue? e.appFn!.appArg! | return .rfl
+  let some b := Sym.getStringValue? e.appArg! | return .rfl
+  let result ← Sym.share <| toExpr (a ++ b)
+  return .step result (← Sym.mkEqRefl result)
+
+/-- Reduce `String.push "abc" 'd'` to `"abcd"` for literal strings and chars. -/
+builtin_cbv_simproc cbv_eval simpStringPush (String.push _ _) := fun e => do
+  let some s := Sym.getStringValue? e.appFn!.appArg! | return .rfl
+  let some c := Sym.getCharValue? e.appArg! | return .rfl
+  let result ← Sym.share <| toExpr (s.push c)
+  return .step result (← Sym.mkEqRefl result)
+
+/-- Reduce `String.singleton 'a'` to `"a"` for literal chars. -/
+builtin_cbv_simproc cbv_eval simpStringSingleton (String.singleton _) := fun e => do
+  let some c := Sym.getCharValue? e.appArg! | return .rfl
+  let result ← Sym.share <| toExpr (String.singleton c)
+  return .step result (← Sym.mkEqRefl result)
+
+/-- Reduce `String.ofList ['a', 'b', 'c']` to `"abc"` for literal char lists. -/
+builtin_cbv_simproc cbv_eval simpStringOfList (String.ofList _) := fun e => do
+  let some elems := getListLitElems e.appArg! | return .rfl
+  let mut s := ""
+  for elem in elems do
+    let some c := Sym.getCharValue? elem | return .rfl
+    s := s.push c
+  let result ← Sym.share <| toExpr s
+  return .step result (← Sym.mkEqRefl result)
+
+/-- Reduce `String.toList "abc"` to `['a', 'b', 'c']` for literal strings. -/
+builtin_cbv_simproc cbv_eval simpStringToList (String.toList _) := fun e => do
+  let some s := Sym.getStringValue? e.appArg! | return .rfl
+  let result ← Sym.share <| toExpr s.toList
+  return .step result (← Sym.mkEqRefl result)
+
+end Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/Cbv/CbvEvalExt.lean

@@ -35,11 +35,13 @@ open Lean.Meta.Sym.Simp
 
 /--
   Entry of the `CbvEvalExtension`.
-  Consists of the precomputed `Theorem` object and a name of the head function appearing on the left-hand side of the theorem.
+  Consists of name of the theorem used, the precomputed `Theorem` object 
+  and a name of the head function appearing on the left-hand side of the theorem.
 -/
 structure CbvEvalEntry where
-  appFn : Name
-  thm  : Theorem
+  origin : Name
+  appFn  : Name
+  thm    : Theorem
   deriving BEq, Inhabited
 
 /-- Create a `CbvEvalEntry` from a theorem declaration. When `inv = true`, creates an
@@ -62,15 +64,38 @@ def mkCbvTheoremFromConst (declName : Name) (inv : Bool := false) : MetaM CbvEva
       thmDeclName ← mkAuxLemma (kind? := `_cbv_eval) cinfo.levelParams invType invVal
     return (constName, thmDeclName)
   let thm ← mkTheoremFromDecl thmDeclName
-  return ⟨fnName, thm⟩
+  return ⟨declName, fnName, thm⟩
 
 structure CbvEvalState where
-  lemmas : NameMap Theorems := {}
+  lemmas  : NameMap Theorems := {}
+  entries : NameMap <| Array CbvEvalEntry := {}
   deriving Inhabited
 
 def CbvEvalState.addEntry (s : CbvEvalState) (e : CbvEvalEntry) : CbvEvalState :=
-  let existing := (s.lemmas.find? e.appFn).getD {}
-  { s with lemmas := s.lemmas.insert e.appFn (existing.insert e.thm) }
+  let lemmas := (s.lemmas.find? e.appFn).getD {}
+  let entries := (s.entries.find? e.appFn).getD {}
+  { s with
+    lemmas  := s.lemmas.insert e.appFn (lemmas.insert e.thm)
+    entries := s.entries.insert e.appFn <| entries.push e}
+
+/-- Rebuild the `Theorems` for a given `appFn` from the entries that target it. -/
+private def CbvEvalState.rebuildLemmas (entries : NameMap <| Array CbvEvalEntry) (appFn : Name) (lemmas : NameMap Theorems) : NameMap Theorems := 
+  let appFnEntries := entries.getD appFn #[] 
+  if appFnEntries.isEmpty then
+    lemmas.erase appFn
+  else
+    lemmas.insert appFn (appFnEntries.foldl (fun thms e => thms.insert e.thm) {})
+
+/-- Erase a theorem from the state. Returns `none` if the theorem is not found. -/
+def CbvEvalState.erase (s : CbvEvalState) (declName : Name) : Option CbvEvalState := do
+  let (appFn, oldEntries) ← s.entries.foldl (init := none) fun acc appFn entries =>
+    if acc.isSome then acc
+    else if entries.any (·.origin == declName) then some (appFn, entries)
+    else none
+  let newEntries := oldEntries.filter (·.origin != declName)
+  let entries := if newEntries.isEmpty then s.entries.erase appFn
+    else s.entries.insert appFn newEntries
+  return { lemmas := rebuildLemmas entries appFn s.lemmas, entries }
 
 abbrev CbvEvalExtension := SimpleScopedEnvExtension CbvEvalEntry CbvEvalState
 
@@ -99,6 +124,11 @@ builtin_initialize
       let inv := !stx[1].isNone
       let (entry, _) ← MetaM.run (mkCbvTheoremFromConst lemmaName (inv := inv)) {}
       cbvEvalExt.add entry kind
+    erase := fun declName => do
+      let s := cbvEvalExt.getState (← getEnv)
+      match s.erase declName with
+      | some s' => modifyEnv fun env => cbvEvalExt.modifyState env fun _ => s'
+      | none => logWarning m!"`{.ofConstName declName}` does not have the `[cbv_eval]` attribute"
   }
 
 end Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/Cbv/CbvSimproc.lean

@@ -0,0 +1,274 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+prelude
+public import Lean.Compiler.InitAttr
+public import Lean.ScopedEnvExtension
+public import Lean.Meta.Sym.Simp.SimpM
+public import Lean.Meta.Sym.Simp.Result
+public import Lean.Meta.Sym.Simp.App
+public import Lean.Meta.Sym.Simp.DiscrTree
+public import Lean.Meta.Sym.Pattern
+
+public section
+namespace Lean.Meta.Tactic.Cbv
+open Lean.Meta.Sym
+open Lean.Meta.Sym.Simp
+
+/--
+The phase at which a `cbv_simproc` fires during cbv normalization.
+
+- `pre` (`↓`): Fires on each subexpression *before* cbv reduction, so arguments are still
+  unreduced. Runs before cbv-specific pre-steps (projection reduction, unfolding, etc.).
+- `eval` (`cbv_eval`): Fires during the post phase, after ground evaluation but *before*
+  `handleApp` attempts equation lemmas, unfolding, and recursion reduction.
+  Arguments have already been reduced.
+- `post` (`↑`, default): Fires during the post phase, *after* `handleApp` has attempted
+  standard reduction. Arguments have already been reduced.
+-/
+inductive CbvSimprocPhase where
+  | pre | eval | post
+  deriving Inhabited, BEq, Hashable, Repr
+
+instance : ToExpr CbvSimprocPhase where
+  toExpr
+    | .pre  => mkConst ``CbvSimprocPhase.pre
+    | .eval => mkConst ``CbvSimprocPhase.eval
+    | .post => mkConst ``CbvSimprocPhase.post
+  toTypeExpr := mkConst ``CbvSimprocPhase
+
+structure CbvSimprocOLeanEntry where
+  declName : Name
+  phase    : CbvSimprocPhase := .post
+  keys     : Array DiscrTree.Key := #[]
+  deriving Inhabited
+
+structure CbvSimprocEntry extends CbvSimprocOLeanEntry where
+  proc : Simproc
+
+instance : BEq CbvSimprocEntry where
+  beq e₁ e₂ := e₁.declName == e₂.declName
+
+instance : ToFormat CbvSimprocEntry where
+  format e := format e.declName
+
+structure CbvSimprocs where
+  pre          : DiscrTree CbvSimprocEntry := {}
+  eval         : DiscrTree CbvSimprocEntry := {}
+  post         : DiscrTree CbvSimprocEntry := {}
+  simprocNames : PHashSet Name := {}
+  erased       : PHashSet Name := {}
+  deriving Inhabited
+
+def CbvSimprocs.addCore (s : CbvSimprocs) (keys : Array DiscrTree.Key) (declName : Name)
+    (phase : CbvSimprocPhase) (proc : Simproc) : CbvSimprocs :=
+  let entry : CbvSimprocEntry := { declName, phase, keys, proc }
+  let s := { s with simprocNames := s.simprocNames.insert declName, erased := s.erased.erase declName }
+  match phase with
+  | .pre  => { s with pre  := s.pre.insertKeyValue keys entry }
+  | .eval => { s with eval := s.eval.insertKeyValue keys entry }
+  | .post => { s with post := s.post.insertKeyValue keys entry }
+
+def CbvSimprocs.erase (s : CbvSimprocs) (declName : Name) : CbvSimprocs :=
+  { s with erased := s.erased.insert declName, simprocNames := s.simprocNames.erase declName }
+
+structure BuiltinCbvSimprocs where
+  keys  : Std.HashMap Name (Array DiscrTree.Key) := {}
+  procs : Std.HashMap Name Simproc := {}
+  deriving Inhabited
+
+builtin_initialize builtinCbvSimprocDeclsRef : IO.Ref BuiltinCbvSimprocs ← IO.mkRef {}
+
+def registerBuiltinCbvSimproc (declName : Name)
+    (keys : Array DiscrTree.Key) (proc : Simproc) : IO Unit := do
+  unless (← initializing) do
+    throw (IO.userError s!"Invalid builtin cbv simproc declaration: \
+      It can only be registered during initialization")
+  if (← builtinCbvSimprocDeclsRef.get).keys.contains declName then
+    throw (IO.userError s!"Invalid builtin cbv simproc declaration \
+      `{privateToUserName declName}`: It has already been declared")
+  builtinCbvSimprocDeclsRef.modify fun { keys := ks, procs } =>
+    { keys := ks.insert declName keys, procs := procs.insert declName proc }
+
+structure CbvSimprocDecl where
+  declName : Name
+  keys     : Array DiscrTree.Key
+  deriving Inhabited
+
+def CbvSimprocDecl.lt (d₁ d₂ : CbvSimprocDecl) : Bool :=
+  Name.quickLt d₁.declName d₂.declName
+
+structure CbvSimprocDeclExtState where
+  builtin    : Std.HashMap Name (Array DiscrTree.Key)
+  newEntries : PHashMap Name (Array DiscrTree.Key) := {}
+  deriving Inhabited
+
+builtin_initialize cbvSimprocDeclExt :
+    PersistentEnvExtension CbvSimprocDecl CbvSimprocDecl CbvSimprocDeclExtState ←
+  registerPersistentEnvExtension {
+    mkInitial       := return { builtin := (← builtinCbvSimprocDeclsRef.get).keys }
+    addImportedFn   := fun _ => return { builtin := (← builtinCbvSimprocDeclsRef.get).keys }
+    addEntryFn      := fun s d =>
+      { s with newEntries := s.newEntries.insert d.declName d.keys }
+    exportEntriesFn := fun s =>
+      let result := s.newEntries.foldl (init := #[]) fun result declName keys =>
+        result.push { declName, keys }
+      result.qsort CbvSimprocDecl.lt
+  }
+
+def getCbvSimprocDeclKeys? (declName : Name) : CoreM (Option (Array DiscrTree.Key)) := do
+  let env ← getEnv
+  let keys? ← match env.getModuleIdxFor? declName with
+    | some modIdx => do
+      let some decl :=
+        (cbvSimprocDeclExt.getModuleEntries env modIdx).binSearch { declName, keys := #[] } CbvSimprocDecl.lt
+        | pure none
+      pure (some decl.keys)
+    | none => pure ((cbvSimprocDeclExt.getState env).newEntries.find? declName)
+  if let some keys := keys? then
+    return some keys
+  else
+    return (cbvSimprocDeclExt.getState env).builtin[declName]?
+
+def isCbvSimproc (declName : Name) : CoreM Bool :=
+  return (← getCbvSimprocDeclKeys? declName).isSome
+
+def isBuiltinCbvSimproc (declName : Name) : CoreM Bool := do
+  return (cbvSimprocDeclExt.getState (← getEnv)).builtin.contains declName
+
+def registerCbvSimproc (declName : Name) (keys : Array DiscrTree.Key) : CoreM Unit := do
+  let env ← getEnv
+  unless (env.getModuleIdxFor? declName).isNone do
+    throwError "Invalid cbv simproc declaration `{.ofConstName declName}`: \
+      It is declared in an imported module"
+  if (← isCbvSimproc declName) then
+    throwError "Invalid cbv simproc declaration `{.ofConstName declName}`: \
+      It has already been declared"
+  modifyEnv fun env => cbvSimprocDeclExt.modifyState env fun s =>
+    { s with newEntries := s.newEntries.insert declName keys }
+
+abbrev CbvSimprocExtension := ScopedEnvExtension CbvSimprocOLeanEntry CbvSimprocEntry CbvSimprocs
+
+unsafe def getCbvSimprocFromDeclImpl (declName : Name) : ImportM Simproc := do
+  let ctx ← read
+  match ctx.env.find? declName with
+  | none      => throw <| IO.userError ("Unknown constant `" ++ toString declName ++ "`")
+  | some info =>
+    match info.type with
+    | .const ``Simproc _ =>
+      IO.ofExcept <| ctx.env.evalConst Simproc ctx.opts declName
+    | _ => throw <| IO.userError s!"Cbv simproc `{privateToUserName declName}` has an \
+        unexpected type: Expected `Simproc`, but found `{info.type}`"
+
+@[implemented_by getCbvSimprocFromDeclImpl]
+opaque getCbvSimprocFromDecl (declName : Name) : ImportM Simproc
+
+def toCbvSimprocEntry (e : CbvSimprocOLeanEntry) : ImportM CbvSimprocEntry := do
+  return { toCbvSimprocOLeanEntry := e, proc := (← getCbvSimprocFromDecl e.declName) }
+
+builtin_initialize builtinCbvSimprocsRef : IO.Ref CbvSimprocs ← IO.mkRef {}
+
+builtin_initialize cbvSimprocExtension : CbvSimprocExtension ←
+  registerScopedEnvExtension {
+    name         := `cbvSimprocExt
+    mkInitial    := builtinCbvSimprocsRef.get
+    ofOLeanEntry := fun _ => toCbvSimprocEntry
+    toOLeanEntry := fun e => e.toCbvSimprocOLeanEntry
+    addEntry     := fun s e => s.addCore e.keys e.declName e.phase e.proc
+  }
+
+def eraseCbvSimprocAttr (declName : Name) : AttrM Unit := do
+  let s := cbvSimprocExtension.getState (← getEnv)
+  unless s.simprocNames.contains declName do
+    throwError "`{.ofConstName declName}` does not have a [cbv_simproc] attribute"
+  modifyEnv fun env => cbvSimprocExtension.modifyState env fun s => s.erase declName
+
+def addCbvSimprocAttrCore (declName : Name) (kind : AttributeKind)
+    (phase : CbvSimprocPhase) : CoreM Unit := do
+  let proc ← getCbvSimprocFromDecl declName
+  let some keys ← getCbvSimprocDeclKeys? declName |
+    throwError "Invalid `[cbv_simproc]` attribute: \
+      `{.ofConstName declName}` is not a cbv simproc"
+  cbvSimprocExtension.add { declName, phase, keys, proc } kind
+
+def parseCbvSimprocPhase (stx : Syntax) : CbvSimprocPhase :=
+  if stx.isNone then .post
+  else
+    let inner := stx[0]
+    if inner.getKind == `Lean.Parser.Tactic.simpPre then .pre
+    else if inner.getKind == `Lean.Parser.cbvSimprocEval then .eval
+    else .post
+
+def addCbvSimprocAttr (declName : Name) (stx : Syntax)
+    (attrKind : AttributeKind) : AttrM Unit := do
+  ensureAttrDeclIsMeta `cbvSimprocAttr declName attrKind
+  let go : MetaM Unit := do
+    addCbvSimprocAttrCore declName attrKind (parseCbvSimprocPhase stx[1])
+  discard <| go.run {} {}
+
+def addCbvSimprocBuiltinAttrCore (ref : IO.Ref CbvSimprocs) (declName : Name)
+    (phase : CbvSimprocPhase) (proc : Simproc) : IO Unit := do
+  let some keys := (← builtinCbvSimprocDeclsRef.get).keys[declName]? |
+    throw (IO.userError s!"Invalid `[builtin_cbv_simproc]` attribute: \
+      `{privateToUserName declName}` is not a builtin cbv simproc")
+  ref.modify fun s => s.addCore keys declName phase proc
+
+def addCbvSimprocBuiltinAttr (declName : Name) (phase : CbvSimprocPhase)
+    (proc : Simproc) : IO Unit :=
+  addCbvSimprocBuiltinAttrCore builtinCbvSimprocsRef declName phase proc
+
+private def addBuiltinCbvSimproc (declName : Name) (stx : Syntax) : AttrM Unit := do
+  let go : MetaM Unit := do
+    let phase := parseCbvSimprocPhase stx[1]
+    let val := mkAppN (mkConst ``addCbvSimprocBuiltinAttr)
+      #[toExpr declName, toExpr phase, mkConst declName]
+    let initDeclName ← mkFreshUserName (declName ++ `declare)
+    declareBuiltin initDeclName val
+  go.run' {}
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `cbvSimprocAttr
+    descr           := "Cbv simplification procedure"
+    applicationTime := AttributeApplicationTime.afterCompilation
+    add             := fun declName stx attrKind => addCbvSimprocAttr declName stx attrKind
+    erase           := fun declName => eraseCbvSimprocAttr declName
+  }
+
+builtin_initialize
+  registerBuiltinAttribute {
+    ref             := by exact decl_name%
+    name            := `cbvSimprocBuiltinAttr
+    descr           := "Builtin cbv simplification procedure"
+    applicationTime := AttributeApplicationTime.afterCompilation
+    erase           := fun _ => throwError "Not implemented yet, [-builtin_cbv_simproc]"
+    add             := fun declName stx _ => addBuiltinCbvSimproc declName stx
+  }
+
+def getCbvSimprocs : CoreM CbvSimprocs :=
+  return cbvSimprocExtension.getState (← getEnv)
+
+def cbvSimprocDispatch (tree : DiscrTree CbvSimprocEntry)
+    (erased : PHashSet Name) : Simproc := fun e => do
+  let candidates := Sym.getMatchWithExtra tree e
+  if candidates.isEmpty then
+    trace[Debug.Meta.Tactic.cbv.simprocs] "no cbv simprocs found for {e}"
+    return .rfl
+  for (entry, numExtra) in candidates do
+    unless erased.contains entry.declName do
+      let result ← if numExtra == 0 then
+        entry.proc e
+      else
+        simpOverApplied e numExtra entry.proc
+      if result matches .step _ _ _ then
+        trace[Debug.Meta.Tactic.cbv.simprocs] "cbv simproc `{entry.declName}` result {e} => {result.getResultExpr e}"
+        return result
+      if result matches .rfl (done := true) then
+        return result
+  return .rfl
+
+end Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/Cbv/ControlFlow.lean

@@ -21,6 +21,8 @@ import Lean.Meta.Tactic.Cbv.TheoremsLookup
 import Lean.Meta.Tactic.Cbv.Opaque
 import Lean.Meta.Tactic.Cbv.CbvEvalExt
 import Lean.Compiler.NoncomputableAttr
+import Init.CbvSimproc
+import Lean.Meta.Tactic.Cbv.CbvSimproc
 
 /-!
 # Control Flow Handling for Cbv
@@ -81,7 +83,7 @@ def simpAndMatchIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback
 
 /-- Like `simpIte` but also evaluates `Decidable.decide` when the condition does not
 reduce to `True`/`False` directly. -/
-public def simpIteCbv : Simproc := fun e => do
+builtin_cbv_simproc ↓ simpIteCbv (@ite _ _ _ _ _) := fun e => do
   let numArgs := e.getAppNumArgs
   if numArgs < 5 then return .rfl (done := true)
   propagateOverApplied e (numArgs - 5) fun e => do
@@ -149,7 +151,7 @@ def simpAndMatchDIteDecidableCongr (f α c inst a b c' h inst' : Expr) (fallback
 
 /-- Like `simpDIte` but also evaluates `Decidable.decide` when the condition does not
 reduce to `True`/`False` directly. -/
-public def simpDIteCbv : Simproc := fun e => do
+builtin_cbv_simproc ↓ simpDIteCbv (@dite _ _ _ _ _) := fun e => do
   let numArgs := e.getAppNumArgs
   if numArgs < 5 then return .rfl (done := true)
   propagateOverApplied e (numArgs - 5) fun e => do
@@ -187,46 +189,6 @@ public def simpDIteCbv : Simproc := fun e => do
             let h' := mkApp3 (e.replaceFn ``Sym.dite_cond_congr) c' inst' h
             return .step e' h' (done := true)
 
-/-- Short-circuit evaluation of `Or`. Simplifies only the left argument;
-if it reduces to `True`, returns `True` immediately without evaluating the right side. -/
-public def simpOr : Simproc := fun e => do
-  let_expr Or a b := e | return .rfl
-  match (← simp a) with
-  | .rfl _ =>
-    if (← isTrueExpr a) then
-      return .step (← getTrueExpr) (mkApp (mkConst ``true_or) b) (done := true)
-    else if (← isFalseExpr a) then
-      return .step b (mkApp (mkConst ``false_or) b)
-    else
-      return .rfl
-  | .step a' ha _ =>
-    if (← isTrueExpr a') then
-      return .step (← getTrueExpr) (mkApp (e.replaceFn ``Sym.or_eq_true_left) ha) (done := true)
-    else if (← isFalseExpr a') then
-      return .step b (mkApp (e.replaceFn ``Sym.or_eq_right) ha)
-    else
-      return .rfl
-
-/-- Short-circuit evaluation of `And`. Simplifies only the left argument;
-if it reduces to `False`, returns `False` immediately without evaluating the right side. -/
-public def simpAnd : Simproc := fun e => do
-  let_expr And a b := e | return .rfl
-  match (← simp a) with
-  | .rfl _ =>
-    if (← isFalseExpr a) then
-      return .step (← getFalseExpr) (mkApp (mkConst ``false_and) b) (done := true)
-    else if (← isTrueExpr a) then
-      return .step b (mkApp (mkConst ``true_and) b)
-    else
-      return .rfl
-  | .step a' ha _ =>
-    if (← isFalseExpr a') then
-      return .step (← getFalseExpr) (mkApp (e.replaceFn ``Sym.and_eq_false_left) ha) (done := true)
-    else if (← isTrueExpr a') then
-      return .step b (mkApp (e.replaceFn ``Sym.and_eq_left) ha)
-    else
-      return .rfl
-
 /-- Reduce `decide` by matching the `Decidable` instance for `isTrue`/`isFalse`. -/
 def matchDecideDecidable (p inst instToMatch : Expr) (fallback : SimpM Result) : SimpM Result := do
   match_expr instToMatch with
@@ -264,7 +226,7 @@ corresponding boolean directly. Otherwise, simplifies the `Decidable` instance a
 on `isTrue`/`isFalse` to determine the boolean value. When `p` simplified to a new `p'`
 but the instance doesn't reduce to `isTrue`/`isFalse`, falls back to rebuilding
 `decide p'` with a congruence proof. -/
-public def simpDecideCbv : Simproc := fun e => do
+builtin_cbv_simproc ↓ simpDecideCbv (@Decidable.decide _ _) := fun e => do
   let numArgs := e.getAppNumArgs
   if numArgs < 2 then return .rfl (done := true)
   propagateOverApplied e (numArgs - 2) fun e => do
@@ -320,9 +282,7 @@ public def withCbvOpaqueGuard (x : MetaM α) : MetaM α := do
         else return false
   ) x
 
-def tryMatchEquations (appFn : Name) : Simproc := fun e => do
-  let thms ← getMatchTheorems appFn
-  thms.rewrite (d := dischargeNone) e
+builtin_cbv_simproc ↓ simpCbvCond (@cond _ _ _) := simpCond
 
 public def reduceRecMatcher : Simproc := fun e => do
   if let some e' ← withCbvOpaqueGuard <| reduceRecMatcher? e then
@@ -330,7 +290,16 @@ public def reduceRecMatcher : Simproc := fun e => do
   else
     return .rfl
 
-def tryMatcher : Simproc := fun e => do
+builtin_cbv_simproc ↓ simpDecidableRec (@Decidable.rec _ _ _ _ _) := 
+  (simpInterlaced · #[false,false,false,false,true]) >> reduceRecMatcher
+
+def tryMatchEquations (appFn : Name) : Simproc := fun e => do
+  let thms ← getMatchTheorems appFn
+  thms.rewrite (d := dischargeNone) e
+
+/-- Dispatch control flow constructs to their specialized simprocs.
+Precondition: `e` is an application. -/
+public def tryMatcher : Simproc := fun e => do
   unless e.isApp do
     return .rfl
   let some appFn := e.getAppFn.constName? | return .rfl
@@ -342,26 +311,4 @@ def tryMatcher : Simproc := fun e => do
       <|> reduceRecMatcher
         <| e
 
-/-- Dispatch control flow constructs to their specialized simprocs.
-Precondition: `e` is an application. -/
-public def simpControlCbv : Simproc := fun e => do
-  let .const declName _ := e.getAppFn | return .rfl
-  if declName == ``ite then
-    simpIteCbv e
-  else if declName == ``cond then
-    simpCond e
-  else if declName == ``dite then
-    simpDIteCbv e
-  else if declName == ``Decidable.rec then
-    -- We force the rewrite in the last argument, so that we can unfold the `Decidable` instance.
-    (simpInterlaced · #[false,false,false,false,true]) >> reduceRecMatcher <| e
-  else if declName == ``Or then
-    simpOr e
-  else if declName == ``And then
-    simpAnd e
-  else if declName == ``Decidable.decide then
-    simpDecideCbv e
-  else
-    tryMatcher e
-
 end Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/Cbv/Main.lean

@@ -10,9 +10,13 @@ prelude
 public import Lean.Meta.Sym.Simp.SimpM
 public import Lean.Meta.Tactic.Cbv.Opaque
 public import Lean.Meta.Tactic.Cbv.ControlFlow
+import Lean.Meta.Tactic.Cbv.BuiltinCbvSimprocs.Core
+import Lean.Meta.Tactic.Cbv.BuiltinCbvSimprocs.Array
+import Lean.Meta.Tactic.Cbv.BuiltinCbvSimprocs.String
 import Lean.Meta.Tactic.Cbv.Util
 import Lean.Meta.Tactic.Cbv.TheoremsLookup
 import Lean.Meta.Tactic.Cbv.CbvEvalExt
+import Lean.Meta.Tactic.Cbv.CbvSimproc
 import Lean.Meta.Sym
 import Lean.Meta.Tactic.Refl
 import Lean.Meta.Tactic.Replace
@@ -262,7 +266,7 @@ def cbvPreStep : Simproc := fun e => do
   | .lit .. => foldLit e
   | .proj .. => handleProj e
   | .const .. => isOpaqueConst >> handleConst <| e
-  | .app .. => simpControlCbv <|> simplifyAppFn <| e
+  | .app .. => tryMatcher <|> simplifyAppFn <| e
   | .letE .. =>
     if e.letNondep! then
       let betaAppResult ← toBetaApp e
@@ -272,22 +276,30 @@ def cbvPreStep : Simproc := fun e => do
   | .forallE .. | .lam .. | .fvar .. | .mvar .. | .bvar .. | .sort .. => return .rfl (done := true)
   | _ => return .rfl
 
-/-- Pre-pass: skip builtin values and proofs, then dispatch structurally. -/
-def cbvPre : Simproc := isBuiltinValue <|> isProofTerm <|> cbvPreStep
+/-- Pre-pass: skip builtin values and proofs, run pre simprocs, then dispatch structurally. -/
+def cbvPre (simprocs : CbvSimprocs) : Simproc :=
+  isBuiltinValue <|> isProofTerm <|> cbvSimprocDispatch simprocs.pre simprocs.erased <|> cbvPreStep
 
-/-- Post-pass: evaluate ground arithmetic, then try unfolding/beta-reducing applications. -/
-def cbvPost : Simproc := evalGround <|> handleApp
+/-- Post-pass: evaluate ground arithmetic, then try eval simprocs, then try unfolding/beta-reducing applications and finally run post simprocs -/
+def cbvPost (simprocs : CbvSimprocs) : Simproc :=
+  evalGround <|> cbvSimprocDispatch simprocs.eval simprocs.erased <|> handleApp <|> cbvSimprocDispatch simprocs.post simprocs.erased
 
-def cbvCore (e : Expr) (config : Sym.Simp.Config := {}) : Sym.SymM Result :=
-  SimpM.run' (methods := {pre := cbvPre, post := cbvPost}) (config := config)
+def mkCbvMethods (simprocs : CbvSimprocs) : Methods :=
+  { pre := cbvPre simprocs, post := cbvPost simprocs }
+
+def cbvCore (e : Expr) (config : Sym.Simp.Config := {}) : Sym.SymM Result := do
+  let simprocs ← getCbvSimprocs
+  let methods := mkCbvMethods simprocs
+  SimpM.run' (methods := methods) (config := config)
     <| simp e
 
 /-- Reduce a single expression. Unfolds reducibles, shares subterms, then runs the
 simplifier with `cbvPre`/`cbvPost`. Used by `conv => cbv`. -/
 public def cbvEntry (e : Expr) : MetaM Result := do
   trace[Meta.Tactic.cbv] "Called cbv tactic to simplify {e}"
+  let simprocs ← getCbvSimprocs
   let config : Sym.Simp.Config := { maxSteps := cbv.maxSteps.get (← getOptions) }
-  let methods := {pre := cbvPre, post := cbvPost}
+  let methods := mkCbvMethods simprocs
   let e ← Sym.unfoldReducible e
   Sym.SymM.run do
     let e ← Sym.shareCommon e

src/Lean/Meta/Tactic/Cbv/Util.lean

@@ -101,4 +101,11 @@ def isProof (e : Expr) : Sym.SymM Bool := do
 public def isProofTerm : Simproc := fun e => do
   return .rfl (← isProof e)
 
+/-- Extract elements from a `List.cons`/`List.nil` chain. -/
+public partial def getListLitElems (e : Expr) (acc : Array Expr := #[]) : Option <| Array Expr :=
+  match_expr e with
+  | List.nil _ => some acc
+  | List.cons _ a as => getListLitElems as <| acc.push a
+  | _ => none
+
 end Lean.Meta.Tactic.Cbv

src/Lean/Meta/Tactic/FunInd.lean

@@ -287,7 +287,7 @@ fails.
 partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M Expr := withoutExporting do
   unless e.containsFVar oldIH do
     return e
-  withTraceNode `Meta.FunInd (pure m!"{exceptEmoji ·} foldAndCollect ({mkFVar oldIH} → {mkFVar newIH})::{indentExpr e}") do
+  withTraceNode `Meta.FunInd (fun _ => pure m!"foldAndCollect ({mkFVar oldIH} → {mkFVar newIH})::{indentExpr e}") do
 
   let e' ← id do
     if let some matcherApp ← matchMatcherApp? e (alsoCasesOn := true) then
@@ -496,7 +496,7 @@ def M2.branch {α} (act : M2 α) : M2 α :=
 /-- Base case of `buildInductionBody`: Construct a case for the final induction hypothesis.  -/
 def buildInductionCase (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (toErase toClear : Array FVarId)
     (goal : Expr)  (e : Expr) : M2 Expr := do
-  withTraceNode `Meta.FunInd (pure m!"{exceptEmoji ·} buildInductionCase:{indentExpr e}") do
+  withTraceNode `Meta.FunInd (fun _ => pure m!"buildInductionCase:{indentExpr e}") do
   let _e' ← foldAndCollect oldIH newIH isRecCall e
   let IHs : Array Expr ← M.ask
   let IHs ← deduplicateIHs IHs
@@ -611,7 +611,7 @@ as `MVars` as it goes.
 partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
     (oldIH newIH : FVarId) (isRecCall : Expr → Option Expr) (e : Expr) : M2 Expr := do
   withTraceNode `Meta.FunInd
-    (pure m!"{exceptEmoji ·} buildInductionBody: {oldIH.name} → {newIH.name}\ngoal: {goal}:{indentExpr e}") do
+    (fun _ => pure m!"buildInductionBody: {oldIH.name} → {newIH.name}\ngoal: {goal}:{indentExpr e}") do
 
   -- if-then-else cause case split:
   match_expr e with

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -481,7 +481,7 @@ where
   go (proof prop : Expr) : M Unit := do
     let mut proof := proof
     let mut prop := prop
-    if (← getConfig).trace then
+    if (← getConfig).trace || (← getConfig).markInstances then
       /-
       **Note**: It is incorrect to use `mkFreshId` here because we use `withFreshNGen` at
       `instantiateTheorem`. So, we generate an unique id by using the number of instances generated so far.
@@ -927,7 +927,7 @@ private def ematchCore (extraThms : Array EMatchTheorem) : GoalM InstanceMap :=
 
 /--
 Performs one round of E-matching, and returns `true` if new instances were generated.
-Recall that the mapping is nonempty only if tracing is enabled.
+Recall that the mapping is nonempty only if tracing or instance marking is enabled.
 -/
 def ematch' (extraThms : Array EMatchTheorem := #[]) : GoalM (Bool × InstanceMap) := do
   let numInstances := (← get).ematch.numInstances
@@ -943,6 +943,8 @@ def ematch' (extraThms : Array EMatchTheorem := #[]) : GoalM (Bool × InstanceMa
     and we may have pending facts to process.
     -/
     processNewFacts
+  if (← getConfig).markInstances then
+    modifyThe Grind.State fun s => { s with instanceMap := s.instanceMap.insertMany map.toArray }
   return (progress, map)
 
 /--
@@ -954,7 +956,9 @@ def ematch (extraThms : Array EMatchTheorem := #[]) : GoalM Bool :=
 /-- Performs one round of E-matching using the giving theorems, and returns `true` if new instances were generated. -/
 def ematchOnly (thms : Array EMatchTheorem) : GoalM Bool := do
   let numInstances := (← get).ematch.numInstances
-  go |>.run'
+  let (_, s) ← go |>.run
+  if (← getConfig).markInstances then
+    modifyThe Grind.State fun st => { st with instanceMap := st.instanceMap.insertMany s.instanceMap.toArray }
   return (← get).ematch.numInstances != numInstances
 where
   go : EMatch.M Unit := do profileitM Exception "grind ematch" (← getOptions) do

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -18,6 +18,8 @@ import Lean.Meta.Tactic.Grind.ForallProp
 import Lean.Meta.Tactic.Grind.CtorIdx
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.Solve
+import Lean.Meta.Tactic.Grind.EMatch
+import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.LawfulEqCmp
@@ -236,6 +238,55 @@ def Result.toMessageData (result : Result) : MetaM MessageData := do
       msgs := msgs ++ [msg]
   return MessageData.joinSep msgs m!"\n"
 
+/--
+Walks the proof term collecting `Origin`s of E-matching instances that appear,
+using the `mdata` markers placed by `markTheoremInstanceProof`.
+-/
+private partial def collectUsedOrigins (e : Expr) (map : EMatch.InstanceMap) : Std.HashSet Origin :=
+  let (_, s) := go e |>.run ({}, {})
+  s.2
+where
+  go (e : Expr) : StateM (Std.HashSet ExprPtr × Std.HashSet Origin) Unit := do
+    if isMarkedSubsingletonApp e then return ()
+    if (← get).1.contains { expr := e } then return ()
+    modify fun (v, o) => (v.insert { expr := e }, o)
+    if let some uniqueId := EMatch.isTheoremInstanceProof? e then
+      if let some thm := map[uniqueId]? then
+        modify fun (v, o) => (v, o.insert thm.origin)
+    match e with
+    | .lam _ d b _
+    | .forallE _ d b _ => go d; go b
+    | .proj _ _ b
+    | .mdata _ b       => go b
+    | .letE _ t v b _  => go t; go v; go b
+    | .app f a         => go f; go a
+    | _ => return ()
+
+/--
+Checks whether any E-matching lemmas were activated but do not appear in the final proof term.
+Controlled by `set_option grind.unusedLemmaThreshold`.
+Uses grind's instance-marking infrastructure for precise tracking.
+-/
+def checkUnusedActivations (mvarId : MVarId) (counters : Counters) : GrindM Unit := do
+  let threshold := grind.unusedLemmaThreshold.get (← getOptions)
+  if threshold == 0 then return ()
+  let proof ← instantiateMVars (mkMVar mvarId)
+  let map := (← get).instanceMap
+  let usedOrigins := collectUsedOrigins proof map
+  let mut unused : Array (Name × Nat) := #[]
+  for (origin, count) in counters.thm do
+    if count < threshold then continue
+    match origin with
+    | .decl declName =>
+      unless usedOrigins.contains origin do
+        unused := unused.push (declName, count)
+    | _ => pure ()
+  unless unused.isEmpty do
+    let sorted := unused.qsort fun (_, c₁) (_, c₂) => c₁ > c₂
+    let data ← sorted.mapM fun (declName, counter) =>
+      return .trace { cls := `thm } m!"{declName} ↦ {counter}" #[]
+    logWarning <| .trace { cls := `grind } "grind: activated but unused E-matching lemmas" data
+
 /--
 When `Config.revert := false`, we preprocess the hypotheses, and add them to the `grind` state.
 It starts at `goal.nextDeclIdx`. If `num?` is `some num`, then at most `num` local declarations are processed.
@@ -300,9 +351,15 @@ def GrindM.runAtGoal (mvarId : MVarId) (params : Params) (k : Goal → GrindM α
   go.run params (evalTactic? := evalTactic?)
 
 def main (mvarId : MVarId) (params : Params) : MetaM Result := do profileitM Exception "grind" (← getOptions) do
+  let params := if grind.unusedLemmaThreshold.get (← getOptions) > 0 then
+    { params with config.markInstances := true }
+  else params
   GrindM.runAtGoal mvarId params fun goal => do
     let failure? ← solve goal
-    mkResult params failure?
+    let result ← mkResult params failure?
+    if failure?.isNone then
+      checkUnusedActivations mvarId result.counters
+    return result
 
 /--
 Resolves delayed metavariable assignments created inside the current `withNewMCtxDepth` block.

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -78,6 +78,11 @@ register_builtin_option grind.warning : Bool := {
   descr    := "generate a warning whenever `grind` is used"
 }
 
+register_builtin_option grind.unusedLemmaThreshold : Nat := {
+  defValue := 0
+  descr    := "report E-matching lemmas activated at least this many times but not used in the proof (0 = disabled)"
+}
+
 /--
 Anchors are used to reference terms, local theorems, and case-splits in the `grind` state.
 We also use anchors to prune the search space when they are provided as `grind` parameters
@@ -232,6 +237,9 @@ structure State where
   Cached anchors (aka stable hash codes) for terms in the `grind` state.
   -/
   anchors : PHashMap ExprPtr UInt64 := {}
+  /-- Accumulated E-matching instance map for precise unused lemma tracking.
+  Only populated when `config.markInstances` is `true`. -/
+  instanceMap : Std.HashMap Name EMatchTheorem := {}
 
 instance : Nonempty State :=
   .intro {}

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -223,11 +223,6 @@ def mkHeartbeatCheck (leavePercent : Nat) : MetaM (MetaM Bool) := do
     else do
       return (← getRemainingHeartbeats) < hbThreshold
 
-private def librarySearchEmoji : Except ε (Option α) → String
-| .error _ => bombEmoji
-| .ok (some _) => crossEmoji
-| .ok none => checkEmoji
-
 /--
 Interleave x y interleaves the elements of x and y until one is empty and then returns
 final elements in other list.
@@ -291,8 +286,6 @@ def librarySearchSymm (searchFn : CandidateFinder) (goal : MVarId) : MetaM (Arra
   else
     pure $ l1.map (coreGoalCtx, ·)
 
-private def emoji (e : Except ε α) := if e.toBool then checkEmoji else crossEmoji
-
 /-- Create lemma from name and mod. -/
 def mkLibrarySearchLemma (lem : Name) (mod : DeclMod) : MetaM Expr := do
   let lem ← mkConstWithFreshMVarLevels lem
@@ -319,7 +312,7 @@ private def librarySearchLemma (cfg : ApplyConfig) (act : List MVarId → MetaM
   let ((goal, mctx), (name, mod)) := cand
   let ppMod (mod : DeclMod) : MessageData :=
         match mod with | .none => "" | .mp => " with mp" | .mpr => " with mpr"
-  withTraceNode `Tactic.librarySearch (return m!"{emoji ·} trying {name}{ppMod mod} ") do
+  withTraceNode `Tactic.librarySearch (fun _ => return m!"trying {name}{ppMod mod} ") do
     setMCtx mctx
     let lem ← mkLibrarySearchLemma name mod
     let newGoals ← goal.apply lem cfg
@@ -371,7 +364,7 @@ private def librarySearch' (goal : MVarId)
     (includeStar : Bool := true)
     (collectAll : Bool := false) :
     MetaM (Option (Array (List MVarId × MetavarContext))) := do
-  withTraceNode `Tactic.librarySearch (return m!"{librarySearchEmoji ·} {← goal.getType}") do
+  withTraceNode `Tactic.librarySearch (fun _ => return m!"{← goal.getType}") do
   profileitM Exception "librarySearch" (← getOptions) do
     let cfg : ApplyConfig := { allowSynthFailures := true }
     let shouldAbort ← mkHeartbeatCheck leavePercentHeartbeats

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -434,7 +434,7 @@ but if `Config.letToHave` is enabled then we attempt to transform it into a `hav
 If that does not change it, then it is only `dsimp`ed.
 -/
 def simpLet (e : Expr) : SimpM Result := do
-  withTraceNode `Debug.Meta.Tactic.simp (return m!"{exceptEmoji ·} let{indentExpr e}") do
+  withTraceNode `Debug.Meta.Tactic.simp (fun _ => return m!"let{indentExpr e}") do
     assert! e.isLet
     /-
     Recall: `simpLet` is called after `reduceStep` is applied, so `simpLet` is not responsible for zeta reduction.

src/Lean/Meta/Tactic/SolveByElim.lean

@@ -54,7 +54,7 @@ def applyTactics (cfg : ApplyConfig := {}) (transparency : TransparencyMode := .
     (lemmas : List Expr) (g : MVarId) : MetaM (Lean.Meta.Iterator (List Lean.MVarId)) := do
   pure <|
     (← Meta.Iterator.ofList lemmas).filterMapM (fun e => observing? do
-      withTraceNode `Meta.Tactic.solveByElim (return m!"{exceptEmoji ·} trying to apply: {e}") do
+      withTraceNode `Meta.Tactic.solveByElim (fun _ => return m!"trying to apply: {e}") do
         let goals ← withTransparency transparency (g.apply e cfg)
         -- When we call `apply` interactively, `Lean.Elab.Tactic.evalApplyLikeTactic`
         -- deals with closing new typeclass goals by calling

src/Lean/Meta/UnificationHint.lean

@@ -114,7 +114,7 @@ where
 
   tryCandidate candidate : MetaM Bool :=
     withTraceNode `Meta.isDefEq.hint
-      (return m!"{exceptBoolEmoji ·} hint {candidate} at {t} =?= {s}") do
+      (fun _ => return m!"hint {candidate} at {t} =?= {s}") do
     checkpointDefEq do
       let cinfo ← getConstInfo candidate
       let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar

src/Lean/Parser/Do.lean

@@ -86,7 +86,7 @@ def doIdDecl   := leading_parser
   atomic (ident >> optType >> ppSpace >> leftArrow) >>
   doElemParser
 def doPatDecl  := leading_parser
-  atomic (termParser >> ppSpace >> leftArrow) >>
+  atomic (termParser >> optType >> ppSpace >> leftArrow) >>
   doElemParser >> optional ((checkColGe >> " | " >> doSeqIndent) >> optional (checkColGe >> doSeqIndent))
 @[builtin_doElem_parser] def doLetArrow      := leading_parser withPosition <|
   "let " >> optional "mut " >> (doIdDecl <|> doPatDecl)

src/Lean/ReservedNameAction.lean

@@ -37,7 +37,7 @@ Note that the handler can throw an exception.
 -/
 def executeReservedNameAction (name : Name) : CoreM Unit := do
   discard <|
-    withTraceNode `ReservedNameAction (pure m!"{exceptBoolEmoji ·} executeReservedNameAction for {name}") do
+    withTraceNode `ReservedNameAction (fun _ => pure m!"executeReservedNameAction for {name}") do
       (← reservedNameActionsRef.get).anyM (· name)
 
 /--

src/Lean/Shell.lean

@@ -10,7 +10,7 @@ import Lean.Elab.Frontend
 import Lean.Elab.ParseImportsFast
 import Lean.Server.Watchdog
 import Lean.Server.FileWorker
-import Lean.Compiler.IR.EmitC
+import Lean.Compiler.LCNF.EmitC
 import Init.System.Platform
 
 /-  Lean companion to  `shell.cpp` -/
@@ -545,7 +545,8 @@ def shellMain (args : List String) (opts : ShellOptions) : IO UInt32 := do
         | IO.eprintln s!"failed to create '{c}'"
           return 1
       profileitIO "C code generation" opts.leanOpts do
-        let data ← IO.ofExcept <| IR.emitC env mainModuleName
+        let data ← Compiler.LCNF.emitC mainModuleName
+          |>.toIO' { fileName, fileMap := default } { env }
         out.write data.toUTF8
     if let some bc := opts.bcFileName? then
       initLLVM

src/Lean/Util/Trace.lean

@@ -255,6 +255,43 @@ instance [always : MonadAlwaysExcept ε m] [STWorld ω m] [BEq α] [Hashable α]
     MonadAlwaysExcept ε (MonadCacheT α β m) where
   except := let _ := always.except; inferInstance
 
+def bombEmoji := "💥️"
+def checkEmoji := "✅️"
+def crossEmoji := "❌️"
+
+/-- Convert a `TraceResult` to its emoji representation. -/
+def TraceResult.toEmoji : TraceResult → String
+  | .success => checkEmoji
+  | .failure => crossEmoji
+  | .error   => bombEmoji
+
+/-- Convert an `Except` result to a `TraceResult`.
+`Except.error` always maps to `.error`.
+For `Bool`, `.ok false` maps to `.failure`. For `Option`, `.ok none` maps to `.failure`. -/
+class ExceptToTraceResult (ε α : Type) where
+  toTraceResult : Except ε α → TraceResult
+
+instance : ExceptToTraceResult ε Bool where
+  toTraceResult
+    | .error _ => .error
+    | .ok true => .success
+    | .ok false => .failure
+
+instance : ExceptToTraceResult ε (Option α) where
+  toTraceResult
+    | .error _ => .error
+    | .ok (some _) => .success
+    | .ok none => .failure
+
+instance (priority := low) : ExceptToTraceResult ε α where
+  toTraceResult
+    | .error _ => .error
+    | .ok _ => .success
+
+/-- Convert an `Except` to a `TraceResult` using the `ExceptToTraceResult` instance. -/
+def _root_.Except.toTraceResult [ExceptToTraceResult ε α] (e : Except ε α) : TraceResult :=
+  ExceptToTraceResult.toTraceResult e
+
 /-- Run the provided action `k`, and log its execution within a trace node.
 
 The message is produced after the action completes, and has access to its return value.
@@ -262,16 +299,20 @@ If it is more convenient to produce the message as part of the computation,
 then `Lean.withTraceNode'` can be used instead.
 If profiling is enabled, this will also log the runtime of `k`.
 
-A typical invocation might be:
+The class `ExceptToTraceResult` is used to convert the result produced by `k` into a `TraceResult`
+(success/failure/error), which is stored in `TraceData.result?` and also used to select the
+emoji prefix (✅️/❌️/💥️). A typical invocation might be:
 ```lean4
-withTraceNode `isPosTrace (msg := (return m!"{ExceptToEmoji.toEmoji ·} checking positivity")) do
+withTraceNode `isPosTrace
+    (msg := fun _ => return m!"checking positivity") do
   return 0 < x
 ```
 
 The `cls`, `collapsed`, and `tag` arguments are forwarded to the constructor of `TraceData`.
 -/
 @[inline]
-def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls : Name)
+def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m]
+    [ExceptToTraceResult ε α] (cls : Name)
     (msg : Except ε α → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do
   let opts ← getOptions
   if !opts.hasTrace then
@@ -293,7 +334,9 @@ where
       return (← MonadExcept.ofExcept res)
     let ref ← getRef
     let mut m ← try msg res catch _ => pure m!"<exception thrown while producing trace node message>"
-    let mut data := { cls, collapsed, tag }
+    let result := res.toTraceResult
+    m := m!"{result.toEmoji} {m}"
+    let mut data : TraceData := { cls, collapsed, tag, result? := some result }
     if trace.profiler.get opts then
       data := { data with startTime := start, stopTime := stop }
     addTraceNode oldTraces data ref m
@@ -339,56 +382,19 @@ private meta def expandTraceMacro (id : Syntax) (s : Syntax) : MacroM (TSyntax `
 macro "trace[" id:ident "]" s:(interpolatedStr(term) <|> term) : doElem => do
   expandTraceMacro id s.raw
 
-def bombEmoji := "💥️"
-def checkEmoji := "✅️"
-def crossEmoji := "❌️"
-
-/-- Visualize an `Except _ Bool` using a checkmark or cross.
-
-`bombEmoji` is used for `Except.error`. -/
-def exceptBoolEmoji : Except ε Bool → String
-  | .error _ => bombEmoji
-  | .ok true => checkEmoji
-  | .ok false => crossEmoji
-
-/-- Visualize an `Except _ (Option _)` using a checkmark or cross.
-
-`bombEmoji` is used for `Except.error`. -/
-def exceptOptionEmoji : Except ε (Option α) → String
-  | .error _ => bombEmoji
-  | .ok (some _) => checkEmoji
-  | .ok none => crossEmoji
-
-/-- Visualize an `Except` using a checkmark or a cross.
-
-Unlike `exceptBoolEmoji` this shows `.error` with `crossEmoji`. -/
-def exceptEmoji : Except ε α → String
-  | .error _ => crossEmoji
-  | .ok _ => checkEmoji
-
-class ExceptToEmoji (ε α : Type) where
-  /-- Visualize an `Except.ok x` using a checkmark or cross.
-
-  By convention, `bombEmoji` is used for `Except.error`. -/
-  toEmoji : Except ε α → String
-
-instance : ExceptToEmoji ε Bool where
-  toEmoji := exceptBoolEmoji
-
-instance : ExceptToEmoji ε (Option α) where
-  toEmoji := exceptOptionEmoji
 
 /--
 Similar to `withTraceNode`, but msg is constructed **before** executing `k`.
 This is important when debugging methods such as `isDefEq`, and we want to generate the message
-before `k` updates the metavariable assignment. The class `ExceptToEmoji` is used to convert
-the result produced by `k` into an emoji (e.g., `💥️`, `✅️`, `❌️`).
+before `k` updates the metavariable assignment. The class `ExceptToTraceResult` is used to convert
+the result produced by `k` into a `TraceResult` (success/failure/error), which is stored in
+`TraceData.result?` and also used to select the emoji prefix (✅️/❌️/💥️).
 
 TODO: find better name for this function.
 -/
 @[inline]
 def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
-    [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] [ExceptToEmoji ε α] (cls : Name)
+    [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] [ExceptToTraceResult ε α] (cls : Name)
     (msg : Unit → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do
   let opts ← getOptions
   if !opts.hasTrace then
@@ -411,8 +417,9 @@ where
     unless clsEnabled || aboveThresh do
       modifyTraces (oldTraces ++ ·)
       return (← MonadExcept.ofExcept res)
-    let mut msg := m!"{ExceptToEmoji.toEmoji res} {msg}"
-    let mut data := { cls, collapsed, tag }
+    let result := res.toTraceResult
+    let mut msg := m!"{result.toEmoji} {msg}"
+    let mut data : TraceData := { cls, collapsed, tag, result? := some result }
     if trace.profiler.get opts then
       data := { data with startTime := start, stopTime := stop }
     addTraceNode oldTraces data ref msg

src/Std/Do/Triple/SpecLemmas.lean

@@ -688,6 +688,7 @@ After leaving the loop, the cursor's prefix is `xs` and the suffix is empty.
 During the induction step, the invariant holds for a suffix with head element `x`.
 After running the loop body, the invariant then holds after shifting `x` to the prefix.
 -/
+@[mvcgen_invariant_type]
 abbrev Invariant {α : Type u₁} (xs : List α) (β : Type u₂) (ps : PostShape.{max u₁ u₂}) :=
   PostCond (List.Cursor xs × β) ps
 
@@ -710,6 +711,18 @@ won't need to prove anything about the bogus case where the loop has returned ea
 another iteration of the loop body.
 -/
 abbrev Invariant.withEarlyReturn {α} {xs : List α} {γ : Type (max u₁ u₂)}
+  (onContinue : List.Cursor xs → β → Assertion ps)
+  (onReturn : γ → β → Assertion ps)
+  (onExcept : ExceptConds ps := ExceptConds.false) :
+    Invariant xs (MProd (Option γ) β) ps :=
+  ⟨fun ⟨xs, x, b⟩ => spred(
+        (⌜x = none⌝ ∧ onContinue xs b)
+      ∨ (∃ r, ⌜x = some r⌝ ∧ ⌜xs.suffix = []⌝ ∧ onReturn r b)),
+   onExcept⟩
+
+/-- Like `Invariant.withEarlyReturn`, but for the new `do` elaborator which uses `Prod`
+instead of `MProd` for the state tuple. -/
+abbrev Invariant.withEarlyReturnNewDo {α} {xs : List α} {γ : Type (max u₁ u₂)}
   (onContinue : List.Cursor xs → β → Assertion ps)
   (onReturn : γ → β → Assertion ps)
   (onExcept : ExceptConds ps := ExceptConds.false) :
@@ -1997,6 +2010,18 @@ theorem Spec.foldlM_array {α β : Type u} {m : Type u → Type v} {ps : PostSha
   simp
   apply Spec.foldlM_list inv step
 
+/--
+The type of loop invariants used by the specifications of `for ... in ...` loops over strings.
+A loop invariant is a `PostCond` that takes as parameters
+
+* A `String.Pos` representing the current position in the string `s`.
+* A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of
+  `let mut` variables and early return.
+-/
+@[mvcgen_invariant_type]
+abbrev StringInvariant (s : String) (β : Type u) (ps : PostShape.{u}) :=
+  PostCond (s.Pos × β) ps
+
 /--
 Helper definition for specifying loop invariants for loops with early return.
 
@@ -2019,7 +2044,20 @@ abbrev StringInvariant.withEarlyReturn {s : String}
   (onContinue : s.Pos → β → Assertion ps)
   (onReturn : γ → β → Assertion ps)
   (onExcept : ExceptConds ps := ExceptConds.false) :
-    PostCond (s.Pos × MProd (Option γ) β) ps
+    StringInvariant s (MProd (Option γ) β) ps
+    :=
+  ⟨fun ⟨pos, x, b⟩ => spred(
+        (⌜x = none⌝ ∧ onContinue pos b)
+      ∨ (∃ r, ⌜x = some r⌝ ∧ ⌜pos = s.endPos⌝ ∧ onReturn r b)),
+   onExcept⟩
+
+/-- Like `StringInvariant.withEarlyReturn`, but for the new `do` elaborator which uses `Prod`
+instead of `MProd` for the state tuple. -/
+abbrev StringInvariant.withEarlyReturnNewDo {s : String}
+  (onContinue : s.Pos → β → Assertion ps)
+  (onReturn : γ → β → Assertion ps)
+  (onExcept : ExceptConds ps := ExceptConds.false) :
+    StringInvariant s (Prod (Option γ) β) ps
     :=
   ⟨fun ⟨pos, x, b⟩ => spred(
         (⌜x = none⌝ ∧ onContinue pos b)
@@ -2029,7 +2067,7 @@ abbrev StringInvariant.withEarlyReturn {s : String}
 @[spec]
 theorem Spec.forIn_string
     {s : String} {init : β} {f : Char → β → m (ForInStep β)}
-    (inv : PostCond (s.Pos × β) ps)
+    (inv : StringInvariant s β ps)
     (step : ∀ pos b (h : pos ≠ s.endPos),
       Triple
         (f (pos.get h) b)
@@ -2057,6 +2095,18 @@ theorem Spec.forIn_string
       next b => simp [ih _ _ hsp.next]
   | endPos => simpa using Triple.pure _ (by simp)
 
+/--
+The type of loop invariants used by the specifications of `for ... in ...` loops over string slices.
+A loop invariant is a `PostCond` that takes as parameters
+
+* A `String.Slice.Pos` representing the current position in the string slice `s`.
+* A state tuple of type `β`, which will be a nesting of `MProd`s representing the elaboration of
+  `let mut` variables and early return.
+-/
+@[mvcgen_invariant_type]
+abbrev StringSliceInvariant (s : String.Slice) (β : Type u) (ps : PostShape.{u}) :=
+  PostCond (s.Pos × β) ps
+
 /--
 Helper definition for specifying loop invariants for loops with early return.
 
@@ -2079,7 +2129,20 @@ abbrev StringSliceInvariant.withEarlyReturn {s : String.Slice}
   (onContinue : s.Pos → β → Assertion ps)
   (onReturn : γ → β → Assertion ps)
   (onExcept : ExceptConds ps := ExceptConds.false) :
-    PostCond (s.Pos × MProd (Option γ) β) ps
+    StringSliceInvariant s (MProd (Option γ) β) ps
+    :=
+  ⟨fun ⟨pos, x, b⟩ => spred(
+        (⌜x = none⌝ ∧ onContinue pos b)
+      ∨ (∃ r, ⌜x = some r⌝ ∧ ⌜pos = s.endPos⌝ ∧ onReturn r b)),
+   onExcept⟩
+
+/-- Like `StringSliceInvariant.withEarlyReturn`, but for the new `do` elaborator which uses `Prod`
+instead of `MProd` for the state tuple. -/
+abbrev StringSliceInvariant.withEarlyReturnNewDo {s : String.Slice}
+  (onContinue : s.Pos → β → Assertion ps)
+  (onReturn : γ → β → Assertion ps)
+  (onExcept : ExceptConds ps := ExceptConds.false) :
+    StringSliceInvariant s (Prod (Option γ) β) ps
     :=
   ⟨fun ⟨pos, x, b⟩ => spred(
         (⌜x = none⌝ ∧ onContinue pos b)
@@ -2089,7 +2152,7 @@ abbrev StringSliceInvariant.withEarlyReturn {s : String.Slice}
 @[spec]
 theorem Spec.forIn_stringSlice
     {s : String.Slice} {init : β} {f : Char → β → m (ForInStep β)}
-    (inv : PostCond (s.Pos × β) ps)
+    (inv : StringSliceInvariant s β ps)
     (step : ∀ pos b (h : pos ≠ s.endPos),
       Triple
         (f (pos.get h) b)