chore: bump patch version to 1

The namespace cache volumes were running out of space and preventing CI
from running.

.github/workflows/build-template.yml

@@ -66,16 +66,10 @@ jobs:
           brew install ccache tree zstd coreutils gmp libuv
         if: runner.os == 'macOS'
       - name: Checkout
-        if: (!endsWith(matrix.os, '-with-cache'))
         uses: actions/checkout@v6
         with:
           # the default is to use a virtual merge commit between the PR and master: just use the PR
           ref: ${{ github.event.pull_request.head.sha }}
-      - name: Namespace Checkout
-        if: endsWith(matrix.os, '-with-cache')
-        uses: namespacelabs/nscloud-checkout-action@v8
-        with:
-          ref: ${{ github.event.pull_request.head.sha }}
       - name: Open Nix shell once
         run: true
         if: runner.os == 'Linux'

src/CMakeLists.txt

@@ -10,9 +10,9 @@ endif()
 include(ExternalProject)
 project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
-set(LEAN_VERSION_MINOR 29)
-set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_MINOR 28)
+set(LEAN_VERSION_PATCH 1)
+set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Init/SimpLemmas.lean

@@ -44,61 +44,6 @@ theorem implies_congr_left {p₁ p₂ : Sort u} {q : Sort v} (h : p₁ = p₂) :
 theorem implies_congr_right {p : Sort u} {q₁ q₂ : Sort v} (h : q₁ = q₂) : (p → q₁) = (p → q₂) :=
   h ▸ rfl
 
-namespace Lean
-/--
-`Arrow α β` is definitionally equal to `α → β`, but represented as a function
-application rather than `Expr.forallE`.
-
-This representation is useful for proof automation that builds nested implications
-like `pₙ → ... → p₂ → p₁`. With `Expr.forallE`, each nesting level introduces a
-binder that bumps de Bruijn indices in subterms, destroying sharing even with
-hash-consing. For example, if `p₁` contains `#20`, then at depth 2 it becomes `#21`,
-at depth 3 it becomes `#22`, etc., causing quadratic proof growth.
-
-With `arrow`, both arguments are explicit (not under binders), so subterms remain
-identical across nesting levels and can be shared, yielding linear-sized proofs.
--/
-def Arrow (α : Sort u) (β : Sort v) : Sort (imax u v) := α → β
-
-theorem arrow_congr {p₁ p₂ : Sort u} {q₁ q₂ : Sort v} (h₁ : p₁ = p₂) (h₂ : q₁ = q₂) : Arrow p₁ q₁ = Arrow p₂ q₂ :=
-  h₁ ▸ h₂ ▸ rfl
-
-theorem arrow_congr_left {p₁ p₂ : Sort u} {q : Sort v} (h : p₁ = p₂) : Arrow p₁ q = Arrow p₂ q :=
-  h ▸ rfl
-
-theorem arrow_congr_right {p : Sort u} {q₁ q₂ : Sort v} (h : q₁ = q₂) : Arrow p q₁ = Arrow p q₂ :=
-  h ▸ rfl
-
-theorem true_arrow (p : Prop) : Arrow True p = p := by
-  simp [Arrow]; constructor
-  next => intro h; exact h .intro
-  next => intros; assumption
-
-theorem true_arrow_congr_left (p q : Prop) : p = True → Arrow p q = q := by
-  intros; subst p; apply true_arrow
-
-theorem true_arrow_congr_right (q q' : Prop) : q = q' → Arrow True q = q' := by
-  intros; subst q; apply true_arrow
-
-theorem true_arrow_congr (p q q' : Prop) : p = True → q = q' → Arrow p q = q' := by
-  intros; subst p q; apply true_arrow
-
-theorem false_arrow (p : Prop) : Arrow False p = True := by
-  simp [Arrow]; constructor
-  next => intros; exact .intro
-  next => intros; contradiction
-
-theorem false_arrow_congr (p q : Prop) : p = False → Arrow p q = True := by
-  intros; subst p; apply false_arrow
-
-theorem arrow_true (α : Sort u) : Arrow α True = True := by
-  simp [Arrow]; constructor <;> intros <;> exact .intro
-
-theorem arrow_true_congr (α : Sort u) (p : Prop) : p = True → Arrow α p = True := by
-  intros; subst p; apply arrow_true
-
-end Lean
-
 theorem iff_congr {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ ↔ p₂) (h₂ : q₁ ↔ q₂) : (p₁ ↔ q₁) ↔ (p₂ ↔ q₂) :=
   Iff.of_eq (propext h₁ ▸ propext h₂ ▸ rfl)
 

src/Lean/Compiler/IR.lean

@@ -27,7 +27,6 @@ public import Lean.Compiler.IR.ToIR
 public import Lean.Compiler.IR.ToIRType
 public import Lean.Compiler.IR.Meta
 public import Lean.Compiler.IR.Toposort
-public import Lean.Compiler.IR.SimpleGroundExpr
 
 -- The following imports are not required by the compiler. They are here to ensure that there
 -- are no orphaned modules.
@@ -72,7 +71,6 @@ def compile (decls : Array Decl) : CompilerM (Array Decl) := do
   logDecls `result decls
   checkDecls decls
   decls ← toposortDecls decls
-  decls.forM Decl.detectSimpleGround
   addDecls decls
   inferMeta decls
   return decls

src/Lean/Compiler/IR/CompilerM.lean

@@ -186,7 +186,7 @@ def getDecl (n : Name) : CompilerM Decl := do
 def findLocalDecl (n : Name) : CompilerM (Option Decl) :=
   return declMapExt.getState (← getEnv) |>.find? n
 
-/-- Returns the list of IR declarations in reverse declaration order. -/
+/-- Returns the list of IR declarations in declaration order. -/
 def getDecls (env : Environment) : List Decl :=
   declMapExt.getEntries env
 

src/Lean/Compiler/IR/EmitC.lean

@@ -12,7 +12,6 @@ public import Lean.Compiler.IR.NormIds
 public import Lean.Compiler.IR.SimpCase
 public import Lean.Compiler.IR.Boxing
 public import Lean.Compiler.ModPkgExt
-import Lean.Compiler.IR.SimpleGroundExpr
 
 public section
 
@@ -77,26 +76,6 @@ def toCType : IRType → String
   | IRType.struct _ _ => panic! "not implemented yet"
   | IRType.union _ _  => panic! "not implemented yet"
 
-def toHexDigit (c : Nat) : String :=
-  String.singleton c.digitChar
-
-def quoteString (s : String) : String :=
-  let q := "\"";
-  let q := s.foldl
-    (fun q c => q ++
-      if c == '\n' then "\\n"
-      else if c == '\r' then "\\r"
-      else if c == '\t' then "\\t"
-      else if c == '\\' then "\\\\"
-      else if c == '\"' then "\\\""
-      else if c == '?' then "\\?" -- avoid trigraphs
-      else if c.toNat <= 31 then
-        "\\x" ++ toHexDigit (c.toNat / 16) ++ toHexDigit (c.toNat % 16)
-      -- TODO(Leo): we should use `\unnnn` for escaping unicode characters.
-      else String.singleton c)
-    q;
-  q ++ "\""
-
 def throwInvalidExportName {α : Type} (n : Name) : M α :=
   throw s!"invalid export name '{n}'"
 
@@ -122,160 +101,30 @@ def toCInitName (n : Name) : M String := do
 def emitCInitName (n : Name) : M Unit :=
   toCInitName n >>= emit
 
-def ctorScalarSizeStr (usize : Nat) (ssize : Nat) : String :=
-  if usize == 0 then toString ssize
-  else if ssize == 0 then s!"sizeof(size_t)*{usize}"
-  else s!"sizeof(size_t)*{usize} + {ssize}"
-
-structure GroundState where
-  auxCounter : Nat := 0
-
-abbrev GroundM := StateT GroundState M
-
-partial def emitGroundDecl (decl : Decl) (cppBaseName : String) : M Unit := do
-  let some ground := getSimpleGroundExpr (← getEnv) decl.name | unreachable!
-  discard <| compileGround ground |>.run {}
-where
-  compileGround (e : SimpleGroundExpr) : GroundM Unit := do
-    let valueName ← compileGroundToValue e
-    let declPrefix := if isClosedTermName (← getEnv) decl.name then "static" else "LEAN_EXPORT"
-    emitLn <| s!"{declPrefix} const lean_object* {cppBaseName} = (const lean_object*)&{valueName};"
-
-  compileGroundToValue (e : SimpleGroundExpr) : GroundM String := do
-    match e with
-    | .ctor cidx objArgs usizeArgs scalarArgs =>
-      let val ← compileCtor cidx objArgs usizeArgs scalarArgs
-      mkValueCLit "lean_ctor_object" val
-    | .string data =>
-      let leanStringTag := 249
-      let header := mkHeader 0 0 leanStringTag
-      let size := data.utf8ByteSize + 1 -- null byte
-      let length := data.length
-      let data : String := quoteString data
-      mkValueCLit
-        "lean_string_object"
-        s!"\{.m_header = {header}, .m_size = {size}, .m_capacity = {size}, .m_length = {length}, .m_data = {data}}"
-    | .pap func args =>
-      let numFixed := args.size
-      let leanClosureTag := 245
-      let header := mkHeader s!"sizeof(lean_closure_object) + sizeof(void*)*{numFixed}" 0 leanClosureTag
-      let funPtr := s!"(void*){← toCName func}"
-      let arity := (← getDecl func).params.size
-      let args ← args.mapM groundArgToCLit
-      let argArray := String.intercalate "," args.toList
-      mkValueCLit
-        "lean_closure_object"
-        s!"\{.m_header = {header}, .m_fun = {funPtr}, .m_arity = {arity}, .m_num_fixed = {numFixed}, .m_objs = \{{argArray}} }"
-    | .nameMkStr args =>
-      let obj ← groundNameMkStrToCLit args
-      mkValueCLit "lean_ctor_object" obj
-    | .reference refDecl => findValueDecl refDecl
-
-  mkValueName (name : String) : String :=
-    name ++ "_value"
-
-  mkAuxValueName (name : String) (idx : Nat) : String :=
-    mkValueName name ++ s!"_aux_{idx}"
-
-  mkAuxDecl (type value : String) : GroundM String := do
-    let idx ← modifyGet fun s => (s.auxCounter, { s with auxCounter := s.auxCounter + 1 })
-    let name := mkAuxValueName cppBaseName idx
-    emitLn <| s!"static const {type} {name} = {value};"
-    return name
-
-  mkValueCLit (type value : String) : GroundM String := do
-    let valueName := mkValueName cppBaseName
-    emitLn <| s!"static const {type} {valueName} = {value};"
-    return valueName
-
-  groundNameMkStrToCLit (args : Array (Name × UInt64)) : GroundM String := do
-    assert! args.size > 0
-    if args.size == 1 then
-      let (ref, hash) := args[0]!
-      let hash := uint64ToByteArrayLE hash
-      compileCtor 1 #[.tagged 0, .reference ref] #[] hash
-    else
-      let (ref, hash) := args.back!
-      let args := args.pop
-      let lit ← groundNameMkStrToCLit args
-      let auxName ← mkAuxDecl "lean_ctor_object" lit
-      let hash := uint64ToByteArrayLE hash
-      compileCtor 1 #[.rawReference auxName, .reference ref] #[] hash
-
-  groundArgToCLit (a : SimpleGroundArg) : GroundM String := do
-    match a with
-    | .tagged val => return s!"((lean_object*)(((size_t)({val}) << 1) | 1))"
-    | .reference decl =>  return s!"((lean_object*)&{← findValueDecl decl})"
-    | .rawReference decl => return s!"((lean_object*)&{decl})"
-
-  findValueDecl (decl : Name) : GroundM String := do
-    let mut decl := decl
-    while true do
-      if let some (.reference ref) := getSimpleGroundExpr (← getEnv) decl then
-        decl := ref
-      else
-        break
-    return mkValueName (← toCName decl)
-
-  compileCtor (cidx : Nat) (objArgs : Array SimpleGroundArg) (usizeArgs : Array USize)
-      (scalarArgs : Array UInt8) : GroundM String := do
-    let header := mkCtorHeader objArgs.size usizeArgs.size scalarArgs.size cidx
-    let objArgs ← objArgs.mapM groundArgToCLit
-    let usizeArgs : Array String := usizeArgs.map fun val => s!"(lean_object*)(size_t)({val}ULL)"
-    assert! scalarArgs.size % 8 == 0
-    let scalarArgs : Array String := Id.run do
-      let chunks := scalarArgs.size / 8
-      let mut packed := Array.emptyWithCapacity chunks
-      for idx in 0...chunks do
-        let b1 := scalarArgs[idx * 8]!
-        let b2 := scalarArgs[idx * 8 + 1]!
-        let b3 := scalarArgs[idx * 8 + 2]!
-        let b4 := scalarArgs[idx * 8 + 3]!
-        let b5 := scalarArgs[idx * 8 + 4]!
-        let b6 := scalarArgs[idx * 8 + 5]!
-        let b7 := scalarArgs[idx * 8 + 6]!
-        let b8 := scalarArgs[idx * 8 + 7]!
-        let lit := s!"LEAN_SCALAR_PTR_LITERAL({b1}, {b2}, {b3}, {b4}, {b5}, {b6}, {b7}, {b8})"
-        packed := packed.push lit
-      return packed
-    let argArray := String.intercalate "," (objArgs ++ usizeArgs ++ scalarArgs).toList
-    return s!"\{.m_header = {header}, .m_objs = \{{argArray}}}"
-
-  mkCtorHeader (numObjs : Nat) (usize : Nat) (ssize : Nat) (tag : Nat) : String :=
-    let size := s!"sizeof(lean_ctor_object) + sizeof(void*)*{numObjs} + {ctorScalarSizeStr usize ssize}"
-    mkHeader size numObjs tag
-
-  mkHeader {α : Type} [ToString α] (csSz : α) (other : Nat) (tag : Nat) : String :=
-    s!"\{.m_rc = 0, .m_cs_sz = {csSz}, .m_other = {other}, .m_tag = {tag}}"
-
 def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M Unit := do
   let ps := decl.params
   let env ← getEnv
-
-  if isSimpleGroundDecl env decl.name then
-    emitGroundDecl decl cppBaseName
+  if ps.isEmpty then
+    if isExternal then emit "extern "
+    else if isClosedTermName env decl.name then emit "static "
+    else emit "LEAN_EXPORT "
   else
-    if ps.isEmpty then
-      if isExternal then emit "extern "
-      else if isClosedTermName env decl.name then emit "static "
-      else emit "LEAN_EXPORT "
+    if !isExternal then emit "LEAN_EXPORT "
+  emit (toCType decl.resultType ++ " " ++ cppBaseName)
+  unless ps.isEmpty do
+    emit "("
+    -- We omit void parameters, note that they are guaranteed not to occur in boxed functions
+    let ps := ps.filter (fun p => !p.ty.isVoid)
+    -- We omit erased parameters for extern constants
+    let ps := if isExternC env decl.name then ps.filter (fun p => !p.ty.isErased) else ps
+    if ps.size > closureMaxArgs && isBoxedName decl.name then
+      emit "lean_object**"
     else
-      if !isExternal then emit "LEAN_EXPORT "
-    emit (toCType decl.resultType ++ " " ++ cppBaseName)
-    unless ps.isEmpty do
-      emit "("
-      -- We omit void parameters, note that they are guaranteed not to occur in boxed functions
-      let ps := ps.filter (fun p => !p.ty.isVoid)
-      -- We omit erased parameters for extern constants
-      let ps := if isExternC env decl.name then ps.filter (fun p => !p.ty.isErased) else ps
-      if ps.size > closureMaxArgs && isBoxedName decl.name then
-        emit "lean_object**"
-      else
-        ps.size.forM fun i _ => do
-          if i > 0 then emit ", "
-          emit (toCType ps[i].ty)
-      emit ")"
-    emitLn ";"
+      ps.size.forM fun i _ => do
+        if i > 0 then emit ", "
+        emit (toCType ps[i].ty)
+    emit ")"
+  emitLn ";"
 
 def emitFnDecl (decl : Decl) (isExternal : Bool) : M Unit := do
   let cppBaseName ← toCName decl.name
@@ -288,9 +137,10 @@ def emitExternDeclAux (decl : Decl) (cNameStr : String) : M Unit := do
 
 def emitFnDecls : M Unit := do
   let env ← getEnv
-  let decls := getDecls env |>.reverse
+  let decls := getDecls env
   let modDecls  : NameSet := decls.foldl (fun s d => s.insert d.name) {}
-  let usedDecls := collectUsedDecls env decls
+  let usedDecls : NameSet := decls.foldl (fun s d => collectUsedDecls env d (s.insert d.name)) {}
+  let usedDecls := usedDecls.toList
   usedDecls.forM fun n => do
     let decl ← getDecl n;
     match getExternNameFor env `c decl.name with
@@ -503,8 +353,10 @@ def emitArgs (ys : Array Arg) : M Unit :=
     if i > 0 then emit ", "
     emitArg ys[i]
 
-def emitCtorScalarSize (usize : Nat) (ssize : Nat) : M Unit :=
-  emit <| ctorScalarSizeStr usize ssize
+def emitCtorScalarSize (usize : Nat) (ssize : Nat) : M Unit := do
+  if usize == 0 then emit ssize
+  else if ssize == 0 then emit "sizeof(size_t)*"; emit usize
+  else emit "sizeof(size_t)*"; emit usize; emit " + "; emit ssize
 
 def emitAllocCtor (c : CtorInfo) : M Unit := do
   emit "lean_alloc_ctor("; emit c.cidx; emit ", "; emit c.size; emit ", "
@@ -583,18 +435,12 @@ def emitExternCall (f : FunId) (ps : Array Param) (extData : ExternAttrData) (ys
   | some (ExternEntry.inline _ pat)     => do emit (expandExternPattern pat (toStringArgs ys)); emitLn ";"
   | _ => throw s!"failed to emit extern application '{f}'"
 
-def emitLeanFunReference (f : FunId) : M Unit := do
-  if isSimpleGroundDecl (← getEnv) f then
-    emit s!"((lean_object*)({← toCName f}))"
-  else
-    emitCName f
-
 def emitFullApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit := do
   emitLhs z
   let decl ← getDecl f
   match decl with
   | .fdecl (xs := ps) .. | .extern (xs := ps) (ext := { entries := [.opaque], .. }) .. =>
-    emitLeanFunReference f
+    emitCName f
     if ys.size > 0 then
       let (ys, _) := ys.zip ps |>.filter (fun (_, p) => !p.ty.isVoid) |>.unzip
       emit "("; emitArgs ys; emit ")"
@@ -636,6 +482,26 @@ def emitUnbox (z : VarId) (t : IRType) (x : VarId) : M Unit := do
 def emitIsShared (z : VarId) (x : VarId) : M Unit := do
   emitLhs z; emit "!lean_is_exclusive("; emit x; emitLn ");"
 
+def toHexDigit (c : Nat) : String :=
+  String.singleton c.digitChar
+
+def quoteString (s : String) : String :=
+  let q := "\"";
+  let q := s.foldl
+    (fun q c => q ++
+      if c == '\n' then "\\n"
+      else if c == '\r' then "\\r"
+      else if c == '\t' then "\\t"
+      else if c == '\\' then "\\\\"
+      else if c == '\"' then "\\\""
+      else if c == '?' then "\\?" -- avoid trigraphs
+      else if c.toNat <= 31 then
+        "\\x" ++ toHexDigit (c.toNat / 16) ++ toHexDigit (c.toNat % 16)
+      -- TODO(Leo): we should use `\unnnn` for escaping unicode characters.
+      else String.singleton c)
+    q;
+  q ++ "\""
+
 def emitNumLit (t : IRType) (v : Nat) : M Unit := do
   if t.isObj then
     if v < UInt32.size then
@@ -804,7 +670,7 @@ def emitDeclAux (d : Decl) : M Unit := do
   let env ← getEnv
   let (_, jpMap) := mkVarJPMaps d
   withReader (fun ctx => { ctx with jpMap := jpMap }) do
-  unless hasInitAttr env d.name || isSimpleGroundDecl env d.name do
+  unless hasInitAttr env d.name do
     match d with
     | .fdecl (f := f) (xs := xs) (type := t) (body := b) .. =>
       let baseName ← toCName f;
@@ -883,8 +749,7 @@ def emitDeclInit (d : Decl) : M Unit := do
       if getBuiltinInitFnNameFor? env d.name |>.isSome then
         emit "}"
     | _ =>
-      if !isSimpleGroundDecl env d.name then
-        emitCName n; emit " = "; emitCInitName n; emitLn "();"; emitMarkPersistent d n
+      emitCName n; emit " = "; emitCInitName n; emitLn "();"; emitMarkPersistent d n
 
 def emitInitFn : M Unit := do
   let env ← getEnv

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -31,7 +31,6 @@ time. These changes can likely be done similar to the ones in EmitC:
     - function decls need to be fixed
     - full applications need to be fixed
     - tail calls need to be fixed
-- closed term static initializers
 -/
 
 def leanMainFn := "_lean_main"
@@ -538,12 +537,14 @@ def emitFnDecls : M llvmctx Unit := do
   let env ← getEnv
   let decls := getDecls env
   let modDecls  : NameSet := decls.foldl (fun s d => s.insert d.name) {}
-  let usedDecls := collectUsedDecls env decls
-  usedDecls.forM fun n => do
-    let decl ← getDecl n;
+  let usedDecls : NameSet := decls.foldl (fun s d => collectUsedDecls env d (s.insert d.name)) {}
+  let usedDecls := usedDecls.toList
+  for n in usedDecls do
+    let decl ← getDecl n
     match getExternNameFor env `c decl.name with
     | some cName => emitExternDeclAux decl cName
     | none       => emitFnDecl decl (!modDecls.contains n)
+  return ()
 
 def emitLhsSlot_ (x : VarId) : M llvmctx (LLVM.LLVMType llvmctx × LLVM.Value llvmctx) := do
   let state ← get

src/Lean/Compiler/IR/EmitUtil.lean

@@ -25,19 +25,10 @@ def usesModuleFrom (env : Environment) (modulePrefix : Name) : Bool :=
 
 namespace CollectUsedDecls
 
-structure State where
-  set : NameSet := {}
-  order : Array Name := #[]
-
-abbrev M := ReaderT Environment (StateM State)
+abbrev M := ReaderT Environment (StateM NameSet)
 
 @[inline] def collect (f : FunId) : M Unit :=
-  modify fun { set, order } =>
-    let (contained, set) := set.containsThenInsert f
-    if !contained then
-      { set, order := order.push f }
-    else
-      { set, order }
+  modify fun s => s.insert f
 
 partial def collectFnBody : FnBody → M Unit
   | .vdecl _ _ v b   =>
@@ -55,19 +46,14 @@ def collectInitDecl (fn : Name) : M Unit := do
   | some initFn => collect initFn
   | _           => pure ()
 
-def collectDecl : Decl → M Unit
-  | .fdecl (f := f) (body := b) .. => collectInitDecl f *> CollectUsedDecls.collectFnBody b
-  | .extern (f := f) .. => collectInitDecl f
-
-def collectDeclLoop (decls : List Decl) : M Unit := do
-  decls.forM fun decl => do
-    collectDecl decl
-    collect decl.name
+def collectDecl : Decl → M NameSet
+  | .fdecl (f := f) (body := b) .. => collectInitDecl f *> CollectUsedDecls.collectFnBody b *> get
+  | .extern (f := f) .. => collectInitDecl f *> get
 
 end CollectUsedDecls
 
-def collectUsedDecls (env : Environment) (decls : List Decl) : Array Name :=
-  (CollectUsedDecls.collectDeclLoop decls env).run {} |>.snd.order
+def collectUsedDecls (env : Environment) (decl : Decl) (used : NameSet := {}) : NameSet :=
+  (CollectUsedDecls.collectDecl decl env).run' used
 
 abbrev VarTypeMap  := Std.HashMap VarId IRType
 abbrev JPParamsMap := Std.HashMap JoinPointId (Array Param)

src/Lean/Compiler/IR/SimpleGroundExpr.lean

@@ -1,355 +0,0 @@
-/-
-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.IR.CompilerM
-public import Lean.EnvExtension
-import Lean.Compiler.ClosedTermCache
-
-/-!
-This module contains logic for detecting simple ground expressions that can be extracted into
-statically initializable variables. To do this it attempts to compile declarations into
-a simple language of expressions, `SimpleGroundExpr`. If this attempt succeeds it stores the result
-in an environment extension, accessible through `getSimpleGroundExpr`. Later on the code emission
-step can reference this environment extension to generate static initializers for the respective
-declaration.
--/
-
-namespace Lean
-
-namespace IR
-
-/--
-An argument to a `SimpleGroundExpr`. They get compiled to `lean_object*` in various ways.
--/
-public inductive SimpleGroundArg where
-  /--
-  A simple tagged literal.
-  -/
-  | tagged (val : Nat)
-  /--
-  A reference to another declaration that was marked as a simple ground expression. This gets
-  compiled to a reference to the mangled version of the name.
-  -/
-  | reference (n : Name)
-  /--
-  A reference directly to a raw C name. This gets compiled to a reference to the name directly.
-  -/
-  | rawReference (s : String)
-  deriving Inhabited
-
-/--
-A simple ground expression that can be turned into a static initializer.
--/
-public inductive SimpleGroundExpr where
-  /--
-  Represents a `lean_ctor_object`. Crucially the `scalarArgs` array must have a size that is a
-  multiple of 8.
-  -/
-  | ctor (cidx : Nat) (objArgs : Array SimpleGroundArg) (usizeArgs : Array USize) (scalarArgs : Array UInt8)
-  /--
-  A string literal, represented by a `lean_string_object`.
-  -/
-  | string (data : String)
-  /--
-  A partial application, represented by a `lean_closure_object`.
-  -/
-  | pap (func : FunId) (args : Array SimpleGroundArg)
-  /--
-  An application of `Lean.Name.mkStrX`. This expression is represented separately to ensure that
-  long name literals get extracted into statically initializable constants. The arguments contain
-  both the name of the string literal it references as well as the hash of the name up to that
-  point. This is done to make emitting the literal as simple as possible.
-  -/
-  | nameMkStr (args : Array (Name × UInt64))
-  /--
-  A reference to another declaration that was marked as a simple ground expression. This gets
-  compiled to a reference to the mangled version of the name.
-  -/
-  | reference (n : Name)
-  deriving Inhabited
-
-public structure SimpleGroundExtState where
-  constNames : PHashMap Name SimpleGroundExpr := {}
-  revNames : List Name := []
-  deriving Inhabited
-
-builtin_initialize simpleGroundDeclExt : EnvExtension SimpleGroundExtState ←
-  registerEnvExtension (pure {}) (asyncMode := .sync)
-    (replay? := some fun oldState newState _ s =>
-      let newNames := newState.revNames.take (newState.revNames.length - oldState.revNames.length)
-      newNames.foldl (init := s) fun s n =>
-        let g := newState.constNames.find! n
-        { s with constNames := s.constNames.insert n g, revNames := n :: s.revNames }
-    )
-
-/--
-Record `declName` as mapping to the simple ground expr `expr`.
--/
-public def addSimpleGroundDecl (env : Environment) (declName : Name) (expr : SimpleGroundExpr) :
-    Environment :=
-  simpleGroundDeclExt.modifyState env fun s =>
-    { s with constNames := s.constNames.insert declName expr, revNames := declName :: s.revNames }
-
-/--
-Attempt to fetch a `SimpleGroundExpr` associated with `declName` if it exists.
--/
-public def getSimpleGroundExpr (env : Environment) (declName : Name) : Option SimpleGroundExpr :=
-  (simpleGroundDeclExt.getState env).constNames.find? declName
-
-/--
-Like `getSimpleGroundExpr` but recursively traverses `reference` exprs to get to actual ground
-values.
--/
-public def getSimpleGroundExprWithResolvedRefs (env : Environment) (declName : Name) :
-    Option SimpleGroundExpr := Id.run do
-  let mut declName := declName
-  while true do
-    let val := getSimpleGroundExpr env declName
-    match val with
-    | some (.reference ref) => declName := ref
-    | other => return other
-  return none
-
-/--
-Check if `declName` is recorded as being a `SimpleGroundExpr`.
--/
-public def isSimpleGroundDecl (env : Environment) (declName : Name) : Bool :=
-  (simpleGroundDeclExt.getState env).constNames.contains declName
-
-public def uint64ToByteArrayLE (n : UInt64) : Array UInt8 :=
-  #[
-    n.toUInt8,
-    (n >>> 0x08).toUInt8,
-    (n >>> 0x10).toUInt8,
-    (n >>> 0x18).toUInt8,
-    (n >>> 0x20).toUInt8,
-    (n >>> 0x28).toUInt8,
-    (n >>> 0x30).toUInt8,
-    (n >>> 0x38).toUInt8,
-  ]
-
-
-inductive SimpleGroundValue where
-  | arg (arg : SimpleGroundArg)
-  | uint8 (val : UInt8)
-  | uint16 (val : UInt16)
-  | uint32 (val : UInt32)
-  | uint64 (val : UInt64)
-  | usize (val : USize)
-  deriving Inhabited
-
-structure State where
-  groundMap : Std.HashMap VarId SimpleGroundValue := {}
-
-abbrev M := StateRefT State $ OptionT CompilerM
-
-/--
-Attempt to compile `b` into a `SimpleGroundExpr`. If `b` is not compileable return `none`.
-
-The compiler currently supports the following patterns:
-- String literals
-- Partial applications with other simple expressions
-- Constructor calls with other simple expressions
-- `Name.mkStrX`, `Name.str._override`, and `Name.num._override`
-- references to other declarations marked as simple ground expressions
--/
-partial def compileToSimpleGroundExpr (b : FnBody) : CompilerM (Option SimpleGroundExpr) :=
-  compileFnBody b |>.run' {} |>.run
-where
-  compileFnBody (b : FnBody) : M SimpleGroundExpr := do
-    match b with
-    | .vdecl id _ expr (.ret (.var id')) =>
-      guard <| id == id'
-      compileFinalExpr expr
-    | .vdecl id ty expr b => compileNonFinalExpr id ty expr b
-    | _ => failure
-
-  @[inline]
-  record (id : VarId) (val : SimpleGroundValue) : M Unit :=
-    modify fun s => { s with groundMap := s.groundMap.insert id val }
-
-  compileNonFinalExpr (id : VarId) (ty : IRType) (expr : Expr) (b : FnBody) : M SimpleGroundExpr := do
-    match expr with
-    | .fap c #[] =>
-      guard <| isSimpleGroundDecl (← getEnv) c
-      record id (.arg (.reference c))
-      compileFnBody b
-    | .lit v =>
-      match v with
-      | .num v =>
-        match ty with
-        | .tagged =>
-          guard <| v < 2^31
-          record id (.arg (.tagged v))
-        | .uint8 => record id (.uint8 (.ofNat v))
-        | .uint16 => record id (.uint16 (.ofNat v))
-        | .uint32 => record id (.uint32 (.ofNat v))
-        | .uint64 => record id (.uint64 (.ofNat v))
-        | .usize => record id (.usize (.ofNat v))
-        | _ => failure
-        compileFnBody b
-      | .str .. => failure
-    | .ctor i objArgs =>
-      if i.isScalar then
-        record id (.arg (.tagged i.cidx))
-        compileFnBody b
-      else
-        let objArgs ← compileArgs objArgs
-        let usizeArgs := Array.replicate i.usize 0
-        -- Align to 8 bytes for alignment with lean_object*
-        let align (v a : Nat) : Nat :=
-          (v / a) * a + a * (if v % a != 0 then 1 else 0)
-        let alignedSsize := align i.ssize 8
-        let ssizeArgs := Array.replicate alignedSsize 0
-        compileSetChain id i objArgs usizeArgs ssizeArgs b
-    | _ => failure
-
-  compileSetChain (id : VarId) (info : CtorInfo) (objArgs : Array SimpleGroundArg) (usizeArgs : Array USize)
-      (scalarArgs : Array UInt8) (b : FnBody) : M SimpleGroundExpr := do
-    match b with
-    | .ret (.var id') =>
-      guard <| id == id'
-      return .ctor info.cidx objArgs usizeArgs scalarArgs
-    | .sset id' i offset y _ b =>
-      guard <| id == id'
-      let i := i - objArgs.size - usizeArgs.size
-      let offset := i * 8 + offset
-      let scalarArgs ←
-        match (← get).groundMap[y]! with
-        | .uint8 v =>
-          let scalarArgs := scalarArgs.set! offset v
-          pure scalarArgs
-        | .uint16 v =>
-          let scalarArgs := scalarArgs.set! offset v.toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 1) (v >>> 0x08).toUInt8
-          pure scalarArgs
-        | .uint32 v =>
-          let scalarArgs := scalarArgs.set! offset v.toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 1) (v >>> 0x08).toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 2) (v >>> 0x10).toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 3) (v >>> 0x18).toUInt8
-          pure scalarArgs
-        | .uint64 v =>
-          let scalarArgs := scalarArgs.set! offset v.toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 1) (v >>> 0x08).toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 2) (v >>> 0x10).toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 3) (v >>> 0x18).toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 4) (v >>> 0x20).toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 5) (v >>> 0x28).toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 6) (v >>> 0x30).toUInt8
-          let scalarArgs := scalarArgs.set! (offset + 7) (v >>> 0x38).toUInt8
-          pure scalarArgs
-        | _ => failure
-      compileSetChain id info objArgs usizeArgs scalarArgs b
-    | .uset id' i y b =>
-      guard <| id == id'
-      let i := i - objArgs.size
-      let .usize v := (← get).groundMap[y]! | failure
-      let usizeArgs := usizeArgs.set! i v
-      compileSetChain id info objArgs usizeArgs scalarArgs b
-    | _ => failure
-
-  compileFinalExpr (e : Expr) : M SimpleGroundExpr := do
-    match e with
-    | .lit v =>
-      match v with
-      | .str v => return .string v
-      | .num .. => failure
-    | .ctor i args =>
-      guard <| i.usize == 0 && i.ssize == 0 && !args.isEmpty
-      return .ctor i.cidx (← compileArgs args) #[] #[]
-    | .fap ``Name.num._override args =>
-      let pre ← compileArg args[0]!
-      let .tagged i ← compileArg args[1]! | failure
-      let name := Name.num (← interpNameLiteral pre) i
-      let hash := name.hash
-      return .ctor 2 #[pre, .tagged i] #[] (uint64ToByteArrayLE hash)
-    | .fap ``Name.str._override args =>
-      let pre ← compileArg args[0]!
-      let (ref, str) ← compileStrArg args[1]!
-      let name := Name.str (← interpNameLiteral pre) str
-      let hash := name.hash
-      return .ctor 1 #[pre, .reference ref] #[] (uint64ToByteArrayLE hash)
-    | .fap ``Name.mkStr1 args
-    | .fap ``Name.mkStr2 args
-    | .fap ``Name.mkStr3 args
-    | .fap ``Name.mkStr4 args
-    | .fap ``Name.mkStr5 args
-    | .fap ``Name.mkStr6 args
-    | .fap ``Name.mkStr7 args
-    | .fap ``Name.mkStr8 args =>
-      let mut nameAcc := Name.anonymous
-      let mut processedArgs := Array.emptyWithCapacity args.size
-      for arg in args do
-        let (ref, str) ← compileStrArg arg
-        nameAcc := .str nameAcc str
-        processedArgs := processedArgs.push (ref, nameAcc.hash)
-      return .nameMkStr processedArgs
-    | .pap c ys => return .pap c (← compileArgs ys)
-    | .fap c #[] =>
-      guard <| isSimpleGroundDecl (← getEnv) c
-      return .reference c
-    | _ => failure
-
-  compileArg (arg : Arg) : M SimpleGroundArg := do
-    match arg with
-    | .var var =>
-      let .arg arg := (← get).groundMap[var]! | failure
-      return arg
-    | .erased => return .tagged 0
-
-  compileArgs (args : Array Arg) : M (Array SimpleGroundArg) := do
-    args.mapM compileArg
-
-  compileStrArg (arg : Arg) : M (Name × String) := do
-    let .var var := arg | failure
-    let (.arg (.reference ref)) := (← get).groundMap[var]! | failure
-    let some (.string val) := getSimpleGroundExprWithResolvedRefs (← getEnv) ref | failure
-    return (ref, val)
-
-  interpStringLiteral (arg : SimpleGroundArg) : M String := do
-    let .reference ref := arg | failure
-    let some (.string val) := getSimpleGroundExprWithResolvedRefs (← getEnv) ref | failure
-    return val
-
-  interpNameLiteral (arg : SimpleGroundArg) : M Name := do
-    match arg with
-    | .tagged 0 => return .anonymous
-    | .reference ref =>
-      match getSimpleGroundExprWithResolvedRefs (← getEnv) ref with
-      | some (.ctor 1 #[pre, .reference ref] _ _) =>
-        let pre ← interpNameLiteral pre
-        let str ← interpStringLiteral (.reference ref)
-        return .str pre str
-      | some (.ctor 2 #[pre, .tagged i] _ _) =>
-        let pre ← interpNameLiteral pre
-        return .num pre i
-      | some (.nameMkStr args) =>
-        args.foldlM (init := .anonymous) fun acc (ref, _) => do
-          let part ← interpStringLiteral (.reference ref)
-          return .str acc part
-      | _ => failure
-    | _ => failure
-
-
-/--
-Detect whether `d` can be compiled to a `SimpleGroundExpr`. If it can record the associated
-`SimpleGroundExpr` into the environment for later processing by code emission.
--/
-public def Decl.detectSimpleGround (d : Decl) : CompilerM Unit := do
-  let .fdecl (body := body) (xs := params) (type := type) .. := d | return ()
-  if type.isPossibleRef && params.isEmpty then
-    if let some groundExpr ← compileToSimpleGroundExpr body then
-      trace[compiler.ir.simple_ground] m!"Marked {d.name} as simple ground expr"
-      modifyEnv fun env => addSimpleGroundDecl env d.name groundExpr
-
-builtin_initialize registerTraceClass `compiler.ir.simple_ground (inherited := true)
-
-end IR
-
-end Lean

src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean

@@ -82,27 +82,13 @@ def elabMPureIntro : Tactic
     replaceMainGoal [mv]
   | _ => throwUnsupportedSyntax
 
-private def extractPureProp (e : Expr) : MetaM (Option Expr) := do
-  let e ← instantiateMVarsIfMVarApp e
-  let some (_, e) := e.app2? ``ULift.down | return none
-  let f := e.getAppFn
-  unless f.isConstOf ``SPred.pure do return none
-  let args := e.getAppArgs
-  if args.size < 2 then return none
-  let σs := args[0]!
-  let n ← TypeList.length σs
-  unless n = args.size - 2 do return none
-  let p := args[1]!
-  return p
-
 partial def _root_.Lean.MVarId.applyRflAndAndIntro (mvar : MVarId) : MetaM Unit := do
-  -- The target might look like `(⌜nₛ = ?n ∧ ?m = b⌝ s).down`, which we reduce to
-  -- `nₛ = ?n ∧ ?m = b` with `extractPureProp`.
+  -- The target might look like `(⌜?n = nₛ ∧ ?m = b⌝ s).down`, which we reduce to
+  -- `?n = nₛ ∧ ?m = b` by `whnfD`.
   -- (Recall that `⌜s = 4⌝ s` is `SPred.pure (σs:=[Nat]) (s = 4) s` and `SPred.pure` is
   -- semi-reducible.)
-  let ty ← mvar.getType >>= instantiateMVarsIfMVarApp
-  let ty ← (·.getD ty) <$> extractPureProp ty
-  trace[Elab.Tactic.Do.spec] "pure Prop: {ty}"
+  let ty ← whnfD (← mvar.getType)
+  trace[Elab.Tactic.Do.spec] "whnf: {ty}"
   if ty.isAppOf ``True then
     mvar.assign (mkConst ``True.intro)
   else if let some (lhs, rhs) := ty.app2? ``And then
@@ -141,3 +127,16 @@ def MGoal.pureTrivial (goal : MGoal) : OptionT MetaM Expr := do
       return ((), m)
     return prf
   catch _ => failure
+
+/-
+def MGoal.pureRfl (goal : MGoal) : OptionT MetaM Expr := do
+  let mv ← mkFreshExprMVar goal.toExpr
+  let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); rfl)) catch _ => failure
+    | failure
+  return mv
+def MGoal.pureRfl (goal : MGoal) : OptionT MetaM Expr := do
+  let mv ← mkFreshExprMVar goal.toExpr
+  let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); rfl)) catch _ => failure
+    | failure
+  return mv
+-/

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

@@ -209,8 +209,8 @@ def SuccessPoint.clause (p : SuccessPoint) : Expr :=
 
 /-- The last syntactic element of a `FailureCond`. -/
 inductive ExceptCondsDefault where
-  /-- `PUnit.unit`. This means we can suggest `post⟨...⟩`. -/
-  | punit
+  /-- `()`. This means we can suggest `post⟨...⟩`. -/
+  | unit
   /-- `ExceptConds.false`. This means we can suggest `⇓ _ => _`. -/
   | false
   /-- `ExceptConds.true`. This means we can suggest `⇓? _ => _`. -/
@@ -229,7 +229,7 @@ When the default is not defeq to `ExceptConds.false`, we use it as the default.
 -/
 structure FailureCondHints where
   points : Array Expr := #[]
-  default : ExceptCondsDefault := .punit
+  default : ExceptCondsDefault := .unit
 
 /-- Look at how `inv` is used in the `vcs` and collect hints about how `inv` should be instantiated.
 In case it succeeds, there will be
@@ -293,8 +293,8 @@ def collectInvariantHints (vcs : Array MVarId) (inv : MVarId) (xs : Expr) (letMu
         -- Just overwrite the existing entry. Computing a join here is overkill for the few cases
         -- where this is going to be used.
         failureConds := { failureConds with points := points }
-        if conds.isConstOf ``PUnit.unit then
-          failureConds := { failureConds with default := .punit }
+        if conds.isConstOf ``Unit.unit then
+          failureConds := { failureConds with default := .unit }
         else if conds.isAppOfArity ``ExceptConds.false 1 then
           failureConds := { failureConds with default := .false }
         else if conds.isAppOfArity ``ExceptConds.true 1 then
@@ -402,8 +402,8 @@ public def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term :
   -- 2. However, on early return we want to suggest something using `Invariant.withEarlyReturn`.
   -- 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`).
+  --    or `post⟨...⟩` (more than 0 failure handlers, but ending in `()`), and fall back to
+  --    `by exact ⟨...⟩` (not ending in `()`).
   -- 4. Similarly for the `onExcept` argument of `Invariant.withEarlyReturn`.
   -- Hence the spaghetti code.
   --
@@ -429,7 +429,7 @@ public def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term :
       -- Now the configuration mess.
       if failureConds.points.isEmpty then
         match failureConds.default with
-        | .false | .punit =>
+        | .false | .unit =>
           `(Invariant.withEarlyReturn (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 _`.
@@ -469,7 +469,7 @@ where
   postCondWithMultipleConditions (handlers : Array Term) (default : ExceptCondsDefault) : MetaM Term := do
     let handlers := Syntax.TSepArray.ofElems (sep := ",") handlers
     match default with
-    | .punit => `(post⟨$handlers,*⟩)
+    | .unit => `(post⟨$handlers,*⟩)
     -- See the comment in `post⟨_⟩` syntax for why we emit `by exact` here.
     | .false => `(by exact ⟨$handlers,*, ExceptConds.false⟩)
     | .true => `(by exact ⟨$handlers,*, ExceptConds.true⟩)

src/Lean/LibrarySuggestions/Basic.lean

@@ -66,7 +66,7 @@ unsafe def fold {α : Type} (f : Name → α → MetaM α) (e : Expr) (acc : α)
     | .app f a           =>
       let fi ← getFunInfo f (some 1)
       if fi.paramInfo[0]!.isInstImplicit then
-        -- Don't visit instance implicit arguments.
+        -- Don't visit implicit arguments.
         visit f acc
       else
         visit a (← visit f acc)

src/Lean/Meta/Injective.lean

@@ -139,14 +139,13 @@ private partial def andProjections (e : Expr) : MetaM (Array Expr) := do
       return acc.push e
   go e (← inferType e) #[]
 
-private def mkInjectiveEqTheoremValue (ctorVal : ConstructorVal) (targetType : Expr) : MetaM Expr := do
+private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : MetaM Expr := do
   forallTelescopeReducing targetType fun xs type => do
     let mvar ← mkFreshExprSyntheticOpaqueMVar type
     let [mvarId₁, mvarId₂] ← mvar.mvarId!.apply (mkConst ``Eq.propIntro)
-      | throwError "unexpected number of subgoals when proving injective theorem for constructor `{ctorVal.name}`"
-    let injPrf := mkConst (mkInjectiveTheoremNameFor ctorVal.name) (ctorVal.levelParams.map mkLevelParam)
-    let injPrf := mkAppN injPrf xs
-    mvarId₁.assign injPrf
+      | throwError "unexpected number of subgoals when proving injective theorem for constructor `{ctorName}`"
+    let (h, mvarId₁) ← mvarId₁.intro1
+    solveEqOfCtorEq ctorName mvarId₁ h
     let mut mvarId₂ := mvarId₂
     while true do
       let t ← mvarId₂.getType
@@ -159,7 +158,7 @@ private def mkInjectiveEqTheoremValue (ctorVal : ConstructorVal) (targetType : E
       | _ => pure ()
       let (h, mvarId₂') ← mvarId₂.intro1
       (_, mvarId₂) ← substEq mvarId₂' h
-    try mvarId₂.refl catch _ => throwError (injTheoremFailureHeader ctorVal.name)
+    try mvarId₂.refl catch _ => throwError (injTheoremFailureHeader ctorName)
     mkLambdaFVars xs mvar
 
 private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
@@ -168,7 +167,7 @@ private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
   let some type ← mkInjectiveEqTheoremType? ctorVal
     | return ()
   trace[Meta.injective] "type: {type}"
-  let value ← mkInjectiveEqTheoremValue ctorVal type
+  let value ← mkInjectiveEqTheoremValue ctorVal.name type
   addDecl <| Declaration.thmDecl {
     name
     levelParams := ctorVal.levelParams

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -292,8 +292,9 @@ def transform
     let aux1 := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) params'
     let aux1 := mkApp aux1 motive'
     let aux1 := mkAppN aux1 discrs'
-    prependError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}\nfailed with" do
-      check aux1
+    unless (← isTypeCorrect aux1) do
+      prependError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}\nfailed with" do
+        check aux1
     let origAltTypes ← inferArgumentTypesN matcherApp.alts.size aux1
 
     -- We replace the matcher with the splitter
@@ -303,8 +304,9 @@ def transform
     let aux2 := mkAppN (mkConst splitter matcherLevels.toList) params'
     let aux2 := mkApp aux2 motive'
     let aux2 := mkAppN aux2 discrs'
-    prependError m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}\nfailed with" do
-      check aux2
+    unless (← isTypeCorrect aux2) do
+      prependError m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}\nfailed with" do
+        check aux2
     let altTypes ← inferArgumentTypesN matcherApp.alts.size aux2
 
     let mut alts' := #[]
@@ -357,7 +359,8 @@ def transform
     let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) params'
     let aux := mkApp aux motive'
     let aux := mkAppN aux discrs'
-    prependError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux}" do
+    unless (← isTypeCorrect aux) do
+      logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux}"
       check aux
     let altTypes ← inferArgumentTypesN matcherApp.alts.size aux
 

src/Lean/Meta/Sym.lean

@@ -23,7 +23,6 @@ public import Lean.Meta.Sym.Apply
 public import Lean.Meta.Sym.InferType
 public import Lean.Meta.Sym.Simp
 public import Lean.Meta.Sym.Util
-public import Lean.Meta.Sym.Eta
 public import Lean.Meta.Sym.Grind
 
 /-!

src/Lean/Meta/Sym/Eta.lean

@@ -1,53 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.ExprPtr
-public import Lean.Meta.Basic
-import Lean.Meta.Transform
-namespace Lean.Meta.Sym
-/--
-Checks if `body` is eta-expanded with `n` applications: `f (.bvar (n-1)) ... (.bvar 0)`.
-Returns `f` if so and `f` has no loose bvars; otherwise returns `default`.
-- `n`: number of remaining applications to check
-- `i`: expected bvar index (starts at 0, increments with each application)
-- `default`: returned when not eta-reducible (enables pointer equality check)
--/
-def etaReduceAux (body : Expr) (n : Nat) (i : Nat) (default : Expr) : Expr := Id.run do
-  match n with
-  | 0 => if body.hasLooseBVars then default else body
-  | n+1 =>
-    let .app f (.bvar j) := body | default
-    if j == i then etaReduceAux f n (i+1) default else default
-
-/--
-If `e` is of the form `(fun x₁ ... xₙ => f x₁ ... xₙ)` and `f` does not contain `x₁`, ..., `xₙ`,
-then returns `f`. Otherwise, returns `e`.
-
-Returns the original expression when not reducible to enable pointer equality checks.
--/
-public def etaReduce (e : Expr) : Expr :=
-  go e 0
-where
-  go (body : Expr) (n : Nat) : Expr :=
-    match body with
-    | .lam _ _ b _ => go b (n+1)
-    | _ => if n == 0 then e else etaReduceAux body n 0 e
-
-/-- Returns `true` if `e` can be eta-reduced. Uses pointer equality for efficiency. -/
-public def isEtaReducible (e : Expr) : Bool :=
-  !isSameExpr e (etaReduce e)
-
-/-- Applies `etaReduce` to all subexpressions. Returns `e` unchanged if no subexpression is eta-reducible. -/
-public def etaReduceAll (e : Expr) : MetaM Expr := do
-  unless Option.isSome <| e.find? isEtaReducible do return e
-  let pre (e : Expr) : MetaM TransformStep := do
-    let e' := etaReduce e
-    if isSameExpr e e' then return .continue
-    else return .visit e'
-  Meta.transform e (pre := pre)
-
-end Lean.Meta.Sym

src/Lean/Meta/Sym/Pattern.lean

@@ -18,7 +18,6 @@ import Lean.Meta.Sym.ProofInstInfo
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.LitValues
 import Lean.Meta.Sym.Offset
-import Lean.Meta.Sym.Eta
 namespace Lean.Meta.Sym
 open Internal
 
@@ -324,11 +323,7 @@ def isAssignedMVar (e : Expr) : MetaM Bool :=
   | _            => return false
 
 partial def process (p : Expr) (e : Expr) : UnifyM Bool := do
-  let e' := etaReduce e
-  if !isSameExpr e e' then
-    -- **Note**: We eagerly eta reduce patterns
-    process p e'
-  else match p with
+  match p with
   | .bvar bidx => assignExpr bidx e
   | .mdata _ p => process p e
   | .const declName us =>
@@ -728,12 +723,7 @@ def isDefEqApp (tFn : Expr) (t : Expr) (s : Expr) (_ : tFn = t.getAppFn) : DefEq
 @[export lean_sym_def_eq]
 def isDefEqMainImpl (t : Expr) (s : Expr) : DefEqM Bool := do
   if isSameExpr t s then return true
-  -- **Note**: `etaReduce` is supposed to be fast, and does not allocate memory
-  let t' := etaReduce t
-  let s' := etaReduce s
-  if !isSameExpr t t' || !isSameExpr s s' then
-    isDefEqMain t' s'
-  else match t, s with
+  match t, s with
   | .lit  l₁,      .lit l₂       => return l₁ == l₂
   | .sort u,       .sort v       => isLevelDefEqS u v
   | .lam ..,       .lam ..       => isDefEqBindingS t s

src/Lean/Meta/Sym/ProofInstInfo.lean

@@ -9,7 +9,6 @@ public import Lean.Meta.Sym.SymM
 import Lean.Meta.Sym.IsClass
 import Lean.Meta.Sym.Util
 import Lean.Meta.Transform
-import Lean.Meta.Sym.Eta
 namespace Lean.Meta.Sym
 
 /--
@@ -18,8 +17,7 @@ Preprocesses types that used for pattern matching and unification.
 public def preprocessType (type : Expr) : MetaM Expr := do
   let type ← Sym.unfoldReducible type
   let type ← Core.betaReduce type
-  let type ← zetaReduce type
-  etaReduceAll type
+  zetaReduce type
 
 /--
 Analyzes whether the given free variables (aka arguments) are proofs or instances.

src/Lean/Meta/Sym/Simp.lean

@@ -22,4 +22,3 @@ public import Lean.Meta.Sym.Simp.EvalGround
 public import Lean.Meta.Sym.Simp.Discharger
 public import Lean.Meta.Sym.Simp.ControlFlow
 public import Lean.Meta.Sym.Simp.Goal
-public import Lean.Meta.Sym.Simp.Telescope

src/Lean/Meta/Sym/Simp/ControlFlow.lean

@@ -27,16 +27,16 @@ def simpIte : Simproc := fun e => do
     let_expr f@ite α c _ a b := e | return .rfl
     match (← simp c) with
     | .rfl _ =>
-      if (← isTrueExpr c) then
+      if isSameExpr c (← getTrueExpr) then
         return .step a <| mkApp3 (mkConst ``ite_true f.constLevels!) α a b
-      else if (← isFalseExpr  c) then
+      else if isSameExpr c (← getFalseExpr) then
         return .step b <| mkApp3 (mkConst ``ite_false f.constLevels!) α a b
       else
         return .rfl (done := true)
     | .step c' h _ =>
-      if (← isTrueExpr c') then
+      if isSameExpr c' (← getTrueExpr) then
         return .step a <| mkApp (e.replaceFn ``ite_cond_eq_true) h
-      else if (← isFalseExpr c') then
+      else if isSameExpr c' (← getFalseExpr) then
         return .step b <| mkApp (e.replaceFn ``ite_cond_eq_false) h
       else
         let .some inst' ← trySynthInstance (mkApp (mkConst ``Decidable) c') | return .rfl
@@ -56,20 +56,20 @@ def simpDIte : Simproc := fun e => do
     let_expr f@dite α c _ a b := e | return .rfl
     match (← simp c) with
     | .rfl _ =>
-      if (← isTrueExpr c) then
+      if isSameExpr c (← getTrueExpr) then
         let a' ← share <| a.betaRev #[mkConst ``True.intro]
         return .step a' <| mkApp3 (mkConst ``dite_true f.constLevels!) α a b
-      else if (← isFalseExpr c) then
+      else if isSameExpr c (← getFalseExpr) then
         let b' ← share <| b.betaRev #[mkConst ``not_false]
         return .step b' <| mkApp3 (mkConst ``dite_false f.constLevels!) α a b
       else
         return .rfl (done := true)
     | .step c' h _ =>
-      if (← isTrueExpr c') then
+      if isSameExpr c' (← getTrueExpr) then
         let h' ← shareCommon <| mkOfEqTrueCore c h
         let a ← share <| a.betaRev #[h']
         return .step a <| mkApp (e.replaceFn ``dite_cond_eq_true) h
-      else if (← isFalseExpr c') then
+      else if isSameExpr c' (← getFalseExpr) then
         let h' ← shareCommon <| mkOfEqFalseCore c h
         let b ← share <| b.betaRev #[h']
         return .step b <| mkApp (e.replaceFn ``dite_cond_eq_false) h

src/Lean/Meta/Sym/Simp/Forall.lean

@@ -7,8 +7,6 @@ module
 prelude
 public import Lean.Meta.Sym.Simp.SimpM
 import Lean.Meta.Sym.AlphaShareBuilder
-import Lean.Meta.Sym.InferType
-import Lean.Meta.Sym.Simp.Result
 namespace Lean.Meta.Sym.Simp
 
 /--
@@ -27,7 +25,7 @@ The proof uses the approach used in `mkFunextFor` followed by an `Eq.ndrec`.
 def mkForallCongrFor (xs : Array Expr) : MetaM Expr := do
   let prop := mkSort 0
   let type ← mkForallFVars xs prop
-  let w ← Meta.getLevel type
+  let w ← getLevel type
   withLocalDeclD `p type fun p =>
   withLocalDeclD `q type fun q => do
   let eq := mkApp3 (mkConst ``Eq [1]) prop (mkAppN p xs) (mkAppN q xs)
@@ -55,119 +53,6 @@ def mkForallCongrFor (xs : Array Expr) : MetaM Expr := do
 
 open Internal
 
-structure ArrowInfo where
-  binderName : Name
-  binderInfo : BinderInfo
-  u          : Level
-  v          : Level
-
-structure ToArrowResult where
-  arrow : Expr
-  infos : List ArrowInfo
-  v     : Level
-
-def toArrow (e : Expr) : SymM ToArrowResult := do
-  if let .forallE n α β bi := e then
-    if !β.hasLooseBVars then
-      let { arrow, infos, v } ← toArrow β
-      let u ← getLevel α
-      let arrow ← mkAppS₂ (← mkConstS ``Arrow [u, v]) α arrow
-      let info := { binderName := n, binderInfo := bi, u, v }
-      return { arrow, v := mkLevelIMax' u v, infos := info :: infos }
-  return { arrow := e, infos := [], v := (← getLevel e) }
-
-def toForall (e : Expr) (infos : List ArrowInfo) : SymM Expr := do
-  let { binderName, binderInfo, .. } :: infos := infos | return e
-  let_expr Arrow α β := e | return e
-  mkForallS binderName binderInfo α (← toForall β infos)
-
-/--
-Recursively simplifies an `Arrow` telescope, applying telescope-specific simplifications:
-
-- **False hypothesis**: `False → q` simplifies to `True` (via `false_arrow`)
-- **True hypothesis**: `True → q` simplifies to `q` (via `true_arrow`)
-- **True conclusion**: `p → True` simplifies to `True` (via `arrow_true`)
-
-The first two are applicable only if  `q` is in `Prop` (checked via `info.v.isZero`).
-
-Returns the simplified result paired with the remaining `ArrowInfo` list. When a telescope
-collapses (e.g., to `True`), the returned `infos` list is empty, signaling to `toForall`
-that no reconstruction is needed.
--/
-partial def simpArrows (e : Expr) (infos : List ArrowInfo) (simpBody : Simproc) : SimpM (Result × List ArrowInfo) := do
-  match infos with
-  | [] => return ((← simpBody e), [])
-  | info :: infos' =>
-    let_expr f@Arrow p q := e | return ((← simpBody e), infos)
-    let p_r ← simp p
-    if (← isFalseExpr (p_r.getResultExpr p)) && info.v.isZero then
-      match p_r with
-      | .rfl _ => return (.step (← getTrueExpr) (mkApp (mkConst ``false_arrow) q), [])
-      | .step _ h _ => return (.step (← getTrueExpr) (mkApp3 (mkConst ``false_arrow_congr) p q h), [])
-    let (q_r, infos') ← simpArrows q infos' simpBody
-    if (← isTrueExpr (q_r.getResultExpr q)) then
-      match q_r with
-      | .rfl _ => return (.step (← getTrueExpr) (mkApp (mkConst ``arrow_true [info.u]) p), [])
-      | .step _ h _ => return (.step (← getTrueExpr) (mkApp3 (mkConst ``arrow_true_congr [info.u]) p q h), [])
-    match p_r, q_r with
-    | .rfl _, .rfl _ =>
-      if (← isTrueExpr p) && info.v.isZero then
-        return (.step q (mkApp (mkConst ``true_arrow) q), infos')
-      else
-        return (.rfl, infos)
-    | .step p' h _, .rfl _ =>
-      if (← isTrueExpr p') && info.v.isZero then
-        return (.step q (mkApp3 (mkConst ``true_arrow_congr_left) p q h), infos')
-      else
-        let e' ← mkAppS₂ f p' q
-        return (.step e' <| mkApp4 (mkConst ``arrow_congr_left f.constLevels!) p p' q h, info :: infos')
-    | .rfl _, .step q' h _ =>
-      if (← isTrueExpr p) && info.v.isZero then
-        return (.step q' (mkApp3 (mkConst ``true_arrow_congr_right) q q' h), infos')
-      else
-        let e' ← mkAppS₂ f p q'
-        return (.step e' <| mkApp4 (mkConst ``arrow_congr_right f.constLevels!) p q q' h, info :: infos')
-    | .step p' h₁ _, .step q' h₂ _ =>
-      if (← isTrueExpr p') && info.v.isZero then
-        return (.step q' (mkApp5 (mkConst ``true_arrow_congr) p q q' h₁ h₂), infos')
-      else
-        let e' ← mkAppS₂ f p' q'
-        return (.step e' <| mkApp6 (mkConst ``arrow_congr f.constLevels!) p p' q q' h₁ h₂, info :: infos')
-
-/--
-Simplifies a telescope of non-dependent arrows `p₁ → p₂ → ... → pₙ → q` by:
-1. Converting to `Arrow p₁ (Arrow p₂ (... (Arrow pₙ q)))` (see `toArrow`)
-2. Simplifying each `pᵢ` and `q` (see `simpArrows`)
-3. Converting back to `→` form (see `toForall`)
-
-Using `Arrow` (a definitional wrapper around `→`) avoids the quadratic proof growth that
-occurs with `Expr.forallE`. With `forallE`, each nesting level bumps de Bruijn indices in
-subterms, destroying sharing. For example, if each `pᵢ` contains a free variable `x`, the
-de Bruijn representation of `x` differs at each depth, preventing hash-consing from
-recognizing them as identical.
-
-With `Arrow`, both arguments are explicit (not under binders), so subterms remain identical
-across nesting levels and can be shared, yielding linear-sized proofs.
-
-**Tradeoff**: This function simplifies each `pᵢ` and `q` individually, but misses
-simplifications that depend on the arrow structure itself. For example, `q → p → p`
-won't be simplified to `True` (when `p : Prop`) because the simplifier does not have
-a chance to apply `post` methods to the intermediate arrow `p → p`.
-
-Thus, this is a simproc that is meant to be used as a pre-method and marks the
-result as fully simplified to prevent `simpArrow` from being applied.
--/
-public def simpArrowTelescope (simpBody : Simproc := simp) : Simproc := fun e => do
-  unless e.isArrow do return .rfl -- not applicable
-  let { arrow, infos, v } ← toArrow e
-  let (.step arrow' h _, infos) ← simpArrows arrow infos simpBody | return .rfl (done := true)
-  let e' ← toForall arrow' infos
-  let α := mkSort v
-  let v1 := v.succ
-  let h := mkApp6 (mkConst ``Eq.trans [v1]) α e arrow arrow' (mkApp2 (mkConst ``Eq.refl [v1]) α arrow) h
-  let h := mkApp6 (mkConst ``Eq.trans [v1]) α e arrow' e' h (mkApp2 (mkConst ``Eq.refl [v1]) α e')
-  return .step e' h (done := true)
-
 public def simpArrow (e : Expr) : SimpM Result := do
   let p := e.bindingDomain!
   let q := e.bindingBody!
@@ -190,7 +75,7 @@ public def simpArrow (e : Expr) : SimpM Result := do
     let e' ← e.updateForallS! p' q'
     return .step e' <| mkApp6 (mkConst ``implies_congr [u, v]) p p' q q' h₁ h₂
 
-public def simpForall' (simpArrow : Simproc) (simpBody : Simproc) (e : Expr) : SimpM Result := do
+public def simpForall (e : Expr) : SimpM Result := do
   if e.isArrow then
     simpArrow e
   else if (← isProp e) then
@@ -201,7 +86,7 @@ public def simpForall' (simpArrow : Simproc) (simpBody : Simproc) (e : Expr) : S
     return .rfl
 where
   main (xs : Array Expr) (b : Expr) : SimpM Result := do
-    match (← simpBody b) with
+    match (← simp b) with
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
@@ -216,7 +101,4 @@ where
     | .forallE _ _ b _ => if b.hasLooseBVar 0 then getForallTelescopeSize b (n+1) else n
     | _ => n
 
-public def simpForall : Simproc :=
-  simpForall' simpArrow simp
-
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Simp/Have.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Simp.SimpM
-public import Lean.Meta.Sym.Simp.Lambda
+import Lean.Meta.Sym.Simp.Lambda
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.InstantiateS
 import Lean.Meta.Sym.ReplaceS
@@ -316,8 +316,7 @@ For each application `f a`:
 - If only `a` changed: use `congrArg : a = a' → f a = f a'`
 - If neither changed: return `.rfl`
 -/
-def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level)
-    (simpBody : Simproc) : SimpM Result := do
+def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level) : SimpM Result := do
   return (← go e 0).1
 where
   go (e : Expr) (i : Nat) : SimpM (Result × Expr) := do
@@ -340,7 +339,7 @@ where
           let h := mkApp6 (← mkCongrPrefix ``congr fType i) f f' a a' hf ha
           pure <| .step e' h
       return (r, fType.bindingBody!)
-    | .lam .. => return (← simpBody e, fType)
+    | .lam .. => return (← simpLambda e, fType)
     | _ => unreachable!
 
   mkCongrPrefix (declName : Name) (fType : Expr) (i : Nat) : SymM Expr := do
@@ -376,12 +375,12 @@ e₃ = e₄    (by rfl, definitional equality from toHave)
 e₁ = e₄    (by transitivity)
 ```
 -/
-def simpHaveCore (e : Expr) (simpBody : Simproc) : SimpM SimpHaveResult := do
+def simpHaveCore (e : Expr) : SimpM SimpHaveResult := do
   let e₁ := e
   let r ← toBetaApp e₁
   let e₂ := r.e
   let { fnUnivs, argUnivs } ← getUnivs r.fType
-  match (← simpBetaApp e₂ r.fType fnUnivs argUnivs simpBody) with
+  match (← simpBetaApp e₂ r.fType fnUnivs argUnivs) with
   | .rfl _ => return { result := .rfl, α := r.α, u := r.u }
   | .step e₃ h _ =>
     let h₁ := mkApp6 (mkConst ``Eq.trans [r.u]) r.α e₁ e₂ e₃ r.h h
@@ -398,8 +397,8 @@ Simplify a `have`-telescope.
 This is the main entry point for `have`-telescope simplification in `Sym.simp`.
 See module documentation for the algorithm overview.
 -/
-public def simpHave (e : Expr) (simpBody : Simproc) : SimpM Result := do
-  return (← simpHaveCore e simpBody).result
+public def simpHave (e : Expr) : SimpM Result := do
+  return (← simpHaveCore e).result
 
 /--
 Simplify a `have`-telescope and eliminate unused bindings.
@@ -407,8 +406,8 @@ Simplify a `have`-telescope and eliminate unused bindings.
 This combines simplification with dead variable elimination in a single pass,
 avoiding quadratic behavior from multiple passes.
 -/
-public def simpHaveAndZetaUnused (e₁ : Expr) (simpBody : Simproc) : SimpM Result := do
-  let r ← simpHaveCore e₁ simpBody
+public def simpHaveAndZetaUnused (e₁ : Expr) : SimpM Result := do
+  let r ← simpHaveCore e₁
   match r.result with
   | .rfl _ =>
     let e₂ ← zetaUnused e₁
@@ -426,7 +425,7 @@ public def simpHaveAndZetaUnused (e₁ : Expr) (simpBody : Simproc) : SimpM Resu
         (mkApp2 (mkConst ``Eq.refl [r.u]) r.α e₃)
       return .step e₃ h
 
-public def simpLet' (simpBody : Simproc) (e : Expr) : SimpM Result := do
+public def simpLet (e : Expr) : SimpM Result := do
   if !e.letNondep! then
     /-
     **Note**: We don't do anything if it is a dependent `let`.
@@ -434,9 +433,6 @@ public def simpLet' (simpBody : Simproc) (e : Expr) : SimpM Result := do
     -/
     return .rfl
   else
-    simpHaveAndZetaUnused e simpBody
-
-public def simpLet : Simproc :=
-  simpLet' simpLambda
+    simpHaveAndZetaUnused e
 
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Simp/Lambda.lean

@@ -46,12 +46,12 @@ def mkFunextFor (xs : Array Expr) (β : Expr) : MetaM Expr := do
   let result ← mkLambdaFVars #[f, g, h] result
   return result
 
-public def simpLambda' (simpBody : Simproc) (e : Expr) : SimpM Result := do
+public def simpLambda (e : Expr) : SimpM Result := do
   lambdaTelescope e fun xs b => withoutModifyingCacheIfNotWellBehaved do
     main xs (← shareCommon b)
 where
   main (xs : Array Expr) (b : Expr) : SimpM Result := do
-    match (← simpBody b) with
+    match (← simp b) with
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
@@ -69,7 +69,4 @@ where
       modify fun s => { s with funext := s.funext.insert { expr := key } h }
       return h
 
-public def simpLambda : Simproc :=
-  simpLambda' simp
-
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Simp/Result.lean

@@ -26,8 +26,4 @@ public def Result.markAsDone : Result → Result
   | .rfl _ => .rfl true
   | .step e h _ => .step e h true
 
-public def Result.getResultExpr : Expr → Result → Expr
-  | e, .rfl _ => e
-  | _, .step e _ _ => e
-
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Simp/Telescope.lean

@@ -1,25 +0,0 @@
-/-
-Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-module
-prelude
-public import Lean.Meta.Sym.Simp.SimpM
-import Lean.Meta.Sym.Simp.Have
-import Lean.Meta.Sym.Simp.Forall
-namespace Lean.Meta.Sym.Simp
-/--
-Simplify telescope binders (`have`-expression values, and arrow hypotheses)
-but not the final body. This simproc is useful to simplify target before
-introducing.
--/
-public partial def simpTelescope : Simproc := fun e => do
-  match e with
-  | .letE .. =>
-    simpLet' (simpLambda' simpTelescope) e
-  | .forallE .. =>
-    simpForall' (simpArrow := simpArrowTelescope simpTelescope) (simpBody := simpLambda' simpTelescope) e
-  | _ => return .rfl
-
-end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/SymM.lean

@@ -157,12 +157,8 @@ def getSharedExprs : SymM SharedExprs :=
 
 /-- Returns the internalized `True` constant.  -/
 def getTrueExpr : SymM Expr := return (← getSharedExprs).trueExpr
-/-- Returns `true` if `e` is the internalized `True` expression.  -/
-def isTrueExpr (e : Expr) : SymM Bool := return isSameExpr e (← getTrueExpr)
 /-- Returns the internalized `False` constant.  -/
 def getFalseExpr : SymM Expr := return (← getSharedExprs).falseExpr
-/-- Returns `true` if `e` is the internalized `False` expression.  -/
-def isFalseExpr (e : Expr) : SymM Bool := return isSameExpr e (← getFalseExpr)
 /-- Returns the internalized `Bool.true`.  -/
 def getBoolTrueExpr : SymM Expr := return (← getSharedExprs).btrueExpr
 /-- Returns the internalized `Bool.false`.  -/

src/Lean/Meta/Tactic/FunInd.lean

@@ -658,6 +658,7 @@ partial def buildInductionBody (toErase toClear : Array FVarId) (goal : Expr)
     return mkApp4 (mkConst ``Bool.dcond [u]) goal c' t' f'
   | _ =>
 
+
   -- Check for unreachable cases. We look for the kind of expressions that `by contradiction`
   -- produces
   if e.isAppOf ``False.elim && 1 < e.getAppNumArgs then
@@ -845,7 +846,7 @@ where doRealize (inductName : Name) := do
             throwError "Function {name} defined via WellFounded.fix with unexpected arity {funBody.getAppNumArgs}:{indentExpr funBody}"
           else
             throwError "Function {name} not defined via WellFounded.fix:{indentExpr funBody}"
-
+      check e'
       let (body', mvars) ← M2.run do
         forallTelescope (← inferType e').bindingDomain! fun xs goal => do
           if xs.size ≠ 2 then
@@ -875,6 +876,10 @@ where doRealize (inductName : Name) := do
       let e' ← instantiateMVars e'
       return (e', paramMask)
 
+  unless (← isTypeCorrect e') do
+    logError m!"failed to derive a type-correct induction principle:{indentExpr e'}"
+    check e'
+
   let eTyp ← inferType e'
   let eTyp ← elimTypeAnnotations eTyp
   let eTyp ← letToHave eTyp
@@ -1061,9 +1066,13 @@ where doRealize inductName := do
         let value ← mkLambdaFVars alts value
         let value ← mkLambdaFVars motives value
         let value ← mkLambdaFVars params value
+        check value
         let value ← cleanPackedArgs eqnInfo value
         return value
 
+  unless ← isTypeCorrect value do
+    logError m!"final term is type incorrect:{indentExpr value}"
+    check value
   let type ← inferType value
   let type ← elimOptParam type
   let type ← letToHave type
@@ -1293,6 +1302,10 @@ where doRealize inductName := do
           trace[Meta.FunInd] "complete body of mutual induction principle:{indentExpr e'}"
           pure (e', paramMask, motiveArities)
 
+  unless (← isTypeCorrect e') do
+    logError m!"constructed induction principle is not type correct:{indentExpr e'}"
+    check e'
+
   let eTyp ← inferType e'
   let eTyp ← elimTypeAnnotations eTyp
   let eTyp ← letToHave eTyp
@@ -1431,6 +1444,9 @@ def deriveCases (unfolding : Bool) (name : Name) : MetaM Unit := do
             let e' ← mkLambdaFVars #[motive] e'
             mkLambdaFVarsMasked params e'
 
+    mapError (f := (m!"constructed functional cases principle is not type correct:{indentExpr e'}\n{indentD ·}")) do
+      check e'
+
     let eTyp ← inferType e'
     let eTyp ← elimTypeAnnotations eTyp
     let eTyp ← letToHave eTyp

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

@@ -162,7 +162,7 @@ structure Context where
   extensions   : ExtensionStateArray := #[]
   debug        : Bool -- Cached `grind.debug (← getOptions)`
 
-export Sym (getTrueExpr getFalseExpr getBoolTrueExpr getBoolFalseExpr getNatZeroExpr getOrderingEqExpr getIntExpr isTrueExpr isFalseExpr)
+export Sym (getTrueExpr getFalseExpr getBoolTrueExpr getBoolFalseExpr getNatZeroExpr getOrderingEqExpr getIntExpr)
 
 /-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
@@ -379,6 +379,14 @@ Abstracts nested proofs in `e`. This is a preprocessing step performed before in
 def abstractNestedProofs (e : Expr) : GrindM Expr :=
   Meta.abstractNestedProofs e
 
+/-- Returns `true` if `e` is the internalized `True` expression.  -/
+def isTrueExpr (e : Expr) : GrindM Bool :=
+  return isSameExpr e (← getTrueExpr)
+
+/-- Returns `true` if `e` is the internalized `False` expression.  -/
+def isFalseExpr (e : Expr) : GrindM Bool :=
+  return isSameExpr e (← getFalseExpr)
+
 /--
 Creates a congruence theorem for a `f`-applications with `numArgs` arguments.
 -/
@@ -1107,11 +1115,11 @@ def getGeneration (e : Expr) : GoalM Nat :=
 
 /-- Returns `true` if `e` is in the equivalence class of `True`. -/
 def isEqTrue (e : Expr) : GoalM Bool := do
-  return (← isTrueExpr (← getENode e).root)
+  return isSameExpr (← getENode e).root (← getTrueExpr)
 
 /-- Returns `true` if `e` is in the equivalence class of `False`. -/
 def isEqFalse (e : Expr) : GoalM Bool := do
-  return (← isFalseExpr (← getENode e).root)
+  return isSameExpr (← getENode e).root (← getFalseExpr)
 
 /-- Returns `true` if `e` is in the equivalence class of `Bool.true`. -/
 def isEqBoolTrue (e : Expr) : GoalM Bool := do

src/Lean/Util/Trace.lean

@@ -270,9 +270,9 @@ withTraceNode `isPosTrace (msg := (return m!"{ExceptToEmoji.toEmoji ·} checking
 
 The `cls`, `collapsed`, and `tag` arguments are forwarded to the constructor of `TraceData`.
 -/
-@[inline]
 def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls : Name)
     (msg : Except ε α → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do
+  let _ := always.except
   let opts ← getOptions
   if !opts.hasTrace then
     return (← k)
@@ -280,27 +280,21 @@ def withTraceNode [always : MonadAlwaysExcept ε m] [MonadLiftT BaseIO m] (cls :
   unless clsEnabled || trace.profiler.get opts do
     return (← k)
   let oldTraces ← getResetTraces
-  let resStartStop ← withStartStop opts <| let _ := always.except; observing k
-  postCallback opts clsEnabled oldTraces msg resStartStop
-where
-  postCallback (opts : Options) (clsEnabled oldTraces msg resStartStop) : m α := do
-    let _ := always.except
-    let (res, start, stop) := resStartStop
-    let aboveThresh := trace.profiler.get opts &&
-      stop - start > trace.profiler.threshold.unitAdjusted opts
-    unless clsEnabled || aboveThresh do
-      modifyTraces (oldTraces ++ ·)
-      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 }
-    if trace.profiler.get opts then
-      data := { data with startTime := start, stopTime := stop }
-    addTraceNode oldTraces data ref m
-    MonadExcept.ofExcept res
+  let (res, start, stop) ← withStartStop opts <| observing k
+  let aboveThresh := trace.profiler.get opts &&
+    stop - start > trace.profiler.threshold.unitAdjusted opts
+  unless clsEnabled || aboveThresh do
+    modifyTraces (oldTraces ++ ·)
+    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 }
+  if trace.profiler.get opts then
+    data := { data with startTime := start, stopTime := stop }
+  addTraceNode oldTraces data ref m
+  MonadExcept.ofExcept res
 
 /-- A version of `Lean.withTraceNode` which allows generating the message within the computation. -/
-@[inline]
 def withTraceNode' [MonadAlwaysExcept Exception m] [MonadLiftT BaseIO m] (cls : Name)
     (k : m (α × MessageData)) (collapsed := true) (tag := "") : m α :=
   let msg := fun
@@ -386,10 +380,10 @@ the result produced by `k` into an emoji (e.g., `💥️`, `✅️`, `❌️`).
 
 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)
     (msg : Unit → m MessageData) (k : m α) (collapsed := true) (tag := "") : m α := do
+  let _ := always.except
   let opts ← getOptions
   if !opts.hasTrace then
     return (← k)
@@ -400,23 +394,18 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m]
   let ref ← getRef
   -- make sure to preserve context *before* running `k`
   let msg ← withRef ref do addMessageContext (← msg ())
-  let resStartStop ← withStartStop opts <| let _ := always.except; observing k
-  postCallback opts clsEnabled oldTraces ref msg resStartStop
-where
-  postCallback (opts : Options) (clsEnabled oldTraces ref msg resStartStop) : m α := do
-    let _ := always.except
-    let (res, start, stop) := resStartStop
-    let aboveThresh := trace.profiler.get opts &&
-      stop - start > trace.profiler.threshold.unitAdjusted opts
-    unless clsEnabled || aboveThresh do
-      modifyTraces (oldTraces ++ ·)
-      return (← MonadExcept.ofExcept res)
-    let mut msg := m!"{ExceptToEmoji.toEmoji res} {msg}"
-    let mut data := { cls, collapsed, tag }
-    if trace.profiler.get opts then
-      data := { data with startTime := start, stopTime := stop }
-    addTraceNode oldTraces data ref msg
-    MonadExcept.ofExcept res
+  let (res, start, stop) ← withStartStop opts <| observing k
+  let aboveThresh := trace.profiler.get opts &&
+    stop - start > trace.profiler.threshold.unitAdjusted opts
+  unless clsEnabled || aboveThresh do
+    modifyTraces (oldTraces ++ ·)
+    return (← MonadExcept.ofExcept res)
+  let mut msg := m!"{ExceptToEmoji.toEmoji res} {msg}"
+  let mut data := { cls, collapsed, tag }
+  if trace.profiler.get opts then
+    data := { data with startTime := start, stopTime := stop }
+  addTraceNode oldTraces data ref msg
+  MonadExcept.ofExcept res
 
 def addTraceAsMessages [Monad m] [MonadRef m] [MonadLog m] [MonadTrace m] : m Unit := do
   if trace.profiler.output.get? (← getOptions) |>.isSome then

src/Std/Do/PostCond.lean

@@ -330,7 +330,7 @@ abbrev PostCond (α : Type u) (ps : PostShape.{u}) : Type u :=
 
 @[inherit_doc PostCond]
 scoped macro:max "post⟨" handlers:term,+,? "⟩" : term =>
-  `(by exact ⟨$handlers,*, PUnit.unit⟩)
+  `(by exact ⟨$handlers,*, ()⟩)
   -- NB: Postponement through by exact is the entire point of this macro
   -- until https://github.com/leanprover/lean4/pull/8074 lands
 

src/Std/Do/WP/Basic.lean

@@ -143,27 +143,12 @@ you want to use `mvcgen` to reason about `prog`.
 theorem ReaderM.of_wp_run_eq {α} {x : α} {prog : ReaderM ρ α} (h : ReaderT.run prog r = x) (P : α → Prop) :
   (⊢ₛ wp⟦prog⟧ (⇓ a _ => ⌜P a⌝) r) → P x := h ▸ (· True.intro)
 
-/--
-Adequacy lemma for `Except`.
-Useful if you want to prove a property about a complex expression `prog : Except ε α` that you have
-generalized to a variable `x` and you want to use `mvcgen` to reason about `prog`.
--/
-theorem Except.of_wp_eq {ε α : Type u} {x prog : Except ε α} (h : prog = x) (P : Except ε α → Prop) :
-    (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.error e)⌝⟩) → P x := by
-  subst h
-  intro hspec
-  simp only [wp, PredTrans.pushExcept_apply, PredTrans.pure_apply] at hspec
-  split at hspec
-  case h_1 a s' heq => rw[← heq] at hspec; exact hspec True.intro
-  case h_2 e s' heq => rw[← heq] at hspec; exact hspec True.intro
-
 /--
 Adequacy lemma for `Except`.
 Useful if you want to prove a property about an expression `prog : Except ε α` and you want to use
 `mvcgen` to reason about `prog`.
 -/
-@[deprecated Except.of_wp_eq (since := "2026-01-26")]
-theorem Except.of_wp {ε α : Type u} {prog : Except ε α} (P : Except ε α → Prop) :
+theorem Except.of_wp {α} {prog : Except ε α} (P : Except ε α → Prop) :
     (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.error e)⌝⟩) → P prog := by
   intro hspec
   simp only [wp, PredTrans.pushExcept_apply, PredTrans.pure_apply] at hspec
@@ -171,20 +156,6 @@ theorem Except.of_wp {ε α : Type u} {prog : Except ε α} (P : Except ε α
   case h_1 a s' heq => rw[← heq] at hspec; exact hspec True.intro
   case h_2 e s' heq => rw[← heq] at hspec; exact hspec True.intro
 
-/--
-Adequacy lemma for `Option`.
-Useful if you want to prove a property about a complex expression `prog : Option α` that you have
-generalized to a variable `x` and you want to use `mvcgen` to reason about `prog`.
--/
-theorem Option.of_wp_eq {α : Type u} {x prog : Option α} (h : prog = x) (P : Option α → Prop) :
-    (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x := by
-  subst h
-  intro hspec
-  simp only [wp, PredTrans.pushOption_apply, PredTrans.pure_apply] at hspec
-  split at hspec
-  case h_1 a s' heq => rw[← heq] at hspec; exact hspec True.intro
-  case h_2   s' heq => rw[← heq] at hspec; exact hspec True.intro
-
 /--
 Adequacy lemma for `EStateM.run`.
 Useful if you want to prove a property about an expression `x` defined as `EStateM.run prog s` and

src/include/lean/lean.h

@@ -324,6 +324,55 @@ LEAN_EXPORT LEAN_NORETURN void lean_internal_panic(char const * msg);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_out_of_memory(void);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_unreachable(void);
 LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_rc_overflow(void);
+LEAN_EXPORT LEAN_NORETURN void lean_internal_panic_overflow(void);
+
+static inline bool lean_usize_mul_would_overflow(size_t a, size_t b) {
+#if defined(__GNUC__) || defined(__clang__)
+    size_t r;
+    return __builtin_mul_overflow(a, b, &r);
+#else
+    return a != 0 && b > SIZE_MAX / a;
+#endif
+}
+
+static inline bool lean_usize_add_would_overflow(size_t a, size_t b) {
+#if defined(__GNUC__) || defined(__clang__)
+    size_t r;
+    return __builtin_add_overflow(a, b, &r);
+#else
+    return a > SIZE_MAX - b;
+#endif
+}
+
+static inline size_t lean_usize_mul_checked(size_t a, size_t b) {
+#if defined(__GNUC__) || defined(__clang__)
+    size_t r;
+    if (LEAN_UNLIKELY(__builtin_mul_overflow(a, b, &r))) {
+        lean_internal_panic_overflow();
+    }
+    return r;
+#else
+    if (a != 0 && b > SIZE_MAX / a) {
+        lean_internal_panic_overflow();
+    }
+    return a * b;
+#endif
+}
+
+static inline size_t lean_usize_add_checked(size_t a, size_t b) {
+#if defined(__GNUC__) || defined(__clang__)
+    size_t r;
+    if (LEAN_UNLIKELY(__builtin_add_overflow(a, b, &r))) {
+        lean_internal_panic_overflow();
+    }
+    return r;
+#else
+    if (a > SIZE_MAX - b) {
+        lean_internal_panic_overflow();
+    }
+    return a + b;
+#endif
+}
 
 static inline size_t lean_align(size_t v, size_t a) {
     return (v / a)*a + a * (v % a != 0);
@@ -609,7 +658,7 @@ static inline uint8_t * lean_ctor_scalar_cptr(lean_object * o) {
 
 static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, unsigned scalar_sz) {
     assert(tag <= LeanMaxCtorTag && num_objs < LEAN_MAX_CTOR_FIELDS && scalar_sz < LEAN_MAX_CTOR_SCALARS_SIZE);
-    lean_object * o = lean_alloc_ctor_memory(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz);
+    lean_object * o = lean_alloc_ctor_memory(lean_usize_add_checked(lean_usize_add_checked(sizeof(lean_ctor_object), lean_usize_mul_checked(sizeof(void*), num_objs)), scalar_sz));
     lean_set_st_header(o, tag, num_objs);
     return o;
 }
@@ -715,7 +764,7 @@ static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lea
 static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) {
     assert(arity > 0);
     assert(num_fixed < arity);
-    lean_closure_object * o = (lean_closure_object*)lean_alloc_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
+    lean_closure_object * o = (lean_closure_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_closure_object), lean_usize_mul_checked(sizeof(void*), num_fixed)));
     lean_set_st_header((lean_object*)o, LeanClosure, 0);
     o->m_fun = fun;
     o->m_arity = arity;
@@ -761,7 +810,7 @@ LEAN_EXPORT lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object**
 
 /* Arrays of objects (low level API) */
 static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) {
-    lean_array_object * o = (lean_array_object*)lean_alloc_object(sizeof(lean_array_object) + sizeof(void*)*capacity);
+    lean_array_object * o = (lean_array_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_array_object), lean_usize_mul_checked(sizeof(void*), capacity)));
     lean_set_st_header((lean_object*)o, LeanArray, 0);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -934,8 +983,18 @@ LEAN_EXPORT lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);
 
 /* Array of scalars */
 
+static inline bool lean_alloc_sarray_would_overflow(unsigned elem_size, size_t capacity) {
+    if (lean_usize_mul_would_overflow(elem_size, capacity)) {
+        return true;
+    }
+    if (lean_usize_add_would_overflow(sizeof(lean_sarray_object), elem_size * capacity)) {
+        return true;
+    }
+    return false;
+}
+
 static inline lean_obj_res lean_alloc_sarray(unsigned elem_size, size_t size, size_t capacity) {
-    lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(sizeof(lean_sarray_object) + elem_size*capacity);
+    lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_sarray_object), lean_usize_mul_checked(elem_size, capacity)));
     lean_set_st_header((lean_object*)o, LeanScalarArray, elem_size);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -1090,7 +1149,7 @@ static inline lean_obj_res lean_float_array_set(lean_obj_arg a, b_lean_obj_arg i
 /* Strings */
 
 static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_t len) {
-    lean_string_object * o = (lean_string_object*)lean_alloc_object(sizeof(lean_string_object) + capacity);
+    lean_string_object * o = (lean_string_object*)lean_alloc_object(lean_usize_add_checked(sizeof(lean_string_object), capacity));
     lean_set_st_header((lean_object*)o, LeanString, 0);
     o->m_size = size;
     o->m_capacity = capacity;
@@ -3175,12 +3234,6 @@ static inline lean_obj_res lean_manual_get_root(lean_obj_arg _unit) {
     return lean_mk_string(LEAN_MANUAL_ROOT);
 }
 
-#ifdef LEAN_EMSCRIPTEN
-#define LEAN_SCALAR_PTR_LITERAL(b1, b2, b3, b4, b5, b6, b7, b8) (lean_object*)((uint32_t)b1 | ((uint32_t)b2 << 8) | ((uint32_t)b3 << 16) | ((uint32_t)b4 << 24)), (lean_object*)((uint32_t)b5 | ((uint32_t)b6 << 8) | ((uint32_t)b7 << 16) | ((uint32_t)b8 << 24))
-#else
-#define LEAN_SCALAR_PTR_LITERAL(b1, b2, b3, b4, b5, b6, b7, b8) (lean_object*)((uint64_t)b1 | ((uint64_t)b2 << 8) | ((uint64_t)b3 << 16) | ((uint64_t)b4 << 24) | ((uint64_t)b5 << 32) | ((uint64_t)b6 << 40) | ((uint64_t)b7 << 48) | ((uint64_t)b8 << 56))
-#endif
-
 #ifdef __cplusplus
 }
 #endif

src/runtime/compact.cpp

@@ -143,7 +143,7 @@ object * object_compactor::copy_object(object * o) {
 void object_compactor::insert_sarray(object * o) {
     size_t sz        = lean_sarray_size(o);
     unsigned elem_sz = lean_sarray_elem_size(o);
-    size_t obj_sz = sizeof(lean_sarray_object) + elem_sz*sz;
+    size_t obj_sz = lean_usize_add_checked(sizeof(lean_sarray_object), lean_usize_mul_checked(elem_sz, sz));
     lean_sarray_object * new_o = (lean_sarray_object*)alloc(obj_sz);
     lean_set_non_heap_header_for_big((lean_object*)new_o, LeanScalarArray, elem_sz);
     new_o->m_size     = sz;
@@ -155,7 +155,7 @@ void object_compactor::insert_sarray(object * o) {
 void object_compactor::insert_string(object * o) {
     size_t sz        = lean_string_size(o);
     size_t len       = lean_string_len(o);
-    size_t obj_sz = sizeof(lean_string_object) + sz;
+    size_t obj_sz = lean_usize_add_checked(sizeof(lean_string_object), sz);
     lean_string_object * new_o = (lean_string_object*)alloc(obj_sz);
     lean_set_non_heap_header_for_big((lean_object*)new_o, LeanString, 0);
     new_o->m_size     = sz;
@@ -214,7 +214,7 @@ bool object_compactor::insert_array(object * o) {
     }
     if (missing_children)
         return false;
-    size_t obj_sz = sizeof(lean_array_object) + sizeof(void*)*sz;
+    size_t obj_sz = lean_usize_add_checked(sizeof(lean_array_object), lean_usize_mul_checked(sizeof(void*), sz));
     lean_array_object * new_o = (lean_array_object*)alloc(obj_sz);
     lean_set_non_heap_header_for_big((lean_object*)new_o, LeanArray, 0);
     new_o->m_size     = sz;
@@ -274,8 +274,8 @@ bool object_compactor::insert_promise(object * o) {
 void object_compactor::insert_mpz(object * o) {
 #ifdef LEAN_USE_GMP
     size_t nlimbs = mpz_size(to_mpz(o)->m_value.m_val);
-    size_t data_sz = sizeof(mp_limb_t) * nlimbs;
-    size_t sz = sizeof(mpz_object) + data_sz;
+    size_t data_sz = lean_usize_mul_checked(sizeof(mp_limb_t), nlimbs);
+    size_t sz = lean_usize_add_checked(sizeof(mpz_object), data_sz);
     mpz_object * new_o = (mpz_object *)alloc(sz);
     memcpy(new_o, to_mpz(o), sizeof(mpz_object));
     lean_set_non_heap_header((lean_object*)new_o, sz, LeanMPZ, 0);
@@ -287,8 +287,8 @@ void object_compactor::insert_mpz(object * o) {
     m._mp_alloc = nlimbs;
     save(o, (lean_object*)new_o);
 #else
-    size_t data_sz = sizeof(mpn_digit) * to_mpz(o)->m_value.m_size;
-    size_t sz      = sizeof(mpz_object) + data_sz;
+    size_t data_sz = lean_usize_mul_checked(sizeof(mpn_digit), to_mpz(o)->m_value.m_size);
+    size_t sz      = lean_usize_add_checked(sizeof(mpz_object), data_sz);
     mpz_object * new_o = (mpz_object *)alloc(sz);
     // Manually copy the `mpz_object` to ensure `mpz` struct padding is left as
     // zero as prepared by `object_compactor::alloc`. `memcpy` would copy the

src/runtime/exception.cpp

@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "runtime/exception.h"
 #include "runtime/thread.h"
 #include "runtime/sstream.h"
-#include <lean/version.h>
 
 namespace lean {
 throwable::throwable(char const * msg):m_msg(msg) {}
@@ -19,7 +18,7 @@ throwable::~throwable() noexcept {}
 char const * throwable::what() const noexcept { return m_msg.c_str(); }
 
 stack_space_exception::stack_space_exception(char const * component_name):
-    m_msg((sstream() << "deep recursion was detected at '" << component_name << "' (potential solution: increase elaboration stack size using the `lean --tstack` flag). This flag can be set in the `weakLeanArgs` field of the Lake configuration. Further details are available in the Lean reference manual at " << LEAN_MANUAL_ROOT << "find/?domain=Verso.Genre.Manual.section&name=lake-config-toml").str()) {
+    m_msg((sstream() << "deep recursion was detected at '" << component_name << "' (potential solution: increase stack space in your system)").str()) {
 }
 
 memory_exception::memory_exception(char const * component_name):

src/runtime/io.cpp

@@ -583,6 +583,9 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h) {
 /* Handle.read : (@& Handle) → USize → IO ByteArray */
 extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes) {
     FILE * fp = io_get_handle(h);
+    if (lean_alloc_sarray_would_overflow(1, nbytes)) {
+        return io_result_mk_error(decode_io_error(ENOMEM, NULL));
+    }
     obj_res res = lean_alloc_sarray(1, 0, nbytes);
     usize n = std::fread(lean_sarray_cptr(res), 1, nbytes, fp);
     if (n > 0) {
@@ -861,6 +864,9 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes) {
     }
 #endif
 
+    if (lean_alloc_sarray_would_overflow(1, nbytes)) {
+        return io_result_mk_error(decode_io_error(ENOMEM, NULL));
+    }
     obj_res res = lean_alloc_sarray(1, 0, nbytes);
     size_t remain = nbytes;
     uint8_t *dst = lean_sarray_cptr(res);

src/runtime/mpz.cpp

@@ -340,7 +340,7 @@ static void mpz_dealloc(void *ptr, size_t size) {
 
 void mpz::allocate(size_t s) {
     m_size   = s;
-    m_digits = static_cast<mpn_digit*>(mpz_alloc(s * sizeof(mpn_digit)));
+    m_digits = static_cast<mpn_digit*>(mpz_alloc(lean_usize_mul_checked(s, sizeof(mpn_digit))));
 }
 
 void mpz::init() {
@@ -409,8 +409,8 @@ void mpz::init_int64(int64 v) {
 void mpz::init_mpz(mpz const & v) {
     m_sign   = v.m_sign;
     m_size   = v.m_size;
-    m_digits = static_cast<mpn_digit*>(mpz_alloc(m_size * sizeof(mpn_digit)));
-    memcpy(m_digits, v.m_digits, m_size * sizeof(mpn_digit));
+    m_digits = static_cast<mpn_digit*>(mpz_alloc(lean_usize_mul_checked(m_size, sizeof(mpn_digit))));
+    memcpy(m_digits, v.m_digits, lean_usize_mul_checked(m_size, sizeof(mpn_digit)));
 }
 
 mpz::mpz() {

src/runtime/object.cpp

@@ -99,6 +99,10 @@ extern "C" LEAN_EXPORT void lean_internal_panic_rc_overflow() {
     lean_internal_panic("reference counter overflowed");
 }
 
+extern "C" LEAN_EXPORT void lean_internal_panic_overflow() {
+    lean_internal_panic("integer overflow in runtime computation");
+}
+
 bool g_exit_on_panic = false;
 bool g_panic_messages = true;
 

src/runtime/uv/tcp.cpp

@@ -182,6 +182,9 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d
     }
 
     // Allocate buffer array for uv_write
+    if (lean_usize_mul_would_overflow(array_len, sizeof(uv_buf_t))) {
+        return lean_io_result_mk_error(decode_io_error(ENOMEM, nullptr));
+    }
     uv_buf_t* bufs = (uv_buf_t*)malloc(array_len * sizeof(uv_buf_t));
 
     for (size_t i = 0; i < array_len; i++) {

src/runtime/uv/udp.cpp

@@ -140,6 +140,9 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg d
         return lean_io_result_mk_ok(promise);
     }
 
+    if (lean_usize_mul_would_overflow(array_len, sizeof(uv_buf_t))) {
+        return lean_io_result_mk_error(decode_io_error(ENOMEM, nullptr));
+    }
     uv_buf_t* bufs = (uv_buf_t*)malloc(array_len * sizeof(uv_buf_t));
 
     for (size_t i = 0; i < array_len; i++) {