Merge remote-tracking branch 'origin/master' into mvcgen-with-grind

# Conflicts:
#	tests/bench/mvcgen/sym/lakefile.lean
#	tests/bench/mvcgen/sym/lib/VCGen.lean

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/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/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/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/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/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/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/Tactic/Do/Attr.lean

@@ -262,10 +262,30 @@ builtin_initialize mvcgenInvariantAttr : TagAttribute ←
 
 /--
 Returns `true` if `ty` is an application of a type tagged with `@[mvcgen_invariant_type]`.
-Falls back to checking for `Std.Do.Invariant` for bootstrapping purposes.
 -/
 def isMVCGenInvariantType (env : Environment) (ty : Expr) : Bool :=
   if let .const name .. := ty.getAppFn then
-    mvcgenInvariantAttr.hasTag env name || name == ``Std.Do.Invariant
+    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}"
@@ -188,7 +192,8 @@ where
     -- Last resort: Split match
     trace[Elab.Tactic.Do.vcgen] "split match: {e}"
     burnOne
-    return ← info.splitWith goal.toExpr (useSplitter := true) fun altSuff expAltType idx params => do
+    return ← info.splitWith goal.toExpr (useSplitter := true) fun altSuff expAltType idx altFVars => do
+      let params := altFVars.altParams
       burnOne
       let some goal := parseMGoal? expAltType
         | throwError "Bug in `mvcgen`: Expected alt type {expAltType} could not be parsed as an MGoal."
@@ -249,8 +254,8 @@ where
       mkFreshExprSyntheticOpaqueMVar hypsTy (name.appendIndexAfter i)
 
     let (joinPrf, joinGoal) ← forallBoundedTelescope joinTy numJoinParams fun joinParams _body => do
-      let φ ← info.splitWith (mkSort .zero) fun _suff _expAltType idx altParams =>
-        return mkAppN hypsMVars[idx]! (joinParams ++ altParams)
+      let φ ← info.splitWith (mkSort .zero) fun _suff _expAltType idx altFVars =>
+        return mkAppN hypsMVars[idx]! (joinParams ++ altFVars.altParams)
       withLocalDecl (← mkFreshUserName `h) .default φ fun h => do
         -- NB: `mkJoinGoal` is not quite `goal.withNewProg` because we only take 4 args and clear
         -- the stateful hypothesis of the goal.
@@ -351,60 +356,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 +478,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 +488,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 +502,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 isMVCGenInvariantType (← getEnv) ty 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/Split.lean

@@ -51,30 +51,106 @@ def altInfos (info : SplitInfo) : Array (Nat × Expr) := match info with
   | matcher matcherApp => matcherApp.altNumParams.mapIdx fun idx numParams =>
       (numParams, matcherApp.alts[idx]!)
 
+/-- The expression represented by a `SplitInfo`. -/
+def expr : SplitInfo → Expr
+  | .ite e => e
+  | .dite e => e
+  | .matcher matcherApp => matcherApp.toExpr
+
+/--
+Introduces fvars for all varying parts of a `SplitInfo` and provides the abstract
+`SplitInfo` and fvars to the continuation.
+
+For `ite`/`dite`, introduces `c : Prop`, `dec : Decidable c`, `t : mα` (or `t : c → mα`),
+`e : mα` (or `e : ¬c → mα`).
+For `matcher`, introduces discriminant fvars and alternative fvars, builds a non-dependent
+motive `fun _ ... _ => mα`, and adjusts matcher universe levels.
+
+The abstract `SplitInfo` satisfies `abstractInfo.expr = abstractProgram`.
+
+For `matcher`, the abstract `MatcherApp` stores eta-expanded fvar alts so that
+`splitWith`/`matcherApp.transform` can `instantiateLambda` them directly (no patching needed).
+Since eta-expanded alts like `fun n => alt n` can cause expensive higher-order unification in
+backward rule patterns, callers building backward rules should eta-reduce them first (e.g.
+via `Expr.eta` on the alt arguments of `abstractInfo.expr`).
+-/
+def withAbstract {n} {α} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [Inhabited α]
+    (info : SplitInfo) (resTy : Expr)
+    (k : (abstractInfo : SplitInfo) → (splitFVars : Array Expr) → n α) : n α :=
+  match info with
+  | .ite _ =>
+    withLocalDeclD `c (mkSort 0) fun c =>
+    withLocalDeclD `dec (mkApp (mkConst ``Decidable) c) fun dec =>
+    withLocalDeclD `t resTy fun t =>
+    withLocalDeclD `e resTy fun e => do
+    let u ← liftMetaM <| getLevel resTy
+    k (.ite <| mkApp5 (mkConst ``_root_.ite [u]) resTy c dec t e) #[c, dec, t, e]
+  | .dite _ =>
+    withLocalDeclD `c (mkSort 0) fun c =>
+    withLocalDeclD `dec (mkApp (mkConst ``Decidable) c) fun dec => do
+    let tTy ← liftMetaM <| mkArrow c resTy
+    let eTy ← liftMetaM <| mkArrow (mkNot c) resTy
+    withLocalDeclD `t tTy fun t =>
+    withLocalDeclD `e eTy fun e => do
+    let u ← liftMetaM <| getLevel resTy
+    k (.dite <| mkApp5 (mkConst ``_root_.dite [u]) resTy c dec t e) #[c, dec, t, e]
+  | .matcher matcherApp => do
+    let discrNamesTypes ← matcherApp.discrs.mapIdxM fun i discr => do
+      return ((`discr).appendIndexAfter (i+1), ← liftMetaM <| inferType discr)
+    withLocalDeclsDND discrNamesTypes fun discrs => do
+    -- Non-dependent motive: fun _ ... _ => mα
+    let motive ← liftMetaM <| lambdaTelescope matcherApp.motive fun motiveArgs _ =>
+      mkLambdaFVars motiveArgs resTy
+    -- The matcher's universe levels include a `uElimPos` slot for the elimination target level.
+    -- Our abstract motive `fun _ ... _ => mα` may target a different level than the original
+    -- dependent motive, so we update `matcherLevels[uElimPos]` to `getLevel mα`.
+    let matcherLevels ← match matcherApp.uElimPos? with
+      | none => pure matcherApp.matcherLevels
+      | some pos => do
+        let uElim ← liftMetaM <| getLevel resTy
+        pure <| matcherApp.matcherLevels.set! pos uElim
+    -- Build partial application to infer alt types
+    let matcherPartial := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params
+    let matcherPartial := mkApp matcherPartial motive
+    let matcherPartial := mkAppN matcherPartial discrs
+    let origAltTypes ← liftMetaM <| inferArgumentTypesN matcherApp.alts.size matcherPartial
+    let altNamesTypes := origAltTypes.mapIdx fun i ty => ((`alt).appendIndexAfter (i+1), ty)
+    withLocalDeclsDND altNamesTypes fun alts => do
+    -- Eta-expand fvar alts so `splitWith`/`matcherApp.transform` can `instantiateLambda` them.
+    let abstractMatcherApp : MatcherApp := {
+      matcherApp with
+      matcherLevels := matcherLevels
+      discrs        := discrs
+      motive        := motive
+      alts          := (← liftMetaM <| alts.mapM etaExpand)
+      remaining     := #[]
+    }
+    k (.matcher abstractMatcherApp) (discrs ++ alts)
+
 def splitWith
   {n} [MonadLiftT MetaM n] [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadEnv n] [MonadLog n]
   [AddMessageContext n] [MonadOptions n]
-  (info : SplitInfo) (resTy : Expr) (onAlt : Name → Expr → Nat → Array Expr → n Expr) (useSplitter := false) : n Expr := match info with
+  (info : SplitInfo) (resTy : Expr) (onAlt : Name → Expr → Nat → MatcherApp.TransformAltFVars → n Expr) (useSplitter := false) : n Expr := match info with
   | ite e => do
     let u ← getLevel resTy
     let c := e.getArg! 1
     let h := e.getArg! 2
     if useSplitter then -- dite is the "splitter" for ite
       let n ← liftMetaM <| mkFreshUserName `h
-      let t ← withLocalDecl n .default c fun h => do mkLambdaFVars #[h] (← onAlt `isTrue resTy 0 #[])
-      let e ← withLocalDecl n .default (mkNot c) fun h => do mkLambdaFVars #[h] (← onAlt `isFalse resTy 1 #[])
+      let t ← withLocalDecl n .default c fun h => do mkLambdaFVars #[h] (← onAlt `isTrue resTy 0 { fields := #[h] })
+      let e ← withLocalDecl n .default (mkNot c) fun h => do mkLambdaFVars #[h] (← onAlt `isFalse resTy 1 { fields := #[h] })
       return mkApp5 (mkConst ``_root_.dite [u]) resTy c h t e
     else
-      let t ← onAlt `isTrue resTy 0 #[]
-      let e ← onAlt `isFalse resTy 1 #[]
+      let t ← onAlt `isTrue resTy 0 { fields := #[] }
+      let e ← onAlt `isFalse resTy 1 { fields := #[] }
       return mkApp5 (mkConst ``_root_.ite [u]) resTy c h t e
   | dite e => do
     let u ← getLevel resTy
     let c := e.getArg! 1
     let h := e.getArg! 2
     let n ← liftMetaM <| mkFreshUserName `h
-    let t ← withLocalDecl n .default c fun h => do mkLambdaFVars #[h] (← onAlt `isTrue resTy 0 #[h])
-    let e ← withLocalDecl n .default (mkNot c) fun h => do mkLambdaFVars #[h] (← onAlt `isFalse resTy 1 #[h])
+    let t ← withLocalDecl n .default c fun h => do mkLambdaFVars #[h] (← onAlt `isTrue resTy 0 { args := #[h], fields := #[h] })
+    let e ← withLocalDecl n .default (mkNot c) fun h => do mkLambdaFVars #[h] (← onAlt `isFalse resTy 1 { args := #[h], fields := #[h] })
     return mkApp5 (mkConst ``_root_.dite [u]) resTy c h t e
   | matcher matcherApp => do
     let mask := matcherApp.discrs.map (·.isFVar)
@@ -83,8 +159,8 @@ def splitWith
     (·.toExpr) <$> matcherApp.transform
       (useSplitter := useSplitter) (addEqualities := useSplitter) -- (freshenNames := true)
       (onMotive := fun xs _body => pure (absMotiveBody.instantiateRev (Array.mask mask xs)))
-      (onAlt := fun idx expAltType params _alt => do
-        onAlt ((`h).appendIndexAfter (idx+1)) expAltType idx params)
+      (onAlt := fun idx expAltType altFVars _alt => do
+        onAlt ((`h).appendIndexAfter (idx+1)) expAltType idx altFVars)
 
 def simpDiscrs? (info : SplitInfo) (e : Expr) : SimpM (Option Simp.Result) := match info with
   | dite _ | ite _ => return none -- Tricky because we need to simultaneously rewrite  `[Decidable c]`

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/Meta/Match/MatcherApp/Transform.lean

@@ -201,6 +201,47 @@ private def forallAltTelescope'
       fun ys args _mask _bodyType => k ys args
   ) k
 
+/--
+Fvars/exprs introduced in the telescope of a matcher alternative during `transform`.
+
+* `args` are the values passed to `instantiateLambda` on the original alt. They usually
+  coincide with `fields`, but may include non-fvar values (e.g. `Unit.unit` for thunked alts).
+* `fields` are the constructor-field fvars (proper fvar subset of `args`).
+* `overlaps` are overlap-parameter fvars (splitter path only, for non-`casesOn` splitters).
+* `discrEqs` are discriminant-equation fvars from the matcher's own type (`numDiscrEqs`).
+* `extraEqs` are equation fvars added by the `addEqualities` flag.
+
+**Example.** `transform` with `addEqualities := true` on a `Nat.casesOn` application
+`Nat.casesOn (motive := …) n alt₀ alt₁` opens alt telescopes:
+```
+Alt 0 (zero):  (heq : n = Nat.zero) → motive Nat.zero
+  ⟹ { args := #[], fields := #[], extraEqs := #[heq] }
+
+Alt 1 (succ):  (k : Nat) → (heq : n = Nat.succ k) → motive (Nat.succ k)
+  ⟹ { args := #[k], fields := #[k], extraEqs := #[heq] }
+```
+-/
+structure TransformAltFVars where
+  /-- Arguments for `instantiateLambda` on the original alternative (see example above).
+  May include non-fvar values like `Unit.unit` for thunked alternatives. -/
+  args : Array Expr := #[]
+  /-- Constructor field fvars, i.e. the proper fvar subset of `args` (see example above). -/
+  fields : Array Expr
+  /-- Overlap parameter fvars (non-casesOn splitters only). -/
+  overlaps : Array Expr := #[]
+  /-- Discriminant equation fvars from the matcher's own type (`numDiscrEqs`). -/
+  discrEqs : Array Expr := #[]
+  /-- Extra equation fvars added by `addEqualities` (see `heq` in the example above). -/
+  extraEqs : Array Expr := #[]
+
+/-- The `altParams` that were used for `instantiateLambda alt altParams` inside `transform`. -/
+def TransformAltFVars.altParams (fvars : TransformAltFVars) : Array Expr :=
+  fvars.args ++ fvars.discrEqs
+
+/-- All proper fvars in binding order, matching the lambdas that `transform` wraps around the alt result. -/
+def TransformAltFVars.all (fvars : TransformAltFVars) : Array Expr :=
+  fvars.fields ++ fvars.overlaps ++ fvars.discrEqs ++ fvars.extraEqs
+
 /--
 Performs a possibly type-changing transformation to a `MatcherApp`.
 
@@ -229,7 +270,7 @@ def transform
     (addEqualities : Bool := false)
     (onParams : Expr → n Expr := pure)
     (onMotive : Array Expr → Expr → n Expr := fun _ e => pure e)
-    (onAlt : Nat → Expr → Array Expr → Expr → n Expr := fun _ _ _ e => pure e)
+    (onAlt : Nat → Expr → TransformAltFVars → Expr → n Expr := fun _ _ _ e => pure e)
     (onRemaining : Array Expr → n (Array Expr) := pure) :
     n MatcherApp := do
 
@@ -331,7 +372,7 @@ def transform
               let altParams := args ++ ys3
               let alt ← try instantiateLambda alt altParams
                         catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
-              let alt' ← onAlt altIdx altType altParams alt
+              let alt' ← onAlt altIdx altType { args, fields := ys, overlaps := ys2, discrEqs := ys3, extraEqs := ys4 } alt
               mkLambdaFVars (ys ++ ys2 ++ ys3 ++ ys4) alt'
         if splitterAltInfo.hasUnitThunk then
           -- The splitter expects a thunked alternative, but we don't want the `x : Unit` to be in
@@ -372,7 +413,7 @@ def transform
           let names ← lambdaTelescope alt fun xs _ => xs.mapM (·.fvarId!.getUserName)
           withUserNames xs names do
             let alt ← instantiateLambda alt xs
-            let alt' ← onAlt altIdx altType xs alt
+            let alt' ← onAlt altIdx altType { args := xs, fields := xs, extraEqs := ys4 } alt
             mkLambdaFVars (xs ++ ys4) alt'
       alts' := alts'.push alt'
 
@@ -446,7 +487,7 @@ def inferMatchType (matcherApp : MatcherApp) : MetaM MatcherApp := do
       }
       mkArrowN extraParams typeMatcherApp.toExpr
     )
-    (onAlt := fun _altIdx expAltType _altParams alt => do
+    (onAlt := fun _altIdx expAltType _altFVars alt => do
       let altType ← inferType alt
       let eq ← mkEq expAltType altType
       let proof ← mkFreshExprSyntheticOpaqueMVar eq

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/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/Main.lean

@@ -11,6 +11,8 @@ 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

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

@@ -315,7 +315,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
             -- statement and the inferred alt types
             let dummyGoal := mkConst ``True []
             mkArrow eTypeAbst dummyGoal)
-          (onAlt := fun _altIdx altType _altParams alt => do
+          (onAlt := fun _altIdx altType _altFVars alt => do
             lambdaTelescope1 alt fun oldIH' alt => do
               forallBoundedTelescope altType (some 1) fun newIH' _goal' => do
                 let #[newIH'] := newIH' | unreachable!
@@ -333,7 +333,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
           (onMotive := fun _motiveArgs motiveBody => do
             let some (_extra, body) := motiveBody.arrow? | throwError "motive not an arrow"
             M.eval (foldAndCollect oldIH newIH isRecCall body))
-          (onAlt := fun _altIdx altType _altParams alt => do
+          (onAlt := fun _altIdx altType _altFVars alt => do
             lambdaTelescope1 alt fun oldIH' alt => do
             -- We don't have suitable newIH around here, but we don't care since
             -- we just want to fold calls. So lets create a fake one.
@@ -691,7 +691,7 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
         (addEqualities := true)
         (onParams := (foldAndCollect oldIH newIH isRecCall ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (Array.mask mask xs)))
-        (onAlt := fun altIdx expAltType _altParams alt => M2.branch do
+        (onAlt := fun altIdx expAltType _altFVars alt => M2.branch do
           lambdaTelescope1 alt fun oldIH' alt => do
             forallBoundedTelescope expAltType (some 1) fun newIH' goal' => do
               let #[newIH'] := newIH' | unreachable!
@@ -714,7 +714,7 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
         (addEqualities := true)
         (onParams := (foldAndCollect oldIH newIH isRecCall ·))
         (onMotive := fun xs _body => pure (absMotiveBody.beta (Array.mask mask xs)))
-        (onAlt := fun altIdx expAltType _altParams alt => M2.branch do
+        (onAlt := fun altIdx expAltType _altFVars alt => M2.branch do
           withRewrittenMotiveArg expAltType (rwMatcher altIdx) fun expAltType' =>
             buildInductionBody toErase toClear expAltType' oldIH newIH isRecCall alt)
       return matcherApp'.toExpr

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 ← 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/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)

src/Std/Tactic/Do/Syntax.lean

@@ -364,14 +364,29 @@ macro "mvcgen_trivial" : tactic =>
   )
 
 /--
-An invariant alternative of the form `· term`, one per invariant goal.
+A goal section alternative of the form `· term`, one per goal.
+Used by both `invariants` and `witnesses` sections.
 -/
-syntax invariantDotAlt := ppDedent(ppLine) cdotTk (colGe term)
+syntax goalDotAlt := ppDedent(ppLine) cdotTk (colGe term)
 
 /--
-An invariant alternative of the form `| inv<n> a b c => term`, one per invariant goal.
+A goal section alternative of the form `| label<n> a b c => term`, one per goal.
+Used by both `invariants` and `witnesses` sections.
 -/
-syntax invariantCaseAlt := ppDedent(ppLine) "| " caseArg " => " (colGe term)
+syntax goalCaseAlt := ppDedent(ppLine) "| " caseArg " => " (colGe term)
+
+/--
+The contextual keyword ` witnesses `.
+-/
+syntax witnessesKW := &"witnesses "
+
+/--
+After `mvcgen [...]`, there can be an optional `witnesses` followed by either
+* a bulleted list of witnesses `· term; · term`.
+* a labelled list of witnesses `| witness1 => term; witness2 a b c => term`, which is useful for
+  naming inaccessibles.
+-/
+syntax witnessAlts := witnessesKW withPosition((colGe (goalDotAlt <|> goalCaseAlt))*)
 
 /--
 Either the contextual keyword ` invariants ` or its tracing form ` invariants? ` which suggests
@@ -380,14 +395,14 @@ skeletons for missing invariants as a hint.
 syntax invariantsKW := &"invariants " <|> &"invariants? "
 
 /--
-After `mvcgen [...]`, there can be an optional `invariants` followed by either
+After `mvcgen [...] witnesses ...`, there can be an optional `invariants` followed by either
 * a bulleted list of invariants `· term; · term`.
 * a labelled list of invariants `| inv1 => term; inv2 a b c => term`, which is useful for naming
   inaccessibles.
 The tracing variant ` invariants? ` will suggest a skeleton for missing invariants; see the
 docstring for `mvcgen`.
 -/
-syntax invariantAlts := invariantsKW withPosition((colGe (invariantDotAlt <|> invariantCaseAlt))*)
+syntax invariantAlts := invariantsKW withPosition((colGe (goalDotAlt <|> goalCaseAlt))*)
 
 /--
 In induction alternative, which can have 1 or more cases on the left
@@ -404,7 +419,7 @@ syntax vcAlts := "with " (ppSpace colGt tactic)? withPosition((colGe vcAlt)*)
 @[tactic_alt Lean.Parser.Tactic.mvcgenMacro]
 syntax (name := mvcgen) "mvcgen" optConfig
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
-  (invariantAlts)? (vcAlts)? : tactic
+  (witnessAlts)? (invariantAlts)? (vcAlts)? : tactic
 
 /--
 A hint tactic that expands to `mvcgen invariants?`.